PRISM-games: generated strategies do not fulfill verified property

[Georg Schuppe]

Hello,

I have created a very concise example to illustrate my problem and hope to receive some clarification, explanation or even a solution here:

I run PRISM-games 3.0, compiled from source, all tests are running and everything seems to be setup correctly.

I created a very simple stochastic game starting from a state x=0, where player 1 can choose to advance the state to either x=1 or x=2, and player 2 does nothing but revert it back to x=0. The model file is attached.

In this very simple "game", I would like to verify that player 1 can reach x=2: 

<< p1 >> P>=1 [F x=2]

Verification of this property promptly returns a positive answer, as expected. If I modify the game such that player 2 could prevent reaching the desired state, verification concludes negatively, as expected.

The problem arises when I generate a strategy. The strategy is memoryless and deterministic, as expected, but it instructs player1 to choose the action that transitions to x=1 with probability 1 instead of simply going to x=2. Also, when verifying with the generated strategy, the property is not satisfiable anymore.

I understand that this is due to the lack of a bound on the "eventually" operator. If I add a bound, the generated strategy eventually chooses to go to x=2, but it always goes to the accepting state on the very last possible moment.

Is it possible to generate strategies that actually solve such reachability problems in simulation without specifying a bound?

Best,

Georg

[Dave Parker]

Hi Georg,

Thanks for reporting this. I looked into it and it is indeed a bug. The
presence of loops (in your example, the possibility to cycle between
states 0 and 1) requires careful handling when generating optimal
strategies. We deal with this correctly for the simpler model of MDPs,
but it seems that an error slipped through for stochastic games. I will
add a fix and push it. Did you compile PRISM-games from source? (if yes,
it will not be too hard to get a corrcted version).

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/0ccdcc0f-880c-45cc-bcc1-fc7893200dcdn%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/0ccdcc0f-880c-45cc-bcc1-fc7893200dcdn%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Georg Schuppe]

Hello Dave,

thanks for responding so fast and even fixing the problem. That is beyond my expectations. Yes, I compiled the 3.0 source release downloaded from the website. Once the fix is pushed to github, I will try it out immediately. This is very helpful for my research, so thanks again!

Best,

Georg

[Georg Schuppe]

Hi Dave,

I don't want to be a bother, but do you have any word on when you will push the fix? It would be greatly appreciated!

Best,

Georg

[Dave Parker]

No problem Georg and sorry for the delay. I had tried to apply a broader
improvement to the strategy generation, but there were some issues. So
I've just reverted to a simple fix. It is now pushed to GitHub:

https://github.com/prismmodelchecker/prism-games

It resolves the bug on the simple example you posted here (which is in
fact just an MDP), so it would be good to hear if the problem is now
resolved on your more complex example.

Best wishes,

Dave

> <https://groups.google.com/d/msgid/prismmodelchecker/0ccdcc0f-880c-45cc-bcc1-fc7893200dcdn%40googlegroups.com?utm_medium=email&utm_source=footer
> <https://groups.google.com/d/msgid/prismmodelchecker/0ccdcc0f-880c-45cc-bcc1-fc7893200dcdn%40googlegroups.com?utm_medium=email&utm_source=footer>>.

>
>
> --
> 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/327993c8-4cbc-4973-93a9-40491051d0e3n%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/327993c8-4cbc-4973-93a9-40491051d0e3n%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Georg Schuppe]

Hi Dave,

the fix worked and now my agents finally take the last step into the desired states. Thank you again for the great support, PRISM-games has been a delight to work with so far!

Best,

Georg