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 …

Abstract Model checking undiscounted reachability and expected-reward properties on
Markov decision processes (MDPs) is key for the verification of systems that act under …

Markov decision processes are widely used for planning and verification in settings that
combine controllable or adversarial choices with probabilistic behaviour. The standard …

Quantitative formal models capture probabilistic behaviour, real-time aspects, or general
continuous dynamics. A number of tools support their automatic analysis with respect to …

Statistical model checking (SMC) is a technique for analysis of probabilistic systems that
may be (partially) unknown. We present an SMC algorithm for (unbounded) reachability …

Neural networks (NN) are taking over ever more decisions thus far taken by humans, even
though verifiable system-level guarantees are far out of reach. Neither is the verification …

Quantitative verification tools compute probabilities, expected rewards, or steady-state
values for formal models of stochastic and timed systems. Exact results often cannot be …

We employ uncertain parametric CTMCs with parametric transition rates and a prior on the
parameter values. The prior encodes uncertainty about the actual transition rates, while the …

This paper presents COOL-MC, a tool that integrates state-of-the-art reinforcement learning
(RL) and model checking. Specifically, the tool builds upon the OpenAI gym and the …

Statistical model checking avoids the state space explosion problem in verification and
naturally supports complex non-Markovian formalisms. Yet as a simulation-based approach …