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.
翻译:自然可以将结构操作语义学(SOS)扩展至适用于真并发的SOS。从SOS到真并发SOS,本质上是为SOS中的相关概念赋予真并发语义基础,即变迁通过执行一个偏序多重集(pomset)的动作而非单一动作来实现。在SOS框架下,向真并发方向的扩展带来若干变化:标号变迁系统(LTS)被推广为偏序多重集变迁系统(PLTS),变迁系统规范(TSS)被推广为偏序多重集TSS(PTSS),交错行为等价关系被替换为真并发行为等价关系,TSS的同余格式相应演变为PTSS的同余格式;同时,保守扩展的概念、TSS与PTSS的语义含义等要素得以保留。