Structural Operational Semantics for True Concurrency

TL;DR

This paper extends Structural Operational Semantics to true concurrency by introducing a framework where transitions are represented by partially ordered multisets of actions, generalizing traditional interleaving semantics.

Contribution

It develops a formal foundation for true concurrency in SOS by defining Pomset LTS and PTSS, enabling truly concurrent semantics within the SOS framework.

Findings

Introduces Pomset LTS (PLTS) for true concurrency

Defines Pomset TSS (PTSS) as an extension of TSS

Maintains core concepts like conservative extension and denotational semantics

Abstract

It is natural that we can extend Structural Operational Semantics (SOS) to SOS for true concurrency. From SOS to SOS for true concurrency, it is in nature to give the related concepts in SOS a truly concurrent semantics foundation, i.e., a transition occurs by executing a Partially Ordered Multi Set (pomset) of actions replacing just one single action. Under the framework of SOS, for the extension to the truly concurrent one, something are changing: Labelled Transition System (LTS) is generalized to Pomset LTS (PLTS), Transition System Specification (TSS) to Pomset TSS (PTSS), interleaving behavioural equivalences to truly concurrent ones, congruence formats of TSSs to those of PTSSs; something are remained, such as the concept of conservative extension, the meanings of TSSs and PTSSs, higher-order languages and denotational semantics.