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
pathprop is satisfied by all paths from state s"
pathprop is satisfied by some path from state s",
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.