SRI International Computer Science Laboratory
Computing Abstractions of Infinite State Systems Compositionally and
Automatically
Saddek Bensalem, Yassine Lakhnech, and Sam Owre
Presented at
Computer-Aided Verification (CAV'98), Vancouver, BC, Canada, June/July 1998.
Springer-Verlag Lecture Notes in Computer Science Vol. 1427, pp 319-331.
Abstract
We present a method for computing abstractions of infinite state systems
compositionally and automatically. Given a concrete system of programs
and given an abstraction function, using our method one can compute an
abstract system that simulates the concrete system. A distinguishing
feature of our method is that it does not produce a single abstract state
graph but rather preserves the structure of the concrete system. This
feature is a prerequisite to benefit from the techniques developed in the
context of model-checking for mitigating the state explosion problem.
Moreover, our method has the advantage that the process of constructing
the abstract system does not depend on whether the computation model is
synchronous or asynchronous.
postscript (175kb) or
gzipped postscript (55kb)
BibTeX Entry
@inproceedings{Bensalem98:CAV,
AUTHOR = {Saddek Bensalem and Yassine Lakhnech and Sam Owre},
TITLE = {Computing Abstractions of Infinite State Systems
Compositionally and Automatically},
PAGES ={319--331},
CROSSREF = {CAV98}
}
Sam Owre:
Owre@csl.sri.com