Page 165 - 《软件学报》2021年第5期

朱锐 等:基于完全有限前缀展开的行为等价过程树生成算法 1389

(2) 不存在σ使得σ∈࣪(t)∧σ∉࣪(p).
其中,σ表示过程模型 p 或者过程树 t 的一个行为.p 和 t 行为等价从本质上而言就是过程模型 p 中所有出
现的行为一定会在过程树 t 中出现,反之亦然.TEPM 包含所有的 BSPM 模型和一部分具有复杂结构的模型,这
两部分模型都有对应的行为等价过程树,换而言之,有对应行为等价过程树的过程模型就是 TEPM.
2.2 完全前缀展开

对静态过程模型的分析,传统的方法主要使用可达树或者可达图的方法,这种方法面临的主要问题是“状态
空间爆炸”.为避免该问题,1996 年 Esparza 提出了完全前缀展开技术,该技术通过过程模型的完全前缀展开,可
以将过程模型展开为一个包含截断事件的分支进程 Π=(o,h),其中,o=(S,T;F′)是一个出现网,h 是一个映射函数,
例如针对一个过程模型 p=(C,A;F,M 0 )利用分支进程的可能扩展集,不断的扩展其对应的分支进程,直到扩展到
截断条件时停止,最后得到一个包含截断事件的分支进程.
下面对完全前缀展开技术中一些基本概念进行说明,更多相关介绍详见文献[25].
定义 8(出现网). 一个三元组 o=(S,T;F′)作为一个出现网,其中,
(1) (S,T;F′)是一个无环的网,S∪T≠∅;S 是一个库所(即条件)的有限集,∀s∈S 称作一个库所;T 是一个变迁(即
事件)的有限集,∀t∈T 称作一个变迁;F 是出现网的边集,且 F⊆S×T∪T×S.
(2) ∀s∈S,满足|·s|≤1,即任意库所的输入都小于等于 1.
(3) ∀x∈S∪T,满足¬x#x,即任意元素都不能自冲突.
(4) ∀x∈S∪T,满足{∀y∈S∪T|y<x}是有限的.
在出现网中对于∀x,y∈S∪T,x#y 表示 x 与 y 之间存在冲突关系,即在出现网中存在某公共库所 c,从 c 到 x 的
路径与从 c 到 y 的路径不相交.x<y 表示 x 与 y 之间存在因果关系,即在出现网中存在一条从 x 到 y 的路径.x co y
表示 x 与 y 之间存在 co 关系,即 x,y 满足¬x<y∧¬y<x∧¬x#y.
定义 9(分支进程). 对于一个过程模型 p=(C,A;F,M 0 ),其分支进程是一个二元组 Π=(o,h),其中,o=(S,T;F′)是
一个出现网,h 是一个从(S,T;F′)到(C,A;F)的映射,其中,
(1) h(S)⊆C,h(T)⊆A,h(F′)⊆F.
(2) Min(o)与 M 0 是双射关系,Min(o)表示出现网 o 中根据适当偏序关系得到的最小元素集合.
(3) ∀t 1 ,t 2 ∈T,且 t 1 ,t 2 满足·t 1 =·t 2 ∧h(t 1 )=h(t 2 ),则 t 1 =t 2 .
定义 10(分支进程的可能扩展集). 二元组Π=(o,h)是过程模型 p=(C,A;F,M 0 )的一个分支进程,其中,o=(S,
T;F′)是一个出现网,h 是一个映射.分支进程Π的可能扩展集是(t,B)对的集合,记为 PE(Π),其中,B 是Π中条件集 S
的 co 关系集(co-set),t 是过程模型 p 的一个变迁,其中,
(1) h(B)=·t,B 映射到过程模型 p 中是 t 的前集.
(2) h(e) =t 且·e=B,则 B 不包含 e.
定义 11(配置). 一个出现网 o=(P,T;G)的配置 C 是一组变迁的集合,其中,
(1) t∈C⇒∀t′<·t:t′∈C,即配置 C 是由适当偏序组成的闭包.
(2) ∀t,t′∈C:¬(t#t′),即配置 C 中的任意元素是无冲突的.
对于一个出现网 o=(P,T;G),∀t∈T,变迁 t 的本地配置也是一组包含 t 本身,并且是由适当偏序组成的无冲突
的变迁集合,记为[t],满足 t∈[t],且 t 1 ∈[t],t 1 满足[t 1 ]<·[t]∧任意 t 2 ∈C 有¬t 2 #t 1 .
定义 12(适当偏序关系). 一个出现网 o=(P,T;G)的上的适当偏序关系是本地配置之间的关系,用<·表示适当
偏序关系,其中,
(1)) <·是对⊂的改进,即∀t,t′∈T 有[t]⊂[t′],则[t]<·[t′].
(2) <·通过有限扩展得到保留,即∀t,t′∈T 有[t]<·[t′]和 Mark(t)=Mark(t′),则对于[t]的有穷扩展[t]⊕E,存在一个
同构变换 I,使[t]⊕E<·[t′]⊕I(E).
定义 13(割集). 一个出现网 o=(P,T;G)的有限配置 C,其割集 Cut(C),是一组只包含 co 关系的条件集,Cut(C)
被定义为 Cut(C)=(Min(o)∪C·)\·C.