Codensity Games for Bisimilarity
Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, Ichiro Hasuo

TL;DR
This paper introduces a categorical framework for bisimilarity games that unifies and extends game characterizations of bisimilarity and its quantitative variants across various system types.
Contribution
It provides a formal fibrational and coalgebraic framework that derives codensity bisimilarity games, covering known and new bisimilarity notions.
Findings
Unified categorical framework for bisimilarity games
Derivation of codensity bisimilarity games
Applicability to both classical and quantitative systems
Abstract
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: notably, 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 codensity bisimilarity games: a general categorical game…
| position | player | possible moves |
|---|---|---|
| S | ||
| D |
| position | P | possible moves |
|---|---|---|
| S | ||
| such that | ||
| D | ||
| such that |
| position | pl. | possible moves |
|---|---|---|
| S | s.t. , | |
| and | ||
| D | such that | |
| S | such that | |
| , and | ||
| D | such that | |
| , and | ||
| fibration | indistinguishability structure | decent map | ||
|---|---|---|---|---|
| topology | continuous func. | generated from | ||
| -field | measurable func. | generated from | ||
| pseudometric | non-expansive func. | |||
| endorelation | relation preserving func. | |||
| preorder | monotone func. | |||
| equivalence relation | relation preserving func. |
| position | pl. | possible moves |
|---|---|---|
| S | s.t. | |
| D | s.t. |
| position | pl. | possible moves |
|---|---|---|
| S | s.t. | |
| D | s.t. | |
| position | pl. | possible moves |
|---|---|---|
| S | and s.t. | |
| and | D | s.t. |
| position | pl. | possible moves |
|---|---|---|
| S | s.t. | |
| D | s.t. |
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Codensity Games for Bisimilarity
††thanks: The authors are supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST. S.K. and I.H. are supported by the JSPS-Inria Bilateral Joint Research Project CRECOGI; 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, and B.K.’s visit, at National Institute of Informatics, Tokyo, Japan.
Yuichi Komorida12, Shin-ya Katsumata1, Nick Hu3, Bartek Klin4, Ichiro Hasuo12a
1 National Institute of Informatics, Tokyo, Japan
2 The Graduate University for Advanced Studies (SOKENDAI), Hayama, Japan
3 University of Oxford, United Kingdom
4 University of Warsaw, Poland
Abstract
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: notably, 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 codensity bisimilarity games: a general categorical game characterization of bisimilarity. Our framework covers known bisimilarity-like notions (such as bisimulation metric) as well as new ones (including what we call bisimulation topology).
††publicationid: pubid: 978-1-7281-3608-0/19/$31.00 ©2019 IEEE
I Introduction
I-A Bisimilarity Notions and Games
Since the seminal works by Park and Milner [1, 2], bisimilarity has played a central role in theoretical computer science. It is an equivalence notion between branching systems; it abstracts away internal states and stresses the black-box observation-oriented view on process semantics. Bisimilarity is usually defined as the largest bisimulation, which is a binary relation that satisfies a suitable mimicking condition. In fact, a bisimulation can be characterized as a post-fixed point using a suitable relation transformer ; from this we obtain that bisimilarity is the greatest fixed point of by the Knaster–Tarski theorem. This order-theoretic foundation is the basis of a variety of advanced techniques for reasoning about (or using) bisimilarity, such as bisimulation up-to—see, e.g., [3].
Bisimilarity is conventionally defined for state-based systems with nondeterministic branching. However, as the applications of computer systems become increasingly pervasive and diverse (such as cyber-physical systems), extension of bisimilarity to systems with other branching types has been energetically sought in the literature. One notable example is the bisimulation notion for probabilistic systems in [4]: it is a relation that witnesses that two states are indistinguishable in their behaviors henceforth. This qualitative notion has also been made quantitative, as the notion of bisimulation metric [5]. It replaces a relation with a metric that is induced by the probabilistic transition structure.
There is a body of literature (including [6, 7, 8, 9, 10, 11, 12]) that aims to identify the mathematical essences that are shared by this variety of bisimilarity, and express the identified essences in a rigorous manner using category theory. Our particular interest is in the correspondence between bisimilarity notions and (safety) games; three examples of which are given below. This interest in bisimilarity games is shared by the recent work [10], and the comparison is discussed in §I-D.
I-A1 Bisimilarity Games
It is well-known that the following game characterizes the conventional notion of bisimilarity between Kripke frames. Let be a Kripke frame where ; the game is played between Duplicator (D) and Spoiler (S). In a position , Spoiler challenges Duplicator’s claim that and are bisimilar, by choosing one of the states (say ) and further choosing a transition . Duplicator responds by choosing a transition from the other state, and the game is continued from . Duplicator wins if Spoiler gets stuck, or the game continues infinitely long, and this witnesses that and are bisimilar.
I-A2 Games for Probabilistic Bisimilarity
A recent step forward in the topic of bisimilarity and games is the characterization of probabilistic bisimulation introduced in [13]. For simplicity, here we describe its discrete version.
Let be a Markov chain, where is a countable set of states, and is a transition kernel that assigns to each state a probability subdistribution . Here denotes the set of probability subdistributions over . For , let denote the probability with which a successor of is chosen from ; that is, . Since is only a sub-distribution over , the probability is rather than . The remaining probability can be thought of as the probability of getting stuck.
Recall from [4] that an equivalence relation is a (probabilistic) bisimulation if, for any and each -closed subset , holds.
The game introduced in [13] is in Table I. It is shown in [13] that Duplicator is winning in the game at if and only if and are bisimilar, in the sense of [4] (recalled above). It is not hard to find an intuitive correspondence between the game in Table I and the definition of bisimulation [4]: Spoiler challenges the bisimilarity claim between by exhibiting such that is violated; Duplicator makes a counterargument by claiming that is in fact not bisimilarity-closed, exhibiting a pair of states that Duplicator claims are bisimilar.
I-A3 Games for Probabilistic Bisimulation Metric
Our following observation marked the beginning of the current work: the game for (qualitative) bisimilarity for probabilistic systems (from [13], Table I) can be almost literally adapted to (quantitative) bisimulation metric for probabilistic systems. This metric was first introduced in [5].
For simplicity we focus on the discrete setting; we also restrict to pseudometrics bounded by . Let be a Markov chain with a countable state space . The bisimulation metric is defined to be the smallest pseudometric (with respect to the pointwise order) that makes the transition kernel
[TABLE]
non-expansive with respect to the specified pseudometrics. Here is the so-called Kantorovich metric over induced by the pseudometric over . It is defined as follows. For ,
[TABLE]
where in the above sup, ranges over all non-expansive functions from to \bigl{(}[0,1],d_{[0,1]}\bigr{)}, denotes the usual Euclidean metric, and is the expectation of with respect to .
Our observation is that the bisimulation metric is characterized by the game in Table II: Duplicator is winning at if and only if .
The game seems to be new, although its intuition is similar to the one for Table I. Note that the formula (1) appears in the condition of Spoiler’s moves. Spoiler challenges by exhibiting a “predicate” that suggests violation of the non-expansiveness of ; and Duplicator makes a counterargument that is in fact not non-expansive and thus invalid.
I-A4 Towards a Unifying Framework
The last two games (Table I from [13] and Table II that seems new) motivate a general framework that embraces both. There are some clear analogies: the games are about indistinguishability of states under a class of observations ( and respectively), and the predicates usable in those observations are subject to certain preservation properties (bisimilarity-closedness in the former, and non-expansiveness in the latter).
I-B A Codensity-Based Framework for Bisimilarity and Games
The main contribution of the current paper is a categorical framework that derives a variety of bisimilarity notions and corresponding game notions. The correspondence is proved once and for all on the categorical level of generality. It covers the three examples introduced earlier in §I-A, much like the recent categorical framework in [10] does. However, our fibration-based formalization has another dimension of generality. For example, besides relations and metrics, our examples include what we call bisimulation topology.
The overview of our categorical framework is in the left half of Fig. 1. We build on our previous works [14] and [15]. In [14] a general construction called codensity lifting is introduced: given a fibration and parameters that embody the kind of observations we can make, a functor is lifted to . In [15], codensity lifting is used to introduce a generic family of bisimulation notions called codensity bisimilarity—see \small2⃝. In this paper, we extend these previous results by
- •
introducing the notion of codensity bisimilarity game (\small1⃝) that comes in two variants (untrimmed (§IV) and trimmed (§V)),
- •
establishing the correspondence between codensity bisimulations (\small2⃝) and games (\small1⃝) on a fibrational level of generality, and
- •
working out several concrete examples (\small4⃝, \small5⃝).
In general, devising a game notion (\small4⃝) directly from a bisimilarity notion (\small5⃝) is far from trivial. Indeed, doing so for an individual bisimilarity notion has itself been deemed a scientific novelty [16, 13]. Our codensity-based framework (in the left half of Fig. 1) can automate part of this process in the following precise sense.
We derive concrete notions of bisimilarity (\small5⃝) and bisimilarity game (\small4⃝) as instances; then the correspondence between the two is guaranteed by the categorical general result between \small1⃝ and \small2⃝.
We note, however, that this is no panacea. When one starts with a given concrete notion of bisimilarity (\small5⃝), their next task would be to identify the right choice of the parameters for the codensity lifting (\small3⃝). This task is not easy in general: we needed to get our hands dirty working out the examples in this paper, [14], and [15]. Nevertheless, we believe that the required passage from \small5⃝ to \small3⃝ is much easier than the direct derivation from \small5⃝ to \small4⃝, with our categorical framework providing templates of bisimilarity games (see Tables VIII, IX and X). After all, our framework identifies which part of the path from \small5⃝ to \small4⃝ can be automated, and which part remains to be done individually. This is much like what many other categorical frameworks offer, as meta-level theories.
As an additional benefit, our categorical framework can be used to discover new bisimilarity notions (\small5⃝), starting from (choices of parameters for) \small3⃝. We believe those derived new bisimilarity notions are useful, since our categorical theory embodies sound intuitions about observation, predicate transformation, and indistinguishability—see e.g. §II-B.
I-C Contributions
Our main technical contributions are as follows.
- •
We introduce a categorical framework that uniformly describes various bisimulation notions (including metrics, preorders and topologies) and the corresponding game notions (Fig. 1). The framework is based on coalgebras, fibrations, and codensity liftings in particular [14]. Our general game notion comes in two variants.
- –
The first (the untrimmed codensity game: §IV) arises naturally in a fibration, using its objects and arrows as possible moves. The untrimmed game is theoretically clean, but it tends to have a huge arena.
- –
We therefore introduce a method that restricts these arenas, leading to the (trimmed) codensity bisimilarity game (§V). The reduction method is also described in general fibrational terms, specifically using fibered separators and generating sets.
- •
From the general framework, we derive several concrete examples of bisimilarity and its related notions (\small4⃝ and \small5⃝ in Fig. 1). They are listed in Table VI. Among them, a few bisimilarity notions seem new (especially the bisimulation topology examples), and several game notions also seem new.
- •
We discuss the transfer of codensity bisimilarity by suitable fibered functors (§VII). As an example usage, we give an abstract proof of the fact that (usual) bisimilarity for Kripke frames is necessarily an equivalence (Example VII.2).
- •
Additionally, we conduct investigations of the game notion in [13] (Table I) in concrete, non-categorical terms. For one, we obtain its variation for bisimulation metric (as we showed in Table II). We also give a direct proof of the equivalence to another game notion for probabilistic bisimilarity, previously introduced in [16], by exhibiting a mutual translation of winning strategies (Appendix -A).
I-D Related Work
Besides the one in [13], another game characterization of probabilistic bisimulation has been given in [16]. It is described later in §II (Table IV). The latter game has a bigger arena than the one in [13]: in [16] both players have to play a subset , while in [13] only Spoiler does so.
The work that is the closest to ours is the recent work [10] that studies bisimilarity games in a categorical setting. Their formalization uses (co)algebras (following the (co)algebraic generalization of the Kantorovich metric introduced in [8]), and therefore embraces a variety of different branching types. The major differences between the two works are as follows.
- •
Our current work is fibration-based (in particular -fibrations), while [10] is not. As a consequence, ours accommodates an additional dimension of generality by changing fibrations, which correspond to different indistinguishability notions (relation, metric, topology, preorder, measurable structures, etc.). In contrast, the works [10] and [8] deal exclusively with two settings: binary relations and pseudometrics.
- •
A relationship to modal logic is beautifully established in [10], while it is not done in this work. We expect our fibrational framework can accommodate modal logic too: fibrations have been used for categorical modeling of logics [17]. We leave this aspect to future work.
- •
The categorical generalization [10] is based on the game notion in [16], while ours is based on that in [13]. Therefore, for some bisimulation notions (including the bisimulation metric), we obtain a game notion with a smaller arena. Compare Table II (an instance of ours) and Table IV (an instance of [10]).
There are a number of categorical studies of bisimilarity notions; notable mentions include open map-based approaches [18] and coalgebraic ones [19, 20]. The fibrational approach we adopt also uses coalgebras; it was initiated in [6] and pursued, e.g., in [11, 7, 9], and [15]. For example, in the recent work [11], fibrational generality is exploited to study up-to techniques for bisimilarity metric. They use the Wasserstein lifting of functors introduced in [8] instead of the codensity lifting that we use (it generalizes the Kantorovich lifting in [8], see Example III.4). It is known [8] that the Wasserstein and Kantorovich liftings can differ in general, while they coincide for some specific functors such as the distribution functor.
Some of our new examples are topological: we derive what we call bisimulation topology and a game notion that characterizes it. The relation between these notions and the existing works on bisimulation and topology (including [21, 22]) is left as future work.
I-E Organization
In §II, we present preliminaries on a general theory of games (we can restrict to safety games), and on fibrations. For the latter, we focus on a class called -fibrations, and argue that they offer an appropriate categorical abstraction of sets equipped with indistinguishability structures. In §III, we present codensity lifting and codensity bisimilarity (\small2⃝, \small3⃝ in Fig. 1). The material is based on [15], but we introduce some auxiliary notions needed for the correspondence with games. Our first game notion (the untrimmed one) is introduced in §IV; in §V, we cut down the arenas and obtain trimmed codensity bisimilarity game. The theory is further extended in §VI–VII: in §VI we accommodate multiple observation domains, and in §VII we discuss the transfer of codensity bisimilarities by full-faithful fibered functors preserving meets. These categorical observations give rise to the concrete examples in §VIII.
Some proofs and details are deferred to Appendix -A.
II Preliminaries
We write for the covariant powerset functor, and for the two-point set . We define the function called may-modality by if and only if . We write for the diagonal (equality) relation over a set .
II-A Safety Games
Here we recall some standard game-theoretic notions and results. In capturing bisimilarity-like notions, we can restrict ourselves to safety games—they have a simple winning condition where every infinite play is won by the same player (namely Duplicator). This winning condition reflects the characterization of bisimilarity-like notions by suitable greatest fixed points; the correspondence generalizes, for example, to the one between parity games and nested alternating fixed points—see [23]. The term “safety game” occurs, e.g., in [24, 25].
Safety games are played between two players; in this paper, they are called Duplicator (D) and Spoiler (S). We restrict to those games in which Duplicator and Spoiler alternate turns.
Definition II.1** (safety game).**
A (safety game) arena is a triple of a set of Duplicator’s positions, a set of Spoiler’s positions, and a transition relation . Hence is a bipartite graph. We require that and are disjoint, and that . We write .
For a position , the elements of the set are called the possible moves at . Unlike some works, we allow positions that have no possible moves at them.
A play in an arena is a (finite or infinite) sequence of positions , such that so long as belongs to the sequence.
A play in is won by either player, according to the following conditions: 1) a finite play is won by Spoiler (or by Duplicator) if (or respectively); and 2) every infinite play is won by Duplicator.
Definition II.2** (strategy, winning position).**
In an arena , a strategy of Duplicator is a partial function ; we require that implies . A strategy of Spoiler is defined similarly, as a partial function that returns a possible move at the last position in the history.
Given an initial position and two strategies and for Duplicator and Spoiler respectively, the play from induced by is defined in a natural inductive manner. The induced play is denoted by .
A position is said to be winning for Duplicator if there exists a strategy of Duplicator such that, for any strategy of Spoiler, the induced play is won by Duplicator.
In what follows, for simplicity, we restrict the initial position of a play to be in . (Note that Spoiler’s position can be winning for Duplicator.)
Winning positions of safety games are witnessed by invariants (Prop. II.4), which is a well-known fact.
Definition II.3** (invariant).**
Let be an arena. A subset is called an invariant for Duplicator if, for each and any possible move at , there exists a possible move at that is in . That is, \forall q\in P.\,\forall q^{\prime}\in Q_{\text{D}}.\,\bigl{(}\,(q,q^{\prime})\in E\;\Rightarrow\;\exists q^{\prime\prime}\in Q_{\text{S}}.\,\,(q^{\prime},q^{\prime\prime})\in E\land q^{\prime\prime}\in P\,\bigr{)}.
Proposition II.4**.**
Any position in an invariant for Duplicator is winning for Duplicator. 2. 2.
Invariants are closed under arbitrary union. Therefore, there exists a largest invariant for Duplicator. 3. 3.
The largest invariant for Duplicator coincides with the set of winning positions for Duplicator in . ∎
Examples of safety games have been given in Tables I–II. We present two other examples (Tables IV–IV).
Example II.5** (alternative games for probabilistic bisimilarity and bisimulation metric).**
In [16], a game notion that characterizes (qualitative) probabilistic bisimilarity is presented. It is in Table IV, presented in a slightly adapted form.
This game notion is categorically generalized in [10]; the generalization has freedom in the choice of coalgebra functors (i.e. branching types), as well as in the choice between relations and metrics. The instance of this general game notion for bisimulation metric is shown in Table IV.
The two games (Tables IV–IV) characterize the same bisimilarity-like notions as the games in Tables I–II, respectively; so they are equivalent. We can go further and give a direct equivalence proof by mutually translating winning strategies. Such a proof is not totally trivial; we do so for the pair for probabilistic bisimilarity. See Appendix -A.
We note that the game in Table II (an instance of our current framework) is simpler than Table IV (an instance of [10]). Table II is not only structurally simpler (it has fewer rows), but its set of moves are smaller too, asking for functions only at one place.
Our categorical framework based on codensity liftings (presented in later sections) covers Tables I–II but not Tables IV–IV. Accommodation of the latter two is future work.
II-B *
-fibrations *
II-B1 Definition and Properties
Here we sketch a basic theory of fibrations—see, e.g., [17] for a comprehensive account. In particular, we focus on a class of poset fibrations called -fibrations. We observe that the simple axiomatics of the class adequately capture all the examples of interest—and hence the mathematical essences of the logical phenomena that we wish to model.
Our exposition here is largely based on that in [15]. However, in this paper we introduce new notation and terminology (such as indistinguishability order and decent map)—see §II-B2. They help to further clarify the intuitions.
A formal definition is as follows. (See Appendix -B for a rather gentle introduction to -fibration.)
Definition II.6** (-fibration).**
A -fibration is a fibration such that each fiber (for each ) is a complete lattice, and each pullback functor (for each in ) preserves all meets .
Via the Grothendieck construction, a -fibration is in a bijective correspondence with a functor , where is the category of complete lattices and functions preserving all meets—see [17] and [7], as well as Appendix -B. The functor assigns
- •
a complete lattice (called the fiber over ) to each , and
- •
a function preserving all meets to each in . The map is called a pullback; it is also called a pullback functor since, in the general theory of fibrations, a fiber is a category rather than a poset.
Although the indexed category presentation may be more intuitive at first, we shall stick to the fibration presentation since we will eventually need some global structures in the total category . It turns out that -fibrations are special kinds of topological functor [26] such that each fiber category is a poset. Topological functors are a well-studied topic, and many examples and results are available; a good summary is found in [27].
The use of poset fibrations is common in categorical modeling of logics [7, 9]. -fibrations additionally require fibered small meets; this simple assumption turns out to be a mathematically powerful one.
Proposition II.7**.**
Let be a -fibration.
* is split, and faithful as a functor.* 2. 2.
Each arrow has its pushforward , so that an adjunction is formed. This is a consequence of Freyd’s adjoint functor theorem; it makes a bifibration **[17]**. 3. 3.
* is also a -fibration.* 4. 4.
The change-of-base **[17, Lemma 1.5.1]** of along any functor is also a -fibration. 5. 5.
If is (co)complete, then the total category is also (co)complete. This follows from **[17, Prop. 9.2.1]**.∎
II-B2 Notation, Terminology and Intuitions
Our view of a -fibration is that it equips objects of with what we call indistinguishability structures. This suits our purpose, since various bisimilarity-like notions are all about degrees of indistinguishability between (the behaviors of) states of a system. We present examples later in §II-B3.
Notation II.8** (indistinguishability predicate/order).**
Let be a -fibration. An object in the fiber category (i.e. an element of the complete lattice ) is called an indistinguishability predicate over . Our view is that is an additional structure on ; therefore, as a convention, an object shall also be denoted by .
Each fiber is a complete lattice; its order is denoted by and called the indistinguishability order over . Intuitively, means that has a greater degree of indistinguishability than —that is, is coarser than , and is more discriminating than .
The supremum and infimum with respect to the indistinguishability order are denoted by and respectively.
Definition II.9** (decent map).**
Let be a -fibration, be an arrow in , and be objects in the fibers. We say that is decent (from to ) if there exists a necessarily unique arrow in such that . We write in this case. The following equivalences follow.
[TABLE]
We write if is not decent.
The notion of decency is a fibered generalization of continuity, non-expansiveness, relation-preservation, etc. Decency means respects indistinguishability, carrying -indistinguishable elements to -indistinguishable ones.
II-B3 Examples
As shown in Table VI, various well-known categories can be seen as categories that equip sets with certain indistinguishability structures. The evident forgetful functors from the total categories (, , etc.) to in Table VI are all -fibrations.
Specifically, is the category of topological spaces and continuous maps; is that of measurable spaces and measurable maps; is that of -bounded pseudometric spaces (where a pseudo-metric is a metric without the condition ) and non-expansive maps; is that of sets with endorelations and relation-preserving maps; is that of preordered sets and monotone maps; and is that of sets with equivalence relations and relation-preserving maps—see [15] for details.
Note that, in and , the indistinguishability order is the opposite of the inclusion order. Therefore the meet of a family of indistinguishability structures computed as the one generated from the union of the family.
Another class of examples is given as follows: for any well-powered category admitting small limits, the subobject fibration of is a -fibration. All the algebraic categories over and Grothendieck topoi fall into this class. On the other hand, the forgetful functors from algebraic categories over are rarely (-)fibrations.
III Codensity Bisimilarity
We introduce codensity lifting (\small3⃝ in Fig. 1) and codensity bisimilarity (\small2⃝) based on [15]. These turn out to subsume many bisimilarity-like notions in the literature. The material in §III-A–III-B is largely from [15]; §III-C is new, paving the way to codensity bisimilarity games presented in later sections.
III-A Codensity Lifting
Definition III.1** **(codensity lifting
[15]).
Let be a -fibration, and be a functor. A parameter of codensity lifting of along is a pair of
- •
a -arrow (i.e. an -algebra) called modality [29, 30] and
- •
an -object above called observation domain.
The codensity lifting of with parameter is the endofunctor defined as follows. On objects,
[TABLE]
Its action on arrows is as follows. It is not hard to see that, for each arrow in , the arrow is decent from to . Then we define to be the unique arrow in above .
An alternative description is possible. When has powers and preserves them, is characterized as the following pullback in the fibration :
[TABLE]
where is the tupling. A similar characterization of codensity liftings of monads is in [14].
Table VI lists concrete examples of codensity liftings, with various fibrations , functors , and parameters . Some of them coincide with known notions. For example, the entry VI of the table says that the functor , with the designated and , carries a metric space to the set equipped with the well-known Kantorovich metric induced by —see (1).
Besides the functors listed in the table, there are some natural ways to systematically lift polynomial functors, by defining in an inductive manner—see, e.g., [11].
Example III.2**.**
Let us closely look at the entry VI of Table VI. There we codensity-lift the covariant powerset functor along the -fibration . We use the parameter , where is the modality given in §II.
We shall abbreviate by —a notational convention that is used throughout the paper.
Then relates if and only if
[TABLE]
Straightforward calculation shows that this is equivalent to
[TABLE]
This lifting is the restriction of the standard relational lifting of along , which is used for the usual bisimulation notion for Kripke frames, to .
Example III.3**.**
In the entry VI of Table VI, we codensity-lift along the -fibration (instead of ) with the parameter \bigl{(}(2,\mathrm{Eq}_{2}),\diamond\bigr{)}.
The characterization of is slightly involved. Its relation part relates if and only if
[TABLE]
where denotes the equivalence closure of .
It is not clear at this stage whether the codensity bisimilarities induced by the above liftings (Examples III.2–III.3, i.e. the entries VI & VI of Table VI) coincide with the usual bisimilarity notion for Kripke frames. This is because of the involvement of mandatory equivalence closures—specifically by the use of in Example III.2, and by the occurrence of in Example III.3. Later, in VII.2, we prove that both of the codensity bisimilarities indeed coincide with the usual bisimilarity notion. The proof relies crucially on transfer of codensity liftings via fibered functors.
Example III.4**.**
Here we follow [15, Example 3] and show that codensity lifting generalizes the Kantorovich lifting of functors introduced in [8]. Take as the -fibration in Def. III.1. As , we take with the usual Euclidean metric . There is freedom in the choice of a modality —this corresponds to what is called an evaluation function in [8]. This way we recover the Kantorovich lifting in [8] as .
III-B Codensity Bisimilarity
In [15], codensity bisimulation and bisimilarity are introduced. Recall that a coalgebra is a categorical presentation of state-based transition systems, such as automata, Markov chains, etc.—see, e.g., [20, 19], and also §VIII.
Definition III.5** **(codensity
bisimulation).
Assume the setting of Def. III.1. Let be an -coalgebra. An object is a (-)codensity bisimulation over if ; that is, is decent with respect to the designated indistinguishability structures on and .
We move on to the characterization of codensity bisimulations as (post-)fixed points of suitable predicate transformers.
Definition III.6** (predicate transformer ).**
Assume the setting of Def. III.5. We define a predicate transformer with respect to and by:
[TABLE]
Theorem III.7**.**
Assume the setting of Def. III.5. For any , the following are equivalent.
; that is, is a codensity bisimulation over (Def. III.5). 2. 2.
. 3. 3.
For each , implies . ∎
The predicate transformer is a monotone map from the complete lattice to itself. Therefore, by the Knaster–Tarski theorem, the greatest post-fixed point of exists and it is the greatest fixed point of .
Definition III.8** (codensity bisimilarity ).**
Assume the setting of Def. III.5. The greatest codensity bisimulation, whose existence is guaranteed by the above arguments, is called the codensity bisimilarity. It is denoted by .
Some bisimilarity notions, including bisimilarity of deterministic automata (§VIII-B), are accommodated in the generalized framework with multiple observation domains—see §VI.
Example III.9** (bisimulation metric).**
Consider the -fibration and the subdistribution functor . Recall that As a parameter of codensity lifting, we take (\mathbf{\Omega},\tau)=\bigl{(}\,\bigl{(}[0,1],d_{[0,1]}\bigr{)},\,e\colon\mathcal{D}_{\leq 1}[0,1]\to[0,1]\,\bigr{)}, where is the expectation function and is the Euclidean metric. Let be a coalgebra, identified with a Markov chain.
The codensity bisimilarity in this setting coincides with bisimulation metric from [5] (see also §I-A3). This fact is not hard to check directly; one can also derive the coincidence via III.4 and the observations in [8].
III-C Joint Codensity Bisimulation
We introduce a notion of joint codensity bisimulation. This minor variation of codensity bisimulation becomes useful in the proof of soundness and completeness of our game notion (§IV).
Definition III.10** **(joint codensity
bisimulation).
Assume the setting of Def. III.5. Let ; joins in are denoted by . We say that is a joint codensity bisimulation over if is a codensity bisimulation over .
For instance, the set of all codensity bisimulations is a joint codensity bisimulation, because the join is the largest bisimulation (a consequence of the Knaster–Tarski theorem).
Lemma III.11**.**
In the setting of Def. III.5, the downset is the largest joint codensity bisimulation (with respect to the inclusion order). ∎
IV
Untrimmed Games for Codensity Bisimilarity
As the first main technical contribution, we introduce what we call the untrimmed version of codensity bisimilarity game. It is mathematically simple but its game arenas can become much bigger than necessary. The trimmed version of games—with smaller arenas—will be introduced later in §V, after developing necessary categorical infrastructure.
Assume the setting of Def. III.5 for the rest of the section.
Definition IV.1** (untrimmed codensity bisimilarity game).**
The untrimmed codensity bisimilarity game is the safety game played by two players D and S, shown in Table VIII.
Lemma IV.2**.**
Let . The following are equivalent.
* is an invariant for Duplicator (Def. II.3) in the safety game in Table VIII.* 2. 2.
* is a joint codensity bisimulation over . ∎*
Theorem IV.3**.**
The following coincide.
The set of all winning positions for D. 2. 2.
The downset of the codensity bisimilarity.
Proof*.*
On the one hand, the set of all winning positions for D is the largest invariant for D, by Prop. II.4. On the other hand, the downset is the largest joint codensity bisimulation over . Thus, the statement follows from Lem. IV.2.∎
We conclude that our game characterizes the codensity bisimilarity (Def. III.8).
Corollary IV.4** **(soundness and completeness of untrimmed codensity
games).
* is a winning position for D if and only if . ∎*
Example IV.5**.**
Recall Example III.9. Using the untrimmed codensity bisimilarity game, we can characterize the bisimulation metric from [5]. Our general definition (Def. IV.1) instantiates to the one in Table VIII, which is however more complicated than the game we exhibited in the introduction (Table II). For example, in Table VIII, Duplicator’s move is a pseudometric rather than a triple .
V Trimmed Codensity Games for Bisimilarity
Our previous untrimmed game (Table VIII) is pleasantly simple from a theoretical point of view. However, as we saw in Example IV.5, its instances tend to have a much bigger arena than some known game notions.
Here we push our theory a step further, and present a fibrational construction that allows us to trim our games. We note that our construction still remains on the fibrational level of abstraction.
V-A Generating Sets and Fibered Separators in a Fibration
We start by building some fibrational infrastructure. The following notion is a natural extension of the corresponding lattice-theoretic one. Unlike in the case of algebraic lattices, we do not assume the compactness of elements in .
Definition V.1** (generating set).**
Let be a -fibration and be an object. We say that a set is a generating set of the fiber if, for any , there exists such that .
Example V.2**.**
Consider the -fibration and . For any , we define the equivalence relation to be the least one equating , that is, if and only if . Then the set of elements of the fiber is a generating set.
Example V.3**.**
Recall Example III.9. For () and , the pseudometric over is defined by
[TABLE]
Then the set of pseudometrics is a generating set of the fiber .
One natural question is how to find such a generating set in the fiber over the state space. Below we show that a generating set of the fiber of a special object (called fibered separator) induces a generating set of each fiber by push-forward.
Definition V.4** (fibered separator).**
Let be a -fibration. We say that is a fibered separator if, for any and , we have
[TABLE]
Theorem V.5**.**
Let be a fibered separator of a -fibration , and be a generating set of . For any , the following set is a generating set of :
[TABLE]
Here denotes the pushforward along (§II-B). ∎
In fact, it was Thm. V.5 behind Examples V.2–V.3: in both cases, turns out to be a fibered separator for the fibrations in question ( and ), and the presented generating sets are obtained via push-forward.
The following result is useful in finding fibered separators—see §VIII-F.
Proposition V.6** (change-of-base and fibered separators).**
Let be a -fibration, be a functor with a left adjoint , and be a fibered separator for . Then is a fibered separator of the change-of-base fibration . ∎
V-B -Joint Codensity Bisimulation
We use generating sets to restrict moves in codensity games.
Definition V.7**.**
In the setting of Def. III.5, let be a generating set of . A -joint codensity bisimulation over is a joint codensity bisimulation over such that .
Lemma V.8** (key lemma).**
Assume the setting of Def. III.5, and let be a generating set of . The intersection \bigl{(}\mathop{\downarrow}(\nu\Phi_{c}^{\mathbf{\Omega},\tau})\bigr{)}\cap\mathcal{G} of the downset and the generating set is the largest -joint codensity bisimulation.
Proof*.*
Since is a generating set, the union of all elements of is equal to . Thus, is a -joint codensity bisimulation.
For any -joint codensity bisimulation , we have already shown . We also have by definition. These imply .∎
V-C Trimmed Codensity Bisimilarity Games
The above structural results lead to our second game notion.
Definition V.9** **(trimmed codensity bisimilarity
game).
Assume the setting of Def. III.5, and that is a generating set. The codensity bisimilarity game is the safety game played by two players D and S, shown in Table IX.
Assume the setting of Def. V.9 for the rest of the section.
Lemma V.10**.**
Let . The following are equivalent:
* is an invariant for D (Def. II.3) in the game in Table IX.* 2. 2.
* is a -joint codensity bisimulation over . ∎*
Theorem V.11**.**
The following sets coincide.
The set of D-winning positions in the game in Table IX. 2. 2.
The intersection \bigl{(}\mathop{\downarrow}(\nu\Phi_{c}^{\mathbf{\Omega},\tau})\bigr{)}\cap\mathcal{G} of the downset of the codensity bisimilarity over and the generating set . ∎
We conclude that our second game characterizes the codensity bisimilarity (Def. III.8) too.
Corollary V.12** **(soundness and completeness of trimmed codensity
games).
In Def. V.9, is a winning position for Duplicator if and only if . ∎
VI Multiple Observation Domains
We extend the theory so far and accommodate multiple observation domains and modalities. This extension is needed for some examples, such as those marked with in Table VI.
We consider the class of liftings of an endofunctor along a -fibration . It comes with a natural pointwise partial order:
[TABLE]
and the partially ordered class admits meets of arbitrary size. As done in the original codensity lifting of endofunctors in [15] (and monads in [14]), we extend the codensity lifting so that it takes a family of parameters , and returns the intersection of the codensity liftings of with these parameters.
Definition VI.1** **(codensity lifting of a
functor with multiple parameters [15]).
Let be a functor, be a -fibration, be a class, and be an -indexed family of parameters (of the codensity lifting of along ), which is denoted simply by . The (multiple-parameter) codensity lifting of with is the endofunctor defined by the intersection of the codensity liftings:
[TABLE]
The rest of the theoretical development is completely parallel to the one in the previous sections. Therefore we only present key definitions and the main result (Cor. VI.4). The omitted definitions and results can be recovered from the ones in §III–V, by replacing a single-parameter codensity lifting (Def. III.1) by a multi-parameter one (Def. VI.1).
Definition VI.2** (codensity bisimulation).**
Assume the setting of Def. VI.1. Let be an -coalgebra. An object is a codensity bisimulation over if ; that is, is decent with respect to the designated indistinguishability structures.
Definition VI.3** (codensity bisimilarity game).**
In the setting of Def. VI.2, let be a generating set of . The codensity bisimilarity game is the safety game, played by two players D and S, shown in Table X.
Corollary VI.4** (soundness and completeness of codensity games).**
Assume the setting of Def. VI.3. is a winning position for Duplicator if and only if . ∎
Example VI.5** (bisimulation topology for deterministic automata).**
Here we describe the topological example in Table VI. Consider the -fibration and the functor , where is a fixed alphabet. Coalgebras for this functor are deterministic automata over ; see e.g. [20, 19].
We take the following data as a parameter of codensity lifting (cf. Def. VI.1): , is the Sierpinski space for each , and the modalities (where ) are defined by
[TABLE]
Recall that the Sierpinski space is the set with the topology ; this observation domain models the situation where acceptance of a word is only semi-decidable.
Let be a deterministic automata. The above choice of parameters leads to the following codensity bisimilarity: the state space is equipped with the topology generated by the following family of open sets.
[TABLE]
One can extract various information from this bisimulation topology via standard topological constructs. For example, the specialization order of this topology coincides with the language inclusion order.
For illustration by comparison, consider changing the observation domain from the Sierpinski space to the discrete 2-point set. The bisimulation topology over is now generated by
[TABLE]
We can now observe rejection of a word, too, because is open. The specialization order of this topology is the language equivalence, and it satisfies the R0 separation axiom (while the last Sierpinski example does not).
We take these examples of bisimulation topology as a process-semantical incarnation of the “observability via topology, computability via continuity” paradigm from domain theory. The definition of codensity bisimulation (cf. Def. III.1) fits well with this intuition, too: a continuous map in Def. III.1 is a “computable observation”; accordingly, an open set of the bisimulation topology is a property that is decided by finitely many of those computable observations.
VII Transfer of Codensity Bisimilarities
In our formulation, for the same endofunctor , we can use various -fibrations and parameters to equip -coalgebras with different bisimilarity-like notions. Some relations among those codensity bisimilarities can be categorically captured by the following theorem.
Theorem VII.1** (transfer of codensity bisimilarity).**
Let and be -fibrations, be an endofunctor, be an -coalgebra, be a full and faithful fibered functor from to preserving fibered meets, and be an -indexed family of parameters for codensity lifting of along .
[TABLE]
In this setting, is an -indexed family of parameters for codensity lifting of along , and we have . ∎
Example VII.2**.**
We show that the codensity bisimilarities in Examples III.2 & III.3 are indeed the usual bisimilarity notions for Kripke frames. Recall that they are build on the two -fibrations and .
We first note that the inclusion functor is a reflection, having the equivalence closure as the left adjoint. It follows that is meet-preserving. Moreover, is fibered.
[TABLE]
We introduce shorthands for the liftings in Examples III.2 & III.3:
[TABLE]
Now, for the sake of our proof, let us introduce a relational lifting of along , for which it is obvious that the corresponding bisimilarity notion is the usual bisimilarity for Kripke frames. We do so in concrete terms, instead of as a codensity lifting:
[TABLE]
We note that is the restriction of from to along . Note also that .
Let be a Kripke frame and () be the predicate transformer corresponding to each lifting. Theorem VII.1 states that .
Furthermore, by (where is the order in (3)), we have . From and fiberedness of , we can see that is a fixed point of , which yields by the Knaster–Tarski theorem. The three (in)equalities so far allow us to conclude , stating that the conventional bisimilarity is equal to the codensity bisimilarities in Examples III.2 & III.3. As a consequence, the conventional bisimilarity is necessarily an equivalence relation.
VIII Examples
VIII-A * Kripke Frames and (Conventional) Bisimilarity*
We consider as an underlying -fibration, and a Kripke frame (as a -coalgebra). We further use the codensity lifting (Example III.2) and the generating set described in Example V.2 to trim games; the resulting game is shown in Table XV. As shown in Example VII.2, the codensity bisimilarity (which is in VII.2) coincides with conventional bisimilarity on using the standard relational lifting of to .
Theorem VIII.1**.**
* is a D-winning position if and only if , if and only if and are bisimilar. ∎*
Extension of this result to labeled transition systems and Kripke models (with valuations) is straightforward, using suitable choice of endofunctors—see also §VIII-B.
VIII-B *Deterministic Automata and Their Language
Equivalence*
We use the functor from Example VI.5, for which a coalgebra is a deterministic automaton. Let us lift along the fibration , with the same modalities as in Example VI.5 (where ). Our observation domains are for all . The resulting codensity lifting is concretely described as follows.
[TABLE]
Let be a deterministic automaton. It is not hard to see that the codensity bisimilarity coincides with language equivalence of deterministic automata. Our trimmed codensity game is shown in Table XV (in a slightly optimized form). The game therefore characterizes the language equivalence (Cor. VI.4).
VIII-C Deterministic Automata and the Language Topology
We introduced two versions of bisimulation topology for deterministic automata in Example VI.5. They are in close correspondences with accepted languages; therefore we call them language topologies.
For the first topology in Example VI.5 (where is the Sierpinski space, capturing that acceptance is only semi-decidable), the corresponding (untrimmed) codensity game is shown in Table XV. It follows from our general results that the game notion is sound and complete.
We have not yet found a good way (e.g. generating sets) of trimming the game arena; this is left as future work.
VIII-D Nondeterministic Automata and Bisimilarity
Let us now turn to nondeterministic automata, that is, -coalgebras for the functor . Much like the situation for DFAs, we lift this functor along the -fibration by codensity lifting with multiple observation domains, as follows. Let be the set . We set the parameter of codensity lifting as follows, where .
[TABLE]
The resulting codensity lifting is concretely described as
[TABLE]
Let be a nondeterministic automaton. It is again not hard to see that the codensity bisimilarity is the usual notion of bisimilarity of nondeterministic automata. Our trimmed codensity game is shown in Table XV, in a slightly optimized form, and it captures bisimilarity.
A topological variant of the above story is possible, much like in §VIII-C.
VIII-E Markov Chains and Bisimulation Metric
Recall Examples III.9, IV.5, and V.3. Markov chains are -coalgebras. We use the -fibration , taking pseudometrics as a notion of indistinguishability. With the lifting parameter we described in Example III.9, we get the bisimulation metric as the codensity bisimilarity. We can use the generating set described in Example V.3 to obtain a trimmed codensity game; the resulting game essentially coincides with the one in Table II in the introduction. Therefore, Cor. V.12 gives an abstract proof for the correctness of the game.
VIII-F Continuous State Markov Chains and Bisimulation Metric
In order to accommodate continuous state Markov chains (for which measurable structures are essential), we consider an example that involves . Continuing §VIII-E, by the change-of-base along the forgetful functor , we get another -fibration . A continuous state Markov chain is a coalgebra of the so-called sub-Giry functor over —see, e.g., [29].
Since the forgetful functor has a left adjoint, Prop. V.6 gives us a fibered separator for . This gives us a game notion similar to that in §VIII-E.
VIII-G *Markov Chains and Probabilistic Bisimilarity *
In order to define bisimilarity-like equivalence relation on Markov chains, we first lift along the -fibration . For that purpose, here we use the following multiple lifting parameters. The index set is . For each , we set , and define a threshold modality by if and only if . Then for any , the relation part of the codensity lifting relates if and only if
[TABLE]
Let us fix a Markov chain . All these data give rise to and as in Definitions VI.2 and III.8. It is not hard to see that the resulting codensity bisimilarity coincides with probabilistic bisimilarity in [4]. Note, for example, that a relation-preserving map coincides with an -closed subset of . The resulting trimmed codensity game is in Table XV. It is essentially the same as Table I (arising from [13]). The difference is that is additionally present in Table XV; it is easy to realize that plays no role in the game.
IX Conclusions and Future Work
Motivated by some recent works [13, 10, 11, 8], and especially by the similarity of the two games (Tables I and II), we introduced a fibrational framework that uniformly describes the correspondence between various bisimilarity notions and games. The fibrational abstraction allows us to accommodate some new examples, such as bisimulation topology. Moreover, the structural theory developed in §VI–VII provides new insights to the nature of bisimilarity, we believe, identifying the crucial role of observation maps ( in Def. III.1) in bisimulation notions.
As future work, we intend to accommodate modal logics as is done in [10]. We are also interested in using games with more complex winning conditions (e.g. parity); they have been used for (bi)simulation notions for Büchi and parity automata [31]. Finally, we will pursue the algorithmic use of the current results.
-A Direct Proof of Equivalence of the Two Game Notions Characterizing Probabilistic Bisimilarity (Tables I, IV)
-A1 Table IV
Table I
Assume that Duplicator wins Table IV from , and let Spoiler play some in Table I . There are two cases to consider which are essentially identical, but we write them down separately just to make sure.
- •
If then make Spoiler select and play in Table IV. To this Duplicator responds with some such that , which implies that . Pick any and play it as Spoiler in Table IV; when Duplicator responds with some , play the pair and as Duplicator in Table I.
- •
If then make Spoiler select and play in Table IV. To this Duplicator responds with some such that , which implies that . Pick any and play it as Spoiler in Table IV; when Duplicator responds with some , play the pair and as Duplicator in Table I.
-A2
This is a less straightforward implication. A winning strategy for Duplicator in Table IV is built not from a single strategy in Table I, but rather from an entire collection of winning positions.
Formally, assume that Duplicator wins Table I from , and let Spoiler choose and play some in Table IV. Define
[TABLE]
One basic observation is that , since Duplicator wins from all positions of the form . As a result:
[TABLE]
Another observation is that Spoiler wins Table I from the position . To see this, consider any Duplicator’s response , . Then there is some such that Duplicator wins Table I from . If Duplicator could win Table I from then she could win from as well, which contradicts the assumption that .
Since we assume that Duplicator wins Table I from , cannot be a legal move for Spoiler from , hence
[TABLE]
Together with (4) this implies that
[TABLE]
so is a legal move for Duplicator in stage (ii) of Table IV, no matter if Spoiler chose or in stage (i). To this, in stage (iii) replies with some . By definition of , there is some such that Duplicator wins Table I from , so Duplicator can respond with .
-B Introduction to -Fibration
We present an introduction to (-)fibrations, starting from a functor . The relevance of the latter is explained in §II-B. For details, readers are referred to [17].
-B1 The Grothendieck Construction
In general, the equivalence between index categories and fibrations is well-known. Here we sketch the Grothendieck construction from the former to the latter, focusing the special case of and -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 , as shown in Fig. 2.
On the right-hand side in Fig. 2, we add some arrows (denoted by ) so that we have an arrow in for each . (On the left-hand side, the correspondence \raisebox{0.3pt}{\shortmid}\!\joinrel\dashrightarrow depicts the action of the map .) The diagram in in Fig. 2 should be understood as a Hasse diagram: those arrows which arise from composition are not depicted.
Definition .1** (The Grothendieck construction).**
Given , we define the category by
- •
its objects: a pair of an object and an element of the poset ; and
- •
its arrows: is an arrow in such that
[TABLE]
Here refers to the order of .
Thus arises a category that incorporates:
- •
the order structure of each of the posets , and
- •
the pullback structure by (F_{\mathbb{E}}f)_{f\colon\text{\mathbb{C}-arrow}}.
For fixed , the objects of the form and the arrows between them form a subcategory of . This is denoted by and called the fiber over . It is obvious that is a poset that is isomorphic to .
Moreover, there is a canonical projection functor that carries to .
-B2 Formal Definition of -Fibration
We axiomatize those structures which arise in the way described above.
Definition .2** (-fibration).**
A -fibration consists of two categories and a functor , that satisfy the following properties.
- •
Each fiber is a complete lattice. Here the fiber for is the subcategory of consisting of the following data: objects such that ; and arrows such that (such arrows are said to be vertical).
- •
Given in and , there is an object and an -arrow with the following universal property. For any and in , if then factors through uniquely via a vertical arrow. That is, there exists unique such that and .
[TABLE]
- •
The correspondences and are functorial:
[TABLE]
The last equality can be depicted as follows.
[TABLE]
The category is called the total category of the fibration; is the base category. The arrow is called the Cartesian lifting of and . An arrow in is Cartesian (or reindexing) if it coincides with for some and .
In the case where is induced by an indexed category via Def. .1, a Cartesian lifting is given by .
In the current paper we focus on -fibrations. In a (general) fibration, a fiber 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 -, fibrations (especially to the split ones). We shall often denote a vertical arrow in (i.e. an arrow inside a fiber) by .
-C Codensity Characterization of Hausdorff pseudometric
Proposition .3**.**
Let be a pseudometric space. For any , we define two functions
[TABLE]
and
[TABLE]
The values of two functions coincide.
Proof*.*
First, we show by contradiction.
Suppose it doesn’t hold. Then, by definition, at least one of
[TABLE]
and
[TABLE]
is greater than . We can assume the former is greater than w.l.o.g.
Therefore, for some ,
[TABLE]
holds.
Now, since is a non-expansive function by the triangle inequality, we have
[TABLE]
However, since , we have , which is a contradiction.
Next, we show by contradiction.
Suppose for some . Then, for some non-expansive ,
[TABLE]
holds.
W.l.o.g. we can assume .
Thus, for some and satisfying and ,
[TABLE]
holds. Since
[TABLE]
there exists some satisfying
[TABLE]
However, we have , so
[TABLE]
and
[TABLE]
holds.
Then,
[TABLE]
holds, which is a contradiction.∎
-D Omitted Proofs
-D1 Proof of Lem. III.11
Proof*.*
The downset is a joint codensity bisimulation, because the union of all elements of is equal to a codensity bisimulation .
Let be a joint codensity bisimulation. Then for any , we have , because .∎
-D2 Proof of Lem. IV.2
Proof*.*
We follow the following logical equivalence.
[TABLE]
where the last equivalence is by Thm. III.7.
-D3 Proof of Prop. V.6
Proof*.*
For any , the bijection exists. Thus, naturally identifying and , we have the following for any .
[TABLE]
∎
-D4 Proof of Prop. VII.1
Proof*.*
We have because, for any ,
[TABLE]
holds.
Considering this and the fact that preserves meets, [15, Lemma 20] implies .∎
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] D. Park, “Concurrency and automata on infinite sequences,” in Proceedings of the 5th GI-Conference on Theoretical Computer Science . London, UK, UK: Springer-Verlag, 1981, pp. 167–183. [Online]. Available: http://dl.acm.org/citation.cfm?id=647210.720030
- 2[2] R. Milner, Communication and Concurrency . Prentice-Hall, 1989.
- 3[3] D. Sangiorgi and J. Rutten, Eds., Advanced Topics in Bisimulation and Coinduction , ser. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2011.
- 4[4] K. G. Larsen and A. Skou, “Bisimulation through probabilistic testing,” Inf. Comput. , vol. 94, no. 1, pp. 1–28, 1991.
- 5[5] J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden, “Metrics for labelled markov processes,” Theoretical Computer Science , vol. 318, no. 3, pp. 323 – 354, 2004. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S 0304397503006042
- 6[6] C. Hermida and B. Jacobs, “Structural induction and coinduction in a fibrational setting,” Inf. Comput. , vol. 145, no. 2, pp. 107–152, 1998. [Online]. Available: https://doi.org/10.1006/inco.1998.2725
- 7[7] I. Hasuo, T. Kataoka, and K. Cho, “Coinductive predicates and final sequences in a fibration,” Mathematical Structures in Computer Science , vol. 28, no. 4, pp. 562–611, 2018. [Online]. Available: https://doi.org/10.1017/S 0960129517000056
- 8[8] P. Baldan, F. Bonchi, H. Kerstan, and B. König, “Coalgebraic behavioral metrics,” Logical Methods in Computer Science , vol. 14, no. 3, 2018. [Online]. Available: https://doi.org/10.23638/LMCS-14(3:20)2018
