Relational Structures for Interval Order Semantics of Concurrent Systems

Relational structures like partial orders that are based on acyclic relations capturing a ‘before’ relationship, can provide versatile frameworks for the modelling and verification of a wide class of concurrent systems behaviour. There are also relational structures with an acyclic ‘before’ (strong precedence) relationship and a possibly cyclic ‘not later than’ (weak precedence) relationship, which can be used for more general concurrent behaviours. However, in each of these cases, the execution model is based on sequences or step sequences of executed actions, where actions are assumed to be executed instantaneously. In this paper, we drop this restriction and consider executions modelled by interval orders, where actions are assumed to be executed non-instantaneously. For this execution model, we introduce new relational structures which can capture both strong precedence and weak precedence. This is achieved, in particular, thanks to a novel notion of acyclicity where any mixed cycle of strong and weak precedence is allowed, provided that it contains at least two consecutive weak precedence relationships.