Research Article
Analysis of Markov reward models using zero-suppressed multi-terminal BDDs
@INPROCEEDINGS{10.1145/1190095.1190139, author={K. Lampka and M. Siegle}, title={Analysis of Markov reward models using zero-suppressed multi-terminal BDDs}, proceedings={1st International ICST Conference on Performance Evaluation Methodologies and Tools}, publisher={ACM}, proceedings_a={VALUETOOLS}, year={2012}, month={4}, keywords={Discrete Event Systems Markov Chain Numerical Solution Symbolic Data Structure Performance Evaluation Tool}, doi={10.1145/1190095.1190139} }- K. Lampka
M. Siegle
Year: 2012
Analysis of Markov reward models using zero-suppressed multi-terminal BDDs
VALUETOOLS
ACM
DOI: 10.1145/1190095.1190139
Abstract
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, zero-suppressed 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 specifications, whose underlying MRMs consist of more than 108 states. The proposed algorithms for generating user-defined PVs and computing their moments are independent of the employed symbolic data type. Thus they are highly suited to fit into other symbolic frameworks as realized in popular performance evaluation tools. The efficiency of the presented approach, which we incorporated into the Möbius modeling framework [16], is demonstrated by analyzing several benchmark models from the literature and comparing the obtained run-time data to other techniques.