Codensity Games for Bisimilarity

Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been extended in various ways, such as bisimulation metric between probabilistic systems. An important feature of bisimilarity is its game-theoretic characterization, where Spoiler and Duplicator play against each other; extension of bisimilarity games to quantitative settings has been actively pursued too. In this paper, we present a general framework that uniformly describes game characterizations of bisimilarity-like notions. Our framework is formalized categorically using fibrations and coalgebras. In particular, our characterization of bisimilarity in terms of fibrational predicate transformers allows us to derive what we call codensity bisimilarity games: a general categorical game characterization of bisimilarity. Our framework covers known bisimilarity-like notions (such as bisimulation metric and bisimulation seminorm) as well as new ones (including what we call bisimulation topology).

Not applicable.

Not applicable.

Y.K., S.K., C.E., and I.H. are supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST. Y.K. is supported by JSPS KAKENHI Grant Number JP21J13334. S.K. and I.H. are supported by the JSPS-Inria Bilateral Joint Research Project CRECOGI, and JST Moonshot R &D No. JPMJMS2033. I.H. is supported by Grants-in-Aid No. 15KT0012 and 15K11984, JSPS. B.K. is supported by the ERC under the European Union’s Horizon 2020 research and innovation programme (ERC consolidator grant LIPA, agreement no. 683080). Part of the work was done during N.H.’s internship, S.H.’s internship, and B.K.’s visit, at National Institute of Informatics, Tokyo, Japan.

Y.K., S.K., C.E., and I.H. are supported by ERATO HASUO Metamathematics for Systems Design Project (no. JPMJER1603), JST. Y.K. is supported by JSPS KAKENHI Grant Number JP21J13334. S.K. and I.H. are supported by the JSPS-Inria Bilateral Joint Research Project CRECOGI, and JST Moonshot R &D no. JPMJMS2033. I.H. is supported by Grants-in-Aid No. 15KT0012 and 15K11984, JSPS. B.K. is supported by the ERC under the European Union’s Horizon 2020 research and innovation programme (ERC consolidator grant LIPA, agreement no. 683080).

Authors and Affiliations

1. National Institute of Informatics, Tokyo, Japan

   Yuichi Komorida, Shin-ya Katsumata, Clovis Eberhart & Ichiro Hasuo

2. The Graduate University for Advanced Studies, SOKENDAI, Hayama, Kanagawa, Japan

   Yuichi Komorida & Ichiro Hasuo

3. University of Oxford, Oxford, UK

   Nick Hu & Bartek Klin

4. École Normale Supérieure de Lyon, Lyon, France

   Samuel Humeau

5. Japanese-French Laboratory for Informatics, Tokyo, Japan

   Clovis Eberhart

Corresponding authors

Correspondence to Yuichi Komorida, Shin-ya Katsumata or Ichiro Hasuo.

Conflict of interest

Not applicable.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

To Masami Hagiya on the occasion of his \(2^6\)th birthday. Masami’s research career has been a role model for us theoretical computer scientists who seek real-world impact through the power of logic. He has shown through his works that one good use of logical abstraction is to tame new computing paradigms. The current work draws inspiration from this, and uses logical (and categorical) abstraction to establish a uniform understanding of various bisimilarity-like notions that otherwise look very different from each other.

Appendix 1: Direct Proof of Equivalence of the Two Game Notions Characterizing Probabilistic Bisimilarity (Tables 2 and 4)

1.1 Table 4 \(\leadsto\) Table 2

Assume that Duplicator wins Table 4 from (x, y), and let Spoiler play some Z in Table 2. There are two cases to consider which are essentially identical, but we write them down separately for reference.

• If \(\tau (x,Z)>\tau (y,Z)\) then we make Spoiler select \(s=x\) and play Z in Table 4. To this Duplicator responds with some \(Z'\supseteq Z\) such that \(\tau (x,Z)\le \tau (y,Z')\), which implies that \(Z'\ne Z\). Pick any \(y'\in Z'\setminus Z\) and play it as Spoiler in Table 4; when Duplicator responds with some \(x'\in Z\), play the pair \(x'\) and \(y'\) as Duplicator in Table 2.

• If \(\tau (x,Z)<\tau (y,Z)\) then we make Spoiler select \(s=y\) and play Z in Table 4. To this Duplicator responds with some \(Z'\supseteq Z\) such that \(\tau (y,Z)\le \tau (x,Z')\), which implies that \(Z'\ne Z\). Pick any \(y'\in Z'\setminus Z\) and play it as Spoiler in Table 4; when Duplicator responds with some \(x'\in Z\), play the pair \(x'\) and \(y'\) as Duplicator in Table 2.

1.2 Table 2 \(\leadsto\) Table 4

This is a less straightforward implication. A winning strategy for Duplicator in Table 4 is built not from a single strategy in Table 2, but rather from an entire collection of winning positions.

Formally, assume that Duplicator wins Table 2 from (x, y), and let Spoiler choose \(s\in \{x,y\}\) and play some Z in Table 4. We define

One basic observation is that \(Z\subseteq \bar{Z}\), since Duplicator wins from all positions of the form (w, w). As a result, we have

Another observation is that Spoiler wins Table 2 from the position \(\bar{Z}\). To see this, consider any Duplicator’s response \(x'\in \bar{Z}\), \(y'\not \in \bar{Z}\). Then there is some \(v\in Z\) such that Duplicator wins Table 2 from \((v,x')\). If Duplicator could win Table 2 from \((x',y')\) then she could win from \((v,y')\) as well, which contradicts the assumption that \(y'\not \in \bar{Z}\).

Since we assume that Duplicator wins Table 2 from (x, y), \(\bar{Z}\) cannot be a legal move for Spoiler from (x, y), hence

Together with (A1) this implies that

so \(Z'=\bar{Z}\) is a legal move for Duplicator in the stage (ii) of Table 4, no matter if Spoiler chose \(s=x\) or \(s=y\) in the stage (i). To this, in the stage (iii) Spoiler replies with some \(y'\in \bar{Z}\setminus Z\). By the definition of \(\bar{Z}\), there is some \(v\in Z\) such that Duplicator wins Table 2 from \((v,y')\), so Duplicator can respond with \(x'=v\).

Appendix 2: Introduction to \(\mathbf {CLat}_{\sqcap }\)-Fibration

We present an introduction to (\(\mathbf {CLat}_{\sqcap }\)-)fibrations, starting from a functor \(F_{\mathbb {E}}:\mathbb {C}^{\mathrm {op}}\rightarrow \mathbf {CLat}_{\sqcap }\). The relevance of the latter is explained in Sect. 2.2. For details, readers are referred to [33].

1.1 The Grothendieck Construction

In general, the equivalence between index categories \(\mathbb {C}^{\mathrm {op}}\rightarrow \mathbf {Cat}\) and fibrations is well-known. Here we sketch the Grothendieck construction from the former to the latter, focusing the special case of \(\mathbb {C}^{\mathrm {op}}\rightarrow \mathbf {CLat}_{\sqcap }\) and \(\mathbf {CLat}_{\sqcap }\)-fibrations. Its idea is to “patch up” the family \(\bigl (F_{\mathbb {E}}X\bigr )_{X\in \mathbb {C}}\) of complete lattices, and form a big category \(\mathbb {E}\), as shown in Fig. 2.

On the right-hand side in Fig. 2, we add some arrows (denoted by \(\dashrightarrow\)) so that we have an arrow \((F_{\mathbb {E}} f)(Q)\rightarrow Q\) in \(\mathbb {E}\) for each \(Q\in F_{\mathbb {E}} Y\). (On the left-hand side, the correspondence depicts the action of the map \(F_{\mathbb {E}} f\).) The diagram in \(\mathbb {E}\) in Fig. 2 should be understood as a Hasse diagram: those arrows which arise from composition are not depicted.

Grothendieck construction

Full size image

Definition B.1

(The Grothendieck construction) Given a functor \(F_{\mathbb {E}}:\mathbb {C}^{\mathrm {op}}\rightarrow \mathbf {CLat}_{\sqcap }\), we define the category \(\mathbb {E}\) as follows.

• An object is a pair (X, P) of an object \(X\in \mathbb {C}\) and an element \(P\in F_{\mathbb {E}} X\); and

• An arrow \(f:(X,P)\rightarrow (Y,Q)\) is an arrow \(f:X\rightarrow Y\) in \(\mathbb {C}\) such that

  $$\begin{aligned} P\sqsubseteq (F_{\mathbb {E}} f)(Q). \end{aligned}$$

  Here \(\sqsubseteq\) refers to the order of the complete lattice \(F_{\mathbb {E}} X\).

Thus arises a category \(\mathbb {E}\) that incorporates the following.

• the order structure of each of the posets \((F_{\mathbb {E}} X)_{X\in \mathbb {C}}\), and

• the pullback structure by \((F_{\mathbb {E}} f)_{f:\mathbb {C}-\text {arrow}}\).

For fixed \(X\in \mathbb {C}\), the objects of the form (X, P) and the arrows \(\mathrm {id}_{X}\) between them form a subcategory of \(\mathbb {E}\). This is denoted by \(\mathbb {E}_{X}\) and called the fiber over X. It is obvious that \(\mathbb {E}_{X}\) is a poset that is isomorphic to \(F_{\mathbb {E}} X\).

Moreover, there is a canonical projection functor \(p:\mathbb {E}\rightarrow \mathbb {C}\) that carries (X, P) to X.

1.2 Formal Definition of \(\mathbf {CLat}_{\sqcap }\)-Fibration

We axiomatize those structures which arise in the way described above.

Definition 9.1

(\(\mathbf {CLat}_{\sqcap }\)-fibration) A \(\mathbf {CLat}_{\sqcap }\)-fibration \(\mathbb {E} \xrightarrow {p} \mathbb {C}\) consists of two categories \(\mathbb {E},\mathbb {C}\) and a functor \(p:\mathbb {E}\rightarrow \mathbb {C}\), that satisfy the following properties.

• Each fiber \(\mathbb {E}_{X}\) is a complete lattice. Here the fiber \(\mathbb {E}_{X}\) for \(X\in \mathbb {C}\) is the subcategory of \(\mathbb {E}\) consisting of the following data: objects \(P\in \mathbb {E}\) such that \(pP=X\); and arrows \(f:P\rightarrow Q\) such that \(pf=\mathrm {id}_{X}\) (such arrows are said to be vertical).

• Given \(f:X\rightarrow Y\) in \(\mathbb {C}\) and \(Q\in \mathbb {E}_{Y}\), there is an object \(f^{*} Q\in \mathbb {E}_{X}\) and an \(\mathbb {E}\)-arrow \(\overline{f}Q:f^{*}Q\rightarrow Q\) with the following universal property. For any \(P\in \mathbb {E}_{X}\) and \(g:P\rightarrow Q\) in \(\mathbb {E}\), if \(pg=f\) then g factors through \(\overline{f}(Q)\) uniquely via a vertical arrow. That is, there exists unique \(g'\) such that \(g=\overline{f}(Q)\mathbin {\circ }g'\) and \(pg'=\mathrm {id}_{X}\):

  

• The correspondences \((\_)^{*}\) and \(\overline{(\_)}\) are functorial:

  $$\begin{aligned} \mathrm {id}_{Y}^{*}Q&=Q,&(g\mathbin {\circ }f)^{*}(Q)&= f^{*}(g^{*}Q),\\ \overline{\mathrm {id}_{Y}}(Q)&=\mathrm {id}_{Q},&\overline{g\mathbin {\circ }f}(Q)&= \overline{g}Q\mathbin {\circ }\overline{f}(g^{*}Q). \end{aligned}$$

  The last equality can be depicted as follows:

  

The category \(\mathbb {E}\) is called the total category of the fibration; \(\mathbb {C}\) is the base category. The arrow \(\overline{f}Q:f^{*}Q\rightarrow Q\) is called the Cartesian lifting of f and Q. An arrow in \(\mathbb {E}\) is Cartesian if it coincides with \(\overline{f}Q\) for some f and Q.

In the case where \(\mathbb {E} \xrightarrow {p} \mathbb {C}\) is induced by an indexed category \(F_{\mathbb {E}}:\mathbb {C}^{\mathrm {op}}\rightarrow \mathbf {CLat}_{\sqcap }\) via Definition B.1, a Cartesian lifting is given by \(f^{*}(Q)=(F_{\mathbb {E}} f)(Q)\).

In the current paper we focus on \(\mathbf {CLat}_{\sqcap }\)-fibrations. In a (general) fibration, a fiber \(\mathbb {E}_{X}\) is not just a preorder but a category, and this elicits a lot of technical subtleties. Nevertheless, it should not be hard to generalize the current paper’s observations to general, not necessarily \(\mathbf {CLat}_{\sqcap }\)-, fibrations (especially to the split ones). We shall often denote a vertical arrow in \(\mathbb {E}\) (i.e., an arrow inside a fiber) by \(\sqsubseteq\).

Appendix 3: Codensity Characterization of Hausdorff pseudometric

Proposition C.1

Let (X, d) be a pseudometric space. For any \(S,T\subseteq X\), we define two functions

and

The values of two functions coincide.

Proof

First, we show \(d_{c}(S,T)\ge d_{H}(S,T)\) by contradiction.

Suppose it does not hold. Then, by definition, at least one of

and

is greater than \(d_{c}(S,T)\). We can assume the former is greater than \(d_{c}(S,T)\) w.l.o.g.

Therefore, for some \(x_0 \in S\),

holds.

Now, since \(d(x_0,\_)\) is a non-expansive function by the triangle inequality, we have

However, since \(\inf _{x\in S}d(x_0,x)=0\), we have \(d_{c}(S,T) \ge \inf _{y\in T}d(x_0,y)\), which is a contradiction.

Next, we show \(d_{c}(S,T) \le d_{H}(S,T)\) by contradiction.

Suppose \(d_{c}(S,T) > d_{H}(S,T) + \varepsilon\) for some \(\varepsilon > 0\). Then, for some non-expansive \(k:X\rightarrow [0,1]\),

holds.

W.l.o.g. we can assume \(\inf _{x\in S}k(x) \le \inf _{y\in T}k(y)\).

Thus, for some \(x_0 \in S\) and \(y_0 \in T\) satisfying \(k(x_0) \le \inf _{x\in S}k(x) + \varepsilon /5\) and \(k(y_0) \le \inf _{y\in T}k(y) + \varepsilon /5\),

holds. Since

there exists some \(y_{1} \in T\) satisfying

However, we have \(k(x_0) \le k(y_0) + \varepsilon /5 \le k(y_{1}) + 2\varepsilon /5\), so

and

holds.

Then,

holds, which is a contradiction. \(\square\)