TCS Journal 2020 Journal Article
LTL to self-loop alternating automata with generic acceptance and back
- František Blahoudek
- Juraj Major
- Jan Strejček
Author name cluster
František Blahoudek
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
2 papers
1 author row
Possible papers
2Highlights Conference 2013 Conference Abstract
Effective translation of LTL to deterministic Rabin automata: Beyond the (F, G)-fragment
- Tomáš Babiak
- František Blahoudek
- Mojmir Kretinsky
- Jan Strejček
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 LTL(F, G) which is the LTL fragment using only modalities F and 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.