A simple formal method to synthesize an orchestrator in web service composition

We study the following web service composition problem: given existing web services S₁, ⋯, S_n and a desired web service S₀, the objective is to synthesize an orchestrator Orch that coordinates S₁, ⋯, S_n so that S₀ is provided. We develop a simple input-output automata-based method that solves this composition problem. We also study whether the desired service S₀ is totally or partially provided by the system ((S_i)_i=1⋯n, Orch). The studied problem can be seen as a control problem, where Orch is a controller that restricts the behaviors of S₁, ⋯, S_n so that the controlled system conforms to S₀.