Evaluation of an adversary

[Ashutosh Pandey]

Hello All,

Is it possible to evaluate an adversary on (MDP) PRISM specification?

Basically, using a command-line or through code, I should be able to give a PRISM specification and an adversary as inputs, and PRISM should return the expected utility when the adversary is applied to the specification.

Thanks,

Ashutosh

[Joachim Klein]

Hi Ashutosh,

As far as I know, there is no direct mechanism for this in the current
PRISM. Having some support for that would surely be useful.

Depending on your actual use case, the following might work however:

You can add another 'module' to your PRISM source file, which
synchronizes with the other modules to implement the adversary.

This requires that (1) for the rest of your system, there is no "local
nondeterminism", i.e., that, for each state and module, for a given
action name at most a single command with that action is enabled and
that there are no [] commands.

So:

[a] s=0 -> ...
[a] s=1 -> ...
[b] true -> ...

would be fine (as state + action uniquely determines a single command
per module), but

[a] s=0 -> ...
[a] s>=0 -> ...
[] s=0 -> ...

would not be.

Then, in your adversary module, you can force the rest of the system to
behave according to the adversary, e.g.,

[a] s=0 -> true;
[b] s=1 -> true;

to select [a] for s=0 and [b] for s=1.

If you need memory in the adversary, you can model that as well. You
have to take care that all action names occur in your adversary model,
so that no action in the rest of the system can happen without the
adversary's consent. E.g., to always block the [c] action, you can
add the following command:

[c] false -> true;


For another direction, if I recall correctly, the PRISM-games extension
of PRISM has some support for loading adversaries. It might be worthwile
to look there as well.

Cheers,
Joachim