日本ソフトウェア科学会第 41 回大会 (2024 年度) 講演論文集

Composing Codensity Bisimulations
Mayuko Kori, Kazuki Watanabe, Jurriaan Rot, and Shin-ya Katsumata

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, whereoperations on state-based systems modeled as coalgebras can be elegantly captured through distributive laws
between functors. To prove compositionality, it then suﬃces to show that this distributive law lifts fromsets 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 reﬁne this approach by focusing on so-called codensity lifting of functors, which gives avery 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 simpliﬁed suﬃcient condition. Our suﬃcient 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 isunclear whether the suﬃcient condition holds, and instead we use our setting to give a direct proof ofcompositionality.
In addition, we propose a compositional variant of Komorida et al.’s codensity games for bisimilarities.
A novel feature of this variant is that it can also compose game invariants, which are subsets of winning
positions. Under our suﬃcient condition of the liftability of distributive laws, composed games give analternative proof of the preservation of bisimilarities under the composition.

1 Introduction
Bisimilarity and its many variants are fundamental notions of behavioral equivalence on state-basedsystems. A classical question is whether a given notion of equivalence is compositional w.r.t. algebraic
operations on these systems, such as parallel composition of concurrent systems, product constructions on automata, or other language constructs.
The problem can become particularly challenging
Codensity 双模倣性の合成
郡 茉友子, 渡邉 知樹, 国立情報学研究所, National Institute of Informatics.
郡 茉友子, 渡邉 知樹, 総合研究大学院大学, The Graduate
University for Advanced Studies, SOKENDAI.
Jurriaan Rot, ラドバウド大学, Radboud University.
勝股 審也, 京都産業大学, Kyoto Sangyo University.

when moving from bisimilarity to quantitative notions such as behavioral metrics on probabilisticsystems, where it is already non-trivial to even deﬁne what the right notion of compositionality is(see, e.g. [20] [10]).
To formulate and address the problem of compositionality of algebraic operations on state-based
systems at a high level of generality, a natural formalism is that of coalgebra [14], which is parametricin the type of system, as modeled by a “behavior”
endofunctor F . A key idea, originating in the seminal work of Turi and Plotkin [25], is that composition operations and in fact whole languages specifying state-based systems arise as distributive laws
between F and a functor (or monad) T which models the syntax of a bigger programming language.
In fact, Turi and Plotkin’s abstract GSOS laws areforms of such distributive laws which guarantee
compositionality of strong bisimilarity, generalizing
the analogous result for speciﬁcations in the GSOS
format for labeled transition systems [3]. Distributive laws here precisely capture algebra-coalgebrainteraction needed for compositionality.
The results of Turi and Plotkin speciﬁcally apply
to strong bisimilarity, and not directly to other notions such as similarity or behavioral metrics. Toprove compositionality in these cases, the key observation is that the task is to deﬁne the composition operation at hand not only on state-based
systems but also on relations (or, e.g., pseudometrics). This idea has been formalized in the theoryof coalgebras by requiring a lifting of the distributive law that models the composition operator toa category of relations. The lifting of the behavior functor F then speciﬁes the notion of bisimilarity at hand, and the lifting of the syntax functor
T speciﬁes the way that relations on components
can be combined into bisimulations on the composite system. It has been shown in [5] at a highlevel of generality that the existence of such liftings, referred to in this paper as liftability, ensurescompositionality. The generality there is oﬀered by
the use of liftings of the behavior functor in ﬁbrations which goes back to [13], and which allows us
to study not only relations but also, for instance,coinductively deﬁned metrics or unary predicates(e.g., [16] [23] [12] [4]). But the main challenge here
is to prove liftability; this is what we address in thecurrent paper.
We focus on the codensity lifting of behavior
functors [23], which allows to model a wide variety of coinductive relations and predicates including (bi)similarity but also, for instance, behavioralmetrics; these are commonly referred to as codensity bisimilarity. In fact, the codensity lifting directly generalizes the celebrated Kantorovich distance between probability distributions used to deﬁne, for instance, metrics between probabilistic systems [6]. The codensity lifting is parametric in acollection of modal operators, which makes it on theone hand very ﬂexible and on the other hand much
more structured than arbitrary liftings. Moreover,the codensity lifting allows to characterize codensity
games [16], a generalization of classical bisimilarity
games [24] [7] from transition systems to coalgebras,
and from strong bisimilarity to a wide variety ofcoinductively deﬁned relations, metrics and even
topologies.
In this paper we study compositionality of codensity bisimulations with respect to composition
operators on the underlying state-based systems,
modeled as coalgebras. We model these composition operators as distributive laws between an nary product functor and the behavior functor F ,referred to as one-step composition operators. We
mainly tackle two problems in this paper: 1) How
do we lift the n-ary product functor in order tocapture non-trivial combination of relations, pseudometrics etc? 2) When is a one-step composition
operator liftable?
A key idea for the ﬁrst problem is to use codensity liftings not only to lift the behavior functor F
and get our desired notion of equivalence, but touse another codensity lifting of the product functor, to explain syntactically how relations (or pseudometrics, etc) should be combined from components to the composite system. This combination
can be a simple product between relations, but inmany cases, such as for behavioral metrics, it needs
to be more sophisticated; the ﬂexibility oﬀered by
the codensity lifting helps to deﬁne the appropriate
constructions on relations.
The second problem about liftability then becomes that of proving the existence of a distributive law between codensity liftings. To this end, weexhibit a suﬃcient condition that ensure the existence of this distributive laws, deﬁned in terms oftwo properties: 1) commutation between the underlying modalities that deﬁne codensity liftings, and2) an approximation property, which resembles theone used to prove expressiveness of modal logics
in [17]. Underlying our approach is a combinationof a new generalization of the codensity lifting beyond endofunctors, to allow to lift product functors,
and the adjunction-based decomposition of codensity liftings proposed in [2]. The adjunction-based
approach precisely allows us to arrive at our suﬃcient condition.
We instantiate our approach to pseudometrics ondeterministic automata. We also revisit the compositionality of parallel composition w.r.t. behavioral metrics studied in [10]. In this case it is notclear whether our suﬃcient condition holds; but
the framework nevertheless helps to prove liftability and thereby compositionality.

We further study a compositional variant of codensity games. A key observation is that our composite codensity games consist of positions that aretuples of positions of codensity games for component systems. This design of the composite gamedirectly leads to the compositionality of game invariants, which characterize winning positions. Assuming our suﬃcient condition for the liftability ofdistributive laws, we present an alternative proofof the preservation of bisimilarities along compositions.
In summary, the contributions of this paper are• a generalization of the codensity lifting beyond
endofunctors, which can be used in a special
case to lift products in various ways;• a suﬃcient condition for proving the existenceof a distributive law between codensity liftings,
with several detailed examples;• a composition of codensity games, which also
composes game invariants, and an alternative
proof of the preservation of codensity bisimilarities under our suﬃcient condition;
After the preliminaries, we start the paper with amore detailed overview of our approach.
▷ Related work There is a wide range of resultsin the process algebra literature on proving compositionality and on rule formats that guarantee it,
usually focused on transition systems (see, e.g., [21]for an overview). A full account is beyond thescope of this paper. We focus instead on generality in the type of models and the type of coinductive predicate. Concerning general coalgebraic
frameworks for compositionality, we have alreadymentioned Turi and Plotkin’s abstract GSOS format; the main innovation in the current paper isthat we go beyond bisimilarity by employing thecodensity lifting.
In [5], it is shown that liftings of distributive laws
to ﬁbrations yield so-called compatibility, a property that ensures soundness of up-to techniques,
and which implies compositionality. On the one
hand, if one uses the so-called canonical relation
lifting then all distributive laws lift, but this onlyconcerns strong bisimilarity; on the other hand,in [5] examples beyond bisimilarity are studied but
liftability there is proven on an ad-hoc basis. In
the current paper we identify the codensity lifting
as a sweet spot between the (restricted) canonicalrelation lifting and abstract, unrestricted lifting offunctors, and focus instead on conditions that allow
to prove liftability.
Many bisimilarity notions are known to be characterized by winning positions of certain safety
games, including bisimilarity on Kripke frames [24],probabilistic bisimulation [8] [7], and bisimulation
metric [18]. There are several coalgebraic frameworks [18] [9] that captures such a relationship between games and bisimilarities. In this paper, wefocus on codensity games [16] that are naturally
obtained by codensity liftings and coalgebras.
Codensity liftings are ﬁrst introduced to lift monads across ﬁbrations [15]. They subsume the Kantorivich metric on the Giry monad. In [22], they
are extended to lift endofunctors across CLat⊓ ﬁbrations over Set, and are shown to be a generalization of Baldan et al.’s Kantorovich lifting [1].
Prior to these papers, the monadic property of theKantorovich metric is studied in an unpublishedmanuscript by van Breugel [26]. Codensity liftingsfor endofunctors can be done in other base categories (such as Meas and Vect) without modiﬁcation; see [16]. In [11], the Kantorovich liftings
are studied in the context of Lawvere metric space,and are related with other notions of liftings, suchas lax extensions and (monotone) predicate liftings.
See [19] for further details.
References[ 1 ] Baldan, P., Bonchi, F., Kerstan, H., andKönig, B.: Behavioral Metrics via Functor Lifting, FSTTCS, LIPIcs, Vol. 29, Schloss Dagstuhl Leibniz-Zentrum für Informatik, 2014, pp. 403–415.
[ 2 ] Beohar, H., Gurke, S., König, B., Messing,K., Forster, J., Schröder, L., and Wild, P.: Expressive Quantale-Valued Logics for Coalgebras:
An Adjunction-Based Approach, STACS, LIPIcs,
Vol. 289, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2024, pp. 10:1–10:19.
[ 3 ] Bloom, B., Istrail, S., and Meyer, A. R.:
Bisimulation Can’t be Traced, J. ACM, Vol. 42,No. 1(1995), pp. 232–268.
[ 4 ] Bonchi, F., König, B., and Petrisan, D.: UpTo Techniques for Behavioural Metrics via Fibrations, CONCUR, LIPIcs, Vol. 118, Schloss Dagstuhl- Leibniz-Zentrum für Informatik, 2018, pp. 17:1–17:17.
[ 5 ] Bonchi, F., Petrisan, D., Pous, D., and Rot, J.:
A general account of coinduction up-to, Acta Informatica, Vol. 54, No. 2(2017), pp. 127–190.
[ 6 ] Desharnais, J., Gupta, V., Jagadeesan, R., andPanangaden, P.: Metrics for labelled Markov processes, Theor. Comput. Sci., Vol. 318, No. 3(2004),
pp. 323–354.
[ 7 ] Desharnais, J., Laviolette, F., and Tracol, M.:Approximate Analysis of Probabilistic Processes:Logic, Simulation and Games, QEST, IEEE Computer Society, 2008, pp. 264–273.
[ 8 ] Fijalkow, N., Klin, B., and Panangaden, P.: Expressiveness of Probabilistic Modal Logics, Revisited, ICALP, LIPIcs, Vol. 80, Schloss Dagstuhl Leibniz-Zentrum für Informatik, 2017, pp. 105:1–105:12.
[ 9 ] Ford, C., Milius, S., Schröder, L., Beohar, H.,
and König, B.: Graded Monads and Behavioural
Equivalence Games, LICS, ACM, 2022, pp. 61:1–61:13.
[10] Gebler, D., Larsen, K. G., and Tini, S.: Compositional bisimulation metric reasoning with Probabilistic Process Calculi, Log. Methods Comput. Sci.,
Vol. 12, No. 4(2016).
[11] Goncharov, S., Hofmann, D., Nora, P., Schröder,L., and Wild, P.: Kantorovich Functors and Characteristic Logics for Behavioural Distances, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS
2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS
2023, Paris, France, April 22-27, 2023, Proceedings, Kupferman, O. and Sobocinski, P.(eds.),
Lecture Notes in Computer Science, Vol. 13992,Springer, 2023, pp. 46–67.
[12] Hasuo, I., Kataoka, T., and Cho, K.: Coinductive predicates and ﬁnal sequences in a ﬁbration,
Math. Struct. Comput. Sci., Vol. 28, No. 4(2018),
pp. 562–611.
[13] Hermida, C. and Jacobs, B.: Structural Induction and Coinduction in a Fibrational Setting, Inf.
Comput., Vol. 145, No. 2(1998), pp. 107–152.
[14] Jacobs, B.: Introduction to Coalgebra: TowardsMathematics of States and Observation, Cambridge
Tracts in Theoretical Computer Science, Vol. 59,Cambridge University Press, 2016.
[15] Katsumata, S. and Sato, T.: Codensity Liftings of Monads, CALCO, LIPIcs, Vol. 35, Schloss

Dagstuhl - Leibniz-Zentrum für Informatik, 2015,
pp. 156–170.
[16] Komorida, Y., Katsumata, S., Hu, N., Klin, B.,
Humeau, S., Eberhart, C., and Hasuo, I.: Codensity Games for Bisimilarity, New Gener. Comput.,Vol. 40, No. 2(2022), pp. 403–465.
[17] Komorida, Y., Katsumata, S., Kupke, C., Rot,J., and Hasuo, I.: Expressivity of Quantitative
Modal Logics : Categorical Foundations via Codensity and Approximation, LICS, IEEE, 2021, pp. 1–14.
[18] König, B. and Mika-Michalski, C.: (Metric)
Bisimulation Games and Real-Valued Modal Logics
for Coalgebras, CONCUR, LIPIcs, Vol. 118, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2018,
pp. 37:1–37:17.
[19] Kori, M., Watanabe, K., Rot, J., and Katsumata, S.: Composing Codensity Bisimulations,
LICS, ACM, 2024, pp. 52:1–52:13.
[20] Lago, U. D. and Murgia, M.: Contextual Behavioural Metrics, CONCUR, LIPIcs, Vol. 279,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2023, pp. 38:1–38:17.
[21] Mousavi, M. R., Reniers, M. A., and Groote,
J. F.: SOS formats and meta-theory: 20 years after, Theor. Comput. Sci., Vol. 373, No. 3(2007),
pp. 238–272.
[22] Sprunger, D., Katsumata, S., Dubut, J., and Hasuo, I.: Fibrational Bisimulations and Quantitative
Reasoning, CMCS, Lecture Notes in Computer Science, Vol. 11202, Springer, 2018, pp. 190–213.
[23] Sprunger, D., Katsumata, S., Dubut, J., andHasuo, I.: Fibrational bisimulations and quantitative reasoning: Extended version, J. Log. Comput.,Vol. 31, No. 6(2021), pp. 1526–1559.
[24] Stirling, C.: Bisimulation, Modal Logic andModel Checking Games, Log. J. IGPL, Vol. 7,No. 1(1999), pp. 103–124.
[25] Turi, D. and Plotkin, G. D.: Towards a Mathematical Operational Semantics, LICS, IEEE Computer Society, 1997, pp. 280–291.
[26] van Breugel, F.: The Metric Monad for Probabilistic Nondeterminism, 2005. http://www.cse.
yorku.ca/~franck/research/drafts/monad.pdf.