Realizable temporal logics for web service choreography

• A new & better service implementation algorithm for p-LTL choreographies.
• Introduction of a more expressive logic q-LTL for choreography.
• Service implementation algorithm for q-LTL choreographies.
• A brief undecidability argument for q-LTL with a reference for details.
• Multiple choreography examples in p-LTL & q-LTL.

Web service choreographies specify conditions on observable interactions among the services. An important question in this regard is realizability: given a choreography C, does there exist a set of service implementations I that conform to C? Further, if C is realizable, is there an algorithm to construct implementations in I?We propose two local temporal logics, p-LTL and q-LTL, to specify choreographies. The choreographies written in these logics are realizable by design. The semantics of the logics are defined in terms of partial orders, called Lamport diagrams. For specifications in these logics, we give algorithms to construct service implementations as communicating automata. p-LTL choreographies are realized in terms of nondeterministic finite state automata with a coupling relation, whereas q-LTL choreographies are realized in terms of nondeterministic finite state automata with FIFO queues.