Communica ion Requi emen s o
Team Au oma a
Mau ice H. e Beek1, Josep Ca mona2, Rol Hennicke 3, and Je y Kleijn4
1ISTI–CNR, Pisa, I aly
2Uni e si a Poli ècnica de Ca alunya, Ba celona, Spain
3Ludwig-Maximilians-Uni e si ä , München, Ge many
4LIACS, Leiden Uni e si y, The Ne he lands
Abs ac . Compa ibili y o componen s is an impo an issue in he
ques o sys ems o sys ems ha gua an ee success ul communica ions,
ee om message loss and inde ini e wai ing o inpu s. In his pape ,
we in es iga e compa ibili y in he con ex o sys ems consis ing o e-
ac i e componen s which may communica e h ough he synch onised
execu ion o common ac ions. We model such sys ems in he eam au-
oma a amewo k, which does no impose any a p io i es ic ions on he
synch onisa ion policy ollowed o combine he componen s. We iden i y
a amily o ep esen a i e synch onisa ion ypes based on he numbe
o sending and ecei ing componen s pa icipa ing in synch onisa ions.
Then, we p o ide a gene ic p ocedu e o de i e, o each synch onisa ion
ype, equi emen s o ecep i eness and o esponsi eness o eam au-
oma a ha p e en ha ou pu s a e no accep ed and inpu s a e no
p o ided, espec i ely. Due o he gene ici y o ou app oach w. . . syn-
ch onisa ion policies, we can cap u e compa ibili y no ions o a ious
mul i-componen sys em models known om he li e a u e.
1 In oduc ion
Mode n sys ems a e o en la ge-scale concu en and dis ibu ed sys ems o in-
e connec ed, eac i e componen s which collabo a e h ough message exchange.
Fo hei co ec unc ioning i is no only impo an ha each componen sa is-
ies applica ion-speci ic p ope ies, bu i is also essen ial ha no communica ion
ailu es, like message loss o inde ini e wai ing o inpu , occu du ing sys em
execu ion. This equi es a deep unde s anding o he ypical communica ion and
in e ac ion policies used in such mul i-componen sys ems. To es ablish ha
componen s wi hin a sys em in e ac co ec ly, a concep known as compa ibil-
i y is use ul. In [1], a cha ac e isa ion was gi en o compa ibili y o wo com-
ponen s ha should engage in a dialogue ee om message loss and inde ini e
wai ing. In [2], his bina y no ion o compa ibili y was li ed o mul i-componen
sys ems, in which communica ion may ake place be ween mo e han wo com-
ponen s a he same ime (e.g. b oadcas ing). Compa ibili y ailu es de ec ed
in a dis ibu ed, modula sys em model may e eal impo an p oblems in he
design o one o mo e o i s componen s, o be epai ed be o e implemen a ion.
© IFIP 2017. This is he au ho 's e sion o he wo k. I is pos ed he e by pe mission o IFIP o you pe sonal use. No o edis ibu ion.
The de ini i e e sion was published in: Ca mona, J. [e al.]. Communica ion equi emen s o eam au oma a. A: In e na ional Con e ence on
Coo dina ion Models and Languages. "Coo dina ion Models and Languages, 19 h IFIP WG 6.1 In e na ional Con e ence, COORDINATION
2017: Held as Pa o he 12 h In e na ional Fede a ed Con e ence on Dis ibu ed Compu ing Techniques, DisCoTec 2017: Neuchâ el,
Swi ze land, June 19-22, 2017: p oceedings". Be lín: Sp inge , 2017, p. 256-277. h ps://link.sp inge .com/hap e /10.1007/978-3-319-59746-1_14
Compa ibili y checks conside ing a ious communica ion and in e ac ion policies
hus signi ican ly aid he de elopmen o co ec componen -based sys ems.
I/O- ansi ion sys ems a e equen ly used as a model o eac i e compo-
nen s on which o o mally de ine and analyse compa ibili y. To exp ess eac-
i i y, I/O- ansi ion sys ems ely on dis inguished ou pu (ac i e), inpu (pas-
si e) and in e nal (p i a ely ac i e) ac ions. They come in se e al la ou s, like
I/O au oma a [3,4], eam au oma a [5,6], in e ace au oma a [7,8], componen -
in e ac ion au oma a [9] o modal I/O au oma a [10]. Se e al compa ibili y no-
ions s udied in he li e a u e a e in luenced by he in e ace au oma a app oach,
which uses synch onous poin - o-poin communica ion. Two in e ace au oma a
a e said o be compa ible i no illegal s a e can be eached au onomously in he
synch onous p oduc o he wo. A s a e is illegal i “one o he au oma a may
p oduce an ou pu ac ion ha is an inpu ac ion o he o he au oma on, bu
no accep ed” [7]. The no ion was weakened in [11] by allowing a componen o
s ill pe o m some in e nal ac ions be o e accep ing he inpu . Ou pu s which
a e no accep ed as inpu a e conside ed as message loss o as unspeci ied e-
cep ions [12,13]. I any (au onomously chosen) ou pu is accep ed, we call his
ecep i eness [14]. An o hogonal issue conce ns he iewpoin o a componen
wai ing o ecei e an inpu . I expec s an app op ia e ou pu o be p o ided. Bu
in his case he en i onmen can choose which inpu o se e. He e we e e o
his kind o communica ion equi emen (which was al eady conside ed as pa
o a no ion o I/O-compa ibili y in [1]) as esponsi eness.
Condi ions o ecep i eness and esponsi eness ha e been conside ed in [13]
o se ices and in [2] o eam au oma a. Bo h app oaches suppo compa ibili y
in mul i-componen en i onmen s o synch onous p oduc s, which a e known
o hei appealing composi ionali y and modula i y p ope ies [4,15–18]. A i s
explo a ion on how compa ibili y no ions could be gene alised o a bi a y syn-
ch onisa ion policies was pe o med in [14] in he amewo k o eam au oma a.
Howe e , due o he e y loose na u e o synch onisa ion policies in eam au-
oma a, a sys ema ic me hodology on how o o malise compa ibili y condi ions
in such gene al se ings is s ill missing. I is he mo i a ion o his wo k.
The p esen pape uses as a ounda ion again he eam au oma a ame-
wo k, bu we addi ionally de ine a ep esen a i e se o communica ion pa e ns,
called synch onisa ion ypes, which help o classi y he synch onisa ion policies
ha can be ealised in eam au oma a. A synch onisa ion ype (snd, c )can
speci y anges o he numbe o sende s and ecei e s which can ake pa in
a communica ion inside he sys em (possibly based on side condi ions). Any
synch onisa ion ype uniquely de e mines a synch onisa ion policy i he unde -
lying sys em o componen s is closed. O he wise, synch onisa ion policies wi h
he same ype may a y conce ning op ions o in e ac ion wi h he en i on-
men o he sys em. In any global s a e o a sys em S, one o i s componen s
o —mo e gene ally—a g oup o componen s in Smay equi e ce ain communi-
ca ions wi h o he componen s in he sys em depending on he cu en ly enabled
ac ions. I (common) ou pu s a e enabled in a g oup o componen s his leads o
equi emen s o ecep ion. Con e sely, enabled inpu s lead o equi emen s o
p o iding app op ia e ou pu , i.e. esponsi eness equi emen s. This allows us o
de ine a no ion o compa ibili y o eam au oma a in e ms o hei compliance
wi h communica ion equi emen s. A eam au oma on is said o be complian
wi h communica ion equi emen s i he desi ed communica ions can immedi-
a ely occu in he eam; i is said o be weakly complian i he communica ion
can e en ually occu a e some in e nal ac ions ha e been pe o med.
In his pape , we p opose a gene al p ocedu e o sys ema ically de i e ecep-
i eness and esponsi eness equi emen s om any synch onisa ion ype. Then
we can check o any eam au oma on o synch onisa ion ype (snd, c )whe he
i is complian wi h he ecep i eness and/o esponsi eness equi emen s de-
i ed om (snd, c ). Thus we ge a amily o compa ibili y no ions indexed by
synch onisa ion ypes. Ou me hodology is illus a ed wi h se e al examples. We
show ha ou no ions can be ins an ia ed wi h well-known compa ibili y no ions
om he li e a u e whe e pa icula synch onisa ion ypes a e conside ed. In pa -
icula , ou app oach can exp ess wo di e en pa adigms o compa ibili y in
open sys ems, o en called he op imis ic and pessimis ic app oaches (c . [19]).
The pape is o ganised as ollows. In Sec . 2, we in oduce eam au oma a
ollowed by he no ion o synch onisa ion ypes in Sec . 3. In Sec . 4, we de ine
communica ion equi emen s o ecep i eness and esponsi eness and he com-
pliance o eam au oma a wi h such equi emen s. In Sec . 5, we show how o
de i e hese equi emen s om synch onisa ion ypes and how known compa i-
bili y no ions om he li e a u e can be cap u ed. We conclude wi h Sec . 6.
2 Componen Au oma a and Team Au oma a
Componen au oma a and eam au oma a a e de ined as ( eac i e) au oma a
wi hou inal s a es which dis inguish inpu , ou pu and in e nal ac ions and
which can be combined by synch onisa ions on common ac ions acco ding o
synch onisa ion policies. Fi s we ix some no a ion.
Gi en a ini e index se I={1, . . . , n}, we deno e he Ca esian p oduc o
se s V1, . . . , Vnas Qi∈I Vi. I = ( 1, . . . , n)∈Qi∈I Viand i∈ I, hen he i- h
en y o is ob ained by applying he p ojec ion unc ion p oji:Qi∈I Vi→Vi
de ined by p oji( 1, . . . , n) = i.
De ini ion 1 (Componen au oma on). Acomponen au oma on is a uple
A= (Q, Σ, δ, I), wi h se Qo s a es; se Σo ac ions, such ha Q∩Σ=∅,
and Σis he union o h ee pai wise disjoin se s Σinp,Σou and Σin o inpu ,
ou pu and in e nal ac ions, espec i ely; δ⊆Q×Σ×Qis i s se o (labelled)
ansi ions; and ∅ 6=I⊆Qi s se o ini ial s a es.u
A (componen ) au oma on (Q, Σ, δ, I)wi h inpu , ou pu and in e nal ac ions
Σinp,Σou and Σin , espec i ely, may be speci ied as (Q, (Σinp, Σou , Σin ), δ, I).
By Σex we deno e he se Σinp ∪Σou o ex e nal ac ions. Especially in igu es,
we may emphasise he ole o ex e nal ac ions by appending inpu ac ions wi h ?
and ou pu ac ions wi h !. Fo an ac ion a∈Σ, we de ine he se o a- ansi ions
as δa=δ∩(Q× {a} × Q). We may w i e pa
−→Ap0ins ead o (p, a, p0)∈δ.
The beha iou o an au oma on Ais de e mined by he execu ion o ac ions
enabled a i s cu en s a e. We say ha ais enabled in Aa s a e p∈Q, deno ed
by aenAp, i he e exis s p0∈Qsuch ha pa
−→Ap0. The ( ini e, sequen ial)
compu a ions o A, deno ed by C(A), a e hose sequences p0a1p1· · · pk−1akpk
such ha k≥0,p0∈Iand pi−1
ai
−→Api o all i∈ {1, . . . , k}. Fo X⊆Σ, we
w i e pX
−→∗
Ap0i he e exis s p0
a1
−→Ap1, . . . , pj−1
aj
−→Apj o some j≥0, wi h
p0,...pj∈Q,a1, . . . , aj∈X,p=p0, and p0=pj. A s a e p∈Qis eachable i
p0
Σ
−→∗
Ap(wi h p0∈I) and he se o eachable s a es o Ais deno ed by R(A).
As usual, we may omi subsc ip s e e ing o Ai no con usion can a ise.
Team au oma a consis o componen au oma a ha collabo a e h ough
synch onised execu ions o sha ed ac ions. When and which ac ions a e execu ed
and by how many componen s depends on he chosen synch onisa ion policy.
Le I={1, . . . , n}be a ini e index se . Le S={ Ai|i∈ I } be a se o com-
ponen au oma a de ined, o each i∈ I, as Ai= (Qi,(Σi,inp, Σi,ou , Σi,in ), δi, Ii)
wi h Σi=Σi,inp ∪Σi,ou ∪Σi,in .Sis composable i Σi,in ∩Sn
j=1,j6=iΣj=∅ o all
i∈ I. Thus in a composable sys em, in e nal ac ions a e no sha ed. No e ha
e e y subse o a composable se o componen au oma a is again composable.
Σ=Si∈I Σiis he se o ac ions o S,Σin =Si∈I Σi,in i s se o in e nal
ac ions and Σex =Si∈I Σi,ex i s se o ex e nal ac ions. Mo eo e , Σcom =
Si∈I Σi,inp ∩Si∈I Σi,ou is he se o communica ing ac ions o S. Hence, an
ac ion (o S) is communica ing i i occu s in Σex bo h as an inpu ac ion o
one o he au oma a and as an ou pu ac ion o an au oma on.
Fo an ac ion a∈Σ, i s domain in S, deno ed by doma(S), consis s o he
indices o all au oma a om Sin which i appea s as an ac ion. So, doma(S) =
{i|a∈Σi}. Hence in a composable sys em, he domain o an in e nal ac ion
is always a single on se . Fo a∈Σex , we le doma,inp(S) = {i|a∈Σi,inp }be
i s inpu domain (in S) and doma,ou (S) = {i|a∈Σi,ou }i s ou pu domain
(in S). Hence an ac ion is a communica ing ac ion o Si bo h i s ou pu and
i s inpu domain in Sa e no emp y.
Finally, we say ha Sis open i i has ex e nal ac ions ha a e no com-
munica ing ( hey appea only as an inpu o only as an ou pu ac ion). I Sis
no open, i may be e e ed o as closed; in his case all i s ex e nal ac ions a e
communica ing (all ha e a leas one communica ion pa ne ).
No a ion. Fo he emainde o his pape , we ix Iand Sas abo e. Mo eo e ,
Sis composable. We e e o Q=Qi∈I Qias he s a e space o Sand o Σ,
Σin ,Σex and Σcom as i s se o ac ions, in e nal ac ions, ex e nal ac ions and
communica ing ac ions, espec i ely.
De ini ion 2 (Sys em ansi ion). A uple (q, a, q0)∈Q×Σ×Qis a an-
si ion on a(in S) i he e exis s an i∈ I such ha (p oji(q), a, p oji(q0)) ∈δi,
and i o all i∈ I, ei he (p oji(q), a, p oji(q0)) ∈δio p oji(q) = p oji(q0).
Fo a∈Σ,∆a(S)is he se o all ansi ions on ain S, while ∆(S) =
Sa∈Σ∆a(S)is he se o all ansi ions in S.u
I (q, a, q0)∈∆(S), hen any componen Ai o which (p oji(q), a, p oji(q0)) ∈δi
is said o be in ol ed in (q, a, q0). By de ini ion, in all ansi ions in S, a leas one
componen is in ol ed h ough a ‘local’ ansi ion. Mo eo e , all ansi ions in
∆a(S)a e combina ions o exis ing a- ansi ions om he componen au oma a
in Sand all possible combina ions occu in ∆a(S). As in ea lie pape s, we will
o en e e o he elemen s o ∆a(S)as synch onisa ions on aalso when no mo e
han one componen is ac i ely in ol ed. In pa icula , when ais an in e nal
ac ion o a componen au oma on, hen all ansi ions on aa e execu ed by ha
componen alone. Mo eo e , o each ansi ion on an ex e nal ac ion in one o
he au oma a, ∆(S)will also con ain all synch onisa ions ha in ol e only ha
componen h ough ha pa icula local ansi ion. When a synch onisa ion on
an ex e nal ac ion ain ol es bo h a componen in which ais an inpu ac ion
and one in which i is an ou pu ac ion, i is called a communica ion.
All eam au oma a o e Swill ha e Σas hei se o ac ions, consis ing o he
ex e nal ac ions Σex o he componen s and he in e nal ac ions Σin comp ising
all in e nal ac ions o he componen s. In addi ion, we need o de ine he se s
o inpu and ou pu ac ions. We ollow he idea om [6] ha componen s ha e
con ol o e hei ou pu ac ions whe eas inpu ac ions a e passi e, i.e. d i en
by he en i onmen . As a consequence, ac ions ha appea as an ou pu ac ion
in one o mo e o he componen s a e conside ed o be unde he con ol o he
eam and hence will be ou pu ac ions o he eam (e en i hey a e inpu o
some o he componen s). Inpu ac ions ha do no appea as ou pu , a e inpu
ac ions o he eam. Fo mally, Σou =Si∈I Σi,ou and Σinp = (Si∈I Σi,inp) Σou .
Fu he mo e, Q=Qi∈I Qiwill be he se o s a es o e e y eam au oma on
o e Sand I=Qi∈I Iii s se o ini ial s a es.
Finally, i is he choice o synch onisa ions, hus he choice o a subse δo
∆(S), ha de ines a speci ic eam au oma on. As in e nal ac ions a e assumed
o be unde he con ol o he componen au oma a, all ansi ions on in e nal
ac ions will always be included as ansi ions o any eam au oma on o e S.
Subse s δo ∆(S), such ha δa=∆a(S) o all a∈Σin , a e e e ed o as
synch onisa ion policies (o e S).
De ini ion 3 (Team au oma on). The eam au oma on o e Swi h synch o-
nisa ions δis he componen au oma on T= (Q, (Σinp, Σou , Σin ), δ, I).u
Each eam au oma on de e mines a synch onisa ion policy o e Sand ice e sa.
Since e e y eam au oma on is a componen au oma on, eam au oma a can be
used in hie a chical cons uc ions (sys ems o sys ems).
3 Synch onisa ion Types
We ha e seen ha eam au oma a o e a composable sys em a e de ined by syn-
ch onisa ion policies. Fo all s a es o he sys em and o each ex e nal ac ion
enabled a he co esponding local s a e o a leas one o i s componen s, i has
o be decided which synch onisa ions on ha ac ion o include as a ( eam) an-
si ion. In p ac ice, his will seldom be decided indi idually o e e y candida e
synch onisa ion. The sys em designe will mos likely ha e a ce ain synch oni-
sa ion pa e n in mind. In his sec ion, we in oduce so-called synch onisa ion
ypes which allow us o de ine in a compac way speci ic synch onisa ion policies.

Synch onisa ion ypes speci y lowe and uppe bounds on he numbe o
componen s in ol ed in a synch onisa ion o hey indica e ha he synch o-
nisa ion is o an ac ion-indispensible o s a e-indispensible ype. These no ions
we e o iginally in oduced in [6]. The e an ac ion-indispensible synch onisa ion
policy equi es o e e y eam ansi ion on a gi en ac ion he in ol emen o
all componen s o which ha ac ion belongs; a policy is s a e-indispensible i
in e e y eam ansi ion on a gi en ac ion all componen s ha could be in-
ol ed (because ha ac ion is enabled a he cu en local s a e) a e in ol ed.
He e, we apply his idea o communica ing ac ions and dis inguish be ween
hei inpu and ou pu oles. We use ai and si o indica e he numbe o
inpu o ou pu componen s ha could maximally be in ol ed in a synch o-
nisa ion on a communica ing ac ion (ha ing ha ac ion as inpu o ou pu ,
espec i ely, and o si he ac ion is mo eo e enabled a he cu en local s a e).
The nex de ini ion in oduces synch onisa ion ypes as pai s ha can be used
o speci y o a synch onisa ion on a communica ing ac ion, possible numbe s o
componen s in ol ed as sending componen s ( o which he ac ion execu ed is an
ou pu ac ion) and as ecei ing componen s ( o which he ac ion is an inpu ).
De ini ion 4 (Synch onisa ion ype). Asynch onisa ion ype is a pai
(snd, c )such ha o x=snd and o x= c ei he xis an in e al [k, m]
wi h 0≤kand (k≤mo m=∗)o x∈ {ai ,si }. We call snd and c he
sending and ecei ing mul iplici y, espec i ely, o he synch onisa ion ype. u
Nex , we u n o synch onisa ions. Fo (p, a, p0)∈∆(S), he numbe o au oma a
in ol ed as ou pu o inpu componen in (p, a, p0)is deno ed as ollows:
ou a(p, a, p0)=#{i∈ I | (p oji(p), a, p oji(p0)) ∈δiand a∈Σi,ou }
inpa(p, a, p0)=#{i∈ I | (p oji(p), a, p oji(p0)) ∈δiand a∈Σi,inp }
To be able o deal wi h si , we deno e he numbe o au oma a, o which an
ou pu o inpu ac ion a∈Σcom is locally enabled a s a e p∈Q, as ollows:
ou si (p, a)=#{i∈ I | aenAip oji(p)and a∈Σi,ou }
inpsi (p, a)=#{i∈ I | aenAip oji(p)and a∈Σi,inp }
In wha ollows, `∈Nis said o sa is y an in e al [k, m]wi h 0≤k≤m
whene e k≤`≤m; and `sa is ies [k, ∗]i k≤`.
De ini ion 5 (Typed synch onisa ion policy). Le a∈Σcom,p∈Qand
(p, a, p0)∈∆(S). Then
(p, a, p0)is o ype (snd, c )i















snd = [o1, o2]and ou a(p, a, p0)sa is ies [o1, o2]
snd =ai and ou a(p, a, p0) = #doma,ou (S)
snd =si and ou a(p, a, p0) = ou si (p, a)
c = [i1, i2]and inpa(p, a, p0)sa is ies [i1, i2]
c =ai and inpa(p, a, p0) = #doma,inp(S)
c =si and inpa(p, a, p0) = inpsi (p, a)
We say ha a synch onisa ion policy δ⊆∆(S)is o ype (snd, c )i δcon ains,
o all a∈Σcom, all ansi ions on ao ype (snd, c )and no o he ansi ions
on a. A eam au oma on To e Swi h synch onisa ion policy δis o ype
(snd, c )i δis o ype (snd, c ).u
F om De ini ion 5 i ollows ha o closed sys ems whe e all ex e nal ac ions
a e communica ing, a synch onisa ion ype (snd, c )de e mines a unique syn-
ch onisa ion policy δand hence a eam au oma on. Synch onisa ion ypes do
no apply o non-communica ing ex e nal ac ions and so, i he sys em is open,
a synch onisa ion policy o a ce ain ype may con ain any subse o ansi ions
(p, a, p0)∈∆(S)wi h ac ions a∈Σex Σcom. I all o hem a e selec ed, hen
he synch onisa ion policy is called maximal.
No e ha a ansi ion in Smay be o se e al, di e en ypes. Fu he mo e,
a eam au oma on may ha e a synch onisa ion policy ha includes communica-
ions ha do no ha e a common synch onisa ion ype.
Le us now conside some amilia synch onisa ion ypes which occu in he
li e a u e and in conc e e sys ems.
([1,1],[1,1]): bina y communica ion, meaning ha a communica ing ac ion can
be execu ed only as a synch onisa ion in ol ing exac ly one componen o
which i is an ou pu ac ion and exac ly one o which i is an inpu ac ion.
([1,1],[0,1]): as di ec ly abo e, bu now o e a lossy channel, meaning ha a
communica ing ac ion can be los (i.e. in ol ing exac ly one componen o
which i is an ou pu ac ion and a mos one o which i is an inpu ac ion).
([1,1],[0,∗]): mul icas communica ion, meaning ha a communica ing ac ion
can be execu ed only as a synch onisa ion in ol ing exac ly one componen
o which i is an ou pu ac ion and any numbe o he componen s in which
i is an inpu ac ion. This is called weak synch onisa ion in BIP [20].
([1,1],si ): b oadcas communica ion, meaning ha whene e a communica ing
ac ion is execu ed i occu s exac ly once in i s ou pu ole in ha ansi ion
wi h as many as possible (all cu en ly enabled) inpu componen s in ol ed.
([1,1],ai ): s ong b oadcas communica ion, as di ec ly abo e, bu now wi h all
inpu componen s in ol ed. This is called s ong synch onisa ion in BIP.
(ai ,ai ): ansi ions on communica ing ac ions a e always ‘ ull’ synch onisa ions,
meaning ha all componen s ha sha e a communica ing ac ion a e in ol ed
in all ansi ions on ha ac ion. When all ex e nal ac ions a e communica ing
(Sis a closed sys em), his means ha we a e dealing wi h he classical
synch onous p oduc o au oma a (c ., e.g., [2,14,21]).
([1,∗],[0,∗]): ansi ions on communica ing ac ions always in ol e a leas one
componen whe e ha ac ion is an ou pu ac ion. This is he idea o ‘mas e -
sla e’ communica ion (c . [6]), acco ding o which a mas e (ou pu ) can
always be execu ed and sla es (inpu ) ne e p oceed on hei own.
([1,∗],[1,∗]): as di ec ly abo e, bu now a leas one sla e has o ‘obey’ ( he mas-
e ). This is called ‘s ong mas e -sla e’ communica ion (c . [6]), by which a
mas e (ou pu ) can always be execu ed and sla es (inpu ) mus be in ol ed.
([0,1],[0,1]): no obliga o y bina y communica ion (communica ing ac ions may
also be execu ed as s and alone) like in CCS [22]. u
These synch onisa ion ypes de ine eam au oma a based on one ype o syn-
ch onisa ion only, bu o u u e wo k combina ions could be imagined as well.
Example 1. We conside he sys em Sys1={Runne 1,Runne 2,Con olle }de-
pic ed in Fig. 1. He e and in all subsequen examples componen s ha e exac ly
one ini ial s a e deno ed by 0. All ac ions apa om he in e nal ac ions un1
and un2a e communica ing. We wan o combine hese componen s in a eam
in a way ha he con olle componen s a s bo h unne componen s a he
same ime, bu each unne can sepa a ely signal o he con olle when i has
eached he inish line. To his aim, he synch onisa ion ype (ai ,ai )wi h all
ansi ions on communica ing ac ions being ull synch onisa ions is app op ia e.
Thus we ob ain he eam au oma on T1o ype (ai ,ai )o e Sys1. (Since he
sys em is closed, his eam is unique.) u
0
1
2
s a ? un1
inish1!
(a) Runne 1
0
1
2
s a ? un2
inish2!
(b) Runne 2
0
2
1
3
s a !
inish1? inish2?
inish2? inish1?
(c) Con olle
Fig. 1: Au oma a Runne i, wi h i∈ {1,2}, and Con olle o Sys1
Example 2. Now we conside he sys em Sys2={Runne 0
1,Runne 0
2,Con olle 0}
depic ed in Fig. 2. The idea is simila o Example 1. As be o e, he con olle
should s a he unne s a he same ime and each unne should sepa a ely
send i s inish signal o he con olle . The di e ence wi h Sys1is ha bo h un-
ne s use he same inish signal o communica e wi h he con olle . The e o e we
canno use he synch onisa ion ype (ai ,ai )bu choose he ype ([1,1],ai )in-
s ead. The sending mul iplici y [1,1] en o ces ha communica ion in he sys em
will always in ol e exac ly one sende , which p ecludes he wo unne s sending
hei inish signal oge he . The ecei ing mul iplici y is ai since he wo unne s
mus ecei e he s a signal oge he . This leads o he eam au oma on T2o
ype ([1,1],ai )o e he sys em Sys2.u
0
1
2
s a ? un1
inish!
(a) Runne 0
1
0
1
2
s a ? un2
inish!
(b) Runne 0
2
0
2
1
s a !
inish? inish?
(c) Con olle 0
Fig. 2: Au oma a Runne 0
i, wi h i∈ {1,2}, and Con olle 0o Sys2
4 Communica ion Requi emen s
In his pape , we a e in e es ed in he communica ions be ween componen s in a
eam buil o e he sys em S. In any s a e po S, one o i s componen s o , mo e
gene ally, a g oup o componen s in Smay equi e ce ain communica ions wi h
o he componen s in he sys em. This is o mally exp essed by communica ion
equi emen s. In he ollowing, we ep esen a g oup o componen s in Sby hei
indices, i.e. by a non-emp y subse J ⊆ I. By abuse o e minology, we will
o en iden i y Jwi h he g oup o componen s ep esen ed by J.
Fo a communica ing ac ion a∈Σcom, a g oup J ⊆doma,ou (S)in he ou pu
domain o amay ha e a communica ion equi emen (J, a)a some s a e p, i
(ou pu ) ac ion ais enabled in he local s a es p ojj(p)o all componen s Ajwi h
j∈ J . This equi emen exp esses ha a leas one componen in he inpu do-
main o ashould communica e wi h g oup Jand ecei e ain he cu en s a e.
Thus (synch onised g oups o ) sending componen s can ha e demands w. . .
he ecep ion o an ou pu ac ion and he e o e (J, a)will be called a ecep-
i eness equi emen . Acco ding o De s. 7 and 8 below, i will depend on he
synch onisa ion policy o a eam whe he ecep i eness equi emen s a e ul illed.
Simila ly, we conside g oups J ⊆ doma,inp(S)in he inpu domain o a.
Then a communica ion equi emen (J, a)can be gi en o a s a e p, i (inpu )
ac ion ais enabled in he local s a es p ojj(p)o all componen s Ajwi h j∈ J .
Acco ding o his equi emen a leas one componen in he ou pu domain o
ashould communica e wi h he g oup and send ain he cu en s a e. Thus
(synch onised g oups o ) ecei ing componen s may equi e ou pu om o he
componen s and hen (J, a)will also be called a esponsi eness equi emen
(al hough i is no necessa ily a esponse o a o me call). Again i will depend
on he synch onisa ion policy o a eam whe he esponsi eness equi emen s a e
sa is ied (c . De s. 7 and 8).
Communica ion equi emen s can be combined by conjunc ion and disjunc-
ion. As we shall see in Sec . 5, he o me will be in pa icula use ul o combin-
ing ecep i eness equi emen s and he la e o esponsi eness equi emen s.
De ini ion 6 (Communica ion equi emen ).
(i) A ecep i eness equi emen a p∈Qis a pai (J, a)wi h a∈Σcom and
∅6=J ⊆ doma,ou (S)such ha aenAjp ojj(p) o all j∈ J .
(ii) A esponsi eness equi emen a p∈Qis a pai (J, a)wi h a∈Σcom and
∅6=J ⊆ doma,inp(S)such ha aenAjp ojj(p) o all j∈ J .
(iii) An a omic communica ion equi emen a p∈Qis ei he he i ial equi e-
men ue o a ecep i eness equi emen a po a esponsi eness equi e-
men a p.
(i ) A communica ion equi emen a p∈Qis ei he an a omic communica ion
equi emen o a conjunc ion ψ1∧ψ2o a disjunc ion ψ1∨ψ2o communi-
ca ion equi emen s ψ1and ψ2a pu
When all non- i ial a omic equi emen s occu ing in a communica ion equi e-
men ϕa e ecep i eness ( esponsi eness) equi emen s, we also e e o ϕas a
ecep i eness ( esponsi eness) equi emen , espec i ely.
Le us play a bi wi h his example o see he impo ance o synch onisa ion
ypes. Assume we would ha e chosen he sending mul iplici y [1,2] ins ead. The
co esponding synch onisa ion policy δ0would hen allow ha he wo unne s
send simul aneously he inish signal o he con olle , i.e. we ge an addi ional
ansi ion om s a e (1,2,2) o s a e (2,0,0) labelled wi h inish. Then we de i e
esponsi eness equi emen ({Con olle }, inish)∨({Runne 1,Runne 2},s a )
a he newly eachable s a e (2,0,0). Clea ly his equi emen is no ul illed by
he eam wi h synch onisa ion policy δ0(and hence i was a good idea o choose
he sending mul iplici y [1,1] o he sys em Sys1). u
01 n
k
ask1?
g an 1!
askk?.... ..g an k!
askn?
g an n!
(a) A bi e
012
join!
con i m?
con i m?
lea e!
msg!
wdmsg?
(b) Clien i
0 12
3
4 5
join?
lea e?
con i m!
imeou imeou
con i m!
msg?
imeou
ask!
g an i?
wdmsg!
(c) Se e j
Fig. 4: Au oma a A bi e ,Clien iand Se e j, wi h 1≤i≤mand 1≤j≤n
Example 7. As a mo e ealis ic example, conside a dis ibu ed cha sys em
whe e buddies can in e ac once hey egis e in o he sys em. Th ee ypes o
componen s o m he dis ibu ed cha sys em (c . Fig. 4): se e s, clien s and
an a bi e . To inc ease he obus ness o he sys em, no one bu se e al se e s
a e de o ed o con ol bo h new en ies in o o exi s om he cha , as well as o
coo dina e he main ac i i y in he cha , iz. o wa ding clien messages o he
cha . Communica ing ac ions a e pa i ioned in o cha access ac ions (join,lea e,
con i m), cha messaging (msg, wdmsg) and a bi e selec ion o he o wa ding
se e (aski,g an i). The o e all messaging p o ocol is ha clien s communi-
ca e messages o he se e s (ac ion msg), and only one among he se o se e s
b oadcas s he ecei ed message o he whole se o clien s in he cha ( h ough
ac ion wdmsg). The selec ion o he se e ha o wa ds he message is done
by he A bi e . No e ha in some o he s a es, se e s con ain an in e nal ac-
ion imeou o allow a se e o e u n o i s ini ial s a e whene e i does no
pa icipa e in he communica ion. Conside eam au oma on Tcha cons uc ed
o e he a o emen ioned sys em wi h synch onisa ion ype ([1,1],[1,∗]). We will
assume he sys em o con ain nse e s, mclien s and one a bi e . S a es in his
sys em a e exp essed as n+m+ 1 uples (q1, . . . , qn, qn+1, . . . , qn+m, qn+m+1),
i.e. he i s ns a es co espond o se e s a es, he second ms a es deno e
clien s a es and he las s a e co esponds o he a bi e s a e.

Le us now de i e wo examples o ecep i eness equi emen s (c . Sec . 5.1):
({Clien i},join)a (q1, . . . , qn,...qn+i−1,0, qn+i+1, . . . , qn+m+1)
({Se e j}, wdmsg)a (q1, . . . , qj−1,5, qj+1, . . . , qn+m+1)
These equi emen s exp ess ecep i eness obliga ions ul illed by Tcha . Fo in-
s ance, he i s equi emen exp esses ha in he s a e 0o Clien i, join ac ions
should be ecei ed by a leas one se e . Likewise, he second equi emen ex-
p esses ha he message o wa ded o he cha by a se e will be ecei ed by
he clien s. In his second equi emen , i is assumed ha some clien is s ill in
he cha (i.e. ∃i, n + 1 ≤i≤n+m:qi= 2).
An example o a esponsi eness equi emen is he ollowing (c . Sec . 5.2):
({Se e j},join)∨({Se e j},lea e)∨({Se e j},msg)
a (q1, . . . , qj−1,0, qj+1, . . . , qn,...qn+m+1)
This esponsi eness equi emen a s a e 0o Se e jp o ides a choice conce n-
ing he se e ’s unc ionali y: i can ei he coo dina e joining o exi ing ac ions
om a clien , o messages sen in he cha . As be o e o he se e ’s ecep-
i eness equi emen , i is assumed ha some clien is s ill in he cha (i.e.
∃i, n + 1 ≤i≤n+m:qi= 2).
Ano he example o a esponsi eness equi emen is as ollows (c . Sec . 5.2):
({A bi e },ask1)∨ · · · ∨ ({A bi e },askn)a (q1, . . . , qn+m,0)
This equi emen applies when a leas one se e is asking o pe mission o
o wa d he ecei ed message (i.e. ∃j, 1≤j≤n:qj= 3) and a leas one clien
is in he cha (i.e. ∃i, n + 1 ≤i≤n+m:qi= 2). I makes an obliga ion o
some o he se e s o p o ide some o he equi ed inpu s o he a bi e . u
5.4 Rela ed Compa ibili y No ions
In he li e a u e, compa ibili y no ions a e o en conside ed o sys ems buil
acco ding o a speci ic synch onisa ion ype. Fo ins ance, in e ace au oma a [7]
and many o he s, like [10,19,24], conside synch onous p oduc s o composable
I/O- ansi ion sys ems wi h (bina y) poin - o-poin communica ion, i.e. he syn-
ch onisa ion ype is ([1,1],[1,1]). These pape s mo eo e deal wi h he aspec o
ecep i eness only. We can say ha a eam au oma on o ype ([1,1],[1,1]) o e
a closed sys em o componen s A1and A2is ecep i e in he sense o De . 9 i
A1and A2a e compa ible in he sense o [7] i hey a e s ongly compa ible in
he sense o [24] i hey a e ecep i e in he sense o [1].
Fo open sys ems, he heo y o in e ace au oma a elies on he op imis ic
app oach. Two componen s a e compa ible i he e exis s a ‘help ul’ en i onmen
which a oids ha he sys em can each a communica ion e o . As we ha e seen,
synch onisa ion ypes de ine synch onisa ion policies uniquely only o closed
sys ems, while o open sys ems he e is s ill a possibili y o es ic he se o
ansi ions wi h ex e nal, non-communica ing ac ions. The e o e, we can ind an
app op ia e policy o make wo componen s ecep i e i hey a e compa ible in
he sense o [7]. Weak ecep i eness co esponds o weak compa ibili y in [24]
and is also cap u ed by unspeci ied ecep ions compa ibili y in [13]. We a e awa e
o only a ew app oaches ha conside compa ibili y w. . . esponsi eness. In [1],
esponsi eness is cap u ed by deadlock- eeness and in [13] i is exp essed by pa
o he de ini ion o bidi ec ional complemen a i y compa ibili y which, howe e ,
does no suppo choice o inpu s as we do.
5.5 Applica ions
The con ibu ions o his pape enable o explo e componen -based modelling
and composi ion acco ding o a wide ange o synch onisa ion policies, no lim-
i ed o he classical synch onous p oduc , b inging up on he communica ion
equi emen s ha mus be ul illed o de i e a complian sys em.
We o esee many applica ion a eas whe e he pe spec i e aken in his pa-
pe can play an impo an ole o enhance he in e ac ion and communica ion
policies ha a e used. In Swa m In elligence, o ins ance, agen s communica e
by means o senso s, ac ua o s and connec o s. Such senso s and ac ua o s allow
communica ion h ough he ecei ing and sending o signals. This communi-
ca ion o en conce ns a small selec ion o agen s ha changes o e ime, hus
de ia ing om he synch onous p oduc [25]. Being able o cons uc swa m ne -
wo ks ha ul il ce ain compa ibili y gua an ees on al e na i e communica ion
policies, like he ones conside ed in his pape , may ep esen an impo an s ep
owa ds hei sa is ac o y applica ion.
Ano he applica ion a ea is So wa e Enginee ing. In pa icula , he p o ision
o compa ibili y heo ies ha go beyond limi ed o malisms like UML s a echa s
composed acco ding o he synch onous p oduc , will ise he exp essibili y le el,
hus widening he applicabili y scope o co e much mo e eal-wo ld si ua ions.
Also concu en asynch onous p og amming languages can bene i om ha -
ing a gene al heo y o compa ibili y such as he one we en ision in his pape .
E lang [26] is a p ominen example: i s asynch onous communica ion mode al-
lows o a e y lexible communica ion a chi ec u e, bu i used inco ec ly i may
lead o in alid/subop imal sys em implemen a ions. To he bes o ou knowl-
edge, cu en app oaches ollow a pos -mo em app oach o e i y p ope ies like
li eness and sa e y o E lang p og ams. Ins ead, co ec -by-cons uc ion design
migh become applicable i he heo ies desc ibed in his pape we e used in he
speci ica ion o E lang p og ams.
Finally, he ield o Web se ices may also be a nice applica ion a ena o
he ideas pu o wa d in his pape . Like in some o he p e ious examples, we
a e only awa e o no ions o compa ibili y o he composi ion o Web se ices
de ined o e he es ic ed synch onous p oduc [27,28].
6 Conclusion
We ha e in es iga ed compa ibili y no ions conce ning ecep i eness and espon-
si eness in he eam au oma a amewo k. Team au oma a a e cha ac e ised by
he synch onisa ion policy hey use o coo dina e he componen s o a gi en
sys em. The e is a huge a ie y o possible synch onisa ion policies. The syn-
ch onisa ion ypes as we in oduced hem he e suppo a sys ema ic app oach
o he in es iga ion o compa ibili y no ions ela ed o communica ion. To ind
app op ia e compa ibili y no ions, we i s analysed wha kind o communica-
ion equi emen s can occu when componen s a e composed. We dis inguished
ecep i eness and esponsi eness equi emen s and we showed how such equi e-
men s can be sys ema ically de i ed depending on a synch onisa ion ype. A
eam au oma on is complian wi h a communica ion equi emen i (g oups o )
componen s in he eam issuing eques s o communica ion can success ully
ind pa ne s o join. I his is he case o all ecep i eness ( esponsi eness)
equi emen s, hen he eam au oma on is ecep i e ( esponsi e, espec i ely).
Ou app oach is app op ia e o bo h closed and open sys ems. A eam au-
oma on o e an open sys em is i sel a eac i e componen and hus gi es ise o
hie a chical composi ion. One o he nex s eps in ou esea ch will be o s udy
compa ibili y in he con ex o hie a chical composi ion and o synch onisa ion
policies ha a e no necessa ily uni o m bu combine di e en synch onisa ion
ypes. The la e would also conce n an in es iga ion o compa ibili y no ions
ailo ed o pa icula connec o s as used, e.g., in BIP and Reo (c . [29] o a
compa ison). Also he inco po a ion o asynch onous communica ion in syn-
ch onisa ion policies and he s udy o compa ibili y no ions in his case [24, 30]
is a opic o u u e esea ch. Mo eo e , app op ia e no ions o equi alences and
e inemen s o eam au oma a and how hey beha e w. . . ou ecep i eness and
esponsi eness no ions a e in e es ing ques ions o conside .
Acknowledgmen s We hank he e iewe s o hei commen s. J. Ca mona is
suppo ed by he Spanish Minis y o Economy and Compe i i eness (MINECO)
and he EU (FEDER unds) unde g an COMMAS (TIN2013-46181-C2-1-R).
Re e ences
1. J. Ca mona and J. Co adella. Inpu /Ou pu Compa ibili y o Reac i e Sys ems.
In FMCAD’02, olume 2517 o LNCS, pages 360–377. Sp inge , 2002.
2. J. Ca mona and J. Kleijn. Compa ibili y in a mul i-componen en i onmen .
Theo . Compu . Sci., 484:1–15, 2013.
3. N. A. Lynch and M. R. Tu le. Hie a chical Co ec ness P oo s o Dis ibu ed
Algo i hms. In PODC’87, pages 137–151. ACM, 1987.
4. N. A. Lynch and M. R. Tu le. An In oduc ion o Inpu /Ou pu Au oma a. CWI
Qua e ly, 2(3):219–246, 1989. h ps://i .cwi.nl/pub/18164.
5. C. A. Ellis. Team Au oma a o G oupwa e Sys ems. In GROUP’97, pages 415–
424. ACM, 1997.
6. M. H. e Beek, C. A. Ellis, J. Kleijn, and G. Rozenbe g. Synch oniza ions in Team
Au oma a o G oupwa e Sys ems. Compu . Sup. Coop. Wo k, 12(1):21–69, 2003.
7. L. de Al a o and T. A. Henzinge . In e ace Au oma a. In ESEC/FSE’01, pages
109–120. ACM, 2001.
8. L. de Al a o and T. A. Henzinge . In e ace-Based Design. In Enginee ing Theo ies
o So wa e In ensi e Sys ems, olume 195 o NATO Science Se ies, pages 83–104.
Sp inge , 2005.
9. L. B im, I. Ce ná, P. Va eko á, and B. Zimme o a. Componen -In e ac ion Au-
oma a as a Ve i ica ion-O ien ed Componen -Based Sys em Speci ica ion. ACM
So w. Eng. No es, 31(2), 2006.
10. K. G. La sen, U. Nyman, and A. Wąsowski. Modal I/O Au oma a o In e ace
and P oduc Line Theo ies. In ESOP’07, olume 4421 o LNCS, pages 64–79.
Sp inge , 2007.
11. S. S. Baue , P. Maye , A. Sch oede , and R. Hennicke . On Weak Modal Com-
pa ibili y, Re inemen , and he MIO Wo kbench. In TACAS’10, olume 6015 o
LNCS, pages 175–189. Sp inge , 2010.
12. D. B and and P. Za i opulo. On Communica ing Fini e-S a e Machines. J. ACM,
30(2):323–342, 1983.
13. F. Du án, M. Ouede ni, and G. Salaün. A gene ic amewo k o n-p o ocol com-
pa ibili y checking. Sci. Compu . P og am., 77(7-8):870–886, 2012.
14. M. H. e Beek, J. Ca mona, and J. Kleijn. Condi ions o Compa ibili y o Com-
ponen s: The Case o Mas e s and Sla es. In ISoLA’16, olume 9952 o LNCS,
pages 784–805. Sp inge , 2016.
15. B. Jonsson. Composi ional Speci ica ion and Ve i ica ion o Dis ibu ed Sys ems.
ACM T ans. P og am. Lang. Sys ., 16(2):259–303, 1994.
16. M. H. e Beek and J. Kleijn. Team Au oma a Sa is ying Composi ionali y. In
FME’03, olume 2805 o LNCS, pages 381–400. Sp inge , 2003.
17. G. Gössle and J. Si akis. Composi ion o componen -based modeling. Sci. Com-
pu . P og am., 55:161–183, 2005.
18. M. H. e Beek and J. Kleijn. Modula i y o eams o I/O au oma a. In . P ocess.
Le ., 95(5):487–495, 2005.
19. G. Lü gen, W. Vogle , and S. Fend ich. Riche in e ace au oma a wi h op imis ic
and pessimis ic compa ibili y. Ac a In ., 52(4-5):305–336, 2015.
20. A. Basu, M. Bozga, and J. Si akis. Modeling He e ogeneous Real- ime Componen s
in BIP. In SEFM’06, pages 3–12. IEEE, 2006.
21. A. A nold. Fini e T ansi ion Sys ems: Seman ics o Communica ing Sys ems.
P en ice Hall, 1994.
22. R. Milne . Communica ion and Concu ency. P en ice Hall, 1989.
23. G. Engels and L. G oenewegen. Towa ds Team-Au oma a-D i en Objec -O ien ed
Collabo a i e Wo k. In Fo mal and Na u al Compu ing, olume 2300 o LNCS,
pages 257–276. Sp inge , 2002.
24. R. Hennicke , M. Bidoi , and T.-S. Dang. On Synch onous and Asynch onous
Compa ibili y o Communica ing Componen s. In COORDINATION’16, olume
9686 o LNCS, pages 138–156. Sp inge , 2016.
25. T. Isokawa, F. Pepe , M. Mi sui, J.-Q. Liu, K. Mo i a, H. Umeo, N. Kamiu a, and
N. Ma sui. Compu ing by Swa m Ne wo ks. In ACRI’08, olume 5191 o LNCS,
pages 50–59. Sp inge , 2008.
26. J. A ms ong. E lang. Commun. ACM, 53(9):68–75, 2010.
27. M. H. e Beek, A. Bucchia one, and S. Gnesi. Web Se ice Composi ion Ap-
p oaches: F om Indus ial S anda ds o Fo mal Me hods. In ICIW’07. IEEE, 2007.
28. Q. Z. Sheng, X. Qiao, A. V. Vasilakos, C. Szabo, S. Bou ne, and X. Xu. Web
se ices composi ion: A decade’s o e iew. In . Sci., 280:218–238, 2014.
29. K. Dok e , S.-S. T. Q. Jongmans, F. A bab, and S. Bliudze. Combine and conque :
Rela ing BIP and Reo. J. Log. Algeb . Me h. P og am., 86(1), 2017.
30. J. L. Fiadei o and A. Lopes. An in e ace heo y o se ice-o ien ed design. Theo .
Compu . Sci., 503:1–30, 2013.