# A storm is Coming: A Modern Probabilistic Model Checker

arXiv: https://arxiv.org/abs/1702.04311 · HTML: https://mlsanity.com/paper/1702.04311/

## Key facts

- Cited by 34 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Feb 2017.

## Built on by (most cited first, 30 of 34)

- [Online Shielding for Reinforcement Learning](https://mlsanity.com/paper/2212.01861/) (2022)
- [COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking](https://mlsanity.com/paper/2209.07133/) (2022)
- [dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts](https://mlsanity.com/paper/2101.07202/) (2021)
- [Convex Optimization for Parameter Synthesis in MDPs](https://mlsanity.com/paper/2107.00108/) (2021)
- [Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems](https://mlsanity.com/paper/2606.17182/) (2026)
- [Bayesian Learning for the Robust Verification of Autonomous Robots](https://mlsanity.com/paper/2303.08476/) (2023)
- [Algebraically Explainable Controllers: Decision Trees and Support Vector Machines Join Forces](https://mlsanity.com/paper/2208.12804/) (2022)
- [PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP](https://mlsanity.com/paper/2206.01465/) (2022)
- [Fine-Tuning the Odds in Bayesian Networks](https://mlsanity.com/paper/2105.14371/) (2021)
- [Dependability Analysis of Deep Reinforcement Learning based Robotics and Autonomous Systems through Probabilistic Model Checking](https://mlsanity.com/paper/2109.06523/) (2021)
- [Data-driven abstractions via adaptive refinements and a Kantorovich metric [extended version]](https://mlsanity.com/paper/2303.17618/) (2023)
- [Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives](https://mlsanity.com/paper/2304.09930/) (2023)
- [Inductive Synthesis for Probabilistic Programs Reaches New Horizons](https://mlsanity.com/paper/2101.12683/) (2021)
- [Lifted Model Checking for Relational MDPs](https://mlsanity.com/paper/2106.11735/) (2021)
- [Active Learning of Markov Decision Processes using Baum-Welch algorithm (Extended)](https://mlsanity.com/paper/2110.03014/) (2021)
- [TriCEGAR: A Trace-Driven Abstraction Mechanism for Agentic AI](https://mlsanity.com/paper/2601.22997/) (2026)
- [Measuring the Unmeasurable: Markov Chain Reliability for LLM Agents](https://mlsanity.com/paper/2604.24579/) (2026)
- [Robust Probabilistic Shielding for Safe Offline Reinforcement Learning](https://mlsanity.com/paper/2605.10293/) (2026)
- [An Abstraction-based Method to Check Multi-Agent Deep Reinforcement-Learning Behaviors](https://mlsanity.com/paper/2102.01434/) (2021)
- [SOCKS: A Stochastic Optimal Control and Reachability Toolbox Using Kernel Methods](https://mlsanity.com/paper/2203.06290/) (2022)
- [Formally Verified Approximate Policy Iteration](https://mlsanity.com/paper/2406.07340/) (2024)
- [Explaining Control Policies through Predicate Decision Diagrams](https://mlsanity.com/paper/2503.06420/) (2025)
- [Are Agents Probabilistic Automata? A Trace-Based, Memory-Constrained Theory of Agentic AI](https://mlsanity.com/paper/2510.23487/) (2025)
- [Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems](https://mlsanity.com/paper/2110.02125/) (2021)
- [Bayesian Statistical Model Checking for Multi-agent Systems using HyperPCTL*](https://mlsanity.com/paper/2209.02672/) (2022)
- [MM Algorithms to Estimate Parameters in Continuous-time Markov Chains](https://mlsanity.com/paper/2302.08588/) (2023)
- [Probabilistic ML Verification via Weighted Model Integration](https://mlsanity.com/paper/2402.04892/) (2024)
- [Analyzing Value Functions of States in Parametric Markov Chains](https://mlsanity.com/paper/2504.17020/) (2025)
- [Verification-Guided Falsification for Safe RL via Explainable Abstraction and Risk-Aware Exploration](https://mlsanity.com/paper/2506.03469/) (2025)
- [BayesL: a Logical Framework for the Verification of Bayesian Networks](https://mlsanity.com/paper/2506.23773/) (2025)

## Abstract (arXiv)

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.