Storm

Engines

Table of contents

As with so many things, there is no one-size-fits-all in probabilistic model checking. Generally, it depends on the characteristics of the input model, which of the model checking approaches works best (for example in terms of time or memory requirements). Therefore, established model checkers provide a range of different engines that pursue different approaches to solve the same problem. In practice, the functionality of the engines is typically incomparable, that is there may be features that an engine can solve that another one cannot and vice versa. In the following, we give a brief intuitive overview on the engines provided by Storm. We also indicate how to select them, in which cases certain engines are well-suited and which major restrictions exist.

Sparse

Storm’s main engine is the sparse engine in the sense that it tends to have the most features. It takes the model description and directly builds a representation based on explicit data structures, mainly bit vectors and sparse matrices. Then, model checking is performed using these data structures. Since these permit easy access to single elements, they are standard representations for many tasks involved in the solution procedure (like solving linear equations). This enables the use of off-the-shelf libraries, for instance Eigen or gmm++, that implement sophisticated solution methods.

Select: --engine sparse or -e sparse

Characteristics:

Advisable if:

Major restrictions:

DD

Binary decision diagrams (BDDs) are a data structure to represent switching functions. They have proven to enable the verification of gigantic hardware circuits. Multi-terminal BDDs (MTBDDs) extend BDDs to allow representing functions that map to numbers rather than just true or false. The dd engine builds a representation of the model in terms of BDDs (state sets) and MTBDDs (matrices, vectors), which is often referred to as a symbolic representation (rather than an explicit representation as in the sparse engine). As MTBDDs support certain arithmetical operations, they are also used in the quantitative model checking step. However, DDs do not allow for (efficient) random access, which limits the numerical solution techniques that are applicable.

Select: --engine dd or -e dd

Characteristics:

Advisable if:

Major restrictions:

Hybrid

The hybrid engine tries to combine the sparse and dd engines. It first builds a DD-based representation of the system. Then, however, the model checking is performed in a hybrid manner. That is, operations that are deemed to be more efficient on DDs (qualitative computations) are carried out in this realm, while the heavy numerical computations are performed on an explicit representation derived from the systems’ DDs.

Select: --engine hybrid or -e hybrid

Characteristics:

Advisable if:

Exploration

All engines so far have the requirement that a representation of the model needs to be built prior to model checking. This can be prohibitive for some models and may be unnecessary as fragments of the model may already allow for an answer (within a given precision) to a query. The exploration engine is based on the ideas of applying techniques from machine learning [1]. Intuitively, it tries to explore the parts of the system on-the-fly that contribute most to the model checking result.

Select: --engine expl or -e expl

Advisable if:

Major restrictions:

Abstraction-Refinement

All other engines are not suited for models with an infinite state space. The approach of the abstraction-refinement engine is to start with a coarse over-approximation of the concrete model. This abstract model is then analyzed. Based on the result, one of two things happen: either the result carries over to the concrete model and and an answer can be returned or the abstraction needs to be refined. In the latter case, the abstraction is analyzed again and the loop is repeated until a conclusive answer can be given.

This engine relies heavily on SMT solving (more concretely an enumeration of all satisfying assignments of a formula) and Craig interpolation. Therefore, this engine needs MathSAT and Storm has to be built with MathSAT support, which requires a manual setup.

Select: --engine abs or -e abs

Advisable if:

Major restrictions:

References