The Complexity of Tree Automata and Logics of Programs (Extended Abstract)

Abstract

We investigate the (computational) com- plexity of testing nonemptiness of finite state automata on infinite trees. We show that for tree automata with m states and n pairs nonemptiness can be tested in time O((m~z)~), even though we show that the problem is in general NP-complete. The new nonemptiness algorithm enables us to obtain exponentially improved, essentially tight upper bounds for numerous important modal log- ics of programs, interpreted with the usual semantics over structures generated by binary relations. For example, we show that satisfiability for the full branching time logic CTL* can be tested in deterministic double exponential time. It also follows that satisfiability for Propositional Dynamic Logic with a repetition construct (PDL-delta) and for the Propositional Mu-calculus (L p) can be teated in deterministic single exponential time.