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 - http://www.scopus.com/inward/record.url?scp=85108257399&partnerID=8YFLogxK
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 -
