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)

Comparison of LTL to Deterministic Rabin Automata Translators. - Frantisek Blahoudek; Mojmír Kretínský; Jan Strejcek (LPAR, 2013)

Is there a best büchi automaton for explicit model checking? - Frantisek Blahoudek; Alexandre Duret-Lutz; Mojmír Kretínský; Jan Strejcek (SPIN, 2014)

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)

On Refinement of Büchi Automata for Explicit Model Checking. - Frantisek Blahoudek; Alexandre Duret-Lutz; Vojtech Rujbr; Jan Strejcek (SPIN, 2015)

Complementing Semi-deterministic Büchi Automata. - Frantisek Blahoudek; Matthias Heizmann; Sven Schewe; Jan Strejcek; Ming-Hsien Tsai 001 (TACAS, 2016)

Seminator: A Tool for Semi-Determinization of Omega-Automata. - Frantisek Blahoudek; Alexandre Duret-Lutz; Mikulás Klokocka; Mojmír Kretínský; Jan Strejcek (LPAR, 2017)

Generic Emptiness Check for Fun and Profit. - Christel Baier; Frantisek Blahoudek; Alexandre Duret-Lutz; Joachim Klein 001; David Müller 001; Jan Strejcek (ATVA, 2019)

ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata. - Juraj Major; Frantisek Blahoudek; Jan Strejcek; Miriama Sasaráková; Tatiana Zboncáková (ATVA, 2019)

LTL to Smaller Self-Loop Alternating Automata and Back. - Frantisek Blahoudek; Juraj Major; Jan Strejcek (ICTAC, 2019)

Qualitative Controller Synthesis for Consumption Markov Decision Processes. - Frantisek Blahoudek; Tomás Brázdil; Petr Novotný 001; Melkior Ornik; Pranay Thangeda; Ufuk Topcu (CAV (2), 2020)

Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization. - Frantisek Blahoudek; Alexandre Duret-Lutz; Jan Strejcek (CAV (2), 2020)

LTL to self-loop alternating automata with generic acceptance and back. - Frantisek Blahoudek; Juraj Major; Jan Strejcek (Theor. Comput. Sci., 2020)

Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption. - Frantisek Blahoudek; Murat Cubuktepe; Petr Novotný 001; Melkior Ornik; Pranay Thangeda; Ufuk Topcu (FM, 2021)

Polynomial-Time Algorithms for Multi-Agent Minimal-Capacity Planning. - Murat Cubuktepe; Frantisek Blahoudek; Ufuk Topcu (CoRR, 2021)

Word Equations in Synergy with Regular Constraints (Technical Report). - Frantisek Blahoudek; Yu-Fang Chen 001; David Chocholatý; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Juraj Síc (CoRR, 2022)

Polynomial-Time Algorithms for Multiagent Minimal-Capacity Planning. - Murat Cubuktepe; Frantisek Blahoudek; Ufuk Topcu (IEEE Trans. Control. Netw. Syst., 2022)

Word Equations in Synergy with Regular Constraints. - Frantisek Blahoudek; Yu-Fang Chen 001; David Chocholatý; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Juraj Síc (FM, 2023)

Efficient Strategy Synthesis for MDPs With Resource Constraints. - Frantisek Blahoudek; Petr Novotný 001; Melkior Ornik; Pranay Thangeda; Ufuk Topcu (IEEE Trans. Autom. Control., 2023)