From LTL to Deterministic Automata: A Safraless Compositional Approach

Investor logo

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

ESPARZA Javier KŘETÍNSKÝ Jan

Year of publication 2014
Type Article in Proceedings
Conference Computer Aided Verification - 26th International Conference, CAV 2014
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-08867-9_13
Field Informatics
Keywords linear temporal logic; automata; determinism; synthesis; probabilistic model checking
Description We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula phi. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of phi. The slave automaton for G(psi) is in charge of recognizing whether FG(psi) holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.
Related projects:

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

More info