Composition of Interactive Web Services Based on Controller Synthesis

We study an abstract form of service composition where Web services are represented as nondeterministic communicating automata. Considering the case in which communication is done via channels able to hold at most one message at a time, the service composition problem consists, given a client service, a goal service and a community of available services, to determine whether there exists a mediator service able to communicate with the client and the services of the given community in such a way that their global behavior satisfies the client service request expressed as the given goal service. We demonstrate the decidability of this problem via a reduction to a decidable control problem.