Tim Quatmann

Computing optimal conditional reachability probabilities in Markov decision processes (MDPs) is tractable by a reduction to reachability probabilities. Yet, this reduction yields cyclic, challenging MDPs that are often notoriously hard to solve. We present an alternative, practically efficient method to compute optimal conditional reachabilities. This new method is numerically stable, can decide the threshold problem in linear time on acyclic MDPs, and yields performance comparable to standard reachability queries. We also integrate the method in an abstraction-refinement framework to analyse millions of Markov chains at once. We demonstrate the efficacy of the new methods on benchmarks from Bayesian network analysis, probabilistic programs, and runtime monitoring and show speed-ups up to multiple orders of magnitude.

This tutorial paper presents a hands-on perspective on probabilistic model checking with the Storm model checker. Storm is a decade-old model checker that excels in performance and a rich Python-based ecosystem, which makes it easy to integrate in various workflows. This tutorial focuses on Markov decision processes (MDP), which are popular in a variety of fields. It demonstrates the basic workflow, from Python-based modeling, model checking with a variety of properties, to the extraction of policies. Further, it showcases the support for recent topics that focus on different types of uncertainty, such as interval MDP and POMDP, and the ability to quickly implement simple algorithms on top of existing data structures.

Practical verification tasks often involve multiple goals, such as maximising an expected reward within a specified reliability threshold. Algorithms to solve such multi-objective probabilistic model checking (MO-PMC) problems were developed over a decade ago, and are implemented by multiple tools. However, the algorithms are unsound in general—at best delivering some underapproximation of the true result—and the implementations are unreliable, with different tools producing inconsistent results. In this paper, we present the first implementations of recently-developed sound MO-PMC algorithms that bound the true result from above and below, in two independent tools. We discuss ways to consistently treat infinite rewards and extend the algorithms with relative-error termination criteria. On the practical side, we add support for multi-objective properties to the Jani interchange format for tool interoperability, and extend the Quantitative Verification Benchmark Set with multi-objective problems. Based on the latter, we conduct an extensive experimental evaluation of the two tools’ new sound MO-PMC capabilities, showing in particular that they produce consistent results.

Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) are key for the verification of systems that act under uncertainty. Popular algorithms are policy iteration and variants of value iteration; in tool competitions, most participants rely on the latter. These algorithms generally need worst-case exponential time. However, the problem can equally be formulated as a linear programme, solvable in polynomial time. In this paper, we give a detailed overview of today’s state-of-the-art algorithms for MDP model checking with a focus on performance and correctness. We highlight their fundamental differences, and describe various optimizations and implementation variants. We experimentally compare floating-point and exact-arithmetic implementations of all algorithms on three benchmark sets using two probabilistic model checkers. Our results show that (optimistic) value iteration is a sensible default, but other algorithms are preferable in specific settings. This paper thereby provides a guide for MDP verification practitioners—tool builders and users alike.

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.

Computing reachability probabilities and expected rewards for Markov decision processes is a core feature of probabilistic model checkers. Value iteration (VI) is the predominantly implemented approach but occasionally yields vastly incorrect results. Interval iteration (II), sound value iteration (SVI), and optimistic value iteration (OVI) are recently proposed variants of VI that produce sound approximations of the desired values. Hartmanns and Kaminski (CAV (2), pp. 488–511, 2020) empirically compared the three approaches using implementations in the model checker mcsta and a broad selection of benchmarks. They concluded that OVI is faster than II and SVI for the majority of instances. We replicate these research results using implementations in the model checker Storm. The key insight is that OVI still mostly outperforms II and SVI, but the competition becomes tighter.

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.