Quasi-stratified Order Semantics of Concurrency

TL;DR

This paper introduces quasi-stratified orders as a new class of partial orders for modeling concurrent system executions, bridging the gap between stratified and interval orders, and develops relational structures for their analysis.

Contribution

It proposes quasi-stratified orders for hierarchical concurrency and develops relational models based on 'before' and 'not later' relations for analyzing concurrent behaviors.

Findings

Quasi-stratified orders effectively model hierarchical concurrent executions.

Relational structures based on causal and independence relations facilitate analysis.

The approach provides a new framework for abstract behavioral specifications.

Abstract

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.