Composing Codensity Bisimulations
Mayuko Kori, Kazuki Watanabe, Jurriaan Rot, Shin-ya Katsumata
TL;DR
The paper develops a unified, category-theoretic approach to compositionality of behavioral equivalence for state-based systems via codensity liftings. It generalizes codensity liftings beyond endofunctors, introduces a 2-categorical decomposition to analyze liftability, and provides a concrete sufficient condition for lifting a distributive law between codensity liftings to ensure compositionality of both qualitative and quantitative (e.g., probabilistic) notions. The framework is instantiated to deterministic automata and various probabilistic models, yielding bisimulation, similarity, and bisimulation metrics for product systems, while also constructing composite codensity games to reason about invariants and preservation. The methods offer a flexible, modular toolkit for deriving compositional proofs in a broad range of coalgebraic settings and metrics, with clear transfer principles for modalities across fibrations and potential extensions to higher-order GSOS frameworks.
Abstract
Proving compositionality of behavioral equivalence on state-based systems with respect to algebraic operations is a classical and widely studied problem. We study a categorical formulation of this problem, where operations on state-based systems modeled as coalgebras can be elegantly captured through distributive laws between functors. To prove compositionality, it then suffices to show that this distributive law lifts from sets to relations, giving an explanation of how behavioral equivalence on smaller systems can be combined to obtain behavioral equivalence on the composed system. In this paper, we refine this approach by focusing on so-called codensity lifting of functors, which gives a very generic presentation of various notions of (bi)similarity as well as quantitative notions such as behavioral metrics on probabilistic systems. The key idea is to use codensity liftings both at the level of algebras and coalgebras, using a new generalization of the codensity lifting. The problem of lifting distributive laws then reduces to the abstract problem of constructing distributive laws between codensity liftings, for which we propose a simplified sufficient condition. Our sufficient condition instantiates to concrete proof methods for compositionality of algebraic operations on various types of state-based systems. We instantiate our results to prove compositionality of qualitative and quantitative properties of deterministic automata. We also explore the limits of our approach by including an example of probabilistic systems, where it is unclear whether the sufficient condition holds, and instead we use our setting to give a direct proof of compositionality. ...