关于π演算的基本概念,在文献[3]中已有详细介绍在此不再赘述。在给出π演算中递归表达式基本形式之前,先看一个例子:

(1)

式(1)中每个通道 a、 b、 c、…中都保存着一个数值 h'(这个数值可以不一样),从已知通道 a开始,读取通道内当前值 h'加到现有的值上,直到得到的 h值大于10时可以选择执行输出该值。这样,从 a开始到输出 h时所有计算过的通道即是该get函数的路径。

在式(1)中,既有自调用的算子,又有非自调用的算子,并且有选择运算符“+”将两个进程相连。在不满足递归出口条件时,多次执行前缀算子 ab获取下一个通道,并执行计算 h值操作。当满足递归出口条件时,可以选择继续自调用,也可以终止调用过程。

本文给出了一种一般π演算的递归表达式的基本形式:

(2)

式中: 均为非自调用的表达式。可以看出,式(1)符合该表达式形式。

当然,在一些表达式中也会出现有多个自调用表达式的形式,比如:

(3)

(4)

(5)

在式(3)至式(5)中,均有两次自调用,虽然在转换时与式(2)有点不同,但基本转换思路大致相同。为了方便描述转换过程,在本文中,以式(2)这种递归形式为例。

为了更好地记录递归运算的层次,本文引入轨迹的概念。通常,轨迹一般用来指进程P所依次执行的一系列活动,一般用表示。

定义1 轨迹:π演算递归结构执行时,为了记录递归运算的层次,我们将递归调用的顺序称为轨迹,用字母trail表示。调用一次用 σ₁ 表示,调用第二次用 σ₂ 表示,以此类推,调用第 n次用 σ _n 表示,则进程中递归结构执行的轨迹trail=< σ₁, σ₂,…, σ_n>。

定义2 逆轨迹:与轨迹相应地,在递归返回时其轨迹称为逆轨迹,记为trail^-1,上述递归返回的逆轨迹即为trail^-1=< σ _n, σ _n-1,…, σ₁>。

在本文中,π演算进程P转换而成的Petri网记为 N_P, N _P是一个有向连通图,其节点分别称为库所和变迁。这些节点通过有向弧相连。相同类型的两个节点之间是不允许相连的。

递归π演算向Petri网转换要遵循一些转换规则,在本文中将这些规则概括为两类:基本进程的转换规则以及组合规则。

1.2.1 基本进程转换规则

对于向子网 K( ρ)的转换,是根据表达式 的语法树,其组成为给定基本子项(进程项0,进程调用,内部动作以及输入输出前缀)的图转换。

由于不涉及任何的名字操作,因此进步进程项0和内部动作前缀 τ十分简单。进程调用 X( α₁,…, α _nX)也类似,但是结果将产生一个层次变迁,它将通过标识等价规则进行激发变换^{[ 10]}。

每个输出前缀 β(其中 α≠ β),将会被转换成未标识的Petri网的形式 ,其中 t _k表示已知输出变迁, t _n表示新的输出变迁, t _c表示交互输出变迁。

具体的转换规则如图1所示。

图1

Fig.1

	Figure Option ViewDownloadNew Window
	图1 空进程、哑动作 τ、进程调用、动作前缀向Petri网转换规则Fig.1 Translation rules from o, τ,the process call and the prefix to Petri nets

1.2.2 组合规则

本节中的组合规则用于合并Petri网的算子,包括前缀组合规则、选择组合规则、并行组合规则以及范围处理规则,其中前3个规则给出了合并标签库所、相应的持有者的方法^{[ 12]}。

假设有网 是两个不相干的未标记的Petri网,并且有 如果 那么 D₁= D₂,即被相同符号标识的持有者库所也有同样的值类型集合。下面将给出四种组合规则的形式化处理方法,如图2所示。

图2

Fig.2

	Figure Option ViewDownloadNew Window
	图2 组合规则Fig.2 Composition rules

前缀组合规则: N₁. N₂ 。假设 N₁有唯一的入口控制库所和唯一的出口控制库所(出口控制库所记作 s₁),通过如下步骤获得组合结果:

(1)网 N₁和网 N₂并排放置。

(2)对应每个 创建一个新的库所 s'₂,用符号 i标识,同时将网 N₁和网 N₂中在 s_i和 t∈ T_i ( i∈{1,2})的弧 Ψ在新的库所 s'₂和 t上标记,并使用同样的注释符号和同样的弧类型(无向或是有向的)标记,而后网 N₁的唯一出口控制库所和网 N₂的出口控制库所将被删除。

(3)对于有相同标识符号和类型的持有者库所将被合并为一个持有者库所,并且如前一样,具有相同的标识符号和类型,在原来的网 N₁和网 N₂中连接合并的持有者库所与变迁之间的弧及注释标识在合并后的持有者库所中保持不变。

1)选择组合规则: N₁+ N₂,可通过如下过程获得图转换结果:

①网 N₁和网 N₂并排放置。

对于每个 和 创建一个新的库所 s,用符号e标识,并且使得每个在 s _i和t∈ T _i, i∈{1,2}的弧 Ψ在新的库所 s和变迁 t上作同样标识,即使用相同的注释符号和相同的弧类型(无向或是有向的);类似地,对于每个 和 创建一个新的库所 s ,用符号 x标识,其连接性与上面规则定义一致。最后,将原来在网 N₁和网 N₂中标识的入口控制库所(被符号 e标识)和出口控制库所(被符号 x标识)删除。

②具有相同名字的持有者库所的合并可参见前缀组合规则。

2)并行组合规则: N₁| N₂,可通过如下过程获得图转换结果:

①网 N₁和网 N₂并排放置;

②具有相同名字的持有者库所的合并可参见前缀组合规则。

3)范围处理规则: N= sco( N₁),可通过如下过程获得图转换结果:

①对于每对变迁 t₁, t₂∈ T₁,其中 t₁和 t₂分别被snd或rcv所标识,创建一个新的变迁 t,用符号 τ标识,而在变迁 t与库所 s上的弧注释符号是在变迁 t₁与库所 s以及变迁 t₂与库所 s的弧注释符号的简单合并。在这里注意在snd所标识的变迁周围的弧与rcv所标识的变迁周围的弧是互不相干的,所以不需要进行反复的合并操作。

②最后删除被snd和rcv所标识的变迁以及与其相连接的弧。

类似于式(1)中的例子,当数据 h满足 h>10时才可以选择执行 ,因此在执行递归时要判断是否满足递归出口的条件。因此在递归调用和递归返回间加入一个判定库所,用来存储判定是否满足递归出口条件的判定托肯。判定托肯的形式为F.D或者T.D,其中F.D表示不满足递归出口条件,D表示这个托肯的类型是判定托肯(decision token);T.D表示满足递归出口条件。

对于如何记录当前数据属于哪次递归操作,本文采用trail.data.place的形式,即当前轨迹.数据值.所在库所的形式存储在栈库所中。

对于轨迹,在执行递归调用时,调用一次用 σ₁ 标记,调用第二次用 σ₂ 标记,…,调用第 n次用 σ _n 表示,进程中递归结构执行的轨迹trail=< σ₁, σ₂,…, σ _n >。例如递归主体 X( a₁,…, a_n)将用轨迹标记为 σ₁, σ₂,…, σ _n. X( a₁,…, a_n)。对于递归主体后面的 ,在递归返回之前是不执行的,在执行 时是按照轨迹< σ₁, σ₂,…, σ _n >的逆轨迹< σ _n, σ _{n -1},…, σ₁>执行的。

对于π演算递归结构向Petri网的转换,本文采用层次化方法,即将表达式中的每一个子表达式(包括递归主体)都先转换成对应的子网,然后组合起来;如果自调用表达式没有满足递归出口条件,那么对自调用表达式的网结构进行进一步细化,将下一次调用的网结构展开代替上一层中自调用表达式对应的网结构。

下面给出关于式(2)的递归结构全景图第一层,如图3所示。

说明:

(1)最开始的库所 与最后的库所 是此π演算表达式对应网结构的控制库所,这是假设该表达式是一个主式;如果此递归π演算表达式是其他π演算表达式的子式,这两个库所应换成与外界相连、用于传递控制信号的内部库所 i。

图3

Fig.3

	Figure Option ViewDownloadNew Window
	图3 典型π演算递归结构转换结果全景图第一层Fig.3 First layer of franslation panoramic view from typical recursion π calculus to Petri net

(2)图中的库所 是本文新加库所——判定库所,存储了判定是否满足递归出口条件的判定托肯F.D和T.D。

(3)在自调用表达式对应的网结构与判定库所 d之间有一条弧相连,表示在执行自调用表达式时,其中的条件发生了变化,这个变化的条件要及时传给判定库所,使判定库所做出合理的判断。

(4)在 等表达式前进行了轨迹的标记;而表达式 R( b₁,…, b _n)却没有轨迹标记,因为在递归调用时此表达式只执行一次。

(5)判定库所对应一个判断逻辑,严格来讲,如果系统中有多个递归表达式,则每一个表达式单独对应一个判定库所。

(6)出于版面考虑,这里没有画出栈库所、名字持有者库所、标签库所以及相关弧。

式(2)递归结构全景的第二层如图4所示。

图4

Fig.4

	Figure Option ViewDownloadNew Window
	图4 典型π演算递归结构转换结果全景图第二层Fig.4 Second layer of translation panoramic view from typical recursion π calculus to Petri net

类似地,调用多次的π演算表达式对应的网结构也能够给出。

对于形如式(2)的π演算表达式,采用层次化方法,将π演算递归结构转换成Petri网的步骤为:

(1)按照1.2节中的基本进程转换规则及组合规则将 以及 分别转换成对应的子网 N_P1 、 N_P2 、 N_P3 。

(2)将自调用表达式 X(a'₁,…,a'_n)先看做一个整体表示,对应的网结构先用 N_P0 表示。各个组成部分用构造sco( N_P1 | N_P2 | N_P3 | N_P0)网连接起来,这将多种标签库所和可能来自不同部分的有 uv和 标记的变迁对合并起来。这个构造并不合并其他的持有者库所。移除所有标记为 uv和 的变迁。

(3)判断 是否满足递归出口条件,若不满足,将 视为 转步骤(1)。用不同的标记来记录不同的调用;若满足,转(4)。

(4)将图3中的变迁 P( a₁,…, a _n)用子网 N_P1 替换,如果 N_P1 只有一个输入库所 e,那么将此库所与开始的库所 e合并,仍旧记为 e;否则创建一个辅助变迁 t₁,使开始库所 e指向辅助变迁 t₁,然后由变迁 t₁ 指向 N_P1 所有的输入库所 e,再将 N_P1 所有的输入库所 e改为内部库所 i。

同样地,如果 N_P1 只有一个输出库所 x,将此库所与最后库所 x合并,记为 x;否则创建一个辅助变迁 t₂,使 N_P1 所有的输出库所 x指向辅助变迁 t₂,然后由变迁 t₂ 指向最后的库所 x,再将 N_P1 所有的输出库所 x改为内部库所 i。

在用 N_P2 、 N_P3 替换 R( b₁,…, b _n)、 Q( a″₁,…, a″_n)时也做同样的处理。

(5)将相同的名字持有者库所合并,与原库所相连的弧以原方式练到合并后的库所上。将需要保存数据的变迁用弧与栈库所相连。

(6)为了得到完整的变迁网 N _p,向输入库所中插入一个小黑点作为托肯,并把下面的通道插入到持有者库所中去:

①把 ζ( α)插入到每个 α标记的持有者库所中,其中 α∈ domain( ζ);

②把 a. a. K插入到标签库所中,其中对于每一个 α∈ known( ζ);

③把 n. N插入到标签库所中,其中 n∈ C\ konwn( ζ);

④把 Δ. R插入到标签库所中,其中 Δ∈ rstr( ζ)。

本文定义了从递归π演算到Petri网的语义转换,从而产生了有限结构转换网—— N _P,它是具有有限库所、变迁和弧的网结构,该递归结构的标号迁移系统 Its_P与转换后的Petri网所对应的标号迁移系统It 是强互模拟。

定理1 N _p是具有有限库所、变迁和弧的Petri网图,并且使得Its_P和It 是互为强互模拟的标号迁移系统。

证明 基本π演算部分的Petri网语义等价证明在文献^{[ 12]}中详细介绍了转换的思想、方法以及相关的语义等价证明,在此不再赘述。

关于递归结构的Petri网语义等价的证明采用数学归纳法。具体如下:

设 K为递归结构执行次数,即递归层数。

(1)当 K=1时,按照文中所述递归π演算向Petri网的转换方法,其直接转换为不带递归结构的基本π演算,其互模拟等价性是已知的。

(2)假设当 K= n时,从递归π演算向Petri网的转换具有互模拟等价性,那么证明当 K= n+1时互模拟等价仍成立。由于当 K= n时,前 n层的递归调用已经实现,即可以将前 n层递归调用得到的π演算表达式看做一个复杂无递归的基本π演算表达式,这样再加上第 n+1层的递归调用转化为(1)中的形式,此时 K'=1,符合(1)中所证互模拟等价。因此当 K= n+1时递归π演算向Petri网转化的互模拟等价性成立。证毕。

分析如式(2)形式的π演算的递归结构,如果该π演算表达式不满足递归出口条件,那么会循环执行自调用表达式之前的子表达式 P( a₁,…, a _n),执行过程大致如图5所示。

图5

Fig.5

	Figure Option ViewDownloadNew Window
	图5 π演算表达式递归结构执行图Fig.5 Execution of π calculus expression recursive structure

如果π演算表达式的递归结构执行多次,那么会产生巨大的Petri网,因此本文考虑将其进行简化,得到一种更简洁的Petri网表示。受图3启发,本文将典型π演算递归结构转换结果用全景图表示,如图6所示。

图6

Fig.6

	Figure Option ViewDownloadNew Window
	图6 一种更简洁的Petri网表示Fig.6 A more compact representation of Petri net

这里需要考虑以下几个问题:

对于递归出口之前每次执行的表达式 P(a₁,…, a _n),其每次具体执行是不一样的,我们在其前面用轨迹标记,表示按照轨迹 σ₁, σ₂,…, σ_n 执行,这里的轨迹是根据判定库所的变化一步一步生成的。然后在执行递归返回时, Q(a″₁,…,a″_n)按照轨迹 σ₁, σ₂,…, σ_n 的逆轨迹 σ_n, σ_n-1,…, σ₁执行。

经过判断,只有执行P(a₁,…,a_n)时,判定条件发生的改变,那么需要将与自调用表达式对应的网结构相连的弧改为表达式P(a₁,…,a_n)对应的网结构与判定库所相连。

本文给出了 N _p 的一种更简洁Petri网表示,记为 N _c,它是具有有限库所、变迁和弧的网结构,保留了系统的语义,编码完全相同的轨迹集合。

定理2 N _c是具有有限库所、变迁和弧的Petri网图,并且使得 N _p和 N _c编码完全相同的轨迹集合(激发顺序)。

证明 针对递归结构,分别从递归调用、递归出口及递归返回三部分考虑其执行的轨迹集合。

(1)对每次递归调用执行的表达式 P( a₁,…, a _n), N _p 和 N _c 的执行轨迹均为{ σ₁, σ₂,…, σ_n}。

(2)对递归出口执行的表达式 R( b₁,…, b _n),由于只执行一次,因此其轨迹集合可以忽略。

(3)对递归返回表达式 Q( a″₁,…, a″ _n), N _p 和 N _c 的轨迹集合均为{ σ_n, σ_n-1,…, σ₁}。证毕。