Standard

On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking. / Bugaychenko, D.Y.

Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer Nature, 2012. p. 104-118.

Research output: Chapter in Book/Report/Conference proceeding › Article in an anthology

Harvard

Bugaychenko, DY 2012, On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking. in Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer Nature, pp. 104-118. <http://link.springer.com/chapter/10.1007%2F978-3-642-27940-9_8?LI=true>

APA

Bugaychenko, D. Y. (2012). On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking. In Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) (pp. 104-118). Springer Nature. http://link.springer.com/chapter/10.1007%2F978-3-642-27940-9_8?LI=true

Vancouver

Bugaychenko DY. On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking. In Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer Nature. 2012. p. 104-118

Author

Bugaychenko, D.Y. / On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking. Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer Nature, 2012. pp. 104-118

BibTeX

@inbook{b4c1483b9dbe41f8a5bca2848029399e,
title = "On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking",
abstract = "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.",
keywords = "probabilistic model checking, binary decision diagrams",
author = "D.Y. Bugaychenko",
year = "2012",
language = "English",
isbn = "978-3-642-27939-3",
pages = "104--118",
booktitle = "Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)",
publisher = "Springer Nature",
address = "Germany",

}

RIS

TY - CHAP

T1 - On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking

AU - Bugaychenko, D.Y.

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

KW - probabilistic model checking

KW - binary decision diagrams

M3 - Article in an anthology

SN - 978-3-642-27939-3

SP - 104

EP - 118

BT - Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)

PB - Springer Nature

ER -

ID: 4452816