Linking theories of concurrency by retraction

Theories of concurrency can be distinguished by the set of processes that they model, and by their choice of pre-ordering relation used to compare processes to prove their correctness. A link between two theories is a function L, which maps the processes of the source theory onto those of the target theory. Its image defines exactly the set of processes of the target theory. The ordering relation of the target theory is obtained by applying the link L to one or both operands of the source theory ordering. We will use the normal transition rules of a structured operational semantics to define a series of linking functions: W for weak simulation, R for refusals, T for traces refinement, D for divergences, etc. We then show that each function is a retraction, in the sense that it is monotonic, decreasing and idempotent. Finally we show their composition is a retraction.