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

TL;DR

This paper introduces a unified coalgebraic framework for reward-sensitive bisimulations, capturing both qualitative and quantitative system differences using categorical and fibrational techniques.

Contribution

It develops a novel categorical approach that unifies graded and ungraded reward-sensitive bisimulations within a coalgebraic setting.

Findings

Framework encompasses relation-based and metric-based bisimulations.

Categorical gluing relates graded and ungraded bisimulations.

Unified characterization applies to various system types.

Abstract

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.