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. PRISM's property specification language subsumes several well-known probabilistic temporal logics, including PCTL, CSL, probabilistic LTL and PCTL*. PCTL is used for specifying properties of discrete-time models such as DTMCs or PTAs, and also real-time models such as PTAs; CSL is an extension of PCTL for CTMCs; LTL and PCTL* can be used to specify properties of discrete-time models (or untimed properties of CTMCs). PRISM also supports most of the (non-probabilistic) temporal logic CTL.
In fact, PRISM also 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. The presentation given here is relatively informal. For the precise syntax and semantics of the various logics, see [HJ94],[BdA95] for PCTL, [ASSB96],[BKH99] for CSL and, for example, [Bai98] for LTL and PCTL*. You can also find various pointers to useful papers in the About and Documentation sections of the PRISM website.
Before discussing property specifications in more 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"
"the probability that more than 5 errors occur within the first 100 time units is less than 0.1"
"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" (for an MDP/PTA)
"the long-run probability that the queue is more than 75% full"
Furthermore, PRISM makes it easy to combine such properties into more complex expressions, compute their values 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 terms of the way temporal logics are usually presented, these correspond to atomic propositions.
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. We say that the expression is "satisfied" in these states.
For example, in the property given above:
the expression num_errors > 5 is used to identify states of the model where more than 5 errors have occurred.
It is also common to use labels to identify states in this way, like "terminate" in the example:
Properties can refer to labels either from the model to which the property relates, or included in the same properties file.
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, such as 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 discrete-time models. 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:
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.
PRISM models can be augmented with information about rewards (or, equivalently, 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 =?, min=? or max=?.
In the latter case, filters can be used, as for the P and S operators.
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 various different types of reward properties:
F prop
F (prop1 & F prop2)
C<=t
C
I=t
S.
Below, we consider each of these cases in turn. The descriptions here are kept relatively informal. Precise definitions for most of these can be found in, for example, [KNP07a] (for DTMCs and CTMCs) or [FKNP11] (for MDPs).
"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 the probability of reaching a state satisfying prop is less than 1, 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".
These generalise the "reachability" properties above. Again, reward is accumulated along a path up until some point,
but this is specified in a more general way, by giving a formula in the co-safe fragment of linear temporal logic (LTL).
Rewards are accumulated up until the point where the formula is first satisfied. For example, this property, for a DTMC or CTMC,
queries the expected reward accumulated until first goal equals 1 and then subsequently goal equals 2:
and this property, for an MDP, minimises the expected reward until loc equals 1,
having passed only through states where loc never equals 4
As for reachability rewards, if the probability of satisfying the formula is less than 1, then the expected reward is defined to be infinite.
Intuitively, a co-safe formula is one that is satisfied within a finite period of time,
and remains true for ever once it becomes true for the first time.
For simplicity, PRISM actually supports the syntactic co-safe fragment of LTL,
which is defined as any LTL formula that only uses the temporal operators F, U and X
(but not G, for example).
PRISM's notation for LTL formulas is described here.
"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".
"Total reward" properties refer to the accumulation of state and transition rewards in the same way as for "reachability reward" and "cumulative reward" properties, but the rewards is accumulated indefinitely, i.e. the total reward accumulated along the whole (infinite) path. Note that this means that, unless a path ends up remaining forever in states with zero reward, the total reward will be infinite.
Re-using the reward structure in the previous example,
returns "the expected total number of lost requests".
"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.
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".
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.
There are currently a few restrictions on the model checking engines that can be used for some reward properties. The following table summarises the currently availability, where S, M, H and E denote the "sparse", "MTBDD", "hybrid" and "explicit" engines, respectively, for DTMCs, CTMCs and MDPs. For PTAs, support for rewards is currently quite restrictive; see the later section on real-time model properties for details.
F | cosafe | C<=t | C | I=t | S | |
| DTMCs | SMHE | SMHE | SMHE | SMHE | SMHE | SMHE |
| CTMCs | SMHE | SMHE | SMHE | SMHE | SMHE | SMHE |
| MDPs | SM-E | SMHE | S--E | ---- | SM-E | ---- |
For MDPs, PRISM supports multi-objective properties. Consider a property that uses the P operator. For example:
This states that, for all strategies (or policies) of the MDP, the probability of reaching an "error" state is less than 0.01.
Multi-objective queries differ in two important ways. Firstly, (by default) they ask about the existence of a strategy. Secondly they refer to multiple properties of a strategy. For example:
means: "does there exist a strategy of the MDP under which the probability of reaching an "error1" state is less than 0.01 and the probability of reaching an "error2" state is less than 0.02?"
To use the terminology from [FKP12], the above is an "achievability" query (i.e., is this combination of objectives achievable by some strategy?). PRISM also supports two other kinds of multi-objective query: "numerical" and "Pareto" queries.
A "numerical" query looks like:
meaning "what is the minimum possible probability of reaching "error1", over all strategies of the MDP for which the probability of reaching "error2" is less than 0.02?".
A "Pareto" queries leaves both of the objectives unbounded, e.g.:
This asks PRISM to compute (approximately), the Pareto curve for this pair objectives. Intuitively, this is the set of pairs of probabilities (of reaching "error1"/"error2") such that reducing one probability any more would necessitate an increase in the other probability.
For simplicity, the examples above all refer to the probability of reaching classes of states in the model. Other types of property (objective) are also possible.
Firstly, we can extend the examples above by referring to the probability of any LTL property. For example:
"What is the maximum probability of staying forever in "good1" states, such that the probability of visiting "good2" states infinitely often remains at least 0.9?".
We can also use more than 2 objectives, e.g.:
"What is the maximum probability of staying forever in "good1" states, such that the probability of visiting "good2" states infinitely often remains at least 0.9 and the probability of visiting "good3" states infinitely often remains at least 0.95?".
Multi-objective queries can also refer to the expected total cumulative value of a reward structure. We write such properties in the form:
"What is the minimum expected cumulative value of reward structure "time", such that the expected cumulative value of reward structure "energy" is below 1.45.
Note that this C reward operator differs from the F "target" operator, usually used for standard (single-objective) MDP model checking. Whereas the F "target" operator refers to the expected reward accumulated until a "target" state is reached the C operator refers to the expected total reward.
A few important notes regarding rewards:
Finally, time-bounded variants of both probabilistic reachability and expected cumulative rewards objectives can be used. Here is an example that uses the latter:
PRISM can perform multi-objective model checking using two distinct solution methods, which are described in [FKN+11] and [FKP12]. The former is based on the use of linear programming; the latter reduces multi-objective model checking to a series of simpler problems, solved using value iteration (or the Gauss-Seidel variant of value iteration). The default is "Value iteration". You can change this in the GUI using the option "MDP multi-objective solution methods", or using the command-line switches -lp, -valiter, -gs.
There are some restrictions for the different methods, e.g.
The classes of property that can be checked for real-time models (PTAs and POPTAs) are currently more restricted than for the other kinds of models that PRISM supports. This is because the model checking procedures are quite different for this type of model. We describe these restrictions here. The situation is also dependent on which of the PTA model checking engines is being used.
For the "stochastic games" engine, we essentially only allow unbounded or time-bounded probabilistic reachability properties, i.e. properties of the form:
where target is a Boolean-valued expression that does not include references to any clock variables and T is an integer-valued expression. The P operator cannot be nested and the S and R operators are not supported.
The "backwards reachability" engine is similar but currently only handles maximum probabilities.
For the "digital clocks" engine, there is slightly more flexibility,
e.g. until (U) properties are allowed, as are clock variables in expressions and arithmetic expressions such as:
This engine, like the "stochastic games" engine, does not allowed nested properties. Also, references to clocks must, like in the modelling language, not use strict comparisons
(e.g. x<=5 is allowed, x<5 is not).
The digital clocks also has support for rewards: it is possible to check reachability reward properties of the form:
Reward structures specified in the model, though, must not depend on clock variables. Formally, the class of PTAs with this kind of reward structure is sometime called linearly priced PTAs (see e.g. [KNPS06].
The digital clocks method is based on a language-level translation from a PTA model to an MDP one. If you want to see the MDP PRISM model that was generated, add the switch -exportdigital digital.nm when model checking property to export the model file to digital.nm.
For partially observable models (POMDPs and POPTAs), PRISM uses the same property language as the their fully observational equivalents (MDPs and PTAs). However, a more limited range of properties are available. For POMDPs, PRISM currently supports probabilistic reachability, probabilistic until, or expected reachability rewards properties, i.e.:
or bounded variants with a probability/threshold instead
of the min=? or max=?.
For the verification methods currently implemented,
there are a few additional restrictions.
Firstly, the target (and remain) expression appearing
in the property must be an observable.
In other words, if any state of the POMDP satisfies the expression,
then all other observationally equivalent states must also satisfy it.
This is easily achieved by only using either observable variables
or named observables in the expression, but that is not required.
Secondly, probabilities and expected rewards are only computed from a single state.
POPTAs are currently verified using the "digital clocks" approach to translate them into a POMDP, so they inherit the same restrictions (that strict or diagonal clock comparisons are not allowed). However for POPTAs, time-bounded probabilistic reachability is also supported.
For uncertain models, currently interval MDPs (IMDPs) or interval DTMCs (IDTMCs), PRISM performs robust verification, which considers the best- or worst-case behaviour that can arise depending on the way that probabilities are selected from intervals.
For example, instead of a property for a DTMC such as
which asks for the probability to reach a state satisfying "goal", IDTMCs use MDP-style queries:
which compute the minimum or maximum possible probability that can arise.
Similarly, for an IMDP, there are now two separate quantifications, firstly over strategies (policies) and secondly over the distinct ways that transition probabilities can be selected from intervals, for which min or max appear in that order in the query. For example:
return the minimum and maximum values, respectively, over resolutions of transition probabilities for the maximum probability of reaching "goal". Similarly, minmin and minmax are used for the minimum probability of reaching "goal". Model checking is supported for:
P operator, for next and bounded/unbounded until/reachability properties
R operator, for the expected reward to reach a target or satisfy a co-safe LTL formula
PRISM also supports model checking of the non-probabilistic temporal logics CTL (computation tree logic) and LTL (linear temporal logic).
Properties in these logics use the A (for all) and E (there exists) operators,
instead of the probabilistic P operator used in many other properties supported by PRISM.
Properties take the form:
which are true in a state s of a model if
"path property pathprop is satisfied by all paths from state s"
and
"path property pathprop is satisfied by some path from state s",
respectively.
The syntax for LTL formulas is the same as those allowed within the P operator.
Example properties include:
If you check a CTL property of the form A [ G "inv" ] and it is false, PRISM will generate a counterexample in the form of a path that reaches a state where "inv" is not true. This is displayed either in the simulator (from the GUI) or at the command-line. Similarly, if you check E [ F "goal" ] and the result is true, a witness (a path reaching a "goal" state) will be generated.
The syntax of the PRISM property specification language subsumes various probabilistic temporal logics, including PCTL, CSL, (probabilistic) LTL, PCTL* and CTL. Informally, the syntax can be summarised as follows: a property can be any valid, well-typed PRISM expression, which (optionally) also includes the probabilistic operators discussed previously (P, S and R) and the non-probabilistic (CTL) ones A and E). This mean that any of the following operators can be used:
- (unary minus)
*, / (multiplication, division)
+, - (addition, subtraction)
<, <=, >=, > (relational operators)
=, != (equality operators)
! (negation)
& (conjunction)
| (disjunction)
<=> (if-and-only-if)
=> (implication)
? (condition evaluation: condition ? a : b means "if condition is true then a else b")
P (probabilistic operator)
S (steady-state operator)
R (reward operator)
A (for-all operator)
E (there-exists operator)
This allows you to write any property expressible in logics such as PCTL and CSL. For example, CSL allows you to nest P and S operators:
"the probability of it taking more than 2 hours to get to a state from which the long-run probability of at least 5 servers being operational is >0.9"
You can also express various arithmetic expressions such as:
"the probability that the system is not operational at any point during the second hour of operation"
"the expected fraction of time that the system is available (i.e. the expected interval availability) in the time interval [0, t]"
"the (conditional) probability that component A eventually fails, given that at least one component fails"
We omit a formal presentation of the semantics of the PRISM property language. The semantics of the probabilistic temporal logics that the language incorporates can be found from a variety of sources. See for example the pointers given in the About and Documentation sections of the PRISM website.
It is worth, however, clarifying a few points specific to PRISM. A property is evaluated with respect to a particular state of a model. Depending on the type of the property, this value may either be a Boolean, an integer or a double. When performing model checking, PRISM usually has to actually compute the value for all states of the model but, for clarity, will by default report just a single value. Typically, this is the value for the (single) initial state of the model. For example, this:
will report the probability, from the initial state of the model, of reaching an "error" state. This:
will return true if and only if the probability, from the initial state, is greater than 0.5.
Note: This is contrast to older versions of PRISM, which treated numerical and Boolean-valued properties differently in this respect.
For models with multiple initial states, we need to adapt these definitions slightly. In this case, the two properties above will yield, respectively:
true if and only if the probability is greater than 0.5 from all initial states.
You can also ask PRISM to return different values using filters, which are described in the next section.
As discussed above, when reporting the result of model checking a property, PRISM will by default return the value for the (single) initial state of the model. However, since PRISM in fact usually has to compute values for all states simultaneously, you can customise PRISM properties to obtain different results. This is done using filters.
Filters are created using the filter keyword. They take the following form:
where op is the filter operator (see below), prop is any PRISM property and states is a Boolean-valued expression identifying a set of states over which to apply the filter.
In fact, the states argument is optional; if omitted, the filter is applied over all states. So, the following properties are equivalent:
Here's a simple example of a filter:
This gives the maximum value, starting from any state satisfying x=0, of the probability of reaching an "error" state.
Here's another simple example, which checks whether, starting from any reachable state, we eventually reach a "done" state with probability 1.
We could modify this property slightly to instead check whether, from any state that satisfies the label "ready", we eventually reach a "done" state with probability 1. This could be done with either of the following two equivalent properties:
Note: In older versions of PRISM, the property above could be written just as "ready" => P>=1 [ F "done" ] since the result was checked for all states by default, not just the initial state. Now, you need to explicitly include a filter, as shown above, to achieve this.
Most filters of the form filter(op, prop, states)
apply some operator op to the values of property prop
for all the states satisfying states,
resulting in a single value.
The full list of filter operators op in this category is:
min: the minimum value of prop over states satisfying states
max: the maximum value of prop over states satisfying states
count: counts the number of states satisfying states for which prop is true
sum (or +): sums the value of prop for states satisfying states
avg: the average value of prop over states satisfying states
first: the value of prop for the first (lowest-indexed) state satisfying states
range: the range (interval) of values of prop over states satisfying states
forall (or &): returns true if prop is true for all states satisfying states
exists (or |): returns true if prop is true for some states satisfying states
state: returns the value for the single state satisfying states (if there is more than one, this is an error)
There are also a few filters that, rather than returning a single value, return different values for each state, like a normal PRISM property:
argmin: returns true for the states satisfying states that yield the minimum value of prop
argmax: returns true for the states satisfying states that yield the maximum value of prop
print: does not change the result of prop but prints the (non-zero) values to the log
printall: like print, but displays all values, even for states where the value is zero
Here are some further illustrative examples of properties that use filters.
Filters provide a quick way to print the results of a model checking query for several states. In most cases, for example, a P=? query just returns the probability from the initial state. To see the probability for all states satisfying x>2, use:
Values are printed in the log (i.e. to the "Log" tab in the GUI or to the terminal from the command-line). For small models, you could omit the final states argument (x>2 here) and view the probabilities from all states. You can also use PRISM's verbose mode to view values for all states, but filters provide an easier and more flexible solution.
print filters do not actually alter the result returned so, in the example above, PRISM will still return the probability for the initial state, in addition to printing other probabilities in the log.
You can also use print filters to display lists of states. For example, this property:
prints the states which have the highest probability of reaching an error state.
However, you should exercise caution when using argmax (or argmin) on properties such as P=? [ ... ] (or S=? [ ... ] or R=? [ ... ]), whose results are only approximate due to the nature of the methods used to compute them (or because of round-off errors.)
Another common use of filters is to display the value for a particular state of the model (rather than the initial state, which is used by default). To achieve this, use e.g.:
where x=2&y=3 is assumed to specify one particular state.
A state filter will produce an error if the filter expression is not satisfied by exactly one state of the model.
Filters can also be built up into more complex expressions. For example, the following two properties are equivalent:
The range filter, unlike most PRISM expressions which are of type Boolean, integer or double, actually returns an interval: a pair of integers or doubles. For example:
gives the range of all possible values for the probability of reach a state satisfying count=10, from all states satisfying count=0.
As will be described below, this kind of property also results from the use of old-style ({...}) filters and properties on models with multiple initial states.
In older versions of PRISM, filters were also available, but in a less expressive form. Previously, they were only usable on P, S or R properties and only a small set of filter operators were permitted. They were also specified in a different way, using braces ({...}). For compatibility with old properties files (and for compactness), these forms of filters are still allowed. These old-style forms of filters:
are equivalent to:
Notice that the first of the four properties above (i.e. an old-style filter of the form {states} will result in an error if states is not satisfied by exactly one state of the model. Older versions of PRISM just gave you the value for the first state state satisfying the filter, without warning you about this. If you want to recreate the old behaviour, just use a first filter:
Finally, for completeness, we show what the default filters are in PRISM, i.e. how the way that PRISM returns values from properties by default could have been achieved equivalently using filters.
Queries of the form:
are the same as:
and queries of the form:
are the same as either:
for the cases where there the model has a single initial state or multiple initial states, respectively.
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, values such as the 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 labels are illustrated in the following example:
Two special cases are the "init" and "deadlock" labels which are always defined.
These are true in initial states of the model and states where deadlocks were found (and, usually, fixed by adding self-loops), respectively.
For convenience, properties can be annotated with names, as shown in the following example:
which gives the name "safe" to the property. It is then possible to include named properties as sub-expressions of other properties, e.g.:
Notice that the syntax for referring to named properties is identical to the syntax for labels. For this reason, property names must be disjoint from those of any existing labels.
You can refer to property names when using the command-line switch -prop to specify which property is to be model checked.
A PRISM properties file can contain any number of properties. It is good practice, as shown in the examples above, to terminate each property with a semicolon. Currently, this is not enforced by PRISM (to prevent incompatibility with old properties files) but this may change in the future.
Like model files, properties can also include any amount of white space (spaces, tabs, new lines, etc.) and C-style comments, which are both ignored.
The recommended file extension for PRISM properties is now .props.
Previously, though, the convention was to use extension .pctl for properties of DTMCs, MDPs or PTAs
and extension .csl for properties of CTMCs, so these are still also valid.
Site hosted at the Department of Computer Science, University of Oxford