Reasoning about infinite computations (Q1341752)

The authors investigate extensions of temporal logic by connectives defined by finite automata on infinite words, and consider three different logics, corresponding to three different types of acceptance conditions for the automata. It turns out that these logics all have the same expressive power and that their decision problems are all PSPACE- complete. The authors also investigate connectives defined by alternating automata and show that they do not increase the expressive power of the logics or the complexity of the decision problems.