Automata on infinite trees with counting constraints

Abstract

We investigate finite automata on infinite trees with the usual Muller criterion for the success of an infinite computation path, but with the acceptance paradigm modified in that not all the computation paths need to be successful. Instead, it is required that the number of successfnl paths must belong to a specified set of cardinals Γ. We show that Muller automata with the acceptance constraint of the form “there are at least γ accepting paths” can be always simulated by tree automata with a weaker criterion for successful paths, namely Büchi acceptance condition. We also show that this is the most general class of constraints for which a simulation by Büichi automata is always possible. Next, we characterize the maximal class of constraints which can be simulated by classical Muller automata (known to be more powerful than Büchi automata). The condition requiered of the set Γ there, is that the intersection with natural numbers forms a recognizable set. Finally, we exhibit a set of trees which is recognized by a classical Büchi automaton but fails to be recognized by any Muller automaton with a non trivial cardinality constraint (i.e., except for Γ = 0).