Showing 1–17 of 17 results for author: Quatmann, T

Compositional Reasoning for Parametric Probabilistic Automata

Authors: Hannah Mertens, Tim Quatmann, Joost-Pieter Katoen

Abstract: 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… ▽ More 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. △ Less

Submitted 10 June, 2025; originally announced June 2025.

Comments: Full version of a paper accepted for publication at CONCUR 2025

Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains

Authors: Linus Heck, Tim Quatmann, Jip Spel, Joost-Pieter Katoen, Sebastian Junges

Abstract: 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… ▽ More 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. △ Less

Submitted 8 April, 2025; originally announced April 2025.

Fixed Point Certificates for Reachability and Expected Rewards in MDPs

Authors: Krishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, Daniel Zilken

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 quantitat… ▽ More 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. △ Less

Submitted 20 January, 2025; originally announced January 2025.

Comments: Extended version of the TACAS 2025 paper

A Spectrum of Approximate Probabilistic Bisimulations

Authors: Timm Spork, Christel Baier, Joost-Pieter Katoen, Jakob Piribauer, Tim Quatmann

Abstract: 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 in… ▽ More 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. △ Less

Submitted 10 July, 2024; originally announced July 2024.

Comments: Full version of a paper accepted for publication at CONCUR 2024

Tools at the Frontiers of Quantitative Verification

Authors: Roman Andriushchenko, Alexander Bork, Carlos E. Budde, Milan Češka, Kush Grover, Ernst Moritz Hahn, Arnd Hartmanns, Bryant Israelsen, Nils Jansen, Joshua Jeppson, Sebastian Junges, Maximilian A. Köhl, Bettina Könighofer, Jan Křetínský, Tobias Meggendorfer, David Parker, Stefan Pranger, Tim Quatmann, Enno Ruijters, Landon Taylor, Matthias Volk, Maximilian Weininger, Zhen Zhang

Abstract: 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 o… ▽ More 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. △ Less

Submitted 22 May, 2024; originally announced May 2024.

Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains

Authors: Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler

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… ▽ More 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. △ Less

Submitted 20 February, 2024; v1 submitted 19 January, 2024; originally announced January 2024.

A Practitioner's Guide to MDP Model Checking Algorithms

Authors: Arnd Hartmanns, Sebastian Junges, Tim Quatmann, Maximilian Weininger

Abstract: 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… ▽ More 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. △ Less

Submitted 24 January, 2023; originally announced January 2023.

Under-Approximating Expected Total Rewards in POMDPs

Authors: Alexander Bork, Joost-Pieter Katoen, Tim Quatmann

Abstract: 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 s… ▽ More 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. △ Less

Submitted 21 January, 2022; originally announced January 2022.

Comments: Technical report for TACAS 2022 paper with the same title

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

Authors: Tim Quatmann, Joost-Pieter Katoen

Abstract: 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 o… ▽ More 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. △ Less

Submitted 7 January, 2021; v1 submitted 26 October, 2020; originally announced October 2020.

Verification of indefinite-horizon POMDPs

Authors: Alexander Bork, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann

Abstract: 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… ▽ More 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. △ Less

Submitted 30 June, 2020; originally announced July 2020.

Comments: Technical report for ATVA 2020 paper with the same title

The Probabilistic Model Checker Storm

Authors: Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk

Abstract: 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 probabilist… ▽ More 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. △ Less

Submitted 6 October, 2020; v1 submitted 17 February, 2020; originally announced February 2020.

Simple Strategies in Multi-Objective MDPs (Technical Report)

Authors: Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, Mickael Randour

Abstract: 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… ▽ More 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. △ Less

Submitted 17 February, 2020; v1 submitted 24 October, 2019; originally announced October 2019.

Parameter Synthesis for Markov Models: Covering the Parameter Space

Authors: Sebastian Junges, Erika Ábrahám, Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk

Abstract: 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 ch… ▽ More 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. △ Less

Submitted 7 November, 2023; v1 submitted 16 March, 2019; originally announced March 2019.

Comments: 86 pages. Preprint of accepted FMSD Journal Paper

Sound Value Iteration

Authors: Tim Quatmann, Joost-Pieter Katoen

Abstract: 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 con… ▽ More 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. △ Less

Submitted 13 April, 2018; originally announced April 2018.

Comments: Technical Report

Permissive Finite-State Controllers of POMDPs using Parameter Synthesis

Authors: Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker

Abstract: We study finite-state controllers (FSCs) for partially observable Markov decision processes (POMDPs) that are provably correct with respect to given specifications. The key insight is that computing (randomised) FSCs on POMDPs is equivalent to - and computationally as hard as - synthesis for parametric Markov chains (pMCs). This correspondence allows to use tools for parameter synthesis in pMCs to… ▽ More We study finite-state controllers (FSCs) for partially observable Markov decision processes (POMDPs) that are provably correct with respect to given specifications. The key insight is that computing (randomised) FSCs on POMDPs is equivalent to - and computationally as hard as - synthesis for parametric Markov chains (pMCs). This correspondence allows to use tools for parameter synthesis in pMCs to compute correct-by-construction FSCs on POMDPs for a variety of specifications. Our experimental evaluation shows comparable performance to well-known POMDP solvers. △ Less

Submitted 17 July, 2018; v1 submitted 24 October, 2017; originally announced October 2017.

Comments: This is an extended version of the paper: S. Junges, N. Jansen, R. Wimmer, T. Quatmann, L. Winterer, J.-P. Katoen, B. Becker: Finite-state Controllers of POMDPs via Parameter Synthesis. Proceedings of the Conference on Uncertainty in Artificial Intelligence (UAI 2018), Monterey, CA, USA, August 6-10, 2018

Markov Automata with Multiple Objectives

Authors: Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen

Abstract: Markov automata combine non-determinism, probabilistic branching, and exponentially distributed delays. This compositional variant of continuous-time Markov decision processes is used in reliability engineering, performance evaluation and stochastic scheduling. Their verification so far focused on single objectives such as (timed) reachability, and expected costs. In practice, often the objectives… ▽ More Markov automata combine non-determinism, probabilistic branching, and exponentially distributed delays. This compositional variant of continuous-time Markov decision processes is used in reliability engineering, performance evaluation and stochastic scheduling. Their verification so far focused on single objectives such as (timed) reachability, and expected costs. In practice, often the objectives are mutually dependent and the aim is to reveal trade-offs. We present algorithms to analyze several objectives simultaneously and approximate Pareto curves. This includes, e.g., several (timed) reachability objectives, or various expected cost objectives. We also consider combinations thereof, such as on-time-within-budget objectives - which policies guarantee reaching a goal state within a deadline with at least probability $p$ while keeping the allowed average costs below a threshold? We adopt existing approaches for classical Markov decision processes. The main challenge is to treat policies exploiting state residence times, even for untimed objectives. Experimental results show the feasibility and scalability of our approach. △ Less

Submitted 10 May, 2017; v1 submitted 21 April, 2017; originally announced April 2017.

Parameter Synthesis for Markov Models: Faster Than Ever

Authors: Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen

Abstract: We propose a simple technique for verifying probabilistic models whose transition probabilities are parametric. The key is to replace parametric transitions by nondeterministic choices of extremal values. Analysing the resulting parameter-free model using off-the-shelf means yields (refinable) lower and upper bounds on probabilities of regions in the parameter space. The technique outperforms the… ▽ More We propose a simple technique for verifying probabilistic models whose transition probabilities are parametric. The key is to replace parametric transitions by nondeterministic choices of extremal values. Analysing the resulting parameter-free model using off-the-shelf means yields (refinable) lower and upper bounds on probabilities of regions in the parameter space. The technique outperforms the existing analysis of parametric Markov chains by several orders of magnitude regarding both run-time and scalability. Its beauty is its applicability to various probabilistic models. It in particular provides the first sound and feasible method for performing parameter synthesis of Markov decision processes. △ Less

Submitted 26 May, 2016; v1 submitted 16 February, 2016; originally announced February 2016.