Rabinizer 4: From LTL to your favourite deterministic automaton

Jan Křetínský; Tobias Meggendorfer; Salomon Sickert; Christopher Ziegler

doi:10.1007/978-3-319-96145-3_30

Rabinizer 4: From LTL to your favourite deterministic automaton

Jan Křetínský, Tobias Meggendorfer, Salomon Sickert, Christopher Ziegler

Technical University of Munich

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

32 Scopus citations

Abstract

We present Rabinizer 4, a tool set for translating formulae of linear temporal logic to different types of deterministic ω-automata. The tool set implements and optimizes several recent constructions, including the first implementation translating the frequency extension of LTL. Further, we provide a distribution of PRISM that links Rabinizer and offers model checking procedures for probabilistic systems that are not in the official PRISM distribution. Finally, we evaluate the performance and in cases with any previous implementations we show enhancements both in terms of the size of the automata and the computational time, due to algorithmic as well as implementation improvements.

Original language	English
Title of host publication	Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
Editors	Georg Weissenbacher, Hana Chockler
Publisher	Springer Verlag
Pages	567-577
Number of pages	11
ISBN (Print)	9783319961446
DOIs	https://doi.org/10.1007/978-3-319-96145-3_30
State	Published - 2018
Event	30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom Duration: 14 Jul 2018 → 17 Jul 2018

Publication series

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

Conference

Conference	30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country/Territory	United Kingdom
City	Oxford
Period	14/07/18 → 17/07/18

Access to Document

10.1007/978-3-319-96145-3_30

Cite this

Křetínský, J., Meggendorfer, T., Sickert, S., & Ziegler, C. (2018). Rabinizer 4: From LTL to your favourite deterministic automaton. In G. Weissenbacher, & H. Chockler (Eds.), Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings (pp. 567-577). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10981 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-96145-3_30

Křetínský, Jan ; Meggendorfer, Tobias ; Sickert, Salomon et al. / Rabinizer 4 : From LTL to your favourite deterministic automaton. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. editor / Georg Weissenbacher ; Hana Chockler. Springer Verlag, 2018. pp. 567-577 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{1d16c55aa7e84fad802ba919a6481807,

title = "Rabinizer 4: From LTL to your favourite deterministic automaton",

abstract = "We present Rabinizer 4, a tool set for translating formulae of linear temporal logic to different types of deterministic ω-automata. The tool set implements and optimizes several recent constructions, including the first implementation translating the frequency extension of LTL. Further, we provide a distribution of PRISM that links Rabinizer and offers model checking procedures for probabilistic systems that are not in the official PRISM distribution. Finally, we evaluate the performance and in cases with any previous implementations we show enhancements both in terms of the size of the automata and the computational time, due to algorithmic as well as implementation improvements.",

author = "Jan K{\v r}et{\'i}nsk{\'y} and Tobias Meggendorfer and Salomon Sickert and Christopher Ziegler",

note = "Publisher Copyright: {\textcopyright} The Author(s) 2018.; 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 14-07-2018 Through 17-07-2018",

year = "2018",

doi = "10.1007/978-3-319-96145-3\_30",

language = "English",

isbn = "9783319961446",

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

publisher = "Springer Verlag",

pages = "567--577",

editor = "Georg Weissenbacher and Hana Chockler",

booktitle = "Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",

}

Křetínský, J , Meggendorfer, T, Sickert, S & Ziegler, C 2018, Rabinizer 4: From LTL to your favourite deterministic automaton. in G Weissenbacher & H Chockler (eds), Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10981 LNCS, Springer Verlag, pp. 567-577, 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 14/07/18. https://doi.org/10.1007/978-3-319-96145-3_30

Rabinizer 4: From LTL to your favourite deterministic automaton. / Křetínský, Jan ; Meggendorfer, Tobias; Sickert, Salomon et al.
Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. ed. / Georg Weissenbacher; Hana Chockler. Springer Verlag, 2018. p. 567-577 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10981 LNCS).

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

TY - GEN

T1 - Rabinizer 4

T2 - 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018

AU - Křetínský, Jan

AU - Meggendorfer, Tobias

AU - Sickert, Salomon

AU - Ziegler, Christopher

PY - 2018

Y1 - 2018

N2 - We present Rabinizer 4, a tool set for translating formulae of linear temporal logic to different types of deterministic ω-automata. The tool set implements and optimizes several recent constructions, including the first implementation translating the frequency extension of LTL. Further, we provide a distribution of PRISM that links Rabinizer and offers model checking procedures for probabilistic systems that are not in the official PRISM distribution. Finally, we evaluate the performance and in cases with any previous implementations we show enhancements both in terms of the size of the automata and the computational time, due to algorithmic as well as implementation improvements.

AB - We present Rabinizer 4, a tool set for translating formulae of linear temporal logic to different types of deterministic ω-automata. The tool set implements and optimizes several recent constructions, including the first implementation translating the frequency extension of LTL. Further, we provide a distribution of PRISM that links Rabinizer and offers model checking procedures for probabilistic systems that are not in the official PRISM distribution. Finally, we evaluate the performance and in cases with any previous implementations we show enhancements both in terms of the size of the automata and the computational time, due to algorithmic as well as implementation improvements.

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

U2 - 10.1007/978-3-319-96145-3_30

DO - 10.1007/978-3-319-96145-3_30

M3 - Conference contribution

AN - SCOPUS:85051105233

SN - 9783319961446

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

SP - 567

EP - 577

BT - Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings

A2 - Weissenbacher, Georg

A2 - Chockler, Hana

PB - Springer Verlag

Y2 - 14 July 2018 through 17 July 2018

ER -

Křetínský J , Meggendorfer T, Sickert S, Ziegler C. Rabinizer 4: From LTL to your favourite deterministic automaton. In Weissenbacher G, Chockler H, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer Verlag. 2018. p. 567-577. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-96145-3_30

Rabinizer 4: From LTL to your favourite deterministic automaton

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this