Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking
verfasst von : Dmitry Bugaychenko
Erschienen in: Verification, Model Checking, and Abstract Interpretation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.