The two other principal operators for specifying properties are the P and S operators.
The P operator is applicable to all three model types.
It allows us to reason about the probability that a certain type of behaviour is observed.
Informally, the property:
is true in a state s of a DTMC, MDP or CTMC 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 path property pathprop is satisfied by the paths from state s is greater than 0.98".
The types of path property supported by PRISM and their semantics are discussed below.
For a DTMC, the probability measure of the set of paths from a state s which satisfy a path property pathprop
is well-defined; see e.g. [HJ94].
Similarly, for a CTMC, the probability measure for such a set of paths can also be defined; see e.g. [BKH99].
For MDPs, however, a probability measure can only be feasibly defined once all nondeterminism has been removed.
Hence, the actual meaning of the property
P bound [ pathprop ]
for an MDP is taken to be
"the probability that path property pathprop is satisfied by the paths from state s
meets the bound bound for all possible resolutions of nondeterminism".
This means that, for an MDP, properties using the P operator actually 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.
For more details on this, see e.g. [BK98].
As illustrated in the earlier syntax definition,
various different types of path property can be used inside the P operator.
X : "next"
U : "until"
F : "eventually" (sometimes called "future", "finally", or "forwards")
G : "always" (sometimes called "globally")
as well as bounded variants of the last three:
U time
F time
G time
A path property is evaluated to either true or false for a single path in a model. In the following sections, we describe the semantics for each of the three types of path property.
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 common application of this type of property is the case where prop1 is true.
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.
The "bounded" variants of U, F and G path properties are generalisations where an additional bound is imposed on the property being satisfied. Since in DTMCs and MDPs, time progresses in discrete steps, whereas CTMCs model real (continuous) time,
we treat these two cases separately for this operator.
For a DTMC or MDP, the time interval specification time must be of the form "<=t"
where t is a PRISM expression evaluating to a non-negative integer. A bounded until property prop1 U<=t prop2, for example, 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 steps 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 steps is greater than or equal to 0.98" and:
is true if the probability of y staying equal to 4 for 7 time steps is at least 0.98.
In the context of a CTMC, the time interval specification time can take any of the three forms: >=t, <=t or [t1,t2], where t, t1 and t2 are PRISM expression evaluating to a non-negative doubles, and t1 is no greater than t2. In each case, time defines an interval of real values in which the path property must be true.
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.
states that the probability of y exceeding 1 at some point after 5.5 time-units have elapsed is less than 0.4, and:
says that the probability that y exceeds 1 for the whole time interval [5.5,6.5] is greater than zero".
We can also use the bounded F operator to refer to a single time instant, e.g.:
refers to the probability of y being 6 at time instant 10.
