View - Edit - Print - Search

Property Specification /

The S Operator

The S operator is used to reason about the steady-state behaviour of a model, i.e. its behaviour in the long-run or equilibrium. PRISM currently only provides support for DTMCs and CTMCs. The definition of steady-state (long-run) probabilities for finite DTMCS and CTMCs is well defined (see e.g. [Ste94]). Informally, the property:

is true in a state s of a DTMC or CTMC if "starting from s, the steady-state (long-run) probability of being in a state which satisfies the (Boolean-valued) PRISM property prop, meets the bound bound". A typical example of this type of property would be:

which means: "the long-run probability of the queue being more than 75% full is less than 0.05".

Like the P operator, the S operator can be used in a quantitative form, which returns the actual probability value, e.g.:

and can be further customised with the use of filters.