Branching-Time Temporal Logic and Tree Automata

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. The close connection between linear-time temporal logics and the theory of automata on infinite words has been an active area of research. In particular, automata-theoretic techniques have proven to be an effective approach to linear-time model checking. On the other hand, for branching-time temporal logics, current automata-theoretic techniques involve an exponential blow-up, making them essentially useless for model-checking. In this paper we present an automata-theoretic framework for branching-time model checking. We introduce simultaneous 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 ψ we associate an automaton that accepts exactly these simultaneous trees that originate from structures that satisfy ψ. This enables to use the automaton for model checking which is reduced to the membership problem. We demonstrate our framework with the branching-time temporal logic CTL and show that it yields a linear automata-based model-checking algorithm, matching the known bound. This is the first time that a model-checking algorithm for a branching-time temporal logic has been placed in the automatatheoretic framework. © 1996 Academic Press, Inc.