We study the problem of automatic web service composition. We consider a formal framework where web service business protocols are described by means of Finite State Machines (FSM) and focus on the protocol synthesis problem. We show that this problem can be reduced to that of testing a simulation relation between an FSM and an (infinitely) iterated product of FSMs. While this later problem has never been investigated in the literature, existing results regarding close decision problems in the context of shuffle languages, an extension of regular languages with shuffle and shuffle closure operators, are rather negative and cannot be directly exploited in our context. In this paper, we develop a novel technique to prove the decidability of testing simulation in the case of interest in our setting. As a consequence, our results solve the problem of web service composition (synthesis) existence in presence of an unbounded number of instances, a problem left open in recent related works.
