计算机科学中的共代数方法的研究综述

代数理论已经在抽象数据类型、程序语义等计算机科学领域有了广泛的应用,而代数的对偶概念--共代数,则直到20世纪90年代中后期才被越来越多的计算机学者关注.代数从"构造"的角度研究数据类型,而共代数则从"观察"的角度考察系统及其性质.共代数方法对研究基于状态的系统有独特的优越性,可以对系统的行为等价、不确定性等从数学上进行深入的探讨.目前,共代数理论已经逐步应用在自动机理论、并发程序的语义、面向对象程序的规范等领域.对共代数的基本概念、范畴理论基础、共代数逻辑及应用等方面的最新研究成果进行了介绍,以引起国内相关研究领域的学者对计算机科学中的共代数方法的关注.  

传值系统的互模拟与谓词等式系

本文引入描述传值并系统的新模型“带赋值符号迁移图（ＳＴＧＡ）”推广了Ｈｅｎｎｅｓｓｙ和Ｌｉｎ提出的“符号迁移图”的概念，允许迁移上带有赋值，从而能将更大的一类传值系统表示为有穷状态图，ＳＴＧＡ的中车优点是在并行运算不封闭，文中给给ＳＴＧＡ的操作语义，在此基础上定义了ＳＴＧＡ的互模拟等价关系，为了刻划ＳＴＧＡ的互模拟，以谓词等式系的形式在一阶逻辑的正子集中扩充了最大和最小不动点，并设计了一个算法将Ｓ  

Verilog操作语义研究

提出了一个结构化操作语义模型,用于描述Verilog核心子集的语言特征,此子集包含了事件驱动、基于共享变量的并发特性、时间延迟等Verilog的主要语言成分.在此操作语义模型中,所有的Verilog程序将被统一地认为是开放式系统,所以在此操作语义模型的基础上能够进一步提出Verilog开放进程的观察模型,并提出基于互模拟的观察等价概念来判定进程之间的等价关系.最后证明了所定义的观察等价关系对所有的Verilog构造子而言是一个同余关系,从而为发展相应的进程代数理论提供了一个可靠性基础.  

时间符号迁移图及其互模拟判定

引入时间符号迁移图的概念，作为既涉及通讯又具有实时性的并发系统的模型，该文给出了这种迁移图时间互模拟的算法，并证明了该算法的正确性。  

π-演算互模拟判定算法的优化和实现

π-演算采用互模拟作为进程等价的准则.对有限状态的π-演算进程互模拟等价是可判定的，由此提出了互模拟检测算法的一种优化技术.该技术基于只将输入名字实例化为在以后的等名测试中用到的自由名字.通过实例说明这一优化技术可大大减少所用的时间和空间,并证明了优化算法的正确性.  

基于CCS的软件规范描述及实例研究

软件规范描述方法主要是软件工程化的UML方法与形式化方法二类方法。论文主要给出了基于CCS的软件规范描述,首先根据系统需求画出进程派生树和迁移图,再根据操作语义和系统约束条件得到进程表达式,并用Java语言实现了系统原型代码。笔者的工作证明了CCS具有细节化地描述系统内部状态,便于系统软件实现的能力;在手工转换进程迁移图到进程表达式的基础上,提出了自动转换的进一步研究思路。  

移动进程演算中的开互模拟

该文就移动进程演算中的弱开同余关系进行了研究。文中考虑了一种简单的非确定性移动进程演算模型，证明了Milner的三条tau规则在有等名测试算子时不足以将强开同余关系的完全公理化系统提升到同余关系的完全公理化系统，文中提出了第四条tau规则，处理了在前缀操作下的等名测试算子，并证明了强开同余关系的完全公理化系统加上四条tau规则可得到弱开同余关系的完全公理化系统。该文的结论否定了关于Milner的三条tau规则足以将π－演算中的强同余关系的完全公理化系统提升到弱同余关系的完全公理化系统的猜想。  

Web服务组合的互模拟验证

为检验Web服务组合的实现与用户需求的一致性，在开互模拟形式化理论和检验工具的基础上，提出了一个自动化检验方法。首先，用π-演算分别对用户需求和商业流程可执行语言（BPEL4WS）程序实现建模，然后对它们进行弱开互模拟检验，当它们不互模拟时，检验工具能自动标识关键的不互模拟的BPEL4WS程序片段。最后通过实例说明这一方法的可行性。  

自动机,逻辑与博弈

讨论了特定的自动机、自动机的识别能力、逻辑的表达能力和博弈思想的关系。使用博弈思想可以比较容易地证明一元二阶逻辑(S1S和S2S)的可决定性。主要考虑线性时间(linear time)与分支时间(branch time)两种情况，通过这些逻辑与别的时态逻辑的表达能力的等价性可以证明其它逻辑也具有决定性，可以设计相应的自动机去解决模型检查(Model Checking)问题。  

元Chi进程互模拟等价的一致性

Chi-演算是将π-演算中两类受限名统一后得到的.多态Chi-演算扩充了Chi-演算的通信能力,使得一次通信可传递多个信息.元Chi-演算是在省略多态Chi-演算的前缀操作子之后得到的子语言.研究了元Chi-演算的互模拟等价关系,证明了在某种意义下,元Chi-进程之间只有一个互模拟等价关系.