How to use prism tool to build MDP model?

7 views
Skip to first unread message

tan wenzhao

unread,
Mar 24, 2022, 6:35:06 PMMar 24
to PRISM model checker
I have encountered such a problem. I need to build a simple MDP model. After reading your user manual, I still feel very confused. If a state has two corresponding actions, how can I express it in the model? Eg. for state S1, the agent has two decision actions: left and right. How can I express it in the model?

Dave Parker

unread,
Mar 31, 2022, 4:53:04 PMMar 31
to prismmod...@googlegroups.com, tan wenzhao
Hi Wenzhao,

In general, you might find it helpful to work through some of the
tutorials. See here:

http://www.prismmodelchecker.org/tutorial/

For a very small example of the kind of MDP you mention, see also the
files here:

https://prismmodelchecker.org/files/stratsynth/

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/6c468d88-6a61-4070-88f2-269b0d8e6167n%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/6c468d88-6a61-4070-88f2-269b0d8e6167n%40googlegroups.com?utm_medium=email&utm_source=footer>.
Reply all
Reply to author
Forward
0 new messages