Name
Title | ||
|---|---|---|
Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment. |
Abstract | ||
|---|---|---|
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. |
Year | Venue | DocType |
|---|---|---|
2013 | automated technology for verification and analysis | Conference |
Volume | Citations | PageRank |
abs/1306.4636 | 17 | 0.71 |
References | Authors | |
26 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tomáš Babiak | 1 | 90 | 3.70 |
| Frantisek Blahoudek | 2 | 48 | 4.02 |
| Mojmír Kretínský | 3 | 88 | 7.11 |
| Jan Strejcek | 4 | 99 | 13.83 |