hal-00643416, version 1

From Linear Temporal Logic Properties to Rewrite Propositions

Pierre-Cyrille Heam ^a, 1, Vincent Hugot () ¹, Olga Kouchnarenko (, ) ¹

Work document (2011)

• a –  Université de Franche-Comté
• 1 :  CASSIS (INRIA Lorraine - LORIA / LIFC)
• 
  INRIA – CNRS : FRE2661 – Université de Franche-Comté – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL) France

Références bibliographiques

• Type de publication : Autres publications
• Domaine : Informatique/Logique en informatique
• Titre : From Linear Temporal Logic Properties to Rewrite Propositions
• Résumé : 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.
• Langue du document : Anglais
• Date de publication : 14/10/2011
• Description : Work document

• hal-00643416, version 1
• http://hal.inria.fr/hal-00643416
• oai:hal.inria.fr:hal-00643416
• Contributeur : Olga Kouchnarenko <>
• Soumis le : Lundi 21 Novembre 2011, 18:34:38
• Dernière modification le : Lundi 21 Novembre 2011, 18:34:38