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.} }
Feedback for Dagstuhl Publishing