Implicit GSPN reachability set generation using decision diagrams

Implicit techniques for representing and generating the reachability set of a high-level model have become quite efficient. However, such techniques are usually restricted to models whose events have equal priority. Models containing events with differing classes of priority or complex priority structure, in particular models with immediate events, have thus been required to use less-efficient explicit reachability set generation techniques. In this paper, we present an efficient implicit technique, based on multi-valued decision diagram (MDD) representations for sets of states and matrix diagram representations for next-state functions, that can handle models with complex priority structure. We adapt an efficient Kronecker-based reachability set generation algorithm to work with matrix diagrams. If the model contains immediate events, the vanishing states can be eliminated either during generation, by manipulating the matrix diagram, or after generation, by manipulating the MDD. We apply both techniques to several models and give detailed experimental results.