中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
学科主题: 计算机科学技术基础学科::计算机科学技术基础学科其他学科
题名:
模态逻辑公式为见证的互模拟等价判定
作者: 李明
答辩日期: 2009-05-20
导师: 柳欣欣
授予单位: 中国科学院研究生院
授予地点: 中国科学院软件研究所
学位: 硕士
关键词: 形式化验证 ; 有限状态进程 ; 强互模拟 ; 分支互模拟 ; 诊断公式
摘要: 判定两个进程是否具有某种等价关系,是形式化验证的重要组成部分,很多种等价关系被定义出来以满足不同的验证需求,强互模拟等价和分支互模拟等价是其中两个重要的两种等价关系。强互模拟等价可以用HML(Hennessy-Milner Logic)逻辑刻画,分支互模 拟等价可以用HMLU(HML with Until)等逻辑刻画。两个模型不能强互模拟等价或者分支互模拟等价时,存在一个作为见证的相应逻辑描述的公式,该公式只能被其中一个模型满足,称之为诊断公式。诊断公式的意义在于有助于分析理解模型为什么不具有相应的等价关系,给出诊断公式是对判定算法有意义的扩充。修改后的PT(Paige-Tarjan)算法可以用于计算有限状态进程之间的强互模 拟等价关系,修改后的GV(Groote-Vaandrager)算法可以用于计算分支互模拟,对它们相应的扩充可以为不能强互模拟等价或分支互模拟等价的进程生成诊断公式。 主要工作如下:分析为强互模拟等价和分支互模拟等价生成诊断公式的方法。设计处理有限状态进程表达式并将其转化为标号迁移系统的算法。扩展PT 算法,使其适用于标号迁移系统,并在判定强互模拟等价的过程中为不能强互模拟的进程生成HML 描述的诊断公式。扩展GV 算法,使其能够在判定标号迁移系统上分支互模拟的同时,为不能分支互模拟的进程生成HMLU 描述的诊断公式。
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/109
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
200628015029010_paper.pdf(489KB)----限制开放 联系获取全文

Recommended Citation:
李明. 模态逻辑公式为见证的互模拟等价判定[D]. 中国科学院软件研究所. 中国科学院研究生院. 2009-05-20.
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