39 citations · 42 across the 3 of their papers we have counts for
3 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…