2013/06/19 by Tomáš Babiak, František Blahoudek, Babiak, Tomáš +5
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Natural Language Processing Techniques #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1306.4636
openalex publication_date 2013/06/19 · openalex created_date 2022/10/03 · openalex updated_date 2026/07/28
Some applications of linear temporal logic (LTL) require to translate\nformulae of the logic to deterministic omega-automata. There are currently two\ntranslators producing deterministic automata: ltl2dstar working for the whole\nLTL and Rabinizer applicable to LTL(F,G) which is the LTL fragment using only\nmodalities F and G. We present a new translation to deterministic Rabin\nautomata via alternating automata and deterministic transition-based\ngeneralized Rabin automata. Our translation applies to a fragment that is\nstrictly larger than LTL(F,G). Experimental results show that our algorithm can\nproduce significantly smaller automata compared to Rabinizer and ltl2dstar,\nespecially for more complex LTL formulae.\n