How to determine if a system is DTMC or MDP ?

[Tushar Deshpande]

Hi,

My question is related with model checking in general.

How can we determine if a system is DTMC or MDP ?

I'm trying to model a system where at any given state,
zero or more actions are enabled. I want to determine,
the value of "P" for some final state.

Now, the value of P would be affected by choice of the
type of the model. I would get different values of "P"
depending on if the model is DTMC or MDP.

Are there any guidelines to determine if a system is
DTMC or MDP ?

I presume that if I want PRISM to make probabilistic
choices, then I should choose the model to be DTMC.
For a non-deterministic choice, I should use MDP.

Am I right ?

Thanks & Regards,
Tushar Deshpande

[Gethin Norman]

Tushar,


you are correct that the choice as to whether a model is a MDP or DTMC
is down to how you want the choice between actions (or commands). If you
want the choice to be uniformly at random then specify your model as a
DTMC, while if you want the choice to be nondeterministic then you need
to specify your model as an MDP.

Note that in the case of an MDP, there is no unique probability of
satisfying a formula as this depends on how the nondeterminism is
resolved. Furthermore, you can ask PRISM to find either the minimum or
maximum (under all possible resolutions of the nondeterminism) of
satisfying a property using the Pmin=? and Pmax=? operators.

Gethin

[Tushar Deshpande]

Hi Genthin,

Thanks a lot.

I think that typically MDP would be used
less frequently than DTMCs.

Typically, we would need DTMCs behavior.

e.g. If I want to model a situation where a
number is chosen at random from a range.
Then, it's appropriate to model it as DTMC.
DTMC would ennsure that each number is
chosen with equal probability.

On Oct 1, 5:19 am, Gethin Norman <Gethin.Nor...@comlab.ox.ac.uk>
wrote: