Findig paths and traces of a dtmc model

23 views
Skip to first unread message

Ali A. Noroozi

unread,
Aug 28, 2018, 6:37:37 AM8/28/18
to PRISM model checker developers
Hi,

Given a dtmc model, which is an instance of ProbModel class, how can I find all paths and also traces of a single variable symbolically?

In a non-symbolic method, I did the following:
1. created an instance of StateListMTBDD from JDDNode reach,
2. wrote a function similar to method doPrint() of StateListMTBDD in order to get an explicit list of all reachable states,
3. created a sparse matrix of transitions using the class PrismSparse,
4. Having the explicit set of all reachable states and the sparse matrix of transitions, I traversed the dtmc and extracted paths and then traces.

But this is not efficient in big models (e.g., in my computer, models with more than 3 million states and 8 million transitions). Is there a symbolic method for this?

Joachim Klein

unread,
Sep 1, 2018, 7:50:35 AM9/1/18
to Ali A. Noroozi, PRISM model checker developers
Hi,

> Given a dtmc model, which is an instance of ProbModel class, how can I
> find all paths and also traces of a single variable symbolically?

Could you clarify a bit what you concretely want to do? Do you want to
check something for these paths (symbolically) or do you want to output
the paths? Something like "from the initial state, for each reachable
state give me a path that shows that it can be reached?"


There is functionality in the symbolic CTL model checker of PRISM to
generate counter-examples/witnesses: E.g., for

E[ F "goal" ]

you will get a witness that demonstrates that one state satisfying
"goal" can be reached from an initial state.

So., running

prism prism-examples/dice/dice.pm -pf 'E[ F s=7 ]'

produces

Result: true (property satisfied in the initial state)

Counterexample/witness:
(0,0)
(1,0)
(3,0)
(7,1)


This is implemented in prism.NonProbModelChecker in the method
checkExistsUntil. The general idea is to perform a symbolic reachability
computation and to store in each iteration step the set of newly
discovered states. Then, once a target state has been reached, one can
trace back through these sets to construct a path to one of the initial
states.

Depending on what you want to achieve, this might give you some ideas.

Cheers,
Joachim Klein
Reply all
Reply to author
Forward
0 new messages