We introduce a new class of automata (which we coin EU-automata) running on infininte trees of arbitrary (finite) arity. We develop and study several algorithms to perform classical operations (union, intersection, complement, projection, alternation removal) for those automata, and precisely characterise their complexities. We also develop algorithms for solving membership and emptiness for the languages of trees accepted by EU-automata. We then use EU-automata to obtain several algorithmic and expressiveness results for the temporal logic QCTL (which extends CTL with quantification over atomic propositions) and for MSO. On the one hand, we obtain decision procedures with optimal complexity for QCTL satisfiability and model checking; on the other hand, we obtain an algorithm for translating any QCTL formula with k quantifier alternations to formulas with at most one quantifier alternation, at the expense of a $(k + 1)$-exponential blow-up in the size of the formulas. Using the same techniques, we prove that any MSO formula can be translated into a formula with at most four quantifier alternations (and only one second-order-quantifier alternation), this time with a $(k + 2)$-exponential blow-up in the size of the formula.

翻译：我们引入了一类新型自动机（称为EU-自动机），它运行在任意（有限）元数的无限树上。我们为这类自动机开发并研究了若干算法，以执行经典运算（并、交、补、投影、交替移除），并精确刻画了它们的复杂度。我们还开发了算法来解决EU-自动机所接受的树语言的成员性和空性问题。随后，我们利用EU-自动机为时序逻辑QCTL（通过原子命题上的量化扩展了CTL）和MSO获得了若干算法性和表达力方面的结果。一方面，我们为QCTL的可满足性和模型检测获得了具有最优复杂度的判定过程；另一方面，我们获得了一种算法，可将任何具有k个量词交替的QCTL公式转换为至多具有一个量词交替的公式，代价是公式规模产生$(k + 1)$-指数级的膨胀。使用相同技术，我们证明了任何MSO公式都可以转换为至多具有四个量词交替（且仅有一个二阶量词交替）的公式，此时公式规模产生$(k + 2)$-指数级的膨胀。