Verification by augmented abstraction: The automata-theoretic view

This paper deals with the proof method of verification by finitary abstract ion (VFA), which presents an alternative approach to the verification of (p otentially 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 infinit e-state nondeterministic Buchi discrete system (BDS). The method consists o f 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 sys tem (FDS, which is similar to a BDS but with Streett acceptance conditions) , which is abstracted into a finite-state automaton. The second step uses m odel 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 a pplicable 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 validi ty of the property over the concrete (infinite-state) system. To make the m ethod applicable for the verification of liveness properties, pure abstract ion is sometimes no longer adequate. We show that by augmenting the system with an appropriate (and standardly constructible) progress monitor. we obt ain an augmented system, whose computations are essentially the same as tho se of the original system and which may now be abstracted while preserving the desired liveness properties. We refer to the extended method as verific ation by augmented abstraction (VAA). We then proceed to show that the VAA method is sound and complete fur provi ng all properties: whose negations are expressible by a sus. Given that eve ry linear temporal logic (LTL) property can be translated to a BDS this est ablishes that the VAA method is sound and complete for proving the validity of all LTL properties, including both safety and liveness. (C) 2001 Academ ic Press.