Abstraction and abstraction refinement

Abstract

Abstraction, in the context of model checking, is aimed at reducing the state space of the system by omitting details that are irrelevant to the property being verified. Many successful approaches to the "state explosion problem," some of them described in other chapters, can be seen as abstractions. In this chapter, several notions of abstraction are considered in a uniform setting. Different such notions lead to a variety of preservation results that establish which kind of temporal properties may be verified via an abstracted system. We first define the needed background on simulation and bisimulation relations and their logic preservation. We then present the abstraction that is currently most widely used in practice: existential abstraction, which preserves universal fragments of branching-time logics. We give examples of such abstractions: localization reduction for hardware and predicate abstraction for software. We then proceed to stronger abstractions which preserve full branching-time logics.We introduce Kripke Modal Transition Systems and modal simulation, and show logic preservation. We close the chapter with a review of the presented results in the light of the notion of completeness.