论文部分内容阅读
该文的主要研究内容和成果包括:1.非对称χ<≠>-演算的语法和语义 定义了非对称χ<≠>-演算的语法和语义:在语法上,给出了一组算子用以构造进程,其中就有不等名算子[x≠y];语义上,引入了一个标号转移系统来定义操作语义,强调非对称通信,即区分输入和输出动作,例如形如ax的动作是输出动作,而形如ax的动作则为输入动作.2.非对称χ<≠>-演算的互模拟格 在类χ-演算中,一般用L-互模拟来研究各互模拟关系之间的相关性.L-互模拟的基本思想是,不同的观察者所能看到的进程行为是不同的,因此所能区别的进程对也是不一样的.L-互模拟试图将所有不同的观察行为进行分类,定义出相应的进程间的等价关系.根据这些L-互模拟关系之间的序关系,我们可以构造互模拟格.3.非对称χ<≠>-演算中barbed互模拟的操作性质和代数性质 Barbed互模拟定义简单,可以有效地生成一个合理的观察等价关系,而且对标号转移系统和归约语义均适用,所以在研究一个新进程演算的普适性时,通常要研究barbed互模拟.对通道类的进程演算来说,这种方法通常会得到该演算的最弱的互模拟等价关系.另外,由于barbed互模拟可以应用于各种进程演算中,所以也可用来研究各演算之间的关系.该论文定义了强、弱barbed互模拟关系,并确定了barbed互模拟在互模拟格中处于顶元的位置;研究了barbed互模拟的操作性质,可以看到由于不等名算子和非对称通信结构的存在,其性质相当复杂.Barbed互模拟关系对上下文的依赖性使其难以理解,因此该论文给出了barbed互模拟关系的开形式等价定义,根据该定义可以清楚地了解barbed互模拟进程对的行为方式.开互模拟关系是一个在替换下封闭的互模拟关系,是移动进程最自然的互模拟关系.开barbed互模拟关系既给出了barbed互模拟关系的上下文无关刻划,又有助于建立相应的barbed同余关系的公理化系统.4.非对称χ<≠>-演算的其他L-互模拟关系的性质和公理化研究 该论文最后研究了互模拟格中其他L-互模拟关系的性质.首先,给出了L-互模拟关系的定义及其开形式刻划,并证明了二者的一致性;然后在开L-互模拟关系的基础上定义L-同余关系;最后根据开L-互模拟关系的定义并不是通过对开barbed互模拟关系的定义进行简单地删减而获得的,它们的定义充分体现了相应的L-互模拟关系的性质.另外,L-同余关系的定义也不尽相同,而它们的公理化系统则各具特点.