We present an algorithm that uses decision procedures to generate finite-state abstractions of possibly infinite-state systems. The algorithm compositionally abstracts the transitions of the system, relative to a given, fixed set of assertions. Thus, the number of validity checks is proportional to the size of the system description, rather than the size of the abstract state-space. The generated abstractions are weakly preserving for universal CTL* temporal properties. We describe several applications of the algorithm, implemented using the decision procedures of the Stanford Temporal Prover (STeP).
Appeared in International Conference on Computer-Aided Verification, CAV'98, pp. 293-304, vol. 1427 of LNCS, Springer-Verlag, June/July 1998.
Postscript. PDF. © 1998, Springer Verlag.