The probabilistic model checker Storm

International Journal on Software Tools for Technology Transfer, vol. 24, pp. 589–610

Abstract

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 probabilistic guarded command language. It has a modular setup 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.

Authors 5

1. Christian Hensel Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   RWTH Aachen University

2. Sebastian Junges

   University of California, Berkeley

   Affiliation as printed

   University of California, Berkeley, CA, USA

   University of California–Berkeley

3. Joost-Pieter Katoen corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   RWTH Aachen University

4. Tim Quatmann Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   RWTH Aachen University

5. Matthias Volk Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   RWTH Aachen University