计算机学报
計算機學報
계산궤학보
CHINESE JOURNAL OF COMPUTERS
2000年
4期
345-355
,共11页
李舟军%陈火旺%钟广军%王兵山
李舟軍%陳火旺%鐘廣軍%王兵山
리주군%진화왕%종엄군%왕병산
传值进程%符号迁移图%带赋值符号迁移图%互模拟%谓词等式系
傳值進程%符號遷移圖%帶賦值符號遷移圖%互模擬%謂詞等式繫
전치진정%부호천이도%대부치부호천이도%호모의%위사등식계
为刻画和验证无穷值域上的传值进程, 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為無窮圖,從而使本文所給的弱互模擬算法在適用範圍和效率上受到一定的跼限.最後, 作為一種可應用的情況, 進一步攷慮瞭符號遷移圖的弱互模擬等價和觀察同餘驗證問題.此時由符號雙遷移關繫生成的符號觀察圖和遲符號同餘圖必為有窮圖, 因而我們的弱互模擬等價算法是可行的.與此同時,文中還給齣併證明瞭符號遷移圖上的τ-循環和τ-邊消去定理, 在應用任何弱互模擬和觀察同餘驗證算法之前,均可利用這些定理對所給符號遷移圖進行化簡以提高算法的執行效率.
위각화화험증무궁치역상적전치진정, Hennessy화Lin선후제출부호천이도(STG)화대부치부호천이도(STGA)작위전치진정적어의표시모형,병급출료상응적강호모의산법.위장해방법추엄지실제응용중경상용적약호모의등개화관찰동여적험증문제, 해문수선인입료STGA적일개변충,타여원모형적불동지처재우장부호천이상부치화부호동작적집행차서전도,인이가정의차충STGA결점간적부호쌍천이관계.문중제출료종정칙전치진정생성차류STGA적전부산생규칙,병기우Lin적지강호모의산법급출료침대차류STGA적조강호모의산법.연후이용부호쌍천이관계인입료대부치적조부호관찰도(ESOGA)화조부호동여도(ESCGA),장상술산법추엄지조약호모의등개화조관찰동여적정황.단부호천이상부치적출현유가능도치ESOGA화ESCGA위무궁도,종이사본문소급적약호모의산법재괄용범위화효솔상수도일정적국한.최후, 작위일충가응용적정황, 진일보고필료부호천이도적약호모의등개화관찰동여험증문제.차시유부호쌍천이관계생성적부호관찰도화지부호동여도필위유궁도, 인이아문적약호모의등개산법시가행적.여차동시,문중환급출병증명료부호천이도상적τ-순배화τ-변소거정리, 재응용임하약호모의화관찰동여험증산법지전,균가이용저사정리대소급부호천이도진행화간이제고산법적집행효솔.