Pi演算行为等价理论在Web服务组合中的应用研究

Pi演算的行为等价理论是判断两个并发执行的并且与外部存在交互的系统之间是否具有等价行为（Equivalent Behavior）。如果两个系统具有等价行为，则可以在任何环境中使用一个系统去替换另一个系统。Pi演算中的行为等价理论在互模拟技术的基础上，提供了基于强互模拟的强等价关系和基于弱互模拟的弱等价关系。

定义3.1　如果进程上的二元关系ℜ对于二元组PℜQ满足下面3个条件，则关系ℜ为强模拟。

（1）若，且，则存在一个进程Q′，满足且P′ℜQ′；

（2）若，且，则存在一个进程Q′，满足且对于从x接收的任意名字w都有；

（3）若，且，则存在一个进程Q′，满足且。

定义3.2　如果关系ℜ和ℜ的逆都是强模拟，则关系ℜ为强互模拟关系。

定义3.3　如果在进程P和Q之间存在一个强互模拟ℜ使得（P，Q）∈ℜ，即P和Q是强互模拟的，则这两个进程为强等价，记为P～Q，或者称为强互相似。

定义3.4　如果进程上的二元关系ℜ对于二元组PℜQ满足下面两个条件，则关系ℜ为弱模拟。(www.xing528.com)

（1）若，且，则。

（2）若，且，则。

这里定义了两个记号：，即⇒为→的传递自反闭包，，其中S=α1α2…αn。

定义3.5　如果关系ℜ和ℜ的逆都是弱模拟，则关系ℜ为弱互模拟关系。

定义3.6　如果在进程P和Q之间存在一个弱互模拟ℜ使得（P，Q）∈ℜ，即P和Q是弱互模拟的，则这两个进程为弱等价，记为P≈Q，或者称为弱互相似。

进程间的强互模拟要求进程的内部行为与外部行为都要一致，如果两个进程为强互模拟，则其中一个进程的任意行为动作都可以被另一个进程所模拟，反之亦然。而进程间的弱互模拟允许模拟进程在执行模拟操作的前后可以执行若干内部通信动作，但在外部看来其行为是一致的，即其中一个进程所能执行的动作，另一个进程也能模拟。