Local Distributed Model Checking of RegCTL. - Tomás Brázdil; Ivana Cerná (PDMC@CONCUR, 2002)

Analysis and Prediction of the Long-Run Behavior of Probabilistic Sequential Programs with Recursion (Extended Abstract). - Tomás Brázdil; Javier Esparza; Antonín Kucera 001 (FOCS, 2005)

Computing the Expected Accumulated Reward and Gain for a Subclass of Infinite Markov Chains. - Tomás Brázdil; Antonín Kucera 001 (FSTTCS, 2005)

On the Decidability of Temporal Properties of Probabilistic Pushdown Automata. - Tomás Brázdil; Antonín Kucera 001; Oldrich Strazovský (STACS, 2005)

Stochastic Games with Branching-Time Winning Objectives. - Tomás Brázdil; Václav Brozek; Vojtech Forejt; Antonín Kucera 001 (LICS, 2006)

Model Checking of RegCTL. - Tomás Brázdil; Ivana Cerná (Comput. Artif. Intell., 2006)

Strategy Synthesis for Markov Decision Processes and Branching-Time Logics. - Tomás Brázdil; Vojtech Forejt (CONCUR, 2007)

Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives. - Tomás Brázdil; Vojtech Forejt; Antonín Kucera 001 (ICALP (2), 2008)

The Satisfiability Problem for Probabilistic CTL. - Tomás Brázdil; Vojtech Forejt; Jan Kretínský; Antonín Kucera 001 (LICS, 2008)

Discounted Properties of Probabilistic Pushdown Automata. - Tomás Brázdil; Václav Brozek; Jan Holecek; Antonín Kucera 001 (LPAR, 2008)

Deciding probabilistic bisimilarity over infinite-state probabilistic systems. - Tomás Brázdil; Antonín Kucera 001; Oldrich Strazovský (Acta Informatica, 2008)

Reachability in recursive Markov decision processes. - Tomás Brázdil; Václav Brozek; Vojtech Forejt; Antonín Kucera 001 (Inf. Comput., 2008)

On the Memory Consumption of Probabilistic Pushdown Automata. - Tomás Brázdil; Javier Esparza; Stefan Kiefer (FSTTCS, 2009)

Branching-Time Model-Checking of Probabilistic Pushdown Automata. - Tomás Brázdil; Václav Brozek; Vojtech Forejt (INFINITY, 2009)

Stochastic Real-Time Games with Qualitative Timed Automata Objectives. - Tomás Brázdil; Jan Krcál; Jan Kretínský; Antonín Kucera 001; Vojtech Rehák (CONCUR, 2010)

One-Counter Stochastic Games. - Tomás Brázdil; Václav Brozek; Kousha Etessami (FSTTCS, 2010)

Reachability Games on Extended Vector Addition Systems with States. - Tomás Brázdil; Petr Jancar; Antonín Kucera 001 (ICALP (2), 2010)

One-Counter Markov Decision Processes. - Tomás Brázdil; Václav Brozek; Kousha Etessami; Antonín Kucera 001; Dominik Wojtczak (SODA, 2010)

Fixed-Delay Events in Generalized Semi-Markov Processes Revisited. - Tomás Brázdil; Jan Krcál; Jan Kretínský; Vojtech Rehák (CONCUR, 2011)

Measuring performance of continuous-time stochastic processes using timed automata. - Tomás Brázdil; Jan Krcál; Jan Kretínský; Antonín Kucera 001; Vojtech Rehák (HSCC, 2011)

Qualitative reachability in stochastic BPA games. - Tomás Brázdil; Václav Brozek; Antonín Kucera 001; Jan Obdrzálek (Inf. Comput., 2011)

Efficient Controller Synthesis for Consumption Games with Multiple Resource Types. - Tomás Brázdil; Krishnendu Chatterjee; Antonín Kucera 001; Petr Novotný 001 (CAV, 2012)

Verification of Open Interactive Markov Chains. - Tomás Brázdil; Holger Hermanns; Jan Krcál; Jan Kretínský; Vojtech Rehák (FSTTCS, 2012)

Minimizing Expected Termination Time in One-Counter Markov Decision Processes. - Tomás Brázdil; Antonín Kucera 001; Petr Novotný 001; Dominik Wojtczak (ICALP (2), 2012)

Determinacy in Stochastic Games with Unbounded Payoff Functions. - Tomás Brázdil; Antonín Kucera 001; Petr Novotný 001 (MEMICS, 2012)

Stabilization of Branching Queueing Networks. - Tomás Brázdil; Stefan Kiefer (STACS, 2012)

Stochastic game logic. - Christel Baier; Tomás Brázdil; Marcus Größer; Antonín Kucera 001 (Acta Informatica, 2012)

Space-efficient scheduling of stochastically generated tasks. - Tomás Brázdil; Javier Esparza; Stefan Kiefer; Michael Luttenberger (Inf. Comput., 2012)

Solvency Markov Decision Processes with Interest. - Tomás Brázdil; Taolue Chen 001; Vojtech Forejt; Petr Novotný 001; Aistis Simaitis (FSTTCS, 2013)

On time-average limits in deterministic and stochastic petri nets. - Tomás Brázdil; Lubos Korenciak; Jan Krcál; Jan Kretínský; Vojtech Rehák (ICPE, 2013)

Analyzing probabilistic pushdown automata. - Tomás Brázdil; Javier Esparza; Stefan Kiefer; Antonín Kucera 001 (Formal Methods Syst. Des., 2013)

Approximating the termination value of one-counter MDPs and stochastic games. - Tomás Brázdil; Václav Brozek; Kousha Etessami; Antonín Kucera 001 (Inf. Comput., 2013)

Continuous-time stochastic games with time-bounded reachability. - Tomás Brázdil; Vojtech Forejt; Jan Krcál; Jan Kretínský; Antonín Kucera 001 (Inf. Comput., 2013)

Solving adversarial patrolling games with bounded error: (extended abstract). - Michal Abaffy; Tomás Brázdil; Vojtech Rehák; Branislav Bosanský; Antonín Kucera 001; Jan Krcál (AAMAS, 2014)

Verification of Markov Decision Processes Using Learning Algorithms. - Tomás Brázdil; Krishnendu Chatterjee; Martin Chmelik; Vojtech Forejt; Jan Kretínský; Marta Z. Kwiatkowska; David Parker 001; Mateusz Ujma (ATVA, 2014)

Minimizing Running Costs in Consumption Systems. - Tomás Brázdil; David Klaska; Antonín Kucera 001; Petr Novotný 001 (CAV, 2014)

Zero-reachability in probabilistic multi-counter automata. - Tomás Brázdil; Stefan Kiefer; Antonín Kucera 001; Petr Novotný 001; Joost-Pieter Katoen (CSL-LICS, 2014)

Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes - Tomás Brázdil; Václav Brozek; Krishnendu Chatterjee; Vojtech Forejt; Antonín Kucera 001 (Log. Methods Comput. Sci., 2014)

Efficient Analysis of Probabilistic Programs with an Unbounded Counter. - Tomás Brázdil; Stefan Kiefer; Antonín Kucera 001 (J. ACM, 2014)

Branching-time model-checking of probabilistic pushdown automata. - Tomás Brázdil; Václav Brozek; Vojtech Forejt; Antonín Kucera 001 (J. Comput. Syst. Sci., 2014)

Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. - Tomás Brázdil; Krishnendu Chatterjee; Martin Chmelik; Andreas Fellner; Jan Kretínský (CAV (1), 2015)

Long-Run Average Behaviour of Probabilistic Vector Addition Systems. - Tomás Brázdil; Stefan Kiefer; Antonín Kucera 001; Petr Novotný 001 (LICS, 2015)

Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis. - Tomás Brázdil; Lubos Korenciak; Jan Krcál; Petr Novotný 001; Vojtech Rehák (QEST, 2015)

MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives. - Tomás Brázdil; Krishnendu Chatterjee; Vojtech Forejt; Antonín Kucera 001 (TACAS, 2015)

Strategy Synthesis in Adversarial Patrolling Games. - Tomás Brázdil; Petr Hlinený; Antonín Kucera 001; Vojtech Rehák; Matús Abaffy (CoRR, 2015)

Runtime analysis of probabilistic programs with unbounded recursion. - Tomás Brázdil; Stefan Kiefer; Antonín Kucera 001; Ivana Hutarová Vareková (J. Comput. Syst. Sci., 2015)

Stochastic Shortest Path with Energy Constraints in POMDPs: (Extended Abstract). - Tomás Brázdil; Krishnendu Chatterjee; Martin Chmelik; Anchit Gupta; Petr Novotný 001 (AAMAS, 2016)

Optimizing the Expected Mean Payoff in Energy Markov Decision Processes. - Tomás Brázdil; Antonín Kucera 001; Petr Novotný 001 (ATVA, 2016)

Stability in Graphs and Games. - Tomás Brázdil; Vojtech Forejt; Antonín Kucera 001; Petr Novotný 001 (CONCUR, 2016)

Policy Learning for Time-Bounded Reachability in Continuous-Time Markov Decision Processes via Doubly-Stochastic Gradient Ascent. - Ezio Bartocci; Luca Bortolussi; Tomás Brázdil; Dimitrios Milios; Guido Sanguinetti (QEST, 2016)

Stochastic Shortest Path with Energy Constraints in POMDPs. - Tomás Brázdil; Krishnendu Chatterjee; Martin Chmelik; Anchit Gupta; Petr Novotný 001 (CoRR, 2016)

Efficient Algorithms for Checking Fast Termination in VASS. - Tomás Brázdil; Krishnendu Chatterjee; Antonín Kucera 001; Petr Novotný 001; Dominik Velan (CoRR, 2017)

Trading performance for stability in Markov decision processes. - Tomás Brázdil; Krishnendu Chatterjee; Vojtech Forejt; Antonín Kucera 001 (J. Comput. Syst. Sci., 2017)

Policy learning in continuous-time Markov decision processes using Gaussian Processes. - Ezio Bartocci; Luca Bortolussi; Tomás Brázdil; Dimitrios Milios; Guido Sanguinetti (Perform. Evaluation, 2017)

Solving Patrolling Problems in the Internet Environment. - Tomás Brázdil; Antonín Kucera 001; Vojtech Rehák (IJCAI, 2018)

Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes. - Pranav Ashok; Tomás Brázdil; Jan Kretínský; Ondrej Slámecka (ISoLA (2), 2018)

Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. - Tomás Brázdil; Krishnendu Chatterjee; Antonín Kucera 001; Petr Novotný 001; Dominik Velan; Florian Zuleger (LICS, 2018)

Strategy Representation by Decision Trees in Reactive Synthesis. - Tomás Brázdil; Krishnendu Chatterjee; Jan Kretínský; Viktor Toman (TACAS (1), 2018)

Synthesizing Efficient Solutions for Patrolling Problems in the Internet Environment. - Tomás Brázdil; Antonín Kucera 001; Vojtech Rehák (CoRR, 2018)

Unbounded Orchestrations of Transducers for Manufacturing. - Natasha Alechina; Tomás Brázdil; Giuseppe De Giacomo; Paolo Felli; Brian Logan 001; Moshe Y. Vardi (AAAI, 2019)

Deciding Fast Termination for Probabilistic VASS with Nondeterminism. - Tomás Brázdil; Krishnendu Chatterjee; Antonín Kucera 001; Petr Novotný 001; Dominik Velan (ATVA, 2019)

Strategy Representation by Decision Trees with Linear Classifiers. - Pranav Ashok; Tomás Brázdil; Krishnendu Chatterjee; Jan Kretínský; Christoph H. Lampert; Viktor Toman (QEST, 2019)

Reinforcement Learning of Risk-Constrained Policies in Markov Decision Processes. - Tomás Brázdil; Krishnendu Chatterjee; Petr Novotný 001; Jiri Vahala (AAAI, 2020)

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)

On-the-fly adaptation of patrolling strategies in changing environments. - Tomás Brázdil; David Klaska; Antonín Kucera 001; Vít Musil; Petr Novotný 001; Vojtech Rehák (UAI, 2022)

xOpat: eXplainable Open Pathology Analysis Tool. - Jirí Horák; Katarína Furmanová; Barbora Kozlíková; Tomás Brázdil; Petr Holub; M. Kacenga; Matej Gallo; R. Nenutil; Jan Byska; Vít Rusnák (Comput. Graph. Forum, 2023)

A Summary and Personal Perspective on Recent Advances in Privacy Risk Assessment in Digital Pathology Through Formal Methods. - Tomás Brázdil (Taming the Infinities of Concurrency, 2024)

Beyond Occlusion: In Search for Near Real-Time Explainability of CNN-Based Prostate Cancer Classification. - Martin Krebs; Jan Obdrzálek; Vít Musil; Tomás Brázdil (ISBI, 2025)

Learning Algorithms for Verification of Markov Decision Processes. - Tomás Brázdil; Krishnendu Chatterjee; Martin Chmelik; Vojtech Forejt; Jan Kretínský; Marta Kwiatkowska; Tobias Meggendorfer; David Parker 001; Mateusz Ujma (TheoretiCS, 2025)