A Procedure for Splitting Processes
and its Application to Coordination
Sung-Shik T.Q. Jongmans

Dave Clarke

José Proença

Centrum Wiskunde & Informatica
Amsterdam, the Netherlands
jongmans@cwi.nl

IBBT-DistriNet
Department of Computer Science
Katholieke Universiteit Leuven
Leuven, Belgium
dave.clarke@cs.kuleuven.be

IBBT-DistriNet
Department of Computer Science
Katholieke Universiteit Leuven
Leuven, Belgium
jose.proenca@cs.kuleuven.be

We present a procedure for splitting processes in a process algebra with multi-actions (a subset of the
specification language mCRL2). This splitting procedure cuts a process into two processes along a
set of actions A: roughly, one of these processes contains no actions from A, while the other process
contains only actions from A. We state and prove a theorem asserting that the parallel composition
of these two processes equals the original process under appropriate synchronization.
We apply our splitting procedure to the process algebraic semantics of the coordination language
Reo: using this procedure and its related theorem, we formally establish the soundness of splitting
Reo connectors along the boundaries of their (a)synchronous regions in implementations of Reo.
Such splitting can significantly improve the performance of connectors.

1

Introduction

Over the past decades, coordination languages have emerged for the specification and implementation
of interaction protocols among entities running concurrently (components, services, threads, etc.). This
class of languages includes Reo [1], a graphical language for compositional construction of connectors:
communication mediums through which entities can interact with each other. Figure 1 shows some
example connectors in their usual graphical syntax. Intuitively, connectors consist of one or more channels, through which data items flow, and two or more nodes, on which channel ends coincide. Through
channel composition—the act of gluing channels together on nodes—engineers can construct complex
connectors. Channels often used include the reliable synchronous channel, called sync, and the reliable
asynchronous channel fifon, which has a buffer of capacity n. Importantly, while nodes have a fixed semantics, Reo features an open-ended set of channels. This allows engineers to define their own channels
with custom semantics.
To use connectors in real applications, one must derive executable code from graphical specifications
of connectors (e.g., those in Figure 1). Roughly two implementation approaches exist. In the distributed
approach, one implements the behavior of each of the k constituents of a connector and runs these k
implementations concurrently as a distributed system; in the centralized approach, one computes the
behavior of a connector as a whole, implements this behavior, and runs this implementation sequentially as a centralized system. Neither of these two approaches unconditionally predominates the other:
among other factors of influence, the hardware architecture on which to deploy the application plays
an important role. For example, in the case of a service-oriented application, the distributed approach
seems natural, because the services involved run on different machines and the network between them
This research is partly funded by the EU project FP7-231620 HATS: Highly Adaptable and Trustworthy Software using
Formal Models (http://www.hats-project.eu/)
Natallia Kokash and António Ravara (Eds.): 11th International Workshop on
Foundations of Coordination Languages and Self Adaptation (FOCLASA’12)
EPTCS 91, 2012, pp. 79–96, doi:10.4204/EPTCS.91.6

80

A Procedure for Splitting Processes and its Application to Coordination

x

d

x

a

b

b

d

d

b
(a) FIFO2

a

c

a

b

d

a

(b) LossyFIFO

x
(c) Alternator

d

y

(d) SyncFIFOSync

Figure 1: Some example connectors.
may play a role in their coordination. However, if coordination involves threads running on the same
machine in some multi-threading application, the centralized approach appears more appropriate, as it
avoids communication among the constituents of a connector at runtime: in this scenario, one dedicates
one thread to running the connector.
One optimization technique applicable to both of these approaches involves the identification of the
synchronous and the asynchronous regions of a connector. A synchronous region contains exactly those
nodes and channels of a connector that synchronize collectively to decide on their individual behavior; an
asynchronous region connects synchronous regions in an asynchronous way. For instance, the connector
consisting of a sync channel, a fifo1 channel, and another sync channel (see Figure 1d) has two synchronous regions, connected by an asynchronous region. Intuitively, two synchronous regions can run
completely indepedently of each other;1 an asynchronous regions connecting them takes care of transporting data from one synchronous region to the other. In the distributed approach, this means that nodes
and channels need to share information only with those nodes and channels in the same synchronous
region—not with every node or channel in the connector. In the centralized approach, this means that
one does not need to compute the behavior of a connector as a whole, but rather on a per-region basis.
Recent work shows that the optimization based on identifying regions can significantly improve
performance [6, 18, 19]. However, while intuitively valid, a formal argument establishing the soundness
of this optimization does not exist yet. In this paper, we present such a proof, based on the process
algebraic semantics of Reo [16, 13, 14, 15]. In this semantics, one associates every connector with a
process term describing its behavior. More concretely, we identify the following contributions:
• We introduce a splitting procedure for a subset of the specification language mCRL2 [8, 9]—the
basis of the existing process algebraic semantics of Reo—and prove its soundness.
• We formalize the notion of (a)synchronous regions in the process algebraic semantics of Reo.
• We apply this splitting procedure to the process algebraic semantics of Reo, thereby justifying
the (a)synchronous regions optimization for Reo implementations. In particular, we discuss how
we can implement and use the splitting procedure in the distributed approach, exploiting the local
concurrency available on the computational nodes.
• We lay the foundations for the definition and analysis of new splitting operations for Reo.
This paper is organized as follows. In Section 2, we give an overview of the fragment of mCRL2 that
we use. In Section 3, we summarize the process algebraic semantics of Reo. In Section 4, we introduce
our splitting procedure, and in Section 5, we apply this procedure to connectors. We conclude this paper
with future work in Section 6. See [11] for a version of this paper with an appendix including full proofs
for all the intermediary lemmas.
1 To

see this, suppose that two synchronous regions cannot run completely independently of each other. In that case, there
exist at least one constituent of the one region that synchronizes with at least one constituent of the other region. But then, these
two constituents belong to the same synchronous region—a contradiction.

S.-S.T.Q. Jongmans, D. Clarke & J. Proença

81

a
::= any element from Act
aτ ::= a | τ
α, β ::= aτ | α t β

α δ ::= α | δ
p ::= α δ | P | p + q | p · q
| pkq | pTq | p | q
| ∇V (p) | ∂B (p) | ρR (p) | ΓC (p) | TI (p)

(a) Syntax of multi-actions.

(b) Syntax of processes.

Figure 2: Syntax.

2

A Process Algebra with Multi-Actions

The process algebra considered in this work comprises the data-free and untimed fragment of mCRL2,
a specification language based on ACP [4] and the basis of the existing process algebraic semantics of
Reo. Among other useful constructs, mCRL2 has one feature that makes it particularly well-suited as
a semantic formalism for Reo, namely multi-actions: collections of actions that occur at the same time.
We postpone an explanation of how to use multi-actions for describing the behavior of connectors until
Section 3. In this section, we summarize (our subset of) mCRL2.
Figure 2a shows the syntax of multi-actions. Let Act denote the set of actions, ranged over by the
symbols a, b, c, etc. The distinguished symbol τ denotes the empty multi-action, i.e., the multi-action
consisting of no observable actions. Let the symbols aτ , bτ , cτ , etc., range over the elements in the set
Act ∪ {τ}. The operator t (commutative and associative) combines multi-actions to form larger multiactions; let MAct denote the set of all multi-actions, ranged over by α, β , γ, etc. Processes, ranged over
by p, q, r, etc., combine multi-actions using the operators shown in Figure 2b.
Basic operators The distinguished symbol—or nullary operator—δ denotes the deadlock process, i.e.,
the process performing no multi-actions. Let the symbols α δ , β δ , γ δ , etc., range over the processes
in the set MAct ∪ {δ }. The operators + and · combine processes alternatively and sequentially
in the usual way.2 Let Seq denote the set of sequential processes, which consist only of basic
operators and multi-actions. Finally, let P, Q, R, etc., denote references that refer to process
definitions of the form P 7→ p, Q 7→ q, R 7→ r, etc. For technical convenience, we currently disallow
mutual recursion: if P 7→ p, then only P can occur as a reference in p.
Parallel operators The operator k interleaves and synchronizes processes. The operator T serves as an
auxiliary operator in the axiomatization of k: it makes the process on its left-hand side perform a
multi-action, and afterwards, it combines the remaining process with the process on its right-hand
side the same way k does. The operator | synchronizes processes on the first multi-actions they
perform, and it combines the remaining processes the same way k does.
Additional operators Four additional operators constrain the behavior of processes composed in parallel. The operator ∇ restricts a process p to the multi-actions in a set of nonempty multi-actions
V ⊆ MAct \ {τ} (modulo commutativity and associativity of t). The operator ∂ blocks those actions in a process p that occur also in a set of actions B ⊆ Act. The operator ρ renames the actions
in a process p according to a set of renaming rules R ⊆ Act × Act. Finally, the operator Γ applies
the communications in a set C ⊆ MAct × Act to a process p. We write communication rules as
α → a and require that τ does not occur in α.
2 We

skip the basic operators for conditional composition and summation, because they have no meaning in the data-free
fragment of mCRL2 considered. Similarly, we skip those operators that have no meaning in the untimed fragment of mCRL2.

82

A Procedure for Splitting Processes and its Application to Coordination

Graphical syntax
a
b
a

b

a

b

a

b
d

Textual syntax

Semantics

syncha; bi

Atomically accepts an item on its source end a and dispenses it on its sink end b.

lossysyncha; bi

Atomically accepts an item on its source end a and, non-deterministically, either
dispenses it on its sink end b or loses it.

syncdrainha, b; i Atomically accepts (and loses) items on both of its source ends a and b.
fifo1ha; bi

Atomically accepts an item on its source end and stores it in its buffer, and
atomically dispenses the item d on its sink end and clears its buffer.

Figure 3: Syntax and semantics of common channels.
Abstraction operator The operator T hides those actions in a process p that occur also in a set of
actions I ⊆ Act. The act of hiding an action a, which means “replacing a by τ,” differs from the
act of blocking a, which means “replacing a by δ .”
We adopt the following usual operator precedence (in decreasing order): t, |, ·, k, T, +. We write as few
parentheses as possible, omitting them also in the case of associative or commutative operators. For
example, we write a · b · c + d + e instead of (a · (b · c)) + (d + e).
See Section A for an axiomatization of the operators discussed above.

3

Reo and its Process Algebraic Semantics

Before we continue with our splitting procedure in Section 4, we briefly discuss Reo and its process
algebraic semantics [16, 13, 14, 15]; this helps in relating the abstract discussion in Section 4 to a concrete
case. Recall from Section 1 that connectors consist of channels and nodes. Below, we outline how these
channels and nodes behave and how to describe such behavior as procesess.
Channels. Every channel has exactly two ends, each of which has one of two types: source ends
accept data, while sink ends dispense data. Besides this assumption on their number of ends, Reo makes
no assumptions about channels. This means, for example, that Reo allows channels with two source
ends. Figure 3 shows the graphical syntax of four common channels, a textual syntax, and an informal
description of their behavior. In the process algebraic semantics of Reo, one associates every channel
end with an action. For source ends, such an action represents the acceptance of data; for sink ends, it
represents the dispersal of data. By combining these actions in multi-actions, one can describe channels
that atomically accept and dispense data on their ends. For example, the following recursive process
definitions describe the behavior of the channels in Figure 3.
Syncha; bi
7→ a t b · Syncha; bi
LossySyncha; bi 7→ (a t b + a) · LossySyncha; bi

SyncDrainha, b;i 7→ a t b · SyncDrainha, b;i
Fifo1ha; bi
7→ a · b · Fifo1ha; bi

The definition Syncha; bi models synchronous flow through channel ends a and b, represented by the
multi-action a t b. The definition LossySyncha; bi models a (nondeterministic) choice between flow
through ends a and b and flow through only a, represented by the multi-action a t b + a. The definition
Fifo1ha; bi models flow through a followed by flow through b. The recursion found in each of the four
process definitions above indicates that the channels modeled by them repeat their behavior indefinitely.
In this paper, we adopt the context-insensitive process algebraic semantics of Reo, originally based
on constraint automata [2]. In context-insensitive semantic formalisms, one cannot directly describe

S.-S.T.Q. Jongmans, D. Clarke & J. Proença

83

channels and connectors whose behavior depends not only on their internal state but also on the presence
or absence of I/O operations—their context. In contrast, one can describe such channels and connectors
in semantic formalisms that do support context-sensitivity. For instance, a context-sensitive version of
lossysync should lose a data item only in the absence of I/O operations on its sink end. A context-sensitive
process algebraic semantics of Reo exists, originally based on connector coloring with three colors [5].
However, because this semantics depends on the data component of mCRL2, we do not consider it
in this paper. We remark that we could encode a context-sensitive process algebraic semantics along
the lines of [12], which makes our splitting procedure applicable also to context-sensitive channels and
connectors. For simplicity, however, we do not pursue that in this paper. See [10] for an extensive
overview of context-insensitive and context-sensitive semantic formalisms for Reo.
Nodes Entities communicating through a connector perform I/O operations—writes and takes—on its
nodes. Reo features three kinds of nodes: source nodes on which only source ends coincide, sink nodes
on which only sink ends coincide, and mixed nodes on which both kinds of channel end coincide. Nodes
have the following semantics.
• A source node n has replicator semantics. Once an entity attempts to write a data item d on n,
this node first suspends this operation. Subsequently, n notifies the channels whose source ends
coincide on n that it offers d. Once each of these channels has notified n that it accepts d, n resolves
the write: atomically, n dispenses d to each of its coincident source ends.
• A sink node n has nondeterministic merger semantics. Once an entity attempts to take a data item
from n, this node first suspends this operation. Subsequently, n notifies the channels whose sink
ends coincide on n that it accepts a data item. Once at least one of these channels has notified n that
it offers a data item, n resolves the take: atomically, n fetches this data item from the appropriate
channel end and dispenses it to the entity attempting to take. If multiple sink ends offer a data
item, n chooses one of them nondeterministically.
• A mixed node n has pumping station semantics: a combination of the replicator semantics and
merger semantics discussed above, where fetching and dispensing occurs atomically.
In the process algebraic semantics of Reo, one associates each of the m source ends of a node with
an action src1≤i≤m and each of its n sink ends with an action snk1≤i≤n . Then, one can describe nodes by
combining the processes for a binary replicator (one sink end to two source ends), a binary merger (two
sink ends to one source end), a one-to-one pumping station, and a process for boundary nodes:
Replicatorhsnk; src1 , src2 i 7→ snk t src1 t src2 · Replicatorhsnk; src1 , src2 i
Mergerhsnk1 , snk2 ; srci 7→ (snk1 t src + snk2 t src) · Mergerhsnk1 , snk2 ; srci
PumpingStationhsnk; srci 7→ snk t src · PumpingStationhsnk; srci
Boundaryhbndi
7→ bnd · Boundaryhbndi
Connectors. To get the behavior of a connector as a process, one composes the processes of the constituents of that connector in parallel and synchronizes their actions appropriately. Below, we give the
processes of the connectors in Figures 1a and 1c. See [16, 13, 14, 15] for more examples.
Fig1a = ∂{a1 ,a1 ,x1 ,x1 ,x2 ,x2 ,b1 ,b1 } (Γ{a1 ta1 →a,x1 tx1 →x,x2 tx2 →x,b1 tb1 →b} (
Boundaryha1 i k Fifo1ha1 ; x1 i k PumpingStationhx1 ; x2 i k Fifo1hx2 ; b1 i k Boundaryhb1 i))
Fig1c = ∂{∗bnd ,∗bnd ,∗i ,∗i |∗∈{a,b,c}∧i∈{1,2}} (Γ{∗bnd t∗bnd t∗i t∗i →∗|∗∈{a,b,c}∧i∈{1,2}} (
Boundaryhabnd i k Replicatorhabnd ; a1 , a2 i k Boundaryhbbnd i k Replicatorhbbnd ; b1 , b2 i k
SyncDrainha2 ; b2 i k Syncha1 ; c1 i k Fifo1hb1 ; c2 i k Mergerhc1 , c2 ; cbnd i k Boundaryhcbnd i))

84

4

A Procedure for Splitting Processes and its Application to Coordination

Splitting Processes

Recall from Section 1 that we aim at establishing the validity of optimizing implementations of Reo
through the identification of (a)synchronous regions. Essentially, we want to show that splitting connectors along the boundaries of their (a)synchronous regions (and running the resulting subconnectors
concurrently) does not give rise to inadmissible behavior. In this section, we lay the foundation for this
kind of splitting in terms of a splitting procedure for processes. Later, in Section 5, we apply this procedure to the process algebraic semantics of Reo, thereby justifying the splitting of connectors. Here, we
start by explaining the intuition behind our splitting procedure; formal definitions appear in Section 4.1,
followed by theorems and proofs in Section 4.2. We note that our notion of “splitting” differs from
“decomposition” in the spirit of [17]: in our context, primality or uniqueness do not matter.
Let Acts(p) denote the set of actions occurring in a process p. We introduce the function split, which
splits a process p along a set of actions A into two processes: one of these processes contains no actions in
Acts(p) \ A, while the other process contains no actions in A. We call the former process the A-isolation
of p and the latter process the A-coisolation of p. We aim at constructing p’s isolation and its coisolation
such that their parallel composition equals p under appropriate synchronization. Informally, to construct
p’s A-isolation, replace every action in p as follows:
• If a ∈ A, replace a with the multi-action a t ξ(a), where ξ(a) denotes a fresh action with respect
to Acts(p). Intuitively, ξ(a) represents the act of “disseminating that this process performs a.”
• If b ∈
/ A, replace b with the action ξ(b), where ξ(b) denotes a fresh action with respect to Acts(p).
Intuitively, ξ(b) represents the act of “discovering that another process performs b.”
Symmetrically, to construct the A-coisolation of a process p, replace in p every b ∈ A with ξ(b) and
every b ∈
/ A with b t ξ(b). Note that because the foregoing affects only multi-actions, p’s isolation and
its coisolation have the same structure as p. In other words: the process p, its isolation, and its coisolation
have the same transition system modulo transition labels.
To illustrate isolation and coisolation, consider the process q = a · b as a running example. This process has q1 = a t ξ(a) · ξ(b) as its {a}-isolation and q2 = ξ(a) · b t ξ(b) as its {a}-coisolation. However,
the parallel composition of q1 and q2 is not equal to q yet: to ensure that a process equals the parallel
composition of its isolation and its coisolation, these latter two processes should synchronize on ξ(a)
and ξ(a) for each a. To this end, we apply the communication operator Γ to such compositions. In our
running example, this yields the process ΓC (q1 k q2 ) with C = {ξ(a) t ξ(a) → tau , ξ(b) t ξ(b) → tau}.
The special action tau serves as a placeholder action for τ, and we can hide it immediately using the
abstraction operator T;3 henceforth, without loss of generality, we assume tau ∈
/ Acts(p) for each p.
In our running example, this yields the process TI (ΓC (q1 k q2 )) with I = {tau} and C as before. But
also this process is not equal to q yet: only synchronization and abstraction do not suffice—we must also
block those actions whose performance in isolation “makes no sense.” For instance, we consider every
unpaired occurrence of ξ(a) in a multi-action α nonsensical: intuitively, performing ξ(a) suggests that
some process discovers that another process performs a, even though this does not happen (otherwise,
also ξ(a) would occur in α). By symmetry, we consider also every unpaired occurrence of ξ(a) nonsensical. To block unpaired occurrences of ξ(a) and ξ(a), we apply the blocking operator ∂. In our running
example, this yields the process ∂B (TI (ΓC (q1 k q2 ))) with B = {ξ(a), ξ(a), ξ(b), ξ(b)} and I and C as
before. This process equals q.
3 We

use this construction, because mCRL2 does not permit communications to map directly to τ.

S.-S.T.Q. Jongmans, D. Clarke & J. Proença

85

dom(Ξ) = dom(ξw ) ∩ dom(ξ w )
img(Ξ) = img(ξw ) ∪ img(ξ w )
comm(Ξ) = {ξw (a) t ξ w (a) → tau | (a, w) ∈ dom(Ξ)}

Q1 ?Ξ (τ) ' τ
Q2 ?Ξ (δ ) ' δ
Q3 ?Ξ (p + q) ' ?Ξ (p) + ?Ξ (q)
Q4 ?Ξ (p · q) ' ?Ξ (p) · ?Ξ (q)

Figure 4: Auxiliary functions for substitution environments.

Figure 5: Axioms for ?.

isolΞ (a, A, w) = a t ξw (a) if a ∈ A
isolΞ (b, A, w) = ξ w (b)
if b ∈
/A

isol Ξ (a, A, w) = ξ w (a)
if a ∈ A
isol Ξ (b, A, w) = b t ξw (b) if b ∈
/A

c Ξ (ϑ , A, w)
isol
=ϑ
for ϑ ∈ {τ, δ }
c
c
c
isol Ξ (p ⊕ q, A, w) = isol Ξ (p, A, w) ⊕ isol Ξ (q, A, w)
for ⊕ ∈ {·, t}
c
c
c
isol Ξ (p + q, A, w) = isol Ξ (p, A, w1) + isol Ξ (q, A, w2)
c ∈ {isol, isol}.
Figure 6: The functions isol and isol. Let p ∈ Seq and isol

4.1

Formal Definitions

We proceed with formal definitions of the splitting procedure outlined above. We start with a formal
account of the fresh auxiliary actions of the form ξ(a) and ξ(a). As suggested by this notation, ξ and
ξ denote functions that take an action a as their input and produce another action as their output. We
collect such pairs of functions in substitution environments as follows. Let {1, 2}∗ denote the set of finite
strings over {1, 2}, ranged over by w, v, u, etc.
Definition 1. A substitution environment, typically denoted by Ξ, is a quintuple (Ṗ 7→ ṗ, A, tau, ξ, ξ)
consisting of a process definition Ṗ 7→ ṗ, a set A ⊆ Act, an action tau ∈ Act \ A and injective functions
ξ, ξ : A × {1, 2}∗  Act \ (A ∪ tau) such that img(ξ) ∩ img(ξ) = 0.
/
Henceforth, we write ξw (a) and ξ w (a) instead of ξ(a, w) and ξ(a, w). Note that we dropped the w
subscripts in our running example above: as we did not need this extra string of information, we omitted
it for simplicity. In the general case, however, this information plays a key role, as explained shortly. The
process definition in a substitution environment represents the main process to be split.
Figure 4 shows auxiliary functions for substitution environment. The functions “dom” and “img”
map substitution environments to their domain and image. The function “comm” maps substitution
environments to communications derivable from them.
To formalize the notions of A-isolation and A-coisolation, we introduce the functions isol and isol.
Figure 6 shows their definitions. The functions isol and isol take for arguments a sequential process, a
set of actions A ⊆ Act, a string w ∈ {1, 2}∗ , and a substitution environment (as a subscript for notational
convenience). For most processes p, isolΞ (p, A, w) and isol Ξ (p, A, w) invoke themselves recursively on
p’s immediate subprocesses, the same set A, and the same string w. One exception exists: processes of
the form p + q. For such processes, isol and isol invoke themselves recursively on w1 and w2 instead
of w. This ensures that in their parallel composition, the process isolΞ (p + q, A, w) can “track” which
choice the process isol Ξ (p + q, A, w) makes and vice versa.
To clarify this, let us illustrate what would happen if isolΞ (p + q, A, w) and isol Ξ (p + q, A, w) invoke
themselves recursively without changing w. In that case, w has no influence on the behavior of isol and
isol, and we can omit it from our definitions. Now, suppose that we want to compose the {a}-isolation

86

A Procedure for Splitting Processes and its Application to Coordination

and {a}-coisolation of the process r = a · b + a · c in parallel. We have:
isolΞ (r, {a}) =
a t ξ(a) ·
ξ(b) + a t ξ(a) · ξ(c)
isol Ξ (r, {a}) = ξ(a) · b t ξ(b) +
ξ(a) · c t ξ(c)
Thus, the process isolΞ (r, {a}) can erroneously synchronize its left-most multi-action a t ξ(a) with the
right-most multi-action ξ(a) of the process isol Ξ (r, {a}). By changing w in the recursive invocations of
isolΞ (p + q, A, w) and isol Ξ (p + q, A, w), this problem does not arise: it ensures that a t ξw1 (a) (on the
left) can synchronize only with ξ w1 (a) (also on the left)—not with ξ w2 (a) (on the right). Note that this
depends on the injectivity of ξ and ξ (see Definition 1).
The definition of the function split follows straightforwardly now that we have the functions isol
and isol. We also introduce an auxiliary operator, denoted by ?, which encapsulates the communication,
hiding, and blocking necessary to get equality of processes. Figure 5 shows axioms for this operator.4
Definition 2. ?Ξ (p) = ∂img(Ξ) (T{tau} (Γcomm(Ξ) (p)))
Definition 3. For all Ξ = (Ṗ 7→ ṗ, A, tau, ξ, ξ) such that Acts(p) ⊆ A,

?Ξ (isolΞ (p, A, w) k isol Ξ (p, A, w)) if p ∈ Seq



splitΞ (p1 , A, w) ⊕ splitΞ (p2 , A, w) if p ∈
/ Seq and p = p1 ⊕ p2 and ⊕ ∈ {·, +, k, T, |}
splitΞ (p, A, w) =
†(split
(p
,
A,
w))
if
p
=
†(p1 ) and † ∈ {∇V , ∂B , ρR , ΓC , TI }

1
Ξ


SPLITΞ (Ṗ, A, w)
if p = Ṗ
where SPLITΞ (Ṗ, A, w) denotes a reference to the process splitΞ ( ṗ, A, w).

4.2

Theorems

Suppose an execution environment Ξ = (Ṗ 7→ ṗ, A, tau, ξ, ξ). We prove that splitting ṗ as described
above yields a process equal to ṗ. We proceed in three steps. First, we prove our result for multi-actions.
Then, we extend this result to sequential processes. Finally, we establish it for general processes. In each
of these theorems we restrict our attention to syntactically τ-free specifications, because we work under
strong bisimulation. Under equivalences weaker than strong bisimulation, we can relax this τ-freeness.
The axioms occasionally referred to in the remainder of this section appear in Figure 11, Section A.
4.2.1

A theorem for multi-actions

We start with a theorem for multi-actions, which states that splitting a syntactically τ-free multi-action
equals that multi-action. Let τ-free(α) denote that τ does not occur in α (see [11] for a formal definition).
Theorem 1. For all Ξ = (Ṗ 7→ ṗ, A, tau, ξ, ξ) such that Acts(α) ∪ A ⊆ A,
τ-free(α) implies splitΞ (α, A, w) ' α
To prove this theorem, we need some auxiliary lemmas. We formulate these lemmas below; detailed proofs, as well as additional propositions on which these proofs rely, appear in [11]. The first
lemma states that the parallel composition of the isolation and the coisolation of a process equals their
synchronous composition (after applying communication, hiding, and blocking).
Lemma 1. For all Ξ = (Ṗ 7→ ṗ, A, tau, ξ, ξ) such that Acts(p) ∪ A ⊆ A,


τ-free(p) and p ∈ Seq implies
?Ξ (isolΞ (p, A, w) k isol Ξ (p, A, w)) ' ?Ξ (isolΞ (p, A, w) | isol Ξ (p, A, w))
4 The axiom Q1 follows from the axioms C1, H1, and B1 in Figure 11 in Section A; Q2 follows from C2, H5, and B5; Q3
follows from C3, H6, and B6; Q4 follows from C4, H7, and B7.

S.-S.T.Q. Jongmans, D. Clarke & J. Proença

87

Proof (sketch). By the axioms M and A6, we must show that ?Ξ (isolΞ (p, A, w) T ?Ξ (isol Ξ (p, A, w) and
?Ξ (isol Ξ (p, A, w) T ?Ξ (isolΞ (p, A, w) equal δ . Both of these processes start with a multi-action α δ . By
the definition of isol and isol (and, in particular, the injectivity and image-disjointness of ξ and ξ), if
α δ 6= δ , it must contain an action ξw (a) without ξ w (a) (or vice versa). But then, the blocking operator in ?
(combined with SMA) will equate α δ to δ . This suffices to show that ?Ξ (isolΞ (p, A, w) T ?Ξ (isol Ξ (p, A, w)
and ?Ξ (isol Ξ (p, A, w) T ?Ξ (isolΞ (p, A, w) equal δ by A7 (because these processes start with α δ ). See [11]
for a detailed proof.
Note that Lemma 1 involves sequential processes rather than only multi-actions. This enables us to use
this lemma also in our proof of Theorem 2, below.
The following lemma consists of two parts. The first part states that one can rewrite every multiaction composed of the isolation and the coisolation of a multi-action α into a representation with the
following characteristics: (i) for every communication βi → tau induced by the substitution environment
involved, βi occurs zero or more times; (ii) the remainder ᾰ does not contain any fragment of any βi and
vice versa, denoted as ᾰ ` βi . (See [11] for a formal definition of the latter relation.) The second part of
the following lemma states the additivity property ΓC (α t α2 ) ' ΓC (α1 ) t ΓC (α2 ) when α1 and α2 each
F
have such a representation. Let n β denote the sequence β t · · · t β of length n.
Lemma 2.
1. For all Ξ = (Ṗ 7→ ṗ, A, tau, ξ, ξ) such that Acts(α) ∪ A ⊆ A and dom(comm(Ξ)) = {β1 , . . . , βk },
isolΞ (α, A, w) t isol Ξ (α, A, w) '

n1 β1 t · · · t

F

nk βk t ᾰ

F

and ᾰ ` βi

2. For all C = {β1 → b1 , . . . , βk → bk },




F
F
α1 = n1 β1 t · · · t nk βk t ᾰ1 and ᾰ1 ` βi
ΓC (α1 t α2 ) '
F
F
implies
and α2 = m1 β1 t · · · t mk βk t ᾰ2 and ᾰ2 ` βi
ΓC (α1 ) t ΓC (α2 )
Proof (sketch).
1. If α = a, there exists a β` = ξw (a) t ξ w (a) for some `. By the definition of isol and isol, we have
that isolΞ (α, A, w) t isol Ξ (α, A, w) = β` t a. Identifying ᾰ with a, we must show that a does not
occur in any βi . This follows from the fact that ξ and ξ have disjoint domains and images by their
definition. The general case follows by structural induction.
2. Because ᾰ1 and ᾰ2 do not contain any fragment of any βi (i.e., ᾰ1 ` βi and ᾰ2 ` βi ), combining
them in the same multi-action does not make the communication operator applicable: there exists
no communication in α1 t α2 that did not exist already in α1 or in α2 .
See [11] for a detailed proof.
The following corollary follows from the previous lemma: it asserts the additivity property ΓC (α1 tα2 ) '
ΓC (α1 ) t ΓC (α2 ) for α1 = isolΞ (α, A, w) t isol Ξ (α, A, w) and α2 = isolΞ (β , A, w) t isol Ξ (β , A, w).
Corollary 1. For all Ξ = (Ṗ 7→ ṗ, A, tau, ξ, ξ) such that Acts(α) ∪ A ⊆ A,


Γcomm(Ξ) (isolΞ (α, A, w) t isol Ξ (α, A, w) t isolΞ (β , A, w) t isol Ξ (β , A, w)) '
Γcomm(Ξ) (isolΞ (α, A, w) t isol Ξ (α, A, w)) t Γcomm(Ξ) (isolΞ (β , A, w) t isol Ξ (β , A, w))
Finally, Figure 7 shows a proof of Theorem 1.

88

A Procedure for Splitting Processes and its Application to Coordination
Suppose τ-free(α) (Prem). We proceed by structural induction on α.
Base: α = aτ . If aτ = τ, we get a contradition with Prem. If aτ = a:
?Ξ (splitΞ (α, A, w))

α,aτ ,split

=

Prem→Lem. 1

'

SMA,isol,isol

'
?
=

C1,SMA

'

H4,H3,H2

'

?Ξ (isolΞ (a, A, w) k isol Ξ (a, A, w))
?Ξ (isolΞ (a, A, w) | isol Ξ (a, A, w))
?Ξ (a t ξw (a) t ξ w (a))
∂img(Ξ) (T{tau} (Γcomm(Ξ) (a t ξw (a) t ξ w (a))))
∂img(Ξ) (T{tau} (a | tau))
∂img(Ξ) (a | τ)

B4,SMA

'

atτ

MA3

'

a

aτ ,α

'

α

Step: α = α1 t α2 . Suppose that this proposition holds for α1 (IH1) and α2 (IH2).

α,split

=

Prem→Lem. 1

'

SMA,isol,isol

'
?
=

Cor. 1

'

SMA,B4,H4

'

?,SMA

'

Prem→Lem. 1

'

split

'

?Ξ (splitΞ (α, A, w))
?Ξ (isolΞ (α1 t α2 , A, w) k isol Ξ (α1 t α2 , A, w))
?Ξ (isolΞ (α1 t α2 , A, w) | isol Ξ (α1 t α2 , A, w))
?Ξ (isolΞ (α1 , A, w) t isolΞ (α2 , A, w) t isol Ξ (α1 , A, w) t isol Ξ (α2 , A, w))
∂img(Ξ) (T{tau} (Γcomm(Ξ) (
isolΞ (α1 , A, w) t isolΞ (α2 , A, w) t isol Ξ (α1 , A, w) t isol Ξ (α2 , A, w))))
∂img(Ξ) (T{tau} (
Γcomm(Ξ) (isolΞ (α1 , A, w) t isol Ξ (α1 , A, w)) t
Γcomm(Ξ) (isolΞ (α2 , A, w) t isol Ξ (α2 , A, w))))
∂img(Ξ) (T{tau} (Γcomm(Ξ) (isolΞ (α1 , A, w) t isol Ξ (α1 , A, w)))) |
∂img(Ξ) (T{tau} (Γcomm(Ξ) (isolΞ (α2 , A, w) t isol Ξ (α2 , A, w))))
?Ξ (isolΞ (α1 , A, w) | isol Ξ (α1 , A, w)) | ?Ξ (isolΞ (α2 , A, w) | isol Ξ (α2 , A, w))
?Ξ (isolΞ (α1 , A, w) k isol Ξ (α1 , A, w)) | ?Ξ (isolΞ (α2 , A, w) k isol Ξ (α2 , A, w))
?Ξ (splitΞ (α1 , A, w)) | ?Ξ (splitΞ (α2 , A, w))

IH1,IH2

'

α1 | α2

SMA

'

α1 t α2

α

=

α

Figure 7: Proof of Theorem 1
4.2.2

Theorems for processes

The following theorem generalizes Theorem 1 from multi-actions to processes in Seq: it states that
splitting such a syntactically τ-free process equals that process.
Theorem 2. For all Ξ = (Ṗ 7→ ṗ, A, tau, ξ, ξ) such that Acts(p) ∪ A ⊆ A,


τ-free(p) and p ∈ Seq implies splitΞ (p, A, w) ' p
As for Theorem 1, we need some auxiliary lemmas to prove this theorem. We formulate these lemmas
below; proofs, as well as additional propositions on which these proofs rely, appear in [11]. The first
lemma states the additivity property ?Ξ (r1 | r2 ) = ?Ξ (r1 ) | ?Ξ (r2 ) when r1 and r2 denote the isolation and
the coisolation of the processes p and q. Importantly, while p and q may denote the same process, their
isolation and coisolation must involve different strings over {1, 2} for the additivity to hold.
Lemma 3. For all Ξ = (Ṗ 7→ ṗ, A, tau, ξ, ξ) such that Acts(p) ∪ Acts(q) ∪ A ⊆ A,


τ-free(p) and τ-free(q) and p, q ∈ Seq and w 6= v implies
?Ξ (isolΞ (p, A, w) | isol Ξ (q, A, v)) ' ?Ξ (isolΞ (p, A, w)) | ?Ξ (isol Ξ (q, A, v))

S.-S.T.Q. Jongmans, D. Clarke & J. Proença

89

Proof (sketch). The actions occurring in isolΞ (p, A, w) differ from those occurring in isolΞ (q, A, v) (except
for the original actions in p and q) because ξ and ξ have disjoint images by their definition and because
w 6= v. In that case, there exists no communication in isolΞ (p, A, w) | isol Ξ (p, A, w) that did not exist
already in isolΞ (p, A, w) or in isol Ξ (p, A, w), enabling one to distribute Γ in ? among them. We can do
the same for T and ∂ in ? (by B4 and H4). See [11] for a detailed proof.
The following lemma states that the process ?Ξ (r) deadlocks when r denotes only the isolation or only
the coisolation of a process p.
Lemma 4. For all Ξ = (Ṗ 7→ ṗ, A, tau, ξ, ξ) such that Acts(p) ∪ A ⊆ A,




τ-free(p) and p ∈ Seq implies ?Ξ (isolΞ (p, A, w)) ' δ and ?Ξ (isol Ξ (p, A, w)) ' δ
Proof (sketch). Similar to the proof sketch of Lemma 1. See [11] for a detailed proof.
Suppose that we have two sequential processes, namely r1 = isolΞ (p, A, w) · isolΞ (q, A, w) and r2 =
isol Ξ (p, A, w) · isol Ξ (q, A, w). Moreover, suppose that we take their parallel composition r1 k r2 . Our final
lemma states that instead of taking this parallel composition, one can compose the parallel composition
r] = isolΞ (p, A, w) | isol Ξ (p, A, w) and the parallel composition r[ = isolΞ (q, A, w) | isol Ξ (q, A, w) sequentially and get the same process. In short: r] · r[ equals r1 k r2 .
Lemma 5. For all Ξ = (Ṗ 7→ ṗ, A, tau, ξ, ξ) such that Acts(p) ∪ A ⊆ A,


τ-free(p) and p ∈ Seq implies
?Ξ ((isolΞ (p, A, w) · isolΞ (q, A, w)) k (isol Ξ (p, A, w) · isol Ξ (q, A, w))) '
?Ξ (isolΞ (p, A, w) k isol Ξ (p, A, w) · isolΞ (q, A, w) k isol Ξ (q, A, w))
Proof (sketch). The processes isolΞ (p, A, w) and isol Ξ (p, A, w) always stay “synchronized” when composed in parallel due to the ? operator. This implies that these processes “finish” at the same time.
Consequently, isolΞ (q, A, w) and isol Ξ (q, A, w) start at the same time, which implies the desired result.
See [11] for a detailed proof.
Finally, Figure 8 shows a proof of Theorem 2. Our last theorem generalizes Theorem 2 from sequential
processes to parallel processes; Figure 9 shows a proof.
Theorem 3. For all Ξ = (Ṗ 7→ ṗ, A, tau, ξ, ξ) such that Acts(p) ∪ A ⊆ A,
τ-free( ṗ) implies splitΞ ( ṗ, A, w) ' ṗ

5
5.1

Application: Splitting Connectors
Formalization of (A)synchronous Regions

We provide a formal definition of the synchronous regions of a connector, based on the mCRL2 semantics
of Reo. Let p denote a process describing the behavior of a Reo connector, and let −→ denote its
transition relation (labeled with multi-actions). Recall that every action in p represents a channel end or
a node end. Let a ∈ Acts(p) denote one such an end. We define the a-synchronous region of p as the
smallest set Xa ⊆ Acts(p) such that:
• a ∈ Xa .
β

• If b ∈ Xa then Acts(β ) ⊆ Xa for all β such that q −
→ q0 and b ∈ Acts(β ).

90

A Procedure for Splitting Processes and its Application to Coordination


Suppose τ-free(p) and p ∈ Seq (Prem). We have:
splitΞ (p, A, w)

split

?Ξ (isolΞ (p, A, w) k isol Ξ (p, A, w))

=

Prem→Lem. 1

'

?Ξ (isolΞ (p, A, w) | isol Ξ (p, A, w))

Denote this property by Obs. We proceed by structural induction on p.
Base: p = α δ . If α δ = α, the theorem follows by Theorem 1. If α δ = δ :
Obs,p

splitΞ (p, A, w)

=

?Ξ (isolΞ (δ , A, w) | isol Ξ (δ , A, w))

isol,isol

=

?Ξ (δ | δ )

S4,Q2

'

α δ ,p

=

δ

p

Step: p = p1 ⊕ p2 with ⊕ ∈ {+, ·}. Suppose that this theorem holds for p1 (IH1) and p2 (IH2).
Case: p = p1 + p2 .
splitΞ (p, A, w)
Obs,p

'

isol,isol

=
S7

'
Q3

'
Obs

'

Prem→Lem. 3

'

Prem→Lem. 4

'

?Ξ (isolΞ (p1 + p2 , A, w) | isol Ξ (p1 + p2 , A, w))
?Ξ ((isolΞ (p1 , A, w1) + isolΞ (p2 , A, w2)) | (isol Ξ (p1 , A, w1) + isol Ξ (p2 , A, w2)))
?Ξ (isolΞ (p1 , A, w1) | isol Ξ (p1 , A, w1) + isolΞ (p1 , A, w1) | isol Ξ (p2 , A, w2) +
isolΞ (p2 , A, w2) | isol Ξ (p1 , A, w1) + isolΞ (p2 , A, w2) | isol Ξ (p2 , A, w2))
?Ξ (isolΞ (p1 , A, w1) | isol Ξ (p1 , A, w1)) + ?Ξ (isolΞ (p1 , A, w1) | isol Ξ (p2 , A, w2)) +
?Ξ (isolΞ (p2 , A, w2) | isol Ξ (p1 , A, w1)) + ?Ξ (isolΞ (p2 , A, w2) | isol Ξ (p2 , A, w2))
?Ξ (splitΞ (p1 , A, w1)) + ?Ξ (isolΞ (p1 , A, w1) | isol Ξ (p2 , A, w2)) +
?Ξ (isolΞ (p2 , A, w2) | isol Ξ (p1 , A, w1)) + splitΞ (p2 , A, w2)
splitΞ (p1 , A, w1) + ?Ξ (isolΞ (p1 , A, w1)) | ?Ξ (isol Ξ (p2 , A, w2)) +
?Ξ (isolΞ (p2 , A, w2)) | ?Ξ (isol Ξ (p1 , A, w1)) + splitΞ (p2 , A, w2)
splitΞ (p1 , A, w1) + δ | δ + δ | δ + splitΞ (p2 , A, w2)

IH1,IH2,S4,A6

'

p1 + p2

p

'

p

Case: p = p1 · p2 .
p,split

=

isol,isol

=

Prem→Lem. 5

'
Q4

'
split

'

splitΞ (p, A, w)
?Ξ (isolΞ (p1 · p2 , A, w) k isol Ξ (p1 · p2 , A, w))
?Ξ ((isolΞ (p1 , A, w) · isolΞ (p2 , A, w)) k(isol Ξ (p1 , A, w) · isol Ξ (p2 , A, w)))
?Ξ (isolΞ (p1 , A, w) k isol Ξ (p1 , A, w) · isolΞ (p2 , A, w) k isol Ξ (p2 , A, w))
?Ξ (isolΞ (p1 , A, w) k isol Ξ (p1 , A, w)) · ?Ξ (isolΞ (p2 , A, w) k isol Ξ (p2 , A, w))
splitΞ (p1 , A, w) · splitΞ (p2 , A, w)

IH1,IH2

'

p1 · p2

p

'

p

Figure 8: Proof of Theorem 2.
β

β0

• If b ∈ Xa then Acts(β 0 ) ⊆ Xa for all β , β 0 such that q −
→ q0 and q −
→ q00 and b ∈ Acts(β ).
The second rule states that all the ends that occur in the same multi-action belong to the same synchronous region. The third rule states that all the ends that can have flow in some state q, but possibly
in different transitions leaving q, belong to the same synchronous region. In that case, channel ends may
exclude each other from flow, which requires them to synchronize and communicate about their behavior.
To exemplify the previous definition, consider the connector modeled by the process p = a t b · c + d.
Informally, either this connector has flow through a and b, followed by flow through c, or it has flow
through d. We construct its a-synchronous region starting from the singleton set Xa = {a} (first rule).
Subsequently, due to the multi-action a t b, we add b to this set (second rule). The transition system of
p contains a state with two outgoing transitions: one labeled by a t b, the other labeled by d. Hence,
because a ∈ Xa , we add d to Xa (third rule). This concludes the construction: Xa = Xb = Xd = {a, b, d}.

S.-S.T.Q. Jongmans, D. Clarke & J. Proença

91

First, we prove splitΞ (p, A, w) ' p[SPLITΞ (Ṗ, A, w)/Ṗ] for all p such that τ-free(p) and in which only Ṗ
occurs as a reference (Prem), where p[Q/R] denotes the syntactic substitution of the process reference Q for
the process reference R in p, by structural induction on p.
Base: p ∈ Seq or p = Ṗ. If p ∈ Seq, this theorem follows by Theorem 2. If p = Ṗ:
splitΞ (p, A, w)

p

=
[Q/R]

=

splitΞ (Ṗ, A, w)

split

=

Ṗ[SPLITΞ (Ṗ, A, w)/Ṗ]

SPLITΞ (Ṗ, A, w)
p

=

p[SPLITΞ (Ṗ, A, w)/Ṗ]

Step: p = p1 ⊕ p2 or p = †(p1 ) for ⊕ ∈ {·, +, k, T, |} and † ∈ {∇V , ∂B , ρR , ΓC , TI }. Suppose that this lemma
holds for p1 (IH1) and p2 (IH2). We proceed by case distinction.
Case: p = p1 ⊕ p2 .
splitΞ (p)

p

=
IH1,IH2

'

[Q/R]

=

splitΞ (p1 ⊕ p2 )

split

=

splitΞ (p1 ) ⊕ splitΞ (p2 )

p1 [SPLITΞ (Ṗ, A, w)/Ṗ] ⊕ p2 [SPLITΞ (Ṗ, A, w)/Ṗ]
p

(p1 ⊕ p2 )[SPLITΞ (Ṗ, A, w)/Ṗ]

=

p[SPLITΞ (Ṗ, A, w)/Ṗ]

Case: p = †(p1 ).
splitΞ (p)

p

=
IH1

'

[Q/R]

=

splitΞ (†(p1 ))

split

=

† (splitΞ (p1 ))

†(p1 [SPLITΞ (Ṗ, A, w)/Ṗ])
†(p1 )[SPLITΞ (Ṗ, A, w)/Ṗ]

p

=

p[SPLITΞ (Ṗ, A, w)/Ṗ]

Recall Ṗ 7→ ṗ (such that only Ṗ occurs as a process reference in ṗ—see Section 2) and SPLITΞ (Ṗ, A, w) 7→
splitΞ ( ṗ, A, w). To establish the equality of ṗ and splitΞ ( ṗ, A, w), i.e., ṗ[SPLITΞ (Ṗ, A, w)/Ṗ], we must show
that there exists a process operator Φ of which Ṗ and SPLITΞ (Ṗ, A, w) are fixed points (see also Section 9.6
in [9]). Let Φ = λ Z • ṗ[Z/Ṗ]. It follows that Ṗ = Φ Ṗ and that SPLITΞ (Ṗ, A, w) = Φ SPLITΞ (Ṗ, A, w).

Figure 9: Proof of Theorem 3
We define the set of the synchronous regions of the connector modeled by a process p as
S
X = a∈Acts(p) {Xa }
and the set containing its asynchronous regions as
Y = {(a, b) | connected(a, b) and a ∈ X and b ∈ X 0 and X 6= X 0 and X, X 0 ∈ X },
where connected(a, b) denotes that the ends a and b belong to the same channel.

5.2

Splitting Connectors

We set out to establish the soundness of splitting connectors along the boundaries of their (a)synchronous
regions. However, we can split any (syntactically τ-free) process along any set of actions by Theorem 3.
This suggests that regardless of its (a)synchronous regions, one can split a connector in any possible way
and preserve its original semantics. While true in theory, there is a catch for implementations of splitted connectors in practice: the parallel composition of the isolation and the coisolation of a connector
process must synchronize, represented by the ? operator in Definition 3. Depending on the particular implementation approach, which in turn may depend on the underlying hardware architecture (see
Section 1), performing ? at run-time may cost an unreasonable amount of resources, if possible at all.
Next, we demonstrate that arbitrary splitting, therefore, makes no sense in practice despite its theoretical
validity. Splitting based on (a)synchronous regions, in contrast, does.

92

A Procedure for Splitting Processes and its Application to Coordination

We start with an example of splitting based on (a)synchronous regions. Suppose that we split
fifo1ha, bi into two parts: one part contains only a, while the other part contains only b. Recall from Section 3 that the semantics of this channel is given by the process definition Fifo1ha; bi 7→ a · b · Fifo1ha; bi.
Splitting along {a} (or equivalently, along {b}) yields:
SPLITΞ (Fifo1ha; bi, {a}, ε) 7→ splitΞ (a · b · Fifo1ha; bi, {a}, ε)
= splitΞ (a · b, {a}, ε) · splitΞ (Fifo1ha; bi, {a}, ε)
= ?Ξ (a t ξε (a) ·
ξ ε (b) k
ξ ε (a) · b t ξε (b) ) · SPLITΞ (Fifo1ha; bi, {a}, ε))
with Ξ = (Fifo1ha; bi 7→ a · b · Fifo1ha; bi, {a, b}, tau, ξ, ξ). Here, ? represents the asynchronous region
of fifo1ha; bi. Suppose that we want to implement p = atξε (a)·ξ ε (b) and q = ξ ε (a)·btξε (b) such that,
when run in parallel, they behave as a · b. These implementations should perform the synchronization
implied by ?. Recall from Section 4 that intuitively, ξε (a) represents the act of “disseminating the
performance of a,” while ξ ε (a) represents the act of “discovering the performance of a.” Thus, the
implementation of p should: (1) accept data on a and disseminate this acceptance, and (2) discover the
dispersal of data on b. Meanwhile, the implementation of q should: (1) discover the acceptance of data
on a, and (2) dispense data on b and disseminate this dispersal. Thus, in each step, the implementations
of p and q require only unidirectional communication about their behavior to synchronize: first, the
implementation of p performs ξε (a) and the implementation of q takes notice of this (by performing
ξ ε (a)); afterwards, p and q switch roles to perform ξ ε (b) and ξε (b). This shows that synchronous regions
can decide on their behavior independently of each other: the region {a} does not need to know that the
region {b} dispenses data before it can accept data—it can decide to do so without communication.
In practice, this can yield performance improvements: although the isolation and the coisolation of
a process p have the same transition system modulo transition labels, benefits can arise if one composes
them in parallel with another split process q. In that case, there may exist a transition t of the (co)isolation
of p that can proceed independently—without communication among the ends involved—of a transition
t 0 of the (co)isolation of q. Without splitting, in contrast, communication among those ends must always
take place to decide on whether to behave according to t, t 0 , or both. For instance, if we put two split
fifo1 instances in sequence (as in Figure 1a), the source end a of the first fifo1 can proceed independently
of the sink end b of the second fifo1. This means that, if empty, the first fifo1 can accept a data item on a
(and place it in its buffer) without communicating with b. Similarly, if full, the second fifo1 can dispense
a data item on b (and remove it from its buffer) without communicating with a. In contrast, if we put two
unsplit fifo1 instances in sequence, the source end a and the sink end b communicate with each other to
decide on their joint behavior, even though the behavior of those ends does not depend on each other. By
splitting, one avoids this unnecessary communication, reducing resource consumption at runtime.
To demonstrate that splitting arbitrarily makes no sense, suppose that we split syncha, bi into two
parts: one part contains only a, while the other part contains only b. Recall from Section 3 that the
semantics of this channel is given by the process definition Syncha; bi 7→ a t b · Syncha; bi. Splitting
along {a} (or equivalently, along {b}) yields:
SPLITΞ (Syncha; bi, {a}, ε) 7→ splitΞ (a t b · Syncha; bi, {a}, ε)
= splitΞ (a t b, {a}, ε) · splitΞ (Syncha; bi, {a}, ε)
= ?Ξ (a t ξε (a) t
ξ ε (b) k
ξ ε (a) t b t ξε (b) ) · SPLITΞ (Syncha; bi, {a}, ε)
with Ξ = (Syncha; bi 7→ a t b · Syncha; bi, {a, b}, tau, ξ, ξ). Now, similar to the previous example, suppose that we want to implement p = a t ξε (a) t ξ ε (b) and q = ξ ε (a) t b t ξε (b) such that, when run

S.-S.T.Q. Jongmans, D. Clarke & J. Proença

93

in parallel, they behave as a t b. As before, these implementations should perform the synchronization
implied by ?. Thus, the implementation of p should accept data on a, disseminate this acceptance, and
discover the dispersal of data on b. Meanwhile, the implementation of q should discover the acceptance
of data on a, dispense data on b, and disseminate this dispersal. All of these actions must occur at the
same time. This means that, in contrast to our previous example, the implementations of p and q must
engage in bidirectional communication with each other about the acceptance of data on a and the dispersal of data on b. This suggests that the two ends of syncha, bi must synchronize with each other—they
belong to the same synchronous region and cannot decide on their behavior independently—making it
unreasonable to split them in the first place: the communication necessary to realize the synchronization
necessary inflicts overhead, making it more attractive to run the original syncha, bi without splitting.
Depending on the hardware architecture, one can implement unidirectional communication efficiently; we sketch an implementation of the split fifo1ha, bi on a shared memory machine with multithreading. First, we instantiate two threads, A and B, for the processes p = a t ξε (a) · ξ ε (b) and
q = ξ ε (a) · b t ξε (b). Every multi-action α translates to the atomic execution of a block of code representing the actions occurring in α. We implement the action ξε (a) as setting a shared Boolean flag and
the action ξ ε (a) as waiting for the value of this flag to change. Once the latter happens, thread B unsets
the flag and knows that thread A has accepted data from a. Subsequently, it can dispense the data on b
and set another shared flag for the actions ξε (b) and ξ ε (b). In general, rather than simple Boolean flags,
threads can share more complex data structures to keep track of which actions they have performed.
Now, suppose that fifo1ha, bi constitutes some arbitrarily large connector with a distributed implementatation across multiple machines in a network. In the standard distributed approach (see Section 1),
the implementation of fifo1ha, bi has to share information with each of its neighbors in every step. We
can reduce the amount of communication necessary for this sharing (and improve performance) by using
the implementation of the split fifo1ha, bi as described above (under the assumption that the machine on
which we run this implementation features multi-threading and shared memory). The validity of doing
this follows from Theorem 3: ∂B (ΓC (· · · k Fifo1ha, bi k · · · )) ' ∂B (ΓC (· · · k SPLITΞ (Fifo1ha, bi) k · · · )).

6

Future Work

We identify three main directions for future work.
• Implementing the splitting procedure to facilitate automatic splitting of processes, as well as a tool
for the automatic detection of (a)synchronous regions of Reo connectors. Combined, they allow
us to mechanically split connectors along their (a)synchronous regions. We can then integrate this
in one of the code generation frameworks currently under development for Reo.
• Extending the splitting procedure to full mCRL2, including data and time. We see no fundamental
difficulties along this path, although we expect the technical details and proofs to involve rather
cumbersome derivations.
• Investigating other ways of splitting processes. The procedure we introduced in this paper splits
processes in a synchronous manner, meaning that the action ξw (a) occurs at the same time as the
action a itself. We imagine at least two other ways of splitting processes. In one approach, ξw (a)
occurs after a but before the next action. Then, the process q = a · b has a · ξw (a) · ξ w (b) as its
{a}-isolation (instead of a t ξw (a) · ξ w (b). In another approach, ξw (a) occurs after a but possibly
concurrently with the next action. Then, q has a · (ξw (a) k ξ w (b)) as its isolation. We spectulate
that these splitting approaches are sound only under equivalences weaker than strong bisimulation.

94

A Procedure for Splitting Processes and its Application to Coordination
This line of research seems related to existing work on delay-insensitive circuits (e.g., [20]) and
desynchronization (e.g., [3, 7]), the derivation of an asynchronous system from a synchronous
system: for the class of desynchronizable systems, the original synchronous system and the newly
constructed asynchronous system are semantically equivalent. If we use the splitting procedure
presented in our paper to obtain such an original synchronous system, we may use—perhaps with
modifications—results from desynchronization for our splitting purpose.

References
[1] Farhad Arbab (2004): Reo: a channel-based coordination model for component composition. MSCS 14(3),
pp. 329–366, doi:10.1017/S0960129504004153.
[2] Christel Baier, Marjan Sirjani, Farhad Arbab & Jan Rutten (2006): Modeling component connectors in Reo
by constraint automata. SCICO 61(2), pp. 75–113, doi:10.1016/j.scico.2005.10.008.
[3] Harsh Beohar & Pieter Cuijpers (2010): A theory of desynchronisable closed loop systems. EPTCS 38(1),
pp. 99–114, doi:10.4204/EPTCS.38.10.
[4] Jan Bergstra & Jan Willem Klop (1984): Process Algebra for Synchronous Communication. Information and
Control 60(1–3), pp. 109–137, doi:10.1016/S0019-9958(84)80025-X.
[5] Dave Clarke, David Costa & Farhad Arbab (2007): Connector colouring I: Synchronisation and context
dependency. SCICO 66(3), pp. 205–225, doi:10.1016/j.scico.2007.01.009.
[6] Dave Clarke & José Proença (2012): Partial Connector Colouring. In Marjan Sirjani, editor: Coordination
Models and Languages, LNCS 7274, Springer, pp. 59–73, doi:10.1007/978-3-642-30829-1 5.
[7] Clemens Fischer and Wil Janssen (1996): Synchronous development of asynchronous systems. In Ugo Montanari & Vladimiro Sassone, editors: CONCUR, LNCS 1119, Springer, pp. 735–750, doi:10.1007/3-54061604-7 87.
[8] Jan Friso Groote, Aad Mathijssen, Michel Reniers, Yaroslav Usenko & Muck van Weerdenburg (2007):
The Formal Specification Language mCRL2. In: Proceedings of MMOSS 2007, pp. 1–34. Available at
http://drops.dagstuhl.de/opus/volltexte/2007/862/.
[9] Jan Friso Groote & Mohammad Reza Mousavi (2010): Modelling and Analysis of Communicating Systems.
Available at http://www.win.tue.nl/~jfg/educ/2IW26/herfst2011/mcrl2-book.pdf. To appear.
[10] Sung-Shik Jongmans & Farhad Arbab (2012): Overview of Thirty Semantic Formalisms for Reo. SACS
22(1), pp. 201–251, doi:10.7561/SACS.2012.1.201.
[11] Sung-Shik Jongmans, Dave Clarke & José Proença (2012): A Procedure for Splitting Processes and its
Application to Coordination (Technical Report). Technical Report SEN-1203, CWI.
[12] Sung-Shik Jongmans, Christian Krause & Farhad Arbab (2011): Encoding Context-Sensitivity in Reo into
Non-Context-Sensitive Semantic Models. In Wolfgang de Meuter & Gruia-Catalin Roman, editors: COORDINATION, LNCS 6721, Springer, pp. 31–48, doi:10.1007/978-3-642-21464-6 3.
[13] Natallia Kokash, Christian Krause & Erik de Vink (2010): Data-Aware Design and Verification
of Service Compositions with Reo and mCRL2. In: Proceedings of SAC 2010, pp. 2406–2413,
doi:10.1145/1774088.1774590.
[14] Natallia Kokash, Christian Krause & Erik de Vink (2010): Time and Data-Aware Analysis of Graphical
Service Models in Reo. In: Proceedings of SEFM 2010, pp. 125–134, doi:10.1109/SEFM.2010.26.
[15] Natallia Kokash, Christian Krause & Erik de Vink (2010): Verification of Context-Dependent Channel-Based
Service Models. In Frank de Boer, Marcello Bonsangue, Stefan Hallerstede & Michael Leuschel, editors:
FMCO, LNCS 6286, Springer, pp. 21–40, doi:10.1007/978-3-642-17071-3 2.
[16] Natallia Kokash, Christian Krause & Erik de Vink (2012): Reo+mCRL2: A framework for model-checking
dataflow in service compositions. FAC 24(2), pp. 187–216, doi:10.1007/s00165-011-0191-6.

Appendix

95

CC (α)


CC1 (CC2 (α)) if C = C1 ∪C2 and C1 6= 0/ and C2 6= 0/
= b t CC (α \ β ) if C = {β → b} and β v α

α
otherwise
for C ⊆ MAct × Act a set of communications

n(p)


if p = α
{α}
if p ∈ {τ, δ }
= 0/

n(q) ∪ n(r) if p = q ⊕ r with ⊕ ∈ {+, ·}

⇓(V )

= {β v α | α ∈ V } \ {τ}
for V ⊆ MAct a set of multi-actions


dom(C) =

dom(C1 ) ∪ dom(C2 ) if C = C1 ∪C2 and C1 6= 0/ and C2 6= 0/
{β }
if C = {β → b}

for C ⊆ MAct × Act a set of communications

Figure 10: Auxiliary functions.
[17] Robin Milner & Faron Moller (1993): Unique decomposition of processes. TCS 107(2), pp. 357–363,
doi:10.1016/0304-3975(93)90176-T.
[18] José Proença, Dave Clarke, Erik de Vink & Farhad Arbab (2012): Dreams: a framework for distributed
synchronous coordination. In: Proceedings of SAC 2012, pp. 1510–1515, doi:10.1145/2245276.2232017.
[19] José Proença (2011): Synchronous Coordination of Distributed Components. Ph.D. thesis, Leiden University.
Available at http://hdl.handle.net/1887/17624.
[20] Jan Tijmen Udding (1984): Classification and Composition of Delay-Insensitive Circuits. Ph.D. thesis,
Eindhoven University of Technology. Available at http://repository.tue.nl/25052.

A

Axiomatization

Every process has an associated transition system describing its semantics (see [8] for the SOS rules).
Let ' denote equality of processes. Figure 11 shows a sound and complete axiomatization—for strong
bisimulation—of the operators shown in Figure 2. Figure 11b axiomatizes two additional operators on
multi-actions. Informally, the operator \ subtracts the multi-action on its right-hand side from the multiaction on its left-hand side; the operator v checks if the multi-action on its right-hand side contains the
multi-action on its left-hand side.
The axioms C1 and CL1 in Figure 11d refer to several auxiliary functions; Figure 10 shows their
definitions. The function CC applies the communications in a set C to a multi-action. The function n
maps a basic process p to its alphabet, i.e., the multi-actions that occur in p. The function ⇓ maps a set
of multi-actions V to those nonempty multi-actions contained in at least one multi-action in V . Finally,
the function dom maps a set of communications C to their domains.

96

Appendix

MA1 α t β ' β t α
MA2 (α t β ) t γ ' α t (β t γ)
MA3 α t τ ' α
A1 p + q ' q + p
A2 p + (q + r) ' (p + q) + r
A3 p + p ' p
A4 (p + q) · r ' p · r + q · r
A5 (p · q) · r ' p · (q · r)
A6 p + δ ' p
A7 δ · p ' δ

MD1
MD2
MD3
MD4
MD5

τ \α ' τ
α \τ ' α
α \ (β t γ) ' (α \ β ) \ γ
(a t α) \ a ' α
(a t α) \ b ' a t (α \ b) if a 6= b

MS1
MS2
MS3
MS4

τ v α ' true
α v τ ' false if α 6' τ
atα v atβ ' α v β
atα v btβ '
a t (α \ b) v β if a 6= b

(a) Axioms for multi-actions and for the basic operators.

M
LM1
LM2
LM3
LM4
S1
S2
S3
S4
S5
S6
S7

(b) More axioms for multi-actions.

pkq ' pTq+qT p+ p | q

V1 ∇V (α) ' α if α ∈ V ∪ {τ}
V2 ∇V (α) ' δ if α ∈
/ V ∪ {τ}

αδ T p ' αδ · p
δTp'δ
α · p T q ' α · (p k q)
(p + q) T r ' p T r + q T r

B1
B2
B3
B4

∂B (τ) ' τ
∂B (a) ' a if a ∈
/B
∂B (a) ' δ if a ∈ B
∂B (α | β ) ' ∂B (α) | ∂B (β )

R1
R2
R3
R4

ρR (τ) ' τ
ρR (a) ' b if a → b ∈ R for some b
ρR (a) ' a if a → b ∈
/ R for all b
ρR (α | β ) ' ρR (α) | ρR (β )

p|q'q| p
(p | q) | r ' p | (q | r)
p|τ ' p
αδ | δ ' δ
(α δ · p) | β δ ' α δ | β δ · p
(α δ · p) | (β δ · q) ' α δ | β δ · (p k q)
(p + q) | r ' p | r + q | r

C1 ΓC (α) ' CC (α)
CL1 ΓC (p) ' p if ⇓(n(p)) ∩ dom(C) = 0/

SMA α | β ' α t β
(c) Axioms for the parallel operators.

(d) Axioms for the additional operators.

For all † ∈ {∇V , ∂B , ρR , ΓC },
V3, B5, R5, C2 †(δ ) ' δ
V4, B6, R6, C3 †(α + β ) ' †(α) + †(β )
V5, B7, R7, C4 †(α · β ) ' †(α) · †(β )

(e) More axioms for the additional operators.

H1
H2
H3
H4
H5
H6
H7

TI (τ) ' τ
TI (a) ' τ if a ∈ I
TI (a) ' a if a ∈
/I
TI (α | β ) ' TI (α) | TI (β )
TI (δ ) ' δ
TI (α + β ) ' TI (α) + TI (β )
TI (α · β ) ' TI (α) · TI (β )

(f) Axioms for the abstraction operator.

Figure 11: Axioms.

