How to use prism tool to build MDP model?

Skip to first unread message

tan wenzhao

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

Mar 31, 2022, 4:53:04 PMMar 31
to, tan wenzhao
Hi Wenzhao,

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

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

Best wishes,

> --
> 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
> <>.
> To view this discussion on the web, visit
> <>.
Reply all
Reply to author
0 new messages