论文部分内容阅读
尽管近年来模型检测取得了很大的进步，但是对于大系统的验证能力依然有限。在众多的状态减少和压缩技术中，抽象技术是最有效的方法之一。本文给出了基于K-模拟的抽象的高效算法，并证明了在线性时序逻辑框架下抽象的可靠性和完备性。
基于K-模拟的抽象
【摘 要】
：
尽管近年来模型检测取得了很大的进步，但是对于大系统的验证能力依然有限。在众多的状态减少和压缩技术中，抽象技术是最有效的方法之一。本文给出了基于K-模拟的抽象的高效算法
【机 构】
：
华中科技大学计算机科学与技术学院
【出 处】
：
计算机科学
【发表日期】
：
2007年9期
【基金项目】
：
本文工作得到国家自然科学基金（70271069）的支持.
其他文献
运用在线算法与竞争分析方法，研究了网络环境下当供应商在不同时刻到达，并投标而要求采购商接到每个投标时立即做出决策的在线反向拍卖机制。首先，证明了基于采购商需求曲线的在
通过定义Petri网变迁的指标函数，给出一种基于变迁指标的Petri网分解方法，通过分解得到子网系统均为结构简单的T-网。分析了原网系统与子系统在结构性质和动态性质方面的对应关
垃圾邮件的泛滥已经严重影响邮件的正常使用，由Yahoo和Cisco公司提出的DKIM反垃圾邮件技术，已经提交IETF，有望成为行业标准，能较好地解决垃圾邮件问题。文章分析了目前常用的反垃
从统计学角度推导了风险头寸和多种套期保值工具所组成资产组合的价格协方差矩阵逆矩阵的表达式，分析了该表达式的统计学特征。在此基础上，结合组合套期保值策略的基本模型，研究
视角变化往往会引起目标外观特征的变化,基于单一颜色直方图模型的均值漂移跟踪算法往往不能适应这种变化。本文在对连续自适应均值漂移算法深入分析的基础上,提出利用目标外观信息的先验知识,对其建立多个颜色分布模型。每帧跟踪结束后,算法都会根据当前的目标特征和周围环境从多个模型的凸组合中选出最有利于下一帧跟踪的参考模型。实验结果表明,该算法能很好地适应目标外观的变化,且计算代价不大。
本文分析了目前汉字处理应用中存在的主要问题,归纳出问题的核心是由于缺少能涵盖一切可能汉字的、可计算的字形形式化描述体系,从而造成应用中有一系列障碍。发现了现有字形描述方法共同存在的特征选取缺陷,最后给出了一种可行的汉字网格字形描述方法,该方法不仅能表示一切可能的汉字字形(包括错字),而且为字形特征异同的自动计算奠定了可靠的基础。