One of the most important operators in the PRISM property specification language is the P operator, which is used to reason about the probability of an event's occurrence. This operator was originally proposed in the logic PCTL but also features in the other logics supported by PRISM, such as CSL. The P operator is applicable to all types of models supported by PRISM.
Informally, the property:
is true in a state s of a model if
"the probability that path property pathprop is satisfied by the paths from state s
meets the bound bound".
A typical example of a bound would be:
which means: "the probability that pathprop is satisfied by the paths from state s is greater than 0.98". More precisely, bound can be any of >=p, >p, <=p or <p,
where p is a PRISM language expression evaluating to a double in the range [0,1].
The types of path property supported by PRISM and their semantics will be discussed shortly.
For models that can exhibit nondeterministic behaviour (MDPs or PTAs), some additional clarifications are necessary. Whereas for fully probabilistic models such as DTMCs and CTMCs, probability measures over paths are well defined (see e.g. [KSK76] and [BKH99], respectively), for nondeterministic models a probability measure can only be feasibly defined once all nondeterminism has been removed.
Hence, the actual meaning of the property P bound [ pathprop ] in these cases is:
"the probability that pathprop is satisfied by the paths from state s
meets the bound bound for all possible resolutions of nondeterminism".
This means that, properties using the P operator then effectively reason about the
minimum or maximum probability, over all possible resolutions of nondeterminism,
that a certain type of behaviour is observed.
This depends on the bound attached to the P operator:
a lower bound (> or >=) relates to minimum probabilities
and an upper bound (< or <=) to maximum probabilities.
It is also very often useful to take a quantitative approach to probabilistic model checking, computing the actual probability that some behaviour of a model is observed,
rather than just verifying whether or not the probability is above or below a given bound.
Hence, PRISM allows the P operator to take the following form:
These properties return a numerical rather than a Boolean value. The S and R operators, discussed later, can also be used in this way.
As mentioned above, for nondeterministic models (MDPs or PTAs), either minimum or maximum probability values can be computed. Therefore, in this case, we have two possible types of property:
which return the minimum and maximum probabilities, respectively.
It is also possible to specify to which state the probability returned by a quantitative property refers. This is covered in the later section on filters.
PRISM supports a wide range of path properties that can be used with the P operator.
A path property is a formula that evaluates to either true or false for a single path in a model.
Here, we review some of the simpler properties that feature a single temporal operator,
as used for example in the logics PCTL and CSL. Later, we briefly describe how PRISM also supports more complex LTL-style path properties.
The basic different types of path property that can be used inside the P operator are:
X : "next"
U : "until"
F : "eventually" (sometimes called "future")
G : "always" (sometimes called "globally")
W : "weak until"
R : "release"
In the following sections, we describe each of these temporal operators. We then discuss the (optional) use of time bounds with these operators. Finally, we also discuss LTL-style path properties.
The property X prop is true for a path if prop is true in its second state,
An example of this type of property, used inside a P operator, is:
which is true in a state if "the probability of the expression y=1 being true in the next state is less than 0.01".
The property prop1 U prop2 is true for a path if
prop2 is true in some state of the path and prop1 is true in all preceding states.
A simple example of this would be:
which is true in a state if "the probability that z is eventually equal to 2, and that z remains less than 2 up until that point, is greater than 0.5".
The property F prop is true for a path if prop eventually becomes true at some point along the path. The F operator is in fact a special case of the U operator (you will often see F prop written as true U prop). A simple example is:
which is true in a state if "the probability that z is eventually greater than 2is less than 0.1".
Whereas the F operator is used for "reachability" properties, G represents "invariance". The property G prop is true of a path if prop remains true at all states along the path. Thus, for example:
states that, with probability at least 0.99, z never exceeds 10.
Like F and G, the operators W and R are derivable from other temporal operators.
Weak until (a W b), which is equivalent to (a U b) | G a, requires that a remains true until b becomes true, but does not require that b ever does becomes true (i.e. a remains true forever). For example, a weak form of the until example used above is:
which states that, with probability greater than 0.5, either z is always less than 2, or it is less than 2 until the point where z is 2.
Release (a R b), which is equivalent to !(!a U !b), informally means that b is true until a becomes true, or b is true forever.
All of the temporal operators given above, with the exception of X, have "bounded" variants, where an additional time bound is imposed on the property being satisfied.
The most common case is to use an upper time bound, i.e. of the form "<=t" or "<t", where t is a PRISM expression evaluating to a constant, non-negative value.
For example, a bounded until property prop1 U<=t prop2, is satisfied along a path if prop2 becomes true within t steps and prop1 is true in all states before that point.
A typical example of this would be:
which is true in a state if "the probability of y first exceeding 3 within 7 time units is greater than or equal to 0.98". Similarly:
is true in a state if "the probability of y being equal to 4 within 7 time units is greater than or equal to 0.98" and:
is true if the probability of y staying equal to 4 for 7 time units is at least 0.98.
The time bound can be an arbitrary (constant) expression, but note that you may need to bracket it, as in the following example:
You can also use lower time-bounds (i.e. >=t or >t) and time intervals [t1,t2], e.g.:
which refer to the probability of y becoming equal to 4 after 10 or more time units, and after between 10 and 20 time-units respectively.
For CTMCs, the time bounds can be any (non-negative) numerical values - they are not restricted to integers, as for DTMCs and MDPs. For example:
means that the probability of y being greater than 1 within 6.5 time-units (and remaining less than or equal to 1 at all preceding time-points) is at least 0.25.
We can also use the bounded F operator to refer to a single time instant, e.g.:
or, equivalently:
both of which give the probability of y being 6 at time instant 10.
PRISM also supports probabilistic model checking of the temporal logic LTL (and, in fact, PCTL*). LTL provides a richer set of path properties for use with the P operator, by permitting temporal operators to be combined. Here are a few examples of properties expressible using this functionality:
"with probability greater than 0.99, a request is eventually received, followed immediately by an acknowledgement"
"a message is sent infinitely often with probability 1"
"the probability of an error occurring that is never repaired”
Note that logical operators have precedence over temporal ones, so you will often need to include parentheses when using logical operators, e.g.:
For temporal operators, unary operators (such as F, G and X) have precedence over binary ones (such as U). Unary operators can be nested, without parentheses, but binary ones cannot.
So, these are allowed:
but this is not: