Reference. A Framework for Coalgebraic Reward-Sensitive Bisimulation (Extended Version)

Pedro H. Azevedo de Amorim, Mayuko Kori, Koko Muroya · arXiv · 2026 · coalgebra · arXiv
In this paper we present a framework for modelling reward-sensitive bisimulations, that is, bisimulations that account for quantitative differences such as accumulated rewards. To capture both qualitative and quantitative aspects uniformly, we consider two interacting notions of bisimulation: a graded variant that tracks bounded reward differences, and an ungraded one that abstracts from them. Our characterization of these notions is done in the fibrational and coalgebraic approach to (bi)simulation initiated by Hermida and Jacobs. To formally relate the graded and ungraded notions, we deploy categorical gluing, a standard technique in categorical logic. Furthermore, we show that this construction interacts well with standard coalgebra concepts, such as final coalgebras, and that it yields a unified characterization in terms of combined notions of bisimulations under mild assumptions. In order to demonstrate the versatility of our approach, we show how it encompasses various bisimulation notions for different kinds of systems, including relation-based bisimulations for automata with rewards and metric-based notions of bisimulations for labelled Markov processes.

Cite
Cite as @amorim-2026-a (helia, typst) · \cite{amorim-2026-a} (LaTeX)
BibTeX
bibtex · 8 lines
@misc{amorim-2026-a,
  author = {Azevedo de Amorim, Pedro Henrique and Mayuko Kori and Koko Muroya},
  title = {A Framework for Coalgebraic Reward-Sensitive Bisimulation (Extended Version)},
  year = {2026},
  month = {4},
  eprint = {2604.01103},
  archiveprefix = {arXiv}
}
hayagriva YAML (typst)
yaml · 12 lines
amorim-2026-a:
  type: misc
  title: A Framework for Coalgebraic Reward-Sensitive Bisimulation (Extended Version)
  author:
  - name: Amorim
    given-name: Pedro Henrique
    prefix: Azevedo de
  - Kori, Mayuko
  - Muroya, Koko
  date: 2026-04
  serial-number:
    arxiv: '2604.01103'
Download: amorim-2026-a.bib · amorim-2026-a.yml
Cites 30 works (1 here)
With notes (1)

Logical relations for call-by-push-value models, via internal fibrations in a 2-category amorim_kura_saville_2025LICS · 2025

We give a denotational account of logical relations for call-by-push-value (CBPV) in the fibrational style of Hermida, Jacobs, Katsumata and others. Fibrations – which axiomatise the usual notion of sets-with-relations – provide a clean framework for constructing new, logical relations-style, models. Such models can then be used to study properties such as effect simulation.

Extending this picture to CBPV is challenging: the models incorporate both adjunctions and enrichment, making the appropriate notion of fibration unclear. We handle this using 2-category theory. We identify an appropriate 2-category, and define CBPV fibrations to be fibrations internal to this 2-category which strictly preserve the CBPV semantics.

Next, we develop the theory so it parallels the classical setting. We give versions of the codomain and subobject fibrations, and show that new models can be constructed from old ones by pullback. The resulting framework enables the construction of new, logical relations-style, models for CBPV.

Finally, we demonstrate the utility of our approach with particular examples. These include a generalisation of Katsumata’s ⊤⊤-lifting to CBPV models, an effect simulation result, and a relative full completeness result for CBPV without sum types.

Web · arXiv
External (29)
amorim-2026-a reference entries/refs/amorim-2026-a/amorim-2026-a.hel