Lookup NU author(s): Professor Maciej Koutny,
Dr Lukasz Mikulski
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License (CC BY-NC 4.0).
Non-interleaving semantics of concurrent systems is often expressed using posets, wherecausally related events are ordered and concurrent events are unordered. Each causal poset describesa unique concurrent history, i.e., a set of executions, expressed as sequences or step sequences, thatare consistent with it. Moreover, a poset captures all precedence-based invariant relationships betweenthe events in the executions belonging to its concurrent history. However, concurrent historiesin general may be too intricate to be described solely in terms of causal posets. In this paper, weintroduce and investigate generalised mutex order structures which can capture the invariant causalrelationships in any concurrent history consisting of step sequence executions. Each such structurecomprises two relations, viz. interleaving/mutex and weak causality. As our main result we provethat each generalised mutex order structure is the intersection of the step sequence executions whichare consistent with it.
Author(s): Janicki R, Kleijn J, Koutny M, Mikulski Ł
Publication type: Article
Publication status: Published
Journal: Fundamenta Informaticae
Print publication date: 08/07/2015
Acceptance date: 17/05/2015
Date deposited: 29/05/2015
ISSN (print): 0169-2968
ISSN (electronic): 1875-8681
Publisher: IOS Press
Altmetrics provided by Altmetric