Imprecise result in simple POMDP?

[Alberto Lluch Lafuente]

Hi,

I was playing around with this model

/prism-4.7-src/prism-examples/pomdps/gridworld/3x3grid.prism

and I got some unexpected results.

I have boiled down the problem to a minimal POMDP, with just 2 states (I am copying below the model, attaching the files, and the exported diagram).

The property I consider is 

Pmax=? [ F x=1 ]

The POMDP has perfect information (the only variable of the model is observable). I would expect to obtain 1 as a result (which indeed I get if I transform the model into an MDP).

However, PRISM (Version: 4.7.dev) returns

Result: 0.5 (+/- 0.5; rel err 1.0)

I have tried to find some parameter to increase precision with no success. Does anyone have a hint?

Thanks in advance,

Alberto

=========

PROPERTY

=========

Pmax=? [ F x=1 ]

======

MODEL

======

pomdp

observables
    x
endobservables

module TESTPOPMDP

    x : [0..1] init 0;
   
        // stay or move from 0
        [stay]  x=0 -> (x'=1) ;
        [move]  x=0 -> (x'=0) ;

        // stay at 1
        [done] x=1 -> true;

endmodule

[Dave Parker]

Hi Alberto,

Thanks for flagging this. It looks like a bug actually. POMDPs are
solved by first computing an upper bound of the value, then generating
and solving a corresponding policy to get a lower bound. In this
instance the upper bound is correct and exact (1.0) but the wrong policy
is generated (one that loops in state 0), leading to a lower bound of
0.0 and hence the incorrect results.

Are you compiling PRISM from source? I can push a fix.

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/b28027a9-c1c1-47a6-bc72-eca057b84248n%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/b28027a9-c1c1-47a6-bc72-eca057b84248n%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Alberto Lluch Lafuente]

Great, thanks!

[Alberto Lluch Lafuente]

Hi Dave, 

I tried with the latest github version and the problem seems to still be there.

Did you push the fix?

Thanks,

Alberto