Compositional Approach to Suspension and Other Improvements to LTL Translation

Investor logo

Warning

This publication doesn't include Institute of Computer Science. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BABIAK Tomáš BADIE Thomas DURET-LUTZ Alexandre KŘETÍNSKÝ Mojmír STREJČEK Jan

Year of publication 2013
Type Article in Proceedings
Conference Model Checking Software - 20th International Symposium, SPIN 2013
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-642-39176-7_6
Field Informatics
Keywords linear time logic; model-checking; translation LTL to Buchi automata
Description Recently, there was defined a fragment of LTL (containing fairness properties among other interesting formulae) whose validity over a given infinite word depends only on an arbitrary suffix of the word. Building upon an existing translation from LTL to Büchi automata, we introduce a compositional approach where subformulae of this fragment are translated separately from the rest of an input formula and the produced automata are composed in a way that the subformulae are checked only in relevant accepting strongly connected components of the final automaton. Further, we suggest improvements over some procedures commonly applied to generalized Büchi automata, namely over generalized acceptance simplification and over degeneralization. Finally we show how existing simulation-based reductions can be implemented in a signature-based framework in a way that improves the determinism of the automaton.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info