arXiv subjects

Tim Quatmann

Publications and source records attributed to Tim Quatmann.

At least 19 recordsLinked to original sources

arXiv2026

UMB: A Unified Markov Binary Format for Probabilistic Model Checking (extended version)

This paper presents the unified Markov binary (UMB) format, an efficient, extensible, and well-supported explicit-state file format for representing a wide range of probabilistic systems. UMB addresses the problem that, while probabilistic model checking tools often support common high-level modelling languages, there is no effective mechanism for exchanging low-level model representations. In practice, textual, tool-specific formats are used, hampering interoperability and resulting in large overheads in writing and reading model files. UMB provides a clean, unified, and efficient solution, based on a general underlying mathematical model, and encoded using a small set of bit-level primitive data structures. The format has already been adopted by prominent tools and comes with a convenient Python library for reading, manipulating, creating, and validating models, plus infrastructure for cross-tool installation and continuous validation. We report on both the efficiency of the file format and the new practical use cases that it facilitates.

cs.LO↗

arXiv2026

Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families

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.

cs.LO↗

arXiv2026

Compositional Reasoning for Probabilistic Automata with Uncertainty

This paper develops an assume-guarantee (AG) framework for the compositional verification of probabilistic automata (PAs) with uncertain transition probabilities. We study parametric probabilistic automata (pPAs), where probabilities are given by polynomial functions over a finite set of real-valued parameters and robust probabilistic automata (rPAs)-a generalisation of interval probabilistic automata (iPAs)-where transition probabilities range over potentially uncountable uncertainty sets. Towards pPAs, an existing AG framework for PAs is lifted to the parametric setting. We establish asymmetric, circular, and interleaving proof rules to enable compositional verification of a broad class of multi-objective queries, encompassing probabilistic reachability properties and parametric expected total rewards. In addition, we introduce a dedicated AG rule for compositional reasoning about parameter monotonicity. For convex rPAs and iPAs with history-dependent (memory-full) nature, we establish sound AG rules via a reduction to infinite PAs. We further show that AG reasoning can not straightforwardly be applied to non-convex rPAs, memoryless (once-and-for-all) nature semantics, and the common interval-arithmetic relaxation of parallel composition. Finally, we develop a simulation-based AG style for pPAs: we define strong simulation and robust-strong simulation relations for pPAs and derive their corresponding proof rules.

cs.LO↗

arXiv2026

Probabilistic Model Checking Taken by Storm

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.

cs.SE↗

arXiv2025

Compositional Reasoning for Parametric Probabilistic Automata

We establish an assume-guarantee (AG) framework for compositional reasoning about multi-objective queries in parametric probabilistic automata (pPA) - an extension to probabilistic automata (PA), where transition probabilities are functions over a finite set of parameters. We lift an existing framework for PA to the pPA setting, incorporating asymmetric, circular, and interleaving proof rules. Our approach enables the verification of a broad spectrum of multi-objective queries for pPA, encompassing probabilistic properties and (parametric) expected total rewards. Additionally, we introduce a rule for reasoning about monotonicity in composed pPAs.

cs.LO↗

arXiv2025

Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains

Parametric Markov chains (pMCs) are Markov chains (MCs) with symbolic probabilities. A pMC encodes a family of MCs, where each member is obtained by replacing parameters with constants. The parameters allow encoding dependencies between transitions, which sets pMCs apart from interval MCs. The verification problem for pMCs asks whether each MC in the corresponding family satisfies a given temporal specification. The state-of-the-art approach for this problem is parameter lifting (PL) -- an abstraction-refinement loop that abstracts the pMC to a non-parametric model analyzed with standard probabilistic model checking techniques. This paper presents two key improvements to tackle the main limitations of PL. First, we introduce generalized parameter lifting (GPL) to lift various restrictive assumptions made by PL. Second, we present a big-step transformation algorithm that reduces parameter dependencies in pMCs and, therefore, results in tighter approximations. Experiments show that GPL is widely applicable and that the big-step transformation accelerates pMC verification by up to orders of magnitude.

cs.LO↗

arXiv2025

Fixed Point Certificates for Reachability and Expected Rewards in MDPs

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 Isabelle/HOL and provide a formally verified certificate checker. Moreover, we augment existing algorithms in the probabilistic model checker Storm 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.

cs.LO↗

arXiv2024

A Spectrum of Approximate Probabilistic Bisimulations

This paper studies various notions of approximate probabilistic bisimulation on labeled Markov chains (LMCs). We introduce approximate versions of weak and branching bisimulation, as well as a notion of $\varepsilon$-perturbed bisimulation that relates LMCs that can be made (exactly) probabilistically bisimilar by small perturbations of their transition probabilities. We explore how the notions interrelate and establish their connections to other well-known notions like $\varepsilon$-bisimulation.

cs.LO↗

arXiv2024

Tools at the Frontiers of Quantitative Verification

The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification.

cs.LO↗

arXiv2024

Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains

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

cs.LO↗

arXiv2023

A Practitioner's Guide to MDP Model Checking Algorithms

Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) is 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 program, 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 optimisations 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.

cs.LO↗

arXiv2022

Under-Approximating Expected Total Rewards in POMDPs

We consider the problem: is the optimal expected total reward to reach a goal state in a partially observable Markov decision process (POMDP) below a given threshold? We tackle this -- generally undecidable -- problem by computing under-approximations on these total expected rewards. This is done by abstracting finite unfoldings of the infinite belief MDP of the POMDP. The key issue is to find a suitable under-approximation of the value function. We provide two techniques: a simple (cut-off) technique that uses a good policy on the POMDP, and a more advanced technique (belief clipping) that uses minimal shifts of probabilities between beliefs. We use mixed-integer linear programming (MILP) to find such minimal probability shifts and experimentally show that our techniques scale quite well while providing tight lower bounds on the expected total reward.

cs.AI↗

arXiv2020

Multi-objective Optimization of Long-run Average and Total Rewards

This paper presents an efficient procedure for multi-objective model checking of long-run average reward (aka: mean pay-off) and total reward objectives as well as their combination. We consider this for Markov automata, a compositional model that captures both traditional Markov decision processes (MDPs) as well as a continuous-time variant thereof. The crux of our procedure is a generalization of Forejt et al.'s approach for total rewards on MDPs to arbitrary combinations of long-run and total reward objectives on Markov automata. Experiments with a prototypical implementation on top of the Storm model checker show encouraging results for both model types and indicate a substantial improved performance over existing multi-objective long-run MDP model checking based on linear programming.

cs.LO↗

arXiv2020

Verification of indefinite-horizon POMDPs

The verification problem in MDPs asks whether, for any policy resolving the nondeterminism, the probability that something bad happens is bounded by some given threshold. This verification problem is often overly pessimistic, as the policies it considers may depend on the complete system state. This paper considers the verification problem for partially observable MDPs, in which the policies make their decisions based on (the history of) the observations emitted by the system. We present an abstraction-refinement framework extending previous instantiations of the Lovejoy-approach. Our experiments show that this framework significantly improves the scalability of the approach.

cs.AI↗

arXiv2020

The Probabilistic Model Checker Storm

We present the probabilistic model checker Storm. Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm has three major distinguishing features. It supports multiple input languages for Markov models, including the JANI and PRISM modeling languages, dynamic fault trees, generalized stochastic Petri nets, and the probabilistic guarded command language. It has a modular set-up in which solvers and symbolic engines can easily be exchanged. Its Python API allows for rapid prototyping by encapsulating Storm's fast and scalable algorithms. This paper reports on the main features of Storm and explains how to effectively use them. A description is provided of the main distinguishing functionalities of Storm. Finally, an empirical evaluation of different configurations of Storm on the QComp 2019 benchmark set is presented.

cs.SE↗

arXiv2019

Simple Strategies in Multi-Objective MDPs (Technical Report)

We consider the verification of multiple expected reward objectives at once on Markov decision processes (MDPs). This enables a trade-off analysis among multiple objectives by obtaining the Pareto front. We focus on strategies that are easy to employ and implement. That is, strategies that are pure (no randomization) and have bounded memory. We show that checking whether a point is achievable by a pure stationary strategy is NP-complete, even for two objectives, and we provide an MILP encoding to solve the corresponding problem. The bounded memory case can be reduced to the stationary one by a product construction. Experimental results using \Storm and Gurobi show the feasibility of our algorithms.

cs.LO↗

arXiv2019

Parameter Synthesis for Markov Models: Covering the Parameter Space

Markov chain analysis is a key technique in formal verification. A practical obstacle is that all probabilities in Markov models need to be known. However, system quantities such as failure rates or packet loss ratios, etc. are often not -- or only partially -- known. This motivates considering parametric models with transitions labeled with functions over parameters. Whereas traditional Markov chain analysis relies on a single, fixed set of probabilities, analysing parametric Markov models focuses on synthesising parameter values that establish a given safety or performance specification $\varphi$. Examples are: what component failure rates ensure the probability of a system breakdown to be below 0.00000001?, or which failure rates maximise the performance, for instance the throughput, of the system? This paper presents various analysis algorithms for parametric discrete-time Markov chains and Markov decision processes. We focus on three problems: (a) do all parameter values within a given region satisfy $\varphi$?, (b) which regions satisfy $\varphi$ and which ones do not?, and (c) an approximate version of (b) focusing on covering a large fraction of all possible parameter values. We give a detailed account of the various algorithms, present a software tool realising these techniques, and report on an extensive experimental evaluation on benchmarks that span a wide range of applications.

cs.LO↗

arXiv2018

Sound Value Iteration

Computing reachability probabilities is at the heart of probabilistic model checking. All model checkers compute these probabilities in an iterative fashion using value iteration. This technique approximates a fixed point from below by determining reachability probabilities for an increasing number of steps. To avoid results that are significantly off, variants have recently been proposed that converge from both below and above. These procedures require starting values for both sides. We present an alternative that does not require the a priori computation of starting vectors and that converges faster on many benchmarks. The crux of our technique is to give tight and safe bounds - whose computation is cheap - on the reachability probabilities. Lifting this technique to expected rewards is trivial for both Markov chains and MDPs. Experimental results on a large set of benchmarks show its scalability and efficiency.

cs.LO↗