Structural Operational Semantics for True Concurrency
This work provides a theoretical foundation for true concurrency in operational semantics, which is relevant for researchers in concurrency theory and formal methods.
The paper extends Structural Operational Semantics (SOS) to a truly concurrent setting by replacing single-action transitions with partially ordered multisets (pomsets) of actions, generalizing labeled transition systems to pomset LTS and transition system specifications to pomset TSS, while preserving concepts like conservative extension. The result is a foundational framework for true concurrency in SOS.
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.