Arboreal categories, introduced by Abramsky and Reggio, axiomatise categories with tree-shaped objects. These categories provide a categorical language for formalising behavioural notions such as simulation, bisimulation, and resource-indexing. In this paper, we strengthen the axioms of an arboreal category to exclude `branching' behaviour, obtaining a notion of `linear arboreal category'. We then demonstrate that every arboreal category satisfying a linearisability condition has an associated linear arboreal subcategory related via an adjunction. This identifies the relationship between the pebble-relation comonad, of Montacute and Shah, and the pebbling comonad, of Abramsky, Dawar, and Wang, and generalises it further. As another outcome of this new framework, we obtain a linear variant of the arboreal category for modal logic. By doing so we recover different linear-time equivalences between transition systems as instances of their categorical definitions. We conclude with new preservation and characterisation theorems relating trace inclusion and trace equivalence with different linear fragments of modal logic.

翻译：由Abramsky和Reggio引入的树状范畴公理化地描述了具有树形对象的范畴。这些范畴为形式化模拟、互模拟和资源索引等行为概念提供了范畴论语言。本文通过强化树状范畴的公理以排除“分支”行为，从而得到“线性树状范畴”的概念。我们随后证明，每个满足线性化条件的树状范畴都具有一个通过伴随关系关联的线性树状子范畴。这一结论明确了Montacute和Shah提出的卵石关系余单子与Abramsky、Dawar和Wang提出的卵石余单子之间的关系，并进一步推广了该关系。作为这一新框架的另一成果，我们得到了模态逻辑树状范畴的线性变体。通过这种方式，我们将过渡系统之间不同的线性时间等价关系恢复为其范畴定义的实例。最后，我们提出了新的保持性与刻画定理，这些定理将迹包含与迹等价关联于模态逻辑的不同线性片段。