中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
学科主题: 计算机科学技术基础学科
题名:
弱互模拟等价类算法改进
作者: 李伟松
答辩日期: 2009-06-02
导师: 张文辉
授予单位: 中国科学院研究生院
授予地点: 中国科学院软件研究所
学位: 硕士
摘要: 大量的硬件和软件系统广泛应用在一些重要的领域,在许多情况下错误和失效是不可接受的。需要提供方法来检验软硬件的正确性,增强我们对软硬件系统的信心。形式化验证提供了提高软硬件可靠性的方法。 互模拟等价类和弱互模拟等价类可以用来降低形式化验证中模型的规模。弱互模拟等价类有两种算法:一种是先计算迁移关系的自反传递闭包,然后调用互模拟等价类的算法。另一种是作为IGPTPartEF的一个特例,直接在原图上用划分精化的方法计算。针对这些计算弱互模拟等价类的算法,我们提出两种改进算法。 首先,我们观察到有些状态在划分精化的过程中不会被再次切分,可以事先将它们归类到一个组,在划分精化过程中以这些组为基本单位进行切分,可以在很大程度上减小算法花费的时间。我们用该思想给设计出了改进算法一。 然后,我们观察在Paige-Tarjan算法中引入了“处理比较小的一半”的思想来改进计算互模拟等价类的算法,它使得计算互模拟等价类的算法的时间复杂度从O(mn)(其中m是边数,n是顶点数)改进到O(mlgn),而在前面所述的弱互模拟等价类算法中并没有引入“处理比较小的一半”。我们引入这一思想,设计出了改进算法二。 之后,我们设计实现了原型工具,并进行了数据实验来证实算法在时间上与原算法相比有明显改进。
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/104
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
弱互模拟等价类算法改进.pdf(515KB)----限制开放 联系获取全文

Recommended Citation:
李伟松. 弱互模拟等价类算法改进[D]. 中国科学院软件研究所. 中国科学院研究生院. 2009-06-02.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[李伟松]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[李伟松]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace