Analysis of Markov reward models using zero-suppressed multi-terminal BDDs

High-level stochastic description methods such as stochastic Petri nets, stochastic UML statecharts etc., together with specifications of performance variables (PVs), enable a compact description of systems and quantitative measures of interest. The underlying Markov reward models (MRMs) often exhibit a significant blow-up in size, commonly known as the state space explosion problem. In this paper we employ our recently developed type of symbolic data structure, zerosuppressed multi-terminal binary decision diagram (ZDD). In addition to earlier work [12] the following innovations are introduced: (a) new algorithms for efficiently generating ZDD-based representation of user-defined PVs, (b) a new ZDD-based variant of the approach of [17] for computing state probabilities, and (c) a new ZDD-based algorithm for computing moments of the PVs. These contributions yield a ZDD-based framework which allows the computation of complex performance and reliability measures of high-level system ...

• Type: Conference
• Year: 2006
• Where: VALUETOOLS
• Authors: Kai Lampka, Markus Siegle
• Keywords: Hardware, Performance Evaluation Tool, Symbolic Data Structure, User-defined Pvs, VALUETOOLS 2006