A storm is Coming: A Modern Probabilistic Model Checker
This tool provides a modular and efficient solution for analyzing probabilistic models, which is incremental as it builds on existing model checking concepts.
The authors introduced Storm, a new probabilistic model checker that supports various modeling languages and systems, and demonstrated its competitive performance on multiple benchmarks.
We launch the new probabilistic model checker storm. It features the analysis of discrete- and continuous-time variants of both Markov chains and MDPs. It supports the PRISM and JANI modeling languages, probabilistic programs, dynamic fault trees and generalized stochastic Petri nets. It has a modular set-up in which solvers and symbolic engines can easily be exchanged. It offers a Python API for rapid prototyping by encapsulating storm's fast and scalable algorithms. Experiments on a variety of benchmarks show its competitive performance.