Davide Basile
email: davide.basile@unifi.it

Maurice H Ter Beek
email: maurice.terbeek@isti.cnr.it

Rosario Pugliese
email: rosario.pugliese@unifi.it

Bridging the Gap between Supervisory Control and Coordination of Services: Synthesis of Orchestrations and Choreographies

Keywords: Service Contracts, Contract Automata, Controller Synthesis, Orchestration, Choreography

We explore the frontiers between coordination and control systems by discussing a number of contributions to bridging the gap between supervisory control theory and coordination of services. In particular, we illustrate how the classical synthesis algorithm from supervisory control theory to obtain the socalled most permissive controller can be modified to synthesise orchestrations and choreographies of service contracts formalised as contract automata. The key ingredient to make this possible is a novel notion of controllability. Finally, we present an abstract parametric synthesis algorithm and show that it generalises the classical synthesis as well as the orchestration and choreography syntheses.

Introduction

Coordination of services describes how control and data exchanges are coordinated in distributed service-based applications and systems. Their principled design is identified as one of the primary research challenges for the next 10 years, and the recent Service Computing Manifesto [START_REF] Bouguettaya | A Service Computing Manifesto: The Next 10 Years[END_REF] points out that "Service systems have so far been built without an adequate rigorous foundation that would enable reasoning about them" and, moreover, that "The design of service systems should build upon a formal model of services".

Two widely adopted approaches to the coordination of services are orchestration and choreography. Intuitively, an orchestration yields the description of a distributed workflow from "one party's perspective" [START_REF] Peltz | Web Services Orchestration and Choreography[END_REF], whereas a choreography describes the behaviour of the involved parties from a "global viewpoint" [START_REF] Kavantzas | Web Services Choreography Description Language v1.0[END_REF]. In an orchestrated model, the service components are coordinated by a special component, the orchestrator, which, by interacting with them, dictates the workflow at runtime. In a choreographed model, instead, the service components autonomously execute and interact with each other on the basis of a local control flow expected to comply with their role as specified by the global viewpoint. Ideally, a choreographed model is more efficient due to the absence of the overhead of communications with the orchestrator. Any choreography can be trivially transformed into an orchestration of services, by adding an idle orchestrator.

Similarly, by explicitly adding an orchestrator and its interactions with the service components, and hence the relative overhead, it is possible to transform an orchestration of services into a choreography.

In [START_REF] Basile | Relating two automata-based models of orchestration and choreography[END_REF], two orchestrated and choreographed automata-based models of services, called contract automata3 and communicating finite state machines, respectively, were studied and related. The goal is to compose the automata so that each service is capable of reaching an accepting (final) state by synchronous/asynchronous one-to-one interactions with the other services in the composition. The main difference relies on the fact that communicating machines name the recipient service of each interaction upfront and use FIFO buffers to interact with each other, whereas contract automata are oblivious of their partners and an orchestration is synthesised to drive their interactions. In particular, the model of contract automata was further developed in, e.g., [START_REF] Basile | Automata for Specifying and Orchestrating Service Contracts[END_REF][START_REF] Basile | Playing with Our CAT and Communication-Centric Applications[END_REF][START_REF] Basile | Specifying Variability in Service Contracts[END_REF].

The orchestration synthesis was borrowed from the synthesis of the most permissive controller (mpc) from Supervisory Control Theory [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF][START_REF] Cassandras | Introduction to Discrete Event Systems[END_REF] (SCT), whose aim is to coordinate an ensemble of (local) components into a (global) system that functions correctly. In the context of contract automata, this amounts to refine the composition of service contracts into its largest sub-portion whose behaviour is non-blocking and safe (a notion of service compliance). The adaptation of the mpc synthesis for synthesising an orchestration of services required the introduction of a novel notion of semi-controllability. Basically, the assumption of the presence of an unpredictable environment was dropped in favour of a milder notion of predictable necessary service requests to be fulfilled.

In this paper, we report on the efforts to relate the mpc synthesis and the orchestration synthesis of contract automata through a homogeneous formalisation. The need for semi-controllability is showcased with intuitive examples and its expressiveness is evaluated with respect to standard SCT notions of controllable and uncontrollable actions. Moreover, a novel choreography synthesis algorithm is introduced as a refined version of the orchestration synthesis. Finally, we show that all synthesis algorithms presented in this paper are generalised into a single abstract synthesis algorithm from which each can be obtained through a different instantiation.

The paper is organised as follows. Section 2 contains background notions and results concerning contract automata and SCT. Section 3 and Section 4 introduce the synthesis of orchestrations and the novel synthesis of choreographies in the setting of (modal service) contract automata. Section 5 demonstrates that all the previously introduced syntheses algorithms are instantiations of a more abstract, parametric synthesis algorithm. Section 6 discusses related work, while Section 7 concludes the paper and provides some hints for future work.

Background

In this section, we provide the background needed to appreciate our contributions on the crossroads of supervisory control theory and coordination of services formalised as modal service contract automata.

Contract Automata

A Contract Automaton (CA) represents either a single service (in which case it is called a principal) or a multi-party composition of services performing actions. The number of principals of a CA is called its rank. The states of a CA are vectors of states of principals. In the following, notation ì v stands for a vector and ì v (i) is the ith element. The transitions of CA are labelled with actions, which are vectors of elements in the set of basic actions

L = R ∪ O ∪ {•}, with R ∩ O = ∅ and • R ∪ O.
Intuitively, R is the set of requests (depicted as non-overlined labels on arcs, e.g. ins), O is the set of offers (depicted as overlined labels on arcs, e.g. ins), and • is a distinguished symbol representing the idle action. An action is then a vector ì a of basic actions where there is either a single offer, or a single request, or a single pair of request-offer that match, i.e. there exist i and j such that ì a (i) is an offer and ì a (j) is the complementary request; all other elements of the vector are the symbol •. Such action is called request, offer, or match, respectively. A transition is also deemed request/offer/match according to its labelling action. The goal of each principal is to reach an accepting (final) state such that all its requests and offers are matched. In [START_REF] Basile | Specifying Variability in Service Contracts[END_REF], CA were equipped with modalities, i.e. necessary ( ) and permitted ( ) requests, respectively, and the formalism was called Modal Service Contract Automata (MSCA), formally defined below.

Definition 1 (MSCA [14]). Given a finite set of states

Q = {q 1 , q 2 , . . .}, a Modal Service Contract Automata (MSCA) A of rank n is a septuple Q, ì q 0 , A , A , A o , T, F , with set of states Q = Q 1 × . . . × Q n ⊆ Q n , initial state ì q 0 ∈ Q, A , A ⊆ R (pairwise disjoint)

finite sets of permitted and necessary requests, respectively, with set of requests

A r = A ∪ A , set of offers A o ⊆ O, set of final states F ⊆ Q, set of transitions T ⊆ Q × A × Q, where A ⊆ (A r ∪ A o ∪ {•}) n ,
partitioned into permitted transitions T and necessary transitions T , s.t.: (i) given t = ( ì q, ì a, ì q ) ∈ T, ì a is either a request or an offer or a match; (ii) ∀i ∈ 1 . . . n, ì

a (i) = • implies ì q (i) = ì q (i) . (iii) t ∈ T iff ì
a is either a request or a match on a ∈ A or an offer on a ∈ A o ; otherwise t ∈ T .

A principal is an MSCA of rank 1 such that A r ∩ co(A o ) = ∅, where the involution co : L → L establishing matching among requests and offers is such that

(abusing notation) co(R) = O, co(O) = R, and co(•) = •. A step (w, ì q) ì a
-→(w , ì q ) occurs iff w = ì aw , w ∈ A * , and ( ì q, ì a, ì q ) ∈ T. Let → * be the reflexive and transitive closure of →. The language of A is

L(A) = { w | (w, ì q 0 ) w -→ * (ε, ì q), ì q ∈ F }. A step may be denoted ì q ì a
-→ if w, w , and ì q are irrelevant, and

(w, ì q) → (w , ì q ) if ì a is. Unless stated differently, the MSCA A = Q A , ì q 0 A , A A , A A , A o A , T A , F A of
rank n is assumed to be given. Subscript A may be omitted if no confusion may arise.

Composition of services is rendered through the composition of their MSCA models by means of the composition operator ⊗. This operator basically interleaves or matches the transitions of the component MSCA, but, whenever two component MSCA are ready on their respective request/offer action, then the match is forced to happen. Moreover, a match involving a necessary request is itself necessary. In the resulting MSCA, states and actions are vectors of states and actions of the component MSCA, respectively. The composition is non-associative, i.e. pre-existing matches are not rearranged if a new MSCA joins the composition afterwards.

In a composition of MSCA, typically various properties are analysed. We are especially interested in agreement and strong agreement (a.k.a. in the literature as progress of interactions, deadlock freedom, compliance or conformance of contracts). In an MSCA in strong agreement, all requests and offers must be matched. Instead, the property of agreement only requires to match all requests. An MSCA admits (strong) agreement if it has a trace satisfying the corresponding property, and it is safe if all its traces are such.

Supervisory Control Theory

The aim of Supervisory Control Theory [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF][START_REF] Cassandras | Introduction to Discrete Event Systems[END_REF] (SCT) is to provide an algorithm to synthesise a finite state automaton model of a supervisory controller from given (component) finite state automata models of the uncontrolled system and its requirements. The synthesised supervisory controller, if successfully generated, is such that the controlled system, which is the composition (i.e. synchronous product) of the uncontrolled system and the supervisory controller, satisfies the requirements and is additionally non-blocking, controllable, and maximally permissive.

An automaton is non-blocking if from each state at least one of the so-called marked states (distinguished stable states representing completed 'tasks' [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF]) can be reached without passing through so-called forbidden states, meaning that the system always has the possibility to return to an accepted stable state (e.g. a final state). The algorithm assumes that marked states and forbidden states are indicated for each component model. SCT distinguishes between observable and unobservable, controllable and uncontrollable actions, where unobservable actions are also uncontrollable. The supervisory controller is not permitted to directly block uncontrollable actions from occurring; the controller is only allowed to disable them by preventing controllable actions from occurring. Intuitively, controllable actions correspond to stimulating the system, while uncontrollable actions correspond to messages provided by the environment, like sensors, which may be neglected but cannot be denied from existing. Finally, the fact that the resulting supervisory controller is maximally permissive (or least restrictive) means that as much behaviour of the uncontrolled system as possible is still present in the controlled system without violating neither the requirements, nor controllability, nor the non-blocking condition.

From the seminal work of Ramadge and Wonham [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF], we know that a unique maximally permissive supervisory controller exists, provided that all actions are observable. This is called the most permissive controller (mpc); it coordinates an ensemble of (local) components into a (global) system that works correctly. The synthesis algorithm suffers from the same state space explosion problem as model checking [START_REF] Gohari | On the complexity of supervisory control design in the RW framework[END_REF].

Intuitively, the synthesis algorithm for computing the mpc of a finite state automaton A works as follows. The mpc is computed through an iterative procedure that at each step i updates incrementally a set of states R i containing the bad states, i.e. those states that cannot prevent a forbidden state to be eventually reached, and refines an automaton K i . The algorithm starts with an automaton K 0 equal to A and a set R 0 containing all dangling states, where a state is dangling if it cannot be reached from the initial state or cannot reach a final state. At each step i the algorithm prunes in a backwards fashion transitions with target state in R i or forbidden source state. The set R i is updated by possibly adding source states of uncontrollable transitions of A with a bad target state and dangling states. When no more updates are possible, the algorithm terminates. Since A is finite state and the set R i can only increase at each step, termination is ensured. Now, suppose that at its termination the algorithm returns the pair (K s , R s ). We have that the mpc is empty, if the initial state of A is in R s ; otherwise, the mpc is K s . We report below the standard synthesis algorithm, but we homogenise the notation and simplify the formulation, to align the algorithm with those presented in the next sections. For this purpose, we assume the standard mpc synthesis to operate on MSCA where necessary transitions (T ) are uncontrollable whilst permitted transitions (T ) are controllable. We use to denote the empty automaton. A state q ∈ Q is dangling iff w s.t. q 0 w -→ * q or q w -→ * q f ∈ F. Dangling(A) denotes the set of dangling states of A. Given two MSCA A and A , we say that A is a sub-automaton of A, written A ⊆ A, whenever the components of A are included in the corresponding ones of A. Moreover, given two sets of states R and R , we let

(A, R) ≤ (A , R ) if A ⊆ A and R ⊆ R . It is straightforward to show that (MSCA × 2 Q , ≤) is a complete partial order (cpo).
The algorithm to compute the mpc is then defined in terms of the least fixed point of a monotone function on the cpo (MSCA × 2 Q , ≤).

Definition 2 (Standard synthesis, adapted from [47]). Let A be an MSCA, and let

K 0 = A and R 0 = Dangling(K 0 ). We let the synthesis function f : MSCA × 2 Q → MSCA × 2 Q be defined as follows: f (K i-1 , R i-1 ) = (K i , R i ), with T K i = T K i-1 \ { ( ì q, ì a, ì q ) ∈ T K i-1 | ì q ∈ R i-1 ∨ ì q is forbidden } R i = R i-1 ∪ { ì q | ( ì q, ì a, ì q ) ∈T A , ì q ∈ R i-1 } ∪ Dangling(K i )
Theorem 1 (Standard mpc, adapted from [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF]). The synthesis function f is monotone on the cpo (MSCA × 2 Q , ≤) and its least fixed point is:

(K s , R s ) = sup({ f n (K 0 , R 0 ) | n ∈ N })
The mpc of A, denoted by K A , is:

K A = if ì q 0 ∈ R s Q \ Dangling(K s ), ì q 0 , A , A , A o , T K s , F \ Dangling(K s ) otherwise

Synthesis of Orchestrations

In this section, we discuss how we revised the classical synthesis algorithm from SCT (cf. Theorem 1) to obtain the mpc and synthesise orchestrations of MSCA. Differently from standard SCT, all transitions of MSCA are observable, since MSCA model the execution of services in terms of their requests and offers. Originally, MSCA were capable of expressing only permitted requirements, corresponding to actions that are controllable by the orchestrator. Hence, in the synthesis of the orchestration, all transitions labelled by actions violating the property to be enforced were pruned, and all dangling states were removed (cf. [START_REF] Basile | Automata for Specifying and Orchestrating Service Contracts[END_REF]).

While permitted requests of MSCA are in one-to-one correspondence with controllable actions, interestingly this is not the case for necessary requests and uncontrollable actions. A necessary (request) action is indeed a weaker constraint than an uncontrollable one. This stems from the fact that traditionally uncontrollable actions relate to an unpredictable environment. However, the interpretation of such actions as necessary service requests to be fulfilled in a service contract, as is the case in the setting of MSCA, implies that it suffices that in the synthesised orchestration at least one such synchronisation (i.e. match) actually occurs. This is precisely what is modelled by the notion of semi-controllable actions, anticipated in [START_REF] Basile | Specifying Variability in Service Contracts[END_REF] and introduced in [START_REF] Basile | Orchestration Synthesis for Real-Time Service Contracts[END_REF][START_REF] Basile | Controller synthesis of service contracts with variability[END_REF], discussed next.

The importance of this novel notion in the synthesis algorithm is showcased by an intuitive example. Consider the two MSCA interacting on the necessary service request a depicted in Fig. 1 (left and middle), and their possible composition A depicted in Fig. 1 (right). Note that A models two possibilities of fulfilling request a from the leftmost automaton by matching it with a service offer a of the middle one. Note that a similar composition can be obtained in other automata-based formalisms (such as, e.g., (timed) I/O automata [START_REF] Lynch | An Introduction to Input/Output Automata[END_REF][START_REF] Alur | A Theory of Timed Automata[END_REF][START_REF] David | Timed I/O Automata: A Complete Specification Theory for Real-time Systems[END_REF]). Now assume that a must be matched with a to obtain an agreement (i.e. it is necessary), and that for some reason the bad state is to be avoided in favour of the successful state , i.e. in some sense we would like to express that a must be matched at some point, rather than always. In most automata-based formalisms this is not allowed and the resulting mpc is empty. In the MSCA formalism, it is possible to orchestrate the composition of the two automata on the left in such a way that the result is the automaton A on the right, but without the state and its incident transition.

• a G G • • a 3 3 b G G • a G G • (•, •) ( a , a ) 4 4 (•,b) G G (•, •) ( a , a ) 5 5
. . . In fact, in the MSCA formalism, A depicts a composition in which the automata on the left can synchronise on a so-called semi-controllable action a either in their initial state or after the middle automaton has performed some other action b , ignoring in this case whether a bad or a successful state is reached in the end. Indeed, the notion of semi-controllability is independent from both the specific formalism being used and the requirement (e.g. agreement in case of MSCA) to be enforced.

As far as we know, we were the first to define a synthesis algorithm, in [START_REF] Basile | Orchestration Synthesis for Real-Time Service Contracts[END_REF], that is capable of producing a controller that guarantees that at least one of these two synchronisations actually occurs. Indeed, in the standard synthesis algorithm (cf. Theorem 1), a can either be controllable and hence not necessary as we want, or uncontrollable thus requiring that a must always be matched, a stronger requirement than the one posed by declaring a as necessary.

To formalize the intuitions above4, a semi-controllable transition t becomes controllable if in a given portion of A there exists a semi-controllable match transition t , with source and target states not dangling, such that in both t and t the same principal, in the same local state, does the same request. Otherwise, t is uncontrollable.

Definition 3 (Controllability).

Let A be an MSCA and let t = ( ì q 1 , ì a 1 , ì q 1 ) ∈ T A . Then:

-if ì a 1 is an action on a ∈ A ∪ A o , then t is controllable (in A) and part of T ; -if ì a 1 is a request or match on a ∈ A , then t is semi-controllable (in A) and part of T . Moreover, given A ⊆ A, if t is semi-controllable and ∃ t = ( ì q 2 ì a 2 --→ ì q 2 ) ∈ T A in A s.t. ì a 2 is a match, ì q 2 , ì q 2 Dangling(A ), ì q 1(i) = ì q 2(i) , and ì a 1(i) = ì a 2(i) = a, then t is controllable in A (via t ); otherwise, t is uncontrollable in A .
The algorithm for synthesising an orchestration enforcing agreement of MSCA follows. The main adaptation of the mpc synthesis of Theorem 1 is that transitions are no longer declared uncontrollable, but instead they can be either controllable or semicontrollable. More importantly, a semi-controllable transition switches from controllable to uncontrollable only after it has been pruned in a previous iteration, in which case its source state becomes bad. Finally, in this case there are no forbidden states but rather forbidden transitions (i.e. requests, according to the property of agreement).

Definition 4 (MSCA orchestration synthesis, adapted from [14]).

Let A be an MSCA, and let K 0 = A and R 0 = Dangling(K 0 ). We let the orchestration synthesis function f o : MSCA × 2 Q → MSCA × 2 Q be defined as follows:

f o (K i-1 , R i-1 ) = (K i , R i ), with T K i = T K i-1 \ { ( ì q - → ì q ) = t ∈ T K i-1 | ( ì q ∈ R i-1 ∨ t is a request)} R i = R i-1 ∪ { ì q | ( ì q - →) ∈ T A is uncontrollable in K i } ∪ Dangling(K i )
Theorem 2 (MSCA orchestration mpc, adapted from [START_REF] Basile | Specifying Variability in Service Contracts[END_REF]). The orchestration synthesis function f o is monotone on the cpo (MSCA × 2 Q , ≤) and its least fixed point is:

(K s , R s ) = sup({ f n o (K 0 , R 0 ) | n ∈ N }) The (orchestration) mpc K A of A is: K A = if ì q 0 ∈ R s Q \ R s , ì q 0 , A , A , A o , T K s \ T , F \ R s otherwise where T = { t = ì q - → ∈ K s | t is controllable in K s , ì q ∈ R s }.
Semi-controllability. We now show, by means of an example, that the encoding of an automaton A with semi-controllable actions into an automaton A without, such that the same synthesised controllers are obtained, results in an exponential blow-up of the state space. More precisely, the encoding is intended to preserve safety: the mpc of A equals that of A . The encoding is sketched in Fig. 2: the automaton A is obtained by turning all semi-controllable transitions of the automaton A from Fig. 1 (right) into uncontrollable transitions in A . The intuition for this construction is as follows. If the synchronisation on a specific semi-controllable action a occurs in n different transitions in A (two in our example), then the encoding creates an automaton that is the union of 2 n -1 automata (three in our example), which are obtained by all possible combinations of pruning a subset of the n semi-controllable transitions of A, minus the one in which all n semi-controllable transitions are pruned. In fact, without knowing a priori the set of forbidden and successful states, it is impossible to provide a more efficient encoding. We explain why this is the case. Assume, by contradiction, that there exists an encoding that results in a 'smaller' automaton A , in which one of the 2 n -1 combinations of pruned transitions (say, P) is discarded. It then suffices to specify as a counterexample a property in A such that all source states of transitions in P are forbidden and all target states of the remaining semi-controllable transitions are successful. The synthesis of A against such a property would prune exactly the semi-controllable transitions in P. Thus, in the synthesis of A such an mpc would not be present, a contradiction.

(•, •) Ù Ù ! ! (•, •) (•,b) G G (•, •) ( a , a ) u n c 5 5 (•, •) ( a , a ) u n c 5 5 (•,b) G G (•, •) ( a , a ) u n c 5 5 (•, •) ( a , a ) u n c 5 5 (•,b) G G (•, •) (•, •) (•, •) (•, •) (•, •)

Synthesis of Choreographies

In the previous section we have seen that the orchestration of MSCA is rendered as a particular mpc. The orchestrator is however implicit, in the sense that its interactions with the principals are hidden. Basically, one could assume that before interacting, each principal expects a message from the orchestrator and answers with an acknowledgement after the interaction terminates. The main intuition behind switching from an orchestrated to a choreographic coordination of contracts is that there is no longer the need for such 'hidden' interactions. Ideally, the principals moving autonomously are able to accomplish the behaviour foreseen by the synthesis, which in this case acts as a global type. Differently from the traditional choreographic approach, where the starting point is a global type, in MSCA the global type is synthesised automatically.

The requirements for ensuring that the synthesised mpc is a (form of) choreography were studied in [START_REF] Basile | Relating two automata-based models of orchestration and choreography[END_REF][START_REF] Lange | From Communicating Machines to Graphical Choreographies[END_REF]. Roughly, they amount to the so-called branching condition requiring that principals perform their offers/outputs independently of the other principals in the composition. To formalise it, we let snd( ì a) = i when ì a is a match action or an offer action and ì a (i) ∈ O.

Definition 5 (Branching condition [13]

). An MSCA A satisfies the branching condition iff the following holds for each pair of states ì q 1 , ì q 2 reachable in A:

∀ ì a match action . ( ì q 1 ì a -→ ∧ snd( ì a) = i ∧ ì q 1(i) = ì q 2(i) ) implies ì q 2 ì a -→.
The branching condition is related to a phenomenon known as 'state sharing' in other coordination models (cf., e.g., [START_REF] Ter Beek | Communication Requirements for Team Automata[END_REF]) according to which system components can

(q 0 , •, •) ( a , a , • ) w w ( a , • , a ) @ @ ... G G (q 0 , •, •) ( a , a , • ) 9 9
Fig. 3. Fragment of a possible service composition influence potential synchronisations through their local (component) states even if they are not involved in the actual global (system) transition.

In [START_REF] Basile | Relating two automata-based models of orchestration and choreography[END_REF] it is proved that the mpc corresponds to a well-behaving choreography if and only if it satisfies the branching condition and is strongly safe. Notably, in case the two conditions are not satisfied, that paper does not provide any algorithm for automatically synthesising a choreography, rather the contracts have to be manually amended. Instead, in the remainder of this section, we introduce an algorithm for automatically synthesising a well-behaving choreography.

The property to be enforced during the synthesis is strong agreement: all offers and requests have to be matched, because all messages have to be read (i.e. offers matched). Moreover, in the case of choreography, service contract requests are always permitted whereas service contract offers can be necessary. That is, their roles are swapped with respect to the case of orchestration.

In principle, the synthesis could trivially introduce a coordinator component and its interactions to coordinate the principals. However, this would reduce the choreography to a centralised coordination of contracts. To prevent this, the synthesis can only remove and never add behaviour. Hence, a choreography can only be synthesised if all principals are capable of interacting on their own without resorting to a central coordinator.

Similarly to orchestration synthesis, indicating transitions as either controllable or uncontrollable does not suffice for synthesising a choreography. Moreover, the notion of semi-controllability introduced for the orchestration case does not suffice for expressing necessary offers. Indeed, orchestration synthesis does not ensure the branching condition to be satisfied by the synthesised automaton, as the following example shows.

In Fig. 3, a fragment of a service composition is shown. Two global states are depicted, and in both the first service, say Alice, is in its initial local state (say, q 0 ). Alice performs an output (i.e. offer) a that can be directed to either Bob (second service) or Carol (third service), from the initial global state, or only to Bob from the other state. It is possible to reach either a successful () or a bad () state, left unspecified for the moment. Notably, the output of Alice is neither controllable nor uncontrollable nor semi-controllable by the synthesis. Now assume that the a is controllable and from the initial global state both interactions eventually lead to a bad state (). In this case, those transitions are pruned by the synthesis, and the resulting automaton is wrongly approved. Indeed, Alice has no mean to understand when her output a is enabled, because she has not changed state. The branching condition, which is necessary for obtaining a well-behaving choreography, would be violated. Note that this would happen also if a were semi-controllable. In fact, to satisfy the branching condition, the synthesis should remove all outputs a.

Conversely, assume that the a is uncontrollable and that it is possible from the initial global state to reach a successful state () if the message a is received by Bob. In this case, it would not be possible to prune the transition from the initial state leading to , because it is also uncontrollable. The synthesis would thus be empty, a wrong rejection, because a choreography exists in which Alice autonomously interacts with Bob.

In conclusion, a necessary action is rendered neither as uncontrollable nor semicontrollable and permitted actions require extra pruning operations during the synthesis. A novel notion of semi-controllability for a necessary action is required that is weaker than uncontrollable but stronger than the semi-controllable notion used in the synthesis of orchestration. Basically, for the choreography synthesis, a (semi-controllable) necessary

transition t = ( ì q ì a 1 --→) ∈ T is detected to be uncontrollable iff no necessary transition t = ( ì q ì a 2
--→) ∈ T exists from the same source state such that in both t and t the same offer is provided by the same principal, but possibly with different receivers. Formally: Definition 6. Let A be an MSCA and let t = ( ì q, ì a 1 , ì q 1 ) ∈ T A . Then:

-if ì a 1 is an action on a ∈ A , then t is controllable (in A); -if ì a 1 is an offer or a match on a ∈ A , then t is semi-controllable (in A).

Moreover, given

A ⊆ A, if t is semi-controllable and ∃ t = ( ì q, ì a 2 , ì q 2 ) ∈ T A s.t. ì a 2 is a match, ì
q, ì q 2 Dangling(A ), and snd( ì a) = i and ì

a 1(i) = ì a 2(i) = a, then t is controllable in A (via t ); otherwise, t is uncontrollable in A .
Hence, again a necessary transition is a particular type of transition that switches from being controllable to uncontrollable in case a condition on the global automaton is not met. Note that this condition is stronger than the one required for the case of orchestration (semi-controllability), because for the case of choreography transitions t and t in Definition 6 share the source state. Moreover, also in this case it can be shown that the encoding of this type of semi-controllable transition into an uncontrollable one would result in an exponential growth of the state space of the model.

Similarly to the orchestration synthesis in Definition 4, when a semi-controllable transition previously removed by the synthesis switches from controllable to uncontrollable, its source state is detected to be bad. Apart from the different notion of semi-controllability, another difference with respect to the orchestration synthesis is that each time a controllable transition is pruned, all other transitions violating the branching condition must also be removed. Finally, according to the property of strong agreement, both request and offer transitions are forbidden. The formalisation is provided below.

Definition 7 (MSCA choreography synthesis).

Let A be an MSCA, and let K 0 = A and R 0 = Dangling(K 0 ). We let the choreography synthesis function f c : MSCA×2 Q → MSCA × 2 Q be defined as follows:

f c (K i-1 , R i-1 ) = (K i , R i ), with T K i = T K i-1 \ ({ ( ì q - → ì q ) = t ∈ T K i-1 | ì q ∈ R i-1 ∨ t is a request or an offer } ∪{ ( ì q 1 ì a -→) = t ∈ T K i-1 | ∃ ì q 2 : (snd( ì a) = i ∧ ì q 1(i) = ì q 2(i) ) ∧ ( ì q 2 ì a -→) T K i-1 }) R i = R i-1 ∪ { ì q | ( ì q - →) ∈ T A is uncontrollable in K i } ∪ Dangling(K i )
Theorem 3 (MSCA choreography mpc). The choreography synthesis function f c is monotone on the cpo (MSCA × 2 Q , ≤) and its least fixed point is:

(K s , R s ) = sup({ f n c (K 0 , R 0 ) | n ∈ N })
The (choreography) mpc K A of A is:

K A = if ì q 0 ∈ R s Q \ R s , ì q 0 , A , A , A o , T K s \ T , F \ R s otherwise where T = { t = ì q - → ∈ K s | t is controllable in K s , ì q ∈ R s }. Moreover, K A satisfies the branching condition.
Returning to the example in Fig. 3, the wrongly accepted case is removed because, during the synthesis, the operation of pruning the transitions leading to bad states causes the removal of the remaining transition. Thus, the obtained choreography is empty. Similarly, the wrongly rejected case is not possible because, assuming that the output from the initial state is necessary, this necessary action is not rendered as uncontrollable as long as the output is matched by some other principal from the same initial state.

Abstract Synthesis

We have presented in the previous three sections three slightly different synthesis algorithms. As previously stated, in order to bridge the gap between standard synthesis and orchestration and choreography syntheses, the controllable and uncontrollable actions from SCT are related to permitted and necessary modalities, respectively, of MSCA.

The main intuition is that the SCT assumption of an unpredictable environment responsible for the uncontrollable transitions is not realistic in the case of coordination of services whose behaviour is known and observable. As a result, necessary actions are not in correspondence with uncontrollable actions, but rather require the introduction of a milder notion of controllability. The condition under which a controllable transition becomes uncontrollable varies depending on the particular synthesis algorithm (orchestration or choreography). Conversely, in the standard mpc synthesis such information is local, i.e. a transition is declared to be uncontrollable.

In this section, we discuss an abstract synthesis algorithm that generalises the previous algorithms by abstracting away the conditions under which a transition is pruned or a state is deemed bad. These two conditions, called pruning predicate (φ p ) and forbidden predicate (φ f ) are parameters to be instantiated by the corresponding instance of the synthesis algorithm (e.g. orchestration or choreography). Predicate φ p is used for selecting the transitions to be pruned. Depending on the specific instance, non-local information about the automaton or the set of bad states is needed by φ p . Therefore, φ p takes as input the current transition to be checked, the automaton, and the set of bad states. If φ p evaluates to true, then the corresponding transition will be pruned. Predicate φ f is used for deciding whether a state becomes bad. The input parameters are the same as φ p . However, φ f only inspects necessary transitions (T ). If φ f evaluates to true, then the source state is deemed bad and added to the set R i . The abstract synthesis algorithm is formally defined below.

Definition 8 (Abstract synthesis).

Let A be an MSCA, and let K 0 = A and R 0 = Dangling(K 0 ). Given two predicates φ p , φ f : T × MSC A×Q → Bool, we let the abstract synthesis function f (φ p ,φ f ) : MSCA × 2 Q → MSCA × 2 Q be defined as follows:

f (φ p ,φ f ) (K i-1 , R i-1 ) = (K i , R i ), with T K i = T K i-1 \ { ( ì q ì a -→) = t ∈ T K i-1 | φ p (t, K i-1 , R i-1 ) = true } R i = R i-1 ∪ { ì q | ( ì q - →) = t ∈ T A , φ f (t, K i-1 , R i-1 ) = true } ∪ Dangling(K i )
As in the previous cases, the mpc relative to the pair (φ p , φ f ) is obtained by computing the least fixed point (K s , R s ) of f (φ p ,φ f ) and removing the states R s from K s .

In the following, we show how to instantiate the abstract synthesis function to the standard synthesis function, to the orchestration synthesis function, or to the choreography synthesis function, and prove their correspondences. Definition 8 where, for a generic transition t = ( ì q, ì a, ì q ), predicates φ p and φ f are defined as follows:

Theorem 4 (Abstract mpc synthesis). The standard synthesis function of Definition 2 coincides with the instantiation of the abstract synthesis function of

φ mpc p (t, K, R) = ( ì q ∈ R) ∨ ( ì q is forbidden) φ mpc f (t, K, R) = ( ì q ∈ R)
Note that in Theorem 4 the predicates do not use any non-local information related to the parameter K. For both orchestration and choreography two different semicontrollability conditions are used to decide whether a state has become forbidden. These conditions are translated into the corresponding forbidden predicates. Definition 8 where, for a generic transition t = ( ì q, ì a, ì q ), predicates φ p and φ f are defined as follows:

Theorem 5 (Abstract orchestration synthesis). The orchestration synthesis function of Definition 4 coincides with the instantiation of the abstract synthesis function of

φ orc p (t, K, R) = (t is a request ) ∨ ( ì q ∈ R) φ orc f (t, K, R) = ( ì q 2 ì a 2 --→ ì q 2 ) ∈ T K : ( ì a 2 is a match ) ∧ ( ì q 2 , ì q 2 Dangling(K)) ∧ ( ì q (i) = ì q 2(i) ) ∧ ( ì a (i) = ì a 2(i) = a)
The pruning predicate of Theorem 5 does not use any information coming from the global automaton K, whereas this is no longer the case for the forbidden predicate that indeed specifies the semi-controllability condition for the necessary transitions of an orchestration (cf. Definition 3). Definition 8 where, for a generic transition t = ( ì q, ì a, ì q ), predicates φ p and φ f are defined as follows:

Theorem 6 (Abstract choreography synthesis). The choreography synthesis function of Definition 7 coincides with the instantiation of the abstract synthesis function of

φ cor p (t, K, R) = (t is a request or an offer ) ∨ ( ì q ∈ R) ∨ (∃ ì q 2 ∈ Q K : (snd( ì a) = i) ∧ ( ì q (i) = ì q 2(i) ) ∧ ( ì q 2 ì a -→ T K )) φ cor f (t, K, R) = ( ì q ì a 2 --→ ì q 2 ) ∈ T K : ( ì a 2 is a match ) ∧ ( ì q, ì q 2 Dangling(K)) ∧ ( ì a (i) = ì a 2(i) = a)
Notably, in Theorem 6 both predicates require global information on the whole automaton. Similarly to Theorem 5, the forbidden predicate codifies the semicontrollability condition of Definition 6. Moreover, the pruning predicate removes all transitions violating the branching condition (cf. Definition 5).

We believe that the synthesis algorithms are related. In particular, we conjecture that via a partial order of predicates, appropriately defined as

(φ p 1 , φ f 1 ) ≤ (φ p 2 , φ f 2 ) iff (φ p 1 → φ p 2 ) ∧ (φ f 1 → φ f 2 ), it can be proved that (φ orc p , φ orc f ) ≤ (φ mpc p , φ mpc f ) and therefore K mpc A ⊆ K orc A .
More generally, the cpo of predicates permits to perform abstraction of syntheses, in the sense that the lesser the pair of predicates the greater the corresponding synthesised automaton. This can be useful to perform partial syntheses and skip unnecessary checks or even potentially undecidable computations. For instance, given an MSCA A, from K orc A = , we can conclude K mpc A = without actually computing it, which could potentially require more computational effort.

Related Work

Our contributions to bridging the gap between SCT and coordination of services concern adaptations of the classical synthesis algorithm from SCT in order to synthesise orchestrations and choreographies of service contracts formalised as MSCA. In the literature, there exist many formalisms for modelling and analysing (service) contracts, ranging from behavioural type systems, including behavioural contracts [START_REF] Castagna | A Theory of Contracts for Web Services[END_REF][START_REF] Acciai | Behavioural contracts with request-response operations[END_REF][START_REF] Laneve | An algebraic theory for web service contracts[END_REF] and session types [START_REF] Bruni | Multiparty Sessions in SOC[END_REF][START_REF] Honda | Multiparty Asynchronous Session Types[END_REF][START_REF] Dezani-Ciancaglini | Sessions and Session Types: An Overview[END_REF][START_REF] Castagna | On Global Types and Multi-Party Sessions[END_REF][START_REF] Michaux | Session types for safe Web service orchestration[END_REF], to automata-based formalisms, including interface automata [START_REF] De Alfaro | Interface Automata[END_REF] and (timed) (I/O) automata [START_REF] Lynch | An Introduction to Input/Output Automata[END_REF][START_REF] Alur | A Theory of Timed Automata[END_REF][START_REF] David | Timed I/O Automata: A Complete Specification Theory for Real-time Systems[END_REF]. Foundational models for service contracts and session types are surveyed in [START_REF] Ter Beek | Web Service Composition Approaches: From Industrial Standards to Formal Methods[END_REF][START_REF] Bartoletti | Compliance in Behavioural Contracts: A Brief Survey[END_REF][START_REF] Hüttel | Foundations of Session Types and Behavioural Contracts[END_REF].

The MSCA formalism used in this paper differs fundamentally from these models, which typically study notions of contract compliance involving only two parties, since MSCA primitively support multi-party compliance of contracts that compete on offering or requesting the same service. Furthermore, the above models do not consider modalities of services whereas MSCA provide primitive support for permitted and necessary service actions, resulting in the introduction of a novel notion of semi-controllability in the context of SCT. Modal Transition Systems (MTS) and their extensions [START_REF] Křetínský | 30 Years of Modal Transition Systems: Survey of Extensions and Analysis[END_REF], as adopted for instance in Software Product Line Engineering (SPLE [START_REF] Pohl | Software Product Line Engineering: Foundations, Principles, and Techniques[END_REF][START_REF] Apel | Feature-Oriented Software Product Lines: Concepts and Implementation[END_REF]), like modal I/O automata [START_REF] Larsen | Modal I/O Automata for Interface and Product Line Theories[END_REF] and MTS with variability constraints [START_REF] Ter Beek | Modelling and analysing variability in product families: Model checking of modal transition systems with variability constraints[END_REF], do natively distinguish may and must modalities, but the other differences remain. In particular, they cannot explicitly handle dynamic composition by allowing new services that join composite services to intercept already matched actions.

We are only aware of two other applications of SCT to MTS. In [START_REF] Darondeau | Supervisory Control for Modal Specifications of Services[END_REF], there is no direct relation between may/must and controllable/uncontrollable, and the modal automaton (i.e. MTS with final states) is seen as a predicate that is satisfied if the plant automaton (i.e. the system to be refined against the predicate) is a sort of alternate refinement of the predicate. Similarly, in [START_REF] Feuillade | Modal Specifications for the Control Theory of Discrete Event Systems[END_REF], the control objectives (i.e. the predicate) is a modal automaton, non-blockingness is not considered, and another modal automaton describes which actions are controllable and which are uncontrollable in the plant automaton. In this paper, the predicate is an invariant (i.e. forbidden states and forbidden transitions are given), the modal automaton (i.e. MSCA) is the plant, and a necessary transition induces different notions of controllability according to the adopted coordination paradigm.

SCT was first applied to SPLE in [START_REF] Ter Beek | Supervisory Controller Synthesis for Product Lines Using CIF 3[END_REF] by showing how the CIF 3 toolset [START_REF] Van Beek | CIF 3: Model-Based Engineering of Supervisory Controllers[END_REF] can automatically synthesise a single (global, family) model representing an automaton for each of the valid products of a product line from (i) a feature constraint with attributes (e.g. cost), (ii) behavioural component models associated with the features, and (iii) additional behavioural requirements like state invariants, action orderings, and guards on actions (reminiscent of the Featured Transition Systems of [START_REF] Classen | Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking[END_REF]). The resulting CIF 3 model satisfies all feature-related constraints as well as all given behavioural requirements. Since CIF 3 allows the export of such models in a format accepted by the mCRL2 model checker [START_REF] Cranen | An Overview of the mCRL2 Toolset and Its Recent Advances[END_REF], the latter can be used to verify arbitrary behavioural properties expressed in the modal µ-calculus with data or its feature-oriented variant of [START_REF] Ter Beek | Family-Based Model Checking with mCRL2[END_REF]. An important advantage is that both CIF 3 and mCRL2 can be used off-the-shelf, meaning that no additional tools are required. Differently from our approach, all actions are controllable and orchestration is not considered, whilst a prototype tool supporting orchestration synthesis for contract automata is presented in [START_REF] Basile | Playing with Our CAT and Communication-Centric Applications[END_REF].

The only approach by others to bridge the gap between SCT and coordination of services that we are aware of is that of [START_REF] Atampore | Automated Service Composition Via Supervisory Control Theory[END_REF], where services are formalised as so-called Service Labelled Transition Systems (SLTS), which are a kind of guarded automata with data. To this aim, SCT is adapted to deal with conditions and variables as well as with a means to enforce services based on runtime information. However, service composition through SLTS is based on the standard synchronous product, whilst the contract composition expresses competing contracts. More importantly, in [START_REF] Atampore | Automated Service Composition Via Supervisory Control Theory[END_REF], input actions are considered uncontrollable whilst output actions are controllable, in the standard view of a service interacting with the environment. Our contribution induces novel notions of controllability to express necessary requirements that are semi-controllable. The standard controller synthesis algorithm is used in [START_REF] Gierds | Reducing Adapter Synthesis to Controller Synthesis[END_REF] to synthesise adapters between services. These adapters act like proxies and are used to enforce properties such as deadlock-freedom. Compared to our work, the interactions between services are driven by their contracts rather than by adapters. The standard controller synthesis algorithm cannot be applied for synthesising a correct composition of contracts.

We conclude this section by describing two further extensions of MSCA, developed for different purposes, and for which we also defined adapted synthesis algorithms. In [START_REF] Basile | Controller synthesis of service contracts with variability[END_REF], we present Featured Modal Contract Automata (FMCA). Technically, we extend MSCA with a variability mechanism concerning structural constraints that operate on the service contract, used to define different configurations. This reflects the fact that services are typically reused in configurations that vary over time and need to dynamically adapt to changing environments [START_REF] Yi | Deploying and managing Web services: issues, solutions, and directions[END_REF]. Configurations are characterised by which service actions are mandatory and which forbidden. The valid configurations are those respecting all structural constraints. We follow the well-established paradigm of SPLE, which aims at efficiently managing a product line (family) of highly (re)configurable systems to allow for mass customisation [START_REF] Pohl | Software Product Line Engineering: Foundations, Principles, and Techniques[END_REF][START_REF] Apel | Feature-Oriented Software Product Lines: Concepts and Implementation[END_REF]. To compactly represent a product line, i.e. the set of valid product configurations, we use a so-called feature constraint, a propositional formula ϕ whose atoms are features [START_REF] Batory | Feature Models, Grammars, and Propositional Formulas[END_REF], and we identify features as service actions (offers as well as requests). A valid product then distinguishes a set of mandatory and a set of forbidden actions. Consequently, we define an algorithm to compute the FMCA K A p as the mpc for a valid product p of an FMCA A. The main adaptation of the synthesis algorithm for MSCA is to consider as bad states also those that cannot prevent a forbidden action to be eventually executed and to discard the transitions labelled with actions forbidden by p. Moreover, if some action that is mandatory in p is unavailable in the automaton that results from the fixed point iteration, then the mpc is empty. In [START_REF] Basile | Orchestration Synthesis for Real-Time Service Contracts[END_REF], we introduced Timed Service Contract Automata (TSCA) as an extension of the FMCA from [START_REF] Basile | Controller synthesis of service contracts with variability[END_REF] with real-time constraints. Formally, a configuration of a TSCA is a triple consisting of a recognised trace, a state, and a valuation of clocks. The (finite) behaviour recognised by a TSCA are traces of alternating time and discrete transitions, i.e. in a given configuration either time progresses (a silent action in the languages recognised by TSCA) or a discrete step to a new configuration is performed. Consequently, we define an algorithm to compute the orchestration synthesis of TSCA. To respect the timing constraints, we use the notion of zones from timed games [START_REF] Asarin | Controller Synthesis for Timed Automata[END_REF][START_REF] Cassez | Efficient On-the-Fly Algorithms for the Analysis of Timed Games[END_REF]. The resulting synthesis algorithm resembles a timed game, but it differs from classical timed game algorithms [START_REF] Asarin | Controller Synthesis for Timed Automata[END_REF][START_REF] Cassez | Efficient On-the-Fly Algorithms for the Analysis of Timed Games[END_REF][START_REF] David | Timed I/O Automata: A Complete Specification Theory for Real-time Systems[END_REF] by combining two separate games, viz. reachability games (to ensure that marked states must be reachable) and safety games (to ensure that forbidden states are never traversed). A TSCA might be such that all bad configurations are unreachable (i.e. it is safe), while at the same time no final configuration is reachable (i.e. the resulting orchestration is empty).

Conclusion

In this paper, we have presented recent efforts in bridging the gap between the most permissive controller synthesis from Supervisory Control Theory with synthesis algorithms of orchestrations and choreographies of a formal model of service contracts called modal service contract automata. We have introduced a new algorithm capable of synthesising a safe non-blocking composition of service contracts that is directly translatable into a choreographed formalism. We have also introduced an abstract synthesis algorithm that generalises the synthesis of the choreography, as well as that of the orchestration and that of the most permissive controller.

The properties to be enforced in the algorithms that we have presented are all invariants specified through either forbidden states or forbidden transitions. Future work is needed to investigate the abstract syntheses under other non-invariant properties. Finally, further work is necessary to formally demonstrate that the different synthesis algorithms are related, as conjectured at the end of Section 5.

Fig. 1 .

 1 Fig. 1. Two MSCA (left and middle) and a possible composition A of them (right)

Fig. 2 .

 2 Fig. 2. Automaton A uses uncontrollable transitions to encode automaton A from Fig. 1 (right)

Not to be confused with the contract automata of[START_REF] Azzopardi | Contract automata: An operational view of contracts between interactive parties[END_REF] meant to formalise legal contracts among two parties expressed in natural language.