对称与动作细化

论文摘要

一般硬件系统和软件系统都存在大量的相同的或同构的组件,相应地,它们的模型常常在结构上存在对称性,这种对称结构一般具有相同或非常相近的性质。人们为了使问题简化,根据这种情况开发了对称约简算法来简化模型。特别是在形式化验证中,对称约简方法已经成为解决状态爆炸问题的有效方法之一。进程代数已经是刻画并发系统的最普遍、最常用的描述语言,而事件结构也是刻画真并发系统的强有力的建模工具,它们常常展示出对称性。然而,当前大多数研究都集中在基于变迁系统模型的对称约简,从未涉及这两种建模工具的对称性方面的研究。在本文中,我们对进程代数语言和事件结构模型的对称约简进行了深入研究。这些工作力图从结构上建立对建模语言和模型进行约简的基本理论,目的是希望从结构上建立起类似于行为等价的由细到粗的约简体系,为开发复杂系统而建立的不同层次静态约简模型服务。另一方面,自顶向下逐步细化的层次化设计方法是人们广泛接受的设计计算机硬件系统和软件系统的最主要方法之一。动作细化是系统层次化刻画方法的核心操作,这一理论的研究一般在进程代数和事件结构模型中进行的,已经取得了丰硕的成果。在此基础上,我们研究了对称约简对动作细化的影响,同时研究了交织等价和步进等价在动作细化下的保持问题。本文针对进程代数语言提出了进程的对称性概念,给出了对称约简算法,并证明了约简后的进程与原进程是交织迹和交织互模拟等价的,同时提供了两个有意义的实例来说明对称性的定义并验证了约简算法的正确性。接下来,针对事件结构模型我们提出了基于置换群的对称性概念。在事件结构中,引入了事件结构的商结构模型,证明了商结构与原事件结构是迹、互模拟和偏序多集迹等价的,建立了针对事件结构的对称约简算法,得出了对称约简不影响等价在动作细化下的保持。在研究了事件结构的对称性之后,进一步从理论上比较对称约简与自互模拟约简的区别和联系。交织等价(即交织迹等价和交织互模拟等价)与步进等价(即步进迹等价和步进互模拟等价)在动作细化下是不保持的。一些工作研究了交织互模拟等价在严格限制动作细化的情况下才能保持,但在这种限制下交织迹等价仍然不保持,没有工作进一步讨

论文目录

• 摘要
• Abstract
• 目录
• 第一章 绪论
• 1.1 对称
• 1.1.1 计算机科学中的对称
• 1.1.2 对称与对称约简
• 1.2 动作细化
• 1.2.1 动作细化方法
• 1.2.2 动作细化分类
• 1.2.3 动作细化的保持
• 1.2.4 对称与动作细化
• 1.3 相关工作
• 1.4 本文创新
• 1.5 本文组织
• 第二章 理论基础
• 2.1 进程代数
• 2.2 事件结构
• 2.3 动作细化
• 2.4 标记变迁系统
• 2.5 模型检验
• 第三章 进程代数中的对称性
• 3.1 引言
• 3.2 进程代数与自同构
• 3.2.1 进程代数
• 3.2.2 自同构
• 3.3 进程代数的对称性
• 3.4 行为等价的保持
• 3.5 一个约简算法
• 3.6 例子
• 3.7 小结
• 第四章 事件结构的对称性
• 4.1 引言
• 4.2 事件结构的对称
• 4.2.1 置换群
• 4.2.2 自同构群
• 4.2.3 商事件结构
• 4.3 对称与等价
• 4.4 动作细化的保持
• 4.5 对称约简算法
• 4.6 小结
• 第五章 对称与自互模拟
• 5.1 引言
• 5.2 自互模拟
• 5.3 自互模拟与对称的区别
• 5.4 自互模拟与对称的联系
• 5.5 小结
• 第六章 等价在动作细化下的保持
• 6.1 引言
• 6.2 交织等价
• 6.3 步进等价
• 6.4 动作细化下等价的保持
• 6.4.1 束动作变迁
• 6.4.2 交织等价的保持
• 6.4.3 步进等价的保持
• 6.5 小结
• 第七章 基于束动作的偏序约简
• 7.1 引言
• 7.2 传统的偏序约简
• 7.2.1 Kripke 结构
• 7.2.2 动作独立
• 7.2.3 扫描迹等价（Stuttering Equivalence）
• 7.2.4 偏序约简
• 7.3 动作与束动作
• 7.4 束动作的基本思想
• 7.5 束动作路径扫描迹等价
• 7.6 束动作偏序约简
• 7.7 束动作偏序约简的实现
• 7.8 小结
• 第八章 总结和展望
• 8.1 总结
• 8.2 展望
• 参考文献
• 发表的论文
• 致谢