论文部分内容阅读
标记算法是模型检测用于验证计算树逻辑CTL公式的经典算法。针对标记算法检测大规模公式存在的效率问题，提出一种可用于验证大规模CTL公式的标记算法。算法通过公式预处理标识公式集中的公共子公式，在验证过程中绑定公共子公式与模型状态，避免公式的重复验证。实验结果表明，该算法有效提高了验证效率。
一种改进的大规模CTL公式检测算法
【摘 要】
：
标记算法是模型检测用于验证计算树逻辑CTL公式的经典算法。针对标记算法检测大规模公式存在的效率问题，提出一种可用于验证大规模CTL公式的标记算法。算法通过公式预处理标识
【机 构】
：
国家数字交换系统工程技术研究中心
【出 处】
：
计算机科学
【发表日期】
：
2013年10期
【基金项目】
：
国家863计划（2012AA012902）资助.
其他文献
本文从国际时尚功能家纺流行趋向,探索我国时尚功能家纺创新的新途径,综析了我国餐厨用、毛巾制品、儿童用三大时尚功能家纺时代特征,为发展时尚功能家纺传递了信息。
李克强总理在今年3月5日“两会”上的政府工作报告中提出，“打造更多享誉世界的“中国品牌”，推动中国经济发展进入质量时代。”“要引导企业增品种、提品质、创品牌”。在我国
本文根据有关纺织装饰专家对室内软装饰织物按用途的分类要求,对七大类软装饰织物的系列组合、功能性、实用性、安全性、舒适性、艺术性、可视性作了系统的介绍,家纺软装饰织
对涂自然等人提出的组合猜想上的构造方法及有关结论进行了改良推广,在假设更一般的组合猜想成立的前提下构造了一种具有最优代数免疫度的偶数元布尔函数f,同时还利用f构造了
为了保护用户的隐私,大部分公开数据集都采用隐藏真实ID和引入噪声信息的方法来进行匿名处理.这些匿名处理即使在异步参考信息的攻击下也是脆弱的：即使只有部分位置信息暴露给
直播流媒体系统能够为网络用户提供丰富的直播电视节目,是发展最快的网络应用之一。然而,普遍存在的启动时延大、播放不流畅等问题,严重制约直播流媒体系统服务质量的改善。
计算机支持的协同设计是缩短产品研制周期、提高产品质量和降低研制成本的有效手段之一。针对飞机研制过程中实时/非实时和同构/异构系统信息协作需求并存的特点,提出了一种
运动分割是计算机视觉领域研究的重要内容。提出一种基于均值偏移的自动运动分割算法。该方法首先用特征点匹配关系获得特征点的运动轨迹,并以轨迹的运动向量作为特征,再用均值偏移算法对轨迹的运动向量进行聚类。均值偏移缩小相似的运动向量之间的差别,同时扩大不同运动的运动向量之间的差距。为了自动获得运动分类数,还提出了一种基于非参数核密度的自动分类方法,该方法通过估计运动向量的密度分布,用核密度图自动确定运动分