Covering sharing trees: a compact data structure for parameterized verification |
| |
Authors: | Giorgio Delzanno Jean-François Raskin Laurent Van Begin |
| |
Affiliation: | (1) Dipartimento di Informatica e Scienze dell Informazione, Università di Genova, via Dodecaneso 35, 16146 Genova, Italy;(2) Département d Informatique, Université Libre de Bruxelles, Blvd Du Triomphe, 1050 Bruxelles, Belgium |
| |
Abstract: | 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 [1, 21 ]. 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 [7, 26 ] suffer from the state explosion problem.In order to tackle this problem, in [13] 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 [14] 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 [1, 21 ] into a practical method. We have evaluated the method on several finite-state and infinite-state examples taken from the literature [2, 18 , 20 , 30 ]. In this paper, we will compare the results we obtained in our experiments with those obtained using other finite and infinite-state verification tools. |
| |
Keywords: | Symbolic model checking Infinite-state systems Constraints Efficient data structures Heuristics Static analysis |
本文献已被 SpringerLink 等数据库收录! |
|