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.