Quasi-stratified Order Semantics of Concurrency

TL;DR

The paper introduces quasi-stratified orders (qs-orders) as a new middle-ground semantic model for concurrent systems between stratified and interval orders, formalising them with two relations $\prec$ and $\sqsubset$ to capture precedence and not-later-than. It develops two complementary specification formalisms: qs-orders with quasi-stratified sequences (QSS) and quasi-stratified structures (QSAS), and establishes a hierarchy with maximal (QSMS) and closed (QSCS) variants connected through closure mappings. Key results include the equivalence $\text{QSMS}=\text{QSAS}^{\max}$ and $\text{QSCS}=\text{QSAS}^{\text{clo}}$, along with a constructive correspondence between qs-orders and qs-sequences and a robust closure framework. The framework targets hierarchical/transaction-like concurrency, offering succinct relational specifications that can improve validation and potentially alleviate state-space explosion in verification and scheduling tasks, with future work linking to interval-trace theories.

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.

Figures (6)

• Figure 1: The hierarchy of partial orders represented as directed graphs.
• Figure 2: The hierarchy of forbidden cycles.
• Figure 3: A qs-order which is not stratified, and stratified order which is not qs-order.
• Figure 4: A qsa-structure together with one of its qsm-structures and an interval representation of the corresponding qs-order. Solid and dashed arcs represent relations $\prec$ and $\sqsubset$, respectively. We take advantage of the fact that in the qsm-structures $\prec$ is included in $\sqsubset$.
• Figure 5: A qsa-structure and its closure. We take advantage of the fact that in csc-structures $\prec$ is included in $\sqsubset$ (and only provide solid arcs for such relationships).