Fully abstract models and refinements as tools to compare agents in timed coordination languages

AbstractCoordination languages and models promote the idea of separating computation and interaction aspects. As for traditional concurrency models, the question of safely replacing an agent by another one in any interacting context naturally appears. This paper proposes two tools to answer that question. On the one hand, a fully abstract semantics allows us to identify two processes which behave similarly in any context. On the other hand, a refinement theory allows us to compare processes that appear to be different in view of the fully abstract semantics but which satisfy the substitutability property: if the implementation I refines the specification S and if C[S] is deadlock free, for some context C, then C[I] is also deadlock free. Both theories are novel, are exposed in the context of our timed coordination languages but may actually be transposed in the context of almost any data-driven coordination language