# Towards a Semantic Characterisation
of Global Type Well-formedness

Ilaria Castellani111This research has been supported by the ANR17-CE25-0014-01
CISC project. INRIA, Université Côte d’Azur, France<EMAIL_ADDRESS>DiSSTE, Università del Piemonte Orientale, Italy Paola Giannini222This work
was partially funded by the MUR project “T-LADIES” (PRIN 2020TL3X8X) and has
the financial support of the Università del Piemonte Orientale. DiSSTE,
Università del Piemonte Orientale, Italy<EMAIL_ADDRESS>
###### Abstract

We address the question of characterising the well-formedness properties of
multiparty session types semantically, i.e., as properties of the semantic
model used to interpret types. Choosing Prime Event Structures (PESs) as our
semantic model, we present semantic counterparts for the two properties that
underpin global type well-formedness, namely projectability and boundedness,
in this model. As a first step towards a characterisation of the class of PESs
corresponding to well-formed global types, we identify some simple structural
properties satisfied by such PESs.

##  1 Introduction

This paper builds on our previous work [5], where we investigated the use of
Event Structures (ESs) as a denotational model for multiparty session types
(MPSTs). That paper presented an ES semantics for both sessions and global
types, using respectively Flow Event Structures (FESs) and Prime Event
Structures (PESs), and showed that if a session is typable with a given global
type, then the FES associated with the session and the PES associated with the
global type yield isomorphic domains of configurations.

The ES semantics proposed in [5] abstracts away from the syntax of global
types, by making explicit the concurrency relation between independent
communications. This abstraction is expected since ESs are a “true
concurrency” model, where concurrency is treated as a primitive notion.
However, [5] focussed on the equivalence between the FES of a session and the
PES of its global type, without drawing all the consequences of its results
and demonstrating the full benefits of the ES semantics for MPSTs.

In the present paper, we move one step further by studying how the well-
formedness property of global types considered in [5] is reflected in their
interpretation as Prime Event Structures (PESs). In [5], global type well-
formedness is the conjunction of a _projectability_ condition and a
_boundedness_ condition. Having semantic counterparts for these conditions
will enable us to reason directly on PESs, taking advantage of their faithful
account of concurrency and of their graphical representation.

We prove that: 1) all global types that type the same network yield identical
PESs, 2) our proposed properties of _semantic projectability_ and _semantic
boundedness_ for PESs reflect the corresponding properties of global types,
and 3) PESs obtained from global types enjoy some simple structural
properties.

The rest of the paper is organised as follows. In Section 2 and Section 3 we
recall the necessary background from [5] and present the result 1) above. In
Section 4 we define our semantic notions of projectability and boundedness and
prove the result 2) above. Section 5 is devoted to the result 3). Finally, in
Section 6 we discuss related work and sketch some directions for future work.

In the paper, all theorems are given with proofs while all lemmas are stated
without proofs.

##  2 Networks and Global Types

To set up the stage for our study, we recall the definitions of sessions and
global types from [5]. In the core multiparty session calculus of [5],
sessions are described as networks of sequential processes, and processes
coincide with local types. Session _participants_ are denoted by ${\sf p},{\sf
q},{\sf r}$, and _messages_ by $\lambda,\lambda^{\prime}$.

######  Definition 2.1 (Processes and networks)

  * •

Processes are defined by: $P::=^{coind}\bigoplus_{i\in I}{\sf
p}!\lambda_{i};P_{i}~{}~{}\mid~{}~{}{\Sigma}_{i\in I}{\sf
p}?\lambda_{i};P_{i}~{}~{}\mid~{}~{}\mathbf{0}$
where $I$ is a finite non-empty index set and
$\lambda_{\\_}h\not=\lambda_{\\_}k\,$ for $h\neq k$.

  * •

Networks are defined by: ${\sf N}={\sf
p}_{\\_}1[\\![\,P\,]\\!]\mathrel{\|}\dots\mathrel{\|}{\sf
p}_{\\_}n[\\![\,P\,]\\!]$ with $n\geq 1$ and ${\sf p}_{\\_}h\not={\sf
p}_{\\_}k\,$ for $h\neq k$.

The symbol $::=^{coind}$ in the definition of processes indicates that the
definition is coinductive. This allows infinite processes to be defined
without using an explicit recursion operator. However, in order to achieve
decidability we focus on regular processes, namely those with a finite number
of distinct subprocesses. In writing processes, we will omit trailing
$\mathbf{0}$’s and when $\\!\\!~{}|~{}\\!I\\!~{}|~{}\\!=1$ we will omit the
choice symbol.

A network is a parallel composition of processes, each located at a different
participant. The LTS semantics of networks is specified by the unique rule:

$\begin{array}[]{c}{\sf p}[\\![\,\bigoplus_{i\in I}{\sf
q}!\lambda_{i};P_{i}\,]\\!]\mathrel{\|}{\sf q}[\\![\,{\Sigma}_{j\in J}{\sf
p}?\lambda_{j};Q_{j}\,]\\!]\mathrel{\|}{\sf N}\xrightarrow{{\sf p}{\sf
q}\lambda_{\\_}k}{\sf p}[\\![\,P_{\\_}k\,]\\!]\mathrel{\|}{\sf
q}[\\![\,Q_{\\_}k\,]\\!]\mathrel{\|}{\sf N}~{}~{}~{}\text{where }k\in
I{\cap}J{~{}~{}~{}~{}~{}~{}{[\textsc{Comm}]}}\end{array}$

######  Definition 2.2 (Global types)

Global types ${\sf G}$ are defined by: ${\sf G}::=^{coind}{\sf p}\to{\sf
q}:\\{\lambda_{i};{\sf G}_{i}\\}_{i\in I}~{}\mid~{}\mathsf{End}$
where $I$ is finite non-empty index set and
$\lambda_{\\_}h\not=\lambda_{\\_}k\,$ for $h\neq k$.

Here again, $::=^{coind}$ indicates that the definition is coinductive, and we
focus on _regular_ global types. We will omit trailing $\mathsf{End}$’s and
when $\\!\\!~{}|~{}\\!I\\!~{}|~{}\\!=1$ we will write a global type ${\sf
p}\to{\sf q}:\\{\lambda;{\sf G}\\}$ simply as ${\sf
p}\stackrel{{\scriptstyle\lambda}}{{\to}}{\sf q};{\sf G}$.

A _communication_ ${\sf p}{\sf q}\lambda$ represents the transmission of label
$\lambda$ on the channel ${\sf p}{\sf q}$ from ${\sf p}$ to ${\sf q}$.
Communications are ranged over by $\alpha,\beta$. The following notion of
trace will be extensively used in the sequel.

######  Definition 2.3 (Traces)

A _trace_ $\sigma,\tau$ is a finite sequence of communications, i.e.
$\sigma::=\epsilon\mid\alpha\,{\cdot}\,\sigma$.
The set of traces is denoted by Traces.

It is useful to define sets of participants also for communications and
traces. We define ${\sf part}({\sf p}{\sf q}\lambda)=\\{{\sf p},{\sf q}\\}$,
and we lift this definition to traces by letting ${\sf
part}(\epsilon)=\emptyset$ and ${\sf part}(\alpha\,{\cdot}\,\sigma)={\sf
part}(\alpha)\cup{\sf part}(\sigma)$.

As observed in [5], global types may be viewed as trees whose internal nodes
are decorated by channels ${\sf p}{\sf q}$, leaves by $\mathsf{End}$, and
edges by labels $\lambda$. Given a global type, the sequences of decorations
of nodes and edges on the path from the root to an edge in the tree of the
global type are traces. We denote by ${\sf Tr^{+}}({\sf G})$ the set of traces
of ${\sf G}$. By definition, ${\sf Tr^{+}}(\mathsf{End})=\emptyset$ and each
trace in ${\sf Tr^{+}}({\sf G})$ is non-empty.

The set of participants of a global type ${{\sf G}}$, ${\sf part}({{\sf G}})$,
is the union of the sets of participants of its traces, i.e. ${\sf part}({{\sf
G}})=\bigcup_{\\_}{\sigma\in{\sf Tr^{+}}({\sf G})}{\sf part}(\sigma)$. The
regularity assumption ensures that ${\sf part}({{\sf G}})$ is finite for any
${{\sf G}}$.

The semantics of global types is given by the standard LTS presented in Figure
1, where transitions are labelled by communications.

$\begin{array}[]{c}{\sf p}\to{\sf q}:\\{\lambda_{i};{\sf G}_{i}\\}_{i\in
I}\xrightarrow{{\sf p}{\sf q}\lambda_{\\_}j}{\sf
G}_{\\_}j~{}~{}~{}~{}~{}~{}j\in
I{~{}~{}~{}{[\textsc{Ecomm}]}}\quad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty 1{\sf
G}_{\\_}i\xrightarrow{\alpha}{\sf G}_{\\_}i^{\prime}\quad\text{ for all }i\in
I\quad{\sf part}(\alpha)\cap\\{{\sf p},{\sf q}\\}=\emptyset$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=197.88892pt\hbox{\kern
3.00003pt$~{}~{}~{}{[\textsc{Icomm}]}$}}}\hbox{\kern
35.94876pt\hbox{$\displaystyle{\sf p}\to{\sf q}:\\{\lambda_{i};{\sf
G}_{i}\\}_{i\in I}\xrightarrow{\alpha}{\sf p}\to{\sf q}:\\{\lambda_{i};{\sf
G}^{\prime}_{i}\\}_{i\in I}$}}}}\\\ \\\ \end{array}$

Figure 1:  LTS for global types.

$\begin{array}[]{c}\\\\[-1.0pt] {\sf G}\\!\upharpoonright\\!{\sf
r}\,=\mathbf{0}\text{ if }{\sf r}\not\in{\sf part}({\sf G})\qquad({\sf
p}\to{\sf q}:\\{\lambda_{i};{\sf G}_{i}\\}_{i\in I})\\!\upharpoonright\\!{\sf
r}\,=\begin{cases}{\Sigma}_{i\in I}{\sf p}?\lambda_{i};{\sf
G}_{\\_}i\\!\upharpoonright\\!{\sf r}\,&\text{if }{\sf r}={\sf q},\\\
\bigoplus_{i\in I}{\sf q}!\lambda_{i};{\sf G}_{\\_}i\\!\upharpoonright\\!{\sf
r}\,&\text{if }{\sf r}={\sf p},\\\ {\sf G}_{\\_}1\\!\upharpoonright\\!{\sf
r}\,&\text{if }{\sf r}\not\in\\{{\sf p},{\sf q}\\}\text{ and }{\sf r}\in{\sf
part}({\sf G}_{\\_}1)\\\ &\text{ and }{\sf G}_{\\_}i\\!\upharpoonright\\!{\sf
r}\,={\sf G}_{\\_}1\\!\upharpoonright\\!{\sf r}\,\text{ for all }i\in
I\end{cases}\\\\[13.0pt] \end{array}$

Figure 2: Projection of global types onto participants.

The projection of a global type onto participants is given in Figure 2. As
usual, projection is defined only when it is defined on all participants. Due
to the simplicity of our calculus, the projection of a global type, when
defined, is simply a process. The definition is the standard one from [10,
11]: the projection of a choice type on the sender or the receiver yields an
output choice or an input choice, while its projection on a third participant
is its projection on the continuation of the branch, which must be equal on
all branches. Our coinductive definition is more permissive than the standard
one for infinite types (see [5]).

A global type ${\sf G}$ is _projectable_ if ${{\sf
G}}\\!\upharpoonright\\!{\sf p}\,$ is defined for all ${\sf p}$.

The following property of boundedness for global types is used to ensure
progress.

######  Definition 2.4 (Depth and boundedness)

The two functions $\delta({\sf p},\sigma)$ and $\delta({\sf p},{\sf G})$ are
defined by:

$\begin{array}[]{l}\delta({\sf
p},\sigma)=\begin{cases}\\!\\!~{}|~{}\\!\sigma_{\\_}1\cdot\alpha\\!~{}|~{}\\!&\text{
if }\sigma=\sigma_{\\_}1\,{\cdot}\,\alpha\,{\cdot}\,\sigma_{\\_}2\text{ and
}{\sf p}\notin{\sf part}(\sigma_{\\_}1)\text{ and }{\sf p}\in{\sf
part}(\alpha)\\\ 0&\text{otherwise }\end{cases}\\\ \delta({\sf p},{\sf
G})=\sup(\\{\delta({\sf p},\sigma)\ |\ \sigma\in{\sf Tr^{+}}({\sf
G})\\})\end{array}$

A global type ${{\sf G}}$ is bounded if $\delta({\sf p},{\sf G}^{\prime})$ is
finite for each participant ${\sf p}$ and each subtree ${\sf G}^{\prime}$ of
${{\sf G}}$.

If $\delta({\sf p},{\sf G})$ is finite, then there is no path in the tree of
${\sf G}$ in which ${\sf p}$ is delayed indefinitely. Note that if
$\delta({\sf p},{\sf G})$ is finite, ${\sf G}$ may have subtrees ${\sf
G}^{\prime}$ for which $\delta({\sf p},{\sf G}^{\prime})$ is infinite.

######  Definition 2.5 (Well-formed global types)

A global type ${{\sf G}}$ is well formed if it is projectable and bounded.

We conclude this section by recalling the type system for networks. The unique
typing rule for networks is Rule [Net] in Figure 3. It relies on a preorder on
processes, $P\leq Q$, meaning that process $P$ can be used where we expect
process $Q$. This preorder plays the same role as the standard subtyping for
local types, except that it is invariant for output processes (rather than
covariant). This restriction is imposed in [5] in order to obtain bisimilar
LTSs for networks and their global types, a property which in turn is used to
prove our main result there (isomorphism of the configuration domains of the
two ESs). The preorder rules are interpreted coinductively, since processes
may have infinite (regular) trees.

A network is well typed if all its participants behave as specified by the
projections of the same global type ${\sf G}$. Rule [Net] is standard for
MPSTs, so we do not discuss it further.

$\begin{array}[]{c}\mathbf{0}\leq\mathbf{0}~{}{[\textsc{ $\leq$
-$\mathbf{0}$}]}\quad\mprset{fraction={===},fractionaboveskip=0.2ex,fractionbelowskip=1.30ex}\inferrule[]{P_{\\_}i\leq
Q_{\\_}i~{}~{}~{}~{}~{}i\in I}{~{}{\Sigma}_{i\in I\cup J}{\sf
p}?\lambda_{i};P_{i}\leq{\Sigma}_{i\in I}{\sf p}?\lambda_{i};Q_{i}}{{[\textsc{
$\leq$-In}]}}\quad\mprset{fraction={===},fractionaboveskip=0.2ex,fractionbelowskip=1.30ex}\inferrule[]{P_{\\_}i\leq
Q_{\\_}i~{}~{}~{}~{}~{}i\in I}{~{}\textstyle{\bigoplus}_{i\in I}{\sf
p}!\lambda_{i};P_{i}\leq\bigoplus_{i\in I}{\sf
p}!\lambda_{i};Q_{i}}{{[\textsc{ $\leq$-Out}]}}\\\ \\\
\inferrule{P_{\\_}i\leq{{\sf G}}\\!\upharpoonright\\!{\sf
p}_{\\_}i\,~{}~{}~{}~{}~{}i\in I~{}~{}~{}~{}~{}~{}{\sf part}({{\sf
G}})\subseteq\\{{\sf p}_{\\_}i\mid i\in I\\}}{\vdash{\Pi}_{\\_}{i\in I}{\sf
p}_{\\_}i[\\![\,P_{\\_}i\,]\\!]:{{\sf G}}}~{}{[\textsc{Net}]}\\\\[13.0pt]
\end{array}$

Figure 3: Preorder on processes and network typing rule.

##  3 Event Structure Semantics of Global Types

In this section we present the interpretation of global types as Prime Event
Structures, as proposed in our previous work [5]. We start by recalling the
definition of _Prime Event Structure_ (PES) and configuration from [13]. All
the following definitions (from Definition 3.3 to Definition 3.10) are
required background taken from [5], with some minor variations. The new
material starts immediately after Definition 3.10.

######  Definition 3.1 ( [13] Prime Event Structure)

A prime event structure (PES) is a tuple $S=(E,\leq,~{}\\#~{})$ where $E$ is a
denumerable set of events; $\leq\,\,\subseteq(E\times E)$ is a partial order
relation, called the _causality_ relation; $~{}\\#~{}\subseteq(E\times E)$ is
an irreflexive symmetric relation, called the _conflict_ relation, satisfying
the property of _conflict hereditariness_ : $\forall
e,e^{\prime},e^{\prime\prime}\in E:e\,\\#\,e^{\prime}\leq
e^{\prime\prime}\Rightarrow e\,\\#\,e^{\prime\prime}$.

A PES configuration is a set of events that may have occurred at some stage of
computation.

######  Definition 3.2 ( [13] PES configuration)

Let $S=(E,\leq,~{}\\#~{})$ be a prime event structure. A configuration of $S$
is a finite subset $\mathcal{X}$ of $E$ which is (1) downward-closed:
$e^{\prime}\leq e\in\mathcal{X}\,\ \Rightarrow\ \ e^{\prime}\in\mathcal{X}$;
and (2) conflict-free: $\forall
e,e^{\prime}\in\mathcal{X},\neg(e~{}\\#~{}e^{\prime})$.

The semantics of a PES $S$ is given by its poset of configurations ordered by
set inclusion, where $\mathcal{X}_{\\_}1\subset\mathcal{X}_{\\_}2$ means that
$S$ may evolve from $\mathcal{X}_{\\_}1$ to $\mathcal{X}_{\\_}2$.

The events of the PES associated with a global type will be equivalence
classes of particular traces. We introduce some notations for traces $\sigma$.
We denote by $\and{\sigma}{i}$ the $i$-th element of $\sigma$. If $i\leq j$,
we define $\sigma[i\,...\,j]=\and{\sigma}{i}\cdots\and{\sigma}{j}$ to be the
subtrace of $\sigma$ consisting of the $(j-i+1)$ elements starting from the
$i$-th one and ending with the $j$-th one. If $i>j$, we convene that
$\sigma[i\,...\,j]$ denotes the empty trace $\epsilon$.

A permutation equivalence on Traces is used to swap communications with
disjoint participants.

######  Definition 3.3 (Permutation equivalence)

The permutation equivalence on Traces is the least equivalence $\sim$ such
that

$\sigma\,{\cdot}\,\alpha\,{\cdot}\,\alpha^{\prime}\,{\cdot}\,\sigma^{\prime}\,\sim\,\,\sigma\,{\cdot}\,\alpha^{\prime}\,{\cdot}\,\alpha\,{\cdot}\,\sigma^{\prime}\quad\text{if}\quad{\sf
part}(\alpha)\cap{\sf part}(\alpha^{\prime})=\emptyset$

We denote by $[\sigma]_{\sim}$ the equivalence class of $\sigma$, and by
$\textit{Traces}/\\!\\!\sim$ the set of equivalence classes on Traces.

The events of the PES associated with a global type are equivalence classes of
particular traces that we call _pointed_. Intuitively, a pointed trace “points
to” its last communication, in that all the preceding communications in the
trace should cause some subsequent communication in the trace. Formally:

######  Definition 3.4 (Pointed trace)

A non empty trace $\sigma=\sigma[1\,...\,n]$ is said to be _pointed_ if

$~{}~{}\forall i\,.1\leq i<n,~{}\exists j\,.\,i<j\leq n\,.~{}~{}{\sf
part}(\and{\sigma}i)\cap{\sf part}(\and{\sigma}j)\not=\emptyset$

Note that the condition of Definition 3.4 is vacuously satisfied by any trace
of length $n=1$, since in that case there is no $i$ such that $1\leq i<n$.

Let us also point out that Definition 3.4 is slightly different from (but
equivalent to) the definition of pointed trace given in [5].

For example, let $\alpha_{\\_}1={\sf p}{\sf
q}\lambda_{\\_}1,\,\alpha_{\\_}2={\sf r}{\sf s}\lambda_{\\_}2$ and
$\alpha_{\\_}3={\sf r}{\sf p}\lambda_{\\_}3$. Then
$\sigma_{\\_}1=\alpha_{\\_}1$ and
$\sigma_{\\_}3=\alpha_{\\_}1\,{\cdot}\,\alpha_{\\_}2\,{\cdot}\,\alpha_{\\_}3\,$
are pointed traces, while
$\sigma_{\\_}2=\alpha_{\\_}1\,{\cdot}\,\alpha_{\\_}2\,$ is not a pointed
trace.

If $\sigma$ is non empty, we use ${\sf last}(\sigma)$ to denote the last
communication of $\sigma$. It is easy to prove that, if $\sigma$ is a pointed
trace and $\sigma\sim\sigma^{\prime}$, then $\sigma^{\prime}$ is a pointed
trace and ${\sf last}(\sigma)={\sf last}(\sigma^{\prime})$.

######  Definition 3.5 (Global event)

Let $\sigma=\sigma^{\prime}\,{\cdot}\,\alpha\,$ be a pointed trace. Then
$\gamma=[\sigma]_{\sim}$ is a _global event_ , also called _g-event_ , with
communication $\alpha$, notation ${\sf cm}(\gamma)=\alpha$.

Notice that, due to the observation above, ${\sf cm}(\gamma)$ is well defined.
We denote by $\mathcal{G\\!E}$ the set of g-events.

We now introduce an operator that adds a communication $\alpha$ in front of a
g-event $\gamma$, provided $\alpha$ is a cause of some communication in the
trace of $\gamma$. This ensures that the operator always transforms a g-event
into another g-event. We call this operator _causal prefixing of a g-event by
a communication_.

######  Definition 3.6 (Causal prefixing of a g-event by a communication)

  1. 1.

The causal prefixing of a g-event $\gamma\,$ by a communication $\alpha$ is
defined by:

$\alpha\circ\gamma=\begin{cases}[\alpha\,{\cdot}\,\sigma]_{\sim}&\text{if~{}
$\gamma=[\sigma]_{\sim}$~{} and~{} ${\sf part}(\alpha)\cap{\sf
part}(\sigma)\neq\emptyset$}\\\ \gamma&\text{otherwise}\end{cases}$

  2. 2.

The operator $\circ$ naturally extends to traces by:
$\epsilon\circ\gamma=\gamma\quad(\alpha\,{\cdot}\,\sigma)\circ\gamma=\alpha\circ(\sigma\circ\gamma)$

An easy consequence of Clause 2 is that
$(\sigma^{\prime}\,{\cdot}\,\sigma)\circ\gamma=\sigma^{\prime}\circ(\sigma\circ\gamma)$
for all $\sigma$ and $\sigma^{\prime}$.

Using causal prefixing, we can define the mapping ${\sf ev}(\cdot)$ which,
applied to a trace $\sigma$, yields the g-event representing the communication
${\sf last}(\sigma)$ prefixed by its causes occurring in $\sigma$.

###### Definition 3.7

The g-event generated by a non-empty trace  is defined by: ${\sf
ev}(\sigma\,{\cdot}\,\alpha)=\sigma\circ[\alpha]_{\sim}$

Clearly, ${\sf ev}(\sigma)$ is a subtrace of $\sigma$ and ${\sf cm}({\sf
ev}(\sigma))={\sf last}(\sigma)$. Observe that the function ${\sf ev}(\cdot)$
is not injective on the set of traces of a global type. For example, let ${\sf
G}={\sf p}\to{\sf q}:\\{\lambda_{\\_}1;{\sf
r}\stackrel{{\scriptstyle\lambda}}{{\to}}{\sf s}\,,\,\lambda_{\\_}2;{\sf
r}\stackrel{{\scriptstyle\lambda}}{{\to}}{\sf s}\\}$. Let $\sigma_{\\_}1={\sf
p}{\sf q}\lambda_{\\_}1\cdot{\sf r}{\sf s}\lambda$ and $\sigma_{\\_}2={\sf
p}{\sf q}\lambda_{\\_}2\cdot{\sf r}{\sf s}\lambda$. Then
$\sigma_{\\_}1,\sigma_{\\_}2\in{\sf Tr^{+}}({\sf G})$ and ${\sf
ev}(\sigma_{\\_}1)={\sf ev}(\sigma_{\\_}2)=[{\sf r}{\sf s}\lambda]_{\sim}$.

###### Lemma 3.8

If ${\sf part}(\alpha_{\\_}1)={\sf part}(\alpha_{\\_}2)$ and ${\sf
ev}(\sigma\cdot\alpha_{\\_}1)=[\sigma^{\prime}\cdot\alpha_{\\_}1]_{\sim}$,
then ${\sf
ev}(\sigma\cdot\alpha_{\\_}2)=[\sigma^{\prime}\cdot\alpha_{\\_}2]_{\sim}$.

We proceed now to define the causality and conflict relations on g-events.

######  Definition 3.9 (Causality and conflict relations on g-events)

The causality relation $\leq$ and the conflict relation $~{}\\#~{}$ on the set
of g-events $\mathcal{G\\!E}$ are defined by:

  1. 1.

$\gamma\leq\gamma^{\prime}$ if $\gamma=[\sigma]_{\sim}$ and
$\gamma^{\prime}=[\sigma\,{\cdot}\,\sigma^{\prime}]_{\sim}$ for some
$\sigma,\sigma^{\prime}$;

  2. 2.

$\gamma\,\,\\#\,\,\gamma^{\prime}$ if $\gamma=[\sigma\cdot{\sf p}{\sf
q}\lambda_{\\_}1\cdot\sigma_{\\_}1]_{\sim}$ and
$\gamma^{\prime}=[\sigma\cdot{\sf p}{\sf
q}\lambda_{\\_}2\cdot\sigma_{\\_}2]_{\sim}$ for some
$\sigma,\sigma_{\\_}1,\sigma_{\\_}2,{\sf p},{\sf
q},\lambda_{\\_}1,\lambda_{\\_}2$ where $\lambda_{\\_}1\neq\lambda_{\\_}2$.

If
$\gamma=[\sigma\,{\cdot}\,\alpha\,{\cdot}\,\sigma^{\prime}\,{\cdot}\,\alpha^{\prime}]_{\sim}$,
then the communication $\alpha$ must be done before the communication
$\alpha^{\prime}$. This is expressed by the causality
$[\sigma\,{\cdot}\,\alpha]_{\sim}\leq\gamma$. An example is $[{\sf p}{\sf
q}\lambda]_{\sim}\leq[{\sf r}{\sf s}\lambda^{\prime}\,{\cdot}\,{\sf p}{\sf
q}\lambda\,{\cdot}\,{\sf s}{\sf q}\lambda^{\prime\prime}]_{\sim}$. As regards
the conflict relation, an example is $[{\sf r}{\sf s}\lambda\,{\cdot}\,{\sf
p}{\sf q}\lambda_{\\_}1\,{\cdot}\,{\sf q}{\sf r}\lambda]_{\sim}~{}\\#~{}[{\sf
p}{\sf q}\lambda_{\\_}2\,{\cdot}\,{\sf r}{\sf s}\lambda]_{\sim}$, since ${\sf
p}{\sf q}\lambda_{\\_}2\,{\cdot}\,{\sf r}{\sf s}\lambda\sim{\sf r}{\sf
s}\lambda\,{\cdot}\,{\sf p}{\sf q}\lambda_{\\_}2$.

######  Definition 3.10 ( [5] Event structure of a global type)

The event structure of the global type  ${{\sf G}}$ is the triple
$\mathcal{S}({{\sf G}})=(\mathcal{E}({{\sf G}}),\leq_{\\_}{{\sf
G}},\,\\#\,_{\\_}{{\sf G}})$ where: $\mathcal{E}({{\sf G}})=\\{{\sf
ev}(\sigma)\ |\ \sigma\in{\sf Tr^{+}}({\sf G})\\}$ and $\leq_{\\_}{{\sf G}}$
and $~{}\\#~{}_{\\_}{{\sf G}}$ are the restrictions of $\leq$ and $~{}\\#~{}$
to $\mathcal{E}({{\sf G}})$.

When clear from the context, we shall omit the subscript ${\sf G}$ in the
relations $\leq_{\\_}{\sf G}$ and $~{}\\#~{}_{\\_}{\sf G}$.

In the sequel, a PES obtained from a global type by Definition 3.10 will often
be called a g-PES.

It should be stressed that Definition 3.10 only makes sense for global types
that are projectable. Such global types are guaranteed to be _realisable_ by
some distributed implementation, i.e., to type some network. For these global
types it has been shown in [5] that the semantics in Definition 3.10 preserves
and reflects the operational semantics, namely that ${\sf G}$ performs a
transition sequence labelled by a trace $\sigma$ in the LTS of Figure 1 if and
only if the associated PES admits the configuration $X=\\{{\sf
ev}(\sigma^{\prime})\ |\ \sigma^{\prime}\sqsubseteq\sigma\\}$.

###### Example 3.11

The global type ${\sf G}={\sf p}\to{\sf q}:\\{\lambda_{\\_}1;{\sf
r}\stackrel{{\scriptstyle\lambda_{\\_}3}}{{\to}}{\sf s},\lambda_{\\_}2;{\sf
r}\stackrel{{\scriptstyle\lambda_{\\_}3}}{{\to}}{\sf s}\\}$ is projectable,
with projections:

${\sf G}\\!\upharpoonright\\!{\sf p}\,=P={\sf q}!\lambda_{\\_}1\oplus{\sf
q}!\lambda_{\\_}2\qquad{\sf G}\\!\upharpoonright\\!{\sf q}\,=Q={\sf
p}?\lambda_{\\_}1+{\sf p}?\lambda_{\\_}2\qquad{\sf G}\\!\upharpoonright\\!{\sf
r}\,=R={\sf s}!\lambda_{\\_}3\qquad{\sf G}\\!\upharpoonright\\!{\sf
s}\,=U={\sf r}?\lambda_{\\_}3$

Clearly, ${\sf G}$ types the network ${\sf p}[\\![\,P\,]\\!]\mathrel{\|}{\sf
q}[\\![\,Q\,]\\!]\mathrel{\|}{\sf r}[\\![\,R\,]\\!]\mathrel{\|}{\sf
s}[\\![\,U\,]\\!]$. The PES $S$ associated with ${\sf G}$ by Definition 3.10
has three events $\gamma_{\\_}1=[{\sf p}{\sf
q}\lambda_{\\_}1]_{\sim},\gamma_{\\_}2=[{\sf p}{\sf
q}\lambda_{\\_}2]_{\sim},\gamma_{\\_}3=[{\sf r}{\sf s}\lambda_{\\_}3]_{\sim}$,
with $\leq_{\\_}{\sf G}=Id$ and $\gamma_{\\_}1~{}\\#~{}_{\\_}{\sf
G}\gamma_{\\_}2$.

Consider now the global type ${\sf G}^{\prime}={\sf p}\to{\sf
q}:\\{\lambda_{\\_}1;\mathsf{End},\lambda_{\\_}2;{\sf
r}\stackrel{{\scriptstyle\lambda_{\\_}3}}{{\to}}{\sf s}\\}$, where the first
branch of the choice has no continuation. Clearly, ${\sf G}^{\prime}$ is _not_
projectable. However, Definition 3.10 associates the same PES $S$ with ${\sf
G}^{\prime}$, whereas ${\sf G}^{\prime}$ and $S$ do not have the same
operational semantics, since ${\sf G}^{\prime}\xrightarrow{{\sf p}{\sf
q}\lambda_{\\_}1}\mathsf{End}$ while in the PES $S$ the configuration
$\mathcal{X}=\\{\gamma_{\\_}1\\}$ can be extended to the configuration
$\mathcal{X}^{\prime}=\\{\gamma_{\\_}1,\gamma_{\\_}3\\}$.

Our PES interpretation of global types explicitly brings out the concurrency
between communications that is left implicit in the syntax of global types. We
prove now that all well-formed global types that type the same network yield
the same PES (Theorem 3.15). We start by proving a weaker theorem, which
follows from results established in [13] and [5]. We say that two well-formed
global types ${\sf G}$ and ${\sf G}^{\prime}$ are _equivalent_ if $\vdash{\sf
N}:{\sf G}$ and $\vdash{\sf N}:{\sf G}^{\prime}$ for some network ${\sf N}$.
Let $\cong$ denote PES isomorphism.

######  Theorem 3.12 ( Equivalent well-formed global types yield isomorphic
PESs)

Let ${\sf G}$ and ${\sf G}^{\prime}$ be well-formed global types. If
$\vdash{\sf N}:{\sf G}$ and $\vdash{\sf N}:{\sf G}^{\prime}$ for some network
${\sf N}$, then $\mathcal{S}({\sf G})\cong\mathcal{S}({\sf G}^{\prime})$.

######  Proof 3.13.

It was shown in [5] (Theorem 8.18 p 25) that if $\vdash{\sf N}:{\sf G}$ then
the domain of configurations of $\mathcal{S}({\sf G})$ is isomorphic to the
domain of configurations of the Flow Event Structure associated with ${\sf
N}$. Then, from $\vdash{\sf N}:{\sf G}$ and $\vdash{\sf N}:{\sf G}^{\prime}$
it follows that $\mathcal{S}({\sf G})$ and $\mathcal{S}({\sf G}^{\prime})$
have isomorphic domains of configurations. A classical result in [13] (Theorem
9 p. 102) establishes that a PES $S$ is isomorphic to the PES whose events are
the prime elements of the domain of configurations of $S$, with causality
relation given by set inclusion and conflict relation given by set
inconsistency. We conclude that $\mathcal{S}({\sf G})\cong\mathcal{S}({\sf
G}^{\prime})$.

We now wish to go a step further by showing that $\mathcal{S}({\sf G})$ and
$\mathcal{S}({\sf G}^{\prime})$ are actually _identical_ PESs. We write ${\sf
G}\xrightarrow{\sigma}{\sf G}^{\prime}$ if ${\sf
G}\xrightarrow{\alpha_{\\_}1}{\sf
G}_{\\_}1\cdots\xrightarrow{\alpha_{\\_}n}{\sf G}_{\\_}n$ where
$\alpha_{\\_}1\cdots\alpha_{\\_}n=\sigma$ and ${\sf G}_{\\_}n=G^{\prime}$, and
${\sf G}\xrightarrow{\sigma}$ if there exists ${\sf G}^{\prime}$ such that
${\sf G}\xrightarrow{\sigma}{\sf G}^{\prime}$. A similar notation will be used
for transition sequences of a network ${\sf N}$.

Our next theorem relies on the following key lemma.

######  Lemma 3.14.

Let ${\sf G}$ be a global type and $\sigma$ be a trace. Then:

  1. 1.

$\sigma\in{\sf Tr^{+}}({\sf G})$ implies ${\sf G}\xrightarrow{\sigma}\,$;

  2. 2.

${\sf G}\xrightarrow{\sigma}$ implies ${\sf ev}(\sigma)\in\mathcal{E}({\sf
G})$.

######  Theorem 3.15 ( Equivalent well-formed global types yield identical
PESs).

Let ${\sf G}$ and ${\sf G}^{\prime}$ be well-formed global types. If
$\vdash{\sf N}:{\sf G}$ and $\vdash{\sf N}:{\sf G}^{\prime}$ for some network
${\sf N}$, then $\mathcal{S}({\sf G})=\mathcal{S}({\sf G}^{\prime})$.

######  Proof 3.16.

It is enough to show that $\mathcal{S}({\sf G})$ and $\mathcal{S}({\sf
G}^{\prime})$ have exactly the same sets of events, since events are defined
syntactically and the relations of causality and conflict can be extracted
from their syntax.

We prove that $\mathcal{E}({\sf G})=\mathcal{E}({\sf G}^{\prime})$. Let
$e\in\mathcal{E}({\sf G})$. By Definition 3.10 there exists $\sigma\in{\sf
Tr^{+}}({\sf G})$ such that ${\sf ev}(\sigma)=e$. Then ${\sf
G}\xrightarrow{\sigma}\,$ by Lemma 3.14(1), from which we deduce ${\sf
N}\xrightarrow{\sigma}\,$ by the Session Fidelity result in [5] (Theorem 6.11
p. 16). Then ${\sf G}^{\prime}\xrightarrow{\sigma}\,$ by the Subject Reduction
result in [5] (Theorem 6.10 p. 16). By Lemma 3.14(2) this implies ${\sf
ev}(\sigma)\in\mathcal{E}({\sf G}^{\prime})$, i.e., $e\in\mathcal{E}({\sf
G}^{\prime})$.

##  4 Semantic Well-formedness

We now investigate semantic counterparts for the syntactic well-formedness
property of global types. Recall that type well-formedness is the conjunction
of two properties: projectability and boundedness. We start by defining a
notion of _semantic projectability_ for PESs. We first give some auxiliary
definitions.

######  Definition 4.1.

Let ${\sf G}$ be a global type and $\mathcal{S}({{\sf G}})=(\mathcal{E}({{\sf
G}}),\leq,\,\\#\,)$. Two events
$\gamma_{\\_}1,\gamma_{\\_}2\in\mathcal{E}({{\sf G}})$ are in initial
conflict, $\gamma_{\\_}1\,\\#_{in}\,\gamma_{\\_}2$, if
$\gamma_{\\_}1=[\sigma\,{\cdot}\,{\sf p}{\sf q}\lambda_{\\_}1]_{\sim}$ and
$\gamma_{\\_}2=[\sigma\,{\cdot}\,{\sf p}{\sf q}\lambda_{\\_}2]_{\sim}$ for
some $\sigma,{\sf p},{\sf q},\lambda_{\\_}1,\lambda_{\\_}2$ such that
$\lambda_{\\_}1\neq\lambda_{\\_}2$.

######  Definition 4.2 (Projection of traces on participants).

The projection of $\sigma$ on ${\sf r}$, $\sigma@{\sf r}\,$, is defined by:

$\epsilon@{\sf r}\,=\epsilon\quad\quad({\sf p}{\sf q}\lambda\cdot\sigma)@{\sf
r}\,=\begin{cases}{\sf q}!\lambda\cdot\sigma@{\sf r}\,&\text{if }{\sf r}={\sf
p}\\\ {\sf p}?\lambda\cdot\sigma@{\sf r}\,&\text{if }{\sf r}={\sf q}\\\
\sigma@{\sf r}\,&\text{if }{\sf r}\not\in\\{{\sf p},{\sf q}\\}\end{cases}$

######  Definition 4.3 (Semantic projectability).

Let ${\sf G}$ be a global type and $\mathcal{S}({{\sf G}})=(\mathcal{E}({{\sf
G}}),\leq,\,\\#\,)$. We say that $\mathcal{S}({{\sf G}})$ is semantically
projectable if for all $\gamma_{\\_}1,\gamma_{\\_}2\in\mathcal{E}({{\sf G}})$
in initial conflict:

  * if there is $\gamma^{\prime}_{\\_}1=[\sigma_{\\_}1\,{\cdot}\,\alpha_{\\_}1]_{\sim}$ with $\gamma_{\\_}1\leq_{\\_}{{\sf G}}\gamma^{\prime}_{\\_}1$ and ${\sf r}\in{\sf part}(\alpha_{\\_}1)\backslash{\sf part}({\sf cm}(\gamma_{\\_}1))$,

  * then there is $\gamma^{\prime}_{\\_}2=[\sigma_{\\_}2\,{\cdot}\,\alpha_{\\_}2]_{\sim}$ with $\gamma_{\\_}2\leq_{\\_}{{\sf G}}\gamma^{\prime}_{\\_}2$ and $\alpha_{\\_}2=\alpha_{\\_}1$ and $\sigma_{\\_}2@{\sf r}\,=\sigma_{\\_}1@{\sf r}\,$.

Note that if ${\sf G}$ is semantically projectable, then also any subterm
${{\sf G}}^{\prime}$ of ${\sf G}$ is semantically projectable.

We now show that, if a global type ${\sf G}$ is projectable, then all initial
conflicts between two participants ${\sf p}$ and ${\sf q}$ in the event
structure $\mathcal{S}({{\sf G}})$ reflect branching points between ${\sf p}$
and ${\sf q}$ in the tree of ${\sf G}$. In general, the mapping from branching
points in the tree of ${\sf G}$ to initial conflicts in $\mathcal{S}({{\sf
G}})$ is not injective, namely, there may be several branching points in the
tree of ${\sf G}$ that give rise to the same initial conflict in
$\mathcal{S}({{\sf G}})$.

######  Lemma 4.4 (Initial conflicts in $\mathcal{S}({{\sf G}})$ reflect
branching points in the tree of ${\sf G}$).

Let ${\sf G}$ be a global type and $\mathcal{S}({{\sf G}})=(\mathcal{E}({{\sf
G}}),\leq,\,\\#\,)$. Let $\gamma_{\\_}1,\gamma_{\\_}2\in\mathcal{E}({{\sf
G}})$ be in initial conflict and
$\gamma_{\\_}i=[\sigma\,{\cdot}\,\alpha_{\\_}i]_{\sim}$ for $i\in\\{1,2\\}$.
If ${{\sf G}}$ is projectable then there exists $\sigma^{\prime}$ such that
$\sigma^{\prime}\cdot\alpha_{\\_}i\in{\sf Tr^{+}}({\sf G})$ and ${\sf
ev}(\sigma^{\prime}\cdot\alpha_{\\_}i)=[\sigma\cdot\alpha_{\\_}i]_{\sim}$ for
$i\in\\{1,2\\}$.

Let $\sigma\in{\sf Tr^{+}}({\sf G})$. We denote by ${\sf G}_{\\_}{\sigma}$ the
subterm of ${\sf G}$ after $\sigma$, which is easily defined by induction on
the length of $\sigma$. The converse of Lemma 4.4 is immediate, since any
subterm of ${\sf G}$ is ${\sf G}_{\\_}{\sigma}$ for some $\sigma\in{\sf
Tr^{+}}({\sf G})$. So if ${\sf G}_{\\_}{\sigma}={\sf p}\to{\sf
q}:\\{\lambda_{i};{\sf G}^{\prime}_{i}\\}_{i\in I}$ with $\\{1,2\\}\subseteq
I$, then the two events $\gamma_{\\_}1={\sf ev}(\sigma\cdot{\sf p}{\sf
q}\lambda_{\\_}1)$ and $\gamma_{\\_}2={\sf ev}(\sigma\cdot{\sf p}{\sf
q}\lambda_{\\_}2)$ are in initial conflict because by Lemma 3.8 there exists
$\sigma^{\prime}$ such that ${\sf ev}(\sigma\cdot{\sf p}{\sf
q}\lambda_{\\_}i)=[\sigma^{\prime}\cdot{\sf p}{\sf q}\lambda_{\\_}i]_{\sim}$
for $i\in\\{1,2\\}$.

######  Theorem 4.5 (Projectability preservation).

If ${{\sf G}}$ is projectable then $\mathcal{S}({{\sf G}})$ is semantically
projectable.

######  Proof 4.6.

Let $\gamma_{\\_}1,\gamma_{\\_}2\in\mathcal{E}({{\sf G}})$ and
$\gamma_{\\_}1\,\\#_{in}\,\gamma_{\\_}2$. By definition,
$\gamma_{\\_}1=[\sigma\,{\cdot}\,{\sf p}{\sf q}\lambda_{\\_}1]_{\sim}$ and
$\gamma_{\\_}2=[\sigma\,{\cdot}\,{\sf p}{\sf q}\lambda_{\\_}2]_{\sim}$ for
some $\sigma,{\sf p},{\sf q},\lambda_{\\_}1,\lambda_{\\_}2$ such that
$\lambda_{\\_}1\neq\lambda_{\\_}2$. Let $\alpha_{\\_}i={\sf p}{\sf
q}\lambda_{\\_}i$ for $i\in\\{1,2\\}$.
Since ${{\sf G}}$ is projectable, by Lemma 4.4 there exists $\sigma^{\prime}$
such that $\sigma^{\prime}\cdot\alpha_{\\_}i\in{\sf Tr^{+}}({\sf G})$ and
${\sf
ev}(\sigma^{\prime}\cdot\alpha_{\\_}i)=[\sigma\cdot\alpha_{\\_}i]_{\sim}$ for
$i\in\\{1,2\\}$. Then ${\sf G}_{\\_}{\sigma^{\prime}}={\sf p}\to{\sf
q}:\\{\lambda_{i};{\sf G}^{\prime}_{i}\\}_{i\in I}$ with $\\{1,2\\}\subseteq
I$. Since ${\sf G}$ is projectable, also ${\sf G}_{\\_}{\sigma^{\prime}}$ is
projectable. Thus, for any ${\sf r}\not\in\\{{\sf p},{\sf q}\\}$ we get ${\sf
G}^{\prime}_{\\_}1\\!\upharpoonright\\!{\sf r}\,={\sf
G}^{\prime}_{\\_}2\\!\upharpoonright\\!{\sf r}\,$.
Let $\gamma^{\prime}_{\\_}1\in\mathcal{E}({{\sf G}})$, with
$\gamma_{\\_}1\leq_{\\_}{{\sf G}}\gamma^{\prime}_{\\_}1$, ${\sf
cm}(\gamma^{\prime}_{\\_}1)=\beta$, and ${\sf r}\in{\sf
part}(\beta)\backslash\\{{\sf p},{\sf q}\\}$. Since
$\gamma_{\\_}1\leq_{\\_}{{\sf G}}\gamma^{\prime}_{\\_}1$, it must necessarily
be
$\gamma^{\prime}_{\\_}1=[\sigma\cdot\alpha_{\\_}1\cdot\sigma_{\\_}1\cdot\beta]_{\sim}={\sf
ev}(\sigma^{\prime}\cdot\alpha_{\\_}1\cdot\sigma^{\prime}_{\\_}1\cdot\beta)$
for some $\sigma_{\\_}1,\sigma^{\prime}_{\\_}1$. Then
$\sigma^{\prime}_{\\_}1\cdot\beta$ is a path in ${\sf G}^{\prime}_{\\_}1$.
Since ${\sf G}_{\\_}{\sigma^{\prime}}$ is projectable, ${\sf
G}^{\prime}_{\\_}1\\!\upharpoonright\\!{\sf r}\,={\sf
G}^{\prime}_{\\_}2\\!\upharpoonright\\!{\sf r}\,$. Then there must be a path
$\sigma^{\prime}_{\\_}2$ of ${\sf G}^{\prime}_{\\_}2$ such that
$\sigma^{\prime}_{\\_}1\cdot\beta@{\sf
r}\,=\sigma^{\prime}_{\\_}2\cdot\beta@{\sf r}\,$. We want to show that
$\gamma^{\prime}_{\\_}2={\sf
ev}(\sigma^{\prime}\cdot\alpha_{\\_}2\cdot\sigma^{\prime}_{\\_}2\,{\cdot}\,\beta)=[\sigma^{\prime}\cdot\alpha_{\\_}2\cdot\sigma_{\\_}2\,{\cdot}\,\beta]_{\sim}$
for some $\sigma_{\\_}2$, i.e., that
$\gamma_{\\_}2\leq\gamma^{\prime}_{\\_}2$. Now, if ${\sf
part}(\beta)\cap\\{{\sf p},{\sf q}\\}\neq\emptyset$, we can conclude
immediately. So, let us assume ${\sf part}(\beta)\cap\\{{\sf p},{\sf
q}\\}=\emptyset$.
Since $\gamma^{\prime}_{\\_}1={\sf
ev}(\sigma^{\prime}\cdot\alpha_{\\_}1\cdot\sigma^{\prime}_{\\_}1\cdot\beta)=[\sigma\cdot\alpha_{\\_}1\cdot\sigma_{\\_}1\cdot\beta]_{\sim}$
we know that $\alpha_{\\_}1\cdot\sigma_{\\_}1\cdot\beta$ is a pointed trace.
So, there must be a _bridging communication sequence_ between $\alpha_{\\_}1$
and $\beta$, namely there must be a subtrace $\beta_{\\_}1\cdots\beta_{\\_}n$
of $\sigma_{\\_}1$ for some $n\geq 1$ such that

${\sf part}(\alpha_{\\_}1)\cap{\sf part}(\beta_{\\_}1)\neq\emptyset\qquad{\sf
part}(\beta_{\\_}n)\cap{\sf part}(\beta)\neq\emptyset\qquad{\sf
part}(\beta_{\\_}i)\cap{\sf
part}(\beta_{\\_}{i+1})\neq\emptyset~{}~{}~{}\mbox{for}~{}~{}1\leq i<n$

Correspondingly, we will have
$\sigma^{\prime}_{\\_}1=\widehat{\sigma}_{\\_}1\cdot\beta_{\\_}1\,\cdots\,\widehat{\sigma}_{\\_}n\cdot\beta_{\\_}{n}$.
There are now two possible cases:

\- ${\sf part}(\beta_{\\_}i)\neq\\{{\sf p},{\sf q}\\}$ for every
$i=1,\ldots,n$. Since ${\sf G}_{\\_}{\sigma^{\prime}}$ is projectable, ${\sf
G}^{\prime}_{\\_}1\\!\upharpoonright\\!{\sf s}\,={\sf
G}^{\prime}_{\\_}2\\!\upharpoonright\\!{\sf s}\,$ for all ${\sf
s}\not\in\\{{\sf p},{\sf q}\\}$, i.e., $\sigma^{\prime}_{\\_}1@{\sf
s}\,=\sigma^{\prime}_{\\_}2@{\sf s}\,$. Therefore all the $\beta_{\\_}{i}$’s
for $1\leq i\leq n$ must occur in the same order in $\sigma^{\prime}_{\\_}2$,
i.e.
$\sigma^{\prime}_{\\_}2=\tau_{\\_}1\cdot\beta_{\\_}1\,\cdots\,\tau_{\\_}n\cdot\beta_{\\_}n$
for some $\tau_{\\_}1,\ldots,\tau_{\\_}n$. Hence ${\sf
ev}(\sigma^{\prime}\cdot\alpha_{\\_}2\cdot\sigma^{\prime}_{\\_}2\,{\cdot}\,\beta)=[\sigma^{\prime}\cdot\alpha_{\\_}2\cdot\sigma_{\\_}2\,{\cdot}\,\beta]_{\sim}$
for some $\sigma_{\\_}2$.

\- ${\sf part}(\beta_{\\_}j)=\\{{\sf p},{\sf q}\\}$ for some $j$, $1\leq j\leq
n$. Let $k$ be the maximum such index $j$. Then we know that ${\sf
part}(\beta_{\\_}{h})\neq\\{{\sf p},{\sf q}\\}$ for every $h,k+1\leq h\leq n$,
and either ${\sf p}\in{\sf part}(\beta_{\\_}{k+1})$ or ${\sf q}\in{\sf
part}(\beta_{\\_}{k+1})$. Therefore all the $\beta_{\\_}{h}$’s for $k+1\leq
h\leq n$ must occur in the same order in $\sigma^{\prime}_{\\_}2$, i.e.
$\sigma^{\prime}_{\\_}2=\tau_{\\_}k\cdot\beta_{\\_}{k+1}\,\cdots\,\tau_{\\_}n\cdot\beta_{\\_}n$
for some $\tau_{\\_}k,\ldots,\tau_{\\_}n$. Hence, ${\sf
ev}(\sigma^{\prime}\cdot\alpha_{\\_}2\cdot\sigma^{\prime}_{\\_}2\,{\cdot}\,\beta)=[\sigma^{\prime}\cdot\alpha_{\\_}2\cdot\sigma_{\\_}2\,{\cdot}\,\beta]_{\sim}$
for some $\sigma_{\\_}2$.

The converse is not true, i.e., semantic projectability of $\mathcal{S}({{\sf
G}})$ does not imply projectability of ${\sf G}$, as shown by the global type
${\sf G}^{\prime}$ in Example 3.11. Note that there is no network behaving as
prescribed by ${\sf G}^{\prime}$. We conjecture that for realisable global
types semantic projectability implies projectability.

We now define a notion of semantic boundedness for PESs, which is _global_ in
that it looks simultaneously at all occurrences of each participant ${\sf p}$
in the g-events whose last communication involves ${\sf p}$. Let
$S=(E,\leq,\,\\#\,)$ be a g-PES. For any participant ${\sf p}$, let ${\sf
p}\in{\sf part}(S)$ if there exists $\gamma\in E$ such that ${\sf p}\in{\sf
part}(\gamma)$.

######  Definition 4.7 (Semantic $k$-depth and semantic boundedness).

Let $S=(E,\leq,\,\\#\,)$ be a g-PES. The two functions $\delta_{{\sf
sem}}^{k}({\sf p},\gamma)$ and $\delta_{{\sf gsem}}({\sf p},S)$ are defined
by:

$\begin{array}[]{l}\delta_{{\sf sem}}^{k}({\sf
p},[\sigma]_{\sim})=\begin{cases}\\!\\!~{}|~{}\\!\sigma\\!~{}|~{}\\!&\text{ if
}~{}\sigma=\sigma_{\\_}1\cdot\alpha_{\\_}1\cdots\sigma_{\\_}k\cdot\alpha_{\\_}k\begin{array}[t]{l}\text{
and }{\sf p}\in{\sf part}(\alpha_{\\_}i)~{}~{}\mbox{for $i=1,\ldots,k$}\\\
\text{ and }{\sf p}\notin{\sf part}(\sigma_{\\_}i)~{}~{}\mbox{for
$i=1,\ldots,k$}\end{array}\\\ 0&\text{otherwise }\end{cases}\\\
\delta^{k}_{{\sf gsem}}({\sf p},S)=\sup(\\{\delta_{{\sf sem}}^{k}({\sf
p},\gamma)\ |\ \gamma\in E\\})~{}~{}\mbox{for
every}~{}k\in\mathbb{N}\end{array}$

$S$ is semantically bounded if $\delta^{k}_{{\sf gsem}}({\sf p},S)$ is finite
for each participant ${\sf p}\in{\sf part}(S)$ and each $k\in\mathbb{N}$.

######  Theorem 4.8 (Boundedness preservation).

If ${\sf G}$ is bounded, then $\mathcal{S}({{\sf G}})$ is semantically
bounded.

######  Proof 4.9.

Let ${\sf G}$ be bounded and $\mathcal{S}({{\sf G}})=(\mathcal{E}({{\sf
G}}),\leq,\,\\#\,)$. We want to show that $\delta^{k}_{{\sf gsem}}({\sf
p},\mathcal{S}({{\sf G}}))$ is finite for each participant ${\sf p}\in{\sf
part}(\mathcal{S}({{\sf G}}))$ and each $k\in\mathbb{N}$. Fix some ${\sf p}$.
If ${\sf p}\not\in{\sf part}({\sf G})$ then ${\sf p}\not\in{\sf
part}(\mathcal{S}({{\sf G}}))$ and thus the statement is vacuously true. So,
assume ${\sf p}\in{\sf part}({\sf G})$. We show now, by induction on $k$, that
there exists $n_{\\_}k\in\mathbb{N}$ such that $\delta_{{\sf sem}}^{k}({\sf
p},\gamma)\leq n_{\\_}k$ for any $\gamma\in\mathcal{E}({{\sf G}})$.

\- Case $k=1$. We may assume
$\gamma=[\sigma_{\\_}1\cdot\alpha_{\\_}1]_{\sim}\in\mathcal{E}({\sf G})$ with
${\sf p}\not\in{\sf part}(\sigma_{\\_}1)$ and ${\sf p}\in{\sf
part}(\alpha_{\\_}1)$, since for any $\gamma^{\prime}$ not of this shape we
have $\delta_{{\sf sem}}^{1}({\sf p},\gamma^{\prime})=0$ and we can
immediately conclude. Then there exists
$\sigma^{\prime}_{\\_}1\cdot\alpha_{\\_}1\in{\sf Tr^{+}}({\sf G})$ such that
$\gamma={\sf ev}(\sigma^{\prime}_{\\_}1\cdot\alpha_{\\_}1)$. Note that it must
be ${\sf p}\not\in{\sf part}(\sigma^{\prime}_{\\_}1)$, since otherwise there
would be some $\beta$ in $\sigma^{\prime}_{\\_}1$ such that ${\sf
part}(\beta)\cap{\sf part}(\alpha_{\\_}1)\neq\emptyset$ and the function ${\sf
ev}(\cdot)$ would keep this $\beta$, contradicting the hypothesis ${\sf
p}\not\in{\sf part}(\sigma_{\\_}1)$. Let $n_{\\_}1=\delta({\sf p},{\sf
G})=\sup(\\{\delta({\sf p},\sigma)\ |\ \sigma\in{\sf Tr^{+}}({\sf G})\\})$. By
Definition 2.4 ${\delta({\sf
p},\sigma^{\prime}_{\\_}1\cdot\alpha_{\\_}1)}=\\!\\!~{}|~{}\\!\sigma^{\prime}_{\\_}1\cdot\alpha_{\\_}1\\!~{}|~{}\\!\leq
n_{\\_}1$. Then by Definition 4.7 we get $\delta_{{\sf sem}}^{1}({\sf
p},[\sigma_{\\_}1\cdot\alpha_{\\_}1]_{\sim})={\\!\\!~{}|~{}\\!\sigma_{\\_}1\cdot\alpha_{\\_}1\\!~{}|~{}\\!\leq\\!\\!~{}|~{}\\!\sigma^{\prime}_{\\_}1\cdot\alpha_{\\_}1\\!~{}|~{}\\!\leq
n_{\\_}1}$.

\- Case $k>1$. Assume that $\sup(\\{\delta_{{\sf sem}}^{k-1}({\sf p},\gamma)\
|\ \gamma\in\mathcal{E}({{\sf G}})\\})\leq n_{\\_}{k-1}$. Let
$\sigma=\sigma_{\\_}1\cdot\alpha_{\\_}1\cdots\sigma_{\\_}k\cdot\alpha_{\\_}k$
be such that ${\sf p}\not\in{\sf part}(\sigma_{\\_}i)$ and ${\sf p}\in{\sf
part}(\alpha_{\\_}i)$ for every $i=1,\ldots,k$, and let
$\gamma=[\sigma]_{\sim}\in\mathcal{E}({\sf G})$. Then there exists
$\sigma^{\prime}=\sigma^{\prime}_{\\_}1\cdot\alpha_{\\_}1\cdots\sigma^{\prime}_{\\_}k\cdot\alpha_{\\_}k\in{\sf
Tr^{+}}({\sf G})$ such that $\gamma={\sf ev}(\sigma^{\prime})$. For each
$i=1,\ldots,k$ we must have ${\sf p}\not\in{\sf
part}(\sigma^{\prime}_{\\_}i)$, because otherwise we would contradict the
hypothesis ${\sf p}\not\in{\sf part}(\sigma_{\\_}i)$ (as argued in the
previous case). Let now
$\sigma^{\prime\prime}=\sigma^{\prime}_{\\_}1\cdot\alpha_{\\_}1\cdots\sigma^{\prime}_{\\_}{k-1}\cdot\alpha_{\\_}{k-1}$,
and consider the subterm ${\sf G}_{\\_}{\sigma^{\prime\prime}}$ of ${\sf G}$.

Since ${\sf G}$ is bounded and ${\sf G}_{\\_}{\sigma^{\prime\prime}}$ is a
subtree of ${\sf G}$, by Definition 2.4 we get $\delta({\sf p},{\sf
G}_{\\_}{\sigma^{\prime\prime}})=\sup(\\{\delta({\sf p},\sigma)\ |\
\sigma\in{\sf Tr^{+}}({\sf G}_{\\_}{\sigma^{\prime\prime}})\\})=m\,$ for some
$m\in\mathbb{N}$. Therefore $\delta_{{\sf sem}}^{1}({\sf
p},[\sigma_{\\_}k\cdot\alpha_{\\_}k]_{\sim})=\\!\\!~{}|~{}\\!\sigma_{\\_}k\cdot\alpha_{\\_}k\\!~{}|~{}\\!\leq\\!\\!~{}|~{}\\!\sigma^{\prime}_{\\_}k\cdot\alpha_{\\_}k\\!~{}|~{}\\!=\delta({\sf
p},\sigma^{\prime}_{\\_}k\cdot\alpha_{\\_}k)\leq m$. $\delta({\sf
p},\sigma^{\prime}_{\\_}k\cdot\alpha_{\\_}k)=\\!\\!~{}|~{}\\!\sigma^{\prime}_{\\_}k\cdot\alpha_{\\_}k\\!~{}|~{}\\!\leq
m$. Let $n_{\\_}k=n_{\\_}{k-1}+m$. We may conclude that $\delta_{{\sf
sem}}^{k}({\sf
p},[\sigma_{\\_}1\cdot\alpha_{\\_}1\cdots\sigma_{\\_}k\cdot\alpha_{\\_}k]_{\sim})=\delta_{{\sf
sem}}^{k-1}({\sf
p},[\sigma_{\\_}1\cdot\alpha_{\\_}1\cdots\sigma_{\\_}{k-1}\cdot\alpha_{\\_}{k-1}]_{\sim})+\delta_{{\sf
sem}}^{1}({\sf p},[\sigma_{\\_}k\cdot\alpha_{\\_}k]_{\sim})\leq
n_{\\_}{k-1}+m=n_{\\_}k$.

##  5 Structural Properties of g-PESs

In this section we discuss some additional properties of the PESs we obtain by
interpreting global types. Some of these properties do not depend on the well-
formedness of global types but only on their syntax. For instance, since we
adopt for global types the _directed choice_ construct of [10, 11]: ${\sf
p}\to{\sf q}:\\{\lambda_{i};{\sf G}_{i}\\}_{i\in I}$, every branch of a choice
uses the same channel ${\sf p}{\sf q}$. As a consequence, g-PESs satisfy the
property of _initial conflict uniformity_ : in every set
$X=\\{\gamma_{\\_}1,\ldots,\gamma_{\\_}n\\}$ of initially conflicting
g-events, every $\gamma_{\\_}i\in X$ uses the same channel ${\sf p}{\sf q}$ in
its last communication, i.e., ${\sf cm}(\gamma_{\\_}i)={\sf p}{\sf
q}\lambda_{\\_}i$ for some $\lambda_{\\_}i$. Moreover, since global types have
deterministic LTSs, where no state can perform two different transitions with
the same label, the same holds for g-PESs: if
$\mathcal{X},\mathcal{X}\cup\\{\gamma_{\\_}1\\},\mathcal{X}\cup\\{\gamma_{\\_}2\\}$
are configurations of the same g-PES, then $\gamma_{\\_}1\neq\gamma_{\\_}2$
implies ${\sf cm}(\gamma_{\\_}1)\neq{\sf cm}(\gamma_{\\_}2)$. If moreover
$\neg(\gamma_{\\_}1~{}\\#~{}\gamma_{\\_}2)$, we additionally have ${\sf
part}({\sf cm}(\gamma_{\\_}1))\cap{\sf part}({\sf
cm}(\gamma_{\\_}2))=\emptyset$.

Note that our core session calculus may be viewed as a _linear_ subcalculus of
Milner’s calculus CCS, where parallel composition appears only at top level
and any pair of processes $P$ and $Q$, run by participants ${\sf p}$ and ${\sf
q}$, can communicate only via two unidirectional channels: channel ${\sf
p}{\sf q}$ for communication from ${\sf p}$ to ${\sf q}$, and channel ${\sf
q}{\sf p}$ for communication from ${\sf q}$ to ${\sf p}$. Hence, _restricted
parallel composition_ , which is the kind of parallel composition used in
session calculi, where processes are only allowed to communicate with each
other but not to proceed independently, becomes an associative operation,
while it is not associative in full CCS (as observed by Milner in his 1980
book, see [12] page 21).

Then, a natural question is: how does our ES semantics for the linear
subcalculus of CCS compare to the ES semantics proposed in [3, 4] for other
fragments of CCS? To carry out this comparison, we would need to take a more
extensional view of g-PESs, forgetting about the syntactic structure of
g-events and retaining only their last communication. In other words, we
should consider _Labelled PESs_ , where events are labelled by communications
${\sf p}{\sf q}\lambda$ and have no specific structure. Moreover, some care
should be taken since, unlike our session calculus, our language for global
types is _not_ a subcalculus of CCS: indeed, while the syntax of global types
is included in that of CCS with guarded sums, their semantics is not the same
as that of CCS processes, since some communications may be performed under
guards.

More in detail, the work [3] provides a characterisation of the class of
Labelled PESs obtained by interpreting the fragment of CCS built from actions
$a,b,\ldots$ by means of the three constructors $+,;,\parallel$, denoting
respectively choice, sequential composition and parallel composition with no
communication. As a matter of fact, [3] uses slightly more relaxed PESs where
conflict is not required to be hereditary - let us call them r-PESs - and
shows that the Labelled r-PESs obtained for that fragment of CCS are exactly
those satisfying two structural properties called _triangle freeness_ and _N-
freeness_. In conjunction, these two properties express the possibility of
extracting a head operator among $+,;,\parallel$ from the structure of the
r-PES. We recall from [3] the definition of these properties. Let $\smile$
denote the _concurrency_ relation on the events of a PES
$S=(E,\leq,~{}\\#~{})$, defined by $\smile\,=(E\times
E)-(\leq\cup\geq\cup\,\\#\,)$. Let $\diamond=(\leq\cup\geq)$ denote _causal
connection_. By definition the three relations $\diamond,\,\\#\,$ and $\smile$
set a partition over $E\times E$. Then triangle freeness (or
$\nabla$-freeness) is defined as the absence of a triple of events
$e,e^{\prime},e^{\prime\prime}$ such that
$e\,\diamond\,e^{\prime}\,\\#\,\,e^{\prime\prime}\smile e$ (see [3] page 41).
Note that one half of triangle-freeness, where $\diamond$ is replaced by
$\geq$, is implied by conflict hereditariness in g-PESs. We conjecture that
g-PESs satisfy also the other half of triangle-freeness, where $\diamond$ is
replaced by $\leq$, namely they do not feature the pattern
$e\,\leq\,e^{\prime}\,\\#\,\,e^{\prime\prime}\smile e$, a situation known as
_asymmetric confusion_ in Petri nets. The property of N-freeness is slightly
more involved. For any $R\in\\{\leq,\,\\#\,,\smile\\}$, let $R^{\varepsilon}$
be the reflexive and symmetric closure of $R$ and $\ddagger(R)$ be the
$R-incomparability$ relation defined by $\ddagger(R)=(E\times
E)-R^{\varepsilon}$. Then the N-freeness property is stated as follows:

_N-freeness_ $~{}\forall\,R\in\\{\leq,\,\\#\,,\smile\\}$: (
$e_{\\_}0Re_{\\_}1\,\land\,e_{\\_}0\ddagger(R)e_{\\_}2\,\land\,e_{\\_}2Re_{\\_}3\,\land\,e_{\\_}1\ddagger(R)e_{\\_}3\,)\implies(\,e_{\\_}0Re_{\\_}3\implies
e_{\\_}2Re_{\\_}1\,)$

This property does not hold for g-PESs, e.g., it does not hold for the g-PES
of the global type ${\sf G}={\sf
p}\stackrel{{\scriptstyle\lambda_{\\_}0}}{{\to}}{\sf q};{\sf
p}\stackrel{{\scriptstyle\lambda_{\\_}1}}{{\to}}{\sf t};{\sf
r}\stackrel{{\scriptstyle\lambda_{\\_}2}}{{\to}}{\sf s};{\sf
q}\stackrel{{\scriptstyle\lambda_{\\_}3}}{{\to}}{\sf s}$, with $e_{\\_}0=[{\sf
p}{\sf q}{\lambda_{\\_}0}]_{\sim},e_{\\_}1=[{\sf p}{\sf
q}{\lambda_{\\_}0}\cdot{\sf p}{\sf t}{\lambda_{\\_}1}]_{\sim},e_{\\_}2=[{\sf
r}{\sf s}{\lambda_{\\_}2}]_{\sim},e_{\\_}3=[{\sf p}{\sf
q}{\lambda_{\\_}0}\cdot{\sf r}{\sf s}{\lambda_{\\_}2}\cdot{\sf q}{\sf
s}{\lambda_{\\_}3}]_{\sim}$.

However, we may show that g-PESs satisfy particular instances of N-freeness,
for instance when $R$ is the covering relation of $\leq$ and
$e_{\\_}1\,\\#_{in}\,e_{\\_}3$ (in which case conflict hereditariness enforces
$e_{\\_}0\smile e_{\\_}2$).

The paper [4], on the other hand, presents a Flow Event Structure semantics
for the whole calculus CCS. Our conjecture is that this semantics should
coincide with the Flow ES semantics proposed for sessions in [5]. However,
this is not entirely trivial since the semantics of [4] uses self-conflicting
events, a specific feature of Flow ESs, to interpret restricted parallel
composition, while the semantics of [5] uses a pre-processing phase to rule
out the g-events that do not satisfy a causal well-foundedness condition, and
these events are a superset of those that are self-conflicting in the
semantics of [4]. However, one may already observe that the Flow ESs obtained
by interpreting sessions in [5] trivially satisfy the axiom $\Delta$ put
forward in [6] in order to guarantee that CCS parallel composition is a
categorical product.

##  6 Conclusion

We conclude by further discussing related work and by sketching some
directions for future work.

Related work. In Section 5 we compared our PES semantics for global types to
existing ES semantics for other fragments of CCS. In that case, the comparison
was somewhat hindered by the fact that the target ESs were not exactly the
same (PESs vs r-PESs vs Flow ESs). We now turn to other proposals of
denotational models for MPSTs. The models that are closest to ours are the
_graphical choreographies_ by Guanciale and Tuosto [15], the _choreography
automata_ by Barbanera, Lanese and Tuosto [2], the _global choreographies_ by
de’Liguoro, Melgratti and Tuosto [7], and the _branching pomsets_ by Edixhoven
et al. [9]. It should be noted that most of these works deal with asynchronous
communication, so “events” (or communications) are split into send events and
receive events. Common well-formedness conditions proposed in these works are
_well-branchedness_ [2, 7, 9], which in our case is enforced by the syntax of
global types, and _well-sequencedness_ [2, 7], which is automatically enforced
by our PES semantics. As regards the use of ESs to model MPSTs, the paper [7]
also uses PESs to model (asynchronous) choreographies, but it needs an
additional type system to obtain projectability (so, the resulting notion of
projectability is not totally semantic). In [9], asynchronous choreographies
are modelled with branching pomsets, a model featuring both concurrency and
choice, which is compared with various classes of ESs.

Future work. In this paper, we have devised semantic counterparts for the
well-formedness conditions of global types. However, we have only gone half
the way in establishing a characterisation of the class of Prime ESs
representing well-formed global types. To achieve such a characterisation, we
should prove the converse of Theorem 4.8 and the following weaker form of the
converse of Theorem 4.5:

Conjecture [Projectability reflection] Let ${\sf G}$ be a global type. If
$\mathcal{S}({\sf G})$ is semantically projectable then there exists a
projectable global type ${\sf G}^{\prime}$ such that $\mathcal{S}({\sf
G}^{\prime})=\mathcal{S}({\sf G})$.

If this conjecture were true, then our PES semantics for global types would
also provide a way to “sanitise” ill-formed global types. For instance,
starting from the g-PES $\mathcal{S}({\sf G}^{\prime})$ of the ill-formed
global type ${\sf G}^{\prime}$ of Example 3.11, we would be able to get back
to the well-formed global type ${\sf G}$ of the same example or to the well-
formed global type ${\sf G}^{\prime\prime}={\sf
r}\stackrel{{\scriptstyle\lambda_{\\_}3}}{{\to}}{\sf s};{\sf p}\to{\sf
q}:\\{\lambda_{\\_}1;\mathsf{End},\lambda_{\\_}2;\mathsf{End}\\}$. Once we
achieve a characterisation for this class of g-PESs, the next step would be to
propose an algorithm to synthesise a well-formed global type (or directly a
network) from a g-PES of this class. A further goal would be to semantically
characterise less restrictive notions of projection, such as the one proposed
in [8].

Since g-PESs are images of regular trees, it would be worth investigating
their connection with Regular Event Structures [14]. Moreover, as argued in
the previous section, extensional g-PESs, where g-events have no structure and
are labelled by their last communication, may be viewed as Labelled ESs whose
observable behaviour (the communications) is deterministic. Hence, such
extensional g-PESs could be characterised by the trace language they
recognise333Here,“trace” should be intended as a Mazurkiewicz trace, namely as
an equivalence class of standard traces with respect to an independence
relation $I$ on the alphabet of the language, which in our case is given by
${\sf p}{\sf q}\lambda~{}I~{}{\sf r}{\sf s}\lambda^{\prime}$ if $\\{{\sf
p},{\sf q}\\}\cap\\{{\sf r},{\sf s}\\}=\emptyset$..

### Acknowledgments.

We are grateful to the anonymous reviewers for their useful suggestions. The
first author would also like to acknowledge interesting discussions with
Nobuko Yoshida, Francisco Ferreira and Raymond Hu during her visits to Oxford
University and Queen Mary University of London in 2023.

## References

  * [1]
  * [2] Franco Barbanera, Ivan Lanese & Emilio Tuosto (2020): _Choreography Automata_.  In Simon Bliudze & Laura Bocchi, editors: Coordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, 12134, Springer, pp. 86–106, 10.1007/978-3-030-50029-0_6.
  * [3] Gérard Boudol & Ilaria Castellani (1988): _Concurrency and atomicity_.  Theoretical Computer Science 59(1-2), pp. 25–84, 10.1016/0304-3975(88)90096-5.
  * [4] Gérard Boudol & Ilaria Castellani (1988): _Permutation of transitions: an event structure semantics for CCS and SCCS_.  In J.W. de Bakker, W.-P. de Roever & G. Rozenberg, editors: REX School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Noordwijkerhout, Lecture Notes in Computer Science 354, Springer-Verlag, pp. 411–427, 10.1007/BFb0013028.
  * [5] Ilaria Castellani, Mariangiola Dezani-Ciancaglini & Paola Giannini (2023): _Event structure semantics for multiparty sessions_.  J. Log. Algebraic Methods Program. 131, p. 100844, 10.1016/j.jlamp.2022.100844.
  * [6] Ilaria Castellani & Guo Qiang Zhang (1997): _Parallel product of event structures_.  Theoretical Computer Science 179(1-2), pp. 203–215, 10.1016/S0304-3975(96)00104-1.
  * [7] Ugo de’Liguoro, Hernán C. Melgratti & Emilio Tuosto (2022): _Towards refinable choreographies_.  J. Log. Algebraic Methods Program. 127, p. 100776, 10.1016/j.jlamp.2022.100776.
  * [8] Pierre-Malo Deniélou & Nobuko Yoshida (2013): _Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types_.  In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska & David Peleg, editors: Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, Lecture Notes in Computer Science 7966, Springer, pp. 174–186, 10.1007/978-3-642-39212-2_18.
  * [9] Luc Edixhoven, Sung-Shik Jongmans, José Proença & Ilaria Castellani (2024): _Branching pomsets: Design, expressiveness and applications to choreographies_.  J. Log. Algebraic Methods Program. 136, p. 100919, 10.1016/J.JLAMP.2023.100919.
  * [10] Kohei Honda, Nobuko Yoshida & Marco Carbone (2008): _Multiparty Asynchronous Session Types_.  In George C. Necula & Philip Wadler, editors: POPL, ACM Press, New York, pp. 273–284, 10.1145/1328897.1328472.
  * [11] Kohei Honda, Nobuko Yoshida & Marco Carbone (2016): _Multiparty Asynchronous Session Types_.  Journal of ACM 63(1), pp. 9:1–9:67, 10.1145/2827695.
  * [12] Robin Milner (1980): _A Calculus of Communicating Systems_.  Lecture Notes in Computer Science 92, Springer, 10.1007/3-540-10235-3.
  * [13] Mogens Nielsen, Gordon Plotkin & Glynn Winskel (1981): _Petri Nets, Event Structures and Domains, Part I_.  Theoretical Computer Science 13(1), pp. 85–108, 10.1016/0304-3975(81)90112-2.
  * [14] Mogens Nielsen & P. S. Thiagarajan (2002): _Regular Event Structures and Finite Petri Nets: The Conflict-Free Case_.  In Javier Esparza & Charles Lakos, editors: Applications and Theory of Petri Nets 2002, 23rd International Conference, ICATPN 2002, Adelaide, Australia, June 24-30, 2002, Proceedings, Lecture Notes in Computer Science 2360, Springer, pp. 335–351, 10.1007/3-540-48068-4_20.
  * [15] Emilio Tuosto & Roberto Guanciale (2018): _Semantics of global view of choreographies_.  J. Log. Algebraic Methods Program. 95, pp. 17–40, 10.1016/j.jlamp.2017.11.002.