Simulations as a genuinely categorical concept

Jürgen Koslowski


When considering categories with structured sets as objects, of course structure-preserving functions always are available as morphisms. It would seem natural to consider structure-preserving relations as well, but this has rarely been done, even if the structure itself is specified by means of relations. Notable exceptions are order ideals between pre-ordered sets and the simulations of Park and Milner between labeled transition systems. While the former are just modules (or profunctors) in the pre-ordered setting, the latter, lacking the reversibility of modules, are often seen as a mere stepping stone towards bisimulation equivalence to classify systems in process algebra, but not as morphisms in their own right.

Various flavors of bisimulations have since arisen in theoretical computer science. Their importance is no longer confined to the realm of process algebra, where the notion initially gained prominence.

Different approaches exist to dealing with (bi)simulations categorically, e.g., by means of coalgebra as initiated by Aczel and Mendler, and a synthetic approach as pioneered by Joyal, Nielsen and Winskel, cf. also Cockett and Spooner. In contrast to these we would like to identify simulations as a genuinely categorical concept in its own right. It turns out that Park and Milner's idea of ``structure-preserving relation'' is based on precursors from automata theory by Ginzburg and Yoeli (1963), which in turn were motivated by algebraic considerations of Lambek (1958).

Ginzburg and Yoeli's notion has a direct categorical interpretation in terms of lax transforms between graph morphisms into the bicategory rel of sets, relations and inclusions. The formalism readily extends to spn, and when saturation is taken into account, these categorical simulations are located in between functors and profunctors (or modules). In fact, this idea already makes sense at the level of morphisms between monads in arbitrary bicategories, which emphasizes the inherently 2-dimensional nature of our concept. The latter is often ignored even in categorical treatments of (bi)simulations.

In this fashion the notion of simulation becomes available in areas outside of process algebra or even theoretical computer science.

The essential tool for handling graph morphisms into rel or spn, the interplay between different views of labeled transition systems and the notion of saturation will be graph comprehension, which extends and simplifies an observation of Pavlovic.