中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
学科主题: 计算机科学技术基础学科::计算机科学技术基础学科其他学科
题名:
共代数中的互模拟证明方法及其应用
作者: 罗凌云
答辩日期: 2009-06-02
导师: 柳欣欣
授予单位: 中国科学院软件研究所
授予地点: 北京市中关村中国科学院软件研究所
学位: 硕士
关键词: 共代数
其他题名: Proof Methods for Bisimilarity in the Coalgebra Theory and Applications
摘要: 本论文主要研究共代数中的互模拟证明方法及其应用两个方面。 代数理论已被证实在计算机科学中具有广泛的应用,其对偶概念——共代数理论是近年来兴起的一个理论,它在描述无穷状态系统方面具有明显的优势。 因此,我们在本文中以共代数作为抽象的研究模型。 因为互模拟判定中的up-to方法能够非常有效地加速判定过程,我们首先将该方法从传统的集合论中 扩展到共代数理论。作为Sangiorgi的可靠函数的扩展,我们引入了一致函数。因此, 为了证明某个二元关系中的进程对都是互模拟等价的,只要证明该关系前进到其在某个一致函数作用下得到的新关系中即可。 另外,我们给出了span-互模拟和ref-互模拟之间的等价转换关系,并且,利用该结果证明了共代数中原有的up-to方法 都能被一致函数所覆盖。 一致函数是为单个函子$F$定义的。但是,当$F$是某种类型的多项式函子时,有可能存在一些 函数,它们与$F$的某些子函子一致却不与整个$F$一致。因此,我们将一致函数进一步扩展,定义 联合一致函数,它是那些只与某些子函子一致的函数在一定条件下的组合。联合一致函数使用起来和一致函数一样,能够用来产生 新的up-to证明方法。另外,我们也相应地给出了传统并发理论中的联合一致函数概念,并且利用它给出了 弱互模拟的up-to方法。 在抽象的共代数模型中给出一般化的up-to方法之后,本文继续研究其在具体的无穷状态系统,即 BPA系统上的应用。Caucal的self-互模拟理论在 BPA系统的互模拟判定算法中起着关键作用,而它恰恰 是运用up-to方法协助互模拟判定的一个典范。 因为一个BPA系统也是一个共代数,我们在共代数理论中利用一致函数证明了该理论。 同时,本文给出了一个tableau算法,用来判定包含normed 与unnormed BPA进程的全BPA系统的互模拟等价问题。该算法非常直接且易于理解。 利用该tableau算法,我们证明了Hans H\"{u}ttel 和 Colin Stirling 为normed BPA进程设计的等式理论对于全BPA系统同样是可靠的与完备的。
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/88
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200518015029009罗凌云_paper.pdf(935KB)----限制开放 联系获取全文

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