Comparison of LTL to Deterministic Rabin Automata Translators

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BLAHOUDEK František KŘETÍNSKÝ Mojmír STREJČEK Jan

Year of publication 2013
Type Article in Proceedings
Conference Logic for Programming Artificial Intelligence and Reasoning, LPAR-19
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-642-45221-5_12
Field Informatics
Keywords linear temporal logic; deterministic omega-automata; LTL3DRA; Rabinizer; ltl2dstar
Description Increasing interest in control synthesis and probabilistic model checking caused recent development of LTL to deterministic omega-automata translation. The standard approach represented by ltl2dstar tool employs Safra's construction to determinize a Büchi automaton produced by some LTL to Büchi automata translator. Since 2012, three new LTL to deterministic Rabin automata translators appeared, namely Rabinizer, LTL3DRA, and Rabinizer 2. They all avoid Safra's construction and work on LTL fragments only. We compare performance and automata produced by the mentioned tools, where ltl2dstar is combined with several LTL to Büchi automata translators: besides traditionally used LTL2BA, we also consider LTL->NBA, LTL3BA, and Spot.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.