# The Probabilistic Model Checker Storm

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

## Key facts

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

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

- [Safe Reinforcement Learning via Shielding under Partial Observability](https://mlsanity.com/paper/2204.00755/) (2022)
- [Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study](https://mlsanity.com/paper/2302.04634/) (2023)
- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning](https://mlsanity.com/paper/2209.10341/) (2022)
- [Solving Long-run Average Reward Robust MDPs via Stochastic Games](https://mlsanity.com/paper/2312.13912/) (2023)
- [We'll Fix it in Post: Improving Text-to-Video Generation with Neuro-Symbolic Feedback](https://mlsanity.com/paper/2504.17180/) (2025)
- [Distillation of RL Policies with Formal Guarantees via Variational Abstraction of Markov Decision Processes (Technical Report)](https://mlsanity.com/paper/2112.09655/) (2021)
- [Safety-Oriented Pruning and Interpretation of Reinforcement Learning Policies](https://mlsanity.com/paper/2409.10218/) (2024)
- [Neuro-Symbolic Evaluation of Text-to-Video Models using Formal Verification](https://mlsanity.com/paper/2411.16718/) (2024)
- [NeuS-QA: Grounding Long-Form Video Understanding in Temporal Logic and Neuro-Symbolic Reasoning](https://mlsanity.com/paper/2509.18041/) (2025)
- [Pessimistic Iterative Planning with RNNs for Robust POMDPs](https://mlsanity.com/paper/2408.08770/) (2024)
- [Abstraction-Refinement for Hierarchical Probabilistic Models](https://mlsanity.com/paper/2206.02653/) (2022)
- [Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems](https://mlsanity.com/paper/2404.01769/) (2024)
- [Enhancing RL Safety with Counterfactual LLM Reasoning](https://mlsanity.com/paper/2409.10188/) (2024)
- [Under-Approximating Expected Total Rewards in POMDPs](https://mlsanity.com/paper/2201.08772/) (2022)
- [Discrete-Event Controller Synthesis for Autonomous Systems with Deep-Learning Perception Components](https://mlsanity.com/paper/2202.03360/) (2022)
- [Targeted Adversarial Attacks on Deep Reinforcement Learning Policies via Model Checking](https://mlsanity.com/paper/2212.05337/) (2022)
- [Probabilistic Model Checking of Stochastic Reinforcement Learning Policies](https://mlsanity.com/paper/2403.18725/) (2024)
- [1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization](https://mlsanity.com/paper/2410.18293/) (2024)
- [Learning Explainable and Better Performing Representations of POMDP Strategies](https://mlsanity.com/paper/2401.07656/) (2024)
- [Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games](https://mlsanity.com/paper/2405.03885/) (2024)
- [Leaving Goals on the Pitch: Evaluating Decision Making in Soccer](https://mlsanity.com/paper/2104.03252/) (2021)
- [Turn-based Multi-Agent Reinforcement Learning Model Checking](https://mlsanity.com/paper/2501.03187/) (2025)
- [Scenario-based Compositional Verification of Autonomous Systems with Neural Perception](https://mlsanity.com/paper/2504.20942/) (2025)
- [Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC](https://mlsanity.com/paper/2602.14505/) (2026)
- [Task-Guided Inverse Reinforcement Learning Under Partial Information](https://mlsanity.com/paper/2105.14073/) (2021)
- [Efficient Sensitivity Analysis for Parametric Robust Markov Chains](https://mlsanity.com/paper/2305.01473/) (2023)
- [Graph-Based Reductions for Parametric and Weighted MDPs](https://mlsanity.com/paper/2305.05739/) (2023)
- [Analyzing Intentional Behavior in Autonomous Agents under Uncertainty](https://mlsanity.com/paper/2307.01532/) (2023)
- [Learning-Based Approaches to Predictive Monitoring with Conformal Statistical Guarantees](https://mlsanity.com/paper/2312.01959/) (2023)

## Abstract (arXiv)

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 set-up 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.