Deterministic automata for the (F,G)-fragment of LTL

Jan Křetínský; Javier Esparza

doi:10.1007/978-3-642-31424-7_7

Deterministic automata for the (F,G)-fragment of LTL

Jan Křetínský, Javier Esparza

Masaryk University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

39 Scopus citations

Abstract

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 Büchi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic ω-automaton. We present a direct translation of the (F,G)-fragment of LTL into deterministic ω-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.

Original language	English
Title of host publication	Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings
Pages	7-22
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-31424-7_7
State	Published - 2012
Event	24th International Conference on Computer Aided Verification, CAV 2012 - Berkeley, CA, United States Duration: 7 Jul 2012 → 13 Jul 2012

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7358 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	24th International Conference on Computer Aided Verification, CAV 2012
Country/Territory	United States
City	Berkeley, CA
Period	7/07/12 → 13/07/12

Access to Document

10.1007/978-3-642-31424-7_7

Cite this

Křetínský, J., & Esparza, J. (2012). Deterministic automata for the (F,G)-fragment of LTL. In Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings (pp. 7-22). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7358 LNCS). https://doi.org/10.1007/978-3-642-31424-7_7

@inproceedings{f280040056b7489899e1ca8cb36fbce3,

title = "Deterministic automata for the (F,G)-fragment of LTL",

abstract = "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 B{\"u}chi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic ω-automaton. We present a direct translation of the (F,G)-fragment of LTL into deterministic ω-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.",

author = "Jan K{\v r}et{\'i}nsk{\'y} and Javier Esparza",

year = "2012",

doi = "10.1007/978-3-642-31424-7_7",

language = "English",

isbn = "9783642314230",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "7--22",

booktitle = "Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings",

note = "24th International Conference on Computer Aided Verification, CAV 2012 ; Conference date: 07-07-2012 Through 13-07-2012",

}

Křetínský, J & Esparza, J 2012, Deterministic automata for the (F,G)-fragment of LTL. in Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7358 LNCS, pp. 7-22, 24th International Conference on Computer Aided Verification, CAV 2012, Berkeley, CA, United States, 7/07/12. https://doi.org/10.1007/978-3-642-31424-7_7

Deterministic automata for the (F,G)-fragment of LTL. / Křetínský, Jan ; Esparza, Javier.
Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings. 2012. p. 7-22 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7358 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Deterministic automata for the (F,G)-fragment of LTL

AU - Křetínský, Jan

AU - Esparza, Javier

PY - 2012

Y1 - 2012

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 Büchi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic ω-automaton. We present a direct translation of the (F,G)-fragment of LTL into deterministic ω-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.

AB - 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 Büchi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic ω-automaton. We present a direct translation of the (F,G)-fragment of LTL into deterministic ω-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.

UR - http://www.scopus.com/inward/record.url?scp=84864069045&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-31424-7_7

DO - 10.1007/978-3-642-31424-7_7

M3 - Conference contribution

AN - SCOPUS:84864069045

SN - 9783642314230

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 7

EP - 22

BT - Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings

T2 - 24th International Conference on Computer Aided Verification, CAV 2012

Y2 - 7 July 2012 through 13 July 2012

ER -

Deterministic automata for the (F,G)-fragment of LTL

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this