λ-互模拟的研究

论文摘要

进程代数作为描述和分析并发与分布式系统的重要工具之一是并发理论的主流研究方向。互模拟是进程代数中刻画行为等价的核心概念,而模态逻辑特征是它的一个重要性质。随着进程代数的发展,许多不同的互模拟概念相继被提出。为了描述进程间的近似等价,最近文献中提出了λ-互模拟的概念,并将其性质与度量ρ联系在一起,给出了ρ为超度量时λ-互模拟的模态逻辑特征。但由于ρ不为超度量时λ-互模拟一般不为等价关系,所以无法得到一个具有HML经典形式的逻辑特征。由于在复合下λ-互模拟不能保持同余性,文献中引入了CCSθ,并初步讨论了λ-互模拟在CCSθ中一些有用的性质。本文将就λ-互模拟模态逻辑特征的开问题和CCSθ做一些研究。研究内容主要包括以下几个方面:（1）给出用于描述ρ不要求为超度量时λ-互模拟模态逻辑特征的新刻画形式。（2）引入一个新模态词,并在此基础上使用新的模态逻辑语言给出一个更具一般性的λ-互模拟的模态逻辑特征。（3）讨论CCSθ所描述的系统的特征,引入允许差异程度的概念,给出新的进程代数CCSθ,并初步讨论CCSθ的一些性质。

论文目录

• 第一章 绪论
• 1.1 引言
• 1.2 互模拟
• 1.3 互模拟的模态逻辑特征
• θ'>1.4 λ-互模拟和CCS_θ
• 1.5 本文的研究内容及结构安排
• 第二章 基本概念
• 2.1 CCS
• 2.1.1 CCS 的基本概念和符号
• 2.1.2 CCS
• 2.2 互模拟及其相关理论
• 2.2.1 互模拟的概念
• 2.2.2 互模拟的逻辑特征
• θ'>2.3 λ-互模拟和CCS_θ
• 2.3.1 λ-互模拟
• θ'>2.3.2 CCS_θ
• 第三章 λ-互模拟的模态逻辑特征
• σ,λ^<>'>3.1 模态逻辑语言L_σ,λ^<>
• σ,λ^<>中公式间的H_λ关系'>3.2 L_σ,λ^<>中公式间的H_λ关系
• 3.3 强λ-互模拟的模态逻辑特征
• 3.4 弱λ-互模拟的模态逻辑特征
• 第四章 分层的λ-互模拟的模态逻辑特征
• 4.1 分层的λ-互模拟
• 4.2 模态逻辑语言λ
• λ^k 关系'>4.3 E_λ^k关系
• 4.4 分层λ-互模拟的模态特征
• 4.5 ρ在为超度量时的模态特征
• θ'>第五章 CCS^θ
• 5.1 引言
• θ的讨论'>5.2 CCS_θ的讨论
• θ'>5.3 CCS^θ
• θ中的进程相等'>5.4 CCS^θ中的进程相等
• θ中进程的近似相等'>5.5 CCS^θ中进程的近似相等
• 第六章 总结和讨论
• 6.1 全文总结
• 6.2 进一步的工作
• 参考文献
• 致谢
• 在学期间的研究成果