New to Prism Model Checker

[Debapriyay Mukhopadhyay]

Hi All,
I am new to Prism Model Checker. First of all, can anybody please
provide me with the reference where I will get a brief reference of
the PCTL property and how properties can be captured in PCTL.
I was trying with the first example.

mdp

module M1

x : [0..2] init 0;

[] x=0 -> 0.8:(x'=0) + 0.2:(x'=1);
[] x=1 & y!=2 -> (x'=2);
[] x=2 -> 0.5:(x'=2) + 0.5:(x'=0);

endmodule

module M2

y : [0..2] init 0;

[] y=0 -> 0.8:(y'=0) + 0.2:(y'=1);
[] y=1 & x!=2 -> (y'=2);
[] y=2 -> 0.5:(y'=2) + 0.5:(y'=0);

endmodule

I was trying with two properties ...
Pmin=?[true U (x=2) & (y!=2)] : what I wanted to capture here is what
is the min probability that M1 has enetered into CS, but M2 not. This
value is coming as 0.

Another property is like this.
Pmin=?[true U (x=2) & (y=2)]: what I wanted to capture here is what is
the minimum probability that both M1 and M2 entered into CS same time.
This value is also coming as 0.

How can both this be possible. I must be doing something wrong. Are
the properties correct. How to justify the P_min values that I am
getting for the above two cases.
Please, help.

Thanks.
Regards
Debapriyay Mukhopadhyay

[Mark Kattenbelt]

Hi Debapriyay,

> I am new to Prism Model Checker. First of all, can anybody please
> provide me with the reference where I will get a brief reference of
> the PCTL property and how properties can be captured in PCTL.

The manual has some explanation:
http://www.prismmodelchecker.org/manual/PropertySpecification/

A more formal source of PCTL over MDPs is this paper:
http://www.prismmodelchecker.org/manual/Main/References#BdA95

The "min" in "Pmin" indicates you are computing the minimum probability
of the path formula inside the square brackets for all possible
schedulers of the MDP. In your case, as M1 and M2 by themselves don't
contain non-determinism this is the minimum probability over all
possible schedulings of M1 || M2.

If you reconsider [ true U (x=2) & (y!=2) ] then a feasible scheduling
of M1 || M2 is one where M2 moves continuously, but M1 does not move. In
this case, x=2 never becomes true and the probability is zero. This also
explains why [true U (x=2) & (y=2)] has a minimum probability of zero.

Note that the scheduling where one module moves continuously is not
necessarily fair, but by default PRISM does not deal with fairness. Note
that PRISM is capable of verifying under some fairness assumptions, see:
http://www.prismmodelchecker.org/manual/ConfiguringPRISM/OtherOptions

Kind regards,

Mark

[Debapriyay Mukhopadhyay]

Dear Mark,
Thanks for your reply and help. I will go through the links that
you have sent for studying PCTL bit more. And also the fairness
assumptions that you mentioned in your mail.
But apart from all this, I still have a few questions and
confusions, which are embedded below.

" The "min" in "Pmin" indicates you are computing the minimum
probability
of the path formula inside the square brackets for all possible
schedulers of the MDP. In your case, as M1 and M2 by themselves don't
contain non-determinism this is the minimum probability over all
possible schedulings of M1 || M2."

----- How can then one apply non-determinism on M1 and M2? This non-
determinism will dictate (I guess) the way M1 or M2 in the MDP should
be scheduled. But, if I do a simulation then I see both modules are
making transitions from one state to another. So, is it true that
simulation doesn't show
all possible schedulings of M1 || M2. (Atleast, I have checked upto
20000 steps).

"If you reconsider [ true U (x=2) & (y!=2) ] then a feasible
scheduling
of M1 || M2 is one where M2 moves continuously, but M1 does not move.
In
this case, x=2 never becomes true and the probability is zero. This
also
explains why [true U (x=2) & (y=2)] has a minimum probability of
zero."

------ Does the property has anything to do with the scheduling of M1
|| M2. What my confusion here is the scheduling of models being
controlled by the property. Another question is, if say for example, I
have two modules M1 and M2, and I would like to enforce an alternating
turn based game then how can this scheduling be ensured.

Atleast, these are the questions I have now.
Thanks.

Regards
Debapriyay Mukhopadhyay

[Mark Kattenbelt]

Hi,

> ----- How can then one apply non-determinism on M1 and M2? This non-
> determinism will dictate (I guess) the way M1 or M2 in the MDP should
> be scheduled. But, if I do a simulation then I see both modules are
> making transitions from one state to another. So, is it true that
> simulation doesn't show
> all possible schedulings of M1 || M2. (Atleast, I have checked upto
> 20000 steps).

I am not sure I follow your question. Your model has non-determinism
-- multiple (asynchronous) commands are enabled at the same time
(considering all modules). If you do a simulation the simulator picks
a particular scheduling at random -- please also consider reading this
thread:

http://groups.google.com/group/prismmodelchecker/browse_thread/thread/be8726e14ac3a5c2/bfe68fc148accb74#bfe68fc148accb74

You should be able to achieve any scheduling in the simulator by
picking the appropriate step manually. Note that using the simulator
for debugging purposes is fine, but when it comes to approximating
probabilities it probably won't behave as expected (see this previous
thread).

> ------ Does the property has anything to do with the scheduling of M1
> || M2. What my confusion here is the scheduling of models being
> controlled by the property. Another question is, if say for example, I
> have two modules M1 and M2, and I would like to enforce an alternating
> turn based game then how can this scheduling be ensured.

The property does not control the scheduling. Perhaps this explanation
helps: for each scheduling the probability of the path formula is
fixed. However, in the presence of non-determinism there is more than
one schedulers. Hence, rather than one probability there are many. The
way we deal with this is by giving you the option to choose the
minimum or the maximum probability.

If you want to enforce a scheduler you need to remove all non-
determinism. Probably a sensible way to do this is by adding a module
that acts as a "scheduler", synchronising with the other modules. A
similar method is applied in this tutorial for continuous-time models:

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

I am not sure this will accomplish what you need (i.e. a turn-based
game). However, if you need more information, please ask!

Kind regards,

Mark

[Debapriyay Mukhopadhyay]

Hi Mark,
Thanks for your reply. I think, I have understood the scenario.
If I get into any further confusion, I will let you know.
Thanks.

Regards
Debapriyay

On Apr 26, 6:58 pm, Mark Kattenbelt <mark.kattenb...@comlab.ox.ac.uk>
wrote:

> Hi,
>
> > ----- How can then one apply non-determinism on M1 and M2? This non-
> > determinism will dictate (I guess) the way M1 or M2 in the MDP should
> > be scheduled. But, if I do a simulation then I see both modules are
> > making transitions from one state to another. So, is it true that
> > simulation doesn't show
> > all possible schedulings of M1 || M2. (Atleast, I have checked upto
> > 20000 steps).
>
> I am not sure I follow your question. Your model has non-determinism
> -- multiple (asynchronous) commands are enabled at the same time
> (considering all modules). If you do a simulation the simulator picks
> a particular scheduling at random -- please also consider reading this
> thread:
>

> http://groups.google.com/group/prismmodelchecker/browse_thread/thread...