The probabilistic model checker Storm

Christian Hensel; Sebastian Junges; Joost Pieter Katoen; Tim Quatmann; Matthias Volk

doi:10.1007/s10009-021-00633-z

The probabilistic model checker Storm

Christian Hensel
, Sebastian Junges
, Joost Pieter Katoen^*
, Tim Quatmann
, Matthias Volk

^*Corresponding author for this work

Research output: Contribution to journal › Article › Academic › peer-review

226 Citations (Scopus)

62 Downloads (Pure)

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.

Original language	English
Pages (from-to)	589-610
Number of pages	22
Journal	International journal on software tools for technology transfer
Volume	24
Issue number	4
Early online date	6 Jul 2021
DOIs	https://doi.org/10.1007/s10009-021-00633-z
Publication status	Published - Aug 2022
Externally published	Yes

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 9 Industry, Innovation, and Infrastructure

Keywords

Markov chain
Markov decision process
Model checking
Probilistic systems
Verification

Access to Document

10.1007/s10009-021-00633-zLicence: CC BY

s10009-021-00633-zFinal published version, 1.55 MBLicence: CC BY

Cite this

@article{d60b5558cb6f4b6b806f25da1c587381,

title = "The probabilistic model checker Storm",

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{\textquoteright}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.",

keywords = "Markov chain, Markov decision process, Model checking, Probilistic systems, Verification",

author = "Christian Hensel and Sebastian Junges and Katoen, \{Joost Pieter\} and Tim Quatmann and Matthias Volk",

note = "Funding Information: This work has been supported by the ERC Advanced Grant 787914 (FRAPPANT) and the DFG RTG 2236 {\textquotedblleft}UnRAVeL.{\textquotedblright} S. Junges would like to acknowledge funding from NSF grants 1545126 (VeHICaL) and 1646208, the DARPA Assured Autonomy program, Berkeley Deep Drive, and by Toyota under the iCyPhy center. Publisher Copyright: {\textcopyright} 2021, The Author(s).",

year = "2022",

month = aug,

doi = "10.1007/s10009-021-00633-z",

language = "English",

volume = "24",

pages = "589--610",

journal = "International journal on software tools for technology transfer",

issn = "1433-2779",

publisher = "Springer",

number = "4",

}

TY - JOUR

T1 - The probabilistic model checker Storm

AU - Hensel, Christian

AU - Junges, Sebastian

AU - Katoen, Joost Pieter

AU - Quatmann, Tim

AU - Volk, Matthias

N1 - Funding Information: This work has been supported by the ERC Advanced Grant 787914 (FRAPPANT) and the DFG RTG 2236 “UnRAVeL.” S. Junges would like to acknowledge funding from NSF grants 1545126 (VeHICaL) and 1646208, the DARPA Assured Autonomy program, Berkeley Deep Drive, and by Toyota under the iCyPhy center. Publisher Copyright: © 2021, The Author(s).

PY - 2022/8

Y1 - 2022/8

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

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

KW - Markov chain

KW - Markov decision process

KW - Model checking

KW - Probilistic systems

KW - Verification

UR - https://www.scopus.com/pages/publications/85108257399

U2 - 10.1007/s10009-021-00633-z

DO - 10.1007/s10009-021-00633-z

M3 - Article

AN - SCOPUS:85108257399

SN - 1433-2779

VL - 24

SP - 589

EP - 610

JO - International journal on software tools for technology transfer

JF - International journal on software tools for technology transfer

IS - 4

ER -

The probabilistic model checker Storm

Abstract

UN SDGs

Keywords

Access to Document

Other files and links

Fingerprint

Cite this