Geodesic
Discrete random variables modeling using multiroot decision diagrams
Vestnik Sankt-Peterburgskogo universiteta. Prikladnaâ matematika, informatika, processy upravleniâ, no. 2 (2012), pp. 66-74
Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

The paper proposes a new approach for modeling discrete random variables based on multiroot binary decision diagrams ($MRBDD$). This need arise, for instance, in the problem of probabilistic verification, where another type of decision diagrams – multiterminal binary decision diagrams ($MTBDD$) – is widely used present. Multiroot diagrams have a number of significant advantages compared with multiterminal ones. Due to more efficient reuse of common building blocks multiroot diagrams provide more compact representation consuming less memory, and in many cases allowing a better execution time. Experimental results presented in the paper show that multiroot diagrams are a promising alternative to multiterminal diagrams for such problems as random variables modeling and probabilistic verification.
Keywords: binary decision diagrams, probabilistic verification. 
@article{VSPUI_2012_2_a7,
     author = {D. Yu. Bugaychenko and I. P. Soloviev},
     title = {Discrete random variables modeling using multiroot decision diagrams},
     journal = {Vestnik Sankt-Peterburgskogo universiteta. Prikladna\^a matematika, informatika, processy upravleni\^a},
     pages = {66--74},
     year = {2012},
     number = {2},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/VSPUI_2012_2_a7/}
}
TY  - JOUR
AU  - D. Yu. Bugaychenko
AU  - I. P. Soloviev
TI  - Discrete random variables modeling using multiroot decision diagrams
JO  - Vestnik Sankt-Peterburgskogo universiteta. Prikladnaâ matematika, informatika, processy upravleniâ
PY  - 2012
SP  - 66
EP  - 74
IS  - 2
UR  - http://geodesic.mathdoc.fr/item/VSPUI_2012_2_a7/
LA  - ru
ID  - VSPUI_2012_2_a7
ER  - 
%0 Journal Article
%A D. Yu. Bugaychenko
%A I. P. Soloviev
%T Discrete random variables modeling using multiroot decision diagrams
%J Vestnik Sankt-Peterburgskogo universiteta. Prikladnaâ matematika, informatika, processy upravleniâ
%D 2012
%P 66-74
%N 2
%U http://geodesic.mathdoc.fr/item/VSPUI_2012_2_a7/
%G ru
%F VSPUI_2012_2_a7
D. Yu. Bugaychenko; I. P. Soloviev. Discrete random variables modeling using multiroot decision diagrams. Vestnik Sankt-Peterburgskogo universiteta. Prikladnaâ matematika, informatika, processy upravleniâ, no. 2 (2012), pp. 66-74. http://geodesic.mathdoc.fr/item/VSPUI_2012_2_a7/

[1] Karpov Yu. G., Model Checking. Verifikatsiya parallelnykh i raspredelennykh programmnykh sistem, BKhV-Peterburg, SPb, 2010, 552 pp.

[2] Constant C., Jeannet B., Jéron T., “Automatic test generation from interprocedural specifications”, Testing of Software and Communicating Systems, 2007, 41–57 | DOI

[3] Tillmann N., De Halleux J., “Pex: white box test generation for .NET”, TAP'08, Proc. of the 2nd Intern. conference on tests and proofs, Springer-Verlag, Berlin; Heidelberg, 2008, 134–153

[4] Kong S., Tillmann N., Halleux J. d., “Automated testing of environment-dependent programs – a case study of modeling the file system for Pex”, ITNG '09, Proc. of the 2009 Sixth Intern. Conference on Information Technology: New Generations, IEEE Computer Society, Washington, DC, USA, 2009, 758–762

[5] Zaki M., Tahar S., Bois G., “Formal verification of analog and mixed signal designs”, A survey, Microelectronics Journal, 39:12 (2008), 1395–1404 | DOI

[6] Bäumler S., Balser M., Dunets A. e. a., “Verification of medical guidelines by model checking – a case study”, Model Checking Software, 2006, 219–233 | DOI

[7] Pang J., Fokkink W., Hofman R., Veldema R., “Model checking a cache coherence protocol of a Java DSM implementation”, Journal of Logic and Algebraic Programming, 71:1 (2007), 1–43 | DOI | MR | Zbl

[8] Beyer D., Henzinger T., Jhala R., Majumdar R., “The software model checker Blast”, Intern. J. on Software Tools for Technology Transfer, 9:5 (2007), 505–525 | DOI

[9] Bryant R. E., “Symbolic boolean manipulation with ordered binary-decision diagrams”, ACM Computing Surveys, 24:3 (1992), 293–318 | DOI

[10] Fujita M., McGeer P. C., Yang J. C.-Y., “Multi-terminal binary decision diagrams: An efficient datastructure for matrix representation”, Form. Methods Syst. Des., 10:2-3 (1997), 149–169 | DOI

[11] Bugaychenko D., Soloviev I., “Application of multiroot decision diagrams for integer functions”, Vestn. St. Petersburg University. Mathematics, 43:2 (2010), 92–97 | DOI | MR

[12] Younes H., Kwiatkowska M., Norman G., Parker D., “Numerical vs. statistical probabilistic model checking”, Intern. J. on Software Tools for Technology Transfer (STTT), 8:3 (2006), 216–228 | DOI | MR

[13] Duff I., “A survey of sparse matrix research”, Proc. of the IEEE, 65:4 (2005), 500–535 | DOI

[14] Oldenkamp H., Probabilistic model checking. A comparison of tools, Master's thesis, University of Twente, Twente Noederlande, 2007, 108 pp.

[15] Parker D., Implementation of symbolic model checking for probabilistic system, Ph.D. thesis, University of Birmingham, Birmingham, 2002, 222 pp.

[16] Karatsuba A. A., Ofman Yu. P., “Umnozhenie mnogoznachnykh chisel na avtomatakh”, Dokl. AN SSSR, 145:2 (1962), 293–294

[17] Bugaichenko D., Solovev I., “Biblioteka mnogokornevykh binarnykh reshayuschikh diagramm BddFunctions i ee primenenie”, Sistemnoe programmirovanie, 2010, no. 5, 193–213