A storm is Coming: A Modern Probabilistic Model Checker

2017/02/14 by Christian Dehnert, Dehnert, Christian, Sebastian Junges +5 · 6 citations
Business, Management and Accounting · Computer Science · #Advanced Software Engineering Methodologies #Business Process Modeling and Analysis #FOS: Computer and information sciences #Software Engineering (cs.SE) #Software System Performance and Reliability

paper · pdf · doi:10.48550/arxiv.1702.04311

openalex publication_date 2017/02/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01

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.

Cited by

• Automated Formalization of Probabilistic Requirements from Structured Natural Language
• Are Agents Just Automata? On the Formal Equivalence Between Agentic AI and the Chomsky Hierarchy
• Sound Value Iteration for Simple Stochastic Games
• Data-Driven Abstraction and Synthesis for Stochastic Systems with Unknown Dynamics
• Probabilistic Alternating Simulations for Policy Synthesis in Uncertain Stochastic Dynamical Systems
• Model-based stochastic analysis with probabilistic graph query evaluation

Related

• The Probabilistic Model Checker Storm
• The Probabilistic Model Checker Storm (Extended Abstract)
• Probabilistic Model Checking: Applications and Trends
• Bayesian Inference by Symbolic Model Checking
• DynamicPPL: Stan-like Speed for Dynamic Probabilistic Models