Sciweavers

ICCAD
1996
IEEE

Tearing based automatic abstraction for CTL model checking

13 years 7 months ago
Tearing based automatic abstraction for CTL model checking
Based Automatic Abstraction for CTL Model Checking Woohyuk Lee Abelardo Pardo Jae-Young Jang Gary Hachtel Fabio Somenzi University of Colorado ECEN Campus Box 425 Boulder, CO, 80309 In this paper we present the tearing paradigm as a way to cally 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 veri cation 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 veri cation 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.
Woohyuk Lee, Abelardo Pardo, Jae-Young Jang, Gary
Added 07 Aug 2010
Updated 07 Aug 2010
Type Conference
Year 1996
Where ICCAD
Authors Woohyuk Lee, Abelardo Pardo, Jae-Young Jang, Gary D. Hachtel, Fabio Somenzi
Comments (0)