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.
Cite
CITATION STYLE
Křetínský, J., Meggendorfer, T., Sickert, S., & Ziegler, C. (2018). Rabinizer 4: From LTL to your favourite deterministic automaton. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10981 LNCS, pp. 567–577). Springer Verlag. https://doi.org/10.1007/978-3-319-96145-3_30
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
