BRANCHING-TIME TEMPORAL LOGIC AND TREE AUTOMATA

In temporal-logic model checking, we verify the correctness of a progr am with respect to a desired behavior by checking whether a structure that models the program satisfies a temporal logic formula that specif ies this behavior. The close connection between linear-time temporal l ogics and the theory of automata on infinite words has been an active area of research, In particular, automata-theoretic techniques have pr oven to be an effective approach to linear-time model checking. On the other hand, for branching-time temporal logics, current automata-theo retic techniques involve an exponential blow-up, making them essential ly useless for model-checking. In this paper we present an automata-th eoretic framework for branching-time model checking. We introduce simu ltaneous trees and associate with every structure a simultaneous tree that enables an automaton to visit different nodes on the same path of the structure simultaneously. With every formula psi we associate an automaton that accepts exactly these simultaneous trees that originate from structures that satisfy psi. This enables to use the automaton f or model checking which is reduced to the membership problem. We demon strate our framework with the branching-time temporal logic CTL and sh ow that it yields a linear automata-based model-checking algorithm, ma tching the known bound. This is the first time that a model-checking a lgorithm for a branching-time temporal logic has been placed in the au tomata-theoretic framework. (C) 1996 Academic Press, Inc.