Abstraction for Branching Time Properties

Effective methods of program abstraction are necessary for the successful application of model checking in practice. Most current methods construct abstractions that preserve linear time temporal properties. In this paper, we study the question of constructing abstractions that preserve branching time properties. The key challenge is to simultaneously preserve the existential and universal aspects of a property, without relying on bisimulation between the concrete and abstract programs. To achieve this, we propose a method that abstracts an alternating transition system (ATS), formed by the product of a program with an alternating tree automaton for a property. The AND-OR distinction in the ATS is used to guide the abstraction of its transitions, weakening the transition relation at AND states, and strengthening it at OR states. We show the semantic completeness of the method: i.e., whenever a program satisfies a property, this can be shown using a finite state abstract ATS produced by the method. To achieve completeness, the abstraction process requires further information in the form of choice predicates that help resolve nondeterminism at OR states, and rank functions that are needed to preserve progress properties. Specializing the completeness result to predicate abstraction procedures, we obtain exact characterizations of the types of properties provable with such procedures.