Almost Linear Büchi Automata - Tomás Babiak; Vojtech Rehák; Jan Strejcek (EXPRESS, 2009)

A Short Story of a Subtle Error in LTL Formulas Reduction and Divine Incorrectness - Tomás Babiak; Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (CoRR, 2010)

LTL to Büchi Automata Translation: Fast and More Deterministic. - Tomás Babiak; Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (TACAS, 2012)

Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment. - Tomás Babiak; Frantisek Blahoudek; Mojmír Kretínský; Jan Strejcek (ATVA, 2013)

Compositional Approach to Suspension and Other Improvements to LTL Translation. - Tomás Babiak; Thomas Badie; Alexandre Duret-Lutz; Mojmír Kretínský; Jan Strejcek (SPIN, 2013)

The Hanoi Omega-Automata Format. - Tomás Babiak; Frantisek Blahoudek; Alexandre Duret-Lutz; Joachim Klein 001; Jan Kretínský; David Müller 001; David Parker 001; Jan Strejcek (CAV (1), 2015)