2005 | OriginalPaper | Buchkapitel
Linking Theories of Concurrency by Retraction
verfasst von : He Jifeng
Erschienen in: Distributed Computing and Internet Technology
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.