Game comonads provide a categorical syntax-free approach to finite model theory, and their Eilenberg-Moore coalgebras typically encode important combinatorial parameters of structures. In this paper, we develop a framework whereby the essential properties of these categories of coalgebras are captured in a purely axiomatic fashion. To this end, we introduce arboreal categories, which have an intrinsic process structure, allowing dynamic notions such as bisimulation and back-and-forth games, and resource notions such as number of rounds of a game, to be defined. These are related to extensional or "static" structures via arboreal covers, which are resource-indexed comonadic adjunctions. These ideas are developed in a general, axiomatic setting, and applied to relational structures, where the comonadic constructions for pebbling, Ehrenfeucht-Fra\"iss\'e and modal bisimulation games recently introduced by Abramsky et al. are recovered, showing that many of the fundamental notions of finite model theory and descriptive complexity arise from instances of arboreal covers.

翻译：博弈余单子为有限模型理论提供了一种无范畴语法的语法无关方法，其Eilenberg-Moore余代数通常编码结构的重要组合参数。在本文中，我们建立了一个框架，以纯粹公理化的方式捕获这些余代数范畴的本质属性。为此，我们引入了树状范畴，这类范畴具有内在的过程结构，使得诸如互模拟和往返博弈等动态概念，以及博弈轮数等资源概念得以定义。这些概念通过树状覆盖（即资源索引的余单子伴随）与外延式或“静态”结构相关联。我们在一般性公理化框架中发展这些思想，并将其应用于关系结构，从而重新获得了Abramsky等人近期引入的针对跳棋、Ehrenfeucht-Fraïssé以及模态互模拟博弈的余单子构造，表明了有限模型理论与描述复杂性的许多基本概念皆源自树状覆盖的实例。