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 nonautomatic 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. © 2012 Springer-Verlag.
CITATION STYLE
Héam, P. C., Hugot, V., & Kouchnarenko, O. (2012). From linear temporal logic properties to rewrite propositions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7364 LNAI, pp. 316–331). https://doi.org/10.1007/978-3-642-31365-3_25
Mendeley helps you to discover research relevant for your work.