Activity-Local Symbolic State Graph Generation for High-Level Stochastic Models
Conference: MMB 2006 - 13th GI/ITG Conference Measuring, Modelling and Evaluation of Computer and Communication Systems
03/27/2006 - 03/29/2006 at Nürnberg, Germany
Proceedings: MMB 2006
Pages: 19Language: englishTyp: PDF
Personal VDE Members are entitled to a 10% discount on this title
Authors:
Lampka, Kai; Siegle, Markus (Universität der Bundeswehr München, Institut für Technische Informatik)
Abstract:
This paper introduces a new, efficient method for deriving compact symbolic representations of very large (labelled) Markov chains resulting from high-level model specifications such as stochastic Petri nets, stochastic process algebras, etc.. This so called “activity-local” scheme is combined with a new data structure, called zero-suppressed multi-terminal binary decision diagram, and a new efficient “activity-oriented” scheme for symbolic reachability analysis. Several standard benchmark models from the literature are analyzed in order to show the superiority of our approach.