Modelling Concurrent Systems with Interval Processes

Abstract

Standard operational semantics of the majority of concurrency models is defined in terms of either sequences or step sequences, while standard concurrent history semantics is usually defined in terms of partial orders, stratified order structures (or structures equivalent to them as net processes). It is commonly assumed (first argued by N. Wiener in 1914) that any system run (execution) that can be observed by a single observer must be an interval order of event occurrences. However, generating interval orders directly is problematic for most models of concurrency, as the only feasible sequence representation of interval order is by using Fishburn Theorem (1970) and appropriate sequences of beginnings and endings of events involved. It was shown by Janicki and Koutny in 1997 that concurrent histories involving interval orders can be represented by interval order structures, but how these interval order structures could be derived for particular concurrent systems was not clear. My original contribution to knowledge is defining an interval order semantics for Petri Nets with Inhibitor Arcs. We start with introducing operational interval order semantics, and then we generalize the concept of net process to represent the set of equivalent executions modelled by interval orders. Next we will show that our interval processes correspond to appropriate interval order structures. Finally, we will prove that our model is equivalent to that of Janicki and Yin (2015) where novel interval traces are used to represent equivalent executions. We will also demonstrate that our model covers simpler cases where sequences or step sequences were used to represent system runs.