CAJ | 학술논문

为刻画和验证无穷值域上的传值进程, Hennessy和Lin先后提出符号迁移图(STG)和带赋值符号迁移图(STGA)作为传值进程的语义表示模型,并给出了相应的强互模拟算法.为将该方法推广至实际应用中更常用的弱互模拟等价和观察同余的验证问题, 该文首先引入了STGA的一个变种,它与原模型的不同之处在于将符号迁移上赋值和符号动作的执行次序颠倒,因而可定义此种STGA结点间的符号双迁移关系.文中提出了从正则传值进程生成此类STGA的全部产生规则,并基于Lin的迟强互模拟算法给出了针对此类STGA的早强互模拟算法.然后利用符号双迁移关系引入了带赋值的早符号观察图(ESOGA)和早符号同余图(ESCGA),将上述算法推广至早弱互模拟等价和早观察同余的情况.但符号迁移上赋值的出现有可能导致ESOGA和ESCGA为无穷图,从而使本文所给的弱互模拟算法在适用范围和效率上受到一定的局限.最后, 作为一种可应用的情况, 进一步考虑了符号迁移图的弱互模拟等价和观察同余验证问题.此时由符号双迁移关系生成的符号观察图和迟符号同余图必为有穷图, 因而我们的弱互模拟等价算法是可行的.与此同时,文中还给出并证明了符号迁移图上的τ-循环和τ-边消去定理, 在应用任何弱互模拟和观察同余验证算法之前,均可利用这些定理对所给符号迁移图进行化简以提高算法的执行效率.
위각화화험증무궁치역상적전치진정, Hennessy화Lin선후제출부호천이도(STG)화대부치부호천이도(STGA)작위전치진정적어의표시모형,병급출료상응적강호모의산법.위장해방법추엄지실제응용중경상용적약호모의등개화관찰동여적험증문제, 해문수선인입료STGA적일개변충,타여원모형적불동지처재우장부호천이상부치화부호동작적집행차서전도,인이가정의차충STGA결점간적부호쌍천이관계.문중제출료종정칙전치진정생성차류STGA적전부산생규칙,병기우Lin적지강호모의산법급출료침대차류STGA적조강호모의산법.연후이용부호쌍천이관계인입료대부치적조부호관찰도(ESOGA)화조부호동여도(ESCGA),장상술산법추엄지조약호모의등개화조관찰동여적정황.단부호천이상부치적출현유가능도치ESOGA화ESCGA위무궁도,종이사본문소급적약호모의산법재괄용범위화효솔상수도일정적국한.최후, 작위일충가응용적정황, 진일보고필료부호천이도적약호모의등개화관찰동여험증문제.차시유부호쌍천이관계생성적부호관찰도화지부호동여도필위유궁도, 인이아문적약호모의등개산법시가행적.여차동시,문중환급출병증명료부호천이도상적τ-순배화τ-변소거정리, 재응용임하약호모의화관찰동여험증산법지전,균가이용저사정리대소급부호천이도진행화간이제고산법적집행효솔.