Invariant semantics of nets with inhibitor arcs

Abstract

We here discuss an invariant semantics of concurrent systems which is a generalisation of the causal partial order (CPO) semantics. The new semantics is consistent with the full operational behaviour of inhibitor and priority nets expressed in terms of step sequences. It employs combined partial orders, or composets, where each composet is a relational structure consisting of a causal partial order and a weak causal partial order. In this paper we develop a representation of composets using a novel concept of comtrace, which is certain equivalence class of step sequences. The whole approach resembles to a significant extent the trace semantics introduced by Mazurkiewicz. Composets correspond to posets, comtraces correspond to traces, while step sequences correspond to interleaving sequences. The independency relation is replaced by two new relations. The first is simultaneity which is a symmetric relation comprising pairs of event which may be executed in one step. The other is serialisability which comprises pairs of events (e,f) such that if e and f can be executed in one step then they can also be executed in the order: e followed by f. We show that the comtraces enjoy essentially the same kind of properties as Mazurkiewicz traces, e.g., each comtrace is unambiguously identified by any step sequence which belongs to it. As a system model we consider Elementary Net Systems with Inhibitor Arcs (ENI-systems). We show that the comtrace model provides an invariant semantics for such nets and is in a full agreement with their operational semantics expressed in terms of step sequences. We finally show that the composets represented by comtraces can be generated by generalising the standard construction of a process of a 1-safe Petri net.