| ESPARZA, Javier, Jan KŘETÍNSKÝ and Salomon SICKERT. From LTL to deterministic automata (A safraless compositional approach). Formal Methods in System Design. Springer Netherlands, 2016, vol. 49, No 3, p. 219-271. ISSN 0925-9856. Available from: https://dx.doi.org/10.1007/s10703-016-0259-2. |
Other formats:
BibTeX
LaTeX
RIS
@article{1365661,
author = {Esparza, Javier and Křetínský, Jan and Sickert, Salomon},
article_number = {3},
doi = {http://dx.doi.org/10.1007/s10703-016-0259-2},
keywords = {automata; verification; logic},
language = {eng},
issn = {0925-9856},
journal = {Formal Methods in System Design},
title = {From LTL to deterministic automata (A safraless compositional approach)},
volume = {49},
year = {2016}
}
TY - JOUR
ID - 1365661
AU - Esparza, Javier - Křetínský, Jan - Sickert, Salomon
PY - 2016
TI - From LTL to deterministic automata (A safraless compositional approach)
JF - Formal Methods in System Design
VL - 49
IS - 3
SP - 219-271
EP - 219-271
PB - Springer Netherlands
SN - 09259856
KW - automata
KW - verification
KW - logic
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 co-Büchi automaton for \phi and an array of Rabin automata, one for each G-subformula of \phi. The Rabin automaton for G\psi is in charge of recognizing whether FG\psi holds. This information is passed to the co-Büchi automaton that decides on acceptance. As opposed to standard procedures based on Safra’s determinization, the states of all our automata have a clear logical structure, which allows for various optimizations. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.
ER -
ESPARZA, Javier, Jan KŘETÍNSKÝ and Salomon SICKERT. From LTL to deterministic automata (A safraless compositional approach). \textit{Formal Methods in System Design}. Springer Netherlands, 2016, vol.~49, No~3, p.~219-271. ISSN~0925-9856. Available from: https://dx.doi.org/10.1007/s10703-016-0259-2.
|
