In: LNCS 1785: Tools and Algorithms for the Construction and Analysis of Systems, pages 426-pp. 6th International Conference, TACAS 2000, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March/April 2000. Proceedings / S. Graf, M. Schwartzbach (Eds.) --- Springer Verlag, 2000.
Abstract: The control state reachability problem is decidable for well-structured infinite-state systems like unbounded Petri Nets, Vector Addition Systems, Lossy Petri Nets, and Broadcast Protocols. An abstract algorithm that solves the problem is given in [ACJT96,FS99]. The algorithm computes the closure of the predecessor operator w.r.t. a given upward-closed set of target states. When applied to this class of verification problems, traditional (infinite-state) symbolic model checkers suffer from the state explosion problem even for very small examples. We provide BDD-like data structures to represent in a compact way collections of upwards closed sets over numerical domains. This way, we turn the abstract algorithm of [ACJT96,FS99] into a practical method. Preliminary experimental results indicate the potential usefulness of our method.