From LTL to deterministic automata: A safraless compositional approach

Javier Esparza; Jan Křetínský

doi:10.1007/978-3-319-08867-9_13

From LTL to deterministic automata: A safraless compositional approach

Javier Esparza, Jan Křetínský

Institute of Science and Technology Austria (ISTA)

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

42 Scopus citations

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.

Original language	English
Title of host publication	Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
Publisher	Springer Verlag
Pages	192-208
Number of pages	17
ISBN (Print)	9783319088662
DOIs	https://doi.org/10.1007/978-3-319-08867-9_13
State	Published - 2014
Event	26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria Duration: 18 Jul 2014 → 22 Jul 2014

Publication series

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

Conference

Conference	26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014
Country/Territory	Austria
City	Vienna
Period	18/07/14 → 22/07/14

Access to Document

10.1007/978-3-319-08867-9_13

Cite this

Esparza, J., & Křetínský, J. (2014). From LTL to deterministic automata: A safraless compositional approach. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings (pp. 192-208). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8559 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-08867-9_13

Esparza, Javier ; Křetínský, Jan. / From LTL to deterministic automata : A safraless compositional approach. Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, 2014. pp. 192-208 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{7273bab393b5467d8073da7f22e441e0,

title = "From LTL to deterministic automata: A safraless compositional approach",

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.",

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

year = "2014",

doi = "10.1007/978-3-319-08867-9_13",

language = "English",

isbn = "9783319088662",

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

publisher = "Springer Verlag",

pages = "192--208",

booktitle = "Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings",

note = "26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 ; Conference date: 18-07-2014 Through 22-07-2014",

}

Esparza, J & Křetínský, J 2014, From LTL to deterministic automata: A safraless compositional approach. in Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8559 LNCS, Springer Verlag, pp. 192-208, 26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 18/07/14. https://doi.org/10.1007/978-3-319-08867-9_13

From LTL to deterministic automata: A safraless compositional approach. / Esparza, Javier ; Křetínský, Jan.
Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, 2014. p. 192-208 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8559 LNCS).

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

TY - GEN

T1 - From LTL to deterministic automata

T2 - 26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014

AU - Esparza, Javier

AU - Křetínský, Jan

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

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

U2 - 10.1007/978-3-319-08867-9_13

DO - 10.1007/978-3-319-08867-9_13

M3 - Conference contribution

AN - SCOPUS:84904787423

SN - 9783319088662

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

SP - 192

EP - 208

BT - Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings

PB - Springer Verlag

Y2 - 18 July 2014 through 22 July 2014

ER -

Esparza J , Křetínský J. From LTL to deterministic automata: A safraless compositional approach. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag. 2014. p. 192-208. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-08867-9_13

From LTL to deterministic automata: A safraless compositional approach

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this