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.