## Verification by Finitary Abstraction

**Amir Pnueli**

Weizmann Institute of Science

**Abstract.**
When verifying temporal properties of reactive systems, the common
wisdom is: if it is finite-state, model-check it, otherwise one must
use temporal deduction, supported by theorem provers such as STEP,
PVS, etc.

The study of abstraction as an aid to verification demonstrated that,
in some interesting cases, one can abstract an infinite-state system
into a finite-state one. This suggests an alternative approach to the
temporal verification of infinite-state systems: abstract first and
model check later.

In this talk, we explore the generality of this alternative
approach. Namely, is it the case that everything that can be verified
using temporal deduction can also be verified by abstraction followed
by finite-state model checking? We will identify classes of properties
and abstractions for which the VFA (Verification by Finitary
Abstraction) approach is sound and complete.