PRISM also supports most operators from the temporal logic CTL [CE81], of which the probabilistic logics PCTL and CSL are an extension. CTL uses the A (for all) and E (there exists) operators, instead of the probabilistic P operator, to ask whether all (or some) paths from a state satisfy a particular path formula.
For example:
mean "there exists a path that reaches a state labelled with goal"
and "all paths reach a state labelled with goal", respectively.
Similarly:
state that some path (or all paths) satisfy G "inv", meaning that label "inv" holds in every state along the path.
If you check a 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.