Tearing Based Automatic Abstraction for CTL Model Checking

Woohyuk Lee, Abelardo Pardo, Jae-Young Jang, Gary Hachtel, and Fabio Somenzi

Proceedings of the International Conference on Computer Aided Design, pp 76-81, Nov. 1996

Abstract

In this paper we present the tearing paradigm as a way to automatically abstract behavior to obtain upper and lower bound approximations of a reactive system. We present algorithms that exploit the bounds to perform conservative ECTL and ACTL model checking. We also give an algorithm for false negative (or false positive) resolution for verification based on a theory of a lattice of approximations. We show that there exists a bipartition of the lattice set based on positive versus negative verification results. Our resolution methods are based on determining a pseudo-optimal shortest path from a given, possibly coarse but tractable approximation, to a nearest point on the contour separating one set of the bipartition from the other.

Click here to download the compressed postscript version.

BibTeX Entry

@INPROCEEDINGS { Lee96 ,
        ADDRESS = "San Jose, CA" ,
        AUTHOR = "W. Lee and A. Pardo and J. Jang and G. Hachtel and 
	          F. Somenzi" ,
        BOOKTITLE = "Proceedings of the International Conference on
	             Computer-Aided Design", 
        MONTH =   nov  ,
        PAGES = "76-81" ,
        TITLE = "Tearing Based Abstraction for {CTL} Model Checking" ,
        YEAR = "1996"
        }
Return to the home page