UC BERKELEY
EECS technical reports
TECHNICAL REPORTS


CSD-99-1075.pdf
CSD-99-1075.ps
Conditions of Use

Archive Home Page

Symbolic Representation of Upwards Closed Sets

Authors:
Delzanno, Giorgio
Raskin, Jean-Francois
Technical Report Identifier: CSD-99-1075
1999
CSD-99-1075.pdf
CSD-99-1075.ps

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.