On Locality and the Exchange Law for Concurrent Processes

erschienen 2011 in Joost-Pieter Katoen, Barbara Könnig (eds.): CONCUR 2011 - Concurrency Theory, LNCS 6901, 2011.

Abstract: This paper studies algebraic models for concurrency, in light of recent work on Concurrent Kleene Algebra and Separation Logic. It clarifies that there is a strong connection between the Concurrency and Frame Rules of Separation Logic and a variants of the excahnge law of Category Theory. The algebraic laws admit two standard models: one uses sets of traces, and the other is state-based, using assertions and weakest preconditions. We relate the latter to standard models of the heap as a partial function. We exploit the power of algebra to unify models and classify their variations.