May测试语义前同余性的研究

在面向服务器的进程代数理论中,为了描述服务器和客户之间的并发行为,Bernardi和Hennessy等人提出了三种must-testing语义,并对它们的前同余性以及公理系统进行了研究。但是关于may-testing语义并未涉及,本文将对可能测试语义的前同余性进行研究。

ntyft/ntyxt算子下共变-异变模拟的前同余性

进程代数是刻画并发与交互式反应系统行为的重要模型之一,进程间的(互)模拟关系及其公理化以及结构化操作语义(structural operational semantics,SOS)理论是其重要的两个研究方向。共变-异变模拟(covariant-contravariant simulation,CC-模拟)是(互)模拟关系概念的推广,它对动作进行区分,表达了状态的行为数目越多但并不一定越好的事实。行为关系的(前)同余性质在支持其形式规范的模块化构建和公理系统的推理方面具有重要意义。(前)同余性的证明需要根据进程代数语言中算子的SOS规则逐个验证。为了避免(前)同余性证明的重复劳动,学术界提出了多种类型的SOS规则的框架形式。ntyft/ntyxt规则形式是目前具有代表性的SOS规则框架形式之一。文中基于ntyft/ntyxt规则形式,提出了能满足CC-模拟前同余性的最大ntyft/ntyxt子类CC-ntyft/ntyxt规则形式,并证明了CC-模拟相对CC-ntyft/ntyxt算子的前同余性。