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

Warning

This publication doesn't include Faculty of Sports Studies. 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:	Highly Parallel and Distributed Computing Systems Verification and Analysis of Large-Scale Computer Systems Rozsáhlé výpočetní systémy: modely, aplikace a verifikace