Orna Kupferman

AT&T Bell Labs and DIMACS - SYLA Postdoc

An Automata-Theoretic Approach to Branching Time Model Checking

DIMACS Center - Room 431
Busch Campus
Piscataway, New Jersey
September 20, 1995 at 1:00 PM


In temporal-logic model checking, we verify the correctness of a program with respect to a desired behavior by checking whether a structure that models the program satisfies a temporal logic formula that specifies this behavior. Model-checking methods consider two types of temporal logics: linear and branching. In linear temporal logics, each moment in time has a unique possible future. Accordingly, linear temporal logic formulas are interpreted over a path in a structure and refer to a single computation of a program. In branching temporal logics, each moment in time may split into several possible futures. Accordingly, branching temporal logic formulas are interpreted over a state in a structure and refer to all the computations that start at this state.

Translating linear temporal logic formulas to automata has proven to be an effective approach for implementing linear-time model-checking, and for obtaining many extensions and improvements to this verification method. On the other hand, for branching temporal logic, automata-theoretic techniques have long been thought to introduce an exponential penalty, making them essentially useless for model-checking. In this talk I will describe (briefly) the automata-theoretic approach to linear-time model checking, describe (less briefly) the problems that impeded its extension to branching-time model checking, describe (in detail) why and how alternating tree automata solve these problems, and describe (in the remaining time) the theoretical and practical advantages offered by this approach.