Questions about exportadv

[Jin Ge]

I have some questions with multi-objective adversary generation:

=============Model==================

mdp 

 module ScalarExample 

 x : [0..2] init 2; 

[k0] x=2 -> 0.9:(x'=1)+0.1:(x'=0);

[k1] x=2 -> 0.5:(x'=1)+0.5:(x'=0);

[k2] x=2 -> 0.1:(x'=1)+0.9:(x'=0);

[k1] x=1 -> 1:(x'=0);

endmodule

rewards "Costs"

[k0] true : x*x/2;

[k1] true : x*x;

[k2] true : 4*x*x;

endrewards

===============================

1. I wish to choose the action that has a cost no larger than 10 while maximizing the probability of reaching x=0.

========property=======

multi(P max=?[F x=0],R<=10[C<=2])

=====================

The generated adversary is:

================

3 3

0 0 2 1

1 0 0 0.1

1 0 2 0.9

==========

It seems that instead of choosing among the given k0/k1/k2, the adversary invents x=0 -> (x'=2), and x=1 -> 0.1:(x'=0)+0.9:(x'=2). Did I do something wrong here?

2. I could avoid the multi( , ) by first generating all possible adversaries satisfying a certain property, and then zoom in on the maximizing one, but it seems -exportadv only gives a random action among the satisfying actions?

====Property=====

R <=20[F x=0]

===============

All the actions k0/k1/k2 would work, but only k2 is shown:

======Result======

3 3

1 0 0 1 k1

2 0 0 0.9 k2

2 0 1 0.1 k2

================

3. Also I would expect k0/k1 be chosen when 

====Property=====

R <=15[F x=0]

===============

But -exportadv complains about false result in verification and the adversary remains k2.

===============

3 3

1 0 0 1 k1

2 0 0 0.9 k2

2 0 1 0.1 k2

===============

Anything I misunderstood here?

Thank you very much for any reply!

[Joachim Klein]

Hi,

> 1. I wish to choose the action that has a cost no larger than 10 while
> maximizing the probability of reaching x=0.
> ========property=======
> multi(P max=?[F x=0],R<=10[C<=2])
> =====================
>
> The generated adversary is:
> ================
> 3 3
> 0 0 2 1
> 1 0 0 0.1
> 1 0 2 0.9
> ==========
> It seems that instead of choosing among the given k0/k1/k2, the
> adversary invents x=0 -> (x'=2), and x=1 -> 0.1:(x'=0)+0.9:(x'=2). Did I
> do something wrong here?

It's a bit confusing: The states of the generated adversary are of a
product of the original MDP with deterministic automata (for handling
each of the path formulas in the P operators). You can have a look at
the product state space using the
-exportprodstates prod.sta
switch. There you can see which states in the adversary export
correspond to which states in the original model.

This looks something like this:

(_da,x)
0:(0,1)
1:(0,2)
2:(1,0)

So, the second component corresponds to the x value.

I guess it would be helpful to also display the action names in the
adversary, I have opened

https://github.com/prismmodelchecker/prism/issues/8

for that.

> 2. I could avoid the multi( , ) by first generating all possible
> adversaries satisfying a certain property, and then zoom in on the
> maximizing one, but it seems -exportadv only gives a random action among
> the satisfying actions?

Yes, if there are more than one possible adversary, adversary generation
will generally only return one of them, arbitrarily.

> 3. Also I would expect k0/k1 be chosen when
> ====Property=====
> R <=15[F x=0]
> ===============
> But -exportadv complains about false result in verification and the
> adversary remains k2.
> ===============
> 3 3
> 1 0 0 1 k1
> 2 0 0 0.9 k2
> 2 0 1 0.1 k2
> ===============
> Anything I misunderstood here?

R<=15[ F x=0 ] asks if the maximising adversary will have an expected
reward <=15. If you ask for Rmax=?[ F x=0 ] you'll get the result

> Result: 16.1 (value in the initial state)

Thus, you get the false result (for your question). The adversary is
generated for the maximising adversary, regardless of the bound.


Cheers,
Joachim

[Jin Ge]

Thank you very much for the reply! It helps a lot.

In (1), the result makes sense now. PRISM chose action k2 and totally ignored the reward bound 'R<=10'. The result of (3) also shows that PRISM does not eat 'R<=10'.

So the adversary generation only works for 'Pmax/min=?' and 'R min/max=?', and cannot generate a max/min adversary with certain bounds?

[Dave Parker]

Hi Jin,

Let me clarify (or confuse) matters further regarding your question (1).
PRISM has two distinct methods for checking these multi-objective
properties: "linear programming" and "value iteration", each with
different limitations. Currently, the latter is the default, where
possible, but we only have adversary generation implemented for the
former. Unfortunately, it seems that the value iteration method
currently outputs some intermediate adversaries used during model
checking. So the adversary you have seen is actually not the correct one
for your query (multi(P max=?[F x=0],R<=10[C<=2])).

You can export the correct one by making some changes. First, you will
need to ask PRISM to use the linear programming method, by adding the
switch -lp. However, this does not support time-bounded properties such
as C<=2. The solution is to change the property to:

multi(P max=?[F x=0],R<=10[C])

which uses the long-run cumulated reward, rather than the reward
cumulated over 2 steps. To make that consistent with the model you had
before, change the action of the transition from state x=1 to something
other than k1 (say, k3) to make sure there is no reward attached, and
there are no extra rewards cumulated after 2 steps. The adversary
exported, when using the -lp switch is then:

3 ?
0 2 1 k3
1 0 0.0571429 k2
1 2 0.514286 k2
1 0 0.385714 k0
1 2 0.0428571 k0
2 2 1 _ec

This has the complication mentioned by Joachim that the adversary is
over a product model. Using -exportprodstates and mapping the state
indices above to their value of variable x, you get:

2 1 0.0571429 k2
2 0 0.514286 k2
2 1 0.385714 k0
2 0 0.0428571 k0
1 0 1 k3
0 0 1 _ec

This reveals an additional complication that, if you want to maximise
the probability of reaching x=0, whist keeping the expected cumulative
reward at most 10, the optimal adversary is actually a randomised one.
From the above, you can deduce that, from state x=2, it picks the k0
action with probability 0.4285711 and the k2 action with probability
0.5714289. In fact, the optimal adversary for such constrained queries
(maximising or minimising one objective, whilst putting a bound on the
other) is very often randomised.

Best wishes,

Dave

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To post to this group, send email to prismmod...@googlegroups.com
> <mailto:prismmod...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

[Dave Parker]

One further thing: the alternative model checking query I proposed
showed up a small bug in PRISM, which I have now fixed. So you'll need
to make sure you are using the very latest code to get this to work:

http://www.prismmodelchecker.org/wiki/Developers/GettingTheSource

Best wishes,

Dave

[Jin Ge]

Hi Dave,

Thanks a lot for the reply! I tried out the new version from GitHub <https://github.com/prismmodelchecker/prism-svn>, but when I run 'make' I got error messages:

make[1]: Entering directory `/home/jing/Dropbox/prism-svn-master/prism/src/jdd'

(cd ..; javac -encoding UTF8 -sourcepath jdd/../../src -classpath "jdd/../../classes:jdd/../../lib/*" -d jdd/../../classes jdd/DebugJDD.java)

jdd/../../src/prism/Model.java:69: error: illegal start of type

default boolean hasLabelDD(String label)

^

jdd/../../src/prism/Model.java:69: error: = expected

default boolean hasLabelDD(String label)

       ^

jdd/../../src/prism/Model.java:69: error: ';' expected

default boolean hasLabelDD(String label)

              ^

... ...

Note: Some input files use or override a deprecated API.

Note: Recompile with -Xlint:deprecation for details.

Note: Some input files use unchecked or unsafe operations.

Note: Recompile with -Xlint:unchecked for details.

100 errors

make[1]: *** [../../classes/jdd/DebugJDD.class] Error 1

make[1]: Leaving directory `/home/jing/Dropbox/prism-svn-master/prism/src/jdd'

make: *** [make_dirs] Error 1

Any suggestions about how to solve this? Thanks a lot!

Best,

Jin

>> <mailto:prismmodelchecker+unsub...@googlegroups.com>.

[Marcin Copik]

Jin,

default is a method keyword which has been introduced in Java 8, I believe. Recently Dave announced that PRISM is moving to Java 8:
https://groups.google.com/forum/#!topic/prismmodelchecker-dev/JEthkRiYVxc

You need a JDK in version 1.8 at least.

Best regards,

Marcin

>> an email to prismmodelchec...@googlegroups.com
>> <mailto:prismmodelchec...@googlegroups.com>.

>> To post to this group, send email to prismmod...@googlegroups.com
>> <mailto:prismmod...@googlegroups.com>.

>> Visit this group at https://groups.google.com/group/prismmodelchecker.
>> For more options, visit https://groups.google.com/d/optout.
>

--

You received this message because you are subscribed to the Google Groups "PRISM model checker" group.

To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchec...@googlegroups.com.
To post to this group, send email to prismmod...@googlegroups.com.

[Jin Ge]

Hi Marcin,

Problem solved. Thanks a lot!

Best,

Jin

>> an email to prismmodelchec...@googlegroups.com
>> <mailto:prismmodelchecker+unsub...@googlegroups.com>.

>> To post to this group, send email to prismmod...@googlegroups.com
>> <mailto:prismmod...@googlegroups.com>.