From LTL to deterministic automata: A safraless compositional approach

J. Esparza, J. Kretinsky, in:, Springer, 2014, pp. 192–208.


Conference Paper | Published | English
Author
;
Series Title
LNCS
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.
Publishing Year
Date Published
2014-01-01
Acknowledgement
The author is on leave from Faculty of Informatics, Masaryk University, Czech Republic, and partially supported by the Czech Science Foundation, grant No. P202/12/G061.
Volume
8559
Page
192 - 208
Conference
CAV: Computer Aided Verification
IST-REx-ID

Cite this

Esparza J, Kretinsky J. From LTL to deterministic automata: A safraless compositional approach. In: Vol 8559. Springer; 2014:192-208. doi:10.1007/978-3-319-08867-9_13
Esparza, J., & Kretinsky, J. (2014). From LTL to deterministic automata: A safraless compositional approach (Vol. 8559, pp. 192–208). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-319-08867-9_13
Esparza, Javier, and Jan Kretinsky. “From LTL to Deterministic Automata: A Safraless Compositional Approach,” 8559:192–208. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_13.
J. Esparza and J. Kretinsky, “From LTL to deterministic automata: A safraless compositional approach,” presented at the CAV: Computer Aided Verification, 2014, vol. 8559, pp. 192–208.
Esparza J, Kretinsky J. 2014. From LTL to deterministic automata: A safraless compositional approach. CAV: Computer Aided Verification, LNCS, vol. 8559. 192–208.
Esparza, Javier, and Jan Kretinsky. From LTL to Deterministic Automata: A Safraless Compositional Approach. Vol. 8559, Springer, 2014, pp. 192–208, doi:10.1007/978-3-319-08867-9_13.

Link(s) to Main File(s)
Access Level
OA Open Access

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar