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 explicit reachability set generation techniques. In this paper, we present an efficient implicit technique, based on multi-valued decision diagram representations for sets of states and matrix diagram representations for next-state functions, that can handle models with complex priority structure. 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 multi-valued decision diagram. We apply both techniques to several models and give detailed results.
展开▼
