Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems

Silvio Ghilardi 1 Enrica Nicolini 2 Silvio Ranise 2 Daniele Zucchelli 1, 2
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Manna and Pnueli have extensively shown how a mixture of first-order logic (FOL) and discrete Linear time Temporal Logic (LTL) is sufficient to precisely state verification problems for the class of reactive systems. Theories in FOL model the (possibly infinite) data structures used by a reactive system while LTL specifies its (dynamic) behavior. In this paper, we derive undecidability and decidability results for both the satisfiability of (quantifier-free) formulae and the model-checking of safety properties by lifting combination methods for (non-disjoint) theories in FOL. The proofs of our decidability results suggest how decision procedures for the constraint satisfiability problem of theories in FOL and algorithms for checking the satisfiability of propositional LTL formulae can be integrated. This paves the way to employ efficient Satisfiability Modulo Theories solvers in the model-checking of infinite state systems. We illustrate our techniques on two examples.
Type de document :
Communication dans un congrès
Frank Pfenning. Automated Deduction - CADE-21, Jul 2007, Bremen, Germany. Springer, 4603, pp.362-378, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-73595-3_25〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00576597
Contributeur : Christophe Ringeissen <>
Soumis le : lundi 14 mars 2011 - 17:32:54
Dernière modification le : jeudi 11 janvier 2018 - 06:20:00

Identifiants

Citation

Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli. Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. Frank Pfenning. Automated Deduction - CADE-21, Jul 2007, Bremen, Germany. Springer, 4603, pp.362-378, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-73595-3_25〉. 〈inria-00576597〉

Partager

Métriques

Consultations de la notice

76