【摘 要】
：
精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同的形式化语言进行建模,如能证明两者间存在某种精化关系,且该关系能够维持性质,可得出系统实现满足性质规约
【机 构】
：
浙江工业大学计算机科学与技术学院,SchoolofComputerEngineering
【基金项目】
：
国家自然科学基金（61103044,U1509214）,浙江省自然科学基金（LQ15E050006,LY16F020035）
论文部分内容阅读
精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同的形式化语言进行建模,如能证明两者间存在某种精化关系,且该关系能够维持性质,可得出系统实现满足性质规约.为验证不同类型的系统性质,traces,stable failures和failures-divergence精化检测方法已被提出.精化检测算法依赖于子集构造,因而其面临状态空间爆炸问题.近年来,已有学者针对NFA语言包含问题提出了基于模拟关系的状态空间消减方法,极大地提高了算法的性能,且该方法能够直接用于traces精化检测.在此基础上,提
其他文献
由于肺癌发病隐匿．临床症状并不典型．许多肺癌病人确诊时已是晚期．失去了手术机会。影响肺癌早期诊断的因素多由于误诊．文献报道肺癌误诊为肺结核者最多．尤其是肺癌呈浸润性生长时
技校英语教学要注重文化背景知识的介绍,将语言教学与文化背景知识的教学有机地结合起来,培养学生使用语言的能力.
应对与人的心理健康一直具有十分密切的关系,多年来也一直是西方应用心理学研究的热点问题。在面对压力时,作为一个重要的影响变量,人格必然影响人们的应对方式与心理健康的
SIMD扩展部件是近年来集成到通用处理器中的加速部件，旨在发掘多媒体和科学计算等程序的数据级并行．控制依赖给发掘程序中的数据级并行带来了阻碍，当前，无论基于loop-based还是SL
非刚性点集配准是当前多个领域中的一项重要研究问题.现今流行的配准算法通常使用基于单一特征的对应关系评估与包含单一约束条件的空间变换更新,而单特征与单约束限制了其配准效果与应用领域.提出了一种基于双特征高斯混合模型和双约束空间变换的非刚性点集配准算法.首先定义了双特征描述子,并用全局特征和局部特征构建它;随后,基于此描述子将高斯混合模型改进为双特征高斯混合模型.定义了局部结构约束项,并与全局结构约束
课程改革对职业技术教育教师的素质提出了更高的要求。本文针对中职学生现状，主张结合学生实际施教，既要调动学生学习的积极性，又要将各种能力的培养贯穿于课堂教学中。