In the development of operational semantics of concurrent systems, a key
decision concerns the adoption of a suitable notion of execution model, which
basically amounts to choosing a class of partial orders according to which
events are arranged along the execution line. Typical kinds of such partial
orders are the total, stratified and interval orders. In this paper, we
introduce quasi-stratified orders - positioned in-between the stratified and
interval orders - which are tailored for transaction-like or hierarchical
concurrent executions.
Dealing directly with the vast number of executions of concurrent system is
far from being practical. It was realised long time ago that it can be much
more effective to consider behaviours at a more abstract level of behavioural
specifications (often based on intrinsic relationships between events such as
those represented by causal partial orders), each such specification -
typically, a relational structure - encompassing a (large) number of
executions.
In this paper, we introduce and investigate suitable specifications for
behaviours represented by quasi-stratified orders. The proposed model of
quasi-stratified relational structures is based on two relationships between
events - the 'before' and 'not later' relationships - which can be used to
express and analyse causality, independence, and simultaneity between events.