Abstract
We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula φ. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of φ. The slave automaton for G ψ is in charge of recognizing whether FG ψ 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. © 2014 Springer International Publishing.
Cite
CITATION STYLE
Esparza, J., & Křetínský, J. (2014). From LTL to deterministic automata: A safraless compositional approach. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8559 LNCS, pp. 192–208). Springer Verlag. https://doi.org/10.1007/978-3-319-08867-9_13
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
