Technical Reports

A List by Author: Tomá¹ Brázdil

e-mail:

brazdil(a)fi.muni.cz

Verification of Open Interactive Markov Chains

by Tomá¹ Brázdil, Holger Hermanns, Jan Krèál, Jan Køetínský, Vojtìch Øehák, A full version of the paper presented at conference FSTTCS 2012. November 2012, 52 pages.

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

Abstract:

Interactive Markov chains (IMC) are compositional behavioral models extending both labeled transition systems and continuous-time Markov chains. IMC pair modeling convenience - owed to compositionality properties - with effective verification algorithms and tools - owed to Markov properties. Thus far however, IMC verification did not consider compositionality properties, but considered closed systems. This paper discusses the evaluation of IMC in an open and thus compositional interpretation. For this we embed the IMC into a game that is played with the environment. We devise algorithms that enable us to derive bounds on reachability probabilities that are assured to hold in any composition context.

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).

On the Memory Consumption of Probabilistic Pushdown Automata

by Tomá¹ Brázdil, Javier Esparza, Stefan Kiefer, A full version of the paper presented at FSTTCS 2009 October 2009, 52 pages.

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

Abstract:

We investigate the problem of evaluating memory consumption for systems modelled by probabilistic pushdown automata (pPDA). The space needed by a run of a pPDA is the maximal height reached by the stack during the run. The problem is motivated by the investigation of depth-first computations that play an important role for space-efficient schedulings of multithreaded programs. We study the computation of both the distribution of the memory consumption and its expectation. For the distribution, we show that a naive method incurs an exponential blow-up, and that it can be avoided using linear equation systems. We also suggest a possibly even faster approximation method. Given epsilon>0, these methods allow to compute bounds on the memory consumption that are exceeded with a probability of at most epsilon. For the expected memory consumption, we show that whether it is infinite can be decided in polynomial time for stateless pPDA (pBPA) and in polynomial space for pPDA. We also provide an iterative method for approximating the expectation. We show how to compute error bounds of our approximation method and analyze its convergence speed. We prove that our method converges linearly, i.e., the number of accurate bits of the approximation is a linear function of the number of iterations.

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.

Strategy Synthesis for Markov Decision Processes and Branching-Time Logics

by Tomá¹ Brázdil, Vojtìch Forejt, A full version of the paper presented at CONCUR 2007 July 2007, 28 pages.

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

Abstract:

We consider a class of finite $1\frac{1}{2}$-player games (Markov decision processes) where the winning objectives are specified in the branching-time temporal logic qPECTL$^*$ (an extension of the qualitative PCTL$^*$). We study decidability and complexity of existence of a winning strategy in these games. %The logic is more expressive than the qualitative fragment of PCTL$^*$. We identify a fragment of qPECTL$^*$ called detPECTL$^*$ for which the existence of a winning strategy is decidable in exponential time, and also the winning strategy can be computed in exponential time (if it exists). Consequently we show that every formula of qPECTL$^*$ can be translated to a formula of detPECTL$^*$ (in exponential time) so that the resulting formula is equivalent to the original one over finite Markov chains. From this we obtain that for the whole qPECTL$^*$, the existence of a winning finite-memory strategy is decidable in double exponential time. An immediate consequence is that the existence of a winning finite-memory strategy is decidable for the qualitative fragment of PCTL$^*$ in triple exponential time. We also obtain a single exponential upper bound on the same problem for the qualitative PCTL. Finally, we study the power of finite-memory strategies with respect to objectives described in the qualitative PCTL.

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.

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.

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.