Franco Barbanera

Ivan Lanese
email: ivan.lanese@gmail.com

Emilio Tuosto
email: emilio.tuosto@gssi.it

Choreography Automata

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Choreographies are gaining momentum in the design and implementation of distributed applications also in the ICT industrial sector. This is witnessed by the effort of defining standards for specification languages such as WS-CDL [START_REF] Kavantzas | Web services choreography description language version 1[END_REF] or BPMN [START_REF] Omg | Business Process Model and Notation (BPMN)[END_REF] as well as the recognition of choreographies as suitable approaches to describe modern architectures such as microservices [START_REF] Bonér | Reactive Microsystems -The Evolution Of Microservices At Scale[END_REF][START_REF] Ariola | Testing in the API Economy. Top 5 Myths[END_REF]. Choreographic approaches to the modelling, analysis, and programming of message-passing applications abound. For instance, in [START_REF] Krishna | Checking business process evolution[END_REF][START_REF] Autili | Chorevolution: Automating the realization of highly-collaborative distributed applications[END_REF] abstract models have been applied to verify and debug BPMN specifications. Also, behavioural types have been proposed as suitable formalisations of choreographies [START_REF] Honda | Multiparty asynchronous session types[END_REF] and for the analysis of properties such as liveness or deadlock freedom (e.g., [START_REF] Scalas | Less is more: multiparty session types revisited[END_REF][START_REF] Coppo | Global progress for dynamically interleaved multiparty sessions[END_REF] and the survey [START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF] to mention but few), while other approaches have considered syntax-free models [START_REF] Tuosto | Semantics of global view of choreographies[END_REF]. At a programming level, choreographic programming has been explored in [START_REF] Lanese | Bridging the gap between interaction-and process-oriented choreographies[END_REF][START_REF] Montesi | Choreographic Programming[END_REF].

A distinguished trait of choreographies is the coexistence of two distinct but related views of a distributed system: the global and the local views. The former is an abstraction that yields a holistic description of the system. A global view indeed describes the coordination necessary among the various components of the system "altogether". In contrast, the local views specify the behaviour of the single components in "isolation".

In this paper we revisit the use of finite state automata to formally specify (and analyse) global views of message-passing systems, following an intuition similar to conversation protocols (CP) [START_REF] Fu | Conversation protocols: A formalism for specification and verification of reactive electronic services[END_REF][START_REF] Bultan | Conversation specification: a new approach to design and analysis of e-service composition[END_REF][START_REF] Fu | Conversation protocols: a formalism for specification and verification of reactive electronic services[END_REF], a formalism where choreographies for asynchronous systems are described by means of Büchi automata. Our model, dubbed choreography automata (c-automata, for short), differs from CP in spite of some similarities. A comparison is given in § 6. The transitions of c-automata are labelled with interactions. As in most approaches, an interaction A-→B : m states that participant A sends message m to participant B, which in turn receives it. For instance, consider the c-automaton used to illustrate our model and as our working example through the paper. The c-automaton Cref specifies the coordination among participants C, S, and L whereby a request req from client C is served by server S which replies with a message (of type) res and logs some meta-information cnt on a service L (e.g., for billing purposes). Client C may acknowledge a response of S (i) with an ok message to restart the protocol, or (ii) by requiring a refinement of the response with a ref message, or else (iii) by ending the protocol with a bye message which S forwards to L. In the second case, S sends C either a noRef message if no refinement is possible or another res (with the corresponding cnt to L).

Note that Cref has nested as well as entangled loops. The support for entangled loops is a distinguished and expressive feature of c-automata, not present in many existing models of choreographies or multiparty session types (MST), and that we shall discuss in § 6.

We argue that c-automata provide a number of benefits. An advantage of c-automata is that finite state automata are well-known structures used both in theoretical and applied computer science. For instance, the c-automaton Cref above can be easily understood by practitioners while retaining rigour. Another advantage is that c-automata are syntax-independent; they do not rely on complex linguistic constructs (such as the process algebraic constructs usually adopted in behavioural types). More crucially, we can re-use well-known results of the theory of automata and formal languages (e.g., we use determinisation and trace equivalence) as well as related algorithms. We discuss these advantages more extensively in § 6.

Choreographies enable a so called top-down approach whereby local views can be projected from the global view. Projections are expected to reflect the global specification without spoiling communication soundness (e.g., deadlock freedom, liveness, etc.). These results do not hold in general. In fact, global views abstract away from "low level" peculiarities and projections may exhibit unintended behaviour.

The realisability of a global specification is a natural question to ask:

Can global views such as Cref be realised by distributed components C, S, and L coordinating with each other without intermediaries?

The answer to such question (obviously) depends on the communication infrastructure the distributed components use for the coordination. In fact, global views in general abstractly specify the coordination disregarding several details. For instance, the c-automaton Cref in ( 1) is oblivious of the communication infrastructure used by the participants to coordinate with each other. Are the communications among C, S, and L synchronous or asynchronous? In the latter case, are messages received in their sending order? How is the sequencing reflected at the local level? For instance, should the messages that C sends from state 3 in (1) be sent after L receives the message cnt from S? Tackling the realisability of global views is not a trivial endeavour. For instance, the recent analysis done in [START_REF] Scalas | Less is more: multiparty session types revisited[END_REF] highlights glitches in several projection operations of behavioural types. Also, some decidability results on the realisability of CPs [START_REF] Basu | Deciding choreography realizability[END_REF], the only other automata-based choreographic setting that we are aware of, have been recently proved erroneous [START_REF] Finkel | Synchronizability of communicating finite state machines is not decidable[END_REF].

One would also like to understand whether the distributed components realising a choreography enjoy nice communication properties, e.g., will a component ready to engage in a communication eventually progress? Will a message sent by a participant eventually be received? We will consider such problems, showing that a set of conditions we define on c-automata do guarantee the choreography both to be realisable and to enjoy a number of relevant communication properties such as liveness and deadlock freedom.

Contributions & Structure. After a preliminary section ( § 2) recalling the main notions we deal with in the paper, in § 3 we formalise c-automata and their projections.We adopt communicating systems [START_REF] Brand | On communicating finite-state machines[END_REF] (reviewed in § 2 ) for the local views of choreographies.

We consider both the case of synchronous and asynchronous communications for the local views. The projection from c-automata to communicating systems is defined in § 3 while in § 4 we define the class of well-formed c-automata for the synchronous case. There we show that, on well-formed c-automata, our notion of projection is correct (cf. Thm. 4.14) and guarantees liveness, lockand deadlock-freedom in the synchronous semantics (cf. Thm. 4.15). In § 5 we generalise the above results to the case of asynchronous communications (cf. Thms. 5.6 and 5.7). Concluding remarks, related and future work are discussed in § 6. Additional material and complete proofs can be found in [START_REF] Barbanera | Choreography automata[END_REF].

Some interesting technical points are worth noticing. Firstly, most of our constructions and results rely on basic notions of formal languages and automata theory. This greatly simplifies the presentation and the proofs. The generalisation from synchronous to asynchronous communications requires only a mild strengthening of our notion of well-formedness and no changes to c-automata or their projection. These are further advantages of the use of finite-state automata.

Preliminaries

A Labelled Transition System (LTS) is a tuple A = S, s 0 , L, → where -S is a set of states (ranged over by s, q, . . .) and s 0 ∈ S is the initial state; -L is a finite set of labels (ranged over by l, λ, . . .);

-→⊆ S × (L ∪ { ε }) × S is a set of transitions where ε ∈ L is a distinguished label.
We define a Finite-State Automaton (FSA) as an LTS where S is finite. We use the usual notation s 1 λ -→ s 2 for the transition (s 1 , λ, s 2 ) ∈-→, and s 1 -→ s 2 when there exists λ such that s 1 λ -→ s 2 , as well as -→ * for the reflexive and transitive closure of -→. The set of reachable states of

A is R(A) = { s | s 0 - → * s }.
Remark 2.1. Our definition of FSA omits the set of accepting states since we consider only FSAs where each state is accepting (which is the normal case in LTSs). We discuss this point further at the end of the paper.

We recall standard notions on LTSs.

Definition 2.2 (Traces and Trace equivalence).

A run of an LTS A = S, s 0 , L, → is a (possibly empty) finite or infinite sequence of consecutive transitions starting at s 0 . The trace (or word) w of a run (s i-1 λ i-1 ---→ s i ) 1≤i≤n of A is the concatenation of the labels of the run (assume n = ∞ if the run is infinite), namely w = λ 0 • λ 1 • • • λ n ; label ε, as usual, denotes the identity element of concatenation; if the run is empty then w = ε.

The language L(A) of A is the set of the traces of the runs of A. Two LTSs A and B are trace equivalent iff L(A) = L(B). Also, A accepts w if w ∈ L(A), A accepts w from s if w ∈ L( S, s, L, → ), and an s-run (resp. s-trace) of A is a run (resp. trace) of S, s, L, → .

The notion of language in the definition above includes infinite words; this extends the standard notion of language accepted by an FSA. In particular, we consider an infinite word to be accepted by an FSA if each of its prefixes is accepted in the standard way. This is equivalent to look at an FSA both as a standard FSA and as a Büchi automaton where all the states are final.

Definition 2.3 (Deterministic LTSs). An LTS

A = S, s 0 , L, → is deter- ministic if -it is ε-free, i.e.
there is no transition of the form q ε -→ q , and -whenever q λ -→ q 1 and q λ -→ q 2 then q 1 = q 2 . We denote the determinisation of A (i.e. the translation of a nondeterministic LTS/FSA to a deterministic one) as det(A) 4 .

We adopt communicating finite-state machines (CFSMs) [START_REF] Brand | On communicating finite-state machines[END_REF] to model the local behaviour of systems of distributed components. The following definitions are borrowed from [START_REF] Brand | On communicating finite-state machines[END_REF] and adapted to our context.

Let P be a set of participants (or roles, ranged over by A, B, etc.) and M a set of messages (ranged over by m, n, etc.). We take P and M disjoint. Definition 2.4 (Communicating system). A communicating finite-state machine (CFSM) is an FSA on the set

L act = {A B!m, A B?m | A, B ∈ P, m ∈ M} of actions. The subject of an output (resp. input) action A B!m (resp. A B?m) is A (resp. B). A CFSM is A-local if all its transitions have subject A.
A (communicating) system is a map S = (M A ) A∈P assigning an A-local CFSM M A to each participant A ∈ P such that P ⊆ P is finite and any participant occurring in a transition of M A is in P.

Note that CFSMs may contain ε-transitions. However, projection (see Def. 3.3 below) yields ε-free CFSMs.

Besides being a well-known and widely adopted model, CFSMs are equipped with both synchronous and asynchronous semantics. This enables a uniform treatment of both communication models. The use of CFMSs is also helpful to compare c-automata with other models which are projected on CFSMs as well, such as global graphs [START_REF] Lange | From communicating machines to graphical choreographies[END_REF] and some versions of global types [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF].

The synchronous semantics of communicating systems is an LTS where labels are interactions:

L int = {A-→B : m | A = B ∈ P and m ∈ M}
Definition 2.5 (Synchronous semantics). Let S = (M A ) A∈P be a communicating system where M A = S A , q 0A , L act , → A for each participant A ∈ P. A synchronous configuration of S is a map s = (q A ) A∈P assigning a local state q A ∈ S A to each A ∈ P. We denote q A by s(A) and may denote s by q.

The synchronous semantics of S is the transition system S s = S, q 0 , L int , → defined as follows -S is the set of synchronous configurations of S, as defined above, and q 0 = (q 0A ) A∈P ∈ S is the initial configuration

-q 1 A-→B: m -----→ q 2 if 1. q 1 (A) A B!m ---→ A q 2 (A) and q 1 (B) A B?m ---→ B q 2 (B), and 2. for all C = A, B, q 1 (C) = q 2 (C).
In this case, we say that q 1 (A)

A B!m ---→ A q 2 (A) and q 1 (B) A B?m ---→ B q 2 (B) are component transitions of q 1 A-→B: m -----→ q 2 . -q 1 ε - → q 2 if q 1 (A) ε - → A q 2 (A)
, and for all B = A, q 1 (B) = q 2 (B).

Note that ε-transitions in the semantics of a communicating system are induced by those of the constituent CFSMs. Also, S s is finite; in fact, it is in general a non-deterministic automaton on the alphabet L int .

As one would expect, the notion of synchronous semantics is invariant under language equivalence of CFSMs.

Proposition 2.6. Let S = (M A ) A∈P and S = (M A ) A∈P be two communicating systems. If L(M A ) = L(M A ) for all A ∈ P then L( S s ) = L( S s ).
The asynchronous semantics of systems is defined in terms of transition systems which keep track of both the state of each machine and the content of unbounded FIFO queues b AB which are associated to each channel (A, B) ∈ C, where C = P × P \ {(A, A) A ∈ P}. The queue b AB is where M A puts the messages to M B and from which M B consumes the messages from M A . To avoid cumbersome parenthesis, we write A B ∈ C for (A, B) ∈ C. Definition 2.7 (Asynchronous semantics). Let S = (M A ) A∈P be a communicating system where M A = S A , q 0A , L act , → A for each participant A ∈ P. An asynchronous configuration of S is a pair s = q ; b where q = (q A ) A∈P with q A ∈ Q A and b = (b AB ) AB∈C with b AB ∈ M * ; we write s(A) for q(A) and denote by ε the empty queue. The asynchronous semantics of S is the transition system S a = S, s 0 , L act , → defined as follows -S is the set of asynchronous configurations of S and s 0 = q 0 ; b is the initial configuration where q 0 = (q 0A ) A∈P and all the queues are empty. s l -→ s if s = q ; b , s = q ; b and either (1) or (2) below holds:

1. l = A B!m and s(A) l -→ A s (A) and a. s(C) = s(C) ∀C = A ∈ P and b. b A B = b A B .m and c. b C D = b C D for all C D ∈ C, C D = A B 2. l = A B?m and s(B) l -→ B s (B) and a. s (C) = s(C) ∀C = B ∈ P and b. b A B = m.b A B and c. b C D = b C D for all C D ∈ C, C D = A B
In the first (resp. second) case we say that s(A) The asynchronous semantics is also invariant under equivalence of CFSMs.

A B!m ---→ A s (A) (resp. s(B) A B?m ---→ B s (B)) is a component transition of s A-→B: m -----→ s . -q ; b ε - → q ; b if q(A) ε - → q (A)
Proposition 2.8. Let S = (M A ) A∈P and S = (M A ) A∈P be two communicating systems. If L(M A ) = L(M A ) for all A ∈ P then L( S a ) = L( S a ).
For both the synchronous and the asynchronous semantics we restrict the attention to fair runs. An infinite run is fair if each transition which is continuously enabled is taken in a finite number of steps. A finite run is always fair.

We are interested in standard properties of communicating systems which we now recall. Definitions are alike in the synchronous and asynchronous semantics, hence, to avoid repetitions, below stands for a or s .

Definition 2.9 (Communication properties). Let S = (M A ) A∈P be a communicating system. i) Liveness: S is live if for each configuration s ∈ R( S ), each A ∈ P and each outgoing transition t from s(A) in M A there exists a run of S from s including a transition which has t as component transition. ii) Lock freedom: A configuration s ∈ R( S ) is a lock if there is A ∈ P with an outgoing transition t from s(A) in M A and there exists a run of S starting from s, maximal w.r.t. prefix order, and containing no transition

t involving A. System S is lock-free if for each s ∈ R( S ), s is not a lock. iii) Deadlock freedom: A configuration s ∈ R( S ) is a deadlock if
s has no outgoing transitions in S and there exists A ∈ P such that s(A) has an outgoing transition in M A . System S is deadlock-free if for each s ∈ R( S ), s is not a deadlock.

Liveness, as in [START_REF] Padovani | Typing liveness in multiparty communicating systems[END_REF], establishes the progress of communicating systems we are interested in. Lock freedom casts in our framework the idea that, similarly to [START_REF] Kobayashi | Type-Based Information Flow Analysis for the Pi-Calculus[END_REF][START_REF] Kobayashi | A Partially Deadlock-Free Typed Process Calculus[END_REF], certain communications happen, whereas deadlock freedom extends the definition of deadlock in [START_REF] Cécé | Verification of programs with half-duplex communication[END_REF] to a setting which can be synchronous or asynchronous (as done also in [START_REF] Lange | From communicating machines to graphical choreographies[END_REF][START_REF] Tuosto | Semantics of global view of choreographies[END_REF]).

Choreography Automata

We introduce choreography automata (c-automata) as an expressive and flexible model of global specifications, following the styles of conversation protocols [START_REF] Fu | Conversation protocols: a formalism for specification and verification of reactive electronic services[END_REF], choreographies [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF][START_REF] Kavantzas | Web services choreography description language version 1[END_REF][START_REF] Omg | Business Process Model and Notation (BPMN)[END_REF], global graphs [START_REF] Tuosto | Semantics of global view of choreographies[END_REF] and multiparty session types [START_REF] Carbone | Structured communicationcentred programming for web services[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF]. As customary in choreographic frameworks, we show how to project c-automata on local specifications. As anticipated, our projection yields a system of CFSMs formalising the local behaviour of the participants of a choreography.

C-automata (ranged over by CA, CB, etc.) are FSAs with labels in L int .

Definition 3.1 (Choreography automata). A choreography automaton (cautomaton) is an FSA on the alphabet L int . Elements of L * int are choreography words, subsets of L * int are choreography languages.

Remark 3.2. Def. 3.1 admits non-deterministic c-automata. This does not increase the expressiveness of our framework. In fact, (i) the notions that we use for our results rely on traces and (ii) our projection operation (cf. Def. 3.3) is insensitive to non-determinism (cf. Prop. 3.6). Non-deterministic specifications are however desirable since they are easier to attain for the designer.

Given a c-automaton, our projection operation builds the corresponding communicating system consisting of the set of projections of the c-automaton on each participant, each projection yelding a CFSM. Hereafter, P ⊆ P is the set of participants of c-automata; note that P is necessarily finite. Definition 3.3 (Automata Projection). The projection on A of a transition t = q λ -→ q of a c-automaton, written t ↓ A , is defined by:

t ↓ A =      q A C!m ---→ q if λ = B-→C : m and B = A q B A?m ---→ q if λ = B-→C : m and C = A q ε - → q otherwise
The projection of a c-automaton CA = S, q 0 , L int , → on a participant A ∈ P, denoted CA ↓ A , is obtained by determinising and minimising up-to-language equivalence the intermediate automaton

A A = S, q 0 , L act ∪ { ε }, { (q λ -→ q ) ↓ A | q λ -→ q }
The projection of CA, written CA ↓, is the communicating system (CA ↓ A ) A∈P .

The projection function trivially extends to choreography words and languages.

The projection defined above, apart for determinisation and minimisation, is essentially homomorphic, as most of the projections in the literature. Other approaches such as [START_REF] Dalla Preda | Dynamic choreographies: Theory and implementation[END_REF][START_REF] Francalanza | Reversible choreographies via monitoring in erlang[END_REF] add hidden communications to be able to deal with larger classes of choreographies. We prefer the former approach for its simplicity. Hidden communications can however be added directly at the choreographic level as proposed in [START_REF] Lanese | Amending choreographies[END_REF].

It is a simple observation that the projection on A of CA is A-local, deterministic and hence ε-free. Thanks to the properties of determinisation and minimisation (as, e.g., in the partition refinement algorithm [START_REF] Paige | Three Partition Refinement Algorithms[END_REF]), the states of CA ↓ A are sets of states of CA.

Example 3.4 (Projections of Cref). The projections of our working example are The following proposition relates the language of the projection with the language of the original automaton.

{ 0 } { 1 } { 2, 3 } { 4 } { 5, 6 } Cref ↓C C S!req S C?res C S!ref C S!bye C S ! o k S C?res S C?noRe f { 0 } Cref ↓S { 1 } { 2 } { 3 } { 4 } { 5 } { 6

Well-formed Choreography Automata

To ensure that the communicating system obtained by projection of a c-automaton is well-behaved, some conditions are necessary. Since the conditions depend on the used communication infrastructure, we consider first synchronous communication, leaving to § 5 the case of asynchronous communication.

Definition 4.1 (Concurrent transitions). Let CA = S, q 0 , L, → . Two transitions q l 1 -→ q 1 and q l 2 -→ q 2 are concurrent iff there is a state q ∈ S and transitions q 1 l 2 -→ q and q 2 l 1 -→ q .

Well-branchedness (cf. Def. 4.6) is a key notion which intuitively states that each participant is aware of the choices made in the choreography when its behaviour depends on those choices. The awareness of choice is checked on spans, namely pairs of runs that may constitute alternative branches of choices. Spans are formalised building on the notion of candidate branch which, in turn, is defined in terms of pre-candidate branch. Definition 4.2 (Candidate q-branch). Let q be a state of a c-automaton CA. A pre-candidate q-branch of CA is a q-run of CA such that each cycle has at most one occurrence within the whole run (i.e. any subsequence of the form q -→ . . . -→ q, where q occurs only at the beginning and at the end of the subsequence, is not present more than once in the run). A candidate q-branch is a maximal pre-candidate q-branch with respect to prefix order.

We often refer to a (pre-)candidate q-branch simply as "(pre-)candidate of q". Due to the condition about cycles in Def. 4.2, the following holds trivially.

Fact 1. Given a state q of a c-automaton CA, the set of its pre-canditates is finite, and so is, a fortiori, that of its candidates. Definition 4.4 (q-span). Given a state q of a c-automaton CA, a pair (σ, σ ) of pre-candidate q-branches of CA is a q-span if σ and σ are either cofinal, with no common node but q and the last one; or candidate q-branches with no common node but q; or a candidate q-branch and a loop on q with no other common nodes.

A participant A ∈ P chooses at a q-span (σ, σ ) if the first transition of both σ and σ has A as sender.

Example 4.5 (Spans of Cref). The states with spans of our working example are 3 and 4. A span from 3 is (π a , π f ), where π a and π f are as in Fig. 1. Indeed, π a and π f are cofinal (in 2) pre-candidates of 3 with no common states but 3 and 2. Participant C chooses at (π a , π f ). The pair (π b , π d ), instead, is not a span from 3, since π b and π d are maximal, but share other nodes than 3.

Intuitively, a choice is well-branched when the participants other than the one opting for alternative runs either behave uniformly in each branch, or can ascertain which branch has been chosen from the messages they receive. Definition 4.6 (Well-branchedness). A c-automaton CA is well-branched if for each state q in det(CA) and A ∈ P sender in a transition from q, all of the following conditions must hold:

(1) all transitions from q involving A, have sender A;

(2) for each transition t from q whose sender is not A and each transition t from q whose sender is A, t and t are concurrent (3) for each q-span (σ, σ ) where A chooses at and each participant B = A ∈ P, the first pair of different labels on the runs σ ↓ B and σ ↓ B (if any) is of the form (C B?m, D B?n) with C = D or m = n.

We dub A a selector at q.

In the above definition loops are taken into account in item (3) since the notion of span is defined in terms of candidate branch. The latter is a maximal run where cycles can be considered at most once, as shown in Example 4.3.

In case of a nondeterministic c-automaton, the conditions of Def. 4.6 are checked after the c-automaton has been determinised. In fact, recalling Remark 3.2, we consider properties of languages of c-automata, and determinisation, as well as minimisation, of FSA preserve languages. Also, both operations preserve the system resulting from projection (cf. Prop. 3.6). (Observe that here we exploit classical results of automata theory.) Also, by Fact 1 and the obvious decidability of the conditions of Defs. 4.4 and 4.6 we get Fact 2. Well-branchedness is a decidable property.

Example 4.7 (Well-branchedness of Cref). All the states of Cref satisfy the conditions of Def. 4.6; the only non-trivial cases are states 3 and 4. Condition (1) holds for C, which is the selector of the choice at 3, and for S, which is the selector of the choice at 4; condition (2) holds vacuously, and condition (3) holds for both S and L in all the spans from 3 and from 4. For instance, in the span (π a , π f ) from 3, described in Example 4.5, the first actions of S on π a and π f are the inputs from C which have different messages, whereas, for what concerns L, the condition holds vacuously. As a matter of fact, since π a and π f are cofinal in 2, the well-branchedness conditions on state 2 do guarantee L to behave properly afterwards, independently on whether π a or π f have been followed before.

Condition [START_REF] Ariola | Testing in the API Economy. Top 5 Myths[END_REF], vacuously true in our working example, is needed when multiple participants act as sender in the same state: this ensures that the only possibility is that actions of different participants are concurrent so that possible choices at a state are not affected by independent behaviour.

We add a further condition to rule out c-automata having consecutive transitions involving disjoint participants and not actually concurrent.

Definition 4.8 (Well-sequencedness). A c-automaton CA is well-sequenced if for each two consecutive transitions q

A-→B: m -----→ q C-→D: n -----→ q either they share a participant, that is {A, B} ∩ {C, D} = ∅, or they are concurrent, i.e. there is q such that q C-→D: n -----→ q A-→B: m -----→ q .

Notice that, by finiteness of the transition relation of c-automata, we get Fact 3. Well-sequencedness is a decidable property.

Notation. For the sake of readability, a well-sequenced c-automaton can be represented by omitting, for each diamond, two of its consecutive transitions. We call such representation compact. Notice that, given a compact representation, it is always possible to recover the original c-automaton. So far and hereafter we assume that all c-automata are compactly represented.

Example 4.9 (Well-sequencedness of Cref). It is not difficult to check that Cref is well-sequenced because the first condition of Def. 4.8 holds for any pair of consecutive transitions in Cref.

0 1 2 A - → B : a C - → D : c C-→D : c 0 1 2 3 A - → B : a C - → D : c C-→D : c C - → D : c A - → B : a 0 1 2 3 4 A - → B : a C - → D : c C-→D : c C - → D : c A - → B : a C - → D : c A - → B : a (a) (b) (c)
Fig. 2. Failure of well-sequencedness completion.

Well-sequencedness is necessary to establish a precise correspondence between the language of a c-automaton and of its projection (cf. Thm. 4.14 and the discussion following it).

Remark 4.10. We show that not all c-automata can be "completed" to wellsequenced ones. Consider the c-automaton of Fig. 2(a), which is not well-sequenced because of the transitions from state 0 to state 1 and from state 1 to 2. By "completing the diamond" for such transitions (i.e., by adding the new state 3 and the transitions 0 C-→D: c -----→ 3 and 3 A-→B: a -----→ 2) we obtain the c-automaton of Fig. 2(b). This is still not well sequenced, because of the transitions 3 A-→B: a -----→ 2 and 2 C-→D: c -----→ 0. So we try to make it well-sequenced by completing the diamond once again and obtain the c-automaton of Fig. 2(c). The resulting c-automaton is still not well-sequenced, because of the transitions 4

A-→B: a -----→ 0 and 0 C-→D: c -----→ 3.

Again a vain attempt, because of the transitions 5

A-→B: a -----→ 3 and 3 C-→D: c -----→ 4. It is immediate to check that we could go on indefinitely.

It is impossible to complete the initial c-automaton since the intended completed automaton should generate a non-regular language (since it should generate strings with a number of C-→D : c interactions which is, roughly, double of the number of A-→B : a interactions). It would hence be interesting to know whether, in case the expected completed interaction language of a c-automaton is regular and prefix-closed, it is possible to generate it also by means of a well-sequenced c-automaton. It would be also interesting to establish a condition on cycles (if any) that guarantees the effectiveness of the completion of a c-automaton. We leave these questions for future work.

We show a closure property of the languages of well-sequenced c-automata. is the concurrency closure of L.

The above relation is reminiscent of the swapping relation introduced in [START_REF] Carbone | Deadlock-freedom-by-design: multiparty asynchronous global programming[END_REF], with similar aims. Proposition 4.12. Let CA be a well-sequenced c-automaton. Then L(CA) is concurrency closed, i.e. L(CA) = close(L(CA)).

Notice that the converse of the above proposition does not hold in general. In fact, consider the following c-automaton

0 1 CA 2 3 4 A-→ B : a C-→ D : c C-→D : c A-→B : a we can check that L(CA) = close(L(CA)) but CA is not well-sequenced.
The notion of well-formedness below sums up the requirements needed in order for a c-automaton to be projected to a well-behaved communicating system. Definition 4.13 (Well-formedness). A c-automaton is well-formed if it is both well-branched and well-sequenced.

The next result in Thm. 4.14 establishes that the language of a well-formed c-automaton coincides with the language of the communicating system obtained by projection. This provides a correctness criterion for our projection operation. Notice that well-formedness is a necessary condition for the theorem above. It is in fact easy to check that

(C-→D : m)(A-→B : n) ∈ L( CA ↓ s ) and (C-→D : m)(A-→B : n) ∈ L(CA)
when CA is one of the c-automata (a), (b) or (c) of Fig. 3. In particular, (a) is not well-sequenced whereas (b) and (c) are not well-branched: for (b), item (2) of well-branchedness (Def. 4.6) does not hold; (c) instead violates item (3).

We can now show that the projections of well-formed choreography automata enjoy the communication properties of Def. 2.9.

Theorem 4.15. Given a well-formed c-automaton CA, its projection (CA ↓ A ) A∈P is live, lock-free, and deadlock-free with respect to the synchronous semantics.

Asynchronous Communications

We now transfer the results of the previous sections to the asynchronous semantics of communicating systems (Def. 2.7). Remarkably, the semantics does not affect the definition of c-automata (and of projections) since it is independent of the communication model. Hence, any result depending only on the definition of c-automata still holds. Well-sequencedness instead needs updating.

Definition 5.1 (Asynchronous well-sequencedness). A c-automaton is asynchronously well-sequenced if for each two consecutive transitions q

A-→B: m -----→ q C-→D: n -----→ q either
the sender of the second transition occurs in the first one, that is C ∈ {A, B}, or they are concurrent, i.e. there is q such that q C-→D: n -----→ q A-→B: m -----→ q .

Asynchronous well-sequencedness (Def. 4.8) implies the synchronous one. Indeed, asynchronous well-sequencedness requires either two transitions to be concurrent or that the sender of the second transition occurs in the first one. The latter condition is weaker than having disjoint participants as required in the synchronous case. Note that our working example is well-sequenced but not asynchronously well-sequenced (because e.g., of transitions 2 S-→L: cnt -----→ 3 C-→S: bye ------→ 5). Thus, we now consider it as the compact representation of the actual c-automaton according to Notation on page 11.

Unlike well-sequencedness, the notion of well-branchedness has not to be changed in case asynchronous communications are considered. So, in the asyncronous setting, we define asynchronous well-formedness as the conjunction of asynchronous well-sequencedness (Def. 5.1) and well-branchedness (Def. 4.6).

The correspondence result between the semantics of a c-automaton and of its projection requires to decide which actions to observe on the projection. Indeed, in a c-automaton, each interaction is seen as an atomic event, while in the asynchronous semantics of communicating systems each interaction corresponds to two events: a sending event and a receving event. We opt to observe sending events only because (internal) choices are determined by sending events. This decision also plays well with the notion of well-branchedness, where most of the conditions concern sender participants. Other possible options are discussed in [START_REF] Lanese | Bridging the gap between interaction-and process-oriented choreographies[END_REF], in a process algebraic setting. This idea is formalised by sender traces. Definition 5.2 (Sender traces). The sender traces L ! (S) of a communicating system S are obtained from its asynchronous traces by replacing each output label A B!m with A-→B : m and each input label A B?m with ε.

The modification of well-sequencedness for the asynchronous case does imply that we need to "update" the definition of concurrency closure as well.

Definition 5.3 (Asynchronous concurrency closure). The asynchronous swap relation on choreography words is the smallest pre-order ≤ satisfying

w(A-→B : m)(C-→D : n)w ≤ w(C-→D : n)(A-→B : m)w
where C / ∈ {A, B}.

The downward closure of a choreography language L with respect to ≤

closea(L) = { w ∈ Lint ∃w ∈ L. w ≤ w }
is the asynchronous concurrency closure of L.

The condition for asynchronous concurrency closure is weaker than the one in the synchronous case. This is due to the fact that sender-traces must be closed under asynchronous concurrency (cf. Lemma 5.4 below), so to guarantee that the traces of an automaton do coincide with the sender-traces of its projection (Thm. 5.6 below). We discuss such a necessity with an example after Thm. 5.6. We now proceed to prove the correctness of projection for asynchronous systems. We will reduce it to the corresponding result for synchronous systems (Thm. 4.14). This is done by showing that all asynchronous runs are pairable (see below), that is they can be put in a suitable normal form which directly corresponds to a synchronous run. Notably, such a result is false for c-automata which are not asynchronously well-formed. Definition 5.5 (Pairable runs). Let CA be a c-automaton. A run σ in CA ↓ a is paired into a run σ in CA ↓ a iff they are coinitial, produce the same sender trace, and each output A B!m in σ is immediately followed by the corresponding input A B?m. A run σ is pairable if it is paired into a run σ . Theorem 5.6. Let CA be an asynchronously well-formed c-automaton.

L ! ( CA ↓ a ) = L(CA)
Similarly to Thm. 4.14, asynchronous well-formedness is a necessary condition for Thm. 5.6. Examples (b) and (c) of Fig. 3 work the same also for the asynchronous case, since we do not changed the definition of well-branchedness. We changed instead the definition of well-sequencedness to a stricter version and the c-automaton (a) of Fig. 3 is hence not enough to show the necessity of asyncronous well-sequencedness; this can however be easily done using the following c-automaton which is well-sequenced but not asynchronouly well-sequenced

0 1 CA 2 A-→B : m C-→B : m
Since outputs of asynchronous CFSMs can always be fired, there is a run of the projected system beginning with C B!m and producing the sender trace (C-→B : m)(A-→B : m) ∈ L ! ( CA a ) which trivially does not belong to L(CA) because the interactions cannot be swapped (cf. Def. 5.3).

The communication properties for projected systems can also be obtained.

Theorem 5.7. Given an asynchronous well-formed c-automaton CA, its projection (CA ↓ A ) A∈P is live, lock-free, and deadlock-free with respect to the asyncronous semantics.

Conclusion, Related Work and Future Work

We introduced a model of choreographies based on FSAs whose transitions are labelled by interactions. We showed relevant results both for a synchronous and an asynchronous underlying communication infrastructure. We established a correspondence between the language of an automaton and the one of its projection, as well as proofs of liveness, lock, and deadlock freedom for the latter.

The adoption of an automata-based model brings in two main benefits. Firstly, the constructions that we provided are based on set-theoretic notions and are syntax-independent. This contrasts with syntax-driven models (such as behavioural type systems [START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF]) where expressiveness may be limited and definitions may be more complex due to syntactic reasons. E.g., the example in § 1 cannot be modelled in many behavioural type systems since entangled loops cannot be represented using a recursion operator. Secondly, we can re-use well-known results of the theory of automata (e.g., we used notions of trace equivalence and determinisation) and related tools.

Related work

Automata-based models for specifying the local behaviour of distributed compontents are commonplace in the literature (see e.g., [START_REF] Brand | On communicating finite-state machines[END_REF][START_REF] De Alfaro | Interface automata[END_REF]). Less so is for the global specifications of choreographies: to the best of our knowledge, the conversation protocols (CP) in [START_REF] Fu | Conversation protocols: A formalism for specification and verification of reactive electronic services[END_REF][START_REF] Fu | Conversation protocols: a formalism for specification and verification of reactive electronic services[END_REF][START_REF] Basu | Deciding choreography realizability[END_REF] (and references therein) are the only such model in the literature. The realisability of CP has been first studied in [START_REF] Fu | Conversation protocols: a formalism for specification and verification of reactive electronic services[END_REF]; this is indeed the work closest to ours. Conversation protocols are non-deterministic Büchi automata whose labels resemble our interactions (barred the fact that, contrarily to our formalism, in [START_REF] Fu | Conversation protocols: a formalism for specification and verification of reactive electronic services[END_REF] the sender and the receiver of each message are determined by its content). Our c-automata are basically finite-state automata where infinite words can be taken into account by looking at them as Büchi automata where all states are actually final. It is not immediate to provide a detailed comparison between conversation protocols and c-automata because their semantics and underlying communication models differ. As for the communication model, conversation protocols are realised in a subclass of CFSMs (cf. Section 5 of [START_REF] Fu | Conversation protocols: a formalism for specification and verification of reactive electronic services[END_REF]), whereas we consider the unrestricted model of CFSMs, as well as a synchronous version of it. Concerning the semantics, Definition 4 (item 3(b)) of [START_REF] Fu | Conversation protocols: a formalism for specification and verification of reactive electronic services[END_REF] restricts the runs to those where all messages in queues are eventually consumed, that is they require by definition a form of liveness. Instead, one of our goals is to identify conditions that guarantee relevant liveness properties. We prove them in Theorem 5.7, and in Prop. D.1 in [START_REF] Barbanera | Choreography automata[END_REF] we prove the exact property assumed in [START_REF] Fu | Conversation protocols: a formalism for specification and verification of reactive electronic services[END_REF]. The realisability conditions of conversation protocols are lossless join, synchronous compatibility, and autonomy. Those conditions cannot easily be compared with well-formedness, due to the differences in the models and in the semantics. Furthermore, the style of the conditions is very different, and it also induces very different proof strategies in many cases. In particular, our well-sequencedness is checked on pairs of consecutive transitions and well-branchedness on pairs of coinitial paths; lossless join is a global property, that is a condition on the automaton consisting of the product of the languages of the local projections;

synchronous compatibility is defined in terms of pairs of traces in the projection but verified with an algorithm that checks a global property of an automata costruction, and the same holds for autonomy.

Thus, while the conditions capture similar intuitions, a detailed comparison is very hard. When restricting to the common part of the two models, well-branchedness implies autonomy while the opposite does not hold. Indeed, by well-branchedness the selector is output-ready (according to the terminology in [START_REF] Fu | Conversation protocols: a formalism for specification and verification of reactive electronic services[END_REF]), while any other participant either behaves uniformly in each branch (and is thus either inputready or output-ready or termination-ready) or it is made aware of the choice by distinct inputs (that is it is input-ready). In all the cases autonomy is satisfied.

In the other direction, a choice between traces (A-→B : l)(B-→C : n)(C-→D : w) and (A-→B : r)(B-→C : n)(C-→D : z) satisfies autonomy but not well-branchedness.

As for lossless join, we do not assume it. Actually, it is equivalent to one of our results, namely the correctness of the projection in the synchronous case (Thm. 4.14). Such a result is also used in the asynchronous case (Thm. 5.6), which is proved by reduction to the synchronous one via paired runs. We leave a detailed comparison of the two sets of constraints, in a common setting, for future work. Later works on CP (see, e.g., [START_REF] Basu | Deciding choreography realizability[END_REF]) changed the approach and relied on model checking to show realisability instead of well-formedness conditions. Unfortunately, some of their main decidability results were flawed [START_REF] Finkel | Synchronizability of communicating finite state machines is not decidable[END_REF].

Conditions similar to well-branchedness and well-sequencedness do naturally arise in investigations related to choreoghraphies and their realisability. A unique sender driving a choice is a condition present in several multiparty session types formalisms ( [START_REF] Honda | Multiparty asynchronous session types[END_REF] and [START_REF] Coppo | Global progress for dynamically interleaved multiparty sessions[END_REF] to cite just a couple of them), global graphs formalisms [START_REF] Tuosto | Semantics of global view of choreographies[END_REF], choreography languages in general (for instance see the notion of dominant role in [START_REF] Qiu | Towards the theoretical foundation of choreography[END_REF]). Conditions related to item (3) of Def. 4.6 can also be found in multiparty session types formalisms [START_REF] Severi | Observational Equivalence for Multiparty Sessions[END_REF] or in conversation protocols, as discussed above. Also, notions close to well-sequencedness turn out to arise quite naturally in "well-behaved" choreographies (see for instance the notion of well-informedness of [START_REF] Bultan | Specification of realizable service conversations using collaboration diagrams[END_REF] in the context of collaboration diagrams).

Similarly to what discussed in Remark 4.10, some approaches propose techniques to fix choreographies which are not well-behaved. This issue is considered in some multiparty session types [START_REF] Bocchi | Three algorithms and a methodology for amending contracts for choreographies[END_REF][START_REF] Bocchi | Amending contracts for choreographies[END_REF], in algebraic and automata-based frameworks for choreographies [START_REF] Lanese | Amending choreographies[END_REF][START_REF] Basu | Automated choreography repair[END_REF] as well as in the choreographic middleware ChoreOS [START_REF] Autili | Choreography realizability enforcement through the automatic synthesis of distributed coordination delegates[END_REF][START_REF] Autili | Choreosynt: enforcing choreography realizability in the future internet[END_REF]. While they consider different conditions than ours, trying to adapt their approaches to our setting is an interesting item for future work.

As said, most approaches are not based on automata. For instance, [START_REF] Qiu | Towards the theoretical foundation of choreography[END_REF][START_REF] Lanese | Bridging the gap between interaction-and process-oriented choreographies[END_REF][START_REF] Deniélou | Dynamic multirole session types[END_REF]] use algebraic operators to build larger choreographies from smaller ones, and give conditions on such operations ensuring that the resulting choreography is "well-behaved". This technique is not applicable in our case, since, like most works on automata, we do not consider an algebra to build automata.

While the main aim of c-automata is to provide a choreography model based on FSAs, we remark here that it is rather expressive and complements existing models of choreographies or multiparty session types (MST). In particular, the expressive power of c-automata is not comparable with the one of the MST in [START_REF] Scalas | Less is more: multiparty session types revisited[END_REF], which subsumes most systems in the literature. More precisely, the c-automaton Cref in § 1 cannot be syntactically written in [START_REF] Scalas | Less is more: multiparty session types revisited[END_REF] due to the two entangled loops. That example cannot be expressed in global graphs [START_REF] Tuosto | Semantics of global view of choreographies[END_REF] either, again due to the intersecting loops. We note that the infinite unfolding of the c-automaton is regular and therefore it would fit in the session type system considered in [START_REF] Severi | On sessions and infinite data[END_REF]. However, this type system has not been conceived for choreographies (it is a binary session type system) and does not allow non-determinism.

On the other side, examples such as [45, Ex. 2, Fig. 4] cannot be written in our model (since we expect the same roles to occur in branches which are coinitial, branches inside loops require that all participants in a loop are notified when the loop ends). We conjecture that a refinement of well-branchedness is possible to address this limitation. Global graphs are another model of global specifications. Their advantage is that they feature parallel composition, which c-automata lack. We note however that one could use the classical product of automata on c-automata to model parallel composition in the case where the two branches have disjoint sets of participants (as typically assumed in MST with parallel composition). Mapping global graphs without parallel composition into c-automata is trivial. The same considerations apply to choreography languages where possible behaviours are defined by a suitable process algebra with parallel composition such as [START_REF] Lanese | Bridging the gap between interaction-and process-oriented choreographies[END_REF][START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF].

Future work One of the main motivations to develop a choreography model based on automata was to lift the compositional mechanism discovered in [START_REF] Barbanera | Connecting open systems of communicating finite state machines[END_REF] on CFSMs to global specifications, in such a way that composition of global specifications preserves well-formedness. This is the problem we are currently addressing.

An interesting future development is also to adopt Büchi automata as cautomata. This extension is technically straightforward (just add accepting states to Def. 3.1 and define ω-languages accordingly), but it probably impacts greatly the underlying theory. An interesting yet not trivial effort is the identification of well-formedness conditions on this generalised class of c-automata that guarantee a precise correspondence with the ω-languages of the projections.

The interplay between FSAs and formal languages could lead to a theory of projection of choreographies based on languages instead of automata. For instance, one could try to characterise the languages accepted by well-formed c-automata, similarly to what done in [START_REF] Alur | Inference of Message Sequence Charts[END_REF][START_REF] Lohrey | Safe Realizability of High-Level Message Sequence Charts[END_REF][START_REF] Tuosto | Semantics of global view of choreographies[END_REF]. In those approaches global specifications are rendered as partial orders and the distributed realisability is characterised in terms of closure properties of languages.

A final direction for future work concerns the implementation of tool support for the approach. We are currently working in this direction. A very preliminary and partial implementation by Simone Orlando and Ivan Lanese is available at https://github.com/simoneorlando/Corinne.

C

  -→S : req S-→C : res S-→L : cnt C-→S : ref C-→S : ok S-→C : res S-→C : noRef C-→S : bye S-→L : bye

  for some A ∈ P and for all B = A, q(B) = q (B), and b = b . State q A keeps track of the state of the machine M A and buffer b AB keeps track of the messages sent from A to B (and not yet received by B). In a transition s A B!m ---→ s , participant A adds message m in the queue of the channel A B and symmetrically, in a transition s A B?m ---→ s , participant B consumes message m from the top of the queue of the channel A B. In both cases, any machine or queue not involved in the transition is left unchanged.

  For instance, Cref ↓ C is obtained by determinising (minimisation is the identity in this case) the following intermediate automaton obtained as described in Def.3.3.

Proposition 3 . 5 .

 35 For all c-automata CA and A ∈ P, L(CA↓ A ) = L(CA) ↓ A .The projection operation is well-behaved with respect to trace equivalence. Proposition 3.6. If CA and CA are trace-equivalent c-automata then CA ↓ A and CA ↓ A are isomorphic for each participant A ∈ P.

Example 4 . 3 (CSCSFig. 1 .

 431 Fig. 1. Runs of Cref.

Definition 4 . 11 (Fig. 3 .

 4113 Fig. 3. Well-formedness is necessary for Thm. 4.14.

Theorem 4 .

 4 [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF]. L(CA) = L( CA ↓ s ) for any well-formed c-automaton CA.

Lemma 5 . 4 .

 54 Let CA be a c-automaton. Then L ! ( CA ↓ a ) = close a (L ! ( CA ↓ a )).

The result of det(A) may actually depend on the chosen algorithm, but that is irrelevant for our results.

Research partly supported by the EU H2020 RISE programme under the Marie Sk lodowska-Curie grant agreement No 778233, by the MIUR project PRIN 2017FTXR7S "IT-MaTTerS" (Methods and Tools for Trustworthy Smart Systems). and by the Piano Triennale Ricerca -UNICT 2016-19. The first and second authors have also been partially supported by INdAM as members of GNCS (Grup po Nazionale per il Calcolo Scientifico). The authors thanks the reviewers for their helpful comments and also M. Dezani for her support.