Toggle Main Menu Toggle Search

ePrints

Causal Structures for General Concurrent Behaviours

Lookup NU author(s): Professor Maciej Koutny, Dr Lukasz Mikulski

Downloads


Abstract

Non-interleaving semantics of concurrent systems is often expressed using posets, where causally related events are ordered and concurrent events are unordered. Each causal poset describes a unique concurrent history which is a set of executions, expressed as sequences or step sequences, consistent with it. Moreover, such a poset captures all precedence-based invariant relationships between the events in the executions belonging to the concurrent history. Causal poset semantics underpins efficient verification techniques based on unfoldings of safe Petri nets and concurrent automata models. However, when one considers extensions of these standard models, such as nets with inhibitor arcs, concurrent histories become too intricateto be described solely in terms of causal posets.In this paper, we introduce and investigate generalised mutex order structures which can capture the invariant causal relationships in any concurrent history consisting ofstep sequence executions. Each such structure comprises two relations, viz. interleaving/mutex and weak causality. As our main result we prove that each generalised mutex order structure is the intersection of step sequence executions which are consistent with it.


Publication metadata

Author(s): Janicki R, Kleijn J, Koutny M, Mikulski L

Publication type: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2013

Pages: 28

Print publication date: 01/03/2013

Source Publication Date: March 2013

Report Number: 1378

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/1378.pdf


Share