Probability queries for non-determistic transition systems

[Derek Egolf]

Hi,

I have a model with actions whose pre-conditions are not disjoint. But for each action and each state satisfying the guard of that action, there is exactly one successor state. There are no explicit probabilities in my model.

When I perform a P=? query, and there exists a reachable state that satisfies the guards of action A1 and A2, does prism assume that A1 and A2 are taken with uniform probability at that state?

Thank you for your help.

[Dave Parker]

Hi Derek,

Is this in the context of a single PRISM module? Because, if not,
actions can cause modules to syncronise, which complicates the question.

But, if yes, then commands (in a discrete time Markov chain, which I
assume is your model type), are indeed selected uniformly at random.
This is referred to as "local nondeterminism"; see the bottom paragraph
of this page:

https://www.prismmodelchecker.org/manual/ThePRISMLanguage/LocalNondeterminism

You can check what your model actually does using the simulator:

https://www.prismmodelchecker.org/manual/RunningPRISM/DebuggingModelsWithTheSimulator

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, visit https://groups.google.com/d/msgid/
> prismmodelchecker/3ddf91da-a149-4607-
> afe7-2a278c687fe2n%40googlegroups.com <https://groups.google.com/d/
> msgid/prismmodelchecker/3ddf91da-a149-4607-
> afe7-2a278c687fe2n%40googlegroups.com?utm_medium=email&utm_source=footer>.