Playing with Automata and Trees

Roughly speaking a finite automaton on infinite trees is a finite memory machine that takes as input an infinite node-labelled binary tree and processes it in a top-down fashion as follows. It starts at the root of the tree in its initial state, and picks (possibly nondeterministically) two successor states, one per son, according to the current control state, the letter at the current node and the transition relation. Then the computation proceeds in parallel from both sons, and so on. Hence, a run of the automaton on an input tree is a labelling of this tree by control states of the automaton, that should satisfy the local constrains imposed by the transition relation. A branch in a run is accepting if the ω-word obtained by reading the states along the branch satisfies some acceptance condition (typically an ω-regular condition such as a Büchi or a parity condition). A run is accepting if *all* branches are accepting. Finally, a tree is accepted by the automaton if *there exists* an accepting run over this tree.

Hence, there are three natural  levers on which one can act to define alternative families of tree automata / tree languages.
    - The first lever is local with respect to the run: it is the condition required for a branch to be accepting.
    - The second lever is global with respect to the run: it is the condition required for a run to be accepting.
    - The third lever has to do with the set of runs: it is the condition required for a tree to be accepted (wrt the set of runs over it).

For the usual definition of tree automata the three lever are: parity condition on branches / all branches accepting for run / there exists an accepting run.

In this talk I will mainly focus on the second and third levers and propose variants of them. More precisely (time depending):
    - second lever: count the number of accepting/rejecting branches (cardinality constraint), topologically measure the largeness of the set of accepting/rejecting branches, measure (à la Lebesgue) the set of accepting/rejecting branches.
    - third lever (possibly combined with the second lever): alternating and probabilistic models.
   
In all cases I will show that decidability results can be obtained by extending the well-known equivalence between games and tree automata. This will lead us, in several situations, to leave the usual than perfect-information turn based two-player framework: in particular we will have to deal with stochastic aspects and/or imperfect information.