On automata on infinite trees (Q1186604)

It is well-known the importance of the theory of automata on infinite objects in the study of decision problems and in logic of programs, in particular when dealing with nonterminating computations. In this paper the infinite objects are infinite trees and the authors are interested in the relationship between Büchi and Muller automata (on infinite trees). More precisely, the aim of the paper is to analyze acceptance conditions for sets of trees accepted by such a automata. The authors define a new model of infinite tree automata, i.e. limited Muller (1-Muller) automaton. The 1-Muller automata have the same structure of Muller automata, but their acceptance condition is more restrictive. For an accepting run of an 1-Muller tree automaton on a tree it is required that along each path a set of final states is entered, not left in future by any path coming out and repeated completely again and again. It is shown that the sets of infinite trees accepted by 1-Muller automata are accepted by Büchi and Muller automata. A counterexample shows that the tree languages accepted by 1-Muller automata form a proper subclass of languages accepted by Büchi automata. Then the authors extend the notion of control automata (introduced by Rabin) to the case that more than one language is used to control the set of infinite words that label each path of a successful run of a tree. It is shown that using Boolean operators in defining acceptance conditions for control automata, a characterization for M-automata, introduced by Nivat and Saoudi (1988), in terms of control automata can be given. Finally, a new definition of control automaton, the And-control automaton, is introduced and some properties are investigated.