From Linear Temporal Logic Properties to Rewrite Propositions

Pierre-Cyrille Heam 1, 2 Vincent Hugot 1, 2 Olga Kouchnarenko 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 (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : In the regular model-checking framework, reachability analysis can be guided by temporal logic properties, for instance to achieve the counter example guided abstraction refinement (CEGAR) objectives. A way to perform this analysis is to translate a temporal logic formula expressed on maximal rewriting words into a ''rewrite proposition'' -- a propositional formula whose atoms are language comparisons, and then to generate semi-decision procedures based on (approximations of) the rewrite proposition. This approach has recently been studied using a non-automatic translation method. The extent to which such a translation can be systematised needs to be investigated, as well as the applicability of approximated methods wherever no exact translation can be effected. This paper presents contributions to that effect: 1) we investigate suitable semantics for LTL on maximal rewriting words and their influence on the feasibility of a translation, and 2) we propose a general scheme providing exact results on a fragment of LTL corresponding mainly to safety formulæ, and approximations on a larger fragment.
Type de document :
Communication dans un congrès
IJCAR - International Joint Conference on Automated Reasonning 2012, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.316-331, 2012, Lecture Notes in Computer Science. 〈http://link.springer.com/chapter/10.1007%2F978-3-642-31365-3_25?LI=true〉. 〈10.1007/978-3-642-31365-3_25〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00756598
Contributeur : Pierre-Cyrille Heam <>
Soumis le : vendredi 23 novembre 2012 - 12:51:58
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

Citation

Pierre-Cyrille Heam, Vincent Hugot, Olga Kouchnarenko. From Linear Temporal Logic Properties to Rewrite Propositions. IJCAR - International Joint Conference on Automated Reasonning 2012, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.316-331, 2012, Lecture Notes in Computer Science. 〈http://link.springer.com/chapter/10.1007%2F978-3-642-31365-3_25?LI=true〉. 〈10.1007/978-3-642-31365-3_25〉. 〈hal-00756598〉

Partager

Métriques

Consultations de la notice

204