Composing Codensity Bisimulations
CoRR(2024)
摘要
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. ...
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要