论文部分内容阅读
进程演算从20世纪80年代Milner的CCS交互模型开始已有30年光景.期间成百上千的模型和等价关系被提出来,研究也深入了相关的各个分支。但是在完备交互模型上研究计算理论是一个还未深入研究的方向。对于这个方向首先面临的问题是定义合适的完备模型。绝对等价在完备模型中是个重要的概念,它和传统的外部等价是否一致也是一个有趣且重要的问题。这个问题的解决有助于对互模拟等价关系的进一步理解,更重要的是它能帮助证明一个模型是否是完备的。在绝对等价和外部等价的一致性问题上已经有一些结果。如果在语言中包含加操作符,那么一致性就相对较容易证明,反之,会变得很困难。实际上对在没有加操作符的语言上的一致性已经作为公开问题。加操作符有强大的观察能力而绝对等价又是从观察角度定义的,所以我们可以用加操作符来迫使一个进程做一连串特定的动作。当没有加操作符的时候模型会变得简单。一个模型越简单它的观察能力就越弱,于是证明一致性就更难。但是当模型足够简单时,特别地,当它是有限模型时,我们可以借助有限进程的性质来帮助证明。在一个有限且没有加操作符的模型下,当一个进程做了一个外部动作后它的其他交互能力都还保留。我们利用这个性质证明了有限且没有加操作符的CCS和π演算下的一致性。