Weak Muller Acceptance Conditions for Tree Automata

Over the last decades the theory of automata on infinite objects has been an important source of tools for the specification and the verification of computer programs. Trees are more suitable than words to model nondeterminism and concurrency. In the literature, there are several examples of acceptance conditions that have been proposed for automata on infinite words and then have been fruitfully extended to infinite trees. The type of acceptance condition can influence both the succinctness of the language acceptors and the computational complexity of the decision problems. Here we consider, relatively to automata on infinite trees, two acceptance conditions that are obtained by a relaxation of the Muller acceptance condition: the Landweber and the Muller-Superset conditions. We prove that Muller-Superset tree automata accept the same class of languages as Büchi tree automata. Also, we show that for such languages the minimal Muller-Superset acceptor is at least as succinct as the minimal Büchi acceptor and, in some cases, it can be exponentially more succinct. Landweber tree automata, instead, define a class of languages that is not comparable with that defined by Büchi tree automata. The main result we prove is that the emptiness problem for this class of automata is decidable in polynomial time, and thus we extend the class of automata with a tractable emptiness problem.