Source-linked AI summary
A storm is Coming: A Modern Probabilistic Model Checker
Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk
TL;DR
Probabilistic model checking needs a flexible platform spanning diverse models, formalisms, algorithms, and computational backends. Storm addresses this with broad model and language support, modular engines and solvers, and APIs for prototyping. Across benchmark comparisons, Storm is competitive and mostly outperforms Prism, while several Prism capabilities remain outside its scope.
Problem
Existing open-source probabilistic model checkers are often insufficiently flexible and modular for experimenting with new algorithms, models, formalisms, and features.
Method
Storm provides a probabilistic model checker combining diverse model and input-language support with interchangeable explicit, symbolic, hybrid, solver, and API components.
Results
Storm is mostly better than Prism in verification speed and memory footprint on the Prism benchmark suite, and is significantly faster than IMCA on most Markov-automata instances.
Takeaways & Limitations
Storm offers one platform for analyzing diverse probabilistic models and experimenting with alternative engines, solvers, and verification algorithms.
Takeaways & Limitations
Storm does not support LTL model checking, probabilistic timed automata, multi-objective model checking, statistical model checking, or stochastic-game analysis.
Abstract
from arXiv · showhide
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.
1 Introduction
Storm is an open probabilistic model-checking toolkit designed for extensibility, supporting diverse models, input formalisms, analysis modes, and interfaces. Its benchmark performance is mostly better than Prism, while several Prism capabilities remain unsupported.
- Motivation: Storm provides a modular, extensible platform for experimenting with verification algorithms, probabilistic models, modeling formalisms, and features.Its toolkit contains about 100,000 lines of C++ code and exposes mature components through simple interfaces.
- Modeling support: Storm supports native inputs including the Prism format, generalized stochastic Petri nets, dynamic fault trees, and conditioned probabilistic programs.State-space generation, reduction, and analysis algorithms are partly tailored to these formalisms.
- Modeling support: Storm analyzes discrete- and continuous-time Markov chains, MDPs, and Markov automata, with rewards on states and actions.Markov automata provide a compositional variant of continuous-time MDPs.
- Architecture: Storm supports explicit, fully symbolic BDD-based, and hybrid model checking, with exchangeable solvers and decision-diagram packages.The current release supports about 15 solvers, including CUDD and multi-threaded Sylvan.
- Interfaces: Storm provides a Python API for rapid prototyping using its engines and algorithms.The API encapsulates Storm’s high-performance implementations.
- Evaluation: Storm is mostly better than Prism in verification speed and memory footprint on the Prism benchmark suite.The introduction reports this as a broad performance comparison rather than a single benchmark result.
- Limitations: Storm does not support LTL model checking, probabilistic timed automata, multi-objective model checking, statistical model checking, or stochastic-game analysis.It also lacks Prism’s equivalent hybrid engine and a fully symbolic engine for continuous-time models.
2 Features
Storm combines broad model and language support with multiple symbolic and explicit engines, specialized analyses, counterexample generation, exact arithmetic, and several APIs. These features support both extensible experimentation and practical verification workflows.
- Model types: Storm supports DTMCs, CTMCs, MDPs, and Markov automata, including reward extensions for states and actions.The four model types combine discrete or continuous time with Markovian or nondeterministic behavior.
- Modeling languages: Storm accepts Prism, JANI, generalized stochastic Petri net, and dynamic fault-tree inputs, as well as conditioned probabilistic programs.GSPNs can be handled through a dedicated model builder or encoded in JANI.
- Modeling languages: Storm supports generalized stochastic Petri nets without the confusion-free restriction imposed by existing CSL model checkers for GSPNs.This follows from Storm’s support for Markov automata.
- Analyses: Storm supports reward, conditional-probability, conditional-reward, parametric, exact-arithmetic, and counterexample analyses.Its counterexample capabilities include MILP-based and MaxSat-based high-level generation for Prism models.
- Engines: Storm offers sparse-matrix and MTBDD representations, with engines tailored to different input models and analysis strategies.Sparse matrices target small and moderately sized models, while MTBDDs represent gigantic models with more expensive operations.
- APIs: Storm exposes command-line, C++, and Python APIs for end-user access, performance tuning, fine-grained development, and rapid prototyping.The Python API encapsulates high-performance implementations.
3 Architecture
Storm uses an architecture that separates input handling, model construction, engines, and solver functionality. This modularity supports different input formats and interchangeable high-performance solver backends.
- Architecture: After parsing, Storm conditionally builds a full in-memory model depending on the selected engine and input format.The exploration and abstraction-refinement engines can avoid upfront full model construction.
- Solvers: Storm’s solver infrastructure provides interfaces for linear and Bellman equations, MILP, and SMT using sparse matrices or MTBDDs.These interfaces expose common probabilistic model-checking tasks through dedicated solver backends.
- Solvers: Solver interfaces permit choosing task-specific backends, enabling performance tuning, license-aware configuration, and easier implementation of new solver functionality.Backend performance can vary substantially for the same input.
- Solvers: Table 1 presents the solvers offered by Storm.
4 Evaluation
The evaluation compares Storm and Prism on matched engines and selected best engines across benchmark tasks. Storm is generally competitive or faster, while Prism retains an advantage on large CTMC benchmarks.
- Methodology: Storm and Prism are compared on 24 DTMC, CTMC, and MDP models covering 82 corresponding properties.
- Methodology: The comparison matches engines by general approach, including sparse representations and corresponding model-checking workflows.
- Results: The runtime plots compare total Storm-engine time with matching Prism-engine time; points above the diagonal indicate faster Storm runs.Dashed lines mark speed-ups of 10 and 100, while OoR, Err, and NR identify non-completed or unavailable results.
- Results: Storm’s best engine solves 361 of 380 tasks, compared with 346 tasks solved by Prism.Storm is faster for the overwhelming majority of verification tasks, although Prism tends to be faster on large CTMC benchmarks.
- Results: Storm outperforms Prism by up to three orders of magnitude in exact arithmetic, and is significantly faster than IMCA on most Markov-automata instances.
A.1 Remarks
The appendix clarifies how unsupported or failed tasks are represented and identifies memory consumption as an important but difficult-to-compare evaluation dimension.
- Errors and unsupported tasks: Errors and unsupported tasks are both marked Err because neither outcome provides an answer from the user’s perspective.
- Errors and unsupported tasks: When no engine solves a task, best-runtime plots label the instance NR because Err and OoR have no natural ordering.
- Memory consumption: The experiments compare runtimes only, while memory consumption remains difficult to assess across Java and C++ tools.Java virtual machines may retain allocated memory, and virtual-memory measurements may not reflect actual consumption.
A.2 iscasMC vs. Storm
The appendix compares Storm with Epmc, the upcoming successor to iscasMC, using matching engines on the Prism benchmark suite. Epmc lacks support for some objectives, producing many Err results.
- A.2 iscasMC vs. Storm: Epmc is an upcoming iscasMC successor with major refactorings, and its performance is compared with Storm on the Prism benchmark suite.
- A.2 iscasMC vs. Storm: The comparison uses matching engines to evaluate the performance of Epmc and Storm.
A.3 Accumulated time plots (Prism vs. Storm vs. Epmc)
The accumulated-time plots summarize the fastest engine’s performance for each instance. Each point records how many fastest instances were solved and their accumulated time.
- Each instance contributes the running time of its fastest engine.The comparison includes Prism, Epmc, and Storm, as identified in Figure 4.
- Figure 4 presents the Prism, Epmc, and Storm comparison using the best engine for each instance.
A.4 Prism’s “hybrid” engine
Storm omits an engine comparable to Prism’s hybrid engine because the authors prioritize runtime and report Prism’s sparse engine as faster than its hybrid engine.
- Storm does not currently feature an engine comparable to Prism’s hybrid engine.
- Prism’s hybrid engine is a crossover between its sparse and mtbdd engines.
- Because the comparison focuses on runtime, the authors find little motivation to include a Storm engine analogous to Prism’s hybrid engine.Figure 5 is cited as showing Prism’s hybrid engine dominated by Prism’s sparse engine in runtime.
A.5 MTBDD-based CTMC model checking
Storm does not provide fully symbolic MTBDD-based CTMC model checking. The authors justify this design choice by emphasizing runtime, while acknowledging possible memory advantages of MTBDDs.
- Storm currently lacks fully symbolic MTBDD-based CTMC model checking.
- For CTMCs, Prism’s sparse engine typically outperforms its MTBDD-based engine in runtime.
- The authors prioritize runtime despite acknowledging that the MTBDD engine may consume less memory.