Vérification de propriétés quantitatives sur des automates à contraintes

摘要

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.%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 model-checking 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.