A BRANCHING TIME LOGIC WITH PAST OPERATORS

An expression branching time logic is introduced. Its power allows us to describe the local structure of the underlying graph of the computation. The logic's linear operators correspond to all the relations definable by finite automata and are able to express the computations in the past, in addition to the computations in the future. In particular the logic contains as a fragment the ordinary temporal logic of branching time. It is shown that the logic is decidable. The proof is based on reduction to the emptiness problem for graph automata. (C) 1994 Academa Press, Inc.