PaperlayerView exact revision on arXiv

Source-linked AI summary

The Probabilistic Model Checker Storm

Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk

arXiv:2002.07080v2cs.SE

TL;DR

Probabilistic model checking needs adaptable tools for analyzing stochastic systems across diverse models and properties. This paper presents Storm, a modular checker with broad modeling and analysis support, and evaluates its configurations and comparative performance on QComp 2019. Storm is competitive with existing probabilistic model checkers, while its engines differ in versatility and some model-checking capabilities remain unsupported.

  • Problem

    Probabilistic model checking spans diverse models and properties, motivating a modular and adaptive tool rather than a one-size-fits-all solution.

  • Method

    The paper presents Storm’s modular architecture, modeling-language support, probabilistic model-checking methods, Python interface, and abstraction-based POMDP verification.

  • Results

    Storm was the strongest competitor in QComp 2019 default mode and clearly outperformed competitors in instance-specific mode, performing best on 1/3 and 1/2 of supported benchmarks, respectively.

  • Takeaways & Limitations

    Storm provides an effective and efficient platform for future-proof developments in probabilistic model checking.

  • Takeaways & Limitations

    Storm does not support statistical model checking, LTL model checking, probabilistic timed automata, stochastic games, or Prism’s hybrid engine.

Abstract

from arXiv · show

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.

1 Introduction

Probabilistic model checking addresses verification of systems with stochastic behavior, and Storm was developed as a modular, adaptive platform for this diverse field. The paper reports Storm’s features, usage, and QComp 2019 evaluation.

  • Probabilistic model checking extends model checking to systems involving random phenomena or behavior approximated by randomization.
  • Storm was developed as a modular and adaptive model checker because probabilistic model-checking tools and techniques depend heavily on models and properties.
  • In QComp 2019, Storm solved more benchmark instances and was generally faster on the instances it solved.
  • Storm supports multiple modeling languages and extended probabilistic model checking with parameter synthesis and multi-objective model checking.
  • The paper describes Storm’s main features, supported models and properties, building blocks, interfaces, architecture, and empirical evaluation on QComp 2019.

2 Storm in a Nutshell

Storm combines mature probabilistic model-checking algorithms with multiple representations, interchangeable solvers, broad input support, and interfaces for extending the tool. Its architecture also supports advanced analyses, while important functionality remains outside its scope.

  • Storm implements model-checking algorithms for discrete- and continuous-time Markov chains, Markov decision processes, and Markov automata.
  • Storm supports explicit-state, symbolic, and mixed model checking, with modular exchange of solvers and decision-diagram packages.
  • Storm extends standard probabilistic model checking with counterexample generation, permissive-scheduler synthesis, symbolic bisimulation minimization, and game-based abstraction.
  • Storm supports Prism and Jani, generalized stochastic Petri nets, dynamic fault trees, and conditioned probabilistic programs as native input formats.
  • Storm provides a Python API and library-based access for rapid prototyping and flexible construction of tools using its engines and algorithms.
  • Storm lacks support for statistical model checking, LTL model checking, probabilistic timed automata, stochastic games, and Prism’s hybrid engine.

3 Probabilistic Model Checking with Storm

Storm supports probabilistic model checking across multiple model types, modeling languages, properties, and analysis approaches. Its abstractions cover both probabilistic behavior and nondeterministic choices, including partially observable settings.

  • Model types: Storm analyzes discrete- and continuous-time probabilistic models with and without nondeterministic choices.The supported formalisms include DTMCs, CTMCs, MDPs, and MAs, with additional support for partially observable models.
  • Model types: DTMCs use a single probability distribution per state, whereas MDPs add nondeterministic actions selecting among distributions.Nondeterminism can represent scheduling, adversarial interaction, or underspecification.
  • Model types: CTMCs and MAs model continuous time through exponentially distributed sojourns or delays.MAs combine probabilistic states with nondeterministic choices and Markovian states where time elapses.
  • Modeling languages: Storm supports Prism, Jani, generalized stochastic Petri nets, dynamic fault trees, and probabilistic guarded-command programs.These languages target different modeling domains and can be translated or tailored for analysis within Storm.
  • Properties: Supported queries include reachability, temporal logic, conditional probability and cost, long-run averages, cost-bounded, and multi-objective properties.For nondeterministic models, analyses can quantify over all resolutions or seek a resolution satisfying a property.
  • Analysis approaches: Because no single approach suits every model and property, Storm offers interchangeable explicit and symbolic solving approaches.Users can select methods such as linear-system solving or value-iteration variants, while developers can extend and combine them.

4 Storm’s Features

Storm’s distinguishing features target scalability, accuracy, extensibility, and analysis beyond classical probabilistic model checking. Its modular architecture supports varied algorithms and model-specific techniques.

  • Scalability: Storm reduces model-checking size through cost-bounded methods, symbolic bisimulation minimization, and game-based abstraction.These techniques target scalability by reducing the analyzed model in different ways.
  • Extensions: Storm extends classical analysis with counterexample generation, permissive scheduler synthesis, multi-objective checking, parametric models, and specialized methods.The extensions cover strategies, unknown probabilities, POMDPs, and dynamic fault trees.
  • Modularity: Storm’s modular structure allows specialized methods to reuse regular model-checking and other analysis methods.Table 2 summarizes feature applicability across supported model types.
  • Accuracy: Exact arithmetic represents probabilities and costs as rationals, avoiding numerical representation errors for supported properties.Exact model checking is increasingly costly because number representations grow and approximative methods cannot be applied.
  • Accuracy: Sound numerical methods ensure correctness within user-defined accuracy with a small time penalty, apart from finite-precision implementation effects.The approach addresses limitations of standard value-iteration termination criteria.

4.2 Cost-bounded Reachability

Cost-bounded reachability asks whether a goal can be reached before resource bounds are exceeded. Storm keeps resource costs outside the state space and analyzes the smaller original model.

  • Motivation: Cost-bounded reachability analyzes goal-reaching behavior while respecting bounds on resources such as time or energy.It also covers questions about expected completion time or resource-limited success.
  • Method: Storm attaches non-negative action or state costs to models and evaluates them with cost-bounded queries.The costs are specified in the modeling language rather than encoded as additional state variables.
  • Method: Keeping resources out of the state space keeps the model much smaller while Storm performs a series of model-checking calls.The approach generalizes earlier ideas to multiple cost dimensions.
  • Relation to quantiles: Cost-bounded reachability is closely related to quantile properties, which fix a target probability and ask for the required resource investment.The two property types differ in whether the resource bound or desired probability is fixed first.

4.3 Symbolic Bisimulation Minimization

Storm combines symbolic representation with bisimulation minimization and extends it to nondeterministic models. Its game-based abstraction-refinement loop provides sound bounds while targeting very large or infinite models.

  • Symbolic representation: Decision diagrams exploit model structure and symmetry to represent very large probabilistic state spaces compactly.Storm uses symbolic representations such as MTBDDs and MDDs to address state-space explosion.
  • Bisimulation minimization: Bisimulation minimization merges states with equivalent behavior into a quotient model that preserves the original properties.The quotient can then be analyzed instead of the full model.
  • Storm’s extension: Storm combines symbolic representation with bisimulation minimization for all four supported model types, including nondeterministic models.The resulting quotient is often small enough for explicit representation and efficient analysis.
  • Limitations: Bisimulation may produce overly fine quotients and requires the entire state space and transitions, preventing it from handling some very large or infinite models.These drawbacks motivate analysis-guided abstraction.
  • Game-based abstraction: Game-based abstraction merges states more aggressively, over-approximates behavior, and yields sound bounds for the original model’s measures.The abstraction introduces nondeterminism to represent the over-approximation.
  • Abstraction-refinement loop: Storm refines the abstraction by splitting state partitions until the game-analysis bounds are precise enough to return.The abstract game is initially derived from the property-induced partition and can be extracted directly from high-level models.

4.5 Multi-Objective Model Checking

Storm extends multi-objective model checking beyond independently optimized strategies by supporting combined constraints and broader model classes. It uses preprocessing followed by linear programming or iterative standard techniques, with additional efficient preprocessing.

  • Motivation: Optimal MDP strategies resolve nondeterminism so that the induced behavior satisfies a specified property.
  • Motivation: Independent optimization can produce strategies that satisfy one resource bound while violating another combined time-and-energy property.The same issue arises because independently computed strategies may waste the resource optimized by the other strategy.
  • Approach: State-of-the-art multi-objective checking preprocesses the model before solving a linear program or iteratively applying standard model-checking techniques.
  • Storm support: Storm supports multi-objective model checking on MDPs and MAs under general and more restricted strategies.
  • Storm support: Storm combines flexible properties, including multiple cost bounds, with particularly efficient preprocessing steps.

4.6 Synthesis of High-Level Counterexamples

Storm synthesizes high-level counterexamples to explain violated safety properties and supports parameter synthesis for uncertain probabilistic models. Its parameter-synthesis methods trade explicit rational-function computation against abstraction or monotonicity analysis.

  • High-Level Counterexamples: Counterexamples help locate the part of a system that leads to a bad state reached above a probability threshold.
  • High-Level Counterexamples: Storm computes the smallest Jani or Prism submodel that already witnesses a violated safety property.It searches candidate submodels through guided exploration.
  • Parametric Model Checking: Parametric Markov models represent transition probabilities as symbolic expressions to capture uncertainty in data-based or configurable probabilities.
  • Parametric Model Checking: Storm offers parameter synthesis by state elimination, parameter lifting with sound abstraction, and monotonicity analysis without computing the solution function.The state-elimination method uses heuristics and rational-function representations for faster operations.
  • Partially Observable MDPs: Storm provides three methods for POMDP analysis.
  • Partially Observable MDPs: Storm supports quantitative reachability verification in POMDPs by iteratively constructing finite abstract belief MDPs through abstraction and refinement.The abstraction soundly approximates extremal reachability probabilities.

4.9 Model Checking Dynamic Fault Trees

Storm analyzes dynamic fault trees by translating them into tailored Markov models and applying model checking to reliability, failure-time, and more complex measures. Its dedicated translation exploits fault-tree structure and symmetries to reduce analysis effort.

  • Dynamic Fault Trees: Dynamic fault trees model order-dependent failures, functional dependencies, and spare management through dynamic gates.
  • Analysis: Storm supports reliability, mean-time-to-failure, and degraded-mode queries on Markov models corresponding to dynamic fault trees.
  • Analysis: Storm provides these dynamic-fault-tree queries out of the box, including support for parametric DFTs through its modular architecture.
  • Translation: A dedicated translation uses DFT structure to construct Markov models containing only relevant behavior.
  • Translation: Symmetries in fault trees are exploited to further collapse the translated model before regular model checking.
  • Related POMDP Capability: Storm can compute small-memory and more general policies for hard POMDP reachability problems using SAT encodings and an incremental procedure.

5 Using Storm

Storm can be used through command-line, library, and Python interfaces with models specified in languages such as Jani and Prism. Users can configure analysis engines and solvers, while Docker containers provide a quicker experimental setup at somewhat reduced performance.

  • Overview: Storm is free and open software with documentation available on its website.
  • Installation: Building Storm requires configuration and compilation on the target machine, including dependency handling.
  • Installation: Docker containers let users start experimenting immediately with Storm, at the cost of slightly reduced performance.
  • Model descriptions: Storm accepts multiple input languages, including Jani and Prism.
  • Command Line: The command-line interface specifies the input model and properties, then reports the requested model-checking results.
  • Command Line: Users can configure Storm's analysis engine and linear-equation solver, including hybrid engines and state elimination.
  • Library Interface: Storm can be used as a C++ library for flexible access to internal data structures, but this requires the most effort.
  • Python API: The Stormpy Python API offers quicker flexible access to core functionality, though Python may introduce runtime overhead.Stormpy is also used by larger projects such as the parameter-synthesis tool PROPhESY.

6 Architecture

Storm’s architecture separates model representations, engines, solvers, and interfaces so users can select implementations for different models and verification tasks. The design emphasizes modularity, broad feature support, and exchangeable high-performance components.

  • Architecture: Storm organizes its code into libraries and executables, with core functionality covering matrices, models, expressions, modeling languages, model-checking engines, and solvers.The storm library contains the central data structures and model-checking functionality.
  • Representations: Storm supports sparse matrices and MTBDDs, enabling explicit storage for irregular small-to-moderate models and symbolic storage for models described compactly.Sparse memory use is roughly proportional to nonzero-probability transitions, while MTBDDs are built directly from model descriptions.
  • Model-checking engines: Its engines trade off representation and translation: sparse handles broad functionality, while hybrid and dd-to-sparse engines convert relevant or reusable portions into sparse form.The hybrid engine translates property-relevant parts; dd-to-sparse translates independently of the property for repeated checking or symbolic bisimulation.
  • Model-checking engines: Engine support is uneven: the sparse engine covers all Storm queries and major model classes, whereas other engines have restrictions on time, queries, or model features.Exact arithmetic excludes time-bounded CTMC and MA properties, and several advanced features are implemented only in the sparse engine.
  • Solvers: Storm’s solver interfaces decouple verification tasks from implementations, allowing backend selection, library reuse, licensing flexibility, and simpler addition of new solver functionality.The architecture supports multiple implementations for interfaces such as sparse linear-equation solving.
  • Technicalities: C++ provides fast solver interfacing but advanced templating can be difficult to understand and can substantially increase compilation times.This is the principal trade-off identified for Storm’s implementation language.

7 Evaluation

Storm was evaluated across 96 QComp benchmark instances using seven configurations and resource-bounded correctness checks. The results show complementary strengths: sparse was most versatile, while automatic and symbolic configurations improved performance on many instances.

  • Evaluation setup: 96 benchmark instances were evaluated under 30-minute and 12-GB time and memory limits, with results checked against QVBS references.Four instances were excluded because PTA translation or output support failed.
  • Evaluation setup: Seven configurations covered Storm’s sparse, hybrid, dd, symbolic-bisimulation, sound, exact, and automatic engines.Experiments used Storm 1.6.2 and measured wall-clock runtime including model building and model checking.
  • Overall results: 87 instances were solved with 0 incorrect results by the notional fastest configuration.This configuration combines the best result from the seven tested configurations by running them in parallel.
  • Engine comparison: 73 instances were solved by the sparse engine, which supported all 96 instances and outperformed the hybrid and dd engines in the evaluation.The sparse engine was the most versatile, although the other engines remained competitive and solved some instances symbolically.
  • Evaluation caveats: Benchmark selection strongly affects engine comparisons because symbolic engines rely on model structure and many benchmarks are unsupported by hybrid or dd.Unsupported experiments and other non-solved outcomes can skew quantile-plot lines.
  • Accuracy and performance: Sound model checking often added negligible overhead, whereas exact model checking was comparably costly but superior on a few difficult instances.Exact arithmetic can enlarge number representations and prevents use of approximative numerical solution methods.
  • Engine comparison: The automatic engine often improved sparse-engine runtime and nearly matched the notional fastest configuration.Several instances could only be solved using symbolic techniques based on the hybrid or dd engine.

8 Conclusion

The paper presents Storm as a state-of-the-art probabilistic model checker designed for extensibility and rapid prototyping. Its modularity, Python interface, broad modeling support, and performance make it a competitive platform for future developments.

  • Storm combines modularity, a Python interface, multiple modeling formalisms, and functionality beyond standard probabilistic model-checking algorithms.
  • Storm is competitive with existing probabilistic model checkers and provides an effective, efficient platform for future-proof developments.The tool is open access and publicly available.
  • Maintaining Storm requires continued implementation of new algorithms and revision of existing code as the field progresses.
Loading 2002.07080v2…