Arbitrary-arity Tree Automata and QCTL

TL;DR

This paper introduces EU-automata for infinite trees of arbitrary arity, providing algorithms for classical operations, and applies these automata to improve decision procedures and translation techniques for QCTL and MSO logic.

Contribution

It develops EU-automata for arbitrary-arity trees and applies them to achieve optimal complexity decision procedures and quantifier alternation reductions in QCTL and MSO.

Findings

Optimal complexity decision procedures for QCTL satisfiability and model checking.

Algorithm for translating QCTL formulas with multiple quantifier alternations to fewer alternations.

MSO formulas can be translated into formulas with at most four quantifier alternations.

Abstract

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.