Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment

Investor logo

Warning

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

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

Year of publication 2013
Type Article in Proceedings
Conference 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-02444-8_4
Field Informatics
Keywords linear temporal logic; deterministic omega-automata
Description Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing deterministic automata: ltl2dstar working for the whole LTL and Rabinizer applicable to the fragment LTL(F,G). We present a new translation to deterministic Rabin automata via alternating automata and deterministic transition-based generalized Rabin automata. Our translation applies to a fragment that is strictly larger than LTL(F,G). Experimental results show that our algorithm can produce significantly smaller automata compared to Rabinizer and ltl2dstar, especially for more complex LTL formulae.
Related projects:

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