A choreography describes the interaction between services. It may be used for speci cation purposes, for instance serving as a contract in the design of an interorganizational business process. Typically, not all describable interactions make sense which motivates the study of the realizability problem for a given choreography. In this paper, we show that realizability can be traced back to the problem of controllability which askes whether a service has compatible partner processes. This way of thinking makes algorithms for controllability available for reasoning about realizability. In addition, it suggests alternative de nitions for realizability. We discuss several proposals for de ning realizability which di er in the degree of coverage of the speci ed interaction.
Throughout this paper, x a nite set of message channels M that is partitioned into asynchronous message channels MA and synchronous message channels MS . From M , derive a set of message events E := !E [ ?E [ !?E, consisting of asynchronous send events !E := f!x j x 2 MAg, asynchronous receive events ?E := f?x j x 2 MAg, and synchronization events !?E := f!?x j x 2 MS g. De nition 1 (Conversation, choreography). A conversation is a nite word over E such that, for all x 2 MA, #!x( ) = #?x( ) and for every pre x 0 of holds: #!x( 0) #?x( 0). Thereby, #x( ) denotes the number of occurrences of the message event x in the word . A choreography is a set of conversations. The requirements for a conversation state that asynchronous events are always paired, and a send event always occurs before the respective receive event. A choreography is a set of desired message event sequences. A choreography is de ned with respect to a set of peers which form a collaboration. De nition 2 (Peer, collaboration). A peer P = [I; O] consists of a set of input message channels I M and a set of output message channels O M , I \ O = ;. A collaboration is a set fP1; : : : ; Png of peers such that Ii \ Ij = ; and Oi \ Oj = ; for all i 6= j, and Sin=1 Ii = Sin=1 Oi.
The requirements ensure that communication in a collaboration is always bilateral, yielding a closed system that models no message exchange other than that between the peers.
There are various languages to specify collaborations and choreographies, ranging from formal models such as Interaction Petri Nets [2] to industrial notations such as Let's Dance [3], UML collaboration diagrams, and BPMN. While these languages di er in syntax and semantics, concepts such as an underlying collaboration (i.e., the endpoints and the exchanged messages) and the choreography (i.e., the intended global behavior) can be easily derived from these languages.
To specify the behavior of a service (i.e., the concrete implementation of a peer), again a variety of languages exist. In essence, they all share a concept of a state (e.g., a state of a nite state machine, a marking of a Petri net, or control ow tokens in BPMN) and ways to specify message transfer. These basic concepts can be expressed with service automata.
De nition 3 (Service automaton). A service automaton A = [Q; I; O; ; q0; F ] is a tuple such that Q is a nite set of states, [I; O] is a peer, Q (EI [ EO [ f g) Q is a transition relation, q0 2 Q is an initial state, and F Q is a set of nal states. Thereby, EI := f?x j x 2 I \ MAg [ f!?x j x 2 I \ MS g and EO := f!x j x 2 O \ MAg [ f!?x j x 2 O \ MS g.
We say that A implements [I; O], and for (q; x; q0) 2 , we also write q !x q0. Beside internal (i.e., silent, non-communicating) steps and synchronous communication, service automata also model asynchronous communication, in which messages may overtake each other, but will never get lost. We claim that is | compared to FIFO queues for communicating nite state machines [4] | a more natural approach to model asynchronicity, because it makes less assumptions about the underlying infrastructure. In the composition of two or more service automata, pending asynchronous messages are represented by a multiset. Denote the set of all multisets over MA with Bags(MA). Further denote the empty multiset with [ ], and the multiset containing only one instance of x 2 MA with [x]. Addition of multisets is de ned pointwise.
De nition 4 (Composition of service automata). Let A1; : : : ; An be service automata such that their peers form a collaboration. De ne the composition A1 An as the automaton [Q; ; q0; F ] with Q := Q1 Qn Bags(MA), q0 := [q01 ; : : : ; q0n ; [ ]], F := F1 Fn f[ ]g, and, for all i 6= j the transition relation contains excactly the following elements: { [q1; : : : ; qi; : : : ; qn; B] ! [q1; : : : ; qi0; : : : ; qn; B],
i [qi; ; qi0] 2 i (internal move by Ai), { [q1; : : : ; qi; : : : ; qn; B] !!x [q1; : : : ; qi0; : : : ; qn; B + [x]],
i [qi; !x; qi0] 2 i (asynchronous send by Ai), { [q1; : : : ; qi; : : : ; qn; B + [x]] ?!x [q1; : : : ; qi0; : : : ; qn; B],
i [qi; ?x; qi0] 2 i (asynchronous receive by Ai), and { [q1; : : : ; qi; : : : ; qj ; : : : ; qn; B] !?!x [q1; : : : ; qi0; : : : ; qj0 ; : : : ; qn; B],
i [qi; !?x; qi0] 2 i and [qj ; !?x; qj0 ] 2 j (synchronization between Ai and Aj ). A run of A1 An is a sequence of events x1 xm such that q0 x!1 xm! qf with qf 2 F . For a run , de ne the conversation of as jE . The choreography of A1 An, denoted Chor (A1 An), is the union of the conversations of all runs of A1 An.
The composition is nite i , for each state, the number of pending asynchronous messages is bounded. The choreography of a composition of service automata is the set of all observable event sequences that are produced by runs of the composition. 3
With the notion of realizability, the conversations generated by a composition of services can be related to a speci ed choreography. Bultan et al. [5, 6] de ne realizability of choreographies as follows: De nition 5 (Complete realizability). A choreography C is completely realizable w.r.t. a collaboration fP1; : : : ; Png i there exists a tuple of service automata [A1; : : : ; An] such that, for all i, Ai implements Pi, and Chor (A1
An) = C.
Complete realizability is a strong requirement, because it demands that the observable behavior of the endpoints exactly matches the choreography. In reality, it is often the case that not all aspects of a choreography can be implemented. To this end, Zaha et al. [7] introduce a weaker notion called local enforceability (or partial realizability ) which only demands that a subset of the choreography is realized by the peer implementations: De nition 6 (Partial realizability). A choreography C is partially realizable w.r.t. a collaboration fP1; : : : ; Png i there exists a tuple of service automata [A1; : : : ; An] such that, for all i, Ai implements Pi, and Chor (A1 An) C. Obviously, complete realizability implies partial realizability. Though this weaker notion ensures that all constraints of the choreography are ful lled, it still xes a single tuple of service automata. If there does not exist such tuple of automata that realizes the complete choreography, there might still exist a set of tuples | each partially realizing the choreography | which distributedly realizes the complete choreography: De nition 7 (Distributed realizability). A choreography C is distributedly realizable w.r.t. a collaboration fP1; : : : ; Png i there exist tuples of service automata [A11 ; : : : ; An1 ]; : : : ; [A1m ; : : : ; Anm ] such that, for i = 1; : : : ; n and j = 1; : : : ; m, (i) Aij implements Pi, (ii) Chor (A1j Anj ) C, and (iii) Sjm=1 Chor (A1j Anj ) = C.
Distributed realizability allows for build time coordination between peers. While being a stronger notion than partial realizability (i.e., more of choreography's behavior is implemented), it is still a weaker notion than complete realizability.
y (a) collaboration
A !x x
B ?x ?!x ?!y (b) completely realizable choreography !x !y ?x ?y !y ?y (c) distributedly realizable choreography ?x !y (d) partially realizable choreography
As an example, consider the collaboration depicted in Fig. 1(a) in which two peers, A and B, communicate via message channels x and y. The choreography f!?x; !?yg in which the peers communicate synchronously (b) is completely realizable by a set of peers which synchronously decided whether to synchronize via message x or y. In case the messages are sent asynchronously (c), this is no longer possible. This choreography is not completely realizable, because there does not exist a single pair of service automata that implement the speci ed behavior. Instead, the implementations have to be coordinated: either peer A sends a message and peer B is quiet or the other way around. These two pairs distributedly realize the whole choreography. Finally, choreography (d) can only be partially realized, because the conversation !x!y?x?y cannot be implemented even if the peers are coordinated at build time. This is because the requirement that message x is sent before message y cannot be enforced, because the peers cannot coordinate this. 4
In this section, we show how the di erent realizability notions are related to controllability [8]. Controllability is a correctness criterion for services: a service A is controllable i there exists a service B such that A B is compatible (i.e., deadlock free). Controllability can be extended to multi-port services. In the following, we will transform a choreography into a multi-port service which is controllable if and only if the choreography is realizable.
For a regular1 choreography C, there exists a deterministic nite state machine that accepts exactly the sequences of the choreography. We call this state machine the monitor for C [9]. It unobtrusively monitors the interaction between the peers and reaches a nal state i the monitored conversation was part of the choreography.
De nition 8 (Monitor, monitored composition). Let C be a regular choreography w.r.t. a collaboration fP1; : : : ; Png. De ne the deterministic nite state machine accepting C (the monitor for C) as M = [QM ; M ; q0M ; FM ]. Thereby, QM is a nite set of states, M : QM E ! QM is a transition function, q0M 2 QM is an initial state, and FM QM is a set of nal states.
Let A1; : : : ; An be service automata implementing P1; : : : ; Pn. De ne the monitored composition M (A1 An) as the automaton [Q; ; q0; F ] with Q := QM Q1 Qn Bags(MA), q0 := [q0M ; q01 ; : : : ; q0n ; [ ]], F := FM F1 Fn [ ]], and, for all i 6= j, the transition relation contains excactly the following elements: { [q; q1; : : : ; qi; : : : ; qn; B] ! [q; q1; : : : ; qi0; : : : ; qn; B], i [qi; ; qi0] 2 i (internal move by Ai), { [q; q1; : : : ; qi; : : : ; qn; B] !!x [q0; q1; : : : ; qi0; : : : ; qn; B + [x]], i [qi; !x; qi0] 2 i and [q; !x; q0] 2 M (asynchronous send by Ai, monitored by M ), { [q; q1; : : : ; qi; : : : ; qn; B + [x]] ?!x [q0; q1; : : : ; qi0; : : : ; qn; B], i [qi; ?x; qi0] 2 i and [q; !?; q0] 2 M (asynchronous receive by Ai, monitored by M ), { [q; q1; : : : ; qi; : : : ; qj ; : : : ; qn; B] !?!x [q0; q1; : : : ; qi0; : : : ; qj0 ; : : : ; qn; B], i [qi; !?x; qi0] 2 i, [qj ; !?x; qj0 ] 2 j , and [q; !?x; q0] 2 M (synchronization between Ai and Aj , monitored by M ).
The monitor synchronizes with the message events of the service automata, but does not constrain their behavior. The monitor only has an e ect on the nal states of the composition. Only if all service automata and the monitor reach a nal state, this state is nal in the monitored composition.
We can now change the point of view and regard the monitor as a service that is communicating with several other services by synchronous message events. Again, this service will reach a nal state i the message events from the environment are observed in the correct order.
De nition 9 (Monitor service automaton). Let C be a regular choreography w.r.t. a collaboration fP1; : : : ; Png and let M = [QM ; M ; q0M ; FM ] be a monitor for C. De ne the monitor service automaton AM := [Q; I; O; ; q0; F ] with Q := QM , I := fI1; : : : ; Ing, O := fO1; : : : ; Ong, q0 := q0M , and F := FM . De ne : Q f!?hxi j x 2 Eg ! Q with (q; !?hxi) := M (q; x). 1 Choreographies speci ed by interaction Petri nets, UML collaboration diagrams,
BPMN, or Let's Dance are always regular if they assume synchronous communication. Due to the nature of a choreography to exist of message events (not the messages itself), all message events of the monitor service automaton are synchronous. The original nature of the event (synchronous or asynchronous) is, however, encoded in the events by using the event ?!hxi for event x. The existence of service automata that are compatible to this monitor service automaton proof realizability of the choreography: Theorem 1. Let C be a regular choreography w.r.t. a collaboration fP1; : : : ; Png and AM a monitor service automaton for C. 1. C is partially realizable i AM is decentralized controllable. 2. C is distributedly realizable i AM is decentralized controllable and for the set of strategies S holds: S[A1;:::;An]2S Chor (A1 An) = C. 3. C is completely realizable i AM is decentralized controllable and there exists a strategy [A1; : : : ; An] such that Chor (A1 An) = C.
A strategy for the monitor service automaton is a set of service automata such that the overall composition is compatible. While these automata communicate solely synchronously with the monitor service automaton, a tuple of service automata that actually realize the original choreography can be derived by changing every message event !?hxi back to x (e.g. \!?h!xi" to \!x"). These service automata then can also communicate asynchronously with other peers, yet still follow the speci ed choreography. 5
In this paper, we linked the realizability problem to controllability, making existing tools and algorithms applicable to check choreographies. In particular, our approach allows for speci cation and synthesis of asynchronous peer implementations. This avoids a subsequent analysis and correction when trying to \asynchronize" peer implementations [10]. The current results are independent of a concrete choreography or service description language, but can be easily adapted.
In future work, we plan to study how choreography and service design can be mixed. For example, the realizability of a choreography can be checked w.r.t. some already completely speci ed peers. Such an approach would nicely complement the participant synthesis introduced in [11] by using controllability for both interaction models and interconnection models.
Acknowledgements This work is funded by the DFG project \Operating Guidelines for Services" (WO 1466/8-1). 2. Decker, G., Weske, M.: Local enforceability in interaction petri nets. In: BPM 2007.
LNCS 4714, Springer (2007) 305{319
3. Zaha, J.M., Barros, A.P., Dumas, M., Hofstede, A.H.M.t.: Let's dance: A language
for service behavior modeling. In: OTM 2006. LNCS 4275, Springer (2006) 145{162
4. Brand, D., Za ropulo, P.: On communicating nite-state machines. J. ACM 30(2)
(1983) 323{342
5. Fu, X., Bultan, T., Su, J.: Conversation protocols: a formalism for speci cation
and veri cation of reactive electronic services. Theor. Comput. Sci. 328(