The existence of finite abstractions for branching time model checking

Abstract

Abstraction is often essential to verify a program with model checking. Typically, a concrete source program with an infinite (or finite, but large) state space is reduced to a small, finite state, abstract program on which a correctness property can be checked. The fundamental question we in-vestigate in this paper is whether such a reduction to finite state programs is always possible, for arbitrary branching time temporal properties. We begin by showing that existing abstraction frame-works are inherently incomplete for verifying purely exis-tential or mixed universal-existential properties. We then propose a new, complete abstraction framework which is based on a class of focused transition systems (FTS’s). The key new feature in FTS’s is a way of “focusing ” an ab-stract state to a set of more precise abstract states. While focus operators have been defined for specific contexts, this result shows their fundamental usefulness for proving non-universal properties. The constructive completeness proof provides linear size maximal models for properties expressed in logics such as CTL and the mu-calculus. This substantially improves upon known (worst-case) exponen-tial size constructions for their universal fragments. 1.