Frequently Asked Questions /

PRISM Properties

How do I check if a property is true in multiple (or all) states?

Consider a typical boolean-valued PRISM property, such as:

P<0.01 [ F "error" ]

i.e. "the probability of reaching a state labelled with "error" is less than 0.01. By default, when model checking this query, PRISM will report the result of this property for the initial state of the model, i.e. whether, starting from the initial state, the probability of reaching "error" is below 0.01. (This is in contrast to older versions of PRISM, which used to report whether the property was true for all states.)

To check whether the above property is true for, say, all (reachable) states satisfying the label "safe", you should use filters, as illustrated below:

filter(forall, P<0.01 [ F "error" ], "safe")

If you want to check whether the property is true for all reachable states, you can use either of the following two (equivalent) properties:

filter(forall, P<0.01 [ F "error" ], true)
filter(forall, P<0.01 [ F "error" ])

In older versions of PRISM, checking that a property was true in a particular set of states was done using implication (=>). If you wish, you can still use a similar form of property to achieve this, as shown by the following example:

filter(forall, "safe" => P<0.01 [ F "error" ])

How do I compute the probability of an action occurring?

PRISM's property specification language is primarily state-based, e.g. you can compute the probability of reaching a state that satisfies the label "error":

P=? [ F "error" ]

So how do you compute the probability of a some action b occurring? You need to make a small change to your model. The cleanest way to do this is to add a small module that changes state when the action occurs, e.g.:

module checker

    q : [0..1] init 0;

    [b] q=0 -> (q'=1);
    [b] q=1 -> (q'=1);

endmodule

You can determine the probability of action b occurring in the model with the property:

P=? [ F q=1 ]

By design, the module above will not affect the behaviour (timing, probability, etc.) of your model at all, so all other properties will remain unchanged. This is true for any of the model types that PRISM supports. It may, though, lead to a (hopefully small) increase in total model size.

You can also modify the property above to compute, for example, the probability of b occurring within T time-units or the expected time until b occurs:

P=? [ F<=T q=1 ]
R{"time"}=? [ F q=1 ]

(where a constant T or reward structure time have been added to the model, as appropriate).

PRISM Manual

Frequently Asked Questions

[ View all ]