POMDP strategy extraction

49 views
Skip to first unread message

sebastia...@gmail.com

unread,
Mar 8, 2018, 4:07:04 AM3/8/18
to PRISM model checker
Dear,

is there a possibility to extract strategies from PRISM POMDP?

Best,
Sebastian

Gethin Norman

unread,
Mar 8, 2018, 4:29:39 AM3/8/18
to prismmod...@googlegroups.com, Gethin Norman
Sebastian,

you can extract strategies with the “-exportadv” switch from the command line. This is the strategy for the belief MDP and unfortunately the current output is not the easiest to understand.

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

If you have any questions or problems, let me know and I will try and help.

thanks

Gethin
> --
> 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.
> Visit this group at https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

Seungoh

unread,
Dec 22, 2023, 8:11:22 AM12/22/23
to PRISM model checker
Hi,

It seems that a POMDP strategy cannot be exported with -exportadv anymore. When I try -exportstrat, only the graphical dot format gives complete data, but the strategy itself is not easily readable by a machine from that graphical form. On the other hand, the "induced" format says nothing about the meaning of the agent states and the "actions" format says nothing about probabilistic branching (examples for maze.prism below).

How can I get a complete, machine-readable adversary for POMDP?

Thanks,
Seungoh

induced:
12 12 21
0 0 1 0.2
0 0 2 0.3
0 0 3 0.1
0 0 4 0.1
0 0 5 0.2
0 0 6 0.1
1 0 7 1 north
2 0 3 0.3333333333333333 north
2 0 4 0.3333333333333333 north
2 0 6 0.3333333333333333 north
3 0 8 1 west
4 0 9 1 south
5 0 4 0.5 west
5 0 6 0.5 west
6 0 10 1 east
7 0 3 0.5 north
7 0 6 0.5 north
8 0 4 1 west
9 0 11 1 south
10 0 4 1 east
11 0 11 1

actions:
(false,false,false,false,false),1.0:(-1):
(true,true,false,true,false),0.5:(8)+0.5:(9):north
(true,true,false,false,false),0.3333333333333333:(5)+0.3333333333333333:(6)+0.3333333333333333:(7):north
(false,true,true,false,false),1.0:(4):west
(false,false,true,false,false),1.0:(2):south
(false,false,true,true,false),0.5:(1)+0.5:(3):west
(true,false,true,false,false),1.0:(0):east
(true,true,false,false,false),0.5:(5)+0.5:(7):north
(false,false,true,true,false),1.0:(3):west
(true,true,false,false,false),1.0:(6):south
(false,false,true,true,false),1.0:(1):east

Seungoh

unread,
Dec 22, 2023, 8:56:08 AM12/22/23
to PRISM model checker
Hi,

I guess that those two files need to be read together and the 1st and 3rd column of "induced" is an action number.

Thanks,
Seungoh

Dave Parker

unread,
Dec 22, 2023, 9:09:45 AM12/22/23
to prismmod...@googlegroups.com, Seungoh
Hi Seungoh,

We've tried to make this consistent with the strategy generation for
other models. So the model ("induced") version is in a form that can be
read back into PRISM, and the Dot file version has additional
annotations for visual inspection.

I am guessing that you are trying to get machine readable details of the
belief state corresponding to each state index in the .tra file? Are you
able to get what you need by looking at the actions file too?

Best wishes,

Dave
> <https://groups.google.com/group/prismmodelchecker>.
> > For more options, visit https://groups.google.com/d/optout
> <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
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/b627275a-826e-4d49-b490-0893d641dab7n%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/b627275a-826e-4d49-b490-0893d641dab7n%40googlegroups.com?utm_medium=email&utm_source=footer>.
Reply all
Reply to author
Forward
0 new messages