Rabinizer 4: From LTL to Your Favourite Deterministic Automaton

D 2018

Rabinizer 4: From LTL to Your Favourite Deterministic Automaton

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Salomon SICKERT a Christopher ZIEGLER

Základní údaje

Originální název

Rabinizer 4: From LTL to Your Favourite Deterministic Automaton

Autoři

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Salomon SICKERT a Christopher ZIEGLER

Vydání

Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, od s. 567-577, 11 s. 2018

Nakladatel

Springer

Další údaje

Typ výsledku

Stať ve sborníku

Označené pro přenos do RIV

Organizační jednotka

Fakulta informatiky

ISBN

9783319961446

ISSN

DOI

https://doi.org/10.1007/978-3-319-96145-3_30

Změněno: 17. 3. 2025 14:43, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Citovat

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Salomon SICKERT a Christopher ZIEGLER. Rabinizer 4: From LTL to Your Favourite Deterministic Automaton. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Springer, 2018, s. 567-577. ISBN 9783319961446. Dostupné z: https://doi.org/10.1007/978-3-319-96145-3_30.

@inproceedings{2484808,
   author = {Křetínský, Jan and Meggendorfer, Tobias and Sickert, Salomon and Ziegler, Christopher},
   booktitle = {Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I},
   doi = {https://doi.org/10.1007/978-3-319-96145-3_30},
   isbn = {9783319961446},
   pages = {567-577},
   publisher = {Springer},
   title = {Rabinizer 4: From LTL to Your Favourite Deterministic Automaton},
   year = {2018}
}

TY  - CONF
ID  - 2484808
AU  - Křetínský, Jan - Meggendorfer, Tobias - Sickert, Salomon - Ziegler, Christopher
PY  - 2018
TI  - Rabinizer 4: From LTL to Your Favourite Deterministic Automaton
PB  - Springer
SN  - 9783319961446
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.
ER  -

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Salomon SICKERT a Christopher ZIEGLER. Rabinizer 4: From LTL to Your Favourite Deterministic Automaton. In \textit{Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I}. Springer, 2018, s.~567-577. ISBN~9783319961446. Dostupné z: https://doi.org/10.1007/978-3-319-96145-3\_{}30.

Přehled o publikaci