## Generating Finite-State Abstractions
of Reactive Systems Using Decision Procedures

*Michael Colon,
Tomas Uribe *
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.

Last modified: Wed May 5 14:38:50 PDT
1999