arXiv subjects

Arnd Hartmanns

Publications and source records attributed to Arnd Hartmanns.

At least 19 recordsLinked to original sources

arXiv2026

Path Abstraction for Markov Reward Models

Path abstraction originated as a technique for counterexample refinement in probabilistic model checking. Given a discrete-time Markov chain, it summarises the probabilities passing through a subset of the states onto new transitions of a smaller chain. In earlier work, we proved its correctness and that it is monotonically absorbing. In this paper, we extend path abstraction from reachability probabilities on discrete-time Markov chains to expected rewards on Markov reward models. Working in a novel free monoid view of Markov chains throughout, we prove that path abstraction preserves the Markov reward model structure when abstracting over arbitrary sets of states, and that it remains monotonically absorbing. Finally, we give a numerical recipe, accompanied by a reference implementation in PARI/GP, that computes path abstraction by solving linear equation systems. Its correctness rests on the relationship between expected rewards and expected visiting times of transitions.

cs.FL↗

arXiv2026

Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)

Stochastic automata (SA) are a formal stochastic continuous-time model based on countdown timers whose expiration times follow general probability distributions. SA are particularly useful to faithfully model and analyse dependable systems involving faults, maintenance, and repairs. Effective SA analysis approaches have so far been limited to statistical model checking and thus deterministic SA, while previously proposed model-checking techniques apply to limited subclasses of SA only, or do not scale. In this paper, we present the first dedicated SA model checking approach that is general and effective: It puts few restrictions on the input SA, and we show in our experimental evaluation that it works well for nontrivial examples. It combines a refinable interval abstraction of the continuous distributions with a direct application of the "big time steps" semantics of SA, providing upper/lower bounds on maximum/minimum reachability probabilities. We extend the Modest and Jani modelling formalisms with support for SA, and provide a prototype implementation of our approach in Rust.

cs.LO↗

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↗

arXiv2025

Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling (extended version)

Statistical model checking delivers quantitative verification results with statistical guarantees. It scales to model sizes and model types that are out of reach for exhaustive, analytical techniques. So far, it has been used to evaluate one property value at a time only. Many practical problems, however, require finding the Pareto front of optimal tradeoffs between multiple objectives. In this paper, we present the first statistical model checking approach for such multi-objective Pareto queries, based on lightweight strategy sampling. We introduce an incremental scheme that almost surely converges to a statistically sound confidence band around the true Pareto front in the long run. To obtain a close underapproximation of the true front in finite time, we propose three heuristic approaches that try to make the best of an a-priori fixed sampling budget. We implement our new techniques in the modes simulator of the Modest Toolset, and show their effectiveness on benchmarks from the literature.

cs.LO↗

arXiv2025

Probabilistic Verification for Modular Network-on-Chip Systems (extended version)

Quantitative verification can provide deep insights into reliable Network-On-Chip (NoC) designs. It is critical to understanding and mitigating operational issues caused by power supply noise (PSN) early in the design process: fluctuations in network traffic in modern NoC designs cause dramatic variations in power delivery across the network, leading to unreliability and errors in data transfers. Further complicating these challenges, NoC designs vary widely in size, usage, and implementation. This case study paper presents a principled, systematic, and modular NoC modeling approach using the Modest language that closely reflects the standard hierarchical design approach in digital systems. Using the Modest Toolset, functional and quantitative correctness was established for several NoC models, all of which were instantiated from a generic modular router model. Specifically, this work verifies the functional correctness of a generic router, inter-router communication, and the entire NoC. Statistical model checking was used to verify PSN-related properties for NoCs of size up to 8x8.

cs.LO↗

arXiv2025

A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs

We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstract semantics of MDPs to a low-level implementation in LLVM that is based on floating-point arithmetic. We use the Isabelle/HOL proof assistant to verify convergence of our abstract definition of interval iteration and employ step-wise refinement to derive an efficient implementation in LLVM code. To that end, we extend the Isabelle Refinement Framework with support for reasoning about floating-point arithmetic and directed rounding modes. We experimentally demonstrate that the verified implementation is competitive with state-of-the-art tools for MDPs, while providing formal guarantees on the correctness of the results.

cs.LO↗

arXiv2025

Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality (extended version)

Statistical model checking (SMC) randomly samples probabilistic models to approximate quantities of interest with statistical error guarantees. It is traditionally used to estimate probabilities and expected rewards, i.e. means of different random variables on paths. In this paper, we develop methods using the Dvoretzky-Kiefer-Wolfowitz-Massart inequality (DKW) to extend SMC beyond means to compute quantities such as quantiles, conditional value-at-risk, and entropic risk. The DKW provides confidence bounds on the random variable's entire cumulative distribution function, a much more versatile guarantee compared to the statistical methods prevalent in SMC today. We have implemented support for computing new quantities via the DKW in the 'modes' simulator of the Modest Toolset. We highlight the implementation and its versatility on benchmarks from the quantitative verification literature.

stat.ME↗

arXiv2025

Sound Statistical Model Checking for Probabilities and Expected Rewards (extended version)

Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guarantees. However, many tools use unsound statistical methods that produce incorrect results more often than they claim. In this paper, we provide a comprehensive overview of tools and their correctness, as well as of sound methods available for estimating probabilities from the literature. For expected rewards, we investigate how to bound the path reward distribution to apply sound statistical methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz inequality that has not been used in SMC so far. We prove that even reachability rewards can be bounded in theory, and formalise the concept of limit-PAC procedures for a practical solution. The 'modes' SMC tool implements our methods and recommendations, which we use to experimentally confirm our results.

cs.LO↗

arXiv2025

DTMC Model Checking by Path Abstraction Revisited (extended version)

Computing the probability of reaching a set of goal states G in a discrete-time Markov chain (DTMC) is a core task of probabilistic model checking. We can do so by directly computing the probability mass of the set of all finite paths from the initial state to G; however, when refining counterexamples, it is also interesting to compute the probability mass of subsets of paths. This can be achieved by splitting the computation into path abstractions that calculate "local" reachability probabilities as shown by Ábrahám et al. in 2010. In this paper, we complete and extend their work: We prove that splitting the computation into path abstractions indeed yields the same result as the direct approach, and that the splitting does not need to follow the SCC structure. In particular, we prove that path abstraction can be performed along any finite sequence of sets of non-goal states. Our proofs proceed in a novel way by interpreting the DTMC as a structure on the free monoid on its state space, which makes them clean and concise. Additionally, we provide a compact reference implementation of path abstraction in PARI/GP.

cs.FL↗

arXiv2025

Time-Sensitive Importance Splitting

State-of-the-art methods for rare event simulation of non-Markovian models face practical or theoretical limits if observing the event of interest requires prior knowledge or information on the timed behavior of the system. In this paper, we attack both limits by extending importance splitting with a time-sensitive importance function. To this end, we perform backwards reachability search from the target states, considering information about the lower and upper bounds of the active timers in order to steer the generation of paths towards the rare event. We have developed a prototype implementation of the approach for input/output stochastic automata within the Modest Toolset. Preliminary experiments show the potential of the approach in estimating rare event probabilities for an example from reliability engineering.

cs.LO↗

arXiv2024

Digging for Decision Trees: A Case Study in Strategy Sampling and Learning

We introduce a formal model of transportation in an open-pit mine for the purpose of optimising the mine's operations. The model is a network of Markov automata (MA); the optimisation goal corresponds to maximising a time-bounded expected reward property. Today's model checking algorithms exacerbate the state space explosion problem by applying a discretisation approach to such properties on MA. We show that model checking is infeasible even for small mine instances. Instead, we propose statistical model checking with lightweight strategy sampling or table-based Q-learning over untimed strategies as an alternative to approach the optimisation task, using the Modest Toolset's modes tool. We add support for partial observability to modes so that strategies can be based on carefully selected model features, and we implement a connection from modes to the dtControl tool to convert sampled or learned strategies into decision trees. We experimentally evaluate the adequacy of our new tooling on the open-pit mine case study. Our experiments demonstrate the limitations of Q-learning, the impact of feature selection, and the usefulness of decision trees as an explainable representation.

cs.FL↗

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↗

arXiv2023

Reproduction Report for SV-COMP 2023

The Competition on Software Verification (SV-COMP) is a large computational experiment benchmarking many different software verification tools on a vast collection of C and Java benchmarks. Such experimental research should be reproducible by researchers independent from the team that performed the original experiments. In this reproduction report, we present our recent attempt at reproducing SV-COMP 2023: We chose a meaningful subset of the competition and re-ran it on the competition organiser's infrastructure, using the scripts and tools provided in the competition's archived artifacts. We see minor differences in tool scores that appear explainable by the interaction of small runtime fluctuations with the competition's scoring rules, and successfully reproduce the overall ranking within our chosen subset. Overall, we consider SV-COMP 2023 to be reproducible.

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

Backwards Reachability for Probabilistic Timed Automata: A Replication Report

Backwards reachability is an efficient zone-based approach for model checking probabilistic timed automata w.r.t. PTCTL properties. Current implementations, however, are restricted to maximum probabilities of reachability properties. In this paper, we report on our new implementation of backwards reachability as part of the Modest Toolset. Its support for minimum and maximum probabilities of until formulas makes it the most general implementation available today. We compare its behaviour to the experimental results reported in the original papers presenting the backwards reachability technique.

cs.LO↗

arXiv2022

An Overview of Modest Models and Tools for Real Stochastic Timed Systems

We depend on the safe, reliable, and timely operation of cyber-physical systems ranging from smart grids to avionics components. Many of them involve time-dependent behaviours and are subject to randomness. Modelling languages and verification tools thus need to support these quantitative aspects. In my invited presentation at MARS 2022, I gave an introduction to quantitative verification using the Modest modelling language and the Modest Toolset, and highlighted three recent case studies with increasing demands on model expressiveness and tool capabilities: A case of power supply noise in a network-on-chip modelled as a Markov chain; a case of message routing in satellite constellations that uses Markov decision processes with distributed information; and a case of optimising an attack on Bitcoin via Markov automata model checking. This paper summarises the presentation.

cs.LO↗

arXiv2021

Correct Probabilistic Model Checking with Floating-Point Arithmetic

Probabilistic model checking computes probabilities and expected values related to designated behaviours of interest in Markov models. As a formal verification approach, it is applied to critical systems; thus we trust that probabilistic model checkers deliver correct results. To achieve scalability and performance, however, these tools use finite-precision floating-point numbers to represent and calculate probabilities and other values. As a consequence, their results are affected by rounding errors that may accumulate and interact in hard-to-predict ways. In this paper, we show how to implement fast and correct probabilistic model checking by exploiting the ability of current hardware to control the direction of rounding in floating-point calculations. We outline the complications in achieving correct rounding from higher-level programming languages, describe our implementation as part of the Modest Toolset's 'mcsta' model checker, and exemplify the tradeoffs between performance and correctness in an extensive experimental evaluation across different operating systems and CPU architectures.

cs.LO↗

arXiv2021

Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System

Modern network-on-chip (NoC) systems face reliability issues due to process and environmental variations. The power supply noise (PSN) in the power delivery network of a NoC plays a key role in determining reliability. PSN leads to voltage droop, which can cause timing errors in the NoC. This paper makes a novel contribution towards formally analyzing PSN in NoC systems. We present a probabilistic model checking approach to observe the PSN in a generic 2x2 mesh NoC with a uniform random traffic load. Key features of PSN are measured at the behavioral level. To tackle state explosion, we apply incremental abstraction techniques, including a novel probabilistic choice abstraction, based on observations of NoC behavior. The Modest Toolset is used for probabilistic modeling and verification. Results are obtained for several flit injection patterns to reveal their impacts on PSN. Our analysis finds an optimal flit pattern generation with zero probability of PSN events and suggests spreading flits rather than releasing them in consecutive cycles in order to minimize PSN.

cs.NI↗