Antonín Kučera

AAAI Conference 2025 Conference Paper

Multiple Mean-Payoff Optimization Under Local Stability Constraints

• David Klaška
• Antonín Kučera
• Vojtěch Kůr
• Vít Musil
• Vojtěch Řehák

The long-run average payoff per transition (mean payoff) is the main tool for specifying the performance and dependability properties of discrete systems. The problem of constructing a controller (strategy) simultaneously optimizing several mean payoffs has been deeply studied for stochastic and game-theoretic models. One common issue of the constructed controllers is the instability of the mean payoffs, measured by the deviations of the average rewards per transition computed in a finite "window" sliding along a run. Unfortunately, the problem of simultaneously optimizing the mean payoffs under local stability constraints is computationally hard, and the existing works do not provide a practically usable algorithm even for non-stochastic models such as two-player games. In this paper, we design and evaluate the first efficient and scalable solution to this problem applicable to Markov decision processes.

IJCAI Conference 2025 Conference Paper

Steady-State Strategy Synthesis for Swarms of Autonomous Agents

• Martin Jonáš
• Antonín Kučera
• Vojtěch Kůr
• Jan Mačák

The steady-state synthesis aims to construct a policy for a given MDP D such that the long-run average frequencies of visits to the vertices of D satisfy given numerical constraints. This problem is solvable in polynomial time, and memoryless policies are sufficient for approximating an arbitrary frequency vector achievable by a general (infinite-memory) policy. We study the steady-state synthesis problem for multiagent systems, where multiple autonomous agents jointly strive to achieve a suitable frequency vector. We show that the problem for multiple agents is computationally hard (PSPACE or NP hard, depending on the variant), and memoryless strategy profiles are insufficient for approximating achievable frequency vectors. Furthermore, we prove that even evaluating the frequency vector achieved by a given memoryless profile is computationally hard. This reveals a severe barrier to constructing an efficient synthesis algorithm, even for memoryless profiles. Nevertheless, we design an efficient and scalable synthesis algorithm for a subclass of full memoryless profiles, and we evaluate this algorithm on a large class of randomly generated instances. The experimental results demonstrate a significant improvement against a naive algorithm based on strategy sharing.

AAAI Conference 2024 Conference Paper

Optimizing Local Satisfaction of Long-Run Average Objectives in Markov Decision Processes

• David Klaška
• Antonín Kučera
• Vojtěch Kůr
• Vít Musil
• Vojtěch Řehák

Long-run average optimization problems for Markov decision processes (MDPs) require constructing policies with optimal steady-state behavior, i.e., optimal limit frequency of visits to the states. However, such policies may suffer from local instability in the sense that the frequency of states visited in a bounded time horizon along a run differs significantly from the limit frequency. In this work, we propose an efficient algorithmic solution to this problem.

IJCAI Conference 2023 Conference Paper

Mean Payoff Optimization for Systems of Periodic Service and Maintenance

• David Klaška
• Antonín Kučera
• Vít Musil
• Vojtěch Řehák

Consider oriented graph nodes requiring periodic visits by a service agent. The agent moves among the nodes and receives a payoff for each completed service task, depending on the time elapsed since the previous visit to a node. We consider the problem of finding a suitable schedule for the agent to maximize its long-run average payoff per time unit. We show that the problem of constructing an epsilon-optimal schedule is PSPACE-hard for every fixed non-negative epsilon, and that there exists an optimal periodic schedule of exponential length. We propose randomized finite-memory (RFM) schedules as a compact description of the agent's strategies and design an efficient algorithm for constructing RFM schedules. Furthermore, we construct deterministic periodic schedules by sampling from RFM schedules.

IJCAI Conference 2023 Conference Paper

Synthesizing Resilient Strategies for Infinite-Horizon Objectives in Multi-Agent Systems

• David Klaška
• Antonín Kučera
• Martin Kurečka
• Vít Musil
• Petr Novotný
• Vojtěch Řehák

We consider the problem of synthesizing resilient and stochastically stable strategies for systems of cooperating agents striving to minimize the expected time between consecutive visits to selected locations in a known environment. A strategy profile is resilient if it retains its functionality even if some of the agents fail, and stochastically stable if the visiting time variance is small. We design a novel specification language for objectives involving resilience and stochastic stability, and we show how to efficiently compute strategy profiles (for both autonomous and coordinated agents) optimizing these objectives. Our experiments show that our strategy synthesis algorithm can construct highly non-trivial and efficient strategy profiles for environments with general topology.

AAMAS Conference 2022 Conference Paper

Minimizing Expected Intrusion Detection Time in Adversarial Patrolling

• David Klaška
• Antonín Kučera
• Vit Musil
• Vojtěch Řehák

In adversarial patrolling games, a mobile Defender strives to discover intrusions at vulnerable targets initiated by an Attacker. The Attacker’s utility is traditionally defined as the probability of completing an attack, possibly weighted by target costs. However, in many real-world scenarios, the actual damage caused by the Attacker depends on the time elapsed since the attack’s initiation to its detection. We introduce a formal model for such scenarios, and we show that the Defender always has an optimal strategy achieving maximal protection. We also prove that finite-memory Defender’s strategies are sufficient for achieving protection arbitrarily close to the optimum. Then, we design an efficient strategy synthesis algorithm based on differentiable programming and gradient descent. We evaluate the efficiency of our method experimentally.

Highlights Conference 2019 Conference Abstract

Automatic Synthesis of Efficient Regular Strategies in Adversarial Patrolling Games

• David Klaška
• Antonín Kučera
• Tomáš Lamser
• Vojtěch Řehák.

We give a polynomial-time algorithm for synthesizing efficient regular strategies in adversarial patrolling games with general topology. Regular strategies use finite memory to gather some relevant information about the history of Defender’s moves which results in substantially better protection of the targets. So far, the scope of automatic strategy synthesis was limited to positional strategies (which ignore the history) or to regular strategies where the underlying finite-memory observer had to be supplied \emph{manually}. Furthermore, the existing methods do not give any information on how far are the constructed strategies from being optimal. In this paper, we try to overcome these limitations. We develop a novel \emph{gradient-based} algorithm for synthesizing regular strategies where the underlying finite-memory observers are constructed \emph{algorithmically}. The running time of our algorithm is \emph{polynomial} which makes the algorithm applicable to instances of \emph{realistic size}. Furthermore, we develop an algorithm for computing an \emph{upper bound} on the best achievable protection, and compare the quality of the constructed strategies against this bound. Thus, we can effectively measure the “distance” of the constructed strategies from optimal strategies, and our experiments show that this distance is often quite small.

AAMAS Conference 2016 Conference Paper

Regular Strategies and Strategy Improvement: Efficient Tools for Solving Large Patrolling Problems

• Antonín Kučera
• Tomáš Lamser

In patrolling problems, the task is to compute an optimal strategy for a patroller who moves among vulnerable targets and aims at detecting possible intrusions. Previous approaches to this problem were mostly based on non-linear programming, and the solution space was restricted to positional strategies or to strategies dependent on a bounded history of patroller’s moves. In this paper, we extend the solution space to regular strategies, and show that regular strategies are strictly more powerful than strategies dependent on a bounded history. Further, we design a strategy improvement technique for regular strategies which completely avoids the use of non-linear programming. Intuitively, we start with some regular strategy, and then repeatedly improve this strategy by incorporating a solution of a certain linear program. Our experiments demonstrate that the proposed approach can quickly produce strategies of very good quality even for quite large patrolling problems.

Highlights Conference 2014 Conference Abstract

Zero-Reachability in Probabilistic Multi-Counter Automata

• Antonín Kučera

We study the qualitative and quantitative zero-reachability problem in probabilistic multi-counter systems. We identify the undecidable variants of the problems, and then we concentrate on the remaining two cases. In the first case, when we are interested in the probability of all runs that visit zero in some counter, we show that the qualitative zero-reachability is decidable in time which is polynomial in the size of a given pMC and doubly exponential in the number of counters. Further, we show that the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error ε > 0 in time which is polynomial in log(ε), exponential in the size of a given pMC, and doubly exponential in the number of counters. In the second case, we are interested in the probability of all runs that visit zero in some counter different from the last counter. Here we show that the qualitative zero-reachability is decidable and SquareRootSum-hard, and the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error ε > 0 (these result applies to pMC satisfying a suitable technical condition that can be verified in polynomial time). The proof techniques invented in the second case allow to construct counterexamples for some classical results about ergodicity in stochastic Petri nets.

I&C Journal 2013 Journal Article

Approximating the termination value of one-counter MDPs and stochastic games

• Tomáš Brázdil
• Václav Brožek
• Kousha Etessami
• Antonín Kučera

One-counter MDPs (OC-MDPs) and one-counter simple stochastic games (OC-SSGs) are 1-player, and 2-player turn-based zero-sum, stochastic games played on the transition graph of classic one-counter automata (equivalently, pushdown automata with a 1-letter stack alphabet). A key objective for the analysis and verification of these games is the termination objective, where the players aim to maximize (minimize, respectively) the probability of hitting counter value 0, starting at a given control state and given counter value. Recently, we studied qualitative decision problems (“is the optimal termination value equal to 1? ”) for OC-MDPs (and OC-SSGs) and showed them to be decidable in polynomial time (in NP ∩ coNP, respectively). However, quantitative decision and approximation problems (“is the optimal termination value at least p”, or “approximate the termination value within ε”) are far more challenging. This is so in part because optimal strategies may not exist, and because even when they do exist they can have a highly non-trivial structure. It thus remained open even whether any of these quantitative termination problems are computable. In this paper we show that all quantitative approximation problems for the termination value for OC-MDPs and OC-SSGs are computable. Specifically, given an OC-SSG, and given ε > 0, we can compute a value v that approximates the value of the OC-SSG termination game within additive error ε, and furthermore we can compute ε-optimal strategies for both players in the game. A key ingredient in our proofs is a subtle martingale, derived from solving certain linear programs that we can associate with a maximizing OC-MDP. An application of Azumaʼs inequality on these martingales yields a computable bound for the “wealth” at which a “rich personʼs strategy” becomes ε-optimal for OC-MDPs.

I&C Journal 2013 Journal Article

Continuous-time stochastic games with time-bounded reachability

• Tomáš Brázdil
• Vojtěch Forejt
• Jan Krčál
• Jan Křetínský
• Antonín Kučera

We study continuous-time stochastic games with time-bounded reachability objectives and time-abstract strategies. We show that each vertex in such a game has a value (i. e. , an equilibrium probability), and we classify the conditions under which optimal strategies exist. Further, we show how to compute ε-optimal strategies in finite games and provide detailed complexity estimations. Moreover, we show how to compute ε-optimal strategies in infinite games with finite branching and bounded rates where the bound as well as the successors of a given state are effectively computable. Finally, we show how to compute optimal strategies in finite uniform games.

TCS Journal 2012 Journal Article

Preface

• Petr Hliněný
• Antonín Kučera

I&C Journal 2011 Journal Article

Qualitative reachability in stochastic BPA games

• Tomáš Brázdil
• Václav Brožek
• Antonín Kučera
• Jan Obdržálek

We consider a class of infinite-state stochastic games generated by stateless pushdown automata (or, equivalently, 1-exit recursive state machines), where the winning objective is specified by a regular set of target configurations and a qualitative probability constraint ‘>0’ or ‘=1’. The goal of one player is to maximize the probability of reaching the target set so that the constraint is satisfied, while the other player aims at the opposite. We show that the winner in such games can be determined in P for the ‘>0’ constraint, and in NP ∩ co - NP for the ‘=1’ constraint. Further, we prove that the winning regions for both players are regular, and we design algorithms which compute the associated finite-state automata. Finally, we show that winning strategies can be synthesized effectively.

I&C Journal 2010 Journal Article

On the complexity of checking semantic equivalences between pushdown processes and finite-state processes

• Antonín Kučera
• Richard Mayr

Simulation preorder/equivalence and bisimulation equivalence are the most commonly used equivalences in concurrency theory. Their standard definitions are often called strong simulation/bisimulation, while weak simulation/bisimulation abstracts from internal τ -actions. We study the computational complexity of checking these strong and weak semantic preorders/equivalences between pushdown processes and finite-state processes. We present a complete picture of the computational complexity of these problems and also study fixed-parameter tractability in two important input parameters: x, the size of the finite control of the pushdown process, and y, the size of the finite-state process. All simulation problems are generally EXPTIME-complete and only become polynomial if both parameters x and y are fixed. Weak bisimulation equivalence is PSPACE-complete, but becomes polynomial if and only if parameter x is fixed. Strong bisimulation equivalence is PSPACE-complete, but becomes polynomial if either parameter x or y is fixed.

I&C Journal 2008 Journal Article

Reachability in recursive Markov decision processes

• Tomáš Brázdil
• Václav Brožek
• Vojtěch Forejt
• Antonín Kučera

We consider a class of infinite-state Markov decision processes generated by stateless pushdown automata. This class corresponds to 1 1 2 -player games over graphs generated by BPA systems or (equivalently) 1-exit recursive state machines. An extended reachability objective is specified by two sets S and T of safe and terminal stack configurations, where the membership to S and T depends just on the top-of-the-stack symbol. The question is whether there is a suitable strategy such that the probability of hitting a terminal configuration by a path leading only through safe configurations is equal to (or different from) a given x ∈ { 0, 1 }. We show that the qualitative extended reachability problem is decidable in polynomial time, and that the set of all configurations for which there is a winning strategy is effectively regular. More precisely, this set can be represented by a deterministic finite-state automaton with a fixed number of control states. This result is a generalization of a recent theorem by Etessami and Yannakakis which says that the qualitative termination for 1-exit RMDPs (which exactly correspond to our 1 1 2 -player BPA games) is decidable in polynomial time. Interestingly, the properties of winning strategies for the extended reachability objectives are quite different from the ones for termination, and new observations are needed to obtain the result. As an application, we derive the EXPTIME-completeness of the model-checking problem for 1 1 2 -player BPA games and qualitative PCTL formulae.

TCS Journal 2006 Journal Article

A general approach to comparing infinite-state systems with their finite-state specifications

• Antonín Kučera
• Philippe Schnoebelen

We introduce a generic family of behavioral relations for which the regular equivalence problem (i. e. , comparing an arbitrary transition system to some finite-state specification) can be reduced to the model checking problem against simple modal formulae. As an application, we derive decidability of several regular equivalence problems for well-known families of infinite-state systems.

TCS Journal 2003 Journal Article

The complexity of bisimilarity-checking for one-counter processes

• Antonín Kučera

We study the problem of bisimilarity-checking between processes of one-counter automata and finite-state processes. We show that deciding weak bisimilarity between processes of one-counter nets (which are ‘restricted’ one-counter automata where the counter cannot be tested for zero) and finite-state processes is DP-hard. In particular, this means that the problem is both NP and co-NP hard. The same technique is used to demonstrate co-NP-hardness of strong bisimilarity between processes of one-counter nets. Then we design an algorithm which decides weak bisimilarity between processes of one-counter automata and finite-state processes in time which is polynomial for a large subclass of instances, giving a kind of characterization of all hard instances as a byproduct. Moreover, we show how to efficiently estimate the time which is needed to solve a given instance. Finally, we prove that the problem of strong bisimilarity between processes of one-counter automata and finite-state processes is in P.