 |
|
|||
| 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] |
