symbolically compute reachability probability of a state in a DTMC

[Khayyam Salehi]

Dear all,

How can I symbolically compute reachability probability of a state in a DTMC model? I have state number and values of variable in the state.

Cheers,

Khayyam.

[Joachim Klein]

Hi,

> How can I symbolically compute reachability probability of a state in a
> DTMC model? I have state number and values of variable in the state.

You want to know the probability of reaching this state from the initial
state? Then you can use

P=?[ F (s1=3 & s2=1 & ....) ]

where the part inside the () are just all the values of the variables
for that state (i.e., in the example, there is a variable s1 which has
value 3 in the state of interest, variable s2 has value 1, etc).

I'm not fully sure what you mean by symbolically. If you mean it in the
sense that you want the model to be constructed and the analysis carried
out using a symbolic representation using multi-terminal binary decision
diagrams, you can use the MTBDD engine (-mtbdd switch on the command
line; or selecting that engine in the GUI options).

Alternatively, if you mean symbolically in the sense that you want to
get the exact fraction, you can use the exact engine (using the -exact
switch).


Cheers,
Joachim Kleinn

[Khayyam Salehi]

Thanks for your response. How can I do this by code? I am writing a program and I have the dtmc model as a ProbModel instance.

[Joachim Klein]

Hi,

> Thanks for your response. How can I do this by code? I am writing a > program and I have the dtmc model as a ProbModel instance.

Have a look at the prism.ProbModelChecker class, in particular the
createNewModelChecker and checkExpression methods, as well as the
infrastructure in prism.Prism for loading a model, parsing an expression
and doing model checking.

Cheers,
Joachim Klein