STGA的变种及其互模拟验证

A Variant of STGA and Its Bisimulation Checking

为刻画和验证无穷值域上的传值进程，Ｈｅｎｎｅｓｓｙ和Ｌｉｎ先后提出符号迁移图（ＳＴＧ）和带赋值符号迁移图（ＳＴＧＡ）作为传值进程的语义表示模型，并给出了相应的强互模拟算法．为将该方法推广至实际应用中更常用的弱互模拟等价和观察同余的验证问题，该文首先引入了ＳＴＧＡ的一个变种，它与原模型的不同之处在于将符号迁移上赋值和符号动作的执行次序颠倒，因而可定义此种ＳＴＧＡ结点间的符号双迁移关系．文中提出了从正则传值进程生成此类ＳＴＧＡ的全部产生规则，并基于Ｌｉｎ的迟强互模拟算法给出了针对此类ＳＴＧＡ的早强互模拟算法．然后利用符号双迁移关系引入了带赋值的早符号观察图（ＥＳＯＧＡ）和早符号同余图（ＥＳＣＧＡ），将上述算法推广至早弱互模拟等价和早观察同余的情况．但符号迁移上赋值的出现有可能导致ＥＳＯＧＡ和ＥＳＣＧＡ为无穷图，从而使本文所给的弱互模拟算法在适用范围和效率上受到一定的局限．最后，作为一种可应用的情况，进一步考虑了符号迁移图的弱互模拟等价和观察同余验证问题．此时由符号双迁移关系生成的符号观察图和迟符号同余图必为有穷图，因而我们的弱互模拟等价算法是可行的．与此同时，文中还给出并证明了符号迁移图上的τ－循环和τ－边消去?

In order to check bisimulation for value--passing processes with infinite data domain, the symbolic transition graph (STG) and the symbolic transition graph with assignment (STGA) are introduced by Hennessy and Lin as semantic models of value-passing processes, and strong bisimulation algorithms based on such graphs are also proposed. To generalize the approach to dealing with weak bisimulation and observation congruence,this paper first introduces a variant of STGA. The distinction of proposed model is that the assignment of a transition is performed after rather than before the action and thus the symbolic double transition relations over nodes can be defined. The rules which generate such graphs from regular value--passing processes are presented. Based on the late strong bisimulation algorithm of Lin,an early strong bisimulation algorithm is given. By using symbolic double transitions,the variant STGA can be generalized to the early symbolic observation graph with assignment (ESOGA) and the early symbolic congruence graph with assignment (ESCGA) to check early weak bisimulation and early observation congruence,respectively. However, since the occurrence of assignments over transitions,the generalized ESOGA and ESCGA may be infinite, thus the application scope of the weak bisimulation algorithm is limited. Finally this paper consideres an applicable case--the symbolic transition graph,then the gener allied symbolic observation graph (SOG) and symbolic congruence graph (SCG) can be finite,so authors' algorithm is feasible for weak bisimulation and observation congruence. Moreover, two theorems ensuring the elimination of τ-cycle and τ-edge are proved,and therefore STGs can be simplified significantly once the weak bisimulation or observation congruence is to be checked.