ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 29/3 - 2010  - pp.309-344  - doi:10.3166/tsi.29.309-344
TITRE
Vérification de propriétés quantitatives sur des automates à contraintes

TITLE
Verification of quantitative properties on constraint automata

RÉSUMÉ
Nous définissons un cadre général pour l'extension des logiques temporelles avec des contraintes induites par un domaine concret, composé d'un domaine d'interprétation pour les variables et d'un ensemble de relations. Les extensions que nous considérons permettent de comparer la valeur des variables à différents états de l'exécution. Nous établissons des résultats de décidabilité et complexité pour plusieurs problèmes de modelchecking impliquant diverses instances de ces extensions. Nous privilégions pour cela l'approche à base d'automates en combinant des constructions connues pour les logiques temporelles avec différentes méthodes d'abstraction finie des modèles dont les variables sont interprétées dans des domaines infinis. Nous considérons divers fragments de logiques temporelles (linéaires et arborescentes) étendues avec des contraintes de Presburger.


ABSTRACT
We define a general framework for the extension of temporal logics with constraints induced by a concrete domain, made of an interpretation domain and a set of relations. The extensions we consider allow to compare values of the variables at different states of an execution. We establish decidability and complexity results for several model-checking problems involving several instances of such extensions. We mainly use automata-based techniques that combine some usual constructions for temporal logics with finite abstraction methods for infinite datas. For instance, we consider several fragments of (linear and branching-time) temporal logics extended with constraints on counters induced by Presburger arithmetic.


AUTEUR(S)
Régis GASCON

MOTS-CLÉS
vérification formelle, model-checking, systèmes infinis, logiques temporelles, méthodes à base d'automates, domaines concrets.

KEYWORDS
formal verification, model-checking, infinite systems, temporal logics, automata based approaches, concrete domains.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (427 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier