View - Edit - Print - Search

Running PRISM /

Adversaries

When model checking some properties of MDPs, PRISM can also generate an optimal adversary, i.e. one which corresponds to either the minimum or maximum values of the probabilities or rewards computed during verification. Recall that, for MDPs, PRISM quantifies over all possible adversaries, i.e. all possible resolutions of nondeterminism in the model. A typical property would be:

which computes the maximum probability, over all adversaries, of reaching a state satisfying the label "error", from all states of the model. When under the control of a specific adversary, the behaviour of an MDP is purely probabilistic, yielding a single value (for each state) for the probability of reaching "error". In addition to giving the maximum probability value(s), PRISM can produce an adversary of the MDP for which the probabilities (for each state) coincide with the maximum values.

For a probabilistic reachability property, such as the one above, a memoryless adversary suffices, that is one which always makes the same choice in any given state of the model. So, the default form in which PRISM provides an adversary is a DTMC derived by retaining only a single nondeterministic choice in each state of the MDP. This DTMC is given in the same format as when exporting the transition matrix of a DTMC, i.e. a list of transitions.

Currently, adversary generation is only implemented in the sparse engine, so you need to make sure this engine is enabled. From the command-line, you specify that an optimal adversary should be generated using the -exportadv switch, e.g.:

From the GUI, change the "Adversary export" option (under the "PRISM" settings) from "None" to "DTMC". You can also change the filename for the export adversary which, by default, is adv.tra as in the example above. Another option is to export the adversary as an MDP (this is identical to the model produced using the DTMC option, but can be imported back into PRISM as an MDP, if required). Use switch -exportadvmdp, instead of -exportadv form the command-line, or select the "MDP" option from the GUI.

PRISM also supports generation of adversaries for "reachability reward" properties (i.e. the R operator, with argument F) in identical fashion to the case described above.