Will synthesis of DTMC for given (PO)MDP be included in official PRISM?

[proteusGIT]

Hi,

I have playing around with the POMDP synthesis implementation RTS-POPTAS. I also had a look at NFM18.

Will these be included in PRISM eventually? I believe to have resolved my previous issue with that contribution in the meantime.

Best.

[gethin-norman]

These are generated by exporting the strategy (or adversary) which is essentially the DTMC (although it includes the choices in all the states of the MDP) see:

http://www.prismmodelchecker.org/manual/RunningPRISM/Adversaries

In the case of POMDPs this is a little bit difficult to understand as it is a strategy of the belief MDP. The format of each line of the output is:

state number:(values of visible variables),[belief probabilities for values of hidden variables] & no-det number/probability @ (new values of visible variables) > new state number:(new values of visible variables),[new belief probabilities for values of hidden variables]

However, a student developed a prototype tool which generates a graphical representation of the strategy (it generates a dot file). It is available on github:

https://github.com/munroa/PRISM-POMDP-Analyser

thanks

Gethin

On 4 Jan 2021, at 11:23, proteusGIT notifications@github.com wrote:

Hi,

I have playing around with the POMDP synthesis implementation RTS-POPTAS. However, I expected that a DTMC would be produced describing the optimal strategy. The output also mentions the generation of such a DTMC:

$ bin/prism examples-distr/maze.prism examples-distr/maze.props (..) Strategy DTMC: States: 13 (1 initial) Transitions: 21 Choices: 12 Max/avg: 1/0.92 (..)

But I wonder whether it is also possible to export this DTMC using some prism parameters.

I also had a look at NFM18 but there are also no explanations on how to export the resulting DTMCs.

Best.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[davexparker]

Hi @proteusGIT. As Gethin says, you can use -exportadv to get a view of the model used to synthesise a POMDP strategy. If you are interested, there is a newer version of the code, hopefully to be integrated into the main PRISM release quite soon:

https://github.com/davexparker/prism/tree/pomdps

If you use -exportadv on that version, you get a standard PRISM .tra file representing the model, and also a dot file which annotates with info about the belief states. Here's part of an example:

[davexparker]

Hi @proteusGIT. DTMC policy export for POMDPs is now in the main codebase and also the public release. Use:

prism pomdp.prism pomdp.props -exportadv adv.dot