Regularity is Decidable for Normed PA Processes in Polynomial Time. - Antonín Kucera 001 (FSTTCS, 1996)

Regularity is Decidable for Normed BPA and Normed BPP Processes in Polynomial Time. - Antonín Kucera 001 (SOFSEM, 1996)

Bisimilarity is decidable in the union of normed BPA and normed BPP processes. - Ivana Cerná; Mojmír Kretínský; Antonín Kucera 001 (INFINITY, 1996)

How to Parallelize Sequential Processes. - Antonín Kucera 001 (CONCUR, 1997)

Bisimilarity of processes with finite-state systems. - Petr Jancar; Antonín Kucera 001 (INFINITY, 1997)

Weak Bisimilarity with Infinite-State Systems Can Be Decided in Polynomial Time. - Antonín Kucera 001; Richard Mayr (CONCUR, 1999)

Simulation Preorder on Simple Process Algebras. - Antonín Kucera 001; Richard Mayr (ICALP, 1999)

Comparing Expressibility of Normed BPA and Normed BPP Processes. - Ivana Cerná; Mojmír Kretínský; Antonín Kucera 001 (Acta Informatica, 1999)

On Finite Representations of Infinite-State Behaviours. - Antonín Kucera 001 (Inf. Process. Lett., 1999)

Regularity of Normed PA Processes. - Antonín Kucera 001 (Inf. Process. Lett., 1999)

On Simulation-Checking with Sequential Systems. - Antonín Kucera 001 (ASIAN, 2000)

Efficient Verification Algorithms for One-Counter Processes. - Antonín Kucera 001 (ICALP, 2000)

Simulation and Bisimulation over One-Counter Processes. - Petr Jancar; Antonín Kucera 001; Faron Moller (STACS, 2000)

Effective decomposability of sequential behaviours. - Antonín Kucera 001 (Theor. Comput. Sci., 2000)

Deciding bisimulation-like equivalences with finite-state processes. - Petr Jancar; Antonín Kucera 001; Richard Mayr (Theor. Comput. Sci., 2001)

Why Is Simulation Harder than Bisimulation? - Antonín Kucera 001; Richard Mayr (CONCUR, 2002)

The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. - Antonín Kucera 001; Jan Strejcek (CSL, 2002)

Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds. - Petr Jancar; Antonín Kucera 001; Faron Moller; Zdenek Sawa (FoSSaCS, 2002)

On the Complexity of Semantic Equivalences for Pushdown Automata and BPA. - Antonín Kucera 001; Richard Mayr (MFCS, 2002)

Preface. - Antonín Kucera 001; Richard Mayr (INFINITY, 2002)

Simulation Preorder over Simple Process Algebras. - Antonín Kucera 001; Richard Mayr (Inf. Comput., 2002)

Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time. - Antonín Kucera 001; Richard Mayr (Theor. Comput. Sci., 2002)

Deciding Bisimilarity between BPA and BPP Processes. - Petr Jancar; Antonín Kucera 001; Faron Moller (CONCUR, 2003)

On Homogeneous Segments. - Robert Batusek; Ivan Kopecek; Antonín Kucera 001 (TSD, 2003)

Model checking LTL with regular valuations for pushdown systems. - Javier Esparza; Antonín Kucera 001; Stefan Schwoon (Inf. Comput., 2003)

A Logical Viewpoint on Process-algebraic Quotients. - Antonín Kucera 001; Javier Esparza (J. Log. Comput., 2003)

The complexity of bisimilarity-checking for one-counter processes. - Antonín Kucera 001 (Theor. Comput. Sci., 2003)

DP lower bounds for equivalence-checking and model-checking of one-counter automata. - Petr Jancar; Antonín Kucera 001; Faron Moller; Zdenek Sawa (Inf. Comput., 2004)

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)

Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances. - Javier Esparza; Antonín Kucera 001; Richard Mayr (LICS, 2005)

Characteristic Patterns for LTL. - Antonín Kucera 001; Jan Strejcek (SOFSEM, 2005)

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

The stuttering principle revisited. - Antonín Kucera 001; Jan Strejcek (Acta Informatica, 2005)

Methods for Quantitative Analysis of Probabilistic Pushdown Automata. - Antonín Kucera 001 (INFINITY, 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 Probabilistic Pushdown Automata. - Antonín Kucera 001; Javier Esparza; Richard Mayr (Log. Methods Comput. Sci., 2006)

A general approach to comparing infinite-state systems with their finite-state specifications. - Antonín Kucera 001; Philippe Schnoebelen (Theor. Comput. Sci., 2006)

Equivalence-checking on infinite-state systems: Techniques and results. - Antonín Kucera 001; Petr Jancar (Theory Pract. Log. Program., 2006)

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)

On the Controller Synthesis for Finite-State Markov Decision Processes. - Antonín Kucera 001; Oldrich Strazovský (Fundam. Informaticae, 2008)

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

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)

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)

On the complexity of checking semantic equivalences between pushdown processes and finite-state processes. - Antonín Kucera 001; Richard Mayr (Inf. Comput., 2010)

Effective Analysis of Infinite State Stochastic Processes Games. - Antonín Kucera 001 (Logics and Languages for Reliability and Security, 2010)

Turn-based stochastic games. - Antonín Kucera 001 (Lectures in Game Theory for Computer Scientists, 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)

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)

Playing Games with Counter Automata. - Antonín Kucera 001 (RP, 2012)

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

Preface. - Petr Hlinený; Antonín Kucera 001 (Theor. Comput. Sci., 2012)

The Presburger Award 2014 - Call for Nominations. - Antonín Kucera 001 (Bull. EATCS, 2013)

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

Preface. - Agata Ciabattoni; Rusins Freivalds; Antonín Kucera 001; Igor Potapov; Stefan Szeider (Fundam. Informaticae, 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)

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)

Strategy Synthesis for General Deductive Games Based on SAT Solving. - Miroslav Klimos; Antonín Kucera 001 (CoRR, 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)

On the Existence and Computability of Long-Run Average Properties in Probabilistic VASS. - Antonín Kucera 001 (FCT, 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)

Cobra: A Tool for Solving General Deductive Games. - Miroslav Klimos; Antonín Kucera 001 (LPAR, 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)

Regular Strategies and Strategy Improvement: Efficient Tools for Solving Large Patrolling Problems. - Antonín Kucera 001; Tomás Lamser (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)

Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration. - Lubos Korenciak; Antonín Kucera 001; Vojtech Rehák (MASCOTS, 2016)

Synthesis of Optimal Resilient Control Strategies. - Christel Baier; Clemens Dubslaff; Lubos Korenciak; Antonín Kucera 001; Vojtech Rehák (ATVA, 2017)

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)

Statement from EATCS President and vice Presidents about the recent US travel restrictions to foreigners. - Paul G. Spirakis; Leslie Ann Goldberg; Antonín Kucera 001; Giuseppe Persiano (Bull. EATCS, 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)

Automatic Synthesis of Efficient Regular Strategies in Adversarial Patrolling Games. - David Klaska; Antonín Kucera 001; Tomás Lamser; Vojtech Rehák (AAMAS, 2018)

Automatic Analysis of Expected Termination Time for Population Protocols. - Michael Blondin; Javier Esparza; Antonín Kucera 001 (CONCUR, 2018)

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

Black Ninjas in the Dark: Formal Analysis of Population Protocols. - Michael Blondin; Javier Esparza; Stefan Jaax; Antonín Kucera 001 (LICS, 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)

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

A generic framework for checking semantic equivalences between pushdown automata and finite-state automata. - Antonín Kucera 001; Richard Mayr (J. Comput. Syst. Sci., 2018)

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)

Mean-payoff Optimization in Continuous-time Markov Chains with Parametric Alarms. - Christel Baier; Clemens Dubslaff; Lubos Korenciak; Antonín Kucera 001; Vojtech Rehák (ACM Trans. Model. Comput. Simul., 2019)

Adversarial Patrolling with Drones. - David Klaska; Antonín Kucera 001; Vojtech Rehák (AAMAS, 2020)

Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. - Michael Blondin; Javier Esparza; Martin Helfrich; Antonín Kucera 001; Philipp J. Meyer (CAV (2), 2020)

Efficient Analysis of VASS Termination Complexity. - Antonín Kucera 001; Jérôme Leroux; Dominik Velan (LICS, 2020)

Deciding Polynomial Termination Complexity for VASS Programs. - Michal Ajdarów; Antonín Kucera 001 (CONCUR, 2021)

Regstar: efficient strategy synthesis for adversarial patrolling games. - David Klaska; Antonín Kucera 001; Vít Musil; Vojtech Rehák (UAI, 2021)

Algorithmic analysis of termination and counter complexity in vector addition systems with states: a survey of recent results. - Antonín Kucera 001 (ACM SIGLOG News, 2021)

Minimizing Expected Intrusion Detection Time in Adversarial Patrolling. - David Klaska; Antonín Kucera 001; Vít Musil; Vojtech Rehák (AAMAS, 2022)

Satisfiability of Quantitative Probabilistic CTL: Rise to the Challenge. - Miroslav Chodil; Antonín Kucera 001; Jan Kretínský (Principles of Systems Design, 2022)

General Optimization Framework for Recurrent Reachability Objectives. - David Klaska; Antonín Kucera 001; Vít Musil; Vojtech Rehák (IJCAI, 2022)

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)

Asymptotic Complexity Estimates for Probabilistic Programs and Their VASS Abstractions. - Michal Ajdarów; Antonín Kucera 001 (CONCUR, 2023)

Synthesizing Resilient Strategies for Infinite-Horizon Objectives in Multi-Agent Systems. - David Klaska; Antonín Kucera 001; Martin Kurecka; Vít Musil; Petr Novotný 001; Vojtech Rehák (IJCAI, 2023)

Mean Payoff Optimization for Systems of Periodic Service and Maintenance. - David Klaska; Antonín Kucera 001; Vít Musil; Vojtech Rehák (IJCAI, 2023)

Optimizing Local Satisfaction of Long-Run Average Objectives in Markov Decision Processes. - David Klaska; Antonín Kucera 001; Vojtech Kur; Vít Musil; Vojtech Rehák (AAAI, 2024)

Asymptotic Analysis of Probabilistic Programs: When Expectations Do Not Meet Our Expectations. - Michal Ajdarów; Antonín Kucera 001; Petr Novotný 001 (Principles of Verification (1), 2024)

The Finite Satisfiability Problem for PCTL is Undecidable. - Miroslav Chodil; Antonín Kucera 001 (LICS, 2024)

The Satisfiability and Validity Problems for Probabilistic CTL. - Antonín Kucera 001 (RP, 2024)

The General and Finite Satisfiability Problems for PCTL are Undecidable. - Miroslav Chodil; Antonín Kucera 001 (CoRR, 2024)

The satisfiability problem for a quantitative fragment of PCTL. - Miroslav Chodil; Antonín Kucera 001 (J. Comput. Syst. Sci., 2024)

Multiple Mean-Payoff Optimization Under Local Stability Constraints. - David Klaska; Antonín Kucera 001; Vojtech Kur; Vít Musil; Vojtech Rehák (AAAI, 2025)

The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic Are Highly Undecidable. - Miroslav Chodil; Antonín Kucera 001 (ICALP, 2025)

Steady-State Strategy Synthesis for Swarms of Autonomous Agents. - Martin Jonás; Antonín Kucera 001; Vojtech Kur; Jan Macák (CoRR, 2025)