The value of Pmin is different when I execute my MDP model with simulator ? Would someone please explain ?

[Tushar Deshpande]

Hi,

I'm a graduate student from State University of
New York at Stony Brook.

I'm using Prism to perform a model checking task.

I've written a MDP model in Prism.
Also, I wrote specified a condition that describes
the final state in .pctl file.

The condition is of the form Pmin=? [ F my_condition ]
Pmin is the minimum probability when my_condition
becomes true.

I executed the model with model-checker.
I used following command line
prism -fixdl my_model.nm my_model_check.pctl

To my surprise, I got 0.0 as the value for Pmin.

Then, I ran the same model with simulaor.
I used following command.
prism -fixdl -sim my_model.nm my_model_check.pctl

Now, I got 0.278 as value for Pmin, which I expected.

I'm unable to explain why there's a difference between
the answers that I got without simulation and with
simulation.

There're some deadlock states in the model. But, these
deadlocks states are expected.

Would someone please help me to explain these results ?

Also, it would really help if you help me to interpret
following lines in the output that I got after model checking ?

Model checking: Pmin=? [ F my_condition ]

Prob0E: 4 iterations in 0.02 seconds (average 0.005000, setup 0.00)

Prob1A: 2 iterations in 0.02 seconds (average 0.008000, setup 0.00)

yes = 28, no = 63, maybe = 4

Particularly, I would like to know, what do 'yes', 'no'
and 'maybe' indicate ?

1) Here's the output that I get when I run model
without using a simulator.

PRISM
=====

Version: 3.2
Date: Sun Mar 29 00:56:37 EST 2009
Hostname: home
Command line: prism -fixdl my_model.nm my_model_check.pctl

Parsing model file "my_model.nm"...

Parsing properties file "my_model_check.pctl"...

1 PCTL property:
(1) Pmin=? [ F my_condition ]

-------------------------------------------

Building model...

Computing reachable states...

Reachability: 7 iterations in 1.38 seconds (average 0.197714, setup
0.00)

Time for model construction: 30.672 seconds.

Type: Nondeterministic (MDP)
Modules: module_1 module_2....module_n
Variables: var_1 var_2.....var_n

Warning: 32 deadlock states detected; adding self-loops in these
states...

States: 95 (1 initial)
Transitions: 186
Choices: 144

Transition matrix: 5113 nodes (3 terminal), 186 minterms, vars: 142r/
142c/4nd

-------------------------------------------

Model checking: Pmin=? [ F my_condition ]

Prob0E: 4 iterations in 0.02 seconds (average 0.005000, setup 0.00)

Prob1A: 2 iterations in 0.02 seconds (average 0.008000, setup 0.00)

yes = 28, no = 63, maybe = 4

Computing remaining probabilities...

Building hybrid MTBDD matrices... [nm=2, levels=142, nodes=915] [21.4
KB]
Adding sparse bits... [levels=142-142, num=2, compact=2/2] [0.2 KB]
Creating vector for yes... [dist=2, compact] [0.2 KB]
Allocating iteration vectors... [3 x 0.7 KB]
TOTAL: [24.1 KB]

Starting iterations...

Iterative method: 3 iterations in 0.00 seconds (average 0.000000,
setup 0.00)

Time for model checking: 0.045 seconds.

Result: 0.0


2) Here's the output that I get when I run model
with a simulator.

PRISM
=====

Version: 3.2
Date: Sun Mar 29 00:55:48 EST 2009
Hostname: home
Command line: prism -fixdl -sim my_model.nm my_model_check.pctl

Parsing model file "my_model.nm"...

Parsing properties file "my_model_check.pctl"...

1 PCTL property:
(1) Pmin=? [ F my_condition ]

-------------------------------------------

Simulating: Pmin=? [ F my_condition ]
Simulation parameters: approx = 0.01, conf = 1.0E-10, num samples =
412042, max path len = 10000)

Sampling progress: [ 0% 10% 20% 30% 40% 50% 60% 70% 80% 90% 100% ]

Sampling complete: 412042 iterations in 7.50 seconds (average
0.000018)
Path length statistics: average 4.8, min 3, max 7

Warning: Deadlocks were found during simulation: self-loops were added

Result: 0.27824105309652897


Thanks & Regards,

Tushar Deshpande

[Mark Kattenbelt]

Hi Tushar,

Its hard to answer this question without seeing your model, but
perhaps I can explain an issue that may be at hand here. I apologise
in advance if you already know this.

When you have an MDP the simulator has to resolve the non-determinism
in your model in order to provide you with a probability. The value
0.278 is therefore the probability found by the simulator when every
resolution of non-determinism is equally probable (the simulator will
chose uniformly at random one of the commands that is enabled at each
state). In most cases this is not really what you want from an MDP
model hence simulation of MDPs is not always a good idea.

This is not the case when you verify the property Pmin=? [ ... ]:
PRISM finds the minimum probability over all resolutions of non-
determinism. For instance, if a deadlock state is reachable with
probability 1 from your initial state -- by some sequence of commands
-- then this minimum probability is 0.

If you were expecting the result of the simulation, then perhaps your
model is not an MDP but an DTMC. To find out you need to decide what
should happen when multiple commands are enabled at the same time: if
they should all fire with equal probability then your model should be
a DTMC, if you want to find out the worst/best-case over all possible
ways you could choose a command then it should be a MDP.

Now as for your other question:

> Prob0E: 4 iterations in 0.02 seconds (average 0.005000, setup 0.00)
>
> Prob1A: 2 iterations in 0.02 seconds (average 0.008000, setup 0.00)
>
> yes = 28, no = 63, maybe = 4

Prism does some precomputation before computing probabilities: Prob1A
computes the set of states (yes) that satisfy the property with
probability 1 and Prob0E computes the set of states (no) that satisfy
the property with probability 0. These algorithms are (qualitative)
graph-based and are usually cheaper than the algorithms computing
actual probabilities. (maybe) is the set of states that is neither in
(yes) or in (no), and hence with the precomputation we have to compute
the probability only for this set.

That there are only 4 states in your model that are in your (maybe)
set seems a little odd.

If this didn't help please let us know!

Kind regards,

Mark

[Tushar Deshpande]

Hi Mark,

Thanks a lot for the info. I would revisit my model
and see if things are implemented as you advised.

But, here's a related doubt.

I'm curious about following fact.
How can we tell if a prism model is dtmc or mdp ?

e.g. here's an example from the prism documentation.

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

This example appears as mdp in the docs.

I get following result after running the model.

Building model...

Computing reachable states...

Reachability: 4 iterations in 0.00 seconds (average 0.000000, setup
0.00)

Time for model construction: 0.027 seconds.

Type: Nondeterministic (MDP)
Modules: M1 M2
Variables: x y

States: 8 (1 initial)
Transitions: 24
Choices: 14

Transition matrix: 54 nodes (5 terminal), 24 minterms, vars: 4r/4c/1nd


But, I can treat same model as dtmc.
If I run this model as dtmc, I get following result.

Building model...

Computing reachable states...

Reachability: 4 iterations in 0.00 seconds (average 0.000000, setup
0.00)

Time for model construction: 0.014 seconds.

Type: Probabilistic (DTMC)
Modules: M1 M2
Variables: x y

States: 8 (1 initial)
Transitions: 21

Transition matrix: 54 nodes (7 terminal), 21 minterms, vars: 4r/4c

As, you would notice, there's both outputs are identical.

This raises following question.
How can we tell from prism model code if the model is mdp or dtmc ?

Is there a special syntax for mdp models, especially, how are the
non-deterministic transitions are modeled in prism ?

e.g. In following code snippet, which part is non-deterministic ?
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

Also, is there any relationship between mdp and dtmc models ?
e.g. If I take a dtmc model and change its type to mdp, then would
the new model be a valid model ?

I'm asking this question, because I'm unsure if my model is mdp or
dtmc ?

At present, I feel that my model can be categorized as either mdp or
dtmc ?

On Mar 31, 5:43 am, Mark Kattenbelt <mark.kattenb...@comlab.ox.ac.uk>
wrote:

[Mark Kattenbelt]

Hi Tushar,

To answer your last question first: the only syntactical difference
between dtmcs and mdps in prism is the model declaration, so
syntactically any mdp is also a valid dtmc and vice versa. However,
this would typically not make sense semantically. Which semantics
makes sense for your model depends on your model, and this is your
choice.

As I tried to explain in my previous email, the semantic difference
between the two model types is how prism deals with the case when
multiple commands are enabled at the same state. For dtmcs prism
choses a command at random, whereas for mdps prism chooses a command
non-deterministically. To make this more concrete consider the
following two prism commands:

[] (x <= 2) -> "deadlock"
[] (x < 10) -> "finish"

The "deadlock" and "finish" is not really valid syntax in prism but
imagine this updates lead to particular states that you can select in
a property. Note that the guards of the two commands overlap, for
example in the state (x = 0) both commands are enabled. This is where
it matters whether or not your model is a dtmc or an mdp. In a dtmc
you would reach "deadlock" with probability 1/2 and "finish"
probability 1/2. Hence, if you compute the probability of
"deadlock" (from x = 0) you would get prob. 1/2 and analogously for
"finish".

In an mdp, you have a genuine non-deterministic choice between the two
commands. The maximum/minimum probability prism computes is the
maximum/minimum probability over all resolutions of non-determinism.
This means that when you compute the minimum probability of
"deadlocking" (from x = 0) you would get 0, as you could always pick
the command that leads to "finish". Similarly, the minimum probability
of "finish" is also 0 as in the worst case you could always pick
"deadlock". If you compute the maximum probability of deadlocking you
would get 1 as in the best-case you would always deadlock. Finally, if
you compute the maximum probability of "finish" you would also get 1
as in the best-case you would always "finish".

In the prism example you sent, there is no overlapping commands -- in
each concrete states at most 1 command that is enabled. In this case
the semantics of the dtmcs and mdps are indeed identical.

Hope that helps!

Kind regards,

Mark

On Apr 1, 4:14 am, Tushar Deshpande <tushar.deshpa...@gmail.com>
wrote:

[Gethin Norman]

Tushar,

one thing Mark forgot to mention was there is also a difference between
DTMCs and MDPs due to the scheduling between modules. See:

http://www.prismmodelchecker.org/manual/ThePRISMLanguage/ParallelComposition

(which uses the example you used in your previous mail) for details on this.

Gethin

[Tushar Deshpande]

Hi Mark,

Thanks a lot for extremely useful info.

I reviewed my model.

It seems that my model is indeed dtmc. Earlier, I was
not fully aware of semantics of dtmc and mdp.

I've also noticed that my model is too big. So, prism
runs out of memory while executing it.

But, the simulation of the dtmc model provides the
value of P which I expect.

Here's my question:

In your earlier response, you said that, 'simulation of MDPs
is not always a good idea.'

Then, does simulation of dtmc give reliable results ?

If so, then my job would be considerable easy.

Basically, I've translated a model that I developed using
Murphi model checker into a prism model.

I'm sure that the murphi model is correct.

So, the value of simulation would be sufficient for me
if it can be relied upon.

On Apr 1, 6:07 am, Gethin Norman <Gethin.Nor...@comlab.ox.ac.uk>
wrote:

> Tushar,
>
> one thing Mark forgot to mention was there is also a difference between
> DTMCs and MDPs due to the scheduling between modules. See:
>

> http://www.prismmodelchecker.org/manual/ThePRISMLanguage/ParallelComp...

[Mark Kattenbelt]

Hi Tushar,

> Then, does simulation of dtmc give reliable results ?

It should at least simulate your models with the semantics that you
intended. Clearly, the issue with simulation is that it is not
verification -- there is no guarantee attached to the results. However,
as you increase the number of samples, the confidence in the answer
increases and it is unlikely to be far of the true probability. It
should give you a fairly good indication of the answer to your property.

Perhaps there are ways to reduce the state space of your original model
so that you can verify it. If you would be willing to post a model we
could have a look.

Kind regards,

Mark

[Tushar Deshpande]

Hi Mark,

Thanks a lot for helping me.

I was able to reduce the size of my dtmc model.
I converted some variables into constants
(These variables were never assigned a new
value after initialization).

Now, my model runs perfectly without causing
out-of-memory error. I'm getting the expected
results too.

I've just a final doubt.

For a particular configuration of my model, I expect
that the p=? [F my_condition] should return 1.0

But, I'm getting value of 0.841 instead.

What could be the reason ? When we get value of P
as 1.0 ?

Do, we get value of P as 1.0 if ad only if the start state
is a part of final state in dtmc ?

How does prism go about calculating values of P for a
particular dtmc model ?

Thanks in advance,

Tushar Deshpande


On Apr 2, 4:10 am, Mark Kattenbelt <mark.kattenb...@comlab.ox.ac.uk>
wrote:

[Mark Kattenbelt]

Hi Tushar,

> For a particular configuration of my model, I expect
> that the p=? [F my_condition] should return 1.0
>
> But, I'm getting value of 0.841 instead.
>
> What could be the reason ? When we get value of P
> as 1.0 ?

From a theoretical point of view, for any (finite) dtmc, with
probability 1 you eventually reach a bottom strongly connected component
of your state graph and stay there forever. That you get the value of
0.841 means that there must be some bottom strongly connected component
that can be reached from the initial state (with some non-zero
probability) and that has an empty intersection with my_condition. E.g.
you must have some reachable 'infinite loop' in your model in which
my_condition is never true.

> Do, we get value of P as 1.0 if ad only if the start state
> is a part of final state in dtmc ?

No, you get 1 if and only if from the initial state you can always reach
the final state with probability one.

> How does prism go about calculating values of P for a
> particular dtmc model ?

A good place to start reading up about this is
http://www.prismmodelchecker.org/lectures/02-dtmcs.pdf

I hope that helps,

Kind regards,

Mark

[Tushar Deshpande]

Hi Mark,

Thanks a lot for solving my every doubt.

Finally, I've been able to understand my model
almost completely and justify the results given
by model checker.

The results are according to my expectations.

Using prism was a nice experience and I would look
forward to using it further.

Thanks & Regards,

Tushar Deshpande

On Apr 3, 4:27 am, Mark Kattenbelt <mark.kattenb...@comlab.ox.ac.uk>
wrote:

> A good place to start reading up about this ishttp://www.prismmodelchecker.org/lectures/02-dtmcs.pdf