39 citations · 44 across the 4 of their papers we have counts for
4 papers
Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment
Tomáš Babiak, František Blahoudek, Mojmír Křetínský +1
Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing determini…
LTL to Büchi Automata Translation: Fast and More Deterministic
Tomáš Babiak, Mojmír Křetínský, Vojtěch Řehák +1
We introduce improvements in the algorithm by Gastin and Oddoux translating LTL formulae into Büchi automata via very weak alternating co-Büchi automata and generalized Büchi autom…
A Short Story of a Subtle Error in LTL Formulas Reduction and Divine Incorrectness
Tomáš Babiak, Mojmír Křetínský, Vojtěch Řehák +1
We identify a subtle error in LTL formulas reduction method used as one optimization step in an LTL to Büchi automata translation. The error led to some incorrect answers of the es…
Almost Linear Büchi Automata
Tomáš Babiak, Vojtěch Řehák, Jan Strejček
We introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Buechi automata (BA) called Almost linear Buechi automata (ALBA). We provide effective tran…