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

(for all) and **A**

(there exists) operators,
instead of the probabilistic **E**

operator used in many other properties supported by PRISM.
**P**

Properties take the form:

A [ pathprop ]

E [ pathprop ]

E [ pathprop ]

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:

E [ F "goal" ] // There exists a path that reaches a state satisfying "goal"

A [ G x<=10 ] // Variable x is always at most 10 along all paths of the model

E [ F "ready" & (X "launch") ] // There exists a path along which label "ready" eventually becomes true and label "launch" is true immediately afterwards

A [ (G F x=1) | (G F x=2) ] // Along all paths, either x=1 or x=2 is true infinitely often

A [ G x<=10 ] // Variable x is always at most 10 along all paths of the model

E [ F "ready" & (X "launch") ] // There exists a path along which label "ready" eventually becomes true and label "launch" is true immediately afterwards

A [ (G F x=1) | (G F x=2) ] // Along all paths, either x=1 or x=2 is true infinitely often

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.