Abstraction for branching time properties

Effective program abstraction is needed to successfully apply model checking in practice. This paper studies 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. To achieve this, our method 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, weakening the transition relation at AND states, and strengthening it at OR states. We show semantic completeness: 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 method requires choice predicates that help resolve nondeterminism at OR states, and rank functions that help preserve progress properties. Specializing this result to predicate abstraction, we obtain exact characterizations of the types of properties provable with these methods.