Storm

Properties

Table of contents

Storm takes properties in a format that can be described as an “extended subset” of the PRISM property language. Alternatively, if the input is given in terms of a JANI model, the properties are embedded in the model in the appropriate format.

For DFTs, GSPNs and probabilistic programs, domain-specific properties can be given. For this, we refer to the guide on how to run Storm on those inputs.

Identifying States

Storm allows to identify sets of states by either labels or via the symbolic variables describing the model. Note that it depends on the input language which of these two ways are enabled. For example, for explicit models, there are no symbolic variables and therefore only labels can be used. For PRISM and JANI input, both labels and expressions over model variables are valid. Finally, the expression true can be used to describe the set of all states.

Labels

To refer to a label a model exports, put the name of the label in quotes. For example, if a model has the label done to express that in these states the model is done with something, write "done" to refer to these states.

Propositional Expressions

For symbolic input (PRISM and JANI), one may also use expressions over the model variables to identify states. For example, if the model has an integer-valued state variable s, then s < 5 refers to all states in which s is smaller than five. Of course, Boolean combinations of such expressions are allowed, i.e. s < 5 & (b | s < y) is valid for a model with integer variables s and y and Boolean variable b.

Probabilistic Computation Tree Logic (PCTL) / Continuous Stochastic Logic (CSL)

Idea

The (probability) measure on Markov models is typically defined on paths. These paths are defined as in temporal logic, or more specifically computation tree logic (CTL), a branching-time logic. That means that the formula alternates over descriptions of paths and descriptions of states.

Path Formulae

For this, we assume that a and b are state formulae and {op} is any one of <, <=, >, >=. The available path formulae are:

State Formulae

Here, we assume that a and b are state formulae, phi is a path formula and {op} is any one of <, <=, >, >=. The available state formulae are:

Obtaining Probabilities

Although formally not allowed in PCTL/CSL, one can also request the probability of fulfilling a path formula from each state. Instead of comparing to a given value P{op}b [ phi ], one can write P=? [ phi ] to obtain the actual values rather then obtaining a truth value.

Nondeterministic Models

For nondeterministic models, the formula can (and sometimes needs to) specify whether it refers to minimal or maximal probabilities. Since there is no information on how the nondeterminism in the models is to be resolved, Storm needs information on whether it should resolve the choices to minimize or maximize the values. That is, you cannot write P=? [F a], but have to either write Pmin=? [F a] or Pmax=? [F a]. While you can also specify min and max when comparing to a probability threshold, it’s not necessary to do it. By default, if the comparison operator {op} is < or <=, then the probability is maximized and otherwise minimized. The reasoning is the following: if the property holds in a state, then no matter which resolution of nondeterminism is taken, the probability will always be below (or equal) to the threshold value.

Reward extensions

To measure rewards (or costs) in models, Storm supports extensions of the aforementioned logics. More specifically, there are the following reward formulae, where a is a state formula:

Just like path formulae, these reward formulae can be embedded in an R operator to allow for value comparison or value computation:

In models with several reward structures, a particular reward structure has to be chosen:

In continuous-time models, rewards in states are based on the sojourn time in that state. In particular, a constant reward of 1 in every state reflects the sojourn time. This time-reward does not need to be added manually. Instead, the following immediately reflects the time operator, analogous to above.

Conditional Properties

The extension to conditional properties let’s you query the probabilities of an event conditioned on the fact that something else holds. The formula

can be used to query the probability that a state satisfying a is reached provided that a state satisfying b is also reached.

Examples

To illustrate how the formulae can be used, we give some examples of syntactically valid properties:

Multi-objective Model Checking

Storm supports multi-objective model checking: In nondeterministic models, different objectives might require different choices of actions in order to satisfy the property. This induces trade-offs between different strategies. Multi-objective model checking reveals such trade-offs by computing the Pareto curve, as explained in our example.

The simplest way of asking about these trade-offs are achievability queries: They ask whether there exists a strategy which fulfils all thresholds.

Instead of fixing all values, we can leave one threshold open and ask for the optimal value for the threshold:

If the other properties together are not achievable, the query returns False. One can also leave multiple thresholds open: Instead of a single value, the model checker returns a Pareto curve.

Naming Properties

To allow referring to specific properties, they can be equipped with names. To give the name name to a property P, you can write "name" : P.