pomdp unexpected result

[Mridu Nanda]

Hi,

I wrote a simple die roll pomdp program as follows:

pomdp

observables s, g endobservables

module die

    // local state
    s : [0..4] init 0;
    // value of the die
    d : [0..6] init 0;
    // attacker's guess;
    g : [0..6] init 0;
   
    [throw] s = 0 -> 1/6 : (d' = 1) & (s' = 1)
            + 1/6 : (d' = 2) & (s' = 1)
            + 1/6 : (d' = 3) & (s' = 1)
            + 1/6 : (d' = 4) & (s' = 1)
            + 1/6 : (d' = 5) & (s' = 1)
            + 1/6 : (d' = 6) & (s' = 1);
    [guess_1] s = 1 -> (g' = 1) & (s' = 2);
    [guess_2] s = 1 -> (g' = 2) & (s' = 2);
    [guess_3] s = 1 -> (g' = 3) & (s' = 2);
    [guess_4] s = 1 -> (g' = 4) & (s' = 2);
    [guess_5] s = 1 -> (g' = 5) & (s' = 2);
    [guess_6] s = 1 -> (g' = 6) & (s' = 2);

    [] s = 2 & (d = g) -> (s' = 3);
    [] s = 2 & (d != g) -> (s' = 4);

    [win] s = 3 -> true;
    [lose] s = 4 -> true;
   
endmodule

I wanted to check the following property:

Pmax=? [F s=3]

I expected that Pmax will be reported as 0.16666, since there is a 1/6 chance that we will correctly guess the result of rolling a fair die (assuming we cannot see the fair die). 

However, once I ran the model checker I found that Pmax = 0.18333. In particular, this number was the average of: 

Result bounds: [0.16666666666666663,0.19999999999999984]. 

How should I interpret the result bounds, and the actual number reported by the model checker? I would really appreciate some intuition behind what the POMDP simulation is doing. 

Thanks in advance,

Mridu

[Dave Parker]

Hi Mridu,

The method for solving POMDPs is approximate: it gives you a lower and
upper bound on the result. That's why you see "Result bounds:
[0.16666666666666663,0.19999999999999984]" for your model.

For Pmax=? properties, the upper bound is a calculated upper bound on
the real maximum value, and the lower bound is a value determined from
solving an actual POMDP policy.

In general, you can improve accuracy, at the cost of more expensive
numerical solution, by increasing the -gridresolution parameter. But for
this model, it seems you run out of memory before getting any gain in
accuracy.

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 view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/05fe7b15-b15c-474e-96eb-4d87433cdc2an%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/05fe7b15-b15c-474e-96eb-4d87433cdc2an%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Mridu Nanda]

Hi David,

Thanks for your response! I am still a bit confused.. Can you explain the intuition for the upper bound? What exactly do you mean by the real maximum value? Similarly, could you please clarify what policy is being used to determine the lower bound? Is there a paper and/or documentation you could point me towards to help understand this better (e.g., is this a PRISM specific implementation or does this apply to POMDP's in general)?

The reason I am asking this question is because I am trying to understand the difference between using POMDP versus using MDPs "in a smart way" to hide the variables. In particular, I am trying to hide certain variables from the attacker. If I want to do this in an MDP, I can force the attacker to make the guess, before the die is rolled, as done in the below example:

mdp

module die

    // local state
    s : [0..4] init 0;
    // value of the die
    d : [0..6] init 0;
    // attacker's guess;
    g : [0..6] init 0;

    [guess_1] s = 0 -> (g' = 1) & (s' = 1);
    [guess_2] s = 0 -> (g' = 2) & (s' = 1);
    [guess_3] s = 0 -> (g' = 3) & (s' = 1);
    [guess_4] s = 0 -> (g' = 4) & (s' = 1);
    [guess_5] s = 0 -> (g' = 5) & (s' = 1);
    [guess_6] s = 0 -> (g' = 6) & (s' = 1);

    [throw] s = 1  -> 1/6 : (d' = 1) & (s' = 2)
            + 1/6 : (d' = 2) & (s' = 2)
            + 1/6 : (d' = 3) & (s' = 2)
            + 1/6 : (d' = 4) & (s' = 2)
            + 1/6 : (d' = 5) & (s' = 2)
            + 1/6 : (d' = 6) & (s' = 2);

   
    [] s = 2 & (d = g) -> (s' = 3);
    [] s = 2 & (d != g) -> (s' = 4);

    [win] s = 3 -> true;
    [lose] s = 4 -> true;
   
endmodule

This gives me the expected result of 1/6. Is this way of encoding the MDP logically equivalent to hiding the "d" variable in the POMDP? I think it is, but wanted a sanity check!

Thanks for your help!

Mridu

[Mridu Nanda]

Sorry, I meant to say Hi **Dave. My mistake!

On Apr 26, 2022, at 1:29 PM, Mridu Nanda <mridu...@gmail.com> wrote:

Hi David,

You received this message because you are subscribed to a topic in the Google Groups "PRISM model checker" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/prismmodelchecker/MUzXCNbzflk/unsubscribe.
To unsubscribe from this group and all its topics, send an email to prismmodelchec...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/prismmodelchecker/7b36d725-a057-4d52-a273-47522bc3b5dcn%40googlegroups.com.