Structural Operational Semantics for True Concurrency
Yong Wang
TL;DR
This work builds a formal bridge from traditional structural operational semantics to true concurrency by replacing single-action steps with pomset-based transitions and generalizing LTS/TSS to PLTS/PTSS. It introduces a comprehensive arsenal of true-concurrency notions, including pomset/bisimulation, simulation, ready variants, and history-preserving relations, along with Baldan-Crafa logic (BCL) and its fragments to characterize these semantics. The paper develops model-theoretic, proof-theoretic, and stratification-based approaches for PTSSs, including three-valued stable models, ws-completeness, operational conservative extensions, and a suite of rule formats (panth, ntree, De Simone, GSOS, RBB safe) that ensure various congruence properties. Together these contributions provide a robust framework for specifying and reasoning about truly concurrent systems, bridging SOS with true concurrency formalisms and enabling axiomatization and rewriting techniques in a non-interleaving setting.
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.