Technical Reports

A List by Author: Antonín Kuèera

e-mail:

tony(a)fi.muni.cz

home page:

https://www.fi.muni.cz/usr/kucera/

Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes

by Tomá¹ Brázdil, Václav Bro¾ek, Krishnendu Chatterjee, Vojtìch Forejt, Antonín Kuèera, A full version of the paper presented at conference LICS 2011. April 2011, 32 pages.

FIMU-RS-2011-02. Available as Postscript, PDF.

Abstract:

We study Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) functions. We consider two different objectives, namely, expectation and satisfaction objectives. Given an MDP with k reward functions, in the expectation objective the goal is to maximize the expected limit-average value, and in the satisfaction objective the goal is to maximize the probability of runs such that the limit-average value stays above a given vector. We show that under the expectation objective, in contrast to the single-objective case, both randomization and memory are necessary for strategies, and that finite-memory randomized strategies are sufficient. Under the satisfaction objective, in contrast to the single-objective case, infinite memory is necessary for strategies, and that randomized memoryless strategies are sufficient for epsilon-approximation, for all epsilon. We further prove that the decision problems for both expectation and satisfaction objectives can be solved in polynomial time and the trade-off curve (Pareto curve) can be epsilon-approximated in time polynomial in the size of the MDP and 1/epsilon, and exponential in the number of reward functions, for all epsilon>0. Our results also reveal flaws in previous work for MDPs with multiple mean-payoff functions under the expectation objective, correct the flaws and obtain improved results.

Stochastic Real-Time Games with Qualitative Timed Automata Objectives

by Tomá¹ Brázdil, Jan Krèál, Jan Køetínský, Antonín Kuèera, Vojtìch Øehák, A full version of the paper presented at CONCUR 2010. August 2010, 39 pages.

FIMU-RS-2010-05. Available as Postscript, PDF.

Abstract:

We consider two-player stochastic games over real-time probabilistic processes where the winning objective is specified by a timed automaton. The goal of player I is to play in such a way that the play (a timed word) is accepted by the timed automaton with probability one. Player II aims at the opposite. We prove that whenever player I has a winning strategy, then she also has a strategy that can be specified by a timed automaton. The strategy automaton reads the history of a play, and the decisions taken by the strategy depend only on the region of the resulting configuration. We also give an exponential-time algorithm which computes a winning timed automaton strategy if it exists.

Reachability Games on Extended Vector Addition Systems with States

by Tomá¹ Brázdil, Petr Janèar, Antonín Kuèera, A full version of the paper presented at ICALP 2010. February 2010, 38 pages.

FIMU-RS-2010-02. Available as Postscript, PDF.

Abstract:

We consider two-player turn-based games with zero-reachability and zero-safety objectives generated by extended vector addition systems with states. Although the problem of deciding the winner in such games is undecidable in general, we identify several decidable and even tractable subcases of this problem obtained by restricting the number of counters and/or the sets of target configurations.

Continuous-Time Stochastic Games with Time-Bounded Reachability

by Tomá¹ Brázdil, Vojtìch Forejt, Jan Krèál, Jan Køetínský, Antonín Kuèera, A full version of the paper presented at FST&TCS 2009. October 2009, 46 pages.

FIMU-RS-2009-09. Available as Postscript, PDF.

Abstract:

We study continuous-time stochastic games with time-bounded reachability objectives. 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. Finally, we show how to compute optimal strategies in finite uniform games, and how to compute e-optimal strategies in finitely-branching games with bounded rates (for finite games, we provide detailed complexity estimations).

Qualitative Reachability in Stochastic BPA Games

by Václav Bro¾ek, Tomá¹ Brázdil, Antonín Kuèera, Jan Obdr¾álek, A full version of the paper presented at STACS 2009. May 2009, 37 pages.

FIMU-RS-2009-01. Available as Postscript, PDF.

Abstract:

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 NP intersection co-NP. 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.

Discounted Properties of Probabilistic Pushdown Automata

by Tomá¹ Brázdil, Václav Bro¾ek, Jan Holeèek, Antonín Kuèera, A full version of the paper presented at LPAR 2008 September 2008, 31 pages.

FIMU-RS-2008-08. Available as Postscript, PDF.

Abstract:

We show that several basic discounted properties of probabilistic pushdown automata related both to terminating and non-terminating runs can be efficiently approximated up to an arbitrarily small given precision.

Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives

by Tomá¹ Brázdil, Vojtìch Forejt, Antonín Kuèera, A full version of the paper presented at ICALP 2008. December 2008, 48 pages.

FIMU-RS-2008-05. Available as Postscript, PDF.

Abstract:

We show that controller synthesis and verification problems for Markov decision processes with qualitative PECTL* objectives are 2-EXPTIME complete. More precisely, the algorithms are polynomial in the size of a given Markov decision process and doubly exponential in the size of a given qualitative PECTL* formula. Moreover, we show that if a given qualitative PECTL* objective is achievable by some strategy, then it is also achievable by an effectively constructible one-counter strategy, where the associated complexity bounds are essentially the same as above. For the fragment of qualitative PCTL objectives, we obtain EXPTIME completeness and the algorithms are only singly exponential in the size of the formula.

The Satisfiability Problem for Probabilistic CTL

by Tomá¹ Brázdil, Vojtìch Forejt, Jan Køetínský, Antonín Kuèera, A full version of the paper presented at LICS 2008. June 2008, 34 pages.

FIMU-RS-2008-03. Available as Postscript, PDF.

Abstract:

We study the satisfiability problem for qualitative PCTL (Probabilistic Computation Tree Logic), which is obtained from "ordinary" CTL by replacing the EX, AX, EU, and AU operators with their qualitative counterparts X>0, X=1, U>0, and U=1, respectively. As opposed to CTL, qualitative PCTL does not have a small model property, and there are even qualitative PCTL formulae which have only infinite-state models. Nevertheless, we show that the satisfiability problem for qualitative PCTL is EXPTIME-complete and we give an exponential-time algorithm which for a given formula computes a finite description of a model (if it exists), or answers "not satisfiable" (otherwise). We also consider the finite satisfiability problem and provide analogous results. That is, we show that the finite satisfiability problem for qualitative PCTL is EXPTIME-complete, and every finite satisfiable formula has a model of an exponential size which can effectively be constructed in exponential time. Finally, we give some results about the quantitative PCTL, where the numerical bounds in probability constraints can be arbitrary rationals between 0 and 1. We prove that the problem whether a given quantitative PCTL formula has a model of the branching degree at most k, where k > 1 is an arbitrary but fixed constant, is highly undecidable. We also show that every satisfiable formula F has a model with branching degree at most |F| + 2. However, this does not yet imply the undecidability of the satisfiability problem for quantitative PCTL, and we in fact conjecture the opposite.

Stochastic Games with Branching-Time Winning Objectives

by Tomá¹ Brázdil, Václav Bro¾ek, Vojtìch Forejt, Antonín Kuèera, A full version of the paper presented at LICS 2006. September 2006, 37 pages.

FIMU-RS-2006-02. Available as Postscript, PDF.

Abstract:

We consider stochastic turn-based games where the winning objectives are given by formulae of the branching-time logic PCTL. These games are generally not determined and winning strategies may require memory and/or randomization. Our main results concern history-dependent strategies. In particular, we show that the problem whether there exists a history-dependent winning strategy in 1.5-player games is highly undecidable, even for objectives formulated in the L(F^{=5/8},F^{=1},F^{>0},G^{=1}) fragment of PCTL. On the other hand, we show that the problem becomes decidable (and in fact EXPTIME-complete) for the L(F^{=1},F^{>0},G^{=1}) fragment of PCTL, where winning strategies require only finite memory. This result is tight in the sense that winning strategies for L(F^{=1},F^{>0},G^{=1},G^{>0}) objectives may already require infinite memory.

Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances

by Javier Esparza, Antonín Kuèera, Richard Mayr, A full version of the paper presented at LICS 2005. July 2005, 26 pages.

FIMU-RS-2005-07. Available as Postscript, PDF.

Abstract:

Probabilistic pushdown automata (pPDA) have been identified as a natural model for probabilistic programs with recursive procedure calls. Previous works considered the decidability and complexity of the model-checking problem for pPDA and various probabilistic temporal logics. In this paper we concentrate on computing the expected values and variances of various random variables defined over runs of a given probabilistic pushdown automaton. In particular, we show how to compute the expected accumulated reward and the expected gain for certain classes of reward functions. Using these results, we show how to analyze various quantitative properties of pPDA that are not expressible in conventional probabilistic temporal logics.

On the Decidability of Temporal Properties of Probabilistic Pushdown Automata

by Tomá¹ Brázdil, Antonín Kuèera, Oldøich Stra¾ovský, A full version of the paper presented at STACS 2005. February 2005, 33 pages.

FIMU-RS-2005-01. Available as Postscript, PDF.

Abstract:

We consider qualitative and quantitative model-checking problems for probabilistic pushdown automata (pPDA) and various temporal logics. We prove that the qualitative and quantitative model-checking problem for omega-regular properties and pPDA is in 2-EXPSPACE and 3-EXPTIME, respectively. We also prove that model-checking the qualitative fragment of the logic PECTL* for pPDA is in 2-EXPSPACE, and model-checking the qualitative fragment of PCTL for pPDA is in EXPSPACE. Furthermore, model-checking the qualitative fragment of PCTL is shown to be EXPTIME-hard even for stateless pPDA. Finally, we show that PCTL model-checking is undecidable for pPDA, and PCTL+ model-checking is undecidable even for stateless pPDA.

Characteristic Patterns for LTL

by Antonín Kuèera, Jan Strejèek, A full version of the paper presented at Sofsem 2005. December 2004, 22 pages.

FIMU-RS-2004-10. Available as Postscript, PDF.

Abstract:

We give a new characterization of those languages that are definable in fragments of LTL where the nesting depths of X and U modalities are bounded by given constants. This brings further results about various LTL fragments. We also propose a generic method for decomposing LTL formulae into an equivalent disjunction of ``semantically refined" LTL formulae, and indicate how this result can be used to improve the functionality of existing LTL model-checkers.

Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems

by Tomá¹ Brázdil, Antonín Kuèera, Oldøich Stra¾ovský, A full version of the paper presented at CONCUR`04. September 2004, 26 pages.

FIMU-RS-2004-06. Available as Postscript, PDF.

Abstract:

We prove that probabilistic bisimilarity is decidable over probabilistic extensions of BPA and BPP processes. For normed subclasses of probabilistic BPA and BPP processes we obtain polynomial-time algorithms. Further, we show that probabilistic bisimilarity between probabilistic pushdown automata and finite-state systems is decidable in exponential time. If the number of control states in PDA is bounded by a fixed constant, then the algorithm needs only polynomial time.

A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications

by Antonín Kuèera, Philippe Schnoebelen, A full version of the paper presented at CONCUR`04. June 2004, 32 pages.

FIMU-RS-2004-05. Available as Postscript, PDF.

Abstract:

We introduce a generic family of behavioral relations for which the problem of comparing an arbitrary transition system to some finite-state specification can be reduced to a 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.

An Effective Characterization of Properties Definable by LTL Formulae with a Bounded Nesting Depth of the Next-Time Operator

by Antonín Kuèera, Jan Strejèek, May 2004, 11 pages.

FIMU-RS-2004-04. Available as Postscript, PDF.

Abstract:

It is known that an LTL property is expressible by an LTL formula without any next-time operator if and only if the property is stutter invariant. It is also known that the problem whether a given LTL property is stutter invariant is PSPACE-complete. We extend these results to fragments of LTL obtained by restricting the nesting depth of the next-time operator to a given n. Some interesting facts about the logic LTL follow as simple corollaries.

Model Checking Probabilistic Pushdown Automata

by Javier Esparza, Antonín Kuèera, Richard Mayr, A full version of the paper presented at LICS`04. July 2004, 34 pages.

FIMU-RS-2004-03. Available as Postscript, PDF.

Abstract:

We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model checking for this class of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for general PCTL and the subclass of stateless pPDA. Finally, we consider the class of properties definable by deterministic Buchi automata, and show that both qualitative and quantitative model checking for pPDA is decidable.

A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata

by Antonín Kuèera, Richard Mayr, A full version of the paper presented at IFIP TCS 2004. April 2004, 38 pages.

FIMU-RS-2004-01. Available as Postscript, PDF.

Abstract:

We propose a generic method for deciding semantic equivalences between pushdown automata and finite-state automata. The abstract part of the method is applicable to every process equivalence which is a right PDA congruence. Practical usability of the method is demonstrated on selected equivalences which are conceptual representatives of the whole spectrum. In particular, special attention is devoted to bisimulation-like equivalences (including weak, early, delay, branching, and probabilistic bisimilarity), and it is also shown how the method applies to simulation-like and trace-like equivalences. The generality does not lead to the loss of efficiency; the algorithms obtained by applying our method are essentially time-optimal and sometimes even polynomial. The list of particular results obtained by our method includes items which are first of their kind.

Pre-Proceedings of INFINITY 2002

by Antonín Kuèera, Richard Mayr, August 2002, 153 pages.

FIMU-RS-2002-04. Available as Postscript, PDF.

Abstract:

This volume contains pre-proceedings of 4th International Workshop on Verification of Infinite-State Systems (INFINITY 2002), held on August 24, 2002, in Brno, Czech Republic. The workshop was organized as a satellite event of CONCUR 2002.

The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL

by Antonín Kuèera, Jan Strejèek, A full version of the paper presented at CSL`02. July 2002, 24 pages.

FIMU-RS-2002-03. Available as Postscript, PDF.

Abstract:

It is known that LTL formulae without the `next` operator are invariant under the so-called stutter-equivalence of words. In this paper we extend this principle to general LTL formulae with given nesting depths of the `next` and `until` operators. This allows us to prove the semantical strictness of three natural hierarchies of LTL formulae, which are parametrized either by the nesting depth of just one of the two operators, or by both of them. As another interesting corollary we obtain an alternative characterization of LTL languages, which are exactly the regular languages closed under the generalized form of stutter equivalence. We also indicate how to tackle the state-space explosion problem with the help of presented results.

Why is Simulation Harder Than Bisimulation?

by Antonín Kuèera, Richard Mayr, A full version of the paper presented at CONCUR`02 June 2002, 26 pages.

FIMU-RS-2002-02. Available as Postscript, PDF.

Abstract:

Why is deciding simulation preorder (and simulation equivalence) computationally harder than deciding bisimulation equivalence on almost all known classes of processes? We try to answer this question by describing two general methods that can be used to construct direct one-to-one polynomial-time reductions from bisimulation equivalence to simulation preorder (and simulation equivalence). These methods can be applied to many classes of finitely generated transition systems, provided that they satisfy certain abstractly formulated conditions. Roughly speaking, our first method works for all classes of systems that can test for `non-enabledness` of actions, while our second method works for all classes of systems that are closed under synchronization.

On the Complexity of Semantic Equivalences for Pushdown Automata and BPA

by Antonín Kuèera, Richard Mayr, A full version of the paper presented at MFCS`02. May 2002, 32 pages.

FIMU-RS-2002-01. Available as Postscript, PDF.

Abstract:

We study the complexity of comparing pushdown automata (PDA) and context-free processes (BPA) to finite-state systems, w.r.t. strong and weak simulation preorder/equivalence and strong and weak bisimulation equivalence. We present a complete picture of the complexity of all these problems. In particular, we show that strong and weak simulation preorder (and hence simulation equivalence) is EXPTIME-complete between PDA/BPA and finite-state systems in both directions. For PDA the lower bound even holds if the finite-state system is fixed, while simulation-checking between BPA and any fixed finite-state system is already polynomial. Furthermore, we show that weak (and strong) bisimilarity between PDA and finite-state systems is PSPACE-complete, while strong (and weak) bisimilarity between two (normed) PDAs is EXPTIME-hard.

On Simulation-Checking with Sequential Systems

by Antonín Kuèera, This is a full version of the paper accepted for ASIAN 2000. September 2000, 34 pages.

FIMU-RS-2000-05. Available as Postscript, PDF.

Abstract:

We present new complexity results for simulation-checking and model-checking with infinite-state systems generated by pushdown automata and their proper subclasses of one-counter automata and one-counter nets (one-counter nets are "weak" one-counter automata computationally equivalent to Petri nets with at most one unbounded place).

As for simulation-checking, we show the following: a) simulation equivalence between pushdown processes and finite-state processes is EXPTIME-complete; b) simulation equivalence between processes of one-counter automata and finite-state processes is coNP-hard; c) simulation equivalence between processes of one-counter nets and finite-state processes is in P (to the best of our knowledge, it is the first (and rather tight) polynomiality result for simulation with infinite-state processes).

As for model-checking, we prove that a) the problem of simulation-checking between processes of pushdown automata (or one-counter automata, or one-counter nets) and finite-state processes are polynomially reducible to the model-checking problem with a fixed formula F = nu X. [z]<z> X of the modal mu-calculus. Consequently, model-checking with F is EXPTIME-complete for pushdown processes and coNP-hard for processes of one-counter automata; b) model-checking with a fixed formula <>[a]<>[b]ff of the logic EF (a simple fragment of CTL) is NP-hard for processes of OC nets, and model-checking with another fixed formula []<a>[]<b>tt of EF is coNP-hard. Consequently, model-checking with any temporal logic which can express these simple formulae is computationally hard even for the (very simple) sequential processes of OC-nets.

Efficient Verification Algorithms for One-Counter Processes

by Antonín Kuèera, This is a full version of the paper presented at ICALP 2000. March 2000, 24 pages.

FIMU-RS-2000-03. Available as Postscript, PDF.

Abstract:

We study the problem of strong/weak bisimilarity between processes of one-counter automata and finite-state processes. We show that the problem of weak bisimilarity between processes of one-counter nets (which are "weak" one-counter automata) and finite-state processes is DP-hard (in particular, it 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 most "practical" instances, giving a characterization of all hard instances as a byproduct. Moreover, we show how to efficiently compute a rather tight bound for 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.

A Logical Viewpoint on Process-Algebraic Quotients

by Antonín Kuèera, Javier Esparza, This is a full and revised version of a paper which previously appeared in Proceedings of CSL`99. January 2000, 26 pages.

FIMU-RS-2000-01. Available as Postscript, PDF.

Abstract:

We study the following problem: Given a transition system T and its quotient T/~ under an equivalence ~, which are the sets L, L` of Hennessy-Milner formulae such that: if f belongs to L and T satisfies f, then T/~ satisfies f; if f belongs to L` and T/~ satisfies f, then T satisfies f.

Bisimilarity of Processes with Finite-state Systems

by Petr Janèar, Antonín Kuèera, These results will be presented at INFINITY`97 workshop. May 1997, 19 pages.

FIMU-RS-97-02. Available as Postscript, PDF.

Abstract:

We describe a general method for deciding bisimilarity for pairs of processes where one process has finitely many states. We apply this method to pushdown processes and to PA processes. We also demonstrate that the mentioned problem is undecidable for `state-extended` PA processes.

How to Parallelize Sequential Processes

by Antonín Kuèera, Accepted to the 8th International Conference on Concurrency Theory (CONCUR`97). December 1996, 24 pages.

FIMU-RS-96-05. Available as Postscript, PDF.

Abstract:

A process is prime if it cannot be decomposed into a parallel product of nontrivial processes. We characterize all non-prime normed BPA processes together with their decompositions in terms of normal forms which are designed in this paper. Then we show that it is decidable whether a given normed BPA process is prime and if not, its decomposition can be effectively constructed. This brings other positive decidability results. Finally, we prove that bisimilarity is decidable in a large subclass of normed PA processes.

Comparing Expressibility of Normed BPA and Normed BPP Processes

by Ivana Èerná, Mojmír Køetínský, Antonín Kuèera, This is a full version of the paper which is to be presented at CSL`96. June 1996, 28 pages.

FIMU-RS-96-02. Available as Postscript, PDF.

Abstract:

We compare the classes of behaviours (transition systems) which can be generated by normed BPA_{\tau} and normed BPP_{\tau} processes. We exactly classify the intersection of these two classes, i.e., the class of transition systems which can be equivalently (up to bisimilarity) described by the syntax of normed BPA_{\tau} and normed BPP_{\tau} processes. We provide such a characterisation for classes of normed BPA and normed BPP processes as well.

Next we show that it is decidable in polynomial time whether for a given normed BPA_{\tau} (or BPP_{\tau} respectively) process X there is some (unspecified) normed BPP_{\tau} (or BPA_{\tau} respectively) process X` such that X is bisimilar to X`. Moreover, if the answer is positive then our algorithms also construct the process X`. Simplified versions of the algorithms mentioned above for normed BPA and normed BPP are given too.

As an immediate (but important) consequence we also obtain the decidability of bisimilarity in the union of normed BPA_{\tau} and normed BPP_{\tau} processes.

Regularity is Decidable for Normed PA Processes in Polynomial Time

by Antonín Kuèera, This paper is going to be presented at FST&TCS`96 conference, LNCS 1180, Springer-Verlag. February 1996, 17 pages.

FIMU-RS-96-01. Available as Postscript, PDF.

Abstract:

A process X is regular if it is bisimilar to a process X` with finitely many states. We prove that regularity of normed PA processes is decidable and we present a practically usable polynomial-time algorithm. Moreover, if the tested normed PA process X is regular then the process X` can be effectively constructed. It implies decidability of bisimulation equivalence for any pair of processes such that one process is a normed PA process and the other process has finitely many states.