【摘 要】
：
为刻画和验证无穷值域上的传值进程, Hennessy和Lin先后提出符号迁移图(STG)和带赋值符号迁移图(STGA)作为传值进程的语义表示模型,并给出了相应的强互模拟算法.为将该方法推
论文部分内容阅读
为刻画和验证无穷值域上的传值进程, Hennessy和Lin先后提出符号迁移图(STG)和带赋值符号迁移图(STGA)作为传值进程的语义表示模型,并给出了相应的强互模拟算法.为将该方法推广至实际应用中更常用的弱互模拟等价和观察同余的验证问题, 该文首先引入了STGA的一个变种,它与原模型的不同之处在于将符号迁移上赋值和符号动作的执行次序颠倒,因而可定义此种STGA结点间的符号双迁移关系.文中提出了从正则传值进程生成此类STGA的全部产生规则,并基于Lin的迟强互模拟算法给出了针对此类STGA的早强互模拟算法.然后利用符号双迁移关系引入了带赋值的早符号观察图(ESOGA)和早符号同余图(ESCGA),将上述算法推广至早弱互模拟等价和早观察同余的情况.但符号迁移上赋值的出现有可能导致ESOGA和ESCGA为无穷图,从而使本文所给的弱互模拟算法在适用范围和效率上受到一定的局限.最后, 作为一种可应用的情况, 进一步考虑了符号迁移图的弱互模拟等价和观察同余验证问题.此时由符号双迁移关系生成的符号观察图和迟符号同余图必为有穷图, 因而我们的弱互模拟等价算法是可行的.与此同时,文中还给出并证明了符号迁移图上的τ-循环和τ-边消去定理, 在应用任何弱互模拟和观察同余验证算法之前,均可利用这些定理对所给符号迁移图进行化简以提高算法的执行效率.
其他文献
目的 初步了解异常黑胆质成熟剂中含有的化学成分.方法 采用不同化学定性方法对异常黑胆质成熟剂中化学成分进行研究.结果 糖、皂苷、酚、黄酮、生物碱、香豆素(和/或内酯)、
目的 建立感冒清胶囊中脱水穿心莲内酯的测定方法. 方法 采用HPLC法测定感冒清胶囊中脱水穿心莲内酯的含量.KromasilC-18柱(250 mm×4.6 mm,5 μm),以甲醇-水(65:35)为流动相
目的 观察AF椎弓根系统对胸腰椎骨折的治疗作用.方法 回顾性分析43例胸腰椎骨折患者的临床资料,AF椎弓根系统内固定,行必要的椎管减压和植骨融合.结果 本组手术时间(1.9±0.7
目的研究三七总皂苷对HSC-T6细胞增殖的影响。方法将复苏后处于对数生长期的HSC-T6单细胞悬液稀释成浓度为2.0×105个/ml,并以0.1ml/孔接种,置于37℃、5%CO2培养箱内培养,24h
目的探讨二甲双胍对合并葡萄糖耐量异常(abnormality of glucose tolerance,AGT)的缺血性卒中患者预后的影响。方法从我院初诊的596例缺血性卒中中筛查出合并AGT者155例,随机
采用两种有机金属化合物为起始原料,用溶胶-凝胶法通过合理控制反应条件,制备出β-SiC凝胶粉体,然后在Ar气氛、900～1300℃下热处理,制备出了纯度非常高、颗粒尺寸在10nm左右的
针对开放式系统的安全性问题，对校园网信息系统内部安全管理机制中的身份认证策略、强制登录和 数据保密方法进行了研究和说明，在实际系统中这些安全机制进行了应用，达到了预期
利用软件度量工具度量程序源代码的各类质量属性是提高程序质量的一个重要方法.目前,面向对象语言已逐渐成为主流编程语言,度量基于对象技术的软件成为必然的需求.然而,由于
对连续时间非线性最优控制问题提出了基于双线性二次型问题的 DISOPE算法。在模型与实际存在差异的情况下 ,通过求解修正的基于双线性模型的优化问题和参数估计问题 ,给出了