symbolically compute reachability probability of a state in a DTMC

27 views
Skip to first unread message

Khayyam Salehi

unread,
Dec 28, 2019, 11:35:34 AM12/28/19
to PRISM model checker developers
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

unread,
Dec 28, 2019, 1:17:20 PM12/28/19
to Khayyam Salehi, PRISM model checker developers
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
Message has been deleted

Khayyam Salehi

unread,
Dec 28, 2019, 3:45:59 PM12/28/19
to PRISM model checker developers
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

unread,
Dec 31, 2019, 9:04:27 AM12/31/19
to Khayyam Salehi, PRISM model checker developers
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
Reply all
Reply to author
Forward
0 new messages