We show that the problem of whether a given PCTL formula has a finite model is undecidable. The undecidability result holds even for formulae of the form \(\varphi _1 \wedge {\pmb {\mathtt {G}}}_{=1} \varphi _2\) where the validity of \(\varphi _1,\varphi _2\) depends only on the states reachable in at most two transitions. Consequently, the problem of whether a given PCTL formula is valid in all finite-state Markov chains is not even semi-decidable.

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.

The Probabilistic Computational Tree Logic (PCTL) is the main specification formalism for discrete probabilistic systems modeled by Markov chains. Despite serious research attempts, the decidability of PCTL satisfiability and validity problems remained unresolved for 30 years. We show that both problems are highly undecidable, i.e., beyond the arithmetical hierarchy. Consequently, there is no sound and complete deductive system for PCTL.

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.

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.

We show that the problem of whether a given PCTL formula has a finite model is undecidable. The undecidability result holds even for formulae of the form [EQUATION] where the validity of ϕ1, ϕ2 depends only on the states reachable in at most two transitions. Consequently, the problem of whether a given PCTL formula is valid in all finite-state Markov chains is not even semi-decidable.

The standard approach to analyzing the asymptotic complexity of probabilistic programs is based on studying the asymptotic growth of certain expected values (such as the expected termination time) for increasing input size. We argue that this approach is not sufficiently robust, especially in situations when the expectations are infinite. We propose new estimates for the asymptotic analysis of probabilistic programs with non-deterministic choice that overcome this deficiency. Furthermore, we show how to efficiently compute/analyze these estimates for selected classes of programs represented as Markov decision processes over vector addition systems with states.

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.

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.

We consider the mobile robot path planning problem for a class of recurrent reachability objectives. These objectives are parameterized by the expected time needed to visit one position from another, the expected square of this time, and also the frequency of moves between two neighboring locations. We design an efficient strategy synthesis algorithm for recurrent reachability objectives and demonstrate its functionality on non-trivial instances.

We consider the problem of efficient patrolling strategy adaptation in a changing environment where the topology of Defender’s moves and the importance of guarded targets change unpredictably. The Defender must instantly switch to a new strategy optimized for the new environment, not disrupting the ongoing patrolling task, and the new strategy must be computed promptly under all circumstances. Since strategy switching may cause unintended security risks compromising the achieved protection, our solution includes mechanisms for detecting and mitigating this problem. The efficiency of our framework is evaluated experimentally.

We show that for every fixed $k\geq 3$, the problem whether the termination/counter complexity of a given demonic VASS is $\mathcal{O}(n^k)$, $Ω(n^{k})$, and $Θ(n^{k})$ is coNP-complete, NP-complete, and DP-complete, respectively. We also classify the complexity of these problems for $k\leq 2$. This shows that the polynomial-time algorithm designed for strongly connected demonic VASS in previous works cannot be extended to the general case. Then, we prove that the same problems for VASS games are PSPACE-complete. Again, we classify the complexity also for $k\leq 2$. Interestingly, tractable subclasses of demonic VASS and VASS games are obtained by bounding certain structural parameters, which opens the way to applications in program analysis despite the presented lower complexity bounds.

We design a new efficient strategy synthesis method applicable to adversarial patrolling problems on graphs with arbitrary-length edges and possibly imperfect intrusion detection. The core ingredient is an efficient algorithm for computing the value and the gradient of a function assigning to every strategy its “protection” achieved. This allows for designing an efficient strategy improvement algorithm by differentiable programming and optimization techniques. Our method is the first one applicable to real-world patrolling graphs of reasonable sizes. It outperforms the state-of-the-art strategy synthesis algorithm by a margin.

We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a finite-state program, executed by an unknown number of indistinguishable agents, where the next agent to make a move is determined by the result of a random experiment. We show that if a property of such a system holds, then there is always a witness in the shape of a Presburger stage graph : a finite graph whose nodes are Presburger-definable sets of configurations. Due to the high complexity of the verification problem (non-elementary), we introduce an incomplete procedure for the construction of Presburger stage graphs, and implement it on top of an SMT solver. The procedure makes extensive use of the theory of well-quasi-orders, and of the structural theory of Petri nets and vector addition systems. We apply our results to a set of benchmarks, in particular to a large collection of population protocols, a model of distributed computation extensively studied by the distributed computing community.

The termination complexity of a given VASS is a function L assigning to every n the length of the longest non-terminating computation initiated in a configuration with all counters bounded by n. We show that for every VASS with demonic nondeterminism and every fixed k, the problem whether L ϵ Gk, where Gk is the k-th level in the Grzegorczyk hierarchy, is decidable in polynomial time. Furthermore, we show that if L ϵ G, then L grows at least as fast as the generator Fk+1 of Gk+1. Hence, for every terminating VASS, the growth of L can be reasonably characterized by the least k such that L ϵ Gk.

We propose an algorithm for constructing efficient patrolling strategies in the Internet environment, where the protected targets are nodes connected to the network and the patrollers are software agents capable of detecting/preventing undesirable activities on the nodes. The algorithm is based on a novel compositional principle designed for a special class of strategies, and it can quickly construct (sub)optimal solutions even if the number of targets reaches hundreds of millions.

In this interactive paper, which you should preferably read connected to the Internet, the Black Ninjas introduce you to population protocols, a fundamental model of distributed computation, and to recent work by the authors and their colleagues on their automatic verification.

Vector Addition Systems with States (VASS) provide a well-known and fundamental model for the analysis of concurrent processes, parameterized systems, and are also used as abstract models of programs in resource bound analysis. In this paper we study the problem of obtaining asymptotic bounds on the termination time of a given VASS. In particular, we focus on the practically important case of obtaining polynomial bounds on termination time. Our main contributions are as follows: First, we present a polynomial-time algorithm for deciding whether a given VASS has a linear asymptotic complexity. We also show that if the complexity of a VASS is not linear, it is at least quadratic. Second, we classify VASS according to quantitative properties of their cycles. We show that certain singularities in these properties are the key reason for non-polynomial asymptotic complexity of VASS. In absence of singularities, we show that the asymptotic complexity is always polynomial and of the form Θ(nk), for some integer k ≤ d, where d is the dimension of the VASS. We present a polynomial-time algorithm computing the optimal k. For general VASS, the same algorithm, which is based on a complete technique for the construction of ranking functions in VASS, produces a valid lower bound, i.e., a k such that the termination complexity is Ω(nk). Our results are based on new insights into the geometry of VASS dynamics, which hold the potential for further applicability to VASS analysis.

We study controller synthesis problems for finite-state Markov decision processes, where the objective is to optimize the expected mean-payoff performance and stability (also known as variability in the literature). We argue that the basic notion of expressing the stability using the statistical variance of the mean payoff is sometimes insufficient, and propose an alternative definition. We show that a strategy ensuring both the expected mean payoff and the variance below given bounds requires randomization and memory, under both the above definitions. We then show that the problem of finding such a strategy can be expressed as a set of constraints.

We study graphs and two-player games in which rewards are assigned to states, and the goal of the players is to satisfy or dissatisfy certain property of the generated outcome, given as a mean payoff property. Since the notion of mean-payoff does not reflect possible fluctuations from the mean-payoff along a run, we propose definitions and algorithms for capturing the stability of the system, and give algorithms for deciding if a given mean payoff and stability objective can be ensured in the system.

We consider the fixed-delay synthesis problem for continuous-time Markov chains extended with fixed-delay transitions (fdCTMC). The goal is to synthesize concrete values of the fixed-delays (timeouts) that minimize the expected total cost incurred before reaching a given set of target states. The same problem has been considered and solved in previous works by computing an optimal policy in a certain discrete-time Markov decision process (MDP) with a huge number of actions that correspond to suitably discretized values of the timeouts. In this paper, we design a symbolic fixed-delay synthesis algorithm which avoids the explicit construction of large action spaces. Instead, the algorithm computes a small sets of "promising" candidate actions on demand. The candidate actions are selected by minimizing a certain objective function by computing its symbolic derivative and extracting a univariate polynomial whose roots are precisely the points where the derivative takes zero value. Since roots of high degree univariate polynomials can be isolated very efficiently using modern mathematical software, we achieve not only drastic memory savings but also speedup by three orders of magnitude compared to the previous methods.

We study the pattern frequency vector for runs in probabilistic Vector Addition Systems with States (pVASS). Intuitively, each configuration of a given pVASS is assigned one of finitely many patterns, and every run can thus be seen as an infinite sequence of these patterns. The pattern frequency vector assigns to each run the limit of pattern frequencies computed for longer and longer prefixes of the run. If the limit does not exist, then the vector is undefined. We show that for one-counter pVASS, the pattern frequency vector is defined and takes one of finitely many values for almost all runs. Further, these values and their associated probabilities can be approximated up to an arbitrarily small relative error in polynomial time. For stable two-counter pVASS, we show the same result, but we do not provide any upper complexity bound. As a byproduct of our study, we discover counterexamples falsifying some classical results about stochastic Petri nets published in the 80s.

We show that a subclass of infinite-state probabilistic programs that can be modeled by probabilistic one-counter automata (pOC) admits an efficient quantitative analysis. We start by establishing a powerful link between pOC and martingale theory, which leads to fundamental observations about quantitative properties of runs in pOC. In particular, we provide a “divergence gap theorem”, which bounds a positive non-termination probability in pOC away from zero. Using these observations, we show that the expected termination time can be approximated up to an arbitrarily small relative error in polynomial time, and the same holds for the probability of all runs that satisfy a given ω-regular property encoded by a deterministic Rabin automaton.

We study the complexity of central controller synthesis problems for finite-state Markov decision processes, where the objective is to optimize both the expected mean-payoff performance of the system and its stability. e argue that the basic theoretical notion of expressing the stability in terms of the variance of the mean-payoff (called global variance in our paper) is not always sufficient, since it ignores possible instabilities on respective runs. For this reason we propose alernative definitions of stability, which we call local and hybrid variance, and which express how rewards on each run deviate from the run's own mean-payoff and from the expected mean-payoff, respectively. We show that a strategy ensuring both the expected mean-payoff and the variance below given bounds requires randomization and memory, under all the above semantics of variance. We then look at the problem of determining whether there is a such a strategy. For the global variance, we show that the problem is in PSPACE, and that the answer can be approximated in pseudo-polynomial time. For the hybrid variance, the analogous decision problem is in NP, and a polynomial-time approximating algorithm also exists. For local variance, we show that the decision problem is in NP. Since the overall performance can be traded for stability (and vice versa), we also present algorithms for approximating the associated Pareto curve in all the three cases. Finally, we study a special case of the decision problems, where we require a given expected mean-payoff together with zero variance. Here we show that the problems can be all solved in polynomial time.

federated and organized in parallel by Masaryk University in Brno, Czech Republic.The MFCS symposia, organized since 1972, encourage high-quality research in all branches of theoretical computer science.The broad scope of MFCS provides an opportunity to bring together researchers who do not usually meet at specialized conferences.Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL).The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science.

We propose deterministic timed automata (DTA) as a model-independent language for specifying performance and dependability measures over continuous-time stochastic processes. Technically, these measures are defined as limit frequencies of locations (control states) of a DTA that observes computations of a given stochastic process. Then, we study the properties of DTA measures over semi-Markov processes in greater detail. We show that DTA measures over semi-Markov processes are well-defined with probability one, and there are only finitely many values that can be assumed by these measures with positive probability. We also give an algorithm which approximates these values and the associated probabilities up to an arbitrarily small given precision. Thus, we obtain a general and effective framework for analysing DTA measures over semi-Markov processes.

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

We study the computational complexity of some central analysis problems for One-Counter Markov Decision Processes (OC-MDPs), a class of finitely-presented, countable-state MDPs. OC-MDPs extend finite-state MDPs with an unbounded counter. The counter can be incremented, decremented, or not changed during each state transition, and transitions may be enabled or not depending on both the current state and on whether the counter value is 0 or not. Some states are “random”, from where the next transition is chosen according to a given probability distribution, while other states are “controlled”, from where the next transition is chosen by the controller. Different objectives for the controller give rise to different computational problems, aimed at computing optimal achievable objective values and optimal strategies. OC-MDPs are in fact equivalent to a controlled extension of (discrete-time) Quasi-Birth-Death processes (QBDs), a purely stochastic model heavily studied in queueing theory and applied probability. They can thus be viewed as a natural “adversarial” extension of a classic stochastic model. They can also be viewed as a natural probabilistic/controlled extension of classic one-counter automata. OC-MDPs also subsume (as a very restricted special case) a recently studied MDP model called “solvency games” that model a risk-averse gambling scenario. Basic computational questions for OC-MDPs include “termination” questions and “limit” questions, such as the following: does the controller have a strategy to ensure that the counter (which may, for example, count the number of jobs in the queue) will hit value 0 (the empty queue) almost surely (a.s.)? Or that the counter will have lim sup value ∞, a.s.? Or, that it will hit value 0 in a selected terminal state, a.s.? Or, in case such properties are not satisfied almost surely, compute their optimal probability over all strategies. We provide new upper and lower bounds on the complexity of such problems. Specifically, we show that several quantitative and almost-sure limit problems can be answered in polynomial time, and that almost-sure termination problems (without selection of desired terminal states) can also be answered in polynomial time. On the other hand, we show that the almost-sure termination problem with selected terminal states is PSPACE-hard and we provide an exponential time algorithm for this problem. We also characterize classes of strategies that suffice for optimality in several of these settings. Our upper bounds combine a number of techniques from the theory of MDP reward models, the theory of random walks, and a variety of automata-theoretic methods.

We study continuous-time stochastic games with time-bounded reachability objectives. We show that each vertex in such a game has a \emph{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 $\varepsilon$-optimal strategies in finitely-branching games with bounded rates (for finite games, we provide detailed complexity estimations).

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 $\textbf{NP} \cap \textbf{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.

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 phi 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 phi has a model of the branching degree at most k, where k > 2 is an arbitrary but fixed constant, is highly undecidable. We also show that every satisfiable formula phi has a model with branching degree at most \phi\ + 2. However, this does not yet imply the undecidability of the satisfiability problem for quantitative PCTL, and we in fact conjecture the opposite.

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.

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 PCTL and the subclass of stateless pPDA. Finally, we consider the class of omega-regular properties and show that both qualitative and quantitative model checking for pPDA is decidable.

The paper presents a selection of recently developed and/or used techniques for equivalence-checking on infinite-state systems, and an up-to-date overview of existing results (as of September 2004).

We introduce a family of long-run average properties of Markov chains that are useful for purposes of performance and reliability analysis, and show that these properties can effectively be checked for a subclass of infinite-state Markov chains generated by probabilistic programs with recursive procedures. We also show how to predict these properties by analyzing finite prefixes of runs, and present an efficient prediction algorithm for the mentioned subclass of Markov chains.

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.

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.

Let ∼ be a process equivalence. A formula φ is preserved by ∼-quotients iff for every process s of a transition system T we have that if s satisfies φ, then also [s] satisfies φ, where [s] is the equivalence class of s in the quotient of T under ∼. We classify all formulae of Hennessy–Milner logic which are preserved by ∼-quotients of image-finite processes. Our result is generic in the sense that it works for a large class of process equivalences which admit a modal characterization in Hennessy–Milner logic satisfying certain closure properties. Practical applicability of the result is demonstrated on equivalences of the linear/branching time spectrum.