A Local Logic for Realizability in Web Service Choreographies

TL;DR

This paper introduces a local temporal logic for specifying web service choreographies and provides an algorithm to determine their realizability by constructing corresponding automata, with an implementation and experimental evaluation.

Contribution

It proposes a novel local logic for choreographies and offers an algorithm to decide realizability by constructing communicating automata, including an implementation and experiments.

Findings

Algorithm successfully constructs service implementations when realizable.

Implementation demonstrates practical feasibility through experimental results.

Logic effectively specifies choreographies and determines realizability.

Abstract

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 a local temporal logic in which choreographies can be specified, and for specifications in the logic, we solve the realizability problem by constructing service implementations (when they exist) as communicating automata. These are nondeterministic finite state automata with a coupling relation. We also report on an implementation of the realizability algorithm and discuss experimental results.