######  Definition  (Causal $\mathbb{O}$-ILTSAC).

The _Causal_ $\mathbb{O}$-ILTS ($\mathbb{O}$-ILTSAC)
$(\mathscr{M},\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
1.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\hbox{\kern
0.0pt\raise 1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
6.5pt\raise 3.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{$\scriptstyle{\quad}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 21.1111pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise 0.00002pt\hbox{\hbox{\kern
3.8889pt\hbox{{\hbox{\kern-3.8889pt\hbox{\ignorespaces\hbox{\kern
0.0pt\raise-2.57344pt\hbox{$\textstyle{\RHD}$}}}}}}}}}}}}{\hbox{\hbox{\kern
0.0pt\raise 1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}{\hbox{\hbox{\kern 0.0pt\raise
1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}{\hbox{\kern 25.0pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces)$ is the
smallest one generated by the rule

$\frac{O\rhd c\xRightarrow{K\vdash a}\delta(O,K,a)\rhd c^{\prime}}{O\rhd
c\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
1.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\hbox{\kern
0.0pt\raise 1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
2.78813pt\raise 5.43056pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\hbox{$\scriptstyle{K\vdash a}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 21.1111pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise 0.00002pt\hbox{\hbox{\kern
3.8889pt\hbox{{\hbox{\kern-3.8889pt\hbox{\ignorespaces\hbox{\kern
0.0pt\raise-2.57344pt\hbox{$\textstyle{\RHD}$}}}}}}}}}}}}{\hbox{\hbox{\kern
0.0pt\raise 1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}{\hbox{\hbox{\kern 0.0pt\raise
1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}{\hbox{\kern 25.0pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\boldsymbol{\delta}(O)\rhd
c^{\prime}[\epsilon(O,K,a)]}$

This translation does not affect bisimilarities: two states can do the same
transitions in CGAC if and only if they can do the same transitions also in
$\mathbb{O}$-ILTSAC; continuations only differ for an order-embedding, but by
section 3.2 and section 6ii, the $\mathbb{O}$-indexed bisimilarity and
$\sim_{\mathtt{AC}}$ are closed under order-embeddings.

We call _causal_ coalgebra the $B$-coalgebra equivalent to
$(\mathscr{M},\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
1.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\hbox{\kern
0.0pt\raise 1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
6.5pt\raise 3.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{$\scriptstyle{\quad}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 21.1111pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise 0.00002pt\hbox{\hbox{\kern
3.8889pt\hbox{{\hbox{\kern-3.8889pt\hbox{\ignorespaces\hbox{\kern
0.0pt\raise-2.57344pt\hbox{$\textstyle{\RHD}$}}}}}}}}}}}}{\hbox{\hbox{\kern
0.0pt\raise 1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}{\hbox{\hbox{\kern 0.0pt\raise
1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}{\hbox{\kern 25.0pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces)$. We have the
following theorem, which collects the results of this section, instantiated to
the causal coalgebra.

######  Theorem .

$\mathbb{O}$-indexed bisimulations on $(\mathscr{M},\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
1.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\hbox{\kern
0.0pt\raise 1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
6.5pt\raise 3.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{$\scriptstyle{\quad}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 21.1111pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise 0.00002pt\hbox{\hbox{\kern
3.8889pt\hbox{{\hbox{\kern-3.8889pt\hbox{\ignorespaces\hbox{\kern
0.0pt\raise-2.57344pt\hbox{$\textstyle{\RHD}$}}}}}}}}}}}}{\hbox{\hbox{\kern
0.0pt\raise 1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}{\hbox{\hbox{\kern 0.0pt\raise
1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}{\hbox{\kern 25.0pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces)$ are
equivalent to:

  * •

$B$-bisimulations on the causal coalgebra;

  * •

$\mathtt{AC}$-bisimulations closed under order-embeddings.

In particular, we have that the greatest $\mathbb{O}$-indexed bisimulation,
$B$-bisimilarity on the causal coalgebra and $\sim_{\mathtt{AC}}$ are all
equivalent, thanks to section 3.2. These, by section 6, are equivalent to the
kernel of the unique morphism from the causal coalgebra to the final one.

##  7 From coalgebras to HD-automata

In order to give a characterization of the causal coalgebra in terms of named
sets, we employ the results of [10]. Here authors define a _symmetry group
over a category $\mathbf{C}$_ to be a collection of morphisms in
$\mathbf{C}[c,c]$, for any $c\in|\mathbf{C}|$, which is a group w.r.t.
composition of morphisms. Then they take families of such groups as their
notion of generalized named sets. A first result establishes the equivalence
between these families and _coproducts of symmetrized representables_ , that
are functors of the form

$\sum_{i\in I}\operatorname{Hom}_{\mathbf{C}}(c_{i},\\_)_{/\Phi_{i}}$

where $\Phi_{i}$ is a symmetry group over $\mathbf{C}$ with domain $c_{i}$,
and the quotient identifies morphisms that are obtained one from the other by
precomposing elements of $\Phi_{i}$. These functors, in turn, are shown to be
isomorphic to _wide-pullback-preserving_ presheaves on $\mathbf{C}$, a wide
pullback being the limit of a diagram with an arbitrary number of morphisms
pointing to the same object (pullbacks are a special case, with two such
morphisms). The described results are summarized in the following theorem from
[10].

######  Theorem .

Let $\mathbf{C}$ be a category that is small, has wide pullbacks, and such
that all its morphisms are monic and those in $\mathbf{C}[c,c]$ are
isomorphisms, for every $c\in|\mathbf{C}|$. Then every wide-pullback-
preserving $P\\!\in\\!|\mathbf{Set}^{\mathbf{C}}|$ is equivalent to a
coproduct of symmetrized representables.

Our category $\mathbb{O}$ satisfies the hypothesis of this theorem: it is
small and has wide pullbacks due to the existence of pullbacks. In fact, the
diagram of a wide pullback in $\mathbb{O}$ is formed by a finite number of
morphisms, because a finite poset always has a finite number of ingoing poset-
reflecting monomorphisms, so its limit can be computed via binary pullbacks.
Moreover, $\mathbb{O}$ has only monos, as order-embeddings are always monic,
and $\mathbb{O}[O,O]$ clearly has only isomorphisms, for each
$O\in|\mathbb{O}|$. Finally, our presheaf of causal markings $\mathscr{M}$
preserves (wide) pullbacks (section 6), so there exists an equivalent
coproduct of symmetrized representables.

section 7 indeed describes an equivalence between pullback-preserving
presheaves and families, which induces one on coalgebras. We shall now
investigate this point. Let $\mathbf{Set}^{\mathbb{O}}_{\diamond}$ be the full
subcategory of $\mathbf{Set}^{\mathbb{O}}$ formed by pullback-preserving
presheaves. We have that our behavioral endofunctor $B$ indeed defines an
endofunctor on $\mathbf{Set}^{\mathbb{O}}_{\diamond}$.

######  Proposition .

All the endofunctors on $\mathbf{Set}^{\mathbb{O}}$ in section 6 can be
restricted to endofunctors on $\mathbf{Set}^{\mathbb{O}}_{\diamond}$.

Let
$B_{\diamond}\colon\mathbf{Set}^{\mathbb{O}}_{\diamond}\to\mathbf{Set}^{\mathbb{O}}_{\diamond}$
be the restricted behavioral endofunctor. The causal coalgebra is clearly a
$B_{\diamond}$-coalgebra. Restricting to
$\mathbf{Set}^{\mathbb{O}}_{\diamond}$ does not affect the final coalgebra:
${B}\textbf{-Coalg}$ and ${B_{\diamond}}\textbf{-Coalg}$ have the same final
object and final morphisms from common objects. In fact, the terminal sequence
starts from the final presheaf $1$, pointwise defined as the singleton set,
which trivially preserves pullbacks, and goes through
$B^{n}(1)=B_{\diamond}^{n}(1)$, for any $n$.

######  Corollary  (of section 7).

Let $\widetilde{B}$ be the behavioral endofunctor on families defined by
lifting all functors in section 6 along the equivalence. Then the category
${B_{\diamond}}\textbf{-Coalg}$ is equivalent to
${\widetilde{B}}\textbf{-Coalg}$.

In particular, the equivalence relates the final $B_{\diamond}$-coalgebra and
the final $\widetilde{B}$-coalgebra, and their final morphisms. Moreover,
since kernels are preserved by equivalence, identifications made by the final
morphisms are preserved, hence behavioral equivalence is preserved too.

Now that we have proved that our categorical setting is suitable for HD-
automata, we can translate the causal coalgebra to a HD-automaton. We adopt
the definition of HD-automaton given in [11]: a HD-automaton is a(ny)
coalgebra over a named set. We introduce a notion of named set closer to a
more traditional one, but indeed equivalent to the families mentioned above.
Given a set $S$ of morphism and a morphism $\sigma$ in $\mathbb{O}$, we write
$S\circ\sigma$ for the set $\\{\tau\circ\sigma\mid\tau\in S\\}$ (analogously
for $\sigma\circ S$).

######  Definition  (Category $\textbf{Sym}(\mathbb{O})$).

Let $\textbf{Sym}(\mathbb{O})$ be the category defined as follows:

  * •

objects $\Phi$ are subsets of $\mathbb{O}[O,O]$ that are groups w.r.t.
composition in $\mathbb{O}$;

  * •

morphisms $\Phi_{1}\to\Phi_{2}$ are sets of morphisms $\sigma\circ\Phi_{1}$
such that $\sigma\colon dom(\Phi_{1})\to dom(\Phi_{2})$ and
$\Phi_{2}\circ\sigma\subseteq\sigma\circ\Phi_{1}$.

######  Definition  (Category $\mathbb{O}\textbf{-Set}$).

The category $\mathbb{O}\textbf{-Set}$ is defined as follows:

  * •

objects are _$\mathbb{O}$ -named sets_, that are pairs
$N=(Q_{N},\mathtt{G}_{N})$ of a set $Q_{N}$ and a function
$\mathtt{G}_{N}\colon Q_{N}\to|Sym(\mathbb{O})|$. The _local poset_ of $q\in
Q_{N}$, denoted $\|q\|$, is $dom(\sigma)$, for any
$\sigma\in\mathtt{G}_{N}(q)$.

  * •

morphisms $f\colon N\to M$ are _$\mathbb{O}$ -named functions_, that are pairs
$(h,\Sigma)$ of a function $h\colon Q_{N}\to Q_{M}$ and a function $\Sigma$
mapping each $q\in Q_{N}$ to a morphism
$\mathtt{G}_{M}(h(q))\to\mathtt{G}_{N}(q)$ in $Sym(\mathbb{O})$.

In the rest of this section we give an explicit description of the
$\mathbb{O}$-named set produced from $\mathscr{M}$ by the equivalence. Its
elements will be minimal P-markings with symmetries. We will show that the
translation from P-markings to minimal ones with symmetries is achieved via
categorical constructions. We need the notions of support, seed and orbit.

######  Definition  (Support and seed).

Given $O\rhd c$, its _support_ , denoted $supp(c)$, is the wide-pullback-
object of the following morphisms

$\\{\sigma\colon O^{\prime}\to O\mid\exists O^{\prime}\rhd
c^{\prime}:c^{\prime}[\sigma]=c\\}$

Let $\Sigma_{c}$ be the embedding $supp(c)\hookrightarrow O$ given by the
pullback. Then the _seed_ of $c$, denoted $seed(c)$, is the unique element of
$\mathscr{M}(supp(c))$ such that $seed(c)[\Sigma_{c}]=c$.

As shown in [10, 15], preservation of pullbacks by $\mathscr{M}$ is essential
to ensure existence and uniqueness of seeds. The seed operation achieves the
first two properties of minimal P-markings (see section 3.3): $seed(c)$ just
contains immediate causes for each token and $supp(c)$ contains all and only
those causes. This is illustrated by the following example.

######  Example .

Consider the following P-marking for the running example

$\\{e_{a}\preccurlyeq e^{\prime}_{a},e^{\prime\prime}_{a}\preccurlyeq
e^{\prime\prime\prime}_{a}\\}\rhd\\{\\{e_{a},e^{\prime}_{a}\\}\vdash
s_{1},\\{e^{\prime\prime}_{a},e^{\prime\prime\prime}_{a}\\}\vdash s_{2}\\}$

which is reachable after firing $t_{1}$ and $t_{2}$ twice. The set of
morphisms of section 7 has four elements

$f_{1},f_{2}\colon\\{e_{a}\preccurlyeq
e^{\prime}_{a},e^{\prime\prime}_{a}\\}\to\\{e_{a}\preccurlyeq
e^{\prime}_{a},e^{\prime\prime}_{a}\preccurlyeq
e^{\prime\prime\prime}_{a}\\}\qquad
f_{3},f_{4}\colon\\{e_{a},e^{\prime}_{a}\\}\to\\{e_{a}\preccurlyeq
e^{\prime}_{a},e^{\prime\prime}_{a}\preccurlyeq e^{\prime\prime\prime}_{a}\\}$
$f_{1}=\begin{cases}e_{a}\longmapsto e_{a}\\\ e^{\prime}_{a}\longmapsto
e^{\prime}_{a}\\\ e^{\prime\prime}_{a}\longmapsto
e^{\prime\prime\prime}_{a}\end{cases}\qquad
f_{2}=\begin{cases}e_{a}\longmapsto e^{\prime\prime}_{a}\\\
e^{\prime}_{a}\longmapsto e^{\prime\prime\prime}_{a}\\\
e^{\prime\prime}_{a}\longmapsto e^{\prime}_{a}\end{cases}\qquad
f_{3}=\begin{cases}e_{a}\longmapsto e^{\prime}_{a}\\\
e^{\prime}_{a}\longmapsto e^{\prime\prime\prime}_{a}\end{cases}\qquad
f_{4}=\begin{cases}e_{a}\longmapsto e^{\prime\prime\prime}_{a}\\\
e^{\prime}_{a}\longmapsto e^{\prime}_{a}\end{cases}$

In fact, we have

$\left.\begin{aligned} (\\{e_{a}\preccurlyeq
e^{\prime}_{a},e^{\prime\prime}_{a}\\}\rhd\\{\\{e_{a},e^{\prime}_{a}\\}\vdash
s_{1},\\{e^{\prime\prime}_{a}\\}\vdash s_{2}\\})\ [f_{1}]\\\\[4.30554pt]
(\\{e_{a}\preccurlyeq
e^{\prime}_{a},e^{\prime\prime}_{a}\\}\rhd\\{\\{e^{\prime\prime}_{a}\\}\vdash
s_{1},\\{e_{a},e^{\prime}_{a}\\}\vdash s_{2}\\})\ [f_{2}]\\\\[4.30554pt]
(\\{e_{a},e^{\prime}_{a}\\}\rhd\\{\\{e_{a}\\}\vdash
s_{1},\\{e^{\prime}_{a}\\}\vdash s_{2}\\})\ [f_{3}]\\\\[4.30554pt]
(\\{e_{a},e^{\prime}_{a}\\}\rhd\\{\\{e^{\prime}_{a}\\}\vdash
s_{1},\\{e_{a}\\}\vdash s_{2}\\})\
[f_{4}]\end{aligned}\right\\}=\\{e_{a}\preccurlyeq
e^{\prime}_{a},e^{\prime\prime}_{a}\preccurlyeq
e^{\prime\prime\prime}_{a}\\}\rhd\\{\\{e_{a},e^{\prime}_{a}\\}\vdash
s_{1},\\{e^{\prime\prime}_{a},e^{\prime\prime\prime}_{a}\\}\vdash s_{2}\\}$

Recall that each $[f_{i}]=\mathscr{M}(f_{i})$ is a function that, when applied
to a P-marking, replaces events according to $f_{i}$ and then down-closes the
result w.r.t. $\\{e_{a}\preccurlyeq
e^{\prime}_{a},e^{\prime\prime}_{a}\preccurlyeq
e^{\prime\prime\prime}_{a}\\}$. It is easy to check that the pullback object
of all four morphisms is $\\{e_{a},e^{\prime}_{a}\\}$, so the corresponding
seed is

$\\{e_{a},e^{\prime}_{a}\\}\rhd\\{\\{e_{a}\\}\vdash
s_{1},\\{e^{\prime}_{a}\\}\vdash s_{2}\\}.$

Notice that two events have been discarded, because they are not immediate
causes.

######  Definition  (Orbit).

The _orbit_ of $O\rhd c$ is

$orb(c)=\\{c[\sigma]\mid\sigma\in\mathbb{O}[O,O]\\}$

We denote by $[c]^{o}$ a canonical choice of an element of $orb(c)$.

The _orbit_ of $c$ is the set of causal markings obtained by applying to $c$
all functions induced by poset automorphisms. Automorphisms are isomorphisms,
so taking a canonical representative for this orbit achieves the third
requirement of minimal P-markings: it amounts to applying the operation
$[O\rhd c]_{\cong}$, i.e., choosing a representative of isomorphism classes
for $O\rhd c$.

######  Definition .

The $\mathbb{O}$-named set of minimal P-markings is $(M,\mathtt{G}_{M})$,
where

$\displaystyle M$ $\displaystyle=\\{supp(c)\RHD[seed(c)]^{o}\mid O\rhd
c\in\mathord{\int}\mathscr{M}\\}$ $\displaystyle\mathtt{G}_{M}$
$\displaystyle=\lambda O\RHD c.\\{\Phi\in|\textbf{Sym}(\mathbb{O})|\mid
dom(\Phi)=O\land\forall\sigma\in\Phi:c[\sigma]=c\\}$

The set $M$ is produced from elements of $\mathscr{M}$: for each of these, we
compute the seed, and then we only take the canonical representative for the
seed’s orbit. As explained, the final result is indeed a minimal P-marking
$O\RHD c$. This P-marking is associated a symmetry by $\mathtt{G}_{M}$, namely
$\Phi=\mathtt{G}_{M}(O\RHD c)$, so it becomes the P-marking with symmetry
${O}\RHD_{\Phi}{c}$.

The derivation of an HD-automaton on $(M,\mathtt{G}_{M})$ in
${\widetilde{B}}\textbf{-Coalg}$ from the causal coalgebra, along the
equivalence, is the category-theoretic counterpart of the derivation of CGICS
from CGAC. The correspondence between CGICSs and coalgebras over named sets is
analogous to the $\pi$-calculus case, where we have set-theoretical HD-
automata on one side [19] and categorical ones, namely coalgebras over named
sets, on the other side. The correspondence for the $\pi$-calculus has been
worked out in [9, 11], and the theory introduced therein seems robust enough
to accommodate different notions of named sets such as ours. In particular,
functors used to define coalgebras over named sets, such as powerset and
allocation functors, should be very similar to those defining $\tilde{B}$.

We briefly illustrate the $\tilde{B}$-coalgebra for the running example. The
$\mathbb{O}$-named set $(M,\mathtt{G}_{M})$ is as follows: $M$ includes all
P-markings in Figure 3, and $\mathtt{G}_{M}$ returns the symmetry $\\{id\\}$
for each of them. Transitions are represented as a $\mathbb{O}$-named function
$(h,\Sigma)\colon(M,\mathtt{G}_{M})\to\widetilde{B}(M,\mathtt{G}_{M})$, where
$h$ maps each state ${O}\RHD_{\\{id\\}}{c}$ to its label and continuation, and
$\Sigma({O}\RHD_{\\{id\\}}{c})$ encodes all history maps for outgoing
transitions.

We leave a deeper investigation of the category of $\mathbb{O}$-named sets and
of $\tilde{B}$-coalgebras for future work.

##  8 Conclusions

In this paper we have introduced an approach to derive compact operational
models for causality in Petri nets. In order to do this, we have constructed a
labeled semantics of Petri nets in terms of causal case graphs, and we have
given a procedure to refine them in order to get minimal, possibly finite-
state, representations. We have then modeled causal case graphs in a
categorical setting, exploiting a nominal representation of causal relations:
they are modeled as posets over event names with action labels. Our
categorical treatment is simpler and more natural than the set-theoretic one,
and employs standard constructs and results for nominal calculi, namely
presheaf-based coalgebras and their equivalence with HD-automata. In
particular, reducing the state-space and showing that this operation preserves
the semantics require some technical effort in the set-theoretic version,
whereas the categorical version employs a general construction that
automatically performs this reduction in a semantics-preserving way.

Our approach has a practical significance: we show how to synthesize HD-
automata from Petri nets, and how to compute minimal realizations for them, in
order to detect bisimilar states. As mentioned, minimization of HD-automata is
possible in many cases. Even if our approach does not actually provide a way
to minimize nets themselves, one can still decide bisimilarity of markings by
minimizing their reachable HD-automata and matching the results.

Finally, our contribution is also methodological: we provide a further example
in which the presheaf/HD-automata framework is successfully applied. We
emphasize that this framework is highly parametric and can possibly be useful
in many other cases.

###  8.1 Related work

This paper follows a line of research on coalgebraic models of causality,
started in [7] by the same authors. The categorical machinery is the same in
both papers, namely presheaf-based coalgebras, HD-automata, and the
equivalence among them. However, this paper takes a further step towards a
general categorical theory of causality. In [7], in fact, we have provided
models for a particular class of causal LTSs, namely Degano-Darondeau ones. In
this paper, instead, we treat Petri nets, which are much more general. For
instance, unlike Degano-Darondeau LTSs, Petri nets can describe
synchronizations of more than two processes.

In [7] we start from existing set-theoretic models, similar to abstract CGs,
whereas the models we introduce here are novel. In both papers we represent
causal dependencies as posets over events, but in [7] events are unlabeled and
are canonically represented as natural numbers. Here we have labels and we
take a more general approach: instead of choosing specific representatives of
events, we make abstract CGs parametric in this choice. This requires more
technical work and it further validates the categorical approach, where book-
keeping details are abstracted away. The categorical environment in this paper
is more elaborate than [7], due to labeling. In particular, event generation
is more complex, and is studied in greater detail. Another difference is that
here we give conditions under which the model with only immediate causes is
finite, whereas in [7] decidability is not treated.

A first version of HD-automata for Petri nets, called _causal automata_ , has
been introduced in [18]. However, their construction is purely set-theoretical
and does not include symmetries, so the existence of a minimal model is not
guaranteed. This version of HD-automata is similar to what we call immediate
causes CG (without symmetries). HD-automata with symmetries were developed for
the $\pi$-calculus in [21, 19], and a general categorical treatment was
provided in [11]. In all these cases nominal structures associated to states
are just a sets of (event) names, whereas we have posets, which are more
adequate to represent causal dependencies.

We can cite [8] for the introduction of transitions systems for causality
whose states are elements of presheaves, intended to model the causal
semantics of the $\pi$-calculus as defined in [6]. However, the index of a
state is a set of names, without any information about events and causal
relations. The advantage of our index category is that it allows reducing the
state-space in an automatic way, exploiting a standard categorical
construction. This cannot be done in the framework of [8]. Finally, an HD-
automaton for causality has been described in [11], but it is derived as a
direct translation of causal automata and its states do not take into account
causal relations.

Other related works are [26, 28], where event structures have been
characterized as (contravariant) presheaves on posets. While the meaning of
presheaves is similar, the context is different: we consider the more concrete
realm of coalgebras and nominal automata. A more precise correspondence with
such models should be worked out.

###  8.2 Future work

Logics for causality have been recently studied in [5]. As future work, we
would like to understand whether they can be captured in our coalgebraic
setting. Another open research question is how to obtain coalgebraic models
for other notions of causal bisimulation, such as hereditary history
preserving bisimulation.

## References

  * [1] Jir̂í Adámek.  Introduction to coalgebra.  TAC, 14(8):157–199, 2005.
  * [2] Jirí Adámek, Filippo Bonchi, Mathias Hülsbusch, Barbara König, Stefan Milius, and Alexandra Silva.  A coalgebraic perspective on minimization and determinization.  In FoSSaCS, pages 58–73, 2012.
  * [3] Jir̂í Adámek and Jir̂í Rosický.  Locally Presentable and Accessible Categories.  Cambridge University Press, 1994.
  * [4] Paolo Baldan and Alberto Carraro.  Non-interference by unfolding.  In PETRI NETS, pages 190–209, 2014.
  * [5] Paolo Baldan and Silvia Crafa.  A logic for true concurrency.  J. ACM, 61(4):24, 2014.
  * [6] Michele Boreale and Davide Sangiorgi.  A fully abstract semantics for causality in the $\pi$-calculus.  Acta Inf., 35(5):353–400, 1998.
  * [7] Roberto Bruni, Ugo Montanari, and Matteo Sammartino.  Revisiting causality, coalgebraically.  Acta Inf., 52(1):5–33, 2015.  Preprint available at http://www.cs.ru.nl/M.Sammartino/publications/ACTA2014.pdf.
  * [8] Gian Luca Cattani and Peter Sewell.  Models for name-passing processes: interleaving and causal.  Inf. Comput., 190(2):136–178, 2004.
  * [9] Vincenzo Ciancia.  Accessible Functors and Final Coalgebras for Named Sets.  PhD thesis, University of Pisa, 2008.
  * [10] Vincenzo Ciancia, Alexander Kurz, and Ugo Montanari.  Families of symmetries as efficient models of resource binding.  Electr. Notes Theor. Comput. Sci., 264(2):63–81, 2010.
  * [11] Vincenzo Ciancia and Ugo Montanari.  Symmetries, local names and dynamic (de)-allocation of names.  Inf. Comput., 208(12):1349 – 1367, 2010.
  * [12] Gian Luigi Ferrari, Ugo Montanari, and Emilio Tuosto.  Coalgebraic minimization of HD-automata for the $\pi$-calculus using polymorphic types.  Theor. Comput. Sci., 331(2-3):325–365, 2005.
  * [13] Marcelo P. Fiore and Daniele Turi.  Semantics of name and value passing.  In LICS, pages 93–104, 2001.
  * [14] Sibylle B. Fröschle and Thomas T. Hildebrandt.  On plain and hereditary history-preserving bisimulation.  In MFCS, pages 354–365, 1999.
  * [15] Fabio Gadducci, Marino Miculan, and Ugo Montanari.  About permutation algebras, (pre)sheaves and named sets.  Higher-Order and Symbolic Computation, 19(2-3):283–304, 2006.
  * [16] André Joyal, Mogens Nielsen, and Glynn Winskel.  Bisimulation from open maps.  Inf. Comput., 127(2):164–185, 1996.
  * [17] Paris C. Kanellakis and Scott A. Smolka.  Ccs expressions, finite state processes, and three problems of equivalence.  Inf. Comput., 86(1):43–68, 1990.
  * [18] Ugo Montanari and Marco Pistore.  Minimal transition systems for history-preserving bisimulation.  In STACS, pages 413–425, 1997.
  * [19] Ugo Montanari and Marco Pistore.  Structured coalgebras and minimal HD-automata for the $\pi$-calculus.  Theor. Comput. Sci., 340(3):539–576, 2005.
  * [20] Mogens Nielsen, Gordon D. Plotkin, and Glynn Winskel.  Petri nets, event structures and domains, part I.  Theor. Comput. Sci., 13:85–108, 1981.
  * [21] Marco Pistore.  History Dependent Automata.  PhD thesis, University of Pisa, 1999.
  * [22] Jan J. M. M. Rutten.  Universal coalgebra: a theory of systems.  Theor. Comput. Sci., 249(1):3–80, 2000.
  * [23] Davide Sangiorgi and David Walker.  $\pi$-Calculus: A Theory of Mobile Processes.  Cambridge University Press, New York, NY, USA, 2001.
  * [24] Sam Staton.  Name-passing process calculi: operational models and structural operational semantics.  Technical Report 688, University of Cambridge, 2007.
  * [25] Sam Staton.  Relating coalgebraic notions of bisimulation.  LMCS, 7(1), 2011.
  * [26] Sam Staton and Glynn Winskel.  On the expressivity of symmetry in event structures.  In LICS, pages 392–401, 2010.
  * [27] Boris A. Trakhtenbrot and Alexander Moshe Rabinovich.  Behavior structures and nets of processes.  Fund. Inf., 11(4):357–403, 1988.
  * [28] Glynn Winskel.  Event structures as presheaves — two representation theorems.  In CONCUR, pages 541–556, 1999.
  * [29] James Worrell.  Terminal sequences for accessible endofunctors.  Electr. Notes Theor. Comput. Sci., 19:24–38, 1999.

##  A Proofs

We first introduce some technical lemmata. Then we give proofs for the claims
in the paper.

###  A.1 Additional lemmata

######  Lemma .

Let $O_{1},O_{2}$ be finite $Act$-labeled posets and let $\sigma\colon
O_{1}\to O_{2}$ be an order-embedding. Then:

  1. $(i)$

$O_{1}\rhd c\xrightarrow{K\vdash{e}_{a}}\delta(O_{1},K,e_{a})\rhd c^{\prime}$
implies
$O_{2}\rhd{{(c\sigma)}\\!\\!\downarrow_{O_{2}}}\xrightarrow{\sigma(K)\vdash{e^{\prime}_{a}}}O_{2}^{\prime}\rhd{{(c^{\prime}\sigma[\nicefrac{{e^{\prime}_{a}}}{{e_{a}}}])}\\!\\!\downarrow_{O_{2}^{\prime}}}$,
for any $e^{\prime}\notin X_{O_{2}}$, with
$O_{2}^{\prime}=\delta(O_{2},\sigma(K),e^{\prime}_{a})$;

  2. $(ii)$

$O_{2}\rhd c\xrightarrow{K\vdash{e}_{a}}\delta(O_{2},K,e_{a})\rhd c^{\prime}$
implies $O_{1}\rhd
c^{\prime\prime}\xrightarrow{K^{\prime}\vdash{e^{\prime}_{a}}}\delta(O_{1},K^{\prime},e^{\prime}_{a})\rhd
c^{\prime\prime\prime}$, with $c^{\prime\prime}\sigma=c$,
$\sigma(K^{\prime})=K$ and
$c^{\prime\prime\prime}\sigma[\nicefrac{{e_{a}}}{{e^{\prime}_{a}}}]=c^{\prime}$,
for any $e^{\prime}\notin X_{O_{1}}$.

###### Proof.

We prove item (i), the other one is analogous. Suppose $O_{1}\rhd
c\xrightarrow{K\vdash{e}_{a}}\delta(O_{1},K,e_{a})\rhd c^{\prime}$ is derived
from the rule of section 3.1 as follows

$\frac{t\in T\quad|c_{1}|={}^{\bullet}{t}\quad a=l(t)\quad e\notin
X_{O_{1}}\quad K=\max_{O_{1}}\mathscr{K}(c_{1})}{O_{1}\rhd c_{1}\cup
c_{2}\xrightarrow{K\vdash{e}_{a}}\delta(O_{1},K,e_{a})\rhd(\mathscr{K}(c_{1})\cup\\{e_{a}\\}\vdash{t}^{\bullet})\cup
c_{2}}$

where $c=c_{1}\cup c_{2}$ and
$c^{\prime}=(\mathscr{K}(c_{1})\cup\\{e_{a}\\}\vdash{t}^{\bullet})\cup c_{2}$.
Clearly we have
${{(c\sigma)}\\!\\!\downarrow_{O_{2}}}={{(c_{1}\sigma)}\\!\\!\downarrow_{O_{2}}}\cup{{(c_{2}\sigma)}\\!\\!\downarrow_{O_{2}}}$,
with $|{{(c_{1}\sigma)}\\!\\!\downarrow_{O_{2}}}|=|c_{1}|$, because $\sigma$
only affects events, not tokens. Moreover, it can be easily verified that
$\max_{O_{2}}\mathscr{K}({{(c_{1}\sigma)}\\!\\!\downarrow_{O_{2}}})=\sigma(\max_{O_{1}}\mathscr{K}(c_{1}))=\sigma(K)$.
In fact, causes of ${{(c_{1}\sigma)}\\!\\!\downarrow_{O_{2}}}$ are: those of
$c_{1}\sigma$, related exactly as their counterimages, due to $\sigma$
preserving and reflecting order; additional causes, smaller than those of
$c_{1}\sigma$, added by the closure. Therefore we can again apply the rule as
follows

$\frac{t\in
T\quad|{{(c_{1}\sigma)}\\!\\!\downarrow_{O_{2}}}|={}^{\bullet}{t}\quad
a=l(t)\quad e^{\prime}\notin
X_{O_{2}}\quad\sigma(K)=\max_{O_{2}}\mathscr{K}({{(c_{1}\sigma)}\\!\\!\downarrow_{O_{2}}})}{O_{2}\rhd{{(c_{1}\sigma)}\\!\\!\downarrow_{O_{2}}}\cup{{(c_{2}\sigma)}\\!\\!\downarrow_{O_{2}}}\xrightarrow{\sigma(K)\vdash{e^{\prime}_{a}}}O_{2}^{\prime}\rhd(\mathscr{K}({{(c_{1}\sigma)}\\!\\!\downarrow_{O_{2}}})\cup\\{e^{\prime}_{a}\\}\vdash{t}^{\bullet})\cup{{(c_{2}\sigma)}\\!\\!\downarrow_{O_{2}}}}$

where $O_{2}^{\prime}=\delta(O_{2},\sigma(K),e^{\prime}_{a})$. Now, observe
that, by definition of $\delta$, we have

$\mathscr{K}({{(c_{1}\sigma)}\\!\\!\downarrow_{O_{2}}})\subseteq\mathscr{K}({{(c_{1}\sigma)}\\!\\!\downarrow_{O^{\prime}_{2}}})\qquad{{\\{e^{\prime}_{a}\\}}\\!\\!\downarrow_{O^{\prime}_{2}}}=\mathscr{K}({{(c_{1}\sigma)}\\!\\!\downarrow_{O^{\prime}_{2}}})\cup\\{e^{\prime}_{a}\\}$

which implies

$\displaystyle\mathscr{K}({{(c_{1}\sigma)}\\!\\!\downarrow_{O_{2}}})\cup\\{e^{\prime}_{a}\\}\vdash{t}^{\bullet}$
$\displaystyle={{(\mathscr{K}(c_{1}\sigma)\cup\\{e^{\prime}_{a}\\})}\\!\\!\downarrow_{O^{\prime}_{2}}}\vdash{t}^{\bullet}$
$\displaystyle={{(\mathscr{K}(c_{1})\cup\\{e_{a}\\})\sigma[\nicefrac{{e^{\prime}_{a}}}{{e_{a}}}]}\\!\\!\downarrow_{O_{2}^{\prime}}}\vdash{t}^{\bullet}$
$\displaystyle={{(\mathscr{K}(c_{1})\cup\\{e_{a}\\}\vdash{t}^{\bullet})\sigma[\nicefrac{{e^{\prime}_{a}}}{{e_{a}}}]}\\!\\!\downarrow_{O_{2}^{\prime}}}$

From this equation, and from
${{(c_{2}\sigma)}\\!\\!\downarrow_{O_{2}}}={{(c_{2}\sigma[\nicefrac{{e^{\prime}_{a}}}{{e_{a}}}])}\\!\\!\downarrow_{O_{2}^{\prime}}}$,
because $e_{a}\notin\mathscr{K}(c_{2})$, it follows that the continuation
derived from the above rule has the required shape. ∎

######  Lemma .

Let $\sigma\colon O\to O^{\prime}$ be an isomorphism. Then $O\rhd
c_{1}\sim_{\mathtt{C}}O\rhd c_{1}$ implies $O^{\prime}\rhd
c_{1}\sigma\sim_{\mathtt{C}}O^{\prime}\rhd c_{2}\sigma$.

###### Proof.

We will prove that the following relation is a $\mathtt{C}$-bisimulation

$R_{O^{\prime}}=\\{(O^{\prime}\rhd c_{1}\sigma,O^{\prime}\rhd c_{2}\sigma)\mid
O\rhd c_{1}\sim_{\mathtt{C}}O\rhd c_{2},\text{$\sigma\colon O\to O^{\prime}$
is an isomorphism}\\}$

Take $(O^{\prime}\rhd c_{1}\sigma,O^{\prime}\rhd c_{2}\sigma)\in
R_{O^{\prime}}$ and

$O^{\prime}\rhd
c_{1}\sigma\xrightarrow{K^{\prime}\vdash{e^{\prime}}_{a}}\delta(O^{\prime},K^{\prime},e^{\prime}_{a})\rhd
c_{1}^{\prime}$

We have to find a simulating transition of $O^{\prime}\rhd c_{2}\sigma$. Let
$e\notin X_{O}$. We can apply section 3.2, using the isomorphism
$\sigma^{-1}[\nicefrac{{e_{a}}}{{e^{\prime}_{a}}}]$, and get

$O\rhd
c_{1}\xrightarrow{\sigma^{-1}(K)\vdash{e}_{a}}\delta(O,\sigma^{-1}(K),e_{a})\rhd
c_{1}^{\prime}\sigma^{-1}[\nicefrac{{e_{a}}}{{e^{\prime}_{a}}}]$

Since $O\rhd c_{1}\sim_{\mathtt{C}}O\rhd c_{2}$, there is a simulating
transition

$O\rhd
c_{2}\xrightarrow{\sigma^{-1}(K)\vdash{e}_{a}}\delta(O,\sigma^{-1}(K),e_{a})\rhd
c_{2}^{\prime}\enspace.$

Applying again section 3.2 with $\sigma[\nicefrac{{e^{\prime}_{a}}}{{e_{a}}}]$
to this transition, we get

$O^{\prime}\rhd
c_{2}\sigma\xrightarrow{K^{\prime}\vdash{e^{\prime}}_{a}}\delta(O^{\prime},K^{\prime},e^{\prime}_{a})\rhd
c_{2}^{\prime}\sigma[\nicefrac{{e^{\prime}_{a}}}{{e_{a}}}]\enspace.$

This is the required simulating transition. In fact, since

$\delta(O,\sigma^{-1}(K),e_{a})\rhd
c_{1}^{\prime}\sigma^{-1}[\nicefrac{{e_{a}}}{{e^{\prime}_{a}}}]\;\;\sim_{\mathtt{C}}\;\;\delta(O,\sigma^{-1}(K),e_{a})\rhd
c_{2}^{\prime}$

and $\sigma[\nicefrac{{e^{\prime}_{a}}}{{e_{a}}}]$ is an isomorphism, by
definition of $R_{O^{\prime}}$ we have

$(\;\delta(O^{\prime},K^{\prime},e^{\prime}_{a})\rhd
c_{1}^{\prime}\;\;,\;\;\delta(O^{\prime},K^{\prime},e^{\prime}_{a})\rhd
c_{2}^{\prime}\sigma[\nicefrac{{e^{\prime}_{a}}}{{e_{a}}}]\;)\in
R_{O^{\prime}}\enspace.$

∎

######  Lemma .

Let $O\rhd c_{1}$ and $O\rhd c_{2}$ be abstract P-markings. Then $O\rhd
c_{1}\sim_{\mathtt{C}}O\rhd c_{2}$ if and only if $O\rhd
c_{1}\sim_{\mathtt{AC}}O\rhd c_{2}$.

###### Proof.

We show the left-to-right implication, the other one is analogous. We prove
that the following relation is an $\mathtt{AC}$-bisimulation

$R_{O}=\\{(O\rhd c_{1},O\rhd c_{2})\mid O\rhd c_{1}\sim_{\mathtt{C}}O\rhd
c_{2}\\}$

Take $(O\rhd c_{1},O\rhd c_{2})\in R_{O}$ and suppose

$O\rhd c_{1}\xRightarrow{K\vdash a}\delta(O,K,a)\rhd c_{1}^{\prime}$

then we must find a simulating transition of $O\rhd c_{2}$. By section 3.2,
the above transition can be derived from

$O\rhd c_{1}\xrightarrow{K\vdash{e}_{a}}\delta(O,K,e_{a})\rhd
c_{1}^{\prime\prime}$

with
$c^{\prime\prime}_{1}old(O,K,e_{a})[\nicefrac{{new(O,K,e_{a})}}{{e_{a}}}]=c^{\prime}_{1}$.
Since $O\rhd c_{1}\sim_{\mathtt{C}}O\rhd c_{2}$ by hypothesis, this transition
can be simulated by

$O\rhd c_{2}\xrightarrow{K\vdash{e}_{a}}\delta(O,K,e_{a})\rhd
c_{2}^{\prime\prime}\enspace.$

Applying again section 3.2, we get the required transition

$O\rhd c_{2}\xRightarrow{K\vdash a}\delta(O,K,a)\rhd
c_{2}^{\prime\prime}(old(O,K,e_{a})[\nicefrac{{new(O,K,e_{a})}}{{e_{a}}}]).$

In fact, from $\delta(O,K,e_{a})\rhd
c_{1}^{\prime\prime}\sim_{\mathtt{C}}\delta(O,K,e_{a})\rhd
c_{2}^{\prime\prime}$, using section A.1 with the isomorphism
$old(O,K,e_{a})[\nicefrac{{new(O,K,e_{a})}}{{e_{a}}}]$, we get

$\delta(O,K,a)\rhd c_{1}^{\prime}\;\sim_{\mathtt{C}}\;\delta(O,K,a)\rhd
c_{2}^{\prime\prime}(old(O,K,e_{a})[\nicefrac{{new(O,K,e_{a})}}{{e_{a}}}])$

and we can conclude that these P-markings are related by $R_{\delta(O,K,a)}$,
by its definition. ∎

######  Lemma .

Let
$\textstyle{O_{2}}$$\textstyle{O\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma_{2}}$$\scriptstyle{\sigma_{1}}$$\textstyle{O_{1}}$
be a span in $\mathbb{O}$ and let

$\textstyle{O\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma_{2}}$$\scriptstyle{\sigma_{1}}$$\textstyle{O_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p_{1}}$$\textstyle{O_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p_{2}}$$\textstyle{O_{3}\ignorespaces}$

be its pushout in $\mathbf{P}$. Then it is also a pushout in $\mathbf{O}$,
with

$l_{O_{3}}(x)=\begin{cases}l_{O_{1}}(y)&x=p_{1}(y)\\\
l_{O_{2}}(y)&x=p_{2}(y)\end{cases}$

###### Proof.

In [7, Lemma 8] we have proved that pushouts in $\mathbf{P}$ are computed as
in $\mathbf{Graph}$, plus transitive closure of the pushout object. We will
use this fact to prove our claim.

First of all, we check that $l_{O_{3}}$ is well-defined. We only have to
verify that its definition is correct for $x=p_{1}(y_{1})=p_{2}(y_{2})$. If
$p_{1}(y_{1})=p_{2}(y_{2})$ then $y_{1}$ and $y_{2}$ are images via
$\sigma_{1}$ and $\sigma_{2}$ of the same element of $O$, by definition of
pushout in $\mathbf{Graph}$. Since $\sigma_{1}$ and $\sigma_{2}$ preserve
labels, we must have $l_{O_{1}}(y_{1})=l_{O_{2}}(y_{2})$, so $l_{O_{3}}(x)$ is
well-defined on $x$.

Preservation of labels by $p_{1}$ and $p_{2}$ follows immediately from the
definition of $l_{O_{3}}$.

Now we prove that the square is indeed a pushout in $\mathbf{O}$. Consider the
following situation:

$\textstyle{O\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma_{2}}$$\scriptstyle{\sigma_{1}}$$\textstyle{O_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p_{1}}$$\scriptstyle{q_{1}}$$\textstyle{O_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q_{2}}$$\scriptstyle{p_{2}}$$\textstyle{O_{3}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{O_{4}}$

We have to check that, when $q_{1}$ and $q_{2}$ preserve labels, also the
unique mediating morphism $m$, as computed in $\mathbf{P}$, does. We prove it
by contradiction. Suppose $m$ does not preserve labels, then there exists
$x\in X_{O_{3}}$ such that $l_{O_{4}}(m(x))\neq l_{O_{3}}(x)$. Suppose $x$ is
image of $y\in X_{O_{1}}$ via $p_{1}$ (the case $y\in X_{O_{2}}$ and
$x=p_{2}(y)$ is analogous). Then we have

$\displaystyle l_{O_{1}}(y)$ $\displaystyle=l_{O_{3}}(x)$
$\displaystyle(\text{by $p_{1}$ preserving labels})$ $\displaystyle\neq
l_{O_{4}}(m(x))$ $\displaystyle(\text{by hypothesis})$
$\displaystyle=l_{O_{4}}(q_{1}(y))$ $\displaystyle(\text{by $q_{1}=m\circ
p_{1}$})$

which implies that $q_{1}$ does not preserve labels, a contradiction. ∎

###  A.2 Main proofs

###### Proof of section 3.2.

It is just a corollary of section A.1. ∎

###### Proof of section 3.2.

We prove (i), the other point is similar. Suppose

$O\rhd c\xRightarrow{K\vdash a}\delta(O,K,a)\rhd c^{\prime}.$

Then, by section 3.2, this transition can be derived from

$O\rhd c\xrightarrow{K\vdash{e}_{a}}\delta(O,K,e_{a})\rhd c^{\prime\prime}$

with
$c^{\prime}=c^{\prime\prime}old(O,K,e_{a})[\nicefrac{{new(O,K,e_{a})}}{{e_{a}}}]$,
for any $e\notin X_{O}$. Suppose $e\notin X_{O^{\prime}}$. By section A.1(i),
we have

$O^{\prime}\rhd
c\sigma\xrightarrow{\sigma(K)\vdash{e}_{a}}\delta(O^{\prime},\sigma(K),e_{a})\rhd{{(c^{\prime\prime}\sigma[\nicefrac{{e_{a}}}{{e_{a}}}])}\\!\\!\downarrow_{\delta(O^{\prime},\sigma(K),e_{a})}}$

from which, using section 3.2, we get

$O^{\prime}\rhd c\sigma\xRightarrow{\sigma(K)\vdash
a}\delta(O^{\prime},\sigma(K),a)\rhd{{(c^{\prime\prime}\sigma[\nicefrac{{e_{a}}}{{e_{a}}}])}\\!\\!\downarrow_{\delta(O^{\prime},\sigma(K),e_{a})}}\omega$

where
$\omega=old(O^{\prime},\sigma(K),e_{a})[\nicefrac{{new(O^{\prime},\sigma(K),e_{a})}}{{e_{a}}}]$.
We have to prove that the continuation of this transition has the required
form.

It is immediate to verify that, for any isomorphism $\sigma\colon O\to
O^{\prime}$ and causal marking $c$ such that $\mathscr{K}(c)\subseteq|O|$, we
have

${{(c\sigma)}\\!\\!\downarrow_{O^{\prime}}}={{c}\\!\\!\downarrow_{O}}\sigma$

which, for $\sigma=\omega$, implies

${{(c^{\prime\prime}\sigma[\nicefrac{{e_{a}}}{{e_{a}}}])}\\!\\!\downarrow_{\delta(O^{\prime},\sigma(K),e_{a})}}\omega={{(c^{\prime\prime}\sigma[\nicefrac{{e_{a}}}{{e_{a}}}]\omega)}\\!\\!\downarrow_{\delta(O^{\prime},\sigma(K),e_{a})}}\enspace.$
(2)

Now, observe that, by the definition of ${\sigma}^{\\!+}$ we have

$\sigma[\nicefrac{{e_{a}}}{{e_{a}}}]\omega=old(O,K,e_{a})[\nicefrac{{new(O,K,e_{a})}}{{e_{a}}}]{\sigma}^{\\!+}$

therefore (2) is equal to

${{(c^{\prime\prime}old(O,K,e_{a})[\nicefrac{{new(O,K,e_{a})}}{{e_{a}}}]{\sigma}^{\\!+})}\\!\\!\downarrow_{\delta(O^{\prime},\sigma(K),a)}}={{(c^{\prime}{\sigma}^{\\!+})}\\!\\!\downarrow_{\delta(O^{\prime},\sigma(K),a)}}$

as required. ∎

###### Proof of section 3.2.

Both implications can be proved by combining section A.1 and section A.1. ∎

###### Proof of section 3.3.

This is proved as [7, Theorem 2], where specific choices for abstract posets
and $old$ and $new$ maps are made in order to accommodate Darondeau-Degano
LTSs. The proof is exactly the same, where each specific operation is replaced
by its general version described in this paper. ∎

###### Proof of section 3.3.

Take $c\in\mathbin{[{n_{0}}\rangle}$. Then its tokens have been created by at
most $|c|$ transitions. Since we only take immediate causes, i.e., events
generated when those transitions were fired, each $O\RHD c$ is such that $|O|$
contains at most $|c|$ events. $O$ can be any poset on those events but, since
posets of minimal P-markings must be abstract, there are finitely-many such
posets. ∎

###### Proof of section 4.1.

  1. $(i)$

Immediately from the fact that any path from $\emptyset\rhd\emptyset\vdash
m_{0}$ to $O_{c}\rhd c$ builds $O_{c}$ and $c$ incrementally, adding one event
for each transition.

  2. $(ii)$

Suppose there are two parallel transitions from $O\rhd c$ to $O^{\prime}\rhd
c^{\prime}$, with labels $a$ and $b$. Then
$O^{\prime}=\delta(O,K,e_{a})=\delta(O,K^{\prime},e^{\prime}_{b})$, which can
only happen when $K=K^{\prime}$ and $e_{a}=e^{\prime}_{b}$, i.e., when the two
transitions coincide.

Suppose there is a directed cycle starting and ending at $O\rhd c$. Each
transition in the cycle would add a new event to $O$, so the final state would
be $O^{\prime}\rhd c$, with $O^{\prime}$ a strict superposet of $O$, a
contradiction.

∎

###### Proof of section 4.1.

  1. $(i)$

Consider a transition
$c_{1}\xrightarrow{a}_{\raisebox{4.52083pt}{\scriptsize${B_{\mathtt{C}}}$}}c_{1}^{\prime}$
and suppose the corresponding transition in CG${}_{\mathtt{C}}^{r}$ is

$O_{c_{1}}\rhd c_{1}\xrightarrow{K\vdash{e}_{a}}\delta(O_{c_{1}},K,e_{a})\rhd
c_{1}^{\prime}$

Now, observe that there is a trivial embedding of $O_{c_{1}}$ into $O$. In
fact, causes of $c_{1}$ are down-closed w.r.t. both posets, so $O_{c_{1}}$
must be a prefix of $O$. Then, using section A.1(i) and the embedding
$O_{c_{1}}\hookrightarrow O$ on the above transition, we get

$O\rhd
c_{1}\xrightarrow{K\vdash{e^{\prime}_{a}}}\delta(O,K,e^{\prime}_{a})\rhd
c^{\prime}_{1}[\nicefrac{{e^{\prime}_{a}}}{{e_{a}}}]$

for any $e^{\prime}\notin X_{O}$. By the hypothesis $O\rhd
c_{1}\sim_{\mathtt{C}}O\rhd c_{2}$, this transition can be simulated by

$O\rhd
c_{2}\xrightarrow{K\vdash{e^{\prime}_{a}}}\delta(O,K,e^{\prime}_{a})\rhd
c^{\prime}_{2}$

with $\delta(O,K,e^{\prime}_{a})\rhd
c^{\prime}_{1}[\nicefrac{{e^{\prime}_{a}}}{{e_{a}}}]\sim_{\mathtt{C}}\delta(O,K,e^{\prime}_{a})\rhd
c^{\prime}_{2}$. Using section A.1(ii) on the embedding of $O_{c_{2}}$ into
$O$, and noting that $e^{\prime}\notin X_{O_{c_{2}}}$, we recover a transition

$O_{c_{2}}\rhd
c_{2}\xrightarrow{K\vdash{e^{\prime}}_{a}}\delta(O_{c_{2}},K,e^{\prime}_{a})\rhd
c^{\prime}_{2}$

and from this, using the rule in section 4.1, we get
$c_{2}\xrightarrow{a}_{\raisebox{4.52083pt}{\scriptsize${B_{\mathtt{C}}}$}}c_{2}^{\prime}$.
In order to show that this transition simulates
$c_{1}\xrightarrow{a}_{\raisebox{4.52083pt}{\scriptsize${B_{\mathtt{C}}}$}}c_{1}^{\prime}$,
we have to find an isomorphism $\sigma^{\prime}\colon O_{c_{1}^{\prime}}\to
O_{c_{2}^{\prime}}$ such that the following diagram commutes

$\textstyle{O_{c_{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\phi^{\mathtt{C}}_{c_{1},c_{1}^{\prime}}}$$\scriptstyle{\sigma}$$\textstyle{O_{c_{1}^{\prime}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma^{\prime}}$$\textstyle{O_{c_{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\phi^{\mathtt{C}}_{c_{2},c_{2}^{\prime}}}$$\textstyle{O_{c_{2}^{\prime}}}$

We can define $\sigma^{\prime}(x)$ as $\sigma(x)$ if $x\in|O_{c_{1}}|$ and as
$e^{\prime}_{a}$ if $x=e_{a}$.

  2. $(ii)$

We want to prove that the following relation is an $\mathtt{AC}$-bisimulation

$R_{O_{c_{2}}}=\\{(O_{c_{2}}\rhd c_{1}\sigma,O\rhd c_{2})\mid
c_{1}\sim_{bs}^{\sigma}c_{2}\\}$

Suppose $c_{1}\sim_{bs}^{\sigma}c_{2}$ and

$O_{c_{2}}\rhd
c_{1}\sigma\xrightarrow{K\vdash{e}_{a}}\delta(O_{c_{2}},K,e_{a})\rhd
c_{1}^{\prime}.$ (3)

We have to find a simulating transition of $O_{c_{2}}\rhd c_{2}$. Applying
section 3.2 to the last transition, with isomorphism $\sigma^{-1}$, we get

$O_{c_{1}}\rhd
c_{1}\xrightarrow{\sigma^{-1}(K)\vdash{e^{\prime}_{a}}}\delta(O_{c_{1}},\sigma^{-1}(K),e^{\prime}_{a})\rhd
c_{1}^{\prime\prime}$

where
$c_{1}^{\prime\prime}=c_{1}^{\prime}\sigma^{-1}[\nicefrac{{e^{\prime}_{a}}}{{e_{a}}}]$,
for any $e^{\prime}\notin X_{O_{c_{1}}}$. This transition corresponds, via
section 4.1, to the following transition in $B_{\mathtt{C}}$

$c_{1}\xrightarrow{a}_{\raisebox{4.52083pt}{\scriptsize${B_{\mathtt{C}}}$}}c_{1}^{\prime\prime}$

which, by the hypothesis $c_{1}\sim_{bs}^{\sigma}c_{2}$, can be simulated by

$c_{2}\xrightarrow{a}_{\raisebox{4.52083pt}{\scriptsize${B_{\mathtt{C}}}$}}c_{2}^{\prime}$
(4)

with $c_{1}^{\prime}\sim_{bs}^{\sigma^{\prime}}c_{1}^{\prime\prime}$ such that

$\phi^{\mathtt{C}}_{c_{2},c_{2}^{\prime}}\circ\sigma=\sigma^{\prime}\
\circ\phi^{\mathtt{C}}_{c_{1},c_{1}^{\prime\prime}}$ (5)

Now, suppose for simplicity
$\\{e_{a}\\}=|O_{c^{\prime}_{2}}|\setminus|O_{c_{2}}|$ (the general case where
$|O_{c^{\prime}_{2}}|\setminus|O_{c_{2}}|$ contains any event fresh w.r.t.
$O_{c_{2}}$ requires minor changes). By definition of
$\phi^{\mathtt{C}}_{c_{2},c_{2}^{\prime}}$ and
$\phi^{\mathtt{C}}_{c_{1},c_{1}^{\prime\prime}}$, and by (5),
$\sigma^{\prime}$ should act as $\sigma$ on $O_{c_{1}}$, so
$\sigma^{\prime}=\sigma[\nicefrac{{e_{a}}}{{e^{\prime}_{a}}}]$. Moreover,
since $\sigma^{\prime}$ is an isomorphism, we have that the maximal causes of
$e^{\prime}_{a}$, namely $\sigma^{-1}(K)$, are mapped by $\sigma^{\prime}$ to
the maximal causes of $e^{\prime\prime}_{a}$, which then are
$\sigma^{\prime}(\sigma^{-1}(K))=\sigma(\sigma^{-1}(K))=K$, where the first
equation follows from $e^{\prime}_{a}\notin\sigma^{-1}(K)$. Therefore
$O_{c_{2}^{\prime}}=\delta(O_{c_{2}},K,e_{a})$ and (4) is derived, using
section 4.1, from

$O_{c_{2}}\rhd c_{2}\xrightarrow{K\vdash{e_{a}}}\delta(O_{c_{2}},K,e_{a})\rhd
c_{2}^{\prime}$

This transition is the required one simulating (3). In fact,
$c_{1}^{\prime\prime}\sim_{bs}^{\sigma^{\prime}}c_{2}^{\prime}$ implies

$(\delta(O_{c_{2}},K,e_{a})\rhd
c_{1}^{\prime\prime}\sigma^{\prime},\delta(O_{c_{2}},K,e_{a})\rhd
c_{2}^{\prime})\in R_{\delta(O_{c_{2}},K,e_{a})}$

by definition of $R$, and for the first P-marking we have
$c^{\prime\prime}_{1}\sigma^{\prime}=c_{1}^{\prime\prime}\sigma[\nicefrac{{e_{a}}}{{e^{\prime}_{a}}}]=(c_{1}^{\prime}\sigma^{-1}[\nicefrac{{e^{\prime}_{a}}}{{e_{a}}}])\sigma[\nicefrac{{e^{\prime}_{a}}}{{e_{a}}}]=c_{1}^{\prime}$,
which is the causal marking in the continuation of (3).

∎

###### Proof of section 6.

Smallness follows from skeletality. In [7] we have proved that pullbacks in
${\mathbf{P}_{m}}$ are computed as the category $\mathbf{Graph}$ of graphs and
their homomorphisms. It can be easily verified that, given a cospan
$\textstyle{O_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{O_{3}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
O_{2}}$$\scriptstyle{g}$ in $\mathbb{O}$, we can forget labels and compute the
pullback as in $\mathbf{Graph}$. In fact, the pullback poset $O$ has an
element $y$ for each pair of elements $x_{1}\in X_{O_{1}}$ and $x_{2}\in
X_{O_{2}}$ such that $f(x_{1})=g(x_{2})$. But then, since $f$ and $g$ preserve
labels, we must have $l_{O_{1}}(x_{1})=l_{O_{2}}(x_{2})=a$, so $l_{O}(y)=a$
and the pullback maps preserve labels. It is easy to check that pullback
mediating morphisms preserve labels, as they must commute with morphisms with
such property. ∎

###### Proof of section 6.

In ([7, Lemma 8]) we have proved that pushouts of order-embeddings in
$\mathbf{P}$ are commuting squares in ${\mathbf{P}_{m}}$. Therefore we can
compute the two pushouts of (1) in $\mathbf{P}$, take the corresponding
commuting squares in ${\mathbf{P}_{m}}$ and then use Lemma  to get labeling
functions for their bottom-right corners. Diagrams in ${\mathbf{P}_{m}}$ made
of label preserving functions are also diagrams in $\mathbb{O}$.

Finally, the fact that ${\sigma}^{\\!+}$ reflects orders follows from its
definition. ∎

###### Proof of section 6.

$B$ is obtained by composition and product of accessible functors:
$\mathscr{P}_{f}$ is known to be accessible; $\mathcal{L}$ is accessible,
because it can be regarded as a constant endofunctor on
$\mathbf{Set}^{\mathbb{O}}$; $\Delta$ is accessible, because it has a right
adjoint, namely the functor computing right Kan extensions along $\delta$.

In order to show that $B$ covers pullbacks, we will show that it has the form
$\mathscr{P}_{f}\circ B^{\prime}$, with $B^{\prime}$ a pullback preserving
endofunctor on $\mathbf{Set}^{\mathbb{O}}$. The thesis will follow from
$\mathscr{P}_{f}$ covering pullbacks (see [25]). $\Delta$ has a left adjoint,
namely the functor computing left Kan extensions along $\delta$, then it
preserves pullbacks; $\mathcal{L}$ can be seen as a constant, hence pullback-
preserving, endofunctor on $\mathbf{Set}^{\mathbb{O}}$. $B^{\prime}$ is the
product of these two functors, so it preserves pullbacks. ∎

###### Proof of section 6.

Requirement section 6ii corresponds to the fact that a $B$-bisimulation $R$ on
$(P,\rho)$ is a functor and its projections are natural transformations, so we
have $(p,q)[\sigma]_{R}=(p[\sigma]_{P},q[\sigma]_{P})$, for any morphism
$\sigma$ in $\mathbb{O}$. Requirement i corresponds to the fact that $RO$ is
“almost” an ordinary bisimulation, because computing $\overline{B}R(O)$
essentially amounts to computing $\overline{B_{flts}}(RO)$ (see section 5.2)
for each $O\in|\mathbb{O}|$, as images in $\mathbf{Set}^{\mathbb{O}}$ are
computed pointwise in $\mathbf{Set}$, with the difference that continuations
are not in $RO$, but in $R(\delta O)$.∎∎

###### Proof of section 6.

We have to prove that if the square on the left is a pullback then so is the
outer square on the right.

$\textstyle{O\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p_{1}}$$\scriptstyle{p_{2}}$$\textstyle{O_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma_{1}}$$\textstyle{O_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma_{2}}$$\textstyle{O_{3}}$
---
$\textstyle{\mathscr{M}(O)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu}$$\scriptstyle{[p_{1}]}$$\scriptstyle{[p_{2}]}$$\textstyle{\mathscr{M}(O_{1})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{[\sigma_{1}]}$$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{2}}$$\scriptstyle{\pi_{1}}$$\textstyle{\mathscr{M}(O_{2})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{[\sigma_{2}]}$$\textstyle{\mathscr{M}(O_{3})}$

In the right diagram, let $P$ be the pullback in $\mathbf{Set}$ of
$[\sigma_{1}]$ and $[\sigma_{2}]$, namely

$P=\\{(c_{1},c_{2})\mid c_{1}[\sigma_{1}]=c_{2}[\sigma_{2}]\\}$

We will show that that the mediating morphism $\mu$ is an isomorphism, which
implies that $\mathscr{M}(O)$ is a pullback object.

Take $(c_{1},c_{2})\in P$ and $c=c_{1}[\sigma_{1}]=c_{2}[\sigma_{2}]$. Then
these causal markings must be of the form

$c_{1}=\\{K_{1}\vdash s_{1},\dots,K_{n}\vdash s_{n}\\}\qquad
c_{2}=\\{H_{1}\vdash s_{1},\dots,H_{n}\vdash s_{n}\\}\qquad c=\\{L_{1}\vdash
s_{1},\dots,L_{n}\vdash s_{n}\\}$

because $[\sigma_{1}]$ and $[\sigma_{2}]$ do not affect tokens. Moreover, we
must have

$L_{i}={{\sigma_{1}(K_{i})}\\!\\!\downarrow_{O_{1}}}={{\sigma_{2}(H_{i})}\\!\\!\downarrow_{O_{2}}}\qquad(i=1,\dots,n)$

by definition of the action of $\mathscr{M}$ on morphisms, and in particular

$\max_{O_{1}}\sigma_{1}(K_{i})=\max_{O_{2}}\sigma_{2}(H_{i})=max_{O_{3}}L_{i}$

because $K_{i},H_{i}$ and $L_{i}$ are down-closed sets, so they coincide with
the closure of their maxima. It is easy to check that order-preserving and
reflecting morphisms preserve maxima, so we have

$\sigma_{1}(max_{O_{1}}K_{i})=\max_{O_{3}}\sigma_{1}(K_{i})=\max_{O_{2}}\sigma_{2}(H_{i})=\sigma_{2}(max_{O_{2}}H_{i}).$

Therefore, by definition of pullback in $\mathbb{O}$ (computed as in
$\mathbf{Graph}$), there are $J_{i}\subseteq|O|$ such that

$p_{1}(J_{i})=\max_{O_{1}}K_{i}\qquad p_{2}(J_{i})=\max_{O_{2}}H_{i}$ (6)

and we can define the following causal marking in $\mathscr{M}(O)$

$c^{\prime}=\\{\hat{J}_{1}\vdash s_{1},\dots,\hat{J}_{n}\vdash s_{n}\\}$

where $\hat{J}_{i}={{J_{i}}\\!\\!\downarrow_{O}}$.

Now, observe that $c^{\prime}[p_{1}]=c_{1}$ and $c^{\prime}[p_{2}]=c_{2}$,
because (6) implies ${{p_{1}(\hat{J}_{i})}\\!\\!\downarrow_{O_{1}}}=K_{i}$ and
${{p_{2}(\hat{J}_{i})}\\!\\!\downarrow_{O_{2}}}=H_{i}$. Therefore letting
$\mu(c^{\prime})=(c_{1},c_{2})$ makes the whole right diagram commute. So far
we have proved that $\mu$ is surjective. For injectivity, suppose there is
another $c^{\prime\prime}\in\mathscr{M}(O)$ such that
$\mu(c^{\prime\prime})=(c_{1},c_{2})$. Since $c^{\prime\prime}[p_{1}]=c_{1}$
and $c^{\prime\prime}[p_{2}]=c_{2}$, $c^{\prime\prime}$ is again of the form
$\\{M_{1}\vdash s_{1},\dots,M_{n}\vdash s_{n}\\}$, with
${{p_{1}(M_{i})}\\!\\!\downarrow_{O_{1}}}=K_{i}$. Since also
$K_{i}={{p_{1}(\hat{J}_{i})}\\!\\!\downarrow_{O_{1}}}$, $M_{i}$ and
$\hat{J}_{i}$ must have the same set $X$ of maxima. But then we have
$M_{i}={{X}\\!\\!\downarrow_{O}}=\hat{J}_{i}$, so
$c^{\prime\prime}=c^{\prime}$.

∎

###### Proof of section 6.

The first item is just an instance of section 6.

For the second item, we shall show that $R$ is an $\mathtt{AC}$-bisimulation
closed under order-embeddings if and only if it is a $\mathbb{O}$-indexed
bisimulation:

  * $\implies$:

take $(O\rhd c,O\rhd\tilde{c})\in R_{O}$ and suppose

$O\rhd c\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
1.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\hbox{\kern
0.0pt\raise 1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
2.78813pt\raise 5.43056pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\hbox{$\scriptstyle{K\vdash a}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 21.1111pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise 0.00002pt\hbox{\hbox{\kern
3.8889pt\hbox{{\hbox{\kern-3.8889pt\hbox{\ignorespaces\hbox{\kern
0.0pt\raise-2.57344pt\hbox{$\textstyle{\RHD}$}}}}}}}}}}}}{\hbox{\hbox{\kern
0.0pt\raise 1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}{\hbox{\hbox{\kern 0.0pt\raise
1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}{\hbox{\kern 25.0pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\boldsymbol{\delta}(O)\rhd
c^{\prime}.$ (7)

Then, by section 6, there is

$O\rhd c\xRightarrow{K\vdash a}\delta(O,K,a)\rhd c^{\prime\prime}$

such that $c^{\prime}=c^{\prime\prime}[\epsilon(O,K,a)]$. Since $R$ is an
$\mathtt{AC}$-bisimulation, there is

$O\rhd\tilde{c}\xRightarrow{K\vdash a}\delta(O,K,a)\rhd\tilde{c}^{\prime}$

such that $(\delta(O,K,a)\rhd
c^{\prime\prime},\delta(O,K,a)\rhd\tilde{c}^{\prime})\in R_{\delta(O,K,a)}$.
Again by section 6, from the last transition we get

$O\rhd\tilde{c}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
1.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\hbox{\kern
0.0pt\raise 1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
2.78813pt\raise 5.43056pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\hbox{$\scriptstyle{K\vdash a}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 21.1111pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise 0.00002pt\hbox{\hbox{\kern
3.8889pt\hbox{{\hbox{\kern-3.8889pt\hbox{\ignorespaces\hbox{\kern
0.0pt\raise-2.57344pt\hbox{$\textstyle{\RHD}$}}}}}}}}}}}}{\hbox{\hbox{\kern
0.0pt\raise 1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}{\hbox{\hbox{\kern 0.0pt\raise
1.0pt\hbox{\lx@xy@droprule}}\hbox{\kern
0.0pt\raise-1.0pt\hbox{\lx@xy@droprule}}}}{\hbox{\kern 25.0pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\boldsymbol{\delta}(O)\rhd\tilde{c}^{\prime}[\epsilon(O,K,a)].$

This is a simulating transition for (7), because $(\delta(O,K,a)\rhd
c^{\prime\prime},\delta(O,K,a)\rhd\tilde{c}^{\prime})\in R_{\delta(O,K,a)}$
implies $(\boldsymbol{\delta}(O)\rhd
c^{\prime},\boldsymbol{\delta}(O)\rhd\tilde{c}^{\prime}[\epsilon(O,K,a)])\in
R_{\boldsymbol{\delta}(O)}$, by closure of $R$ under order-embeddings.

  * $\impliedby$:

analogous to the previous point. Closure under order-embeddings of $R$ follows
from section 6ii.

∎

###### Proof of section 7.

Analogous to the proof of [7, Proposition 8]. ∎