21 citations · 53 across the 22 of their papers we have counts for
24 papers
Path Abstraction for Markov Reward Models
Arnd Hartmanns, Robert Modderman
Path abstraction originated as a technique for counterexample refinement in probabilistic model checking. Given a discrete-time Markov chain, it summarises the probabilities passin…
Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)
Pedro R. D'Argenio, Arnd Hartmanns, Annabell Petri
Stochastic automata (SA) are a formal stochastic continuous-time model based on countdown timers whose expiration times follow general probability distributions. SA are particularl…
UMB: A Unified Markov Binary Format for Probabilistic Model Checking (extended version)
Roman Andriushchenko, Arnd Hartmanns, Joshua Jeppson +5
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 s…
Probabilistic Verification for Modular Network-on-Chip Systems (extended version)
Nick Waddoups, Jonah Boe, Arnd Hartmanns +4
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 s…
Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling (extended version)
Pedro R. D'Argenio, Arnd Hartmanns, Patrick Wienhöft +1
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, an…
Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality (extended version)
Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer +2
Statistical model checking (SMC) randomly samples probabilistic models to approximate quantities of interest with statistical error guarantees. It is traditionally used to estimate…
DTMC Model Checking by Path Abstraction Revisited (extended version)
Arnd Hartmanns, Robert Modderman
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 computi…
Time-Sensitive Importance Splitting
Gabriel Dengler, Carlos E. Budde, Laura Carnevali +1
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 infor…
A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz +2
We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstra…
Digging for Decision Trees: A Case Study in Strategy Sampling and Learning
Carlos E. Budde, Pedro R. D'Argenio, Arnd Hartmanns
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 optimisat…
Sound Statistical Model Checking for Probabilities and Expected Rewards (extended version)
Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer +2
Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guaran…
Tools at the Frontiers of Quantitative Verification
Roman Andriushchenko, Alexander Bork, Carlos E. Budde +20
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 suppo…
Reproduction Report for SV-COMP 2023
Marcus Gerhold, Arnd Hartmanns
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 be…
A Practitioner's Guide to MDP Model Checking Algorithms
Arnd Hartmanns, Sebastian Junges, Tim Quatmann +1
Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) is key for the verification of systems that act under uncertainty. Popul…
Backwards Reachability for Probabilistic Timed Automata: A Replication Report
Arnd Hartmanns, Bram Kohlen
Backwards reachability is an efficient zone-based approach for model checking probabilistic timed automata w.r.t. PTCTL properties. Current implementations, however, are restricted…
An Overview of Modest Models and Tools for Real Stochastic Timed Systems
Arnd Hartmanns
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…
Correct Probabilistic Model Checking with Floating-Point Arithmetic
Arnd Hartmanns
Probabilistic model checking computes probabilities and expected values related to designated behaviours of interest in Markov models. As a formal verification approach, it is appl…
Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System
Riley Roberts, Benjamin Lewis, Arnd Hartmanns +4
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…
Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids
Thom S. Badings, Arnd Hartmanns, Nils Jansen +1
We study a smart grid with wind power and battery storage. Traditionally, day-ahead planning aims to balance demand and wind power, yet actual wind conditions often deviate from fo…
Symblicit Exploration and Elimination for Probabilistic Model Checking
Ernst Moritz Hahn, Arnd Hartmanns
Binary decision diagrams can compactly represent vast sets of states, mitigating the state space explosion problem in model checking. Probabilistic systems, however, require multi-…
Optimistic Value Iteration
Arnd Hartmanns, Benjamin Lucien Kaminski
Markov decision processes are widely used for planning and verification in settings that combine controllable or adversarial choices with probabilistic behaviour. The standard anal…
A Hierarchy of Scheduler Classes for Stochastic Automata
Pedro R. D'Argenio, Marcus Gerhold, Arnd Hartmanns +1
Stochastic automata are a formal compositional model for concurrent stochastic timed systems, with general distributions and non-deterministic choices. Measures of interest are def…
Efficient Algorithms for Time- and Cost-Bounded Probabilistic Model Checking
Ernst Moritz Hahn, Arnd Hartmanns
In the design of probabilistic timed systems, bounded requirements concerning behaviour that occurs within a given time, energy, or more generally cost budget are of central import…
Explicit Model Checking of Very Large MDP using Partitioning and Secondary Storage
Arnd Hartmanns, Holger Hermanns
The applicability of model checking is hindered by the state space explosion problem in combination with limited amounts of main memory. To extend its reach, the large available ca…