Abstract:
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.