Tutorial T6
Symbolic Decision Diagrams and Their Application to High-Level GSPNs
Giuliana Franceschinis
(Univ. of Piemonte Orientale, Italy)
Yann Thierry-Mieg
(Univ. of Paris 6, France)
Duration: 180 minutes
Well-Formed Nets (WN) and their stochastic time extension (SWN) are High Level Petri Net formalisms which allow the automatic exploitation of the model behavioral symmetries and the direct construction of a reduced state space and state transition diagram (Symbolic Reachability Graph, SRG) for qualitative analysis, as well as a lumped Continuous Time Markov Chain for quantitative analysis. Also decision diagrams allow to represent in a compact way very large state spaces, but exploiting different kinds of symmetries.

We first introduce the SWN formalism and describe the procedure that allows to build the SRG of a SWN model, then we show how the SRG techniqe can be effectively combined with hierarchical decision diagrams (namely Data Decision Diagrams - DDD - and Set Decision Diagrams - SDD) to represent in a very compact way the Symbolic Reachability Set.

Web Maintenance Person.