How to extract transition probability from transition matrix MTBDD

[Ali A. Noroozi]

Hi,

This seems a trivial question, but I could not find an answer to it. Given a dtmc model, which is an instance of ProbModel class and the model's transition matrix "trans", how can I extract transition probability between any two states, for instance between states 1 and 2 ?

[Joachim Klein]

Hi Ali,

In the MTBDD world, questions are seldom trivial :)

Depending on what you want to do, there are several approaches. If you
consider the matrix to range over the full state space that is spanned
by the row and column MTBDD variables (i.e., for n row/col variables you
have states 0 ... 2^n-1), you can encode the row index as an assignment
to the row variables, the column index as an assignment to the column
variables and then use Cudd_Eval to obtain the constant corresponding to
that matrix entry. See, e.g., the code in DD_PrintMatrix

https://github.com/prismmodelchecker/prism/blob/a8999396873a4fc4636b67f93fba6fc3fd0c82ac/prism/src/dd/dd_matrix.cc#L463


If you want to consider trans to be a matrix over a subset of the state
space (i.e., only the reachable states), things get a bit more tricky.
Here, you have to be able to convert between the state index (0th
reachable state, 1st reachable state, ...) and the corresponding
assignment. For that purpose, PRISM maintains an ODD data structure that
allows to compute the state index of a row variable assignment and vice
versa. Consider the code in
https://github.com/prismmodelchecker/prism/blob/f767eb70d04103233d1b68ee2c7b673d0b0a31bd/prism/src/sparse/PS_ExportMatrix.cc#L40
which is used for this purpose (e.g., for exporting the .tra file of the
transition matrix). For convenience, an explicit (sparse) matrix is
generated here (over the reachable states, taking the ODD information
into account) and then there is iteration over the entries of that matrix.

Does this help?

Cheers,
Joachim Klein

[Ali A. Noroozi]

Dear Joachim,

Yes, it helped. I wanted transitions of reachable states. I was already working on PS_ExportMatrix.cc, but I was in doubt that maybe there was an easier way.

Anyway, I implemented a function similar to first part of PS_ExportMatrix to build the explicit sparse matrix and another function for querying the transition probability of two arbitrary state indexes. It seems it is working fine.

Anyway, thanks for your answer.