论文摘要
在并发系统中，多个任务同时执行。对并发系统的理论研究，主要有进程代数、模态逻辑等。其中最有代表性的是Robin Milner提出的CCS进程演算理论及其变种，包括Pure CCS、Value-passing CCS、π-演算、界程演算等等。模型检测技术是一种针对有限状态并发系统的自动分析与验证技术，其基本思想是状态搜索（State Exploration）。对状态空间的穷尽搜索有赖于对系统建立的有穷状态模型，以保证搜索过程的终止。模型检测的优点是能够做到完全自动化，在搜索终止时，如果性质没有满足，能够给出反例，这有利于用户对系统进行改进；缺点是建模比较困难，且面临状态空间爆炸的问题。模型检测算法分为两类，一类是全局检测算法，给定一个逻辑表达式，求出系统中满足给定表达式的所有状态集合，另一类是局部检测算法，给定一个逻辑表达式和一个状态集合，判断状态集合中的所有状态是否满足给定的逻辑表达式。本文的研究工作主要有以下几个方面：1．在界程演算方面。由于在移动界程（Mobile Ambients，MA）中，in、out、open操作可以不受限进行，环境对自身边界没有任何管理权限，并且由于MA中open操作的存在，两个原本不在一块的进程能通过open操作后处在同一环境中，这样可导致两个进程间意想不到的交互（干扰）的产生。为了克服这些不足，安全环境演算（Safe Ambients，SA）中增加了in、out、open协操作，分别是对in、out、open操作的许可；带口令的安全界程演算（Safe Ambients with Password，SAP）SAP在in、out、open、in、out、open操作中增加口令（或通道），只有掌握口令（或通道）的进程才能进行in、out、open操作；盒子界程演算（Boxed Ambients，BA）中取消了open操作，同时增加了父子界程间能够跨界程通信的操作原语。SA、SAP和BA都是对MA演算的改进，但都只是局部的改进，最终SA、SAP不能避免由于open操作带来的干扰，BA也控制不了in和out操作对界程边界的随意穿越。同时由于BA中无open操作，界程一旦建立，将永远停留在系统中，这样将占用大量的系统资源，也不符合进程的实际情况。为了克服MA、SA、SAP和BA的不足，本文提出了一个带口令的安全盒子界程演算（Safe Boxed Ambients with Password，SBAP）。相对于MA，BSAP做了如下几点改进：（1）取消了MA中的open操作，增加了父子界程间的通信操作原语；（2）增加了in、out操作，并在in、out、in、out操作中加入了密码；（3）增加了界程回收操作原语del。通过用SBAP对Internet上的电子邮件系统进行描述和仿真以及对进程死锁的实时处理，说明SBAP在网络计算方面有一定的表现能力。2．在mu-演算模型检测方面。针对完全μ-演算的全局模型检测算法的设计，根据Tarski’s不动点定理，公式中的不动点算子直接用逐次迭代来计算，则对有不动点算子嵌套的逻辑表达式进行计算的全局算法的时间复杂性为O(nk+1)，其中n为变迁系统的状态总数，后为不动点算子嵌套深度。Long等人在分析了计算嵌套不动点表达式的中间结果间的偏序关系找到了一个时间复杂性为O(n（?）d/2（?）+1)，空间复杂性为指数的全局计算算法。本文在Long等人工作的基础上，根据μ-演算公式中函数的单调特性，提出了一个时间复杂性为O(（2n+1）（?）（d+3）/4（?）+（?）（d+2）/4（?）)，空间复杂性为D（dn）的计算交替嵌套μ-演算公式的全局模型检测算法，在目前已知的针对完全μ-演算的全局模型检测算法中是首个空间复杂性为D（dn）且时间复杂性指数部分只有d／2的算法。算法性能的改善，使得不动点算子交替嵌套深度很大的μ-演算公式的求解成为可能，这在模型检测方面有着非常重要的意义。3．在界程逻辑模型检测方面。本文在林惠民院士的工作基础上，讨论了带递归的谓词界程逻辑在有限控制移动界程上的模型检测问题，首次将嵌套谓词等式系应用到带递归的谓词界程逻辑模型检测中，提出了一个时间复杂性与逻辑公式的交错嵌套深度呈指数关系的局部模型检测算法，这是目前首个有明确时间复杂性的谓词界程逻辑模型检测算法，也是目前己知的第二个带递归的谓词界程逻辑模型检测算法。所做的工作主要有：（1）讨论了谓词界程逻辑公式与嵌套谓词等式系间语义的等价性，给出了谓词界程逻辑公式转换成嵌套谓词等式系的方法；（2）讨论了不动点算子无交错的谓词界程逻辑模型检测问题，给出了具体算法；（3）讨论了不动点算子交错嵌套情况下的谓词界程逻辑模型检测问题，给出了一个通用的局部算法。