Abstraction and abstraction refinement
bookPart
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.
TNO Identifier
842715
ISBN
9783319105758 ; 9783319105741
Publisher
Springer
Source title
Handbook of Model Checking
Collation
34 p.
Pages
385-419
Files
To receive the publication files, please send an e-mail request to TNO Repository.