学位论文 > 优秀研究生学位论文题录展示

高阶进程演算的互模拟理论和公理化的研究

作　者: 徐贤
导　师: 傅育熙
学　校: 上海交通大学
专　业: 软件与理论
关键词: 互模拟公理化编码逻辑刻画 π演算 CCS 高阶进程演算
分类号: TP301
类　型: 博士论文
年　份: 2008年
下　载: 192次
引　用: 1次
阅　读: 论文下载

内容摘要

高阶进程演算,因为其很强的抽象能力和理论上的重要性,在进程演算领域一直得到广泛的关注,并成为描述和分析具有动态变换特性的内部连接结构的移动系统的有效数学工具。在本文中,我们对高阶进程演算就如下几方面进行了研究。·带有mismatch的高阶π演算:互模拟理论;带有mismatch的高阶π演算的线性片段:公理化。高阶进程演算的公理化问题,如高阶π演算的公理化问题,一直以来鲜有相关工作。然而无论在理论上还是在应用中,判断两个高阶进程是否在某种互模拟下等价都有其重要意义,这种判断需要一个能够有效地进行分析并给出结论的算法。从算法的观点看,mismatch是在互模拟理论以及公理化中都是很有用的操作子;我们通过考察带有mismatch的高阶π演算来深入研究了公理化问题。我们首先形式化地定义并讨论了存在mismatch时的互模拟理论,其中我们的互模拟称为开弱高阶互模拟,这是一种nondelayed型的开型互模拟。随后,在设计公理系统时我们采用了线性方法,即将演算限制到线性片段上。利用对开弱高阶互模拟的刻画,包括前缀进程间等价与其延续进程间等价之间的关系以及线性演算独有的性质,我们最终证明了公理系统的完备性。我们对高阶互模拟理论和公理化的研究,不仅通过引入一个有用的操作子对以往的工作进行了扩展,且将高阶公理化的研究又向前推进了一步,同时为对其它高阶演算(如Ambient演算)的研究提供了参考。·高阶CCS 编码一阶π演算。不同演算之间的编码是比较它们的表达能力的有效方法,可以揭示它们之间的本质区别。Thomsen和Sangiorgi对高阶演算(分别是高阶CCS和高阶π演算)与一阶π演算之间的相互编码进行了研究,但他们的工作尚不完整,缺少对用高阶CCS对一阶π演算编码的全抽象性质的深入研究。在本文中,我们试图解决这一问题。我们基于Thomsen的编码方法,将一阶π演算翻译到Plain CHOCS中。我们证明这种编码方法在基互模拟性(一阶π演算中)和wired互模拟性(Plain CHOCS中)下是全抽象的,其中wired互模拟性是我们定义的基于仅发送和接收线缆(wire)的wired进程的一种互模拟,它们是编码策略的核心。进一步,由于wired互模拟性蕴含广为人知的上下文互模拟性,我们确保了在基互模拟性和上下文互模拟性下编码的可靠性。我们使用领域中已有的索引技术来处理技术细节中的难点以获得主要结论,即将索引技术应用到原始编码方法中,以此来处理编码中产生的额外内部动作,随后将带索引的编码方法中所获得的结果移植得到原始编码中的相应结论。我们还讨论了如何通过在两个演算中选抒合理的互模拟来获得全抽象性质等问题。我们对进程演算问编码的研究解决了关于在高阶CCS中表达一阶π演算的一个末决问题,从而补充了这两类演算之间的编码研究,这进一步展现了一阶演算和高阶演算之间的关系。此外,编码研究的结果还提供了用高阶演算来实现对λ演算编码的另一种方法。·线性高阶π演算中局部互模拟的逻辑刻画。除了用代数方法对高阶进程演算的互模拟进行工作外,从逻辑角度对互模拟的研究也有其价值所在,目前已经有对Plain CHOCS中的强和弱上下文互模拟进行逻辑刻画的工作。在本文中,我们用逻辑的方法对线性进程演算进行了一些新的研究。我们致力于找到一种对线性高阶π演算中局部互模拟的逻辑刻画。为此我们通过两步来完成准备:首先我们通过一些变体来简化局部互模拟性;其次我们通过互模拟递减链来逼近局部互模拟性。为实现逻辑刻画,我们对演算进行了重新形式化,以获得相对容易实现刻画的等价形式(在互模拟意义上)。我们的逻辑具有完整的非操作(对偶性),并且比已有的逻辑语言简单,这体现在高阶模态被降阶为类似于一阶模态,且构造蕴含操作子仅被用于处理一阶受限输出。我们证明了刻画定理,它将逻辑等价与局部互模拟性相关联。我们关于逻辑刻画的工作对高阶进程演算研究的意义在于提供了另一种观点,即逻辑的观点,以此补充了代数角度的研究。此外,将检验互模拟等价转换为检验逻辑等价使得我们马上可以使用逻辑的一整套方法,后者不但具有诸多模型检测算法,而且有许多实用的工具。本文不仅对高阶进程演算领域内的几个方面的问题进行了研究,且传递了几点有意义的信息。首先是线性性质在确保高阶演算的可靠且完备的公理系统中具有重要意义,这一特征成功的降低了通信进程的表达能力。其次,作为用一阶π演算来表达高阶演算的补充,我们证明了其反向在一些合理的互模拟性下亦成立,这使得我们可以更加确信高阶演算的相对独立性,结合其特有的抽象能力,这种独立性使得高阶演算更有吸引力。再次,通过展示一种可以刻画互模拟等价的简单且完备的逻辑语言,我们的逻辑刻画工作提供了对线性性质的进一步认识,并扩展了高阶进程演算的应用领域。

全文目录

摘要  5-7
ABSTRACT(英文摘要)  7-12
第一章引言  12-26
  §1.1 背景  12-14
    §1.1.1 进程演算的一般背景  12-13
    §1.1.2 Mobility  13-14
  §1.2 动机和贡献  14-23
  §1.3 论文章节安排  23-26
第二章预备知识  26-38
  §2.1 高阶进程演算概览  26-33
    §2.1.1 Plain CHOCS  26-27
    §2.1.2 高阶π演算  27-31
    §2.1.3 线性高阶π演算  31-33
  §2.2 互模拟基础知识简介  33-38
    §2.2.1 强与弱互模拟  33-34
    §2.2.2 迟和早互模拟  34
    §2.2.3 同余  34-35
    §2.2.4 互模拟Up-to  35-38
第三章带mismatch的高阶π演算  38-60
  §3.1 简介  38
  §3.2 带mismatch的高阶π演算  38-45
    §3.2.1 语法  38-42
    §3.2.2 语义  42-44
    §3.2.3 线性片段  44-45
  §3.3 互模拟  45-60
    §3.3.1 互模拟定义  46-52
    §3.3.2 等价关系  52-56
    §3.3.3 同余性  56-60
第四章开弱高阶互模拟的特征刻画  60-72
  §4.1 带前缀进程和剩余进程间的关系  60-66
    §4.1.1 高阶输入  61-63
    §4.1.2 高阶输出  63-66
  §4.2 局部环境中的同余  66-72
    §4.2.1 局部同余  68-69
    §4.2.2 更多技术引理  69-72
第五章公理化  72-98
  §5.1 公理系统  74-77
  §5.2 范式  77-79
  §5.3 Saturation性质  79-82
  §5.4 完备性  82-90
  §5.5 讨论  90-96
    §5.5.1 定义  90-91
    §5.5.2 一些性质  91-93
    §5.5.3 公理系统  93-96
  §5.6 小结  96-98
第六章在高阶演算中表达一阶π演算  98-126
  §6.1 简介  98-99
  §6.2 基本定义  99-107
    §6.2.1 FOPi  99-101
    §6.2.2 Plain CHOCS  101-104
    §6.2.3 Indexed Plain CHOCS  104-107
  §6.3 编码策略  107-113
    §6.3.1 Wire的刻画  109-113
  §6.4 索引技术下的编码策略  113-121
    §6.4.1 带索引的编码策略  114
    §6.4.2 刻画indexed wire  114-118
    §6.4.3 全抽象相关性质  118-121
  §6.5 讨论及工作展望  121-124
  §6.6 小结  124-126
第七章线性高阶π演算中局部互模拟的再研究  126-156
  §7.1 简介  126-127
  §7.2 线性高阶π演算  127-134
    §7.2.1 语法  127-129
    §7.2.2 语义  129-132
    §7.2.3 互模拟  132-134
  §7.3 简化局部互模拟  134-154
    §7.3.1 局部线性互模拟  135
    §7.3.2 刻画局部线性互模拟  135-147
    §7.3.3 与局部互模拟性的一致性  147-149
    §7.3.4 关于一阶受限输出  149-151
    §7.3.5 逼近局部互模拟  151-154
  §7.4 小结  154-156
第八章线性高阶π演算中的逻辑刻画  156-176
  §8.1 简介  156-158
  §8.2 线性高阶π演算的重新形式化  158-165
    §8.2.1 语法  158-159
    §8.2.2 语义  159-162
    §8.2.3 互模拟  162-165
  §8.3 逻辑  165-170
    §8.3.1 特征公式  167-168
    §8.3.2 刻画定理  168-170
  §8.4 讨论  170-174
    §8.4.1 Q-开互模拟  171-172
    §8.4.2 逻辑刻画的再研究  172-174
  §8.5 展望  174-175
  §8.6 小结  175-176
第九章总结与展望  176-180
参考文献  180-186
索引  186-190
图列表  190-191
致谢  191-192
论文列表  192

相似论文

基于DSP的集成光栅细分数显装置的研制,TH822
转轴径向跳动和转速实时检测光电系统的研究,TH822
路面平整度检测系统中的数据采集和定位技术研究,U416.2
说话人识别中不同语音编码影响的补偿方法,TN912.34
基于均值匹配的Turbo码联合译码的Matlab实现,TN911.22
网络语音传输丢包的恢复技术,TN912.3
基于高阶累积量的频谱感知技术仿真分析,TN911.23
联合编码调制技术中TCM与BICM方案性能研究,TN911.22
高频雷达复合调制波形设计与处理,TN958.93
DMR集群系统高层协议的设计和研究,TN929.52
基于纹理特征的视频编码技术研究,TP391.41
图像的稀疏表示及编码模型研究,TP391.41
基于地理位置的WSNs路由算法研究与改进,TN929.5
深水管道回接位姿检测系统研究,TE973.3
物联网在服装行业的应用性研究,TN929.5
江苏省稻瘟病菌遗传多样性及水稻抗瘟基因鉴定,S435.111.41
中老年人健身认知观念的研究,G812.4
2006～2010年某院肺癌病案中M8000/3编码者相关特征分析,R734.2
网络传输中的ROI图像编码算法研究,TN919.81
基于激光测距的罐道位移监测系统的设计与应用,TN247
急性白血病儿童还原型叶酸载体基因多态性研究,R733.71