Abstract. In Service Oriented Architectures (SOAs) services invoked in a composition can be replaced by other services, which are possibly discovered and bound at runtime. Most of the research efforts supporting this replacement assume that the interface of the interchangeable services are the same and known at design time. Such assumption is not realistic since it implies that providers of the same kinds of services agree on the interfaces the services offer. By interface mapping we mean the class of approaches aiming at relaxing this assumption. Most of those approaches available in the literature focus on stateless services and simply address mapping operation names and data structures. Instead, this paper focuses on conversational services for which the sequence of required operation calls, i.e., the interaction protocol, matters. We use model checking to automatically identify the interaction protocols mapping. We validate our technique both by applying it to the invocation of two...