In this paper we present a framework for modelling \emph{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.

翻译：本文提出一个建模奖励敏感双模拟（reward-sensitive bisimulations）的框架，这类双模拟能够刻画累积奖励等定量差异。为统一处理定性与定量方面，我们考虑两种交互作用的双模拟概念：一种是有界奖励差异的渐变变体，另一种是抽象此类差异的非渐变变体。我们借鉴Hermida与Jacobs开创的纤维化与余代数方法对这些概念进行刻画，并通过范畴粘合（这一范畴逻辑中的标准技术）在形式上建立渐变与非渐变概念的联系。进一步，我们证明该构造与最终余代数等标准余代数概念具有良好交互性，并在温和假设下生成以组合双模拟概念为核心的统一刻画。为展示方法的通用性，我们阐释其如何涵盖不同系统类型的多种双模拟概念，包括基于关系的奖励自动机双模拟，以及基于度量的带标号马尔可夫过程双模拟。