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
Abstract:
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.