This paper deals with the proof method of verification by finitary abstraction (vfa), which presents an alternative approach to the verification of (potentially infinite-state) reactive systems. We assume that the negation of the property to be verified is given by the user in the form of an infinite-state nondeterministic Bu chi discrete system (bds). The method consists of a two-step process by which, in a first step, the system and its (negated) specification are combined into a single infinite-state fair discrete system (fds, which is similar to a bds but with Streett acceptance conditions), which is abstracted into a finite-state automaton. The second step uses model checking to establish that the abstracted automaton is infeasible, i.e., has no computations.
The vfa method can be considered as a viable alternative to verification by temporal deduction, which, up to now, has been the main method generally applicable for verification of infinite-state systems.
The paper presents a general recipe for an fds abstraction, which is shown to be sound, where soundness means that infeasibility of the abstracted fds implies infeasibility of the unabstracted one, implying in turn the validity of the property over the concrete (infinite-state) system. To make the method applicable for the verification of liveness properties, pure abstraction is sometimes no longer adequate. We show that by augmenting the system with an appropriate (and standardly constructible) progress monitor, we obtain an augmented system, whose computations are essentially the same as those of