Symbolic Representation of Upwards Closed Sets
Abstract: The reachability problem for a wide class of infinite-state systems is decidable when the initial and the final set of configurations are given as upwards closed sets. Traditional symbolic model checking methods suffer from the state explosion problem when applied to this class of verification problems.
We provide new data structures and algorithms for an efficient manipulation of upwards closed sets. These operations can be incorporated into model checking procedures for integer systems with infinite-states space. We report on experiments for verification problems of Vector Addition Systems.