|
Authors: | Kai Lampka |
Group: | Computer Engineering |
Type: | Inproceedings |
Title: | Multi-rooted ZMTBDDs and the symbolic, quantitative verification of systems |
Year: | 2008 |
Month: | September |
Pub-Key: | Lam08b |
Book Titel: | Proceedings of the 8th Workshop on Boolean Problems (WBP08) |
Pages: | 145-160 |
Keywords: | Binary Decision Diagrams and their algorithms, symbolic data structures for performance analysis |
Publisher: | Freiberg Univ. of Mining and Technology |
Abstract: | Former work developed zero-suppressed Multi-terminal BDDs (ZMTBDDs) for the efficient generation and representation of stochastic transition rate matrices underlying high-level (Markov model) descriptions of systems [Lam06a,Lam07a]. For manipulating ZMTBDDs, possibly defined over different sets of function variables, but allocated in a shared environment as provided by BDD-packages such as CUDD [Cudd] the authors of [Lam07a] and [Lam:08a] developed the concept of partially shared ZMTBDDs. This paper recapitulates important aspects of this concept and presents run-time data as obtained from the analysis of benchmarking models in the context of symbolic, performance analysis of systems. |
Resources: | [BibTeX] |