In this paper we consider the applicability of multi-rooted binary decision diagrams for the probabilistic model checking. The symbolic probabilistic model checking involves manipulation of functions and matrices with the values in $[0,1]$, and multi-terminal binary decision diagrams, sparse matrices, and combinations thereof are used to represent these objects. We propose algorithms for representing these objects by means of multi-rooted binary decision diagrams when a function with the values in $[0,1]$ is approximated by a set of Boolean functions. Each Boolean function is represented by a binary decision diagram and being combined together these diagrams form a mutli-rooted binary decision diagram. Presented experimental results show that this approach allows for the model checking for large problems with a smaller memory footprint, compared to the use of the multi-terminal binary decision diagrams.
Original languageEnglish
Title of host publicationProceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)
PublisherSpringer Nature
Pages104-118
ISBN (Print)978-3-642-27939-3
StatePublished - 2012
Externally publishedYes

    Research areas

  • probabilistic model checking, binary decision diagrams

ID: 4452816