Saturation for a general class of models

Implicit techniques for construction and representation of the reachability set of a high-level model have become quite efficient for certain types of models. In particular, previous work developed a "saturation" algorithm that exploits asynchronous behavior to efficiently construct the reachability set using multiway decision diagrams, but requires each model event to be expressible as a Kronecker product. In this paper, we develop a new version of the saturation algorithm that works for a general class of models: models whose events are not necessarily expressible as Kronecker products, models containing events with complex priority structures, and models whose state variables have unknown bounds. We apply our algorithm to several examples and give detailed experimental results.