Rabinizer 3: Safraless translation of ltl to small deterministic automata Conference Paper


Author(s): Komárková, Zuzana; Křetínský, Jan
Title: Rabinizer 3: Safraless translation of ltl to small deterministic automata
Title Series: LNCS
Affiliation IST Austria
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.
Conference Title: ATVA: Automated Technology for Verification and Analysis
Volume: 8837
Conference Dates: November 3-7, 2014
Conference Location: Sydney, Australia
Publisher: Springer  
Date Published: 2014-01-01
Start Page: 235
End Page: 241
DOI: 10.1007/978-3-319-11936-6_17
Notes: Sponsor: 267989 (QUAREM); ERC; Czech Science Foundation Sponsor: P202/12/G061; GACR; Czech Science Foundation Sponsor: S11402-N23 (RiSE); FWF; Czech Science Foundation
Open access: no
IST Austria Authors
Related IST Austria Work