Abstract
In recent works, we proposed fibred monoidal closed categories of (alternating) automata on infinite tree. These categories are based on the principle "Automata as types, executions as morphisms". They are built on categories of simple games (from game semantics), with a suitable restriction to ``synchronous'' strategies. Following the usual pattern of (categorical approaches to) Gödel's Dialectica interpretation, this synchronous restriction allows to internalize homsets into automata (in the sense of monoidal closure). These categories are meant to provide a basis for realizability models of constructive versions of MSO on infinite trees. In order to correctly interpret the quantifications of MSO (implemented via the usual operation of projection), we rely on the usual simulation of alternating tree automata by non-deterministic ones. This allows to interpret *deduction rules* for the usual exponential connective '!' of linear logic, but unfortunately not in a categorical way (the operator '!' does not preserve composition). In this talk, we plan to discuss (a) how the above mentioned games could be equipped with real '!' modalities (forgetting about their internalization in finite state automata), which amount to devise free (right adjoint) functors to suitable categories of commutative comonoids and/or (b) relations of our game models (when restricted to *non-deterministic* tree automata) to some categorical models of concurrency.