基于符号迁移图的互模拟验证算法

Bisimulation Checking Algorithms Based on Symbolic Transition Graphs

符号迁移图是传值进程的一种直观而简洁的语义表示模型。该模型由Hennessy和Lin首先提出 ,随后又被Lin推广至带赋值的符号迁移图。本文不但定义了符号迁移图各种版本 (基 /符号 )的强操作语义和强互模拟 ,提出了相应的强互模拟算法 ,而且通过引入符号观察图和符号同余图 ,给出了其弱互模拟等价和观察同余的验证算法 ,给出并证明了τ 循环和τ 边消去定理 ,在应用任何弱互模拟和观察同余验证算法之前 ,均可利用这些定理对所给符号迁移图进行化简。

A symbolic transition graph is an intuitive and concise semantic model for value passing processes It is firstly introduced by Hennessy and Lin,and then generalized by Lin to symbolic transition graph with assignment This paper not only defines various versions of strong operational semantics and strong bisimulation for symbolic transition graphs,and proposes strong bisimulation algorithms for them,but also presents corresponding checking algorithms for weak bisimulations and observation congruence by means of symbolic observation graphs and symbolic congruence graphs Theorems ensuring the elimination of τ cycles and τ edges are given and proved,and therefore symbolic transition graphs can be simplified significantly once weak bisimulation and observation congruence are to be checked