ELEKTROTEHNI ˇ SKI VESTNIK 88(4): 190–196, 2021
ORIGINAL SCIENTIFIC PAPER
Realizable Choreographies for Systems of
Components Communicating via Rendezvous,
Mailboxes and Letter Queues
Monika Kapus-Kolar
Joˇ zef Stefan Institute, Department of Communication Systems, Jamova 39, SI-1111 Ljubljana, Slovenia
E-mail: monika.kapus-kolar@ijs.si
Abstract. A recently proposed class of realizable compositionally speciﬁed choreographies for systems of
components communicating over ﬁrst-in-ﬁrst-out channels with exactly one channel for every source-sink pair
is generalized to systems with an arbitrary number of ﬁrst-in-ﬁrst-out channels, mailboxes and rendezvous
channels, with no restrictions on who is allowed to exchange letters on individual channels.
Keywords: choreography, semantics, realizability, pomset, communicating state machine
Izvedljive koreograﬁje za sisteme komponent, ki
komunicirajo prek sreˇ canj, poˇ stnih nabiralnikov in
pisemskih vrst
Pred kratkim predlagan razred izvedljivih kompozicijsko speci-
ﬁciranih koreograﬁj za sisteme komponent, ki komunicirajo
prek pisemskih vrst, z natanko eno vrsto za vsak par poˇ siljatelj-
prejemnik, je posploˇ sen na sisteme s poljubnim ˇ stevilom
pisemskih vrst, poˇ stnih nabiralnikov in kanalov za izmenjavo
pisem prek sreˇ canj, brez omejitev glede tega, kdo sme izme-
njevati pisma prek posameznih komunikacijskih kanalov.
1 INTRODUCTION
When designing a distributed application supposed to
run on a given distributed system, a possible way
to proceed is to ﬁrst conceive a choreography, i.e. a
model of interactions among the system components
from the global point of view. Ideally, the choreography
is realizable, i.e. component processes for its correct
implementation can be obtained simply by its projection.
The paper generalizes our recent extension [1] of the
work of Tuosto and Guanciale [2] on compositional
construction of realizable choreographies for systems in
which (1) every communication channel is between a
pair of two different components, (2) from any com-
ponent to any other component, there is exactly one
communication channel, and (3) every channel is an
initially empty, inﬁnite-capacity buffer in which mes-
sages are queued in the order of arrival and exactly the
ﬁrst in the queue is available for reception. Newly we
allow (1) any number of channels, with no restrictions
on who is allowed to use them for the exchange of
letters (i.e. triplets consisting of the identiﬁer of the
Received 6 May 2021
Accepted 24 August 2021
sender, the identiﬁer of the recipient and the message
carried), (2) besides channels with an inﬁnite-capacity
buffer also channels whose buffer capacity is zero, so
that any letter sent on it must be received in the same
event - a rendezvous of its sender and its recipient, and
(3) besides inﬁnite-capacity communication buffers with
the ﬁrst-in-ﬁrst-out (FIFO) policy also such (we call
them mailboxes) in which letters are not queued and
can be retrieved at any time.
In line with the argumentation of Tuosto and Guan-
ciale [2] that in the formal study of choreographies, it
pays to go abstract, we follow the abstract view of [1]
that a choreography is a set of partially ordered multisets
(shortly pomsets) of interactions. An interaction is an
individual exchange of a certain letter on a certain buffer
and consists of two actions: a transmission of an instance
of the letter into the buffer and its reception from the
buffer at the same or some latter point. In case of a
zero-capacity buffer, the two actions by deﬁnition occur
simultaneously, so that the interaction can be regarded
as a compound action.
With the adopted abstract approach, we deﬁne the
semantics, projection and well-formedness of choreogra-
phies in a way independent of their concrete syntax. Like
[1], [2] and also [3], in which Tuosto and Guanciale
discuss the realizability of choreographies with mailbox
communication only, we deﬁne the semantics of a given
choreography as a set of action pomsets, and component
processes obtained by projection as communicating state
machines (CSMs) [4]. Like [2] and [1], but unlike [3],
we simplify the discussion by banning choreographies
with auto-concurrency (i.e. with multiple concurrent
instances per action) and by assuming that individual
CSMs are allowed to permanently stop exactly when in
a state with no further actions deﬁned. We prove that all
well-formed choreographies are realizable.
REALIZABLE CHOREOGRAPHIES 191
The choreography composition operators introduced
as syntax sugar are the same as in [1], namely the
operators of choice, parallel composition and sequential
composition. For each of them we adapt to the gener-
alized setting the operand constraints which [1] proves
sufﬁcient for the well-formedness of the choreography
resulting from the composition.
As a ﬁnal contribution, we compare our deﬁnition
of well-formed choreographies with the conceptually
similar deﬁnitions recently proposed in [5]–[7]. Contrary
to what is allegedly proved in the three papers, we
demonstrate that (and explain why) none of the similar
deﬁnitions secures the realizability of every well-formed
choreography.
2 BASIC CONCEPTS AND NOTATIONS
2.1 (Inter)actions and Their Instances
We assume that choreographies are designed for a
system with component setC. Elements ofC are ranged
over by c.
Communication buffers, i.e. channels, are ranged over
by b. For a given buffer b, Fifo(b) denotes that it is a
FIFO channel, Mb(b) that it is a mailbox, and Rv(b)
that it is a rendezvous channel.
Messages are ranged over by m. A letter is denoted
as (c;c
0
;m) wherec is its sender,c
0
its recipient andm
its message. Letters are ranged over by l.
Interactions are ranged over by x. An interaction in
which a given letterl is exchanged over a given bufferb
is denoted as b :l, whereas its constituent transmission
and reception are denoted as b!l and b?l, respectively.
In case of Rv(b), the compound action representing a
simultaneous execution of the two constituent actions of
b :l is denoted as b!?l.
Actions, i.e. transmissions, receptions and rendezvous
regarded as compound actions, are ranged over by a,
action sequences by   , and sets of action sequences by
A. The participant set of a given action a of the form
b!(c;c
0
;m), b?(c;c
0
;m) or b!?(c;c
0
;m) is denoted as
prt(a) and deﬁned asfcg,fc
0
g orfc;c
0
g, respectively.
(Inter)action instances are alternatively called events.
Events are ranged over by e, event sets byE, and event
sequences by ".
For a given event e,   (e) denotes its label, i.e. the
(inter)action of which it is an instance. For a given action
instance sequence " = (e
i
)
i=1:::k
, asq(") denotes the
action sequence (  (e
i
))
i=1:::k
.
Interaction instances and their sets are alternatively
(to expose their nature) ranged over byg andG, respec-
tively. For a given interaction instanceg,e
!
g
denotes the
constituent transmission instance, ande
?
g
the constituent
reception instance. For a given instance g of an inter-
action b : l with Rv(b), e
!?
g
denotes the action instance
representing a simultaneous execution ofe
!
g
ande
?
g
. For
a given instance g of an interaction b : l with:Rv(b)
or Rv(b), ais(g) denotes the action instance set deﬁned
asfe
!
g
;e
?
g
g orfe
!?
g
g, respectively.
2.2 Partially Ordered Sets of (Inter)action Instances
A binary relation on a given event setE is a subset of
E E . If it is reﬂexive, anti-symmetric and transitive, it
is called partial order. The transitive closure of a given
binary relation R is denoted as R
?
.
A partially ordered set of events (shortly poset) is an
event setE endowed with a partial order  and denoted
as (E;  ). Posets are ranged over by p.
If for given posetsp = (E;  ) andp
0
= (E
0
;  0
) there
exist bijections   :E!E
0
and   0
: ! 
0
with
(1)8e2E : (  (e) =  (  (e))) and
(2)8(e;e
0
)2  : (  0
((e;e
0
)) = (  (e);  (e
0
))),
then p and p
0
are isomorphic.
For a given poset p = (E;  ), esq(p) denotes the set
of all event sequences (e
i
)
i=1:::jEj
with
(1)E =fe
i
g
i=1:::jEj
and
(2)81  i<j jEj : (e
j
6  e
i
).
For a given poset p = (E;  ), pf(p) denotes the set
of all its preﬁxes, i.e. the set of all posets (E
0
;  0
) with
(1)E
0
 E ,
(2)  0
= \ (E
0
 E
0
) and
(3) \ ((EnE
0
) E
0
) =;.
For given action instance posetp and action sequence
  , pf(p;  ) denotes the set of all posets p
0
2 pf(p)
whose esq(p
0
) comprises an event sequence " with
asq(") =  , whereas asq(p) denotes the set of all action
sequences   0
with pf(p;  0
)6=;.
2.3 Partially Ordered Multisets of (Inter)actions
A partially ordered multiset of (inter)actions (shortly
pomset) is an isomorphism class of posets. The isomor-
phism class to which a given poset p = (E;  ) belongs
is denoted as [p] or [E;  ]. Pomsets are ranged over by
r, and their sets byR.
A natural way to discuss properties of a given pomset
is to discuss properties of a representative of the class.
Likewise, a natural way to deﬁne a composition operator
for pomsets is to do it in terms of selected representatives
of individual operands, taking care that the represen-
tatives are non-intersecting (inter)action instance sets.
When discussing or combining pomset sets, one would
proceed analogously. We therefore deﬁne the following
families of pomset and pomset set representatives:
(1) For given pomset r and (possibly omitted) natural
i, po
i
(r) = (E
r;i
;  r;i
) is the poset selected as the
default representative of the class r (for the natural
i), withE
r;i
\E
r
0
;i
0 =; for every pomset r
0
and
natural i
0
with (r;i)6= (r
0
;i
0
).
(2) For given pomset setR and (possibly omitted) natu-
rali,pos
i
(R) denotes the poset setfpo
i
(r)jr2Rg.
192 KAPUS-KOLAR
For given action pomset r and action sequence   ,
pf(r;  ) denotes the set of all pomsets [p] with p 2
pf(po(r);  ). For given action pomset setR, asq(R)
denotes the union of all action sequence setsasq(p) with
p2 pos(R), whereas  R
denotes the function that for a
given action sequence   2 asq(R) returns the union of
all pomset sets pf(r;  ) with r2R.
2.4 State Machines
An initialized, initially connected and deterministic
state automaton whose individual steps represent in-
dividual actions (shortly state machine) is denoted as
(A;  ) withA the set of all action sequences executable
from the initial state, and   the function that for any
given action sequence in A returns the resulting state.
For a given state machineM = (A;  ), asq(M) denotes
A. For a given action pomset setR, sm(R) denotes the
state machine (asq(R);  R
).
2.5 Projections
For a given action a and component c2 prt(a), a  c
denotes:
(1) if a is a b!?(c;c
0
;m) then the action b!(c;c
0
;m),
(2) if a is a b!?(c
0
;c;m) then the action b?(c
0
;c;m),
(3) otherwise the action a.
For given action instance setE and componentc,E  c
denotes the set of all events e2E with c2 prt(  (e)).
For given action instance poset p = (E;  ) and compo-
nentc,p  c
denotes the poset (E  c
; \ ((E  c
)  (E  c
))).
For given action pomset set R and component c,
R  c
denotes the set of all pomsets [p  c
] with p 2
pos(R), sm
c
(R) denotes the state machine obtained
from sm(R  c
) by changing each of its actions a into
a  c
, and asq
c
(R) denotes the action sequence set
asq(sm
c
(R)). For a given action pomset setR,   (R)
denotes the set of all actions present in at least one
sequence in the set
S
c2C
asq
c
(R).
3 WELL-FORMED CHOREOGRAPHIES
3.1 Choreographies and Their Normal Form
In our simple speciﬁcation language, choreographies
are deﬁned as terms derived by the following grammar
(parentheses not necessary for disambiguation can be
omitted):
G ::=0jb :ljRj (G
1
jG
2
)j (G
1
;G
2
)j (G
1
+G
2
)
In the grammar, 0 denotes doing nothing, b : l is
assumed to be an interaction, R is assumed to be a
non-empty set of interaction pomsets, ‘j’ is the parallel
composition operator, ‘;’ is the sequential composition
operator, and ‘+’ is the choice operator.
To abstract away from the concrete syntax of chore-
ographies, we deﬁne for them a normal form. The
normal form of a given choreography G, denoted as
hhGii, is a non-empty set of interaction pomsets, with
individual pomsets representing individual alternatives
between which the system is supposed to choose when
executingG. For our six choreography types, the normal
form is deﬁned as follows:
hh0ii =f[fg;fg]g
hhb : lii =f[fgg;f(g;g)g]g with g being an instance
of b :l.
The alternatives speciﬁed by a given interaction pom-
set setR are the pomsets. Accordingly,hhRii isR itself.
The alternatives of a G
1
+G
2
are the alternatives of
G
1
and the alternatives ofG
2
. Accordingly,hhG
1
+G
2
ii
is the union ofhhG
1
ii andhhG
2
ii.
The alternatives of a G
1
jG
2
are all those deﬁned as
a parallel composition of an alternative of G
1
and an
alternative of G
2
. Accordingly,hhG
1
jG
2
ii is the set of
all pomsets[G
1
[G
2
;  1
[  2
] where(G
1
;  1
) is a poset
in pos
1
(hhG
1
ii) and (G
2
;  2
) is a poset in pos
2
(hhG
2
ii).
The alternatives of a G
1
;G
2
are all those deﬁned as
a sequential composition of an alternative ofG
1
and an
alternative of G
2
. Accordingly,hhG
1
;G
2
ii is the set of
all pomsets [G
1
[G
2
;(  1
[  2
[(G
1
 G
2
))
?
] where
(G
1
;  1
) is a poset in pos
1
(hhG
1
ii) and (G
2
;  2
) is a
poset in pos
2
(hhG
2
ii).
3.2 Choreography Semantics
For given interactions x
1
= b
1
: (c
1
;c
0
1
;m
1
) and
x
2
=b
2
: (c
2
;c
0
2
;m
2
), letOrd
1
(x
1
;x
2
) denote thatc
2
2
fc
1
;c
0
1
g. For given actions a
1
and a
2
, let Ord
2
(a
1
;a
2
)
denote that (a
1
;a
2
) is
(1) an (a;b!(c;c
0
;m)) with c2 prt(a) or
(2) an (a;b!?(c;c
0
;m)) with c2 prt(a) or
(3) a (b?l
1
;b?l
2
) with Fifo(b) or
(4) a (b?l;b?l) with Mb(b).
In the normal formhhGii of a given choreography
G, each constituent alternative of G is represented by
a pomset specifying the alternative very abstractly, in
terms of interactions. To obtain the semantics of G, we
reﬁne every pomsetr inhhGii into a pomsetr
0
specifying
the alternative of G less abstractly, in terms of actions.
To obtainr
0
, we take the interaction instance posetp that
is the default representative of the isomorphism classr,
reﬁne it into the action instance poset [[p]] below deﬁned
as the semantics of p, and set r
0
to the isomorphism
class to which [[p]] belongs. In other words, we deﬁne
that the semantics of a given choreography G, denoted
as [[G]], is the action pomset setf[[[p]]]jp2 pos(hhGii)g.
In our semantics [[p]] of a given interaction instance
poset p, each of the interaction instances is represented
by its constituent action instances, whereas the extent to
which constituents of interaction instances ordered in p
are ordered in [[p]] is selected in line with the following
assumptions which [1] implicitly makes for every spec-
iﬁed pair (g
1
;g
2
) of ordered interaction instances, with
  (g
i
) a b
i
: (c
i
;c
0
i
;m
i
) for i2f1;2g:
(1) The ordering of g
1
and g
2
means just that e
!
g2
(in
case of Rv(b
2
) a part of e
!?
g2
) is supposed to be
REALIZABLE CHOREOGRAPHIES 193
delayed with respect to e
!
g1
(in case of Rv(b
1
) a
part of e
!?
g1
).
(2) The component responsible for the delaying is c
2
.
(3) If the delaying can be implemented at c
2
, which
is in case of Ord
1
(  (g
1
);  (g
2
)), it must be imple-
mented. Otherwise, the ordering of g
1
and g
2
has
been speciﬁed unintentionally and one is supposed
to pretend that it has not been speciﬁed (at least not
explicitly, for note that there is also ordering because
of the transitivity of the ordering relation).
Formally, our semantics [[p]] of a given interaction
instance poset p = (G;  ) is an action instance poset
(E;(  1
[  2
[  3
)
?
) where
E =
S
g2G
ais(g)
  1
=f(e;e)je2Eg
  2
=f(e
!
g
;e
?
g
)j(g2G)^(ais(g) =fe
!
g
;e
?
g
g)g
  3
=f(e;e
0
)j((e;e
0
)2 
4
)^Ord
2
(  (e);  (e
0
))g
  4
=
S
((g;g
0
)2  5)^(g6=g
0
)
(ais(g)  ais(g
0
))
  5
= (f(g;g
0
)j((g;g
0
)2  )^Ord
1
(  (g);  (g
0
))g)
?
3.3 Choreography Projection, Realizability and
Reception-Completeness
The projection of a given choreography G onto a
given component c is the CSM sm
c
([[G]]). The CSM
system of a given choreographyG is considered correct
(i.e. G is considered realizable) if, starting with every
constituent CSM in the initial state and every buffer
empty, it is unable to reach a deadlock (i.e. a state in
which it cannot proceed in spite of some buffers non-
empty or some constituent CSMs in a state with further
actions deﬁned) or execute a global action sequence not
in asq([[G]]). If, in addition, the CSM system cannot
reach any state that is reception-incomplete (see below),
we say that the system and G are reception-complete.
The current system state is called reception-incomplete
if there exist a buffer b and a letter (c;c
0
;m) for which
one of the following is currently true:
(1) Rv(b) and c is ready for b!(c;c
0
;m), but c
0
is not
ready for b?(c;c
0
;m).
(2):Rv(b) and b allows immediate execution of
b?(c;c
0
;m), but c
0
is not ready for it.
3.4 Auto-Concurrency
For a given action pomset setR, letAc(R) denote the
presence of auto-concurrency, i.e. that for some poset
(E;  )2 pos(R) and event pair (e;e
0
)2E E with
  (e) =  (e
0
), neither e  e
0
nor e
0
  e is true.
Lemma 1. If a given choreography G satisﬁes
(jhhGiij = 1)^:Ac([[G]]), it is realizable and reception-
complete.
Proof: Suppose that the premise is true and consider
the CSM system of G. What G prescribes is that (1)
of any given action, the system executes exactly a
certain number of instances, and (2) action instances are
executed in a certain partial order.
Of any given action a, every component c2 prt(a)
is ready to execute exactly the prescribed number of
instances of a  c
. Hence, if G runs to completion, ev-
ery component reaches a state with no further actions
deﬁned.
For any given buffer b with:Rv(b) and letter l, the
prescribed number of instances is the same for b!l and
b?l. Hence, ifG runs to completion, every letter instance
put in a buffer is also retrieved from it.
For any given action a, by:Ac([[G]]), G prescribes
a total ordering of its instances and every component
c2 prt(a) implements a total ordering of instances of
a  c
. Hence, for any given buffer b, letter l and natural
i, one can, even if Mb(b), safely assume that the i
th
instance of b?l corresponds to the i
th
instance of b!l,
and in case of Rv(b) to the i
th
instance of b!?l.
For any prescribed direct ordering (e
1
;e
2
) of two
different action instancese
1
ande
2
, one of the following
is true:
(1)   (e
2
) is ab!(c;c
0
;m) withc2 prt(  (e
1
)), in which
case e
2
is delayed by c until after e
1
.
(2)   (e
2
) is a b!?(c;c
0
;m) with c 2 prt(  (e
1
)), in
which case the transmission instance in e
2
(and
thereby e
2
itself) is delayed by c until after e
1
.
(3) e
2
is an instance of ab?l ande
1
is the corresponding
transmission instance, in which case b delays its
support for e
2
until after e
1
.
(4) e
2
is an instance of a b?l
2
with Fifo(b) and e
1
is an instance of a b?l
1
for whose corresponding
transmission instance it is prescribed that it comes
before the one corresponding toe
2
, in which caseb
delays its support for e
2
until after e
1
.
(5) e
2
is an instance of a b?l with Mb(b) and e
1
is an
instance of b?l for whose corresponding transmis-
sion instance it is prescribed that it comes before
the one corresponding toe
2
, in which caseb delays
its support for e
2
until after e
1
.
Hence, no event is executed prematurely. Moreover, any
given component c is at any given time during the
execution of G ready for its part of any instance of a
b!?(c
0
;c;m) that is currently supported byc
0
, and for any
instance of a b?(c
0
;c;m) with:Rv(b) that is currently
supported by b, implying that the CSM system of G is
reception-complete and, hence, also deadlock-free.
3.5 Local Choice
For given non-empty action pomset setsR
1
andR
2
,
presumably two alternative sets of alternative behaviours
of the system, let Lc(R
1
;R
2
) denote that the choice
between the two sets is local, i.e. that if it is ever made
by the system, this is upon a transmission (possibly a
part of a rendezvous) executed by a preselected com-
ponent, after (or upon) which every other component
for which the two alternatives are not identical is in
time informed of the choice, upon a reception (pos-
sibly a part of a rendezvous). Formally, Lc(R
1
;R
2
)
194 KAPUS-KOLAR
denotes that there exists such a component setC
0
with
jC
0
j  1 that for every component c, action sequence
  2 (asq
c
(R
1
)\ asq
c
(R
2
)), i2f1;2g and action a
with a 2 (asq
c
(R
i
)nasq
c
(R
3  i
)), all the following is
true:
(1) There exists an action a
0
with  a
0
2 asq
c
(R
3  i
).
(2) If c2C
0
, then a is a b!(c;c
0
;m), otherwise it is a
b?(c
0
;c;m).
Lemma 2. If given realizable and reception-complete
choreographies G
1
and G
2
satisfy Lc([[G
1
]];[[G
2
]]), the
choreographyG =G
1
+G
2
is realizable and reception-
complete.
Proof: Suppose that the premise is true and consider
the CSM system of G. By the realizability of G
1
and
G
2
, the choice of a certain alternativeG
i
2fG
1
;G
2
g is
made, if ever, when a certain component c for the ﬁrst
time executes an action which at the particular point it
is ready to execute inG
i
, but not inG
3  i
. For any such
event e, one of the following is true:
(1) e is an instance of ab!(c;c
0
;m) (possibly a part of a
rendezvous). Hence,c is, by the constraint (2) in the
deﬁnition of Lc([[G
1
]];[[G
2
]]), the preselected global
selector.
(2) e is an instance of a b?(c
0
;c;m) and executed as a
part of a rendezvous e
0
in which the transmission
part is an instance e
00
of b!(c
0
;c;m). e
00
occurs at a
point when, by the reception-completeness ofG
3  i
,
c
0
is ready to execute b!(c
0
;c;m) in G
i
, but not in
G
3  i
. By the assumption thatG
i
is not selected until
upon e, the latter implies that c
0
also chooses G
i
exactly upone
0
. One can, hence, safely say that the
choice ofG
i
is actually made not byc upone, but by
c
0
upon e
00
. Moreover, by the constraint (2) in the
deﬁnition of Lc([[G
1
]];[[G
2
]]), c
0
is the preselected
global selector.
(3) e is an instance of a b?(c
0
;c;m) with:Rv(b) and
executed at a point when b?(c
0
;c;m) is allowed by
b inG
i
, but, by the reception-completeness ofG
3  i
,
not in G
3  i
. The latter, however, implies that just
beforee, the fact thatG
i
is selected in the particular
run is already evident from the current contents of
b and, hence, also from the current event history,
which contradicts the assumption that the choice is
not made until upon e.
Hence, the ﬁrst component, if any, to make the choice
of a certain G
i
2fG
1
;G
2
g is the preselected global
selector, ac. Now suppose that at some later point, some
other componentc
0
becomes the ﬁrst one to chooseG
3  i
instead, by the constraint (2) of Lc([[G
1
]];[[G
2
]]) upon
executing a certain instance e of a certain b?(c
00
;c
0
;m)
which at the particular point it is ready to execute in
G
3  i
, but not in G
i
. By the reception-completeness of
G
i
, one of the following is true:
(1) c
00
6=c and e is executed as a part of a rendezvous
whose transmission part is executed byc
00
when the
component has already selected G
3  i
.
(2) :Rv(b) ande is executed when the contents ofb is
such as currently impossible in G
i
, which can only
be because at least one component inCnfc;c
0
g has
already selected G
3  i
.
Both cases contradict the assumption that the ﬁrst com-
ponent to choose G
3  i
is c
0
. Hence, every component
chooses, if ever, the same G
i
as c. Moreover, when a
given component completes its part of G
i
, it is, by the
constraint (1) in the deﬁnition of Lc([[G
1
]];[[G
2
]]), in
a state with no further actions deﬁned. Hence, by the
realizability of G
1
and G
2
, G is realizable and, by the
reception-completeness of G
1
and G
2
, also reception-
complete.
3.6 Choreography Well-Formedness
For a given action pomset setR, let Wb(R) denote
that R is well-branched, i.e. that either jRj = 1 or
there exist non-empty action pomset setsR
1
 R and
R
2
  R satisfying (R
1
[R
2
= R)^ Wb(R
1
)^
Wb(R
2
)^Lc(R
1
;R
2
). Like [1], we deﬁne that a given
choreography G is well-formed, which we denote as
Wf(G), if:Ac([[G]])^Wb([[G]]).
Proposition 1. If a given choreography G satisﬁes
Wf(G), it is realizable and reception-complete.
Proof: Suppose that the premise is true. Hence,
there exists a choreography G
0
with [[G
0
]] = [[G]] in
which every subterm is either a G
00
with (jhhG
00
iij =
1)^:Ac([[G
00
]]) or a G
1
+G
2
with Lc([[G
1
]];[[G
2
]]).
G
0
and all its subterms are well-formed. By induction
on increasingly larger subterms ofG
0
, in each individual
induction step using Lemma 1 or Lemma 2, respectively,
one can, hence, prove that each of the subterms and G
0
itself are realizable and reception-complete. Hence, by
[[G]] = [[G
0
]], G is realizable and reception-complete.
3.7 Some Rules for the Inference of Choreography
Well-Formedness
In Section 2.5, the deﬁnition of   (R) for a given
action pomset set R is uplifted to our more general
setting. Below, the same is done for the predicate Ls
used in [1]. With the two redeﬁnitions, all the following
inference rules proposed in [1] remain valid in the more
general setting, together with their proofs provided in
[1]:
Proposition 2. If a choreography G satisﬁes (j[[G]]j =
1)^:Ac([[G]]), then Wf(G).
Proposition 3. If a choreographyG is of the form 0 or
b :l, then Wf(G).
Proposition 4. If given choreographiesG andG
0
satisfy
([[G]] = [[G
0
]])^Wf(G), then Wf(G
0
).
REALIZABLE CHOREOGRAPHIES 195
Proposition 5. If for a given choreography G, there
exist non-empty interaction pomset setsR
1
andR
2
with
(R
1
[R
2
=hhGii)^Wf(R
1
+R
2
), then Wf(G).
Proposition 6. If given choreographiesG
1
andG
2
sat-
isfyWf(G
1
)^Wf(G
2
)^Lc([[G
1
]];[[G
2
]]), thenWf(G
1
+
G
2
).
Proposition 7. If given choreographies G
1
and G
2
satisfy Wf(G
1
)^Wf(G
2
)^(  ([[G
1
]])\  ([[G
2
]]) =;),
then Wf(G
1
jG
2
).
For the next rule, we ﬁrst redeﬁne the predicate
Ls(G
1
;G
2
) [1] that for given choreographies G
1
and
G
2
denotes that they are locally strictly sequenced. In
our more general setting, this is in case that for every
interaction instance poset pair ((G
1
;  1
);(G
2
;  2
)) in
pos
1
(hhG
1
ii)  pos
2
(hhG
2
ii), the action instance poset
[[(G
1
[G
2
;(  1
[  2
[(G
1
 G
2
))
?
)]] is an (E;  ) with
   S
c2C
((
S
g2G1
ais(g)  c
)  (
S
g2G2
ais(g)  c
)).
Proposition 8. If given choreographiesG
1
andG
2
sat-
isfyWf(G
1
)^Wf(G
2
)^Ls(G
1
;G
2
), thenWf(G
1
;G
2
).
3.8 Inadequacy of the Three Recently Proposed
Similar Deﬁnitions of Well-Formed Choreographies
In the examples presented in this section, any action
b!(c;c
0
;m), b?(c;c
0
;m) or b!?(c;c
0
;m) whose (b;c;c
0
)
is evident from the context is denoted simply as !m, ?m
or !?m, respectively.
Speaking in terms of the abstract concepts introduced
in the previous subsections of Section 3, the conceptual
difference between our deﬁnition of well-formed chore-
ographies and those in [5]–[7] is that in [5]–[7], the
underlying deﬁnition of the choreography semantics is
virtually based on slightly modiﬁed predicateOrd
2
, and
in [5] also on slightly modiﬁed predicateOrd
1
. The two
modiﬁcations are as follows:
(1) The Ord
2
(a
1
;a
2
) which [5]–[7] implicitly employ
for given actionsa
1
anda
2
is virtually true also ifa
2
is a b!?(c;c
0
;m) with c
0
2 prt(a
1
) or a b?(c;c
0
;m)
with c
0
2 prt(a
1
).
(2) The Ord
1
(x
1
;x
2
) which [5] implicitly employs for
given interactions x
1
= b
1
: (c
1
;c
0
1
;m
1
) and x
2
=
b
2
: (c
2
;c
0
2
;m
2
) is virtually true also if Rv(b
2
)^
(c
0
2
2fc
1
;c
0
1
g).
With the modiﬁcation of Ord
2
, particularly if the
modiﬁcation of Ord
1
is also present, it is no longer
secured that the semantics [[G]] of a given choreography
G avoids prescribing delayed reception, i.e. that the
CSM system ofG is reception-complete. Note, however,
that in our proof of Lemma 1, the deadlock-freeness
of the CSM system of the considered well-formed
G with jhhGiij = 1 is deduced from its reception-
completeness, and that in our proof of Lemma 2, the
reception-completeness assumed for the considered al-
ternative choreographies G
1
and G
2
is employed for
deducing that no letter instance belonging to a given
G
i
2 fG
1
;G
2
g is interpreted by its recipient as one
belonging toG
3  i
. As the two lemmas are employed in
our proof of Proposition 1, it is, hence, possible that with
the modiﬁcation of Ord
2
, well-formed choreographies
are not necessarily realizable. The following examples
prove that this is indeed the case:
Example 1. Consider the choreography
G =(b
AB
: (A;B;x);b
BC
: (B;C;y);
b
CA
: (C;A;a);b
AB
: (A;B;x))+
(b
AC
: (A;C;z);b
CB
: (C;B;b);
b
CA
: (C;A;c);b
AB
: (A;B;x))
where each of the buffers is a FIFO channel or a mail-
box. With the modiﬁcation of Ord
2
, all the following is
true, regardless of whether the modiﬁcation of Ord
1
is
also employed:
(1) Wf(G)
(2) [[G]] forbids that !y and !z are both executed.
(3) In the CSM system of G, A chooses between the ac-
tion sequences!x?a!x and!z?c!x,B chooses between
?x!y?x and ?b?x, and C chooses between ?y!a and
?z!b!c.
(4) Hence, the system possibly executes the action se-
quence !z?z!b!c?c!x?x!y (and thereby !y after !z) and
then terminates, in a state in which b
BC
and b
CB
are
non-empty and B wants to execute another ?x.
Example 2. Consider the choreography
G =(b
AB
: (A;B;x);b
AC
: (A;C;y);
b
CD
: (C;D;z);b
BD
: (B;D;w))+
(b
AC
: (A;C;y);b
AB
: (A;B;x);
b
BD
: (B;D;w);b
CD
: (C;D;z))
where each of the buffers is a rendezvous channel. With
the modiﬁcation of Ord
1
only or with the modiﬁcation
of Ord
2
only, [[G]] is as without the modiﬁcations
and G is realizable and reception-complete. With both
modiﬁcations, however, all the following is true:
(1) Wf(G)
(2) [[G]] forbids the action sequence !?x!?y!?w!?z.
(3) In the CSM system of G, A chooses between the
action sequences !x!y and !y!x, B’s only option
is ?x!w, C’s only option is ?y!z, and D chooses
between ?z?w and ?w?z.
(4) Hence, the system possibly executes the forbidden
!?x!?y!?w!?z.
4 FINAL REMARKS
By forbidding auto-concurrency and assuming that in
every rendezvous, the only participants are a predeﬁned
sender and a predeﬁned recipient, we easily adapted the
in [1] proposed deﬁnition of well-formed choreographies
to the considered more general kind of systems. In
the future, it would be interesting to extend the search
for easy-to-check sufﬁcient conditions for choreography
realizability also to choreographies in which individual
rendezvous have multiple participants, and individual
196 KAPUS-KOLAR
rendezvous participants have no predeﬁned roles, for
note that symmetric multiway rendezvous are a very use-
ful concept, particularly in early system design phases
when the system is considered at a high level of abstrac-
tion [8].
ACKNOWLEDGEMENT
This work was ﬁnanced by the Slovenian Research
Agency (research programme P2-0095).
REFERENCES
[1] M. Kapus-Kolar, “Realizable causal-consistent reversible chore-
ographies for systems with ﬁrst-in-ﬁrst-out communication chan-
nels,” J. Log. Algebraic Methods Program., vol. 114, p. 100560,
2020.
[2] E. Tuosto and R. Guanciale, “Semantics of global view of
choreographies,” Journal of Logical and Algebraic Methods in
Programming, vol. 95, pp. 17–40, 2018.
[3] R. Guanciale and E. Tuosto, “Realisability of pomsets,” J. Log.
Algebr. Meth. Program., vol. 108, pp. 69–89, 2019.
[4] D. Brand and P. Zaﬁropulo, “On communicating ﬁnite-state ma-
chines,” J. ACM, vol. 30, no. 2, pp. 323–342, Apr. 1983.
[5] F. Barbanera, I. Lanese, and E. Tuosto, “Choreography automata,”
in Proc. COORDINATION 2020 (Lecture Notes in Computer
Science, vol. 12134), Springer, Berlin, 2020, pp. 86–106.
[6] K. Schewe, Y . A. Ameur, and S. Benyagoub, “Realisability of
choreographies,” in Proc. FoIKS 2020 (Lecture Notes in Computer
Science, vol. 12012), Springer, 2020, pp. 263–280.
[7] U. de’Liguoro, H. C. Melgratti, and E. Tuosto, “Towards reﬁnable
choreographies,” in Proc. ICE 2020 (EPTCS, vol. 324), 2020, pp.
61–77.
[8] H. Garavel and W. Serwe, “The unheralded value of the multiway
rendezvous: Illustration with the production cell benchmark,” in
Proc. MARS@ETAPS 2017 (EPTCS, vol. 244), 2017, pp. 230–
270.
Monika Kapus-Kolar received her B.Sc. degree in electrical engi-
neering from the University of Maribor, Slovenia, and her M.Sc. and
Ph.D. degrees in computer science from the University of Ljubljana,
Slovenia, in the years 1981, 1984 and 1989, respectively. Since 1981
she has been with the Joˇ zef Stefan Institute, Ljubljana, where she
is currently a senior researcher at the Department of Communication
Systems. Her current research interests include formal speciﬁcation
techniques and methods for the development of real-time, concurrent
and reactive systems.