"11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013" . "Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment"@en . "9783319024431" . . . "Berlin Heidelberg" . "RIV/00216224:14330/13:00066175" . "Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment" . . "4"^^ . "Babiak, Tom\u00E1\u0161" . . "4"^^ . "14330" . "Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment"@en . "K\u0159et\u00EDnsk\u00FD, Mojm\u00EDr" . "Hanoi, Vietnam" . . . . "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."@en . . . "Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment" . "15"^^ . "[B43063C27353]" . "I, P(GBP202/12/G061), S" . "10.1007/978-3-319-02444-8_4" . . . "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." . . . "Strej\u010Dek, Jan" . . "linear temporal logic; deterministic omega-automata"@en . . "0302-9743" . "RIV/00216224:14330/13:00066175!RIV14-MSM-14330___" . . . . . . "Springer-Verlag" . "Blahoudek, Franti\u0161ek" . "71879" . . "2013-01-01+01:00"^^ .