灰箱演算的操作语义及表达能力研究

摘要

灰箱进程演算作为描述和分析移动计算系统的有效工具,因为其很强的抽象能力及其在理论和应用上的重要性,在进程演算领域一直得到广泛的关注。一方面,根据应用或理论研究的需要不断有新的灰箱演算类型被提出,随之而来的是在一些具体模型中出现了一些公开问题；而另一方面,人们开始关注灰箱演算变体之间,以及其它类型的进程演算同灰箱进程演算之间的相对关系。但是综合研究各类文献中的结果可以发现,相关研究一直较为零散,缺乏公信力和说服力。我们工作的主要贡献体现在以下几点:
　　 1.提出并研究了一种新的灰箱演算模型-半参数化安全灰箱演算,它是对经典安全灰箱演算模型的改进和推广。我们深入研究了半参数化安全灰箱演算的语义系统和互模拟理论,并将其中的技术和结果应用于研究安全灰箱演算,得到了安全灰箱演算模型中的一系列新结论,加深了对安全灰箱演算模型的理解。
　　 2.在灰箱演算的表达能力方面,我们的贡献主要体现在两方面:一是在绝对表达能力方面,我们研究了一些公平灰箱演算的子演算上的进程终止问题的可判定性证明。二是在相对表达能力方面,我们重新定义了表达能力比较的标准,然后据之证明了一些表达能力上的否定性结论；此外还给出了一些与灰箱演算有关的进程模型之间的编码,特别是研究了从π演算到安全灰箱演算上的编码。这些编码就满足的性质而言,都是迄今已知的最好编码。这两方面的结论对今后的工作具有较强的启发和指导意义。
　　 3.提出并研究了匿名灰箱演算。匿名灰箱演算作为公平灰箱演算的一种扩展,其特点是定义了动作之间的偏序关系,以及这种偏序关系之上的标号转移系统和互模拟关系。匿名灰箱演算被证明具有非常优美的代数性质,具有广泛的应用前景。作为匿名灰箱演算表达能力的一个证明,我们给出了不带open的移动灰箱演算在匿名灰箱演算中的一个解释。
　　 简要地说,本文着重研究了灰箱演算中的两大类问题:语义问题和表达能力问题。在研究中我们系统而深入地考察了前人的相关结果,在此基础上开展了我们的工作。本文的工作对下一步的研究具有较强的指导意义；在对经典问题的研究上推进了相关领域的研究工作；在提出新模型的研究上,扩展了灰箱演算领域的研究范围。

目录

文摘

英文文摘

上海交通大学博士学位论文答辩决议书

第一章 概述

1.1 背景介绍

1.1.1 进程演算的一般背景

1.1.2 移动计算的形式化模型概览

1.1.3 交互

1.2 动机和贡献

1.2.1 研究动机

1.2.2 主要贡献

1.3 论文的主要内容和结构安排

第二章 半参数化安全灰箱演算

2.1 背景

2.2 HPSA演算

2.2.1 语法及规约语义

2.2.2 基于规约的观测同余

2.3 标号转移语义

2.3.1 标号转移系统

2.3.2 基于标号的互模拟

2.4 互模拟性质

2.5 增加通信

2.6 应用

2.7 本章小结

第三章 安全灰箱演算

3.1 安全灰箱演算

3.2 标号转移语义

3.2.1 标号转移系统

3.2.2 基于标号的互模拟

3.3 互模拟性质

3.4 本章小结

第四章 灰箱演算的表达能力研究

4.1 公平灰箱演算上的判定问题

4.1.1 公平灰箱演算

4.1.2 进程终止问题及WQO

4.1.3 FA片段的终止性判定问题

4.2 进程演算相对表达能力问题

4.2.1 研究相对表达能力的方法

4.2.2 表达能力的比较标准

4.2.3 子互模拟关系在灰箱演算中的应用

4.3 本章小结

第五章 同步π演算到安全灰箱演算的翻译

5.1 背景概要

5.1.1 同步π演算

5.1.2 安全灰箱演算的语义

5.2 编码的标准及对以往编码的讨论

5.2.1 编码的标准

5.2.2 已有的翻译工作及评价

5.3 从同步π演算到安全灰箱演算的翻译

5.3.1 翻译方案Ⅰ:不使用辅助的公开名

5.3.2 翻译方案Ⅱ:使用辅助的公开名

5.4 本章小结

第六章 匿名灰箱演算及其应用

6.1 匿名灰箱演算

6.1.1 标号转移系统

6.1.2 互模拟的定义

6.1.3 匿名灰箱演算上的代数性质

6.2 匿名灰箱演算的应用

6.2.1 对FA的解释

6.2.2 对MA的解释

6.3 本章小结

第七章 总结与展望

7.1 总结

7.2 展望

参考文献

致谢

索引

攻读博士学位期间发表的论文