并发计算的元模型Ⅰ.图模型

借鉴证明论中的一些思想 ,提出了并发计算的一个图模型 .在此模型中 ,计算对象表示为图 ,计算过程表示为图重写 ,重写规则将通信过程视为证明的等价变换过程 .为便于形式化研究图模型 ,提出了模型的形式对应物——图演算 ,该演算类似于进程代数演算 ,与其他进程代数演算的不同之处在于本演算是对称的 .文中用证明论方法研究并行理论 。

并发计算的元模型 Ⅱ.对称通信

在并发计算图模型的基础上 ,提出并研究了一新的进程演算 .该演算的创新处在于它只有一类前缀操作 ,故通信是对称的 .通过建立从 pi演算到对称 pi演算的翻译 ,证明 pi演算是对称 pi演算的子语言 .该翻译既保持前者的操作语义 ,又保持其代数语义 .对称 pi演算的意义在于它既简化了 pi演算 。

并发计算的元模型 Ⅲ.互模拟格

在有关 chi演算的基础上 ,用统一的方法在 chi进程上引入一大类互模拟等价关系 ,即 L-互模拟等价关系 .证明了只有 4个不同的 L-互模拟等价 ;在包含关系下 ,它们构成钻石格 .许多常见的互模拟等价都可定义为