# A storm is Coming: A Modern Probabilistic Model Checker

## TL;DR

This paper introduces Storm, a versatile probabilistic model checker supporting various models and languages, with a modular architecture and Python API, demonstrating competitive performance through extensive benchmarks.

## Contribution

It presents Storm, a new probabilistic model checker with broad model support, modular design, and a Python API, enhancing flexibility and usability over existing tools.

## Key findings

- Supports multiple probabilistic models and languages.
- Offers a modular architecture with interchangeable solvers.
- Demonstrates competitive performance on benchmarks.

## Abstract

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.

---
Source: https://tomesphere.com/paper/1702.04311