Agents interoperability via conformance modulo mapping

We present an algorithm for establishing a flexible conformance relation between two local agent interaction protocols (LAIPs) based on mappings involving agents and messages, respectively. Conformance is in fact computed "modulo mapping": two LAIPs τ and τ may involve different agents and use different syntax for messages, but may still be found to be conformant provided that a given map from entities appearing in τ to corresponding entities in τ is applied. LAIPs are modelled as trace expressions whose high expressive power allows for the design of protocols that could not be specified using finite state automata or equivalent formalisms. This expressive power makes the problem of stating if τ conforms to τ undecidable. We cope with this problem by over-approximating trace expressions that may lead to infinite computations, obtaining a sound but not complete implementation of the proposed conformance check.