Tim Quatmann

TACAS Conference 2026 Conference Paper

Multiple Long-Run and $$\omega $$-Regular Objectives in MDPs

• Julius Ide
• Joost-Pieter Katoen
• Hannah Mertens
• Tim Quatmann

FM Conference 2026 Conference Paper

Probabilistic Model Checking Taken by Storm

• Matthias Volk
• Linus Heck
• Sebastian Junges
• Joost-Pieter Katoen
• Tim Quatmann

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

FM Conference 2026 Conference Paper

Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking

• Arnd Hartmanns
• Tim Quatmann
• Mark van Wijk

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

UAI Conference 2025 Conference Paper

Multi-Cost-Bounded Reachability Analysis of POMDPs

• Alexander Bork
• Joost-Pieter Katoen
• Tim Quatmann
• Svenja Stein

We consider multi-dimensional cost-bounded reachability probability objectives for partially observable Markov decision processes (POMDPs). The goal is to compute the maximal probability to reach a set of target states while simultaneously satisfying specified bounds on incurred costs. Such objectives generalise well-studied POMDP objectives by allowing multiple upper and lower bounds on different cost or reward measures, e. g. to naturally model scenarios where an agent acts under limited resources. We present a reduction of the multi-cost-bounded problem to unbounded reachability probabilities on an unfolding of the original POMDP. We employ a refined approach in case the agent is cost-aware-i. e. , collected costs are fully observed-and also consider a setting where only partial information about the collected costs is known. Our approaches elegantly lift existing results from the fully observable MDP case to POMDPs. An empirical evaluation shows the potential of analysing POMDPs under multi-cost-bounded reachability objectives in practical settings.

UAI Conference 2018 Conference Paper

Finite-State Controllers of POMDPs using Parameter Synthesis

• Sebastian Junges
• Nils Jansen 0001
• Ralf Wimmer 0001
• Tim Quatmann
• Leonore Winterer
• Joost-Pieter Katoen
• Bernd Becker 0001

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