A fundamental computational task in probabilistic programming is to infer a program’s output (posterior) distribution from a given initial (prior) distribution. This problem is challenging, especially for expressive languages that feature loops or unbounded recursion. While most of the existing literature focuses on statistical approximation, in this paper we address the problem of mathematically exact inference. To achieve this for programs with loops, we rely on a relatively underexplored type of probabilistic loop invariant, which is linked to a loop’s so-called occupation measure . The occupation measure associates program states with their expected number of visits, given the initial distribution. Based on this, we derive the notion of an occupation invariant . Such invariants are essentially dual to probabilistic martingales, the predominant technique for formal probabilistic loop analysis in the literature. A key feature of occupation invariants is that they can take the initial distribution into account and often yield a proof of positive almost sure termination as a by-product. Finally, we present an automatic, template-based invariant synthesis approach for occupation invariants by encoding them as generating functions . The approach is implemented and evaluated on a set of benchmarks.

Abstract This paper presents a Hoare-like verification framework for discrete probabilistic programs that we apply to two non-trivial sampling algorithms: Lumbroso’s Fast Dice Roller and Saad et al.’s Fast Loaded Dice Roller . These algorithms have previously resisted formal verification due to their probabilistic nature, intricate loop structure, and parametric input. Our approach complements existing proof rules based on inductive distributional invariants, enabling us to verify both total and partial correctness of the two algorithms.

Abstract Markov decision processes model systems subject to nondeterministic and probabilistic uncertainty. A plethora of verification techniques addresses variations of reachability properties, such as: Is there a scheduler resolving the nondeterminism such that the probability to reach an error state is above a threshold? We consider an understudied extension that relates different reachability probabilities, such as: Is there a scheduler such that two sets of states are reached with different probabilities? These questions appear naturally in the design of randomized algorithms and in various security applications. We provide a tractable algorithm for many variations of this problem, while proving computational hardness of some others. An implementation of our algorithm beats solvers for more general probabilistic hyperlogics by orders of magnitude, on the subset of their benchmarks that are within our fragment.

Abstract The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates —lightweight, easy-to-check proofs of the verification results. In this paper, we develop novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties. Our approach is conceptually simple and relies almost exclusively on elementary fixed point theory. Our certificates work for arbitrary finite MDPs and can be readily computed with little overhead using standard algorithms. We formalize the soundness of our certificates in and provide a formally verified certificate checker . Moreover, we augment existing algorithms in the probabilistic model checker with the ability to produce certificates and demonstrate practical applicability by conducting the first formal certification of the reference results in the Quantitative Verification Benchmark Set.

Abstract We study the accurate and efficient computation of the expected number of times each state is visited in discrete- and continuous-time Markov chains. To obtain sound accuracy guarantees efficiently, we lift interval iteration, optimistic value iteration and topological approaches developed to compute reachability probabilities and expected rewards and prove all these algorithms to be correct. We further establish that expected visiting times are preserved under backward probabilistic bisimilarity. We study various applications of expected visiting times. The reachability probabilities of multiple bottom strongly connected components (BSCCs) can be obtained by solving a single linear equation system—as opposed to solving an equation system per BSCC. Other applications include the sound computation of the stationary distribution as well as expected rewards conditioned on reaching multiple goal states. The implementation of our methods in the probabilistic model checker Storm scales to large systems with millions of states. Our experiments on the quantitative verification benchmark set show that the computation of stationary distributions via expected visiting times consistently outperforms existing approaches—sometimes by several orders of magnitude.

We lay out novel foundations for the computer-aided verification of guaranteed bounds on expected outcomes of imperative probabilistic programs featuring (i) general loops , (ii) continuous distributions, and (iii) conditioning . To handle loops we rely on user-provided quantitative invariants , as is well established. However, in the realm of continuous distributions, invariant verification becomes extremely challenging due to the presence of integrals in expectation-based program semantics. Our key idea is to soundly under- or over-approximate these integrals via Riemann sums . We show that this approach enables the SMT-based invariant verification for programs with a fairly general control flow structure. On the theoretical side, we prove convergence of our Riemann approximations, and establish coRE-completeness of the central verification problems. On the practical side, we show that our approach enables to use existing automated verifiers targeting discrete probabilistic programs for the verification of programs involving continuous sampling . Towards this end, we implement our approach in the recent quantitative verification infrastructure Caesar by encoding Riemann sums in its intermediate verification language. We present several promising case studies.

Abstract We study the accurate and efficient computation of the expected number of times each state is visited in discrete- and continuous-time Markov chains. To obtain sound accuracy guarantees efficiently, we lift interval iteration and topological approaches known from the computation of reachability probabilities and expected rewards. We further study applications of expected visiting times, including the sound computation of the stationary distribution and expected rewards conditioned on reaching multiple goal states. The implementation of our methods in the probabilistic model checker scales to large systems with millions of states. Our experiments on the quantitative verification benchmark set show that the computation of stationary distributions via expected visiting times consistently outperforms existing approaches — sometimes by several orders of magnitude.

Abstract We study turn-based stochastic zero-sum games with lexicographic preferences over objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as controllable and adversarial non-determinism. Lexicographic order allows one to consider multiple objectives with a strict preference order. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. For a mixture of reachability and safety objectives, we show that deterministic lexicographically optimal strategies exist and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in $$\textsf{NP}\cap \textsf{coNP}$$ NP ∩ coNP , matching the current known bound for single objectives; and in general the decision problem is $$\textsf{PSPACE}$$ PSPACE -hard and can be solved in $$\textsf{NEXPTIME}\cap \textsf{coNEXPTIME}$$ NEXPTIME ∩ coNEXPTIME . We present an algorithm that computes the lexicographically optimal strategies via a reduction to the computation of optimal strategies in a sequence of single-objectives games. For omega-regular objectives, we restrict our analysis to one-player games, also known as Markov decision processes. We show that lexicographically optimal strategies exist and need either randomization or finite memory. We present an algorithm that solves the relevant decision problem in polynomial time. We have implemented our algorithms and report experimental results on various case studies.

We consider imperative programs that involve both randomization and pure nondeterminism. The central question is how to find a strategy resolving the pure nondeterminism such that the so-obtained determinized program satisfies a given quantitative specification, i.e., bounds on expected outcomes such as the expected final value of a program variable or the probability to terminate in a given set of states. We show how memoryless and deterministic (MD) strategies can be obtained in a semi-automatic fashion using deductive verification techniques. For loop-free programs, the MD strategies resulting from our weakest preconditionstyle framework are correct by construction. This extends to loopy programs, provided the loops are equipped with suitable loop invariants - just like in program verification. We show how our technique relates to the well-studied problem of obtaining strategies in countably infinite Markov decision processes with reachabilityreward objectives. Finally, we apply our technique to several case studies.

Probabilistic pushdown automata (pPDA) are a natural operational model for a variety of recursive discrete stochastic processes. In this paper, we study certificates – succinct and easily verifiable proofs – for upper and lower bounds on various quantitative properties of a given pPDA. We reveal an intimate, yet surprisingly simple connection between the existence of such certificates and the expected time to termination of the pPDA at hand. This is established by showing that certain intrinsic properties, like the spectral radius of the Jacobian of the pPDA’s underlying polynomial equation system, are directly related to expected runtimes. As a consequence, we obtain that there always exist easy-to-check proofs for positive almost-sure termination: does a pPDA terminate in finite expected time?

Abstract Probabilistic pushdown automata (pPDA) are a standard model for discrete probabilistic programs with procedures and recursion. In pPDA, many quantitative properties are characterized as least fixpoints of polynomial equation systems. In this paper, we study the problem ofcertifyingthat these quantities lie within certain bounds. To this end, we first characterize the polynomial systems that admit easy-to-check certificates for validating bounds on their least fixpoint. Second, we present a sound and complete Optimistic Value Iteration algorithm for computing such certificates. Third, we show how certificates for polynomial systems can be transferred to certificates for various quantitative pPDA properties. Experiments demonstrate that our algorithm computes succinct certificates for several intricate example programs as well as stochastic context-free grammars with $$> 10^4$$ production rules.

Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices and recursive procedures. Temporal properties are useful for specifying the chronological order of events during program execution. Existing approaches for model checking pPDA against temporal properties have focused mostly on $\omega$-regular and LTL properties. In this paper, we give decidability and complexity results for the model checking problem of pPDA against $\omega$-visibly pushdown languages that can be described by specification logics such as CaRet. These logical formulae allow specifying properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties such as total and partial correctness.

Abstract We study discrete probabilistic programs with potentially unbounded looping behaviors over an infinite state space. We present, to the best of our knowledge,the first decidability result for the problem of determining whether such a program generates exactly a specified distribution over its outputs(provided the program terminates almost-surely). The class of distributions that can be specified in our formalism consists of standard distributions (geometric, uniform, etc.) and finite convolutions thereof. Our method relies on representing these (possibly infinite-support) distributions asprobability generating functionswhich admit effective arithmetic operations. We have automated our techniques in a tool called $$\textsc {Prodigy}$$ PRODIGY , which supports automatic invariance checking, compositional reasoning of nested loops, and efficient queries to the output distribution, as demonstrated by experiments.

Abstract Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices, procedures, and returns. Temporal properties are useful for gaining insight into the chronological order of events during program execution. Existing approaches in the literature have focused mostly on $$\omega $$ ω -regular and LTL properties. In this paper, we study the model checking problem of pPDA against $$\omega $$ ω -visibly pushdown languages that can be described by specification logics such as CaRet and are strictly more expressive than $$\omega $$ ω -regular properties. With these logical formulae, it is possible to specify properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties like total and partial correctness.

We study weighted programming, a programming paradigm for specifying mathematical models. More specifically, the weighted programs we investigate are like usual imperative programs with two additional features: (1) nondeterministic branching and (2) weighting execution traces. Weights can be numbers but also other objects like words from an alphabet, polynomials, formal power series, or cardinal numbers. We argue that weighted programming as a paradigm can be used to specify mathematical models beyond probability distributions (as is done in probabilistic programming). We develop weakest-precondition- and weakest-liberal-precondition-style calculi à la Dijkstra for reasoning about mathematical models specified by weighted programs. We present several case studies. For instance, we use weighted programming to model the ski rental problem — an optimization problem. We model not only the optimization problem itself, but also the best deterministic online algorithm for solving this problem as weighted programs. By means of weakest-precondition-style reasoning, we can determine the competitive ratio of the online algorithm on source code level.

We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as angelic and demonic non-determinism. Lexicographic order allows to consider multiple objectives with a strict preference order over the satisfaction of the objectives. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. We establish determinacy of such games and present strategy and computational complexity results. For strategy complexity, we show that lexicographically optimal strategies exist that are deterministic and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in $$\mathsf {NP}\cap \mathsf {coNP}$$ , matching the current known bound for single objectives; and in general the decision problem is $$\mathsf {PSPACE}$$ -hard and can be solved in $$\mathsf {NEXPTIME}\cap \mathsf {coNEXPTIME}$$ . We present an algorithm that computes the lexicographically optimal strategies via a reduction to computation of optimal strategies in a sequence of single-objectives games. We have implemented our algorithm and report experimental results on various case studies.

Simple stochastic games are turn-based 2½-player games with a reachability objective. The basic question asks whether one player can ensure reaching a given target with at least a given probability. A natural extension is games with a conjunction of such conditions as objective. Despite a plethora of recent results on the analysis of systems with multiple objectives, the decidability of this basic problem remains open. In this paper, we present an algorithm approximating the Pareto frontier of the achievable values to a given precision. Moreover, it is an anytime algorithm, meaning it can be stopped at any time returning the current approximation and its error bound.

This paper studies parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over a finite set of parameters. Fixing values for all parameters yields MDPs. In particular, this paper studies the complexity of finding values for these parameters such that the induced MDP satisfies some reachability constraints. We discuss different variants depending on the comparison operator in the constraints and the domain of the parameter values. We improve all known lower bounds for this problem, and notably provide ETR-completeness results for distinct variants of this problem. Furthermore, we provide insights in the functions describing the induced reachability probabilities, and how pMDPs generalise concurrent stochastic reachability games.

In this paper, we report on the realization of an immersive table tennis simulation. After describing the hardware necessities of our system, we give insight into different aspects of the simulation. In particular, the developed methods for collision detection and physical simulation are presented. The design of the virtual opponent is of crucial importance to realize an enjoyable game. Therefore, we report on the implemented game strategy and the animation of the opponent. Since table tennis is one of the fastest sports, the synchronization of the human player's movements and the visual output on the projection wall is a very challenging problem to solve. To overcome the latencies in our system, we designed a prediction method that allows high speed interaction with our application.