Giorgio Delzanno and Jean-Francois Raskin

EECS Department, University of California, Berkeley

Technical Report No. UCB/CSD-99-1075

, 1999

http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/CSD-99-1075.pdf

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. <p>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.

---

BibTeX citation:

@techreport{Delzanno:CSD-99-1075,
    Author= {Delzanno, Giorgio and Raskin, Jean-Francois},
    Title= {Symbolic Representation of Upwards Closed Sets},
    Year= {1999},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/5715.html},
    Number= {UCB/CSD-99-1075},
    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. <p>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.},
}

EndNote citation:

%0 Report
%A Delzanno, Giorgio 
%A Raskin, Jean-Francois 
%T Symbolic Representation of Upwards Closed Sets
%I EECS Department, University of California, Berkeley
%D 1999
%@ UCB/CSD-99-1075
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/5715.html
%F Delzanno:CSD-99-1075