# Relational Presheaves as Labelled Transition Systems

Pawel Sobociński

► To cite this version:

Pawel Sobociński. Relational Presheaves as Labelled Transition Systems. 11th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Mar 2012, Tallinn, Estonia. pp.40-50, 10.1007/978-3-642-32784-1_3. hal-01539889

HAL Id: hal-01539889

https://inria.hal.science/hal-01539889

Submitted on 15 Jun 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Relational Presheaves as Labelled Transition Systems

Paweł Sobociński

ECS, University of Southampton

**Abstract.** We show that viewing labelled transition systems as relational presheaves captures several recently studied examples. This approach takes into account possible algebraic structure on labels. Weak closure of a labelled transition system is characterised as a left (2-)adjoint to a change-of-base functor.

A famous application of coalgebra [3, 4] is as a pleasingly abstract setting for the theory of labelled transition systems (LTS). Indeed, an LTS is a coalgebra for the functor $\mathcal{P}(A \times -)$, where $A$ is the set of labels. LTSs are thus objects of the category of coalgebras for this functor. The arrows, in LTS terminology, are functional bisimulations. This category of coalgebras (modulo size issues) has a final object that gives a canonical notion of equivalence, although other approaches are available in general, see [34]. Ordinary bisimulations can be understood as spans of coalgebra morphisms. The coalgebraic approach has been fruitful: amongst many notable works we mention Turi and Plotkin's elegant approach to structural operational semantics congruence formats via coalgebras [36].

In another influential approach, Winskel and Nielsen [38] advocated the use of presheaf categories as a general semantic universe for the study of labelled transition systems. Morphisms turn out to be functional simulations, functional bisimulations can be characterised as open maps with respect to a canonical (via the Yoneda embedding) choice of path category [20]. Ordinary bisimulations are then spans of open maps, with some side conditions.

Both the coalgebraic approach and the presheaf approach have generated much subsequent research and have found several applications that we do not account for here. Concentrating on the theory of labelled transition systems, there are some limitations to both approaches. For example both take for granted that the set of labels $A$ is monolithic and has no further structure. In fact, several labelled transition systems have “sets” of labels that are monoids [9] or even categories [14, 24, 25]. Such examples are more challenging to capture satisfactorily with the aforementioned approaches but some progress has been made—for instance, Bonchi and Montanari [7] captured labelled transition systems on reactive systems (in the sense of Leifer and Milner [24]) as certain coalgebras on presheaves.

There is also a certain mismatch between notions typically studied by concurrency theorists or researchers in the operational semantics of concurrent languages and the morphisms in categories of coalgebras or in presheaves. From
the point of view of process theory, the morphisms in the aforementioned categories are not the notions typically studied: *functional simulations* and *functional bisimulations*<fnref n="1" /> instead of ordinary simulations and ordinary bisimulations.

Furthermore, the most natural notions of equivalence in applications are often weak (in the sense of Milner) and these tend to be technically challenging to capture in the coalgebra or presheaf settings. One can think of weak bisimulation as ordinary bisimulation on a labelled transition system that has been “saturated” with the silent $\tau$-actions, but this is just another way of saying that $\tau$ is made the identity of a monoid of actions. Because the coalgebraic and presheaf approaches were not designed with a view to accommodate such *algebraic structures* on the set of labels, some work has to be performed in order to talk about weak equivalences, see for example [13, 33].

In this paper we show that several recent examples of LTSs with algebraic structure can be seen as relational presheaves [28]. Relational presheaves are lax functors [22] (or, equivalently, morphisms of bicategories [5]) $\mathbf{C}^{\text{OP}} \to \mathbf{Rel}$, where $\mathbf{Rel}$ is the locally partially ordered 2-category of relations. They have been called various names: specification structures [1], relational variable sets [15], dynamic sets [35], with several applications in Computer Science and related fields. Functors to $\mathbf{Rel}$ as a way of giving semantics to flowcharts were considered as early as 1972 by Burstall [10].

The typical examples of $\mathbf{C}$ that we shall consider will be monoids (i.e. categories with one object) and categories of contexts, in the sense of Leifer and Milner [24, 32]. Ordinary $\mathbf{A}$-labelled transition systems can be seen as instances of the former by considering the free monoid $\mathbf{A}^*$. A more interesting example where the label set is a non-free monoid is the LTS considered in [9] or the LTSs that arise from expressions in the algebra of Span(\textbf{Graph}) [21]. Weak derived LTS for reactive systems in the sense of Jensen [19], are examples of relational presheaves for $\mathbf{C}$ a category of contexts. Tile logics [14] can also be seen as relational presheaves where $\mathbf{C}$ is not merely a monoid.

The morphisms of relational presheaves [28] are oplax natural transformations, and in the aforementioned examples these turn out to be *ordinary simulations*. This suggests the naturality of this abstract setting from the point of view of process theory. The fact that simulations are oplax natural transformations in a relational setting was observed by Jürgen Koslowski [23].

Following Rosenthal, we denote the 2-category of relational presheaves by $\mathcal{R}^*(\mathbf{C})$. Given relational presheaves $h, h' \in \mathcal{R}^*(\mathbf{C})$, morphisms $h \to h'$ organise themselves in a sup-lattice and joins are preserved by composition, in other words $\mathcal{R}^*(\mathbf{C})$ is a quantaloid [28]. Quantaloids have previously been used in the study of process equivalence by Abramsky and Vickers [2]. Simulations and bisimulations have been investigated in the setting of categories enriched over quantaloids by Schmitt and Worytkiewicz [31].

The mathematical universe of relational presheaves with relational morphisms is rich. It is sometimes helpful to restrict to the subcategory of $\mathcal{R}^*(\mathbf{C})$ with arrows the functional morphisms (i.e. functional simulations in the exam-

<footnote n="1">¹ Although Hughes and Jacobs [17] have also studied simulation coalgebraically.</footnote>
ples). Following Rosenthal we shall refer to this category as $\mathcal{R}(\mathbf{C})$. Here, change-of-base functors $u^*$ always have left-adjoints and they have right-adjoints whenever $u$ satisfies the weak factorisation lifting property [26]. One consequence is that $\mathcal{R}(\mathbf{C})$ has limits that are computed pointwise.

Finally, and most importantly, several familiar constructions from the literature can be characterised as adjunctions. For example, we shall show that the weak-closure of a labelled transition system is actually a left (2-)adjoint to a change-of-base functor. In this sense, this paper continues the programme of [37] in that category theory is used to clarify and distill constructions commonly used in the study of models of concurrency.

# 1 Examples

In order to motivate the more abstract developments we start here with a sight-seeing tour of the examples that will turn out to be relational presheaves.

**Example 1 (Ordinary labelled transition systems).** A labelled transition system is a triple $(X, A, T)$ where $T \subseteq X \times A \times X$. The set $X$ is called the statespace, $A$ is a monolithic set of atomic actions and $T$ is a set of transitions. We write $x \xrightarrow{a} x'$ for $(x, a, x') \in T$.

One way to describe such a structure using the coalgebraic approach is to use the functor $\mathcal{P}(A \times -)$, where $\mathcal{P}$ is the (covariant) powerset endofunctor on Set. An LTS with label set $A$ is a coalgebra for the $\mathcal{P}(A \times -)$ Set-endofunctor, i.e. a function

$$h: X \to \mathcal{P}(A \times X) \qquad (1)$$

There are several examples where the set $A$ has more structure, in particular, when it's a monoid or even the set of arrows of a category. We list some of these examples below.

**Example 2 (Weak labelled transition systems).** Consider a special “silent” action $\tau$ that we intend to be unobservable. Define a weak LTS to be $(X, A + \{\tau\}, T)$ where the set $T$ of transitions is reflexive-transitive closed wrt to $\tau$s, i.e. it is closed under the rules below

$$\frac{P \xrightarrow{\tau} Q \quad Q \xrightarrow{a} R \quad R \xrightarrow{\tau} S}{P \xrightarrow{\tau} P} \qquad (2)$$

It is easy to show that bisimilarity and weak bisimilarity coincide on a weak LTS. A weak LTS can be obtained from an LTS with $\tau$-labels via reflexive-transitive $\tau$-closure. In this paper we shall show that this construction arises as a left adjoint to a change-of-base functor (Lemma 12).

**Example 3 (Monoidal structure on labels).** An LTS with monoidal structure on labels is $(X, M, T)$ where $M$ is a monoid with multiplication $\star$ and unit $\iota$, and where the set $T$ of transitions is closed under the following two rules:

$$\frac{P \xrightarrow{\iota} P}{P \xrightarrow{a} P} \qquad \frac{P \xrightarrow{a} Q \quad Q \xrightarrow{b} R}{P \xrightarrow{a \star b} R} \qquad (3)$$
Notice that such LTSs are actually examples of categories, with objects the states, identities $\iota$, and composition given by $\star$. See [9] for a recent example of such an LTS in concurrency theory literature.

**Example 4 (Contexts as labels).** The contexts-as-labels approach was introduced by Leifer and Milner [24] and developed further in [6, 7, 29, 30]. Here we give only a very brief summary: suppose that $\mathbf{C}$ is a (2-)category with objects interfaces and arrows contexts; see [32] for a number of concrete examples. There is a chosen object 0 as the ground interface, arrows with domain 0 are then the ground terms. Given a set of reaction-rules, which is a set of pairs of arrows $r, r' : 0 \to X$ one generates a reaction relation $\dashv$ by closing the rules with respect to reactive contexts: the arrows of a subcategory $\mathbf{D}$ of $\mathbf{C}$. Then one can derive an LTS that has transitions of the form $t \stackrel{c}{\dashv} t'$ where $t : 0 \to X$, $c : X \to Y$, $t' : 0 \to Y$ such that $c \circ t \dashv t'$ and $c$ is the smallest context that makes this reduction possible. The notion of smallest is typically captured via a universal property, in $\mathbf{C}$, of relative (local) pushouts.

Jensen [19, Definition 3.18] introduced the notion of weak bisimilarity for reactive systems (see also [8]), a construction that for every reactive system $R$ with all RPOs, gives a reactive system $W(R)$. The intuition is that reactions are composed to form reactions in $W(R)$: for example $(r, r')$ and $(s, s')$ are composed to $(p \circ r, q \circ s')$ where $p \circ r'$ and $q \circ s$ form an RPO, and “identity” reactions $(r, r)$ are added for all $r$. Bisimilarity on the LTS derived from $W(R)$ acts as a kind of weak bisimilarity in examples. We omit the details here and just mention two properties that are satisfied by this LTS:

1. $u \xrightarrow{\mathrm{id}} u$ for all $u \in \mathbf{C}$,

2. if $u \xrightarrow{a} v$ and $v \xrightarrow{b} w$ then $u \xrightarrow{a;b} w$.

Both are a consequence of [19, Lemma 3.2].

**Example 5 (Tile systems).** Tile systems [14] are double categories, in which the vertical dimension can be viewed as (double) labelled transitions between the arrows of the horizontal category, considered as the statespace. The vertical dimension forms a category, and hence this labelled transition system is closed under composition and has identities.

## 2 LTSs: from coalgebras to relational presheaves

Seeing an LTS as a $\mathcal{P}(A \times -)$ coalgebra (1) emphasises the statespace but wraps the labels within the definition of the functor. In order to consider possible extra structure of $A$ we need to bring the labels out as first class citizens so:

$$ \frac{h : X \to \mathcal{P}(A \times X)}{h' : X \to \mathcal{P}(X)^A} \qquad (4) \\ \frac{h'' : A \to \mathcal{P}(X)^X}{\qquad} $$
That is, to give a standard $\mathcal{P}(A \times -)$ coalgebra is to give an $A$-indexed family of $\mathcal{P}(-)$ coalgebras.

For the sequel, it makes sense to use the fact that $\mathcal{P}$ is a monad, and in particular we can use the composition in the Kleisli category $Kl(\mathcal{P})$.<fnref n="2" /> We can replace the conclusion of (4) by:

$$h : A \to Kl(\mathcal{P})(X, X) \qquad (5)$$

If $A$ is a monoid, then $h$ should preserve the structure in some way. But, first, monoids are exactly one-object categories. So for a general category $\mathbf{C}$, (5) generalises to a mapping

$$h : \mathbf{C} \to Kl(\mathcal{P}) \qquad (6)$$

We shall now elucidate what properties the mapping (6) ought to satisfy. Of course, $Kl(\mathcal{P})$ is another name for **Rel**, the locally partially ordered 2-category with objects sets, arrows relations and 2-cells inclusions.

A natural choice for (6) is that of relational presheaf, that is a lax functor from $\mathbf{C}^{\text{op}}$ to **Rel**:

$$h : \mathbf{C}^{\text{op}} \to \mathbf{Rel} \qquad (7)$$

The laxness here means that:

$$h(b); h(a) \subseteq h(a; b) \qquad \text{id}_{h(x)} \subseteq h(\text{id}_x) \qquad (8)$$

Morphisms of $\varphi : h \to h'$ of relational presheaves $\mathbf{C}^{\text{op}} \to \mathbf{Rel}$ are oplax natural transformations [15,26]. This means, for each $C \in \mathbf{C}$ a relation $\varphi_C : h(C) \to h'(C)$ such that the (lax) naturality condition is satisfied for each $f : D \to C$ in $\mathbf{C}$, i.e.:

$$\begin{array}{ccc}
hC & \xrightarrow{\varphi_C} & h'C \\
\multicolumn{2}{c}{h_f \supseteq h'f} & \\
\downarrow & & \downarrow \\
hD & \xrightarrow{\varphi_D} & h'D
\end{array} \qquad (9)$$

The 2-category with objects relational presheaves and morphisms as above<fnref n="3" /> will be denoted $\mathcal{R}^*(\mathbf{C})$. The subcategory with functional morphisms; those $\varphi : h \to h'$ where $\varphi_C$ in (9) is a function<fnref n="4" /> for all $C \in \mathbf{C}$ will be denoted $\mathcal{R}(\mathbf{C})$.

Now back to examples. Consider $\mathbf{C}$ to be a category with one object, i.e. a monoid $(M, \star, \iota)$.

**Proposition 6.** To give an LTS with a monoidal structure on labels (Example 3) is to give a relational presheaf, i.e. an object of $\mathcal{R}^*(M)$. Morphisms of $\mathcal{R}^*(M)$ are precisely the simulations between such LTSs. □

<footnote n="2">² Jacobs, Hasuo and Sokolova have used coalgebras in Kleisli categories in order to consider trace semantics coalgebraically [16, 18].</footnote>

<footnote n="3">³ Rosenthal [28] calls these generalized rp-morphisms.</footnote>

<footnote n="4">⁴ These are Rosenthal's rp-morphisms.</footnote>
Any ordinary LTS (Example 1) can be considered a relational presheaf by taking $\mathbf{C} = A^*$ and considering the LTS of traces. Not all relational presheaves in $\mathcal{R}^*(A^*)$ are ordinary labelled transition systems in the sense of Example 1. For instance, in a general relational presheaf in $\mathcal{R}^*(A^*)$ there can be transitions $p \xrightarrow{e} q$ for $p \neq q$ and transitions $p \xrightarrow{ab} p'$ without an intermediate $p''$ such that $p \xrightarrow{a} p''$ and $p'' \xrightarrow{b} p'$. Ordinary LTSs with labels in $A$ form the full subcategory of $\mathcal{R}^*(A^*)$ with objects the (ordinary) functors, which we will refer to as LTS($A$).

**Proposition 7.** To give an ordinary LTS with label set $A$ (Example 1) is to give a functor $(A^*)^{\text{op}} \to \text{Rel}$. Let LTS($A$) denote the corresponding full subcategory of $\mathcal{R}^*(A^*)$. The morphisms of LTS($A$) are thus the simulations. $\square$

Taking a reactive system $R$ with category of contexts $\mathbf{C}$, the derived LTS on $W(R)$ [19] is a relational presheaf. This is a direct consequence of [19, Lemma 3.22].

**Proposition 8.** *Given a category of contexts $\mathbf{C}$ with all relative pushouts and a set of reaction rules $R$, the derived LTS on $W(R)$ is a relational presheaf $\mathcal{R}^*(\mathbf{C})$.** $\square$

Similarly, taking $\mathbf{C}$ to be the product of the vertical category of any tile system with itself allows (the LTS generated by) any tile system to be considered as a relational presheaf.

### 3 Relational presheaves as labelled transition systems

The familiar Grothendieck construction instantiated to relational presheaves yields categories, which we can consider as LTSs.

**Definition 9.** Let $h : \mathbf{C}^{\text{op}} \to \text{Rel}$ be a relational presheaf. Then the labelled transition system $\Gamma(h)$ has:

states: pairs $(C, x)$ where $C \in \mathbf{C}$ and $x \in h(C)$

transitions: $(C, x) \xrightarrow{f} (D, y)$ if $C \xrightarrow{f} D$ is in $\mathbf{C}$ and $x \in h(f)(y)$.

As a consequence of (8), $\Gamma(h)$ is closed under the rules of (3). Indeed, if $\mathbf{C}$ has one object then $\Gamma(h)$ is an LTS with a monoidal structure on labels, in the sense of Example 3.

**Proposition 10.** *Morphisms $\varphi : h \to h'$ are in a 1-1 correspondence with simulations from $\Gamma(h)$ to $\Gamma(h')$.** $\square$

Niefield [26] amongst other authors have studied $\mathcal{R}(\mathbf{C})$ and we can use some of the rich theory of relational presheaves to yield insights about the examples that we have identified. An example is the following result.

**Proposition 1.** *Limits exist and are computed pointwise in $\mathcal{R}(\mathbf{C})$.*

*Proof.* Corollary 3.2 in [26].
Now $\mathcal{R}^*(\mathbf{C})$ is a locally partially-ordered 2-category, with natural transformations ordered pointwise by inclusion (these are the modifications [22] in this simple setting). It is well-known that the hom-posets of $\mathcal{R}^*(\mathbf{C})$ are complete suplattices<fnref n="5" /> and this is the generalisation of the fact that simulations are closed under unions.

**Lemma 11.** *The local partial-orders of $\mathcal{R}^*(\mathbf{C})$ are complete sup-lattices.*

*Proof.* We give the proof of this well-known result only to give the flavour of the relational calculus that is used when manipulating morphisms of $\mathcal{R}^*(\mathbf{C})$. Suppose that $\{\varphi^i\}_{i \in I}$ is a family of morphisms from $h$ to $h'$ in $\mathcal{R}^*(\mathbf{C})$. It suffices to show that $\bigcup_{i \in I} \varphi^i$ is a morphism, i.e. that the naturality condition (9) holds. Indeed

$$ 
\begin{align*}
hf; \bigcup_{i \in I} \varphi_D^i &= \bigcup_{i \in I} hf; \varphi_D^i \\
&\subseteq \bigcup_{i \in I} \varphi_C^i; h'f \\
&= (\bigcup_{i \in I} \varphi_C^i); h'f.
\end{align*}
$$

□

# 4 Weak labelled transition systems

Consider an LTS with silent $\tau$ labels. Closing wrt to rules (2), considering $\tau$ as the monoid identity and forming the traces yields a relational presheaf. This is technically somewhat similar to the approaches advocated in [27] and [13]. We shall now make this construction precise and characterise it with a universal property.

Let $A_\tau \stackrel{\text{def}}{=} A + \{\tau\}$. There is a function on sets $A_\tau \to A^*$ that sends each $a \in A$ to itself (considered as a word of length one) and $\tau$ to $\epsilon$. This extends to a morphism of monoids by freeness

$$ u : A_{\tau}^{*} \to A^{*} \qquad (10) $$

that yields a change-of-base functor

$$ u^* : \mathcal{R}^*(A^*) \to \mathcal{R}^*(A_{\tau}^*). $$

In terms of LTSs, it is easy to see that $u^*$ acts by closing a transition system with actions in $A^*$ by the following rule, and on arrows (simulations) as identity.

$$ \frac{P \xrightarrow{\epsilon} Q}{P \xrightarrow{\tau} Q} \qquad (11) $$

The left adjoint $\Sigma_u : \mathcal{R}^*(A_\tau^*) \to \mathcal{R}^*(A^*)$ can be understood in this particular case as first closing an LTS wrt to rules (2) and then renaming $\tau$ to $\epsilon$.

<footnote n="5">⁵ More succinctly, $\mathcal{R}^*(\mathbf{C})$ are quantaloids, see [28].</footnote>
**Lemma 12.** *There is a 2-adjunction*

$$ \mathcal{R}^*(A_\tau^*) \underset{u^*}{\overset{\Sigma_u}{\rightleftarrows}} \mathcal{R}^*(A^*) \quad (12) $$

where $\Sigma_u$ can be understood on objects as closing an LTS wrt to the rules (2) and renaming $\tau$ to $\epsilon$. On arrows $\Sigma_u$ acts as identity.

*Proof.* We define $\Sigma_u$ on objects as first forming the closure under (2) and then renaming $\tau$ to $\epsilon$. On arrows $\Sigma_u$ is the identity. Now if $h$ is an LTS on $A_\tau^*$ then it is easy to check that the identity relation on the statespace is a simulation from $h$ to $u^*\Sigma_u h$. Also, if $g$ is an LTS on $A^*$ then again the identity function is a simulation from $\Sigma_u u^* g$ to $g$. These two families of simulations are natural transformations. The triangle equalities thus trivially hold. $\square$

The definition of $\Sigma_u$ gives us a concise way to capture weak simulation—a relation $\varphi: h \to h'$, where $h, h' \in \mathcal{R}^*(A_\tau^*)$ is a weak simulation precisely when it is defines an arrow $\varphi: \Sigma_u h \to \Sigma_u h'$ in $\mathcal{R}^*(A^*)$.

**Proposition 13.** *The category of (ordinary) labelled transition systems with label set $A_\tau$ and weak simulations is the category with*

- objects those of LTS($A_\tau$) (the full subcategory of $\mathcal{R}^*(A_\tau^*)$ with objects ordinary functors) and

- morphisms $h$ to $h'$ given by $\mathcal{R}^*(A^*)(\Sigma_u(h), \Sigma_u(h'))$.

$\square$

Restricting to the subcategories with functional morphisms, $u$ defined in (10) satisfies the weak factorisation lifting property and hence $u^*$ also has a right adjoint $\Pi_u : \mathcal{R}(A_\tau^*) \to \mathcal{R}(A^*)$ [26, Theorem 4.1]. In terms of LTS terminology, $\Pi_u$ maps an ordinary LTS $L = (X, A_\tau, T)$ to the following LTS with labels in $A$:

states: those $x \in X$ for which $x \xrightarrow{\tau} x$ in $L$

transitions: the non-$\tau$ transitions of $L$.

$\Pi_u(h)$ can thus be understood as the largest $\tau$-reflexive sub-LTS, restricted to the non-$\tau$ actions. It is not difficult to verify that the $\Pi_u$ defined in this way is a right adjoint to $u^*$.

# 5 Conclusions and future work

We have observed that several examples of labelled transition systems, especially when there is algebraic structure on labels, can be considered as relational presheaves. The morphisms between such LTSs are simulations and the resulting categories of LTSs have rich structure due to their mathematical status. As
an example, we characterised weak closure as a left adjoint to a change-of-base
functor.

There are several future directions. The theory of bisimulation needs to be
developed: in the examples that we have examined bisimulations are those mor-
phisms that remain morphisms when reversed via the underlying involution in
**Rel**, it remains to be seen whether this view is fruitful in the wider, general pic-
ture. For example, it is of interest that functional bisimulations in our examples
can be characterised as *maps* in $\mathcal{R}^*(\mathbf{C})$, that is, those 1-cells which have a right
adjoint in the 2-categorical sense.

There are several other settings in which there is an obvious monoidal struc-
ture on labels. One example is reversible transition systems where standard con-
structions [11, 12] may be characterised as universal when viewed as relational
presheaves.

Morphisms in $\mathcal{R}^*(\mathbf{C})$, change-of-base functors and their adjoints give a gen-
eral approach to defining simulations (amongst other equivalences), morphisms
and canonical constructions in models where such notions have not been obvious;
for example in the theory of reactive systems. Finally, **Rel** can be generalised to
**Span** and other (bi)categories, yielding more general notions of labelled transi-
tion systems.

*Acknowledgment.* Thanks go to Bartek Klin for several useful discussions and to Tom Hirschowitz, Jürgen Koslowski and the anonymous referees for several important suggestions.

References

1. S. Abramsky, S. Gay, and R. Nagarajan. Specification structures and propositions-as-types for concurrency. In *Logics for Cuncurrency - Structure versus Automata*, volume 1043 of LNCS, pages 5–40, 1996.

2. S. Abramsky and S. Vickers. Quantales, observational logic and process semantics. *Math. Struct. Comput. Sci.*, 3:161–227, 1993.

3. P. Aczel and N. Mendler. A final coalgebra theorem. In *Category Theory and Computer Science (CTCS '89)*, volume 389 of LNCS, pages 357–365. Springer, 1989.

4. J. Adamek. Introduction to coalgebra. *Theor. App. Categories*, 14(8):157–199, 2005.

5. J. Bénabou. Introduction to bicategories, part 1. In *Midwest Category Seminar*, volume 47 of LNM, pages 1–77. Springer, 1967.

6. F. Bonchi, B. König, and U. Montanari. Saturated semantics for reactive systems. In *Logic in Computer Science (LiCS '06)*. IEEE Press, 2006.

7. F. Bonchi and U. Montanari. Reactive systems, (semi-)saturated semantics and coalgebras on presheaves. *Theor. Comput. Sci.*, 410:4044–4066, 2009.

8. R. Bruni, F. Gadducci, U. Montanari, and P. Sobociński. Deriving weak bisim-
ulation congruences from reduction systems. In *Concurrency Theory (CONCUR '05)*, number 3653 in LNCS, pages 293–307. Springer, 2005.

9. R. Bruni, H. C. Melgratti, and U. Montanari. A connector algebra for P/T nets interactions. In *Concurrency Theory (CONCUR '11)*, volume 6901 of LNCS, pages 312–326. Springer, 2011.
10. R. M. Burstall. An algebraic description of programs with assertions, verification and simulation. In *Conference on Proving Assertions about Programs*, pages 7–14. ACM, 1972.

11. V. Danos and J. Krivine. Reversible communicating systems. In *Concurrency Theory (CONCUR '04)*, volume 3170 of LNCS, pages 292–307. Springer, 2004.

12. V. Danos, J. Krivine, and P. Sobociński. General reversibility. In *Expressiveness in Concurrency (EXPRESS '05)*, ENTCS. Elsevier, 2005.

13. M. P. Fiore, G. L. Cattani, and G. Winskel. Weak bisimulation and open maps. In *Logic in Computer Science (LiCS '99)*. IEEE Press, 1999.

14. F. Gadducci and U. Montanari. The tile model. In *Proof, Language and Interaction: Essays in Honour of Robin Milner*, pages 133–166. MIT Press, 2000.

15. S. Ghilardi and G. Meloni. Relational and partial variable sets and basic predicate logic. *J. Symbolic Logic*, 61(3):843–872, 1996.

16. I. Hasuo, B. Jacobs, and A. Sokolova. Generic trace semantics via coinduction. *Log. Meth. Comput. Sci.*, 3(4), 2007.

17. J. Hughes and B. Jacobs. Simulations in coalgebras. *Theor. Comput. Sci.*, 327(1-2):71–108, 2004.

18. B. Jacobs. Trace semantics for coalgebras. In *Coalgebraic Methods in Computer Science (CMCS '04)*, volume 106 of ENTCS, pages 167–184, 2004.

19. O. H. Jensen. *Mobile Processes in Bigraphs*. PhD thesis, University of Cambridge, 2006.

20. A. Joyal, M. Nielsen, and G. Winsk. Bisimulation from open maps. *Inf. Comput.*, 127:164–185, 1994.

21. P. Katis, N. Sabadini, and R. F. C. Walters. Span(Graph): an algebra of transition systems. In *Algebraic Methodology and Software Technology (AMAST '97)*, volume 1349 of LNCS, pages 322–336. Springer, 1997.

22. G. M. Kelly and R. H. Street. Review of the elements of 2-categories. In *Category Theory*, number 420 in LNM, pages 75–103. Springer, 1973.

23. J. Koslowski. Simulations as a genuinely categorical concepts, 2006. Talk at CT2006, White Point, Nova Scotia, 30.06.2006.

24. J. J. Leifer and R. Milner. Deriving bisimulation congruences for reactive systems. In *Concurrency Theory (CONCUR '00)*. Springer, 2000.

25. P. Mosses. Modular structural operational semantics. *J. Logic Algebr. Progr.*, 60-61:195–228, 2004.

26. S. Niefield. Change of base for relational variable sets. *Theor. App. Categories*, 12(7):248–261, 2004.

27. P. R. Ribeiro, L. S. Barbosa, and S. Wang. An exercise on transition systems. In *Harnessing Theories for Tool Support in Software (TTSS '07)*, volume 207 of ENTCS, pages 89–106, 2007.

28. K. R. Rosenthal. *The theory of Quantaloids*. Addison-Wesley, 1996.

29. V. Sassone and P. Sobociński. Deriving bisimulation congruences using 2-categories. *Nord. J. Comput.*, 10(2):163–183, 2003.

30. V. Sassone and P. Sobociński. Locating reaction with 2-categories. *Theor. Comput. Sci.*, 333(1-2):297–327, 2005.

31. V. Schmitt and K. Worytkiewicz. Bisimulations of enrichments. arXiv:cs/0602077v1, 2006.

32. P. Sobociński. *Deriving process congruences from reaction rules*. PhD thesis, BRICS, University of Aarhus, 2004.

33. A. Sokolova, E. de Vink, and H. Woracek. Weak bisimulation for action-type coalgebras. In *Category Theory in Computer Science (CTCS '04)*, volume 122 of ENTCS, pages 211–228, 2004.
34. S. Staton. Relating coalgebraic notions of bisimulations. *Log. Meth. Comput. Sci.*, 7(1), 2011.

35. J. G. Stell. Granularity in change over time. In *Foundations of Geographic Information Science*, pages 95–115. Taylor and Francis, 2003.

36. D. Turi and G. D. Plotkin. Towards a mathematical operational semantics. In *Logic in Computer Science (LiCS '97)*, pages 280–291. IEEE Press, 1997.

37. G. Winskel and M. Nielsen. Models for concurrency. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, *Handbook of Logic in Computer Science*, pages 1–148. Oxford University Press, 1995.

38. G. Winskel and M. Nielsen. Presheaves as transition systems. In *Partial order methods in verification: DIMACS Workshop*, pages 129–140, 1996.