一种高阶进程代数的弱互模拟研究

摘要

进程代数作为描述和分析并发与分布式系统的重要工具之一，是并发理论的主流研究方向。互模拟是进程代数的核心概念之一，用来刻画进程之间的等价关系，其中描述观察等效的弱互模拟是最为重要的互模拟之一，其性质往往比较难以研究。 高阶进程代数在描述一些系统的时候比较直观，很有优势，受到越来越多的关注，但高阶进程代数的性质难以刻画。本文研究的高阶演算一直没有一个很自然且相对简单的建立在带标记语义系统之上的等价关系，不是给定的互模拟性质太强，就是给出的互模拟证明很繁琐。有学者用环境带标记的转换语义来刻画高阶进程代数，给出的互模拟形式相对简洁。 本文研究了建立在环境带标记的转换基础之上的受限的高阶演算的弱互模拟，证明了弱互模拟的代数性质和同余性质。 近来，人们也越来越多地用规约语义描述进程代数，因为规约语义简洁且能给出一个满意的数学分析。我们介绍了一个规约系统，基于它证明了其与上面给出的环境带标记的语义在弱互模拟的情况下是有等价关系的，即两个进程是弱互模拟的当且仅当它们是规约barbed同余的。