Creative Commons Attribution 3.0 Unported license
We propose a notion of morphisms between tree automata based on game semantics. Morphisms are winning strategies on a synchronous restriction of the linear implication between acceptance games. This leads to split indexed categories, with substitution based on a suitable notion of synchronous tree function. By restricting to tree functions issued from maps on alphabets, this gives a fibration of tree automata. We then discuss the (fibrewise) monoidal structure issued from the synchronous product of automata. We also discuss how a variant of the usual projection operation on automata leads to an existential quantification in the fibered sense. Our notion of morphism is correct (it respects language inclusion), and in a weaker sense also complete.
@InProceedings{riba:LIPIcs.TLCA.2015.302,
author = {Riba, Colin},
title = {{Fibrations of Tree Automata}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {302--316},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.302},
URN = {urn:nbn:de:0030-drops-51719},
doi = {10.4230/LIPIcs.TLCA.2015.302},
annote = {Keywords: Tree automata, Game semantics, Categorical logic.}
}