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 using a Kronecker product expression to represent each model event. For models whose events do not naturally fall into this category, use of the saturation algorithm requires adjusting the model by combining components or splitting events into subevents until a Kronecker product expression is possible. In practice, this can lead to additional overheads during reachability set construction. This paper presents 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. Experimental results are given for several examples