Pi演算操作语义研究成果

Pi演算中的操作语义与CCS中对应的定义有相同的结构，尽管如此，在相当大的程度上细节都是不同的。简要地说，CCS与目前的Pi演算之间的区别主要来自于受限操作符（vx）。

Pi演算的操作语义是通过标记变迁系统（Labeled Transition System，LTS）定义的一系列规则，用于说明进程能够执行的动作，以表明进程的行为能力。每条规则都以A/B这样的形式出现，表示如果A成立，则B也成立。

TAU-ACT规则表示进程τ.P在执行完内部哑操作之后，无条件地演变成进程P。

OUTPUT-ACT规则表示进程.P在执行完输出操作之后，无条件地演变成进程P。

INPUT-ACT规则表示进程x（z）.P在执行完输入操作之后，即在通道x中输入名字w代替名字z之后，无条件地演变成进程P，并将进程P中的名字z也用名字w代替。

SUM规则表示若进程P在执行完操作α之后演变成进程P′，则进程P+Q在执行完操作α之后同样可以演变成进程P′。这里的操作α表示操作x（y）、或τ。

MATCH规则表示若进程P在执行完操作α之后演变成进程P′，则如果名字x与y完全相同，那么进程P在执行完操作α之后同样可以演变成进程P′。(www.xing528.com)

PAR规则表示若进程P在执行完操作α之后演变成进程P′，且α中的受限名不出现在进程Q的自由名中，则进程P|Q在执行完操作α之后可以演变成P′|Q。其中，条件bn（α）∩fn（Q）=Φ保证了该规则的正确性，若不满足该条件则进程P|Q就无法演变成P′|Q。

COM规则表示若进程P在执行完输出操作，即从通道x输出名字y之后演变成进程P′，且进程Q在执行完输入操作x（z），即在通道x接收名字z之后演变成进程Q′，则进程P|Q在执行完哑操作τ之后可以演变成P′|Q′{y/z}。

CLOSE规则表示若进程在执行完输出操作，即从通道x输出名字w之后演变成进程P′，且进程Q在执行完输入操作x（w），即在通道x接收名字w之后演变成进程Q′，则进程P|Q在执行完哑操作τ之后可以演变成（vw）（P′|Q′）。

RES规则表示若进程P在执行完操作α之后演变成进程P′，且y∉n（α），即名字y对α是新鲜的，则进程（vy）P在执行完操作α之后可以演变成进程（vy）P′。

OPEN规则表示若进程P在执行完输出操作，即从通道x输出名字y之后演变成进程P′，且y≠x，w也不出现在进程（vy）P′的自由名中，则进程（vy）P在执行完输出操作，即从通道x输出名字w之后可以演变成进程P′{w/y}。