AUTOMATA ON INFINITE-TREES WITH COUNTING CONSTRAINTS

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 successful paths must belong to a specified set of cardinals Gamma. We show that Muller automata with the acceptance constraint of the form ''there are at least gamma accepting paths'' can be always simulated by tree automata with a weaker criterion for successful paths, namely, the Buchi acceptance condition. We also show that this is the most general class of constraints for which a simulation by Buchi 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 Buchi automata). The condition required of the set Gamma 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 Buchi automaton but fails to be recognized by any Muller automaton with a non trivial cardinality constraint ( i.e., except for Gamma = 0). (C) 1995 Academic Press, Inc.