In order to analyse a probabilistic model which has been specified and constructed in PRISM, it is necessary to identify one or more properties of the model which can be evaluated by the tool. As is typically the case with formal verification techniques, in PRISM this is done using temporal logic. More specifically, properties are expressed in a language based on the logics PCTL (for DTMCs and MDPs) and CSL (for CTMCs), probabilistic extensions of the classical temporal logic CTL. In fact, PRISM supports numerous additional customisations and extensions of these two logics. Full details of the property specifications permitted in PRISM are provided in the following sections. For the precise syntax and semantics of the original two logics, see [HJ94],[BdA95] for PCTL and [ASSB96],[BKH99] for CSL.
Before discussing property specifications in detail, it is perhaps instructive to first illustrate some typical examples of properties which PRISM can handle. The following are a selection of such properties. In each case, we give both the PRISM syntax and a natural language translation:
"the algorithm eventually terminates successfully with probability 1"
"from an initial state, the probability that more than 5 errors occur within the first 100 time units is less than 0.1"
"when a shutdown occurs, the probability of system recovery being completed in between 1 and 2 hours without further failures occurring is greater than 0.75"
"in the long-run, the probability that an inadequate number of sensors are operational is less than 0.01"
Note that the above properties are all assertions, i.e. ones to which we would expect a "yes" or "no" answer. This is because all references to probabilities are associated with an upper or lower bound which can be checked to be either true or false. In PRISM, we can also directly specify properties which evaluate to a numerical value, e.g.:
"the probability that process 1 terminates before process 2 does"
"the maximum probability that more than 10 messages have been lost by time T"
"the long-run probability that the queue is more than 75% full"
Furthermore, PRISM makes it easy to compute the values of such properties for a range of parameters and plot graphs of the results using experiments. This is often a very useful way of identifying interesting patterns or trends in the behaviour of a system. See the Case Studies section of the PRISM website for many examples of this kind of analysis.
One of the most fundamental tasks when specifying properties of a model is to identify particular sets or classes of states of the model. For example, to verify a property such as "the algorithm eventually terminates successfully with probability 1", it is first necessary to identify the states of the model which correspond to situations where "the algorithm has terminated successfully".
In PRISM, this is achieved simply by writing an expression in the PRISM language
which evaluates to a Boolean value.
This expression will typically contain references to variables (and constants)
from the model to which it relates.
The set of states corresponding to this expression is those for which it evaluates to "true".
Returning to our example above, the property "the algorithm has terminated successfully"
might be represented, for instance, by the PRISM language expression
program_counter=10 & num_errors=0.
In terms of the way temporal logics are usually presented,
these expressions correspond to atomic propositions.
The basic syntax of the language for expressing a PRISM property prop is given by the following grammar:
where:
expr is a PRISM language expression which evaluates to a Boolean (as described in the previous section),
p is a PRISM language expression evaluating to a double in the range [0,1],
t is a PRISM language expression evaluating to a non-negative double or integer.
A property is evaluated with respect to a single state of a model.
For the syntax given above, all properties evaluate to Boolean values,
i.e. for any state $s$ of a model, a property is either "true" or "false" in that state.
Equivalently, we also say that a property is "satisfied" or "not satisfied" in a state.
For the basic operators of the logic
(i.e. true, false, expr, !, &, | and =>)
the semantics are as for classical propositional logic:
true is true in all states,
false is not true in any state,
expr is true if the PRISM expression expr evaluates to true,
!prop is true if prop is not true,
prop1 & prop2 is true if both prop1 and prop2 are true,
prop1 | prop2 is true if either prop1 or prop2 is true,
prop1 => prop2 is true if prop1 implies prop2.
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.
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.
Although this could in principle relate to all three model types,
PRISM currently only provides support for CTMCs.
The definition of steady-state (long-run) probabilities for finite CTMCs is well defined (see e.g. [Ste94]).
Informally, the property:
is true in a state s of a CTMC if
"starting from s, the steady-state (long-run) probability of being in a state which satisfies 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".
All of the properties described in the previous sections evaluate to a Boolean value. Although the satisfaction of a property is defined in terms of a single state, when analysing a property of a model, PRISM considers the property to be true if it is satisfied in all states of the model, and false otherwise.
To check if a property is satisfied in some subset of states, for example just the initial states, properties can be prefixed with an implication, e.g.:
See the section "Properties Files" for details of the "init" expression.
As discussed earlier, it is often useful to know the actual probability that some behaviour of a model is observed, rather than just whether or not the probability is above or below a given bound. Hence, PRISM allows properties of the following form:
The arguments to these operands, either a path property for P or another property for S,
are exactly as before; the only difference is that the probability bound is removed.
These properties return a numerical rather than a Boolean value.
Note that the probability bound on a P or S operator can only be replaced with =?
if it is the outermost operator of the property in which it appears; otherwise the semantics are not well defined.
Note also that, for MDPs, the situation is slightly more complex.
Probabilities for an MDP can only be computed once the nondeterminism
has been resolved. Hence, PRISM actually computes either the minimum or maximum probability of
a path property being satisfied, quantifying over all possible resolutions (i.e. the best and worst cases).
Therefore, for MDPs we have two possible types of property:
which return the minimum and maximum probabilities, respectively.
All of these operators return a single numerical value. In the simplest case, where the model being verified has a single initial state, the numerical value returned is the one corresponding to that state. Hence, for example:
returns the probability of, from the initial state, reaching a state satisfying x=5&y=5.
It is also possible, however, to obtain the probability for an arbitrary state,
by specifying an atomic proposition, true only in that state, inside braces ({...}) before the closing ] bracket.
This is known as a filter.
For example, if the model contains two variables, X and y, then:
returns the probability of, from the state (1,2) (i.e. x=1 and y=2),
reaching a state satisfying x=5&y=5.
It is possible of course that the expression in the filter satisfies more than one state.
If this the case, by default the first such state (lexicographically) is chosen.
In this situation, PRISM will display a warning to notify you that the expression in the filter matched multiple states
and will display what the first matching state is.
The same approach is taken in the situation where no filter is given
but the model contains multiple initial states.
In this case, the numerical result obtained is for the first (lexicographically speaking) of the set of initial states.
Note that if the expression in the filter is not satisfied by any states of the model,
an error is reported.
It is also possible to possible to request either the minimum and maximum value from a set of values. For example:
return the minimum and maximum probability, respectively,
of reaching a state satisfying x=5&y=5 from all the states satisfying y=2.
In addition, PRISM will report the states of the model in which the minimum or maximum probability is attained.
You can in fact also request that both the minimum and maximum value are computed simultaneously using,
for example, {y=2}{min}{max}. In this case, both values will be reported, but the actual
return value of the property will be the minimum value.
Finally, filters can also be used for conventional P and S properties.
This has no bearing on the result of model checking a property;
it simply causes the probabilities (where non-zero) for all states satisfying the expression in the filter to be printed during model checking.
For example:
will return a Boolean value, depending whether the property is true in all states of the model or not,
but the probability (where non-zero) of path property true U x=5&y=5 being satisfied will be displayed for all states where y=2.
Files containing properties to be analysed by PRISM can also contain constants, as is the case for model files. These are defined in identical fashion, for example:
As before, these constants can actually be left undefined and then later assigned either a single value or a range of values using experiments.
In fact, probability bounds for the P or S operators (like P above)
and upper or lower bounds for the U operator (like T above)
can be arbitrary expressions, provided they are constant.
Furthermore, expressions in the properties file can also refer to constants previous defined in the model file.
Another feature of properties files is labels. These are a way of defining sets of states that will be referred to in properties (they correspond to atomic propositions in a temporal logic setting). As described earlier, labels can be defined in either model files or property files.
Labels are defined using the keyword label, followed by a name (identifier) in double quotes, and then an expression which evaluates to a Boolean. Definition and usage of formulas are illustrated in the following example:
Two special cases are the "init" and "deadlock" labels which are always defined.
Thes are true in initial states of the model and states where deadlocks were found (and fixed by adding self-loops), respectively.
The former is useful if you only wish to to check whether a property is true in the initial states, e.g.:
A PRISM properties file can contain any number of properties.
Like model files, they can also include any amount of white space (spaces, tabs, new lines, etc.) and C-style comments, which are both ignored.
By convention, files are given the extension .pctl for properties of DTMCs and MDPs
and extension .csl for properties of CTMCs.
PRISM models can be augmented with information about rewards (or costs).
The tool can analyse properties which relate to the expected values of these rewards.
This is achieved using the R operator, which works in a similar fashion to the
P and S operators, and can be used either in a Boolean-valued query, e.g.:
where bound takes the form <r, <=r, >r or >=r for an expression r evaluating to a non-negative double,
or a real-valued query, e.g.:
where query is =? for a DTMC or CTMC, and min=? or max=? for MDPs.
Informally, "R bound [ rewardprop ]" is true in a state of a model if
"the expected reward associated with rewardprop of the model when starting from that state''
meets the bound bound and "R query [ rewardprop ]" returns the actual expected reward value.
There are four different types of reward properties, namely:
F prop
C<=t
I=t
S.
Below, we consider each of these cases in turn. The descriptions here are kept relatively informal. For precise definitions (in the case of DTMCs and CTMCs), see [KNP07a].
"Reachability reward" properties associate a reward with each path of a model. More specifically, they refer to the reward accumulated along a path until a certain point is reached. The manner in which rewards are accumulated depends on the model type. For DTMCs and MDPs, the total reward for a path is the sum of the state rewards for each state along the path plus the sum of the transition rewards for each transition between these states. The situation for CTMCs is similar, except that the state reward assigned to each state of the model is interpreted as the rate at which rewards are accumulated in that state, i.e. if t time units are spent in a state with state reward r, the reward accumulated in that state is r x t. Hence, the total reward for a path in a CTMC is the sum of these products for each state along the path plus the sum of the transition rewards for each transition between these states.
The reward property "F prop" corresponds to the reward cumulated along a path
until a state satisfying property prop is reached,
where rewards are cumulated as described above.
State rewards for the prop-satisfying state reached are not included in the cumulated value.
In the case where no state satisfying prop is reached, the reward is equal to infinity.
A common application of this type of property is the case when the rewards associated with the model correspond to time. One can then state, for example:
which is true in a state s if "the expected time taken to reach, from s, a state where z equals 2 is less than or equal to 9.5".
Note: In the current release of PRISM, "reachability reward" properties for MDPs can only be analysed using the MTBDD or sparse engines; for DTMC and CTMCs, any engine can be used.
"Cumulative reward" properties also associate a reward with each path of a model,
but only up to a given time bound.
The property C<=t corresponds to the reward cumulated along a path
until t time units have elapsed.
For DTMCs and MDPs, the bound t must evaluate to an integer;
for CTMCs, it can evaluate to double.
State and transition rewards along a path are cumulated exactly as described in the previous section.
A typical application of this type of property is the following. Consider a model of a disk-drive controller which includes a queue of incoming disk requests. If we assign a reward of 1 to each transition of the model corresponding to the situation where an incoming request is lost because the queue is full, then the property:
would return, for a given state of the model, "the expected number of lost requests within 15.5 time units of operation".
Note: In the current release of PRISM, "cumulative reward" properties can only be analysed for DTMCs and CTMCs.
"Instantaneous reward" properties refer to the reward of a model at a particular instant in time.
The reward property I=t associates with a path the reward in the state
of that path when exactly t time units have elapsed.
For DTMCs and MDPs, the bound t must evaluate to an integer;
for CTMCs, it can evaluate to double.
Returning to our example from the previous section of a model for a disk-request queue in a disk-drive controller, consider the case where the rewards assigned to each state of the model give the current size of the queue in that state. Then, the following property:
would be true in a state s of the model if "starting from s, the expected queue size exactly 100 time units later is less than 4.4". Note that, for this type of reward property, state rewards for CTMCs do not have to refer to rates; they can refer to any instantaneous measure of interest for a state.
Note: In the current release of PRISM, "instantaneous reward" properties of DTMCs and MDPs can only be analysed with the sparse and MTBDD engines, not hybrid.
Unlike the previous three types of property, "steady-state reward" properties relate not to paths, but rather to the reward in the long-run. A typical application of this type of property would be, in the case where the rewards associated with the model correspond to power consumption, the property:
which is true in a state s if "starting from s, the long-run average power consumption is less than 0.7".
Note: In the current release of PRISM, "steady-state reward" properties can only be analysed for CTMCs.
In the case where a PRISM model has multiple reward structures you may need to specify which reward structure your property refers to. This is done by placing the information in braces ({}) after the R operator. You can do so either using the name assigned to a reward structure (if any) or using the index (where 1 means the first rewards structure in the PRISM model file, 2 the second, etc.). Examples are:
Note that when using an index to specify the reward structure, you can actually put any expression that evaluates to an integer. This allows you to, for example, write a property of the form R{c}=?[...] where c is an undefined integer constant. You can then vary the value of c in an experiment and compute values for several different reward structures at once.
If you don't specify a reward structure to the R operator, by default, the first one in the model file is used.
