Activity-Local Symbolic State Graph Generation for High-Level Stochastic Models

Konferenz: MMB 2006 - 13th GI/ITG Conference Measuring, Modelling and Evaluation of Computer and Communication Systems
27.03.2006 - 29.03.2006 in Nürnberg, Germany

Tagungsband: MMB 2006

Seiten: 19Sprache: EnglischTyp: PDF

Persönliche VDE-Mitglieder erhalten auf diesen Artikel 10% Rabatt

Lampka, Kai; Siegle, Markus (Universität der Bundeswehr München, Institut für Technische Informatik)

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.