Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1187165, author = {Esparza, Javier and Křetínský, Jan}, address = {Heidelberg Dordrecht London New York}, booktitle = {Computer Aided Verification - 26th International Conference, CAV 2014}, doi = {http://dx.doi.org/10.1007/978-3-319-08867-9_13}, keywords = {linear temporal logic; automata; determinism; synthesis; probabilistic model checking}, howpublished = {tištěná verze "print"}, language = {eng}, location = {Heidelberg Dordrecht London New York}, isbn = {978-3-319-08866-2}, pages = {192-208}, publisher = {Springer}, title = {From LTL to Deterministic Automata: A Safraless Compositional Approach}, year = {2014} }
TY - JOUR ID - 1187165 AU - Esparza, Javier - Křetínský, Jan PY - 2014 TI - From LTL to Deterministic Automata: A Safraless Compositional Approach PB - Springer CY - Heidelberg Dordrecht London New York SN - 9783319088662 KW - linear temporal logic KW - automata KW - determinism KW - synthesis KW - probabilistic model checking N2 - 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. ER -
ESPARZA, Javier and Jan KŘETÍNSKÝ. From LTL to Deterministic Automata: A Safraless Compositional Approach. In \textit{Computer Aided Verification - 26th International Conference, CAV 2014}. Heidelberg Dordrecht London New York: Springer, 2014, p.~192-208. ISBN~978-3-319-08866-2. Available from: https://dx.doi.org/10.1007/978-3-319-08867-9\_{}13.
|