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.


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

	AUTHOR = {Saddek Bensalem and Yassine Lakhnech and Sam Owre},
	TITLE = {Computing Abstractions of Infinite State Systems 
		Compositionally and Automatically},
	PAGES ={319--331},

Sam Owre: