Relating coalgebraic notions of bisimulation

Introduction

• A labelled transition system can be represented as a coalgebra, and the paper extends this perspective to objects and next-state morphisms in an arbitrary category.The paper situates coalgebras as generalized transition systems across settings including presheaves, Stone spaces, and probabilistic systems.Source: Introduction · p. 1, Coalgebras in different categories · pp. 1–2

Notions of bisimulation

• Four coalgebraic bisimulation notions generalize the labelled-transition-system notion and coincide for labelled transition systems, but are related only under conditions in the general setting.They include compatible transition structures, relation lifting, congruence, and kernels of common compatible refinements.Source: Notions of bisimulation · p. 2

Relationship with the terminal sequence

• For notions characterized by post-fixed points of a monotone operator, the greatest bisimulation is given by a transfinite relation-refinement sequence starting from the maximal relation.Under certain conditions, the terminal coalgebra sequence and relation-refinement sequence have corresponding steps.Source: Relationship with the terminal sequence · p. 2

Other approaches not considered

• The paper focuses on internal relations between the state objects of two fixed coalgebras, rather than bisimilarity defined by spans of surjective homomorphisms or by bimodules.The latter approaches are mentioned but not discussed.Source: Other approaches not considered · p. 2

1. Coalgebras: Definitions and examples

• A B-coalgebra consists of an object and a morphism to its image under B, while a coalgebra homomorphism preserves the structures; coinductive datatypes are modeled using polynomial endofunctors.The section introduces examples of concepts arising as coalgebras.Source: §1 · p. 3, §1.1 · p. 3, Coinductive datatypes · p. 3

Transition systems

• Labelled transition systems correspond to coalgebras for P(L × (−)); finite powersets provide an alternative for finite nondeterminism and image-finite systems.Here P is the powerset functor and Pf is the finite powerset functor, described as the free semilattice.Source: Transition systems · p. 3

Transition systems in toposes and name-passing calculi

• Name-passing calculi motivate presheaf categories, where states track free variables and the endofunctor can encode input, output, and silent actions.The section describes presheaves over categories including finite sets and injections, and non-empty finite sets and all functions.Source: Transition systems in toposes and… · pp. 3–4
• In presheaf models, powerobjects accommodate infinite branching, but the free semilattice can be too small to record substitution-induced behavior in the π-calculus.The section proposes a partial-map-classifier-generated sub-join-semilattice as a more appropriate finite powerset for this setting.Source: Transition systems in toposes and… · p. 4

Frames in modal logic

• For Stone spaces, coalgebras for the compact-subset functor K correspond dually to modal algebras equipped with a meet-preserving operation.K maps spaces to their compact subsets with the finite, or Vietoris, topology.Source: Frames in modal logic · pp. 4–5

Powersets in algebraic set theory

• Algebraic set theory treats powersets via small maps: finite-fibre maps yield finite powersets on sets, while presheaf and Stone-space examples give other S-powersets.For [F+, Set], Ppf relaxes the naturality condition to injections; the K-as-S-powerset characterization is specific to Stone spaces.Source: Powersets in algebraic set theory · p. 5

Probabilistic transition systems

• Finite-support sub-probability distributions define a functor on Set whose coalgebras are discrete probabilistic transition systems.The distributions assign weights in [0, 1] with total weight at most 1.Source: Probabilistic transition systems · p. 6

Systems where the state space has more structure

• Other settings include continuous stochastic systems on metric or measurable spaces, recursive systems on domains, and similarity on preorders, posets, or quantale-enriched categories.The section cites prior work on each of these settings.Source: Systems where the state space has more… · p. 6

2.1. The lifting-span bisimulation of Aczel and Mendler [2].

• An AM-bisimulation equips a relation with a coalgebra structure that makes it a span of coalgebra homomorphisms.This notion categorically dualizes congruence from universal algebra.Source: §2.1 · p. 7

2.2. The relation-lifting bisimulation of Hermida and Jacobs [25].

• HJ-bisimulations use the relation lifting of the endofunctor, and their associated operator ΦHJ is monotone.The relation lifting is formed as the image of BR → B(X × Y) → BX × BY.Source: §2.2 · p. 7

2.3. The congruences of Aczel and Mendler [2].

• For identical coalgebras, equivalence relations are AM-precongruences exactly when they are congruences in the sense of Aczel and Mendler.AM-precongruences are connected to terminal coalgebras.Source: §2.3 · p. 8

2.4. Terminal coalgebras and kernel-bisimulations.

• A kernel-bisimulation is the pullback of homomorphisms from two coalgebras into a common coalgebra, without requiring a terminal coalgebra.With a terminal coalgebra, the analogous pullback of the unique terminal morphisms is called behavioural equivalence.Source: §2.4 · p. 8

3. Properties of endofunctors

• The five weaker endofunctor conditions include preserving relations, preserving or covering pullbacks, and preserving pullbacks along monos.For the mediating map from the image of a pullback to the pullback of the image, preservation requires an isomorphism, weak preservation a split epi, and covering a cover.Source: §3 · p. 9

3.1. Relevance of the properties.

• Properties such as relation preservation and pullback preservation compose; pullback-covering functors also compose when the inner functor’s outer partner preserves covers.Every polynomial endofunctor on an extensive category preserves pullbacks and covers.Source: §3.1 · p. 9
• For an S-powerset PS, pullbacks along monos are preserved; if S contains all monos, PS also preserves weak pullbacks.Under the stated extensivity, axioms, and collection assumptions, PS covers pullbacks even when S need not contain all monos.Source: §3.1 · pp. 9–10
• Ppf on the name-passing presheaf category preserves weak pullbacks, while the compact-subspace functor on Stone spaces covers pullbacks but does not preserve weak pullbacks.The free semi-lattice functor Pf on a topos covers pullbacks, but preserves weak pullbacks only if the topos is Boolean.Source: §3.1 · p. 10

4. Relating the notions of bisimulation

• Under the stated assumptions, AM-bisimulations are HJ-bisimulations, which are AM-precongruences; every AM-precongruence is contained in a kernel bisimulation that is also an AM-precongruence when C has pushouts.These are items (1)–(3) of Theorem 4.1.Source: §4 · p. 11
• A kernel bisimulation is an AM-bisimulation if B preserves weak pullbacks, an HJ-bisimulation if B covers pullbacks, and an AM-precongruence if B preserves pullbacks along monos and C is regular.The last implication also requires C to have pushouts, as specified in item (6).Source: §4 · p. 11
• An HJ-bisimulation is an AM-bisimulation if all epis split, B preserves relations, or the stated S-powerset or topos powerobject conditions hold.The S-powerset case requires S to contain all monomorphisms and B ≅ PS(B′(−)) for a relation-preserving B′; the topos case requires B ≅ P(B′(−)) with P the powerobject.Source: §4 · p. 11
• The notions do not generally coincide: examples distinguish AM-precongruence from AM-bisimulation and AM-bisimulation from HJ-bisimulation.The cited examples are an endofunctor on Set [2, p. 363] and the Vietoris construction on Stone spaces [9, Sec. 4].Source: §4 · p. 11

4.1. Proof of Theorem 4.1.

• The proof obtains a kernel bisimulation from an AM-precongruence by taking a pushout and then its pullback, which remains an AM-precongruence.For the kernel-to-AM-bisimulation implication, weak pullback preservation supplies a coalgebra structure on the relation; for the HJ-to-AM implication, the proof uses a split cover.Source: §4.1 · pp. 12, 14

4.2. A note about equivalence relations.

• For equivalence relations, the theorem’s assumptions can be weakened: effective equivalence relations, weak preservation or coverage of kernel pairs, and preservation of monos suffice in the corresponding items.The section also states that, in an extensive regular category, covering pullbacks is equivalent to covering kernel pairs and preserving pullbacks along monos.Source: §4.2 · pp. 14–15

5.1. The relation refinement sequence.

• If the relation-refinement sequence becomes stationary, it reaches the greatest HJ-bisimulation; the sequence converges when the relation category is small, for example when the category is well-powered.It starts from the maximal relation and applies the HJ operator at successor stages, with limit stages defined by limits.Source: §5.1 · p. 15
• The relation refinement and AM sequences often coincide, although AM- and kernel-bisimulations cannot generally be characterized as post-fixed points.The relation-refinement sequence extends Milner’s sequence for labelled transition systems.Source: §5.1 · p. 15

5.2. The terminal sequence.

• The terminal sequence starts at the terminal object, applies the endofunctor at successor stages, and takes limits at limit ordinals; convergence yields a final coalgebra.The two coalgebras induce cones over this sequence, which are used to construct relations between their states.Source: §5.2 · p. 16, §5.3 · p. 16

5.3. Relating the relation and terminal sequences.

• At every ordinal, the relation induced by the two terminal-sequence cones contains kernel bisimulations and AM-precongruences; it equals the HJ sequence if the endofunctor covers pullbacks, and the AM sequence if it preserves pullbacks along monos and the category has pushouts.The AM-sequence conclusion also holds when the category lacks all pushouts.Source: §5.3 · p. 16, Note · p. 17

5.4. Convergence for the relation refinement sequences.

• If the terminal sequence converges, the relation-refinement sequence does too, but it may converge earlier; a monic terminal-sequence map at stage α implies Rα = Rα+1.The relation-refinement sequence can converge before the terminal sequence even when a final coalgebra exists.Source: §5.4 · p. 17
• In Set with a filtered-colimit-preserving endofunctor, the terminal sequence becomes monic at ω but does not converge until ω + ω; image-finite transition-system refinement converges at ω.For finite state sets, relation refinement converges before ω; more generally, descending ω-cochains of subobjects from finitely presentable objects in a Boolean Grothendieck topos are eventually constant.Source: §5.4 · p. 17
• The presheaf topos [I, Set] used for name-passing is not Boolean, but its Boolean subcategory Sh¬¬(I) has finitely presentable objects described as finite named-sets with symmetry.The article’s techniques provide a foundation for coalgebra-inspired verification procedures.Source: §5.4 · p. 17

Appendix A. Some concepts from categorical logic

• The appendix introduces concepts from categorical logic: regular categories and powersets from algebraic set theory.Source: Appendix A · p. 17

A.1. Regular and extensive categories.

• An image of a morphism is a minimal subobject through which that morphism factors; the factoring morphism is called a cover.A category has images when every morphism has one.Source: §A.1 · p. 18
• In a category with finite limits, covers are epimorphisms and generalize surjective functions; a category with finite limits and images is regular when covers are stable under pullback.Source: §A.1 · p. 18
• An extensive category has coproducts that are disjoint and stable under pullback.Source: §A.1 · p. 18

A.2. Open maps, powersets, and algebraic set theory.

• Joyal and Moerdijk’s account treats a morphism as a family of classes indexed by its codomain, with smallness intuitively requiring small fibres.An object is small when its terminal map is small.Source: §A.2 · p. 18

• A1 requires open maps to be closed under composition, with every identity map open.Source: Open maps in regular categories · p. 18
• A2 requires open maps to remain open under pullback.Source: Open maps in regular categories · p. 18
• A3 gives descent from a pullback along a cover, while A6 requires openness to pass from f to g when e is a cover.Source: Open maps in regular categories · p. 18
• Unlike many authors, this article does not require additional category structure to interpret the universal quantifier.Source: Open maps in regular categories · p. 18

• A4 requires the maps 0 → 1 and 1 + 1 → 1 to be open.Source: Sums and open maps · p. 18
• A5 requires the coproduct map induced by two open maps to be open.Source: Sums and open maps · p. 18

Powersets.

• An S-relation on A is a jointly monic span whose left projection belongs to S.Source: Powersets · p. 19
• An S-powerset classifies S-relations on A, and its universal property makes morphisms into it correspond to those relations.When every object has an S-powerset, the construction extends to a covariant endofunctor.Source: Powersets · p. 19

Separation and collection.

• Separation corresponds to axiom (M), that all monomorphisms belong to S; collection corresponds to A9, preservation of covers by PS.Source: Separation and collection · p. 19

Further axioms.

• The axioms used here are insufficient as a foundation of mathematics; the text additionally names a small natural numbers object, small powersets, and a universal small map.Source: Further axioms · p. 19