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) …