Covering sharing trees: a compact data structure for parameterized verification

The control state reachability problem is decidable for well-structured infinite-state systems like (Lossy) Petri Nets, Vector Addition Systems, and broadcast protocols. An abstract algorithm that solves the problem is the backward reachability algorithm of Abdulla-Jonsson. The algorithm computes the closure of the predecessor operator with respect to a given upward-closed set of target states. When applied to this class of verification problems, symbolic model checkers based on constraints like suffer from the state explosion problem. In order to tackle this problem, in we introduced a new data structure, called covering sharing trees, to represent in a compact way collections of infinite sets of system configurations. In this paper, we will study the theoretical complexity of the operations over covering sharing trees needed in symbolic model checking. We will also discuss several optimizations that can be used when dealing with Petri Nets. Among them, in previous work we introduced a new heuristic rule based on structural properties of Petri Nets that can be used to efficiently prune the search during symbolic backward exploration. The combination of these techniques allowed us to turn the abstract algorithm of Abdulla-Jonsson into a practical method. We have evaluated the method on several finite-state and infinite-state examples taken from the literature (e.g. unbounded Petri nets). In this paper, we compare the results we obtained in our experiments with those obtained using other finite and infinite-state verification tools.