Rabinizer 3: Safraless translation of ltl to small deterministic automata

Zuzana Komárková; Jan Křetínský

doi:10.1007/978-3-319-11936-6_17

Rabinizer 3: Safraless translation of ltl to small deterministic automata

Zuzana Komárková
, Jan Křetínský

Masaryk University
Institute of Science and Technology Austria (ISTA)

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

34 Scopus citations

Abstract

We present a tool for translating LTL formulae into deterministic ω-automata. It is the first tool that covers the whole LTL that does not use Safra’s determinization or any of its variants. This leads to smaller automata. There are several outputs of the tool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic model checking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings
Editors	Franck Cassez, Jean-François Raskin
Publisher	Springer Verlag
Pages	235-241
Number of pages	7
ISBN (Electronic)	9783319119359
DOIs	https://doi.org/10.1007/978-3-319-11936-6_17
State	Published - 2014
Externally published	Yes
Event	12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014 - Sydney, Australia Duration: 3 Nov 2014 → 7 Nov 2014

Publication series

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

Conference

Conference	12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014
Country/Territory	Australia
City	Sydney
Period	3/11/14 → 7/11/14

Access to Document

10.1007/978-3-319-11936-6_17

Cite this

Komárková, Z., & Křetínský, J. (2014). Rabinizer 3: Safraless translation of ltl to small deterministic automata. In F. Cassez, & J.-F. Raskin (Eds.), Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings (pp. 235-241). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8837). Springer Verlag. https://doi.org/10.1007/978-3-319-11936-6_17

Komárková, Zuzana ; Křetínský, Jan. / Rabinizer 3 : Safraless translation of ltl to small deterministic automata. Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings. editor / Franck Cassez ; Jean-François Raskin. Springer Verlag, 2014. pp. 235-241 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{ff8c0f7935414e3c86a3121ba789aedd,

title = "Rabinizer 3: Safraless translation of ltl to small deterministic automata",

abstract = "We present a tool for translating LTL formulae into deterministic ω-automata. It is the first tool that covers the whole LTL that does not use Safra{\textquoteright}s determinization or any of its variants. This leads to smaller automata. There are several outputs of the tool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic model checking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata.",

author = "Zuzana Kom{\'a}rkov{\'a} and Jan K{\v r}et{\'i}nsk{\'y}",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2014.; 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014 ; Conference date: 03-11-2014 Through 07-11-2014",

year = "2014",

doi = "10.1007/978-3-319-11936-6\_17",

language = "English",

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

publisher = "Springer Verlag",

pages = "235--241",

editor = "Franck Cassez and Jean-Fran{\c c}ois Raskin",

booktitle = "Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings",

}

Komárková, Z & Křetínský, J 2014, Rabinizer 3: Safraless translation of ltl to small deterministic automata. in F Cassez & J-F Raskin (eds), Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8837, Springer Verlag, pp. 235-241, 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014, Sydney, Australia, 3/11/14. https://doi.org/10.1007/978-3-319-11936-6_17

Rabinizer 3: Safraless translation of ltl to small deterministic automata. / Komárková, Zuzana; Křetínský, Jan.
Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings. ed. / Franck Cassez; Jean-François Raskin. Springer Verlag, 2014. p. 235-241 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8837).

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

TY - GEN

T1 - Rabinizer 3

T2 - 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014

AU - Komárková, Zuzana

AU - Křetínský, Jan

PY - 2014

Y1 - 2014

N2 - We present a tool for translating LTL formulae into deterministic ω-automata. It is the first tool that covers the whole LTL that does not use Safra’s determinization or any of its variants. This leads to smaller automata. There are several outputs of the tool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic model checking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata.

AB - We present a tool for translating LTL formulae into deterministic ω-automata. It is the first tool that covers the whole LTL that does not use Safra’s determinization or any of its variants. This leads to smaller automata. There are several outputs of the tool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic model checking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata.

UR - https://www.scopus.com/pages/publications/84908673858

U2 - 10.1007/978-3-319-11936-6_17

DO - 10.1007/978-3-319-11936-6_17

M3 - Conference contribution

AN - SCOPUS:84908673858

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

SP - 235

EP - 241

BT - Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings

A2 - Cassez, Franck

A2 - Raskin, Jean-François

PB - Springer Verlag

Y2 - 3 November 2014 through 7 November 2014

ER -

Komárková Z, Křetínský J. Rabinizer 3: Safraless translation of ltl to small deterministic automata. In Cassez F, Raskin JF, editors, Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings. Springer Verlag. 2014. p. 235-241. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-11936-6_17

Rabinizer 3: Safraless translation of ltl to small deterministic automata

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this