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.
翻译:将结构操作语义学(SOS)扩展为真并发SOS是自然的。从SOS到真并发SOS,本质上是为SOS中的相关概念赋予一个真并发的语义学基础,即一个变迁通过执行一个偏序多集(pomset)的动作而触发,而非仅执行单个动作。在SOS框架下,向真并发语义的扩展中,某些方面发生了变化:标记变迁系统(LTS)被推广为Pomset LTS(PLTS),变迁系统规范(TSS)被推广为Pomset TSS(PTSS),交错行为等价被推广为真并发行为等价,TSS的互模拟格式被推广为PTSS的相应格式;同时,某些方面得以保留,例如保守扩展的概念、TSS与PTSS的含义、高阶语言以及指称语义学。