Simulations as a genuinely categorical concept
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
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