View - Edit - Print - Search

Running PRISM /

Strategies

Properties to be model checked on MDPs (and their variants, such as POMDPs or IMDPs) usually quantify over strategies (or policies) of the model, i.e., over the different possible ways that nondeterminism can be resolved in the model. For example, this property:

determines the maximum probability, over all strategies, of reaching a state satisfying the label "goal". When checking such properties, you can also ask PRISM to generate a corresponding (optimal) strategy, which yields this maximum probability when followed. The strategy can then be viewed, exported or simulated.

Note: For consistency across models, PRISM now uses the terminology strategy (rather than alternatives such as policy). In older versions of the tool, these were referred to as adversaries. Currently, the newer (and more extensive) strategy generation functionality is implemented just for the "explicit" model checking engine, which is used automatically if strategy generation is requested. The old adversary generation functionality (see below) still exists for the "sparse" engine, but will be updated in the future.

Generating strategies. Optimal strategies can be generated either from the command-line or the graphical user interface (GUI). For the former, use the -exportstrat switch. Simple examples are:

From the GUI, you can trigger strategy generation by ticking the "Generate strategy" box either on the popup menu that appears when you right-click a property, or from the "Strategies" menu at the top. As long as it is supported, a strategy will be then generated once "Verify" is clicked.

From the same menu(s), you can then

• export the strategy to a file
• view the strategy by printing it in the log
• explore the strategy in the simulator

Strategy export types. Strategies can be viewed or exported in several different formats:

(i) Action list. This is a list of the action taken in each state of the model, e.g.:

where states, by default, are shown as a tuple of variable values.

(ii) Induced model. This is a representation of the model that is induced when the strategy is applied. There are two "modes" for this export: restrict, which shows the original model but with a restricted set of choices (e.g., an MDP with just one choice in each state); and reduce, which removes the nondeterminism resolved by the strategy (e.g., an MDP becomes a DTMC). The latter can be useful to re-import the model back into PRISM and analyse the induced model; the former is sometimes easier for visualising the strategy's choices. In each case, the transitions of the induced model are presented as a .tra file (as for normal model export), e.g.:

(iii) Dot file. This is, like the previous format, a view of the model induced by the strategy, but in Dot format, which allows it to be visualised.

Configuring strategy export. As hinted in the command-line examples above, the -exportstrat switch uses the file extension to determine the preferred format: if the strategy is exported to a file with extension .tra or .dot, then it uses an induced model or Dot file, respectively. Otherwise, the default is an action list. You can specify the desired format:

Further options can be added, e.g., to specify whether an induced model is exported in "restrict" or "reduce" mode:

A full list of available options is as follows:

• type (actions, induced or dot): the type of strategy export to use (action list, induced model or Dot file)
• mode (restrict or reduce): when exporting as an induced model or Dot file, whether to "restrict" or "reduce" the model (see above); the default is "restrict"
• reach (true or false): whether to restrict the strategy to states that are reachable when it is applied to the model (this is currently only used for exporting induced models and Dot files, and the default value is false and true, respectively, in these two cases)
• states (true or false): whether to show states, rather than state indices, for actions lists or Dot files; this is true by default
• obs (true or false): for partially observable models, whether to merge observationally equivalent states; this is true by default

Strategy types. PRISM generates several types of strategies. The simplest are memoryless deterministic strategies, which pick a single action in each state, as in the examples above. For some query types (e.g., step-bounded properties, or LTL-based properties), finite-memory strategies are generated, where an additional memory value is used. For these, induced models or Dot files are most useful since they will also show how the memory values are updated as the strategy is executed. Note that, in these cases, the state indices of the strategy will correspond to the product model constructed during model checking, not the original model. The product model can be exported using the -exportprodtrans and -exportprodstates switches.

Adversary generation. As mentioned above, the "sparse" model checking engine still includes older so-called "adversary generation" functionality. This can be used to export the induced model to a file using the -exportadv switch, e.g.:

where the -exportadv and -exportadvmdp export a DTMC and an MDP, respectively, i.e., corresponding to the "reduce" and "restrict" modes described above. From the GUI, change the "Adversary export" option (under the "PRISM" settings) from "None" to "DTMC" or "MDP". You can also change the filename for the export adversary which, by default, is adv.tra as in the example above.