Communication requirements for team automata

Communication Requirements for Team Automata Maurice H. ter Beek1, Josep Carmona2, Rolf Hennicker3, and Jetty Kleijn4 1ISTI–CNR, Pisa, Italy 2Universitat Politècnica de Catalunya, Barcelona, Spain 3Ludwig-Maximilians-Universität, München, Germany 4LIACS, Leiden University, The Netherlands Abstract. Compatibility of components is an important issue in the quest for systems of systems that guarantee successful communications, free from message loss and indefinite waiting for inputs. In this paper, we investigate compatibility in the context of systems consisting of reactive components which may communicate through the synchronised execution of common actions. We model such systems in the team automata framework, which does not impose any a priori restrictions on the synchronisation policy followed to combine the components. We identify a family of representative synchronisation types based on the number of sending and receiving components participating in synchronisations. Then, we provide a generic procedure to derive, for each synchronisation type, requirements for receptiveness and for responsiveness of team automata that prevent that outputs are not accepted and inputs are not provided, respectively. Due to the genericity of our approach w.r.t. synchronisation policies, we can capture compatibility notions for various multi-component system models known from the literature. 1 Introduction Modern systems are often large-scale concurrent and distributed systems of interconnected, reactive components which collaborate through message exchange. For their correct functioning it is not only important that each component satisfies application-specific properties, but it is also essential that no communication failures, like message loss or indefinite waiting for input, occur during system execution. This requires a deep understanding of the typical communication and interaction policies used in such multi-component systems. To establish that components within a system interact correctly, a concept known as compatibility is useful. In [1], a characterisation was given for compatibility of two components that should engage in a dialogue free from message loss and indefinite waiting. In [2], this binary notion of compatibility was lifted to multi-component systems, in which communication may take place between more than two components at the same time (e.g. broadcasting). Compatibility failures detected in a distributed, modular system model may reveal important problems in the design of one or more of its components, to be repaired before implementation. © IFIP 2017. This is the author's version of the work. It is posted here by permission of IFIP for your personal use. Not for redistribution. The definitive version was published in: Carmona, J. [et al.]. Communication requirements for team automata. A: International Conference on Coordination Models and Languages. "Coordination Models and Languages, 19th IFIP WG 6.1 International Conference, COORDINATION 2017: Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017: Neuchâtel, Switzerland, June 19-22, 2017: proceedings". Berlín: Springer, 2017, p. 256-277. https://link.springer.com/hapter/10.1007/978-3-319-59746-1_14 Compatibility checks considering various communication and interaction policies thus significantly aid the development of correct component-based systems. I/O-transition systems are frequently used as a model for reactive components on which to formally define and analyse compatibility. To express reactivity, I/O-transition systems rely on distinguished output (active), input (passive) and internal (privately active) actions. They come in several flavours, like I/O automata [3,4], team automata [5,6], interface automata [7,8], componentinteraction automata [9] or modal I/O automata [10]. Several compatibility notions studied in the literature are influenced by the interface automata approach, which uses synchronous point-to-point communication. Two interface automata are said to be compatible if no illegal state can be reached autonomously in the synchronous product of the two. A state is illegal if “one of the automata may produce an output action that is an input action of the other automaton, but not accepted” [7]. The notion was weakened in [11] by allowing a component to still perform some internal actions before accepting the input. Outputs which are not accepted as input are considered as message loss or as unspecified receptions [12,13]. If any (autonomously chosen) output is accepted, we call this receptiveness [14]. An orthogonal issue concerns the viewpoint of a component waiting to receive an input. It expects an appropriate output to be provided. But in this case the environment can choose which input to serve. Here we refer to this kind of communication requirement (which was already considered as part of a notion of I/O-compatibility in [1]) as responsiveness. Conditions for receptiveness and responsiveness have been considered in [13] for services and in [2] for team automata. Both approaches support compatibility in multi-component environments for synchronous products, which are known for their appealing compositionality and modularity properties [4,15–18]. A first exploration on how compatibility notions could be generalised to arbitrary synchronisation policies was performed in [14] in the framework of team automata. However, due to the very loose nature of synchronisation policies in team automata, a systematic methodology on how to formalise compatibility conditions in such general settings is still missing. It is the motivation for this work. The present paper uses as a foundation again the team automata framework, but we additionally define a representative set of communication patterns, called synchronisation types, which help to classify the synchronisation policies that can be realised in team automata. A synchronisation type (snd,rcv)can specify ranges for the number of senders and receivers which can take part in a communication inside the system (possibly based on side conditions). Any synchronisation type uniquely determines a synchronisation policy if the underlying system of components is closed. Otherwise, synchronisation policies with the same type may vary concerning options for interaction with the environment of the system. In any global state of a system S, one of its components or—more generally—a group of components in Smay require certain communications with other components in the system depending on the currently enabled actions. If (common) outputs are enabled in a group of components this leads to requirements for reception. Conversely, enabled inputs lead to requirements for providing appropriate output, i.e. responsiveness requirements. This allows us to define a notion of compatibility for team automata in terms of their compliance with communication requirements. A team automaton is said to be compliant with communication requirements if the desired communications can immediately occur in the team; it is said to be weakly compliant if the communication can eventually occur after some internal actions have been performed. In this paper, we propose a general procedure to systematically derive receptiveness and responsiveness requirements from any synchronisation type. Then we can check for any team automaton of synchronisation type (snd,rcv)whether it is compliant with the receptiveness and/or responsiveness requirements derived from (snd,rcv). Thus we get a family of compatibility notions indexed by synchronisation types. Our methodology is illustrated with several examples. We show that our notions can be instantiated with well-known compatibility notions from the literature where particular synchronisation types are considered. In particular, our approach can express two different paradigms for compatibility in open systems, often called the optimistic and pessimistic approaches (cf. [19]). The paper is organised as follows. In Sect. 2, we introduce team automata followed by the notion of synchronisation types in Sect. 3. In Sect. 4, we define communication requirements for receptiveness and responsiveness and the compliance of team automata with such requirements. In Sect. 5, we show how to derive these requirements from synchronisation types and how known compatibility notions from the literature can be captured. We conclude with Sect. 6. 2 Component Automata and Team Automata Component automata and team automata are defined as (reactive) automata without final states which distinguish input, output and internal actions and which can be combined by synchronisations on common actions according to synchronisation policies. First we fix some notation. Given a finite index set I={1, . . . , n}, we denote the Cartesian product of sets V1, . . . , Vnas Qi∈I Vi. If v= (v1, . . . , vn)∈Qi∈I Viand i∈ I, then the i-th entry of vis obtained by applying the projection function proji:Qi∈I Vi→Vi defined by proji(v1, . . . , vn) = vi. Definition 1 (Component automaton). Acomponent automaton is a tuple A= (Q, Σ, δ, I), with set Qof states; set Σof actions, such that Q∩Σ=∅, and Σis the union of three pairwise disjoint sets Σinp,Σout and Σint of input, output and internal actions, respectively; δ⊆Q×Σ×Qis its set of (labelled) transitions; and ∅ 6=I⊆Qits set of initial states.ut A (component) automaton (Q, Σ, δ, I)with input, output and internal actions Σinp,Σout and Σint, respectively, may be specified as (Q, (Σinp, Σout, Σint), δ, I). By Σext we denote the set Σinp ∪Σout of external actions. Especially in figures, we may emphasise the role of external actions by appending input actions with ? and output actions with !. For an action a∈Σ, we define the set of a-transitions as δa=δ∩(Q× {a} × Q). We may write pa −→Ap0instead of (p, a, p0)∈δ. The behaviour of an automaton Ais determined by the execution of actions enabled at its current state. We say that ais enabled in Aat state p∈Q, denoted by aenAp, if there exists p0∈Qsuch that pa −→Ap0. The (finite, sequential) computations of A, denoted by C(A), are those sequences p0a1p1· · · pk−1akpk such that k≥0,p0∈Iand pi−1 ai −→Apifor all i∈ {1, . . . , k}. For X⊆Σ, we write pX −→∗ Ap0if there exists p0 a1 −→Ap1, . . . , pj−1 aj −→Apjfor some j≥0, with p0,...pj∈Q,a1, . . . , aj∈X,p=p0, and p0=pj. A state p∈Qis reachable if p0 Σ −→∗ Ap(with p0∈I) and the set of reachable states of Ais denoted by R(A). As usual, we may omit subscripts referring to Aif no confusion can arise. Team automata consist of component automata that collaborate through synchronised executions of shared actions. When and which actions are executed and by how many components depends on the chosen synchronisation policy. Let I={1, . . . , n}be a finite index set. Let S={ Ai|i∈ I } be a set of component automata defined, for each i∈ I, as Ai= (Qi,(Σi,inp, Σi,out, Σi,int), δi, Ii) with Σi=Σi,inp ∪Σi,out ∪Σi,int.Sis composable if Σi,int ∩Sn j=1,j6=iΣj=∅for all i∈ I. Thus in a composable system, internal actions are not shared. Note that every subset of a composable set of component automata is again composable. Σ=Si∈I Σiis the set of actions of S,Σint =Si∈I Σi,int its set of internal actions and Σext =Si∈I Σi,ext its set of external actions. Moreover, Σcom = Si∈I Σi,inp ∩Si∈I Σi,out is the set of communicating actions of S. Hence, an action (of S) is communicating if it occurs in Σext both as an input action of one of the automata and as an output action of an automaton. For an action a∈Σ, its domain in S, denoted by doma(S), consists of the indices of all automata from Sin which it appears as an action. So, doma(S) = {i|a∈Σi}. Hence in a composable system, the domain of an internal action is always a singleton set. For a∈Σext, we let doma,inp(S) = {i|a∈Σi,inp }be its input domain (in S) and doma,out(S) = {i|a∈Σi,out }its output domain (in S). Hence an action is a communicating action of Sif both its output and its input domain in Sare not empty. Finally, we say that Sis open if it has external actions that are not communicating (they appear only as an input or only as an output action). If Sis not open, it may be referred to as closed; in this case all its external actions are communicating (all have at least one communication partner). Notation. For the remainder of this paper, we fix Iand Sas above. Moreover, Sis composable. We refer to Q=Qi∈I Qias the state space of Sand to Σ, Σint,Σext and Σcom as its set of actions, internal actions, external actions and communicating actions, respectively. Definition 2 (System transition). A tuple (q, a, q0)∈Q×Σ×Qis a transition on a(in S) if there exists an i∈ I such that (proji(q), a, proji(q0)) ∈δi, and if for all i∈ I, either (proji(q), a, proji(q0)) ∈δior proji(q) = proji(q0). For a∈Σ,∆a(S)is the set of all transitions on ain S, while ∆(S) = Sa∈Σ∆a(S)is the set of all transitions in S.ut If (q, a, q0)∈∆(S), then any component Aifor which (proji(q), a, proji(q0)) ∈δi is said to be involved in (q, a, q0). By definition, in all transitions in S, at least one component is involved through a ‘local’ transition. Moreover, all transitions in ∆a(S)are combinations of existing a-transitions from the component automata in Sand all possible combinations occur in ∆a(S). As in earlier papers, we will often refer to the elements of ∆a(S)as synchronisations on aalso when no more than one component is actively involved. In particular, when ais an internal action of a component automaton, then all transitions on aare executed by that component alone. Moreover, for each transition on an external action in one of the automata, ∆(S)will also contain all synchronisations that involve only that component through that particular local transition. When a synchronisation on an external action ainvolves both a component in which ais an input action and one in which it is an output action, it is called a communication. All team automata over Swill have Σas their set of actions, consisting of the external actions Σext of the components and the internal actions Σint comprising all internal actions of the components. In addition, we need to define the sets of input and output actions. We follow the idea from [6] that components have control over their output actions whereas input actions are passive, i.e. driven by the environment. As a consequence, actions that appear as an output action in one or more of the components are considered to be under the control of the team and hence will be output actions of the team (even if they are input to some other components). Input actions that do not appear as output, are input actions of the team. Formally, Σout =Si∈I Σi,out and Σinp = (Si∈I Σi,inp)\Σout. Furthermore, Q=Qi∈I Qiwill be the set of states of every team automaton over Sand I=Qi∈I Iiits set of initial states. Finally, it is the choice of synchronisations, thus the choice of a subset δof ∆(S), that defines a specific team automaton. As internal actions are assumed to be under the control of the component automata, all transitions on internal actions will always be included as transitions of any team automaton over S. Subsets δof ∆(S), such that δa=∆a(S)for all a∈Σint, are referred to as synchronisation policies (over S). Definition 3 (Team automaton). The team automaton over Swith synchronisations δis the component automaton T= (Q, (Σinp, Σout, Σint), δ, I).ut Each team automaton determines a synchronisation policy over Sand vice versa. Since every team automaton is a component automaton, team automata can be used in hierarchical constructions (systems of systems). 3 Synchronisation Types We have seen that team automata over a composable system are defined by synchronisation policies. For all states of the system and for each external action enabled at the corresponding local state of at least one of its components, it has to be decided which synchronisations on that action to include as a (team) transition. In practice, this will seldom be decided individually for every candidate synchronisation. The system designer will most likely have a certain synchronisation pattern in mind. In this section, we introduce so-called synchronisation types which allow us to define in a compact way specific synchronisation policies. Synchronisation types specify lower and upper bounds on the number of components involved in a synchronisation or they indicate that the synchronisation is of an action-indispensible or state-indispensible type. These notions were originally introduced in [6]. There an action-indispensible synchronisation policy requires for every team transition on a given action the involvement of all components to which that action belongs; a policy is state-indispensible if in every team transition on a given action all components that could be involved (because that action is enabled at the current local state) are involved. Here, we apply this idea to communicating actions and distinguish between their input and output roles. We use ai and si to indicate the number of input or output components that could maximally be involved in a synchronisation on a communicating action (having that action as input or output, respectively, and for si the action is moreover enabled at the current local state). The next definition introduces synchronisation types as pairs that can be used to specify for a synchronisation on a communicating action, possible numbers of components involved as sending components (for which the action executed is an output action) and as receiving components (for which the action is an input). Definition 4 (Synchronisation type). Asynchronisation type is a pair (snd,rcv)such that for x=snd and for x=rcv either xis an interval [k, m] with 0≤kand (k≤mor m=∗)or x∈ {ai ,si }. We call snd and rcv the sending and receiving multiplicity, respectively, of the synchronisation type. ut Next, we turn to synchronisations. For (p, a, p0)∈∆(S), the number of automata involved as output or input component in (p, a, p0)is denoted as follows: outa(p, a, p0)=#{i∈ I | (proji(p), a, proji(p0)) ∈δiand a∈Σi,out } inpa(p, a, p0)=#{i∈ I | (proji(p), a, proji(p0)) ∈δiand a∈Σi,inp } To be able to deal with si , we denote the number of automata, for which an output or input action a∈Σcom is locally enabled at state p∈Q, as follows: outsi (p, a)=#{i∈ I | aenAiproji(p)and a∈Σi,out } inpsi (p, a)=#{i∈ I | aenAiproji(p)and a∈Σi,inp } In what follows, `∈Nis said to satisfy an interval [k, m]with 0≤k≤m whenever k≤`≤m; and `satisfies [k, ∗]if k≤`. Definition 5 (Typed synchronisation policy). Let a∈Σcom,p∈Qand (p, a, p0)∈∆(S). Then (p, a, p0)is of type (snd,rcv)if                snd = [o1, o2]and outa(p, a, p0)satisfies [o1, o2] snd =ai and outa(p, a, p0) = #doma,out(S) snd =si and outa(p, a, p0) = outsi (p, a) rcv = [i1, i2]and inpa(p, a, p0)satisfies [i1, i2] rcv =ai and inpa(p, a, p0) = #doma,inp(S) rcv =si and inpa(p, a, p0) = inpsi (p, a) We say that a synchronisation policy δ⊆∆(S)is of type (snd,rcv)if δcontains, for all a∈Σcom, all transitions on aof type (snd,rcv)and no other transitions on a. A team automaton Tover Swith synchronisation policy δis of type (snd,rcv)if δis of type (snd,rcv).ut From Definition 5 it follows that for closed systems where all external actions are communicating, a synchronisation type (snd,rcv)determines a unique synchronisation policy δand hence a team automaton. Synchronisation types do not apply to non-communicating external actions and so, if the system is open, a synchronisation policy of a certain type may contain any subset of transitions (p, a, p0)∈∆(S)with actions a∈Σext \Σcom. If all of them are selected, then the synchronisation policy is called maximal. Note that a transition in Smay be of several, different types. Furthermore, a team automaton may have a synchronisation policy that includes communications that do not have a common synchronisation type. Let us now consider some familiar synchronisation types which occur in the literature and in concrete systems. ([1,1],[1,1]): binary communication, meaning that a communicating action can be executed only as a synchronisation involving exactly one component for which it is an output action and exactly one for which it is an input action. ([1,1],[0,1]): as directly above, but now over a lossy channel, meaning that a communicating action can be lost (i.e. involving exactly one component for which it is an output action and at most one for which it is an input action). ([1,1],[0,∗]): multicast communication, meaning that a communicating action can be executed only as a synchronisation involving exactly one component for which it is an output action and any number of the components in which it is an input action. This is called weak synchronisation in BIP [20]. ([1,1],si ): broadcast communication, meaning that whenever a communicating action is executed it occurs exactly once in its output role in that transition with as many as possible (all currently enabled) input components involved. ([1,1],ai ): strong broadcast communication, as directly above, but now with all input components involved. This is called strong synchronisation in BIP. (ai ,ai ): transitions on communicating actions are always ‘full’ synchronisations, meaning that all components that share a communicating action are involved in all transitions on that action. When all external actions are communicating (Sis a closed system), this means that we are dealing with the classical synchronous product of automata (cf., e.g., [2,14,21]). ([1,∗],[0,∗]): transitions on communicating actions always involve at least one component where that action is an output action. This is the idea of ‘masterslave’ communication (cf. [6]), according to which a master (output) can always be executed and slaves (input) never proceed on their own. ([1,∗],[1,∗]): as directly above, but now at least one slave has to ‘obey’ (the master). This is called ‘strong master-slave’ communication (cf. [6]), by which a master (output) can always be executed and slaves (input) must be involved. ([0,1],[0,1]): not obligatory binary communication (communicating actions may also be executed as stand alone) like in CCS [22]. ut These synchronisation types define team automata based on one type of synchronisation only, but for future work combinations could be imagined as well. Example 1. We consider the system Sys1={Runner1,Runner2,Controller}depicted in Fig. 1. Here and in all subsequent examples components have exactly one initial state denoted by 0. All actions apart from the internal actions run1 and run2are communicating. We want to combine these components in a team in a way that the controller component starts both runner components at the same time, but each runner can separately signal to the controller when it has reached the finish line. To this aim, the synchronisation type (ai ,ai )with all transitions on communicating actions being full synchronisations is appropriate. Thus we obtain the team automaton T1of type (ai ,ai )over Sys1. (Since the system is closed, this team is unique.) ut 0 1 2 start?run1 finish1! (a) Runner1 0 1 2 start?run2 finish2! (b) Runner2 0 2 1 3 start! finish1?finish2? finish2?finish1? (c) Controller Fig. 1: Automata Runneri, with i∈ {1,2}, and Controller of Sys1 Example 2. Now we consider the system Sys2={Runner0 1,Runner0 2,Controller0} depicted in Fig. 2. The idea is similar to Example 1. As before, the controller should start the runners at the same time and each runner should separately send its finish signal to the controller. The difference with Sys1is that both runners use the same finish signal to communicate with the controller. Therefore we cannot use the synchronisation type (ai ,ai )but choose the type ([1,1],ai )instead. The sending multiplicity [1,1] enforces that communication in the system will always involve exactly one sender, which precludes the two runners sending their finish signal together. The receiving multiplicity is ai since the two runners must receive the start signal together. This leads to the team automaton T2of type ([1,1],ai )over the system Sys2.ut 0 1 2 start?run1 finish! (a) Runner0 1 0 1 2 start?run2 finish! (b) Runner0 2 0 2 1 start! finish?finish? (c) Controller0 Fig. 2: Automata Runner0 i, with i∈ {1,2}, and Controller0of Sys2 4 Communication Requirements In this paper, we are interested in the communications between components in a team built over the system S. In any state pof S, one of its components or, more generally, a group of components in Smay require certain communications with other components in the system. This is formally expressed by communication requirements. In the following, we represent a group of components in Sby their indices, i.e. by a non-empty subset J ⊆ I. By abuse of terminology, we will often identify Jwith the group of components represented by J. For a communicating action a∈Σcom, a group J ⊆doma,out(S)in the output domain of amay have a communication requirement (J, a)at some state p, if (output) action ais enabled in the local states projj(p)of all components Ajwith j∈ J . This requirement expresses that at least one component in the input domain of ashould communicate with group Jand receive ain the current state. Thus (synchronised groups of) sending components can have demands w.r.t. the reception of an output action and therefore (J, a)will be called a receptiveness requirement. According to Defs. 7 and 8 below, it will depend on the synchronisation policy of a team whether receptiveness requirements are fulfilled. Similarly, we consider groups J ⊆ doma,inp(S)in the input domain of a. Then a communication requirement (J, a)can be given for a state p, if (input) action ais enabled in the local states projj(p)of all components Ajwith j∈ J . According to this requirement at least one component in the output domain of ashould communicate with the group and send ain the current state. Thus (synchronised groups of) receiving components may require output from other components and then (J, a)will also be called a responsiveness requirement (although it is not necessarily a response to a former call). Again it will depend on the synchronisation policy of a team whether responsiveness requirements are satisfied (cf. Defs. 7 and 8). Communication requirements can be combined by conjunction and disjunction. As we shall see in Sect. 5, the former will be in particular useful for combining receptiveness requirements and the latter for responsiveness requirements. Definition 6 (Communication requirement). (i) A receptiveness requirement at p∈Qis a pair (J, a)with a∈Σcom and ∅6=J ⊆ doma,out(S)such that aenAjprojj(p)for all j∈ J . (ii) A responsiveness requirement at p∈Qis a pair (J, a)with a∈Σcom and ∅6=J ⊆ doma,inp(S)such that aenAjprojj(p)for all j∈ J . (iii) An atomic communication requirement at p∈Qis either the trivial requirement true or a receptiveness requirement at por a responsiveness requirement at p. (iv) A communication requirement at p∈Qis either an atomic communication requirement or a conjunction ψ1∧ψ2or a disjunction ψ1∨ψ2of communication requirements ψ1and ψ2at put When all non-trivial atomic requirements occurring in a communication requirement ϕare receptiveness (responsiveness) requirements, we also refer to ϕas a receptiveness (responsiveness) requirement, respectively. Let us play a bit with this example to see the importance of synchronisation types. Assume we would have chosen the sending multiplicity [1,2] instead. The corresponding synchronisation policy δ0would then allow that the two runners send simultaneously the finish signal to the controller, i.e. we get an additional transition from state (1,2,2) to state (2,0,0) labelled with finish. Then we derive responsiveness requirement ({Controller},finish)∨({Runner1,Runner2},start) at the newly reachable state (2,0,0). Clearly this requirement is not fulfilled by the team with synchronisation policy δ0(and hence it was a good idea to choose the sending multiplicity [1,1] for the system Sys1). ut 01 n k ask1? grant1! askk?.... ..grantk! askn? grantn! (a) Arbiter 012 join! confirm? confirm? leave! msg! fwdmsg? (b) Clienti 0 12 3 4 5 join? leave? confirm! timeouttimeout confirm! msg? timeout ask! granti? fwdmsg! (c) Serverj Fig. 4: Automata Arbiter,Clientiand Serverj, with 1≤i≤mand 1≤j≤n Example 7. As a more realistic example, consider a distributed chat system where buddies can interact once they register into the system. Three types of components form the distributed chat system (cf. Fig. 4): servers, clients and an arbiter. To increase the robustness of the system, not one but several servers are devoted to control both new entries into or exits from the chat, as well as to coordinate the main activity in the chat, viz. forwarding client messages to the chat. Communicating actions are partitioned into chat access actions (join,leave, confirm), chat messaging (msg,fwdmsg) and arbiter selection of the forwarding server (aski,granti). The overall messaging protocol is that clients communicate messages to the servers (action msg), and only one among the set of servers broadcasts the received message to the whole set of clients in the chat (through action fwdmsg). The selection of the server that forwards the message is done by the Arbiter. Note that in some of the states, servers contain an internal action timeout to allow a server to return to its initial state whenever it does not participate in the communication. Consider team automaton Tchat constructed over the aforementioned system with synchronisation type ([1,1],[1,∗]). We will assume the system to contain nservers, mclients and one arbiter. States in this system are expressed as n+m+ 1 tuples (q1, . . . , qn, qn+1, . . . , qn+m, qn+m+1), i.e. the first nstates correspond to server states, the second mstates denote client states and the last state corresponds to the arbiter state. Let us now derive two examples of receptiveness requirements (cf. Sect. 5.1): ({Clienti},join)at (q1, . . . , qn,...qn+i−1,0, qn+i+1, . . . , qn+m+1) ({Serverj},fwdmsg)at (q1, . . . , qj−1,5, qj+1, . . . , qn+m+1) These requirements express receptiveness obligations fulfilled by Tchat . For instance, the first requirement expresses that in the state 0of Clienti, join actions should be received by at least one server. Likewise, the second requirement expresses that the message forwarded to the chat by a server will be received by the clients. In this second requirement, it is assumed that some client is still in the chat (i.e. ∃i, n + 1 ≤i≤n+m:qi= 2). An example of a responsiveness requirement is the following (cf. Sect. 5.2): ({Serverj},join)∨({Serverj},leave)∨({Serverj},msg) at (q1, . . . , qj−1,0, qj+1, . . . , qn,...qn+m+1) This responsiveness requirement at state 0of Serverjprovides a choice concerning the server’s functionality: it can either coordinate joining or exiting actions from a client, or messages sent in the chat. As before for the server’s receptiveness requirement, it is assumed that some client is still in the chat (i.e. ∃i, n + 1 ≤i≤n+m:qi= 2). Another example of a responsiveness requirement is as follows (cf. Sect. 5.2): ({Arbiter},ask1)∨ · · · ∨ ({Arbiter},askn)at (q1, . . . , qn+m,0) This requirement applies when at least one server is asking for permission to forward the received message (i.e. ∃j, 1≤j≤n:qj= 3) and at least one client is in the chat (i.e. ∃i, n + 1 ≤i≤n+m:qi= 2). It makes an obligation for some of the servers to provide some of the required inputs for the arbiter. ut 5.4 Related Compatibility Notions In the literature, compatibility notions are often considered for systems built according to a specific synchronisation type. For instance, interface automata [7] and many others, like [10,19,24], consider synchronous products of composable I/O-transition systems with (binary) point-to-point communication, i.e. the synchronisation type is ([1,1],[1,1]). These papers moreover deal with the aspect of receptiveness only. We can say that a team automaton of type ([1,1],[1,1]) over a closed system of components A1and A2is receptive in the sense of Def. 9 iff A1and A2are compatible in the sense of [7] iff they are strongly compatible in the sense of [24] iff they are receptive in the sense of [1]. For open systems, the theory of interface automata relies on the optimistic approach. Two components are compatible if there exists a ‘helpful’ environment which avoids that the system can reach a communication error. As we have seen, synchronisation types define synchronisation policies uniquely only for closed systems, while for open systems there is still a possibility to restrict the set of transitions with external, non-communicating actions. Therefore, we can find an appropriate policy to make two components receptive iff they are compatible in the sense of [7]. Weak receptiveness corresponds to weak compatibility in [24] and is also captured by unspecified receptions compatibility in [13]. We are aware of only a few approaches that consider compatibility w.r.t. responsiveness. In [1], responsiveness is captured by deadlock-freeness and in [13] it is expressed by part of the definition of bidirectional complementarity compatibility which, however, does not support choice of inputs as we do. 5.5 Applications The contributions of this paper enable to explore component-based modelling and composition according to a wide range of synchronisation policies, not limited to the classical synchronous product, bringing upfront the communication requirements that must be fulfilled to derive a compliant system. We foresee many application areas where the perspective taken in this paper can play an important role to enhance the interaction and communication policies that are used. In Swarm Intelligence, for instance, agents communicate by means of sensors, actuators and connectors. Such sensors and actuators allow communication through the receiving and sending of signals. This communication often concerns a small selection of agents that changes over time, thus deviating from the synchronous product [25]. Being able to construct swarm networks that fulfil certain compatibility guarantees on alternative communication policies, like the ones considered in this paper, may represent an important step towards their satisfactory application. Another application area is Software Engineering. In particular, the provision of compatibility theories that go beyond limited formalisms like UML statecharts composed according to the synchronous product, will rise the expressibility level, thus widening the applicability scope to cover much more real-world situations. Also concurrent asynchronous programming languages can benefit from having a general theory of compatibility such as the one we envision in this paper. Erlang [26] is a prominent example: its asynchronous communication mode allows for a very flexible communication architecture, but if used incorrectly it may lead to invalid/suboptimal system implementations. To the best of our knowledge, current approaches follow a post-mortem approach to verify properties like liveness and safety of Erlang programs. Instead, correct-by-construction design might become applicable if the theories described in this paper were used in the specification of Erlang programs. Finally, the field of Web services may also be a nice application arena for the ideas put forward in this paper. Like in some of the previous examples, we are only aware of notions of compatibility for the composition of Web services defined over the restricted synchronous product [27,28]. 6 Conclusion We have investigated compatibility notions concerning receptiveness and responsiveness in the team automata framework. Team automata are characterised by the synchronisation policy they use to coordinate the components of a given system. There is a huge variety of possible synchronisation policies. The synchronisation types as we introduced them here support a systematic approach to the investigation of compatibility notions related to communication. To find appropriate compatibility notions, we first analysed what kind of communication requirements can occur when components are composed. We distinguished receptiveness and responsiveness requirements and we showed how such requirements can be systematically derived depending on a synchronisation type. A team automaton is compliant with a communication requirement if (groups of) components in the team issuing requests for communication can successfully find partners to join. If this is the case for all receptiveness (responsiveness) requirements, then the team automaton is receptive (responsive, respectively). Our approach is appropriate for both closed and open systems. A team automaton over an open system is itself a reactive component and thus gives rise to hierarchical composition. One of the next steps in our research will be to study compatibility in the context of hierarchical composition and of synchronisation policies that are not necessarily uniform but combine different synchronisation types. The latter would also concern an investigation of compatibility notions tailored to particular connectors as used, e.g., in BIP and Reo (cf. [29] for a comparison). Also the incorporation of asynchronous communication in synchronisation policies and the study of compatibility notions in this case [24, 30] is a topic for future research. Moreover, appropriate notions of equivalences and refinements for team automata and how they behave w.r.t. our receptiveness and responsiveness notions are interesting questions to consider. Acknowledgments We thank the reviewers for their comments. J. Carmona is supported by the Spanish Ministry for Economy and Competitiveness (MINECO) and the EU (FEDER funds) under grant COMMAS (TIN2013-46181-C2-1-R). References 1. J. Carmona and J. Cortadella. Input/Output Compatibility of Reactive Systems. In FMCAD’02, volume 2517 of LNCS, pages 360–377. Springer, 2002. 2. J. Carmona and J. Kleijn. Compatibility in a multi-component environment. Theor. Comput. Sci., 484:1–15, 2013. 3. N. A. Lynch and M. R. Tuttle. Hierarchical Correctness Proofs for Distributed Algorithms. In PODC’87, pages 137–151. ACM, 1987. 4. N. A. Lynch and M. R. Tuttle. An Introduction to Input/Output Automata. CWI Quarterly, 2(3):219–246, 1989. https://ir.cwi.nl/pub/18164. 5. C. A. Ellis. Team Automata for Groupware Systems. In GROUP’97, pages 415– 424. ACM, 1997. 6. M. H. ter Beek, C. A. Ellis, J. Kleijn, and G. Rozenberg. Synchronizations in Team Automata for Groupware Systems. Comput. Sup. Coop. Work, 12(1):21–69, 2003. 7. L. de Alfaro and T. A. Henzinger. Interface Automata. In ESEC/FSE’01, pages 109–120. ACM, 2001. 8. L. de Alfaro and T. A. Henzinger. Interface-Based Design. In Engineering Theories of Software Intensive Systems, volume 195 of NATO Science Series, pages 83–104. Springer, 2005. 9. L. Brim, I. Cerná, P. Vareková, and B. Zimmerova. Component-Interaction Automata as a Verification-Oriented Component-Based System Specification. ACM Softw. Eng. Notes, 31(2), 2006. 10. K. G. Larsen, U. Nyman, and A. Wąsowski. Modal I/O Automata for Interface and Product Line Theories. In ESOP’07, volume 4421 of LNCS, pages 64–79. Springer, 2007. 11. S. S. Bauer, P. Mayer, A. Schroeder, and R. Hennicker. On Weak Modal Compatibility, Refinement, and the MIO Workbench. In TACAS’10, volume 6015 of LNCS, pages 175–189. Springer, 2010. 12. D. Brand and P. Zafiropulo. On Communicating Finite-State Machines. J. ACM, 30(2):323–342, 1983. 13. F. Durán, M. Ouederni, and G. Salaün. A generic framework for n-protocol compatibility checking. Sci. Comput. Program., 77(7-8):870–886, 2012. 14. M. H. ter Beek, J. Carmona, and J. Kleijn. Conditions for Compatibility of Components: The Case of Masters and Slaves. In ISoLA’16, volume 9952 of LNCS, pages 784–805. Springer, 2016. 15. B. Jonsson. Compositional Specification and Verification of Distributed Systems. ACM Trans. Program. Lang. Syst., 16(2):259–303, 1994. 16. M. H. ter Beek and J. Kleijn. Team Automata Satisfying Compositionality. In FME’03, volume 2805 of LNCS, pages 381–400. Springer, 2003. 17. G. Gössler and J. Sifakis. Composition for component-based modeling. Sci. Comput. Program., 55:161–183, 2005. 18. M. H. ter Beek and J. Kleijn. Modularity for teams of I/O automata. Inf. Process. Lett., 95(5):487–495, 2005. 19. G. Lüttgen, W. Vogler, and S. Fendrich. Richer interface automata with optimistic and pessimistic compatibility. Acta Inf., 52(4-5):305–336, 2015. 20. A. Basu, M. Bozga, and J. Sifakis. Modeling Heterogeneous Real-time Components in BIP. In SEFM’06, pages 3–12. IEEE, 2006. 21. A. Arnold. Finite Transition Systems: Semantics of Communicating Systems. Prentice Hall, 1994. 22. R. Milner. Communication and Concurrency. Prentice Hall, 1989. 23. G. Engels and L. Groenewegen. Towards Team-Automata-Driven Object-Oriented Collaborative Work. In Formal and Natural Computing, volume 2300 of LNCS, pages 257–276. Springer, 2002. 24. R. Hennicker, M. Bidoit, and T.-S. Dang. On Synchronous and Asynchronous Compatibility of Communicating Components. In COORDINATION’16, volume 9686 of LNCS, pages 138–156. Springer, 2016. 25. T. Isokawa, F. Peper, M. Mitsui, J.-Q. Liu, K. Morita, H. Umeo, N. Kamiura, and N. Matsui. Computing by Swarm Networks. In ACRI’08, volume 5191 of LNCS, pages 50–59. Springer, 2008. 26. J. Armstrong. Erlang. Commun. ACM, 53(9):68–75, 2010. 27. M. H. ter Beek, A. Bucchiarone, and S. Gnesi. Web Service Composition Approaches: From Industrial Standards to Formal Methods. In ICIW’07. IEEE, 2007. 28. Q. Z. Sheng, X. Qiao, A. V. Vasilakos, C. Szabo, S. Bourne, and X. Xu. Web services composition: A decade’s overview. Inf. Sci., 280:218–238, 2014. 29. K. Dokter, S.-S. T. Q. Jongmans, F. Arbab, and S. Bliudze. Combine and conquer: Relating BIP and Reo. J. Log. Algebr. Meth. Program., 86(1), 2017. 30. J. L. Fiadeiro and A. Lopes. An interface theory for service-oriented design. Theor. Comput. Sci., 503:1–30, 2013.