STGA的变种及其互模拟验证

摘要：

为刻画和验证无穷值域上的传值进程, Hennessy和Lin先后提出符号迁移图(STG)和带赋值符号迁移图(STGA)作为传值进程的语义表示模型,并给出了相应的强互模拟算法.为将该方法推广至实际应用中更常用的弱互模拟等价和观察同余的验证问题, 该文首先引入了STGA的一个变种,它与原模型的不同之处在于将符号迁移上赋值和符号动作的执行次序颠倒,因而可定义此种STGA结点间的符号双迁移关系.文中提出了从正则传值进程生成此类STGA的全部产生规则,并基于Lin的迟强互模拟算法给出了针对此类STGA的早强互模拟算法.然后利用符号双迁移关系引入了带赋值的早符号观察图(ESOGA)和早符号同余图(ESCGA),将上述算法推广至早弱互模拟等价和早观察同余的情况.但符号迁移上赋值的出现有可能导致ESOGA和ESCGA为无穷图,从而使本文所给的弱互模拟算法在适用范围和效率上受到一定的局限.最后, 作为一种可应用的情况, 进一步考虑了符号迁移图的弱互模拟等价和观察同余验证问题.此时由符号双迁移关系生成的符号观察图和迟符号同余图必为有穷图, 因而我们的弱互模拟等价算法是可行的.与此同时,文中还给出并证明了符号迁移图上的τ-循环和τ-边消去定理, 在应用任何弱互模拟和观察同余验证算法之前,均可利用这些定理对所给符号迁移图进行化简以提高算法的执行效率.

关键词：传值进程、符号迁移图、带赋值符号迁移图、互模拟、谓词等式系

所属期刊栏目：23

分类号：TP301(计算技术、计算机技术)

资助基金：新材料领域项目863-306-ZT05-06-1;中国科学院资助项目69873045

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共11页

页码：345-355