Victor Valls, Panagiotis Promponas, et al.
IEEE Communications Magazine
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, nonemptiness can be tested in deterministic time (mn)O(n); however, it is shown that the problem is in general NP-complete (or co-NP-complete, respectively). The new nonemptiness algorithm yields exponentially improved, essentially tight upper bounds for numerous important modal logics of programs, interpreted with the usual semantics over structures generated by binary relations. For example, it follows that satisfiability for the full branching time logic CTL* can be tested in deterministic double exponential time. Another consequence is that satisfiability for propositional dynamic logic (PDL) with a repetition construct (PDL-delta) and for the propositional Mu-calculus (Lμ) can be tested in deterministic single exponential time.
Victor Valls, Panagiotis Promponas, et al.
IEEE Communications Magazine
A. Gupta, R. Gross, et al.
SPIE Advances in Semiconductors and Superconductors 1990
William Hinsberg, Joy Cheng, et al.
SPIE Advanced Lithography 2010
Michael C. McCord, Violetta Cavalli-Sforza
ACL 2007