Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Linear Arboreal Categories

Samson Abramsky, Yoàv Montacute, Nihil Shah

TL;DR

This work develops a theory of linear arboreal categories that captures linear-time behavioural equivalences within a robust categorical framework. By imposing a linearisability condition, the authors construct a linear arboreal subcategory $\mathscr{C}^{L}$ related to the original arboreal category via an adjunction $I\dashv T$, enabling linear variants of existing comonads. They instantiate this with a linear pebble-relation cover $\mathscr{R}^{PL}_{k}(\sigma)$ (and the associated comonad $\mathbb{PR}_k$) and a linear modal arboreal cover $\mathscr{R}^{ML}_{k}(\sigma)$, linking pathwise embeddings to k-pebble strategies and to linear fragments of modal logic. The paper then proves preservation and characterisation results in this linear setting, notably a Rossman-style preservation theorem for linear modal logics and a Van Benthem–Rosen characterisation tying first-order invariance under labelled trace equivalence to linear fragments $\exists{\curlywedge}ML_k$ with $k=2^{r}$. Overall, the work unifies linear-time behavioural relations with a category-theoretic account, yielding new tools for trace preservation, logic fragments, and model-theoretic characterisations.

Abstract

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.

Linear Arboreal Categories

TL;DR

This work develops a theory of linear arboreal categories that captures linear-time behavioural equivalences within a robust categorical framework. By imposing a linearisability condition, the authors construct a linear arboreal subcategory related to the original arboreal category via an adjunction , enabling linear variants of existing comonads. They instantiate this with a linear pebble-relation cover (and the associated comonad ) and a linear modal arboreal cover , linking pathwise embeddings to k-pebble strategies and to linear fragments of modal logic. The paper then proves preservation and characterisation results in this linear setting, notably a Rossman-style preservation theorem for linear modal logics and a Van Benthem–Rosen characterisation tying first-order invariance under labelled trace equivalence to linear fragments with . Overall, the work unifies linear-time behavioural relations with a category-theoretic account, yielding new tools for trace preservation, logic fragments, and model-theoretic characterisations.

Abstract

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.
Paper Structure (17 sections, 18 theorems, 39 equations, 3 figures)

This paper contains 17 sections, 18 theorems, 39 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Set notation
  4. Category Theory
  5. Kripke frames and transition systems
  6. Arboreal categories
  7. Linear arboreal categories
  8. Linear adjunction
  9. Linear behavioural relations
  10. The pebbling linear arboreal cover
  11. Back-and-forth games
  12. Arboreal categories case
  13. Linear arboreal categories case
  14. The modal linear arboreal cover
  15. Preservation theorems
  16. ...and 2 more sections

Key Result

lemma 1

Let $\mathscr C$ be a linearisable arboreal category and $X \in \mathscr C$ be linearly path-generated. The the following statements hold

Figures (3)

  • Figure 1: Trace equivalent transition systems that are not labelled trace equivalent
  • Figure 2: bijective labelled trace equivalent but non-bisimilar transition systems
  • Figure :

Theorems & Definitions (59)

  • definition 1: lifting property
  • definition 2: weak factorisation system
  • definition 3
  • definition 4: path
  • definition 5: path category arborealJournal
  • definition 6: arboreal category
  • definition 7: arboreal cover
  • definition 8: resource indexing
  • definition 9
  • definition 10: linear arboreal category
  • ...and 49 more