A Framework for Coalgebraic Reward-Sensitive Bisimulation (Extended Version)
This work addresses the need for unified bisimulation models in theoretical computer science, particularly for systems with quantitative aspects, but it is incremental as it builds on existing coalgebraic approaches.
The paper tackles the problem of modeling reward-sensitive bisimulations that account for quantitative differences like accumulated rewards, by developing a framework using graded and ungraded bisimulations with categorical gluing, and demonstrates its versatility across systems such as automata with rewards and labelled Markov processes.
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.