| 2025 | AAAI | Multiple Mean-Payoff Optimization Under Local Stability Constraints. | David Klaska, Antonn Kucera, Vojtech Kur, Vt Musil, Vojtech Rehk |
| 2025 | ICALP | The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic Are Highly Undecidable. | Miroslav Chodil, Antonn Kucera |
| 2025 | IJCAI | Steady-State Strategy Synthesis for Swarms of Autonomous Agents. | Martin Jons, Antonn Kucera, Vojtech Kur, Jan Mack |
| 2024 | AAAI | Optimizing Local Satisfaction of Long-Run Average Objectives in Markov Decision Processes. | David Klaska, Antonn Kucera, Vojtech Kur, Vt Musil, Vojtech Rehk |
| 2024 | LICS | The Finite Satisfiability Problem for PCTL is Undecidable. | Miroslav Chodil, Antonn Kucera |
| 2023 | CONCUR | Asymptotic Complexity Estimates for Probabilistic Programs and Their VASS Abstractions. | Michal Ajdarw, Antonn Kucera |
| 2023 | IJCAI | Synthesizing Resilient Strategies for Infinite-Horizon Objectives in Multi-Agent Systems. | David Klaska, Antonn Kucera, Martin Kurecka, Vt Musil, Petr Novotn, Vojtech Rehk |
| 2023 | IJCAI | Mean Payoff Optimization for Systems of Periodic Service and Maintenance. | David Klaska, Antonn Kucera, Vt Musil, Vojtech Rehk |
| 2022 | IJCAI | General Optimization Framework for Recurrent Reachability Objectives. | David Klaska, Antonn Kucera, Vt Musil, Vojtech Rehk |
| 2022 | UAI | On-the-fly adaptation of patrolling strategies in changing environments. | Toms Brzdil, David Klaska, Antonn Kucera, Vt Musil, Petr Novotn, Vojtech Rehk |
| 2021 | CONCUR | Deciding Polynomial Termination Complexity for VASS Programs. | Michal Ajdarw, Antonn Kucera |
| 2021 | FCT | The Satisfiability Problem for a Quantitative Fragment of PCTL. | Miroslav Chodil, Antonn Kucera |
| 2021 | UAI | Regstar: efficient strategy synthesis for adversarial patrolling games. | David Klaska, Antonn Kucera, Vt Musil, Vojtech Rehk |
| 2020 | CAV | Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. | Michael Blondin, Javier Esparza, Martin Helfrich, Antonn Kucera, Philipp J. Meyer |
| 2020 | LICS | Efficient Analysis of VASS Termination Complexity. | Antonn Kucera, Jrme Leroux, Dominik Velan |
| 2019 | ATVA | Deciding Fast Termination for Probabilistic VASS with Nondeterminism. | Toms Brzdil, Krishnendu Chatterjee, Antonn Kucera, Petr Novotn, Dominik Velan |
| 2018 | CONCUR | Automatic Analysis of Expected Termination Time for Population Protocols. | Michael Blondin, Javier Esparza, Antonn Kucera |
| 2018 | IJCAI | Solving Patrolling Problems in the Internet Environment. | Toms Brzdil, Antonn Kucera, Vojtech Rehk |
| 2018 | LICS | Black Ninjas in the Dark: Formal Analysis of Population Protocols. | Michael Blondin, Javier Esparza, Stefan Jaax, Antonn Kucera |
| 2018 | LICS | Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. | Toms Brzdil, Krishnendu Chatterjee, Antonn Kucera, Petr Novotn, Dominik Velan, Florian Zuleger |
| 2017 | ATVA | Synthesis of Optimal Resilient Control Strategies. | Christel Baier, Clemens Dubslaff, Lubos Korenciak, Antonn Kucera, Vojtech Rehk |
| 2016 | ATVA | Optimizing the Expected Mean Payoff in Energy Markov Decision Processes. | Toms Brzdil, Antonn Kucera, Petr Novotn |
| 2016 | CONCUR | Stability in Graphs and Games. | Toms Brzdil, Vojtech Forejt, Antonn Kucera, Petr Novotn |
| 2016 | MASCOTS | Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration. | Lubos Korenciak, Antonn Kucera, Vojtech Rehk |
| 2015 | FCT | On the Existence and Computability of Long-Run Average Properties in Probabilistic VASS. | Antonn Kucera |
| 2015 | LICS | Long-Run Average Behaviour of Probabilistic Vector Addition Systems. | Toms Brzdil, Stefan Kiefer, Antonn Kucera, Petr Novotn |
| 2015 | LPAR | Cobra: A Tool for Solving General Deductive Games. | Miroslav Klimos, Antonn Kucera |
| 2015 | TACAS | MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives. | Toms Brzdil, Krishnendu Chatterjee, Vojtech Forejt, Antonn Kucera |
| 2014 | CAV | Minimizing Running Costs in Consumption Systems. | Toms Brzdil, David Klaska, Antonn Kucera, Petr Novotn |
| 2014 | CSL | Zero-reachability in probabilistic multi-counter automata. | Toms Brzdil, Stefan Kiefer, Antonn Kucera, Petr Novotn, Joost-Pieter Katoen |
| 2013 | LICS | Trading Performance for Stability in Markov Decision Processes. | Toms Brzdil, Krishnendu Chatterjee, Vojtech Forejt, Antonn Kucera |
| 2012 | CAV | Efficient Controller Synthesis for Consumption Games with Multiple Resource Types. | Toms Brzdil, Krishnendu Chatterjee, Antonn Kucera, Petr Novotn |
| 2012 | ICALP | Minimizing Expected Termination Time in One-Counter Markov Decision Processes. | Toms Brzdil, Antonn Kucera, Petr Novotn, Dominik Wojtczak |
| 2011 | CAV | Efficient Analysis of Probabilistic Programs with an Unbounded Counter. | Toms Brzdil, Stefan Kiefer, Antonn Kucera |
| 2011 | ICALP | Approximating the Termination Value of One-Counter MDPs and Stochastic Games. | Toms Brzdil, Vclav Brozek, Kousha Etessami, Antonn Kucera |
| 2011 | ICALP | Runtime Analysis of Probabilistic Programs with Unbounded Recursion. | Toms Brzdil, Stefan Kiefer, Antonn Kucera, Ivana Hutarov Varekov |
| 2011 | LICS | Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. | Toms Brzdil, Vclav Brozek, Krishnendu Chatterjee, Vojtech Forejt, Antonn Kucera |
| 2010 | CONCUR | Stochastic Real-Time Games with Qualitative Timed Automata Objectives. | Toms Brzdil, Jan Krcl, Jan Kretnsk, Antonn Kucera, Vojtech Rehk |
| 2010 | ICALP | Reachability Games on Extended Vector Addition Systems with States. | Toms Brzdil, Petr Jancar, Antonn Kucera |
| 2010 | SODA | One-Counter Markov Decision Processes. | Toms Brzdil, Vclav Brozek, Kousha Etessami, Antonn Kucera, Dominik Wojtczak |
| 2009 | STACS | Qualitative Reachability in Stochastic BPA Games. | Toms Brzdil, Vclav Brozek, Antonn Kucera, Jan Obdrzlek |
| 2008 | ICALP | Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives. | Toms Brzdil, Vojtech Forejt, Antonn Kucera |
| 2008 | LICS | The Satisfiability Problem for Probabilistic CTL. | Toms Brzdil, Vojtech Forejt, Jan Kretnsk, Antonn Kucera |
| 2008 | LPAR | Discounted Properties of Probabilistic Pushdown Automata. | Toms Brzdil, Vclav Brozek, Jan Holecek, Antonn Kucera |
| 2006 | CONCUR | Reachability in Recursive Markov Decision Processes. | Toms Brzdil, Vclav Brozek, Vojtech Forejt, Antonn Kucera |
| 2006 | LICS | Stochastic Games with Branching-Time Winning Objectives. | Toms Brzdil, Vclav Brozek, Vojtech Forejt, Antonn Kucera |
| 2005 | FOCS | Analysis and Prediction of the Long-Run Behavior of Probabilistic Sequential Programs with Recursion (Extended Abstract). | Toms Brzdil, Javier Esparza, Antonn Kucera |
| 2005 | LICS | Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances. | Javier Esparza, Antonn Kucera, Richard Mayr |
| 2005 | STACS | On the Decidability of Temporal Properties of Probabilistic Pushdown Automata. | Toms Brzdil, Antonn Kucera, Oldrich Strazovsk |
| 2005 | SOFSEM | Characteristic Patterns for LTL. | Antonn Kucera, Jan Strejcek |
| 2004 | CONCUR | Deciding Probabilistic Bisimilarity Over Infinite-State Probabilistic Systems. | Toms Brzdil, Antonn Kucera, Oldrich Strazovsk |
| 2004 | CONCUR | A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications. | Antonn Kucera, Philippe Schnoebelen |
| 2004 | LICS | Model Checking Probabilistic Pushdown Automata. | Javier Esparza, Antonn Kucera, Richard Mayr |
| 2003 | CONCUR | Deciding Bisimilarity between BPA and BPP Processes. | Petr Jancar, Antonn Kucera, Faron Moller |
| 2002 | CONCUR | Why Is Simulation Harder than Bisimulation? | Antonn Kucera, Richard Mayr |
| 2002 | CSL | The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. | Antonn Kucera, Jan Strejcek |
| 2002 | FOSSACS | Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds. | Petr Jancar, Antonn Kucera, Faron Moller, Zdenek Sawa |
| 2002 | MFCS | On the Complexity of Semantic Equivalences for Pushdown Automata and BPA. | Antonn Kucera, Richard Mayr |
| 2002 | SOFSEM | Equivalence-Checking with Infinite-State Systems: Techniques and Results. | Antonn Kucera, Petr Jancar |
| 2000 | ICALP | Efficient Verification Algorithms for One-Counter Processes. | Antonn Kucera |
| 2000 | STACS | Simulation and Bisimulation over One-Counter Processes. | Petr Jancar, Antonn Kucera, Faron Moller |
| 1999 | CONCUR | Weak Bisimilarity with Infinite-State Systems Can Be Decided in Polynomial Time. | Antonn Kucera, Richard Mayr |
| 1999 | CSL | A Logical Viewpoint on Process-Algebraic Quotients. | Antonn Kucera, Javier Esparza |
| 1999 | ICALP | Simulation Preorder on Simple Process Algebras. | Antonn Kucera, Richard Mayr |
| 1998 | ICALP | Deciding Bisimulation-Like Equivalences with Finite-State Processes. | Petr Jancar, Antonn Kucera, Richard Mayr |
| 1997 | CONCUR | How to Parallelize Sequential Processes. | Antonn Kucera |
| 1997 | SOFSEM | On Finite Representations of Infinite-State Behaviours. | Antonn Kucera |
| 1996 | SOFSEM | Regularity is Decidable for Normed BPA and Normed BPP Processes in Polynomial Time. | Antonn Kucera |
| 1986 | MFCS | An Alternative, Priority-Free, Solution to Post's Problem. | Antonn Kucera |