The complexity of tree automata and logics of programs

The complexity of testing nonemptiness of finite state automata on infinite trees is investigated. It is shown that for tree automata with the pairs ( or complemented pairs) acceptance condition having m states and n pairs, no nemptiness can be tested in deterministic time (mn)(O(n)); however, it is s hown that the problem is in general NP-complete (or co-NP-complete, respect ively). The new nonemptiness algorithm yields exponentially improved, essen tially tight upper bounds for numerous important modal logics of programs, interpreted with the usual semantics over structures generated by binary re lations. For example, it follows that satisfiability for the full branching time logic CTL* can be tested in deterministic double exponential time. An other consequence is that satisfiability for propositional dynamic logic (P DL) with a repetition construct (PDL-delta) and for the propositional Mu-ca lculus (L mu) can be tested in deterministic single exponential time.