Other formats:
BibTeX
LaTeX
RIS
@inproceedings{987377,
author = {Křetínský, Jan and Esparza, Javier},
address = {Heidelberg Dordrecht London New York},
booktitle = {Computer Aided Verification - 24th International Conference},
doi = {http://dx.doi.org/10.1007/978-3-642-31424-7_7},
keywords = {linear temporal logic; automata; determinism},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Heidelberg Dordrecht London New York},
isbn = {978-3-642-31423-0},
pages = {7-22},
publisher = {Springer},
title = {Deterministic Automata for the (F,G)-fragment of LTL},
year = {2012}
}
TY - JOUR
ID - 987377
AU - Křetínský, Jan - Esparza, Javier
PY - 2012
TI - Deterministic Automata for the (F,G)-fragment of LTL
PB - Springer
CY - Heidelberg Dordrecht London New York
SN - 9783642314230
KW - linear temporal logic
KW - automata
KW - determinism
N2 - When dealing with linear temporal logic properties in the setting of e.g. games or probabilistic systems, one often needs to express them as deterministic omega-automata. In order to translate LTL to deterministic omega-automata, the traditional approach first translates the formula to a non-deterministic Buchi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic omega-automaton. We present a direct translation of the (F,G)-fragment of LTL into deterministic omega-automata with no determinization procedure involved. Since our approach is tailored to LTL, we often avoid the typically unnecessarily large blowup caused by general determinization algorithms. We investigate the complexity of this translation and provide experimental results and compare them to the traditional method.
ER -
KŘETÍNSKÝ, Jan and Javier ESPARZA. Deterministic Automata for the (F,G)-fragment of LTL. In \textit{Computer Aided Verification - 24th International Conference}. Heidelberg Dordrecht London New York: Springer, 2012, p.~7-22. ISBN~978-3-642-31423-0. Available from: https://dx.doi.org/10.1007/978-3-642-31424-7\_{}7.
|
