REASONING ABOUT INFINITE COMPUTATIONS

We investigate extensions of temporal logic by connectives defined by finite automata on infinite words. We consider three different logics, corresponding to three different types of acceptance conditions (fini te, looping, and repeating) for the automata. It turns out, however th at these logics all have the same expressive power and that their deci sion problems are all PSPACE-complete. We also investigate connectives defined by alternating automata and show that they do not increase th e expressive power of the logic or the complexity of the decision prob lem. (C) 1994 Academic Press, Inc.