LIP, ENS Lyon
Date(s) : 15/10/2015 iCal
11 h 00 min - 12 h 00 min
We propose a notion of morphism between tree automata based on game semantics. These morphisms are winning strategies on a synchronous restriction of the linear implication between acceptance games of automata seen as simple games.
Our setting allows in particular to define substitution functors based on a suitable notion of synchronous tree function. This leads to split indexed categories, and by restricting to tree functions issued from maps on alphabets, this gives a fibration of tree automata.
These fibrations can be equipped with a symmetric monoidal structure issued from the synchronous product of automata. Moreover, a variant of the usual projection operation on automata leads to an existential quantification in the fibered sense.
Thanks to that structure, we can show that our notion of morphism is correct, in the sense that it respects language inclusion, and in a weaker sense also complete.