Translation of LTL to Büchi Automata: Improved Once Again

Investor logo

Warning

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

BABIAK Tomáš

Year of publication 2010
Type Article in Proceedings
Conference Proceedings of 9th International Summer School on Modelling and Verifying Parallel Processes 2010 (MOVEP 2010)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords LTL; linear time logic; translation of LTL; Büchi Automata; model checking
Description We present an improvement of an algorithm translating LTL formulae into Büchi automata via alternating automata. In particular, we improve the transformation of alternating Büchi automata to generalized Büchi automata, where we temporarily ignore some transitions leading from the alternating automata states corresponding to subformulae that are prefix-invariant. Experimental results show that our improvements can lead to faster translation and less nondeterminism of the resulting Büchi automata.
Related projects:

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