可观测共变-逆变模拟及其公理系统的研究

摘要

进程代数研究的核心内容之一是讨论进程之间的行为等价或精化关系。传统的行为等价或精化关系不考虑动作的类型,它们不适合处理具有输入输出的计算模型。最近,Fábregas等人基于动作的分类提出并研究了共变-逆变模拟。目前所有关于共变-逆变模拟的讨论均是基于它的强形式(即,对内、外动作的处理不加区分)。而对于现实计算更有意义的弱形式下的共变-逆变模拟,尚未发现有相关工作的报道。本文对弱形式的共变-逆变模拟进行了研究,主要工作包括如下方面:
　　(1)给出了一种弱共变-逆变模拟及其模态逻辑特征。
　　(2)较深入地研究了包含在弱共变-逆变模拟关系中的最大前同余关系——可观测共变-逆变模拟。给出了可观测共变-逆变模拟的公理系统 ccAX,并证明了该公理系统的可靠及基完备性。
　　(3)证明了当互变动作集为无限集时,BCCSP的两个公理系统1BCCSPAX和2BCCSPAX分别相对于强共变-逆变模拟与可观测共变-逆变模拟是??完备的,进而得出这两个公理系统也是强完备的。

目录

封面

声明

中文摘要

英文摘要

目录

图表清单

缩略词

第一章 绪论

1.1 引言

1.2 进程代数

1.3 共变-逆变模拟研究现状

1.4 本文的研究内容及结构安排

第二章 基本概念

2.1 EBCCSP

2.2 共变-逆变模拟及其逻辑特征

2.3 本章小结

第三章 可观测共变-逆变模拟

3.1 弱共变-逆变模拟

3.2 弱共变-逆变模拟的逻辑特征

3.3 可观测共变-逆变模拟

3.4 的代数性质

3.5 本章小结

第四章 公理系统 ccAX 及其完备性

4.1 公理系统 ccAX

4.2 ccAX 的可靠性

4.3 ccAX 的基完备性

4.4 1BCCSPAX 和 2BCCSPAX 的??完备性

4.5 本章小结

第五章 总结和展望

5.1 全文总结

5.2 进一步的工作

参考文献

致谢

在学期间的研究成果及发表的学术论文