论文摘要
高阶进程演算,因为其很强的抽象能力和理论上的重要性,在进程演算领域一直得到广泛的关注,并成为描述和分析具有动态变换特性的内部连接结构的移动系统的有效数学工具。在本文中,我们对高阶进程演算就如下几方面进行了研究。·带有mismatch的高阶π演算:互模拟理论;带有mismatch的高阶π演算的线性片段:公理化。高阶进程演算的公理化问题,如高阶π演算的公理化问题,一直以来鲜有相关工作。然而无论在理论上还是在应用中,判断两个高阶进程是否在某种互模拟下等价都有其重要意义,这种判断需要一个能够有效地进行分析并给出结论的算法。从算法的观点看,mismatch是在互模拟理论以及公理化中都是很有用的操作子;我们通过考察带有mismatch的高阶π演算来深入研究了公理化问题。我们首先形式化地定义并讨论了存在mismatch时的互模拟理论,其中我们的互模拟称为开弱高阶互模拟,这是一种nondelayed型的开型互模拟。随后,在设计公理系统时我们采用了线性方法,即将演算限制到线性片段上。利用对开弱高阶互模拟的刻画,包括前缀进程间等价与其延续进程间等价之间的关系以及线性演算独有的性质,我们最终证明了公理系统的完备性。我们对高阶互模拟理论和公理化的研究,不仅通过引入一个有用的操作子对以往的工作进行了扩展,且将高阶公理化的研究又向前推进了一步,同时为对其它高阶演算(如Ambient演算)的研究提供了参考。·高阶CCS编码一阶π演算。不同演算之间的编码是比较它们的表达能力的有效方法,可以揭示它们之间的本质区别。Thomsen和Sangiorgi对高阶演算(分别是高阶CCS和高阶π演算)与一阶π演算之间的相互编码进行了研究,但他们的工作尚不完整,缺少对用高阶CCS对一阶π演算编码的全抽象性质的深入研究。在本文中,我们试图解决这一问题。我们基于Thomsen的编码方法,将一阶π演算翻译到Plain CHOCS中。我们证明这种编码方法在基互模拟性(一阶π演算中)和wired互模拟性(Plain CHOCS中)下是全抽象的,其中wired互模拟性是我们定义的基于仅发送和接收线缆(wire)的wired进程的一种互模拟,它们是编码策略的核心。进一步,由于wired互模拟性蕴含广为人知的上下文互模拟性,我们确保了在基互模拟性和上下文互模拟性下编码的可靠性。我们使用领域中已有的索引技术来处理技术细节中的难点以获得主要结论,即将索引技术应用到原始编码方法中,以此来处理编码中产生的额外内部动作,随后将带索引的编码方法中所获得的结果移植得到原始编码中的相应结论。我们还讨论了如何通过在两个演算中选抒合理的互模拟来获得全抽象性质等问题。我们对进程演算问编码的研究解决了关于在高阶CCS中表达一阶π演算的一个末决问题,从而补充了这两类演算之间的编码研究,这进一步展现了一阶演算和高阶演算之间的关系。此外,编码研究的结果还提供了用高阶演算来实现对λ演算编码的另一种方法。·线性高阶π演算中局部互模拟的逻辑刻画。除了用代数方法对高阶进程演算的互模拟进行工作外,从逻辑角度对互模拟的研究也有其价值所在,目前已经有对Plain CHOCS中的强和弱上下文互模拟进行逻辑刻画的工作。在本文中,我们用逻辑的方法对线性进程演算进行了一些新的研究。我们致力于找到一种对线性高阶π演算中局部互模拟的逻辑刻画。为此我们通过两步来完成准备:首先我们通过一些变体来简化局部互模拟性;其次我们通过互模拟递减链来逼近局部互模拟性。为实现逻辑刻画,我们对演算进行了重新形式化,以获得相对容易实现刻画的等价形式(在互模拟意义上)。我们的逻辑具有完整的非操作(对偶性),并且比已有的逻辑语言简单,这体现在高阶模态被降阶为类似于一阶模态,且构造蕴含操作子仅被用于处理一阶受限输出。我们证明了刻画定理,它将逻辑等价与局部互模拟性相关联。我们关于逻辑刻画的工作对高阶进程演算研究的意义在于提供了另一种观点,即逻辑的观点,以此补充了代数角度的研究。此外,将检验互模拟等价转换为检验逻辑等价使得我们马上可以使用逻辑的一整套方法,后者不但具有诸多模型检测算法,而且有许多实用的工具。本文不仅对高阶进程演算领域内的几个方面的问题进行了研究,且传递了几点有意义的信息。首先是线性性质在确保高阶演算的可靠且完备的公理系统中具有重要意义,这一特征成功的降低了通信进程的表达能力。其次,作为用一阶π演算来表达高阶演算的补充,我们证明了其反向在一些合理的互模拟性下亦成立,这使得我们可以更加确信高阶演算的相对独立性,结合其特有的抽象能力,这种独立性使得高阶演算更有吸引力。再次,通过展示一种可以刻画互模拟等价的简单且完备的逻辑语言,我们的逻辑刻画工作提供了对线性性质的进一步认识,并扩展了高阶进程演算的应用领域。