CLT含递归算子的最大前同余性

来源：计算机技术与发展杂志2016年第09期北京时间：

作者：邓鹏辉;张晋津

摘要：进程之间的等价关系或精化关系的同余或前同余性(congruence或precongruence)是组合式推理和模块化设计验证的理论基础。针对面向Web Service的进程演算,Bernardi和Hennessy提出了Client-Must-Testing( CLT)语义及相关的测试前序偃用于描述进程的精化关系,并对包含于奂~的最大前同余关系奂~+进行了研究。递归算子是规范理论中重要而且是基础性的算子,Bernardi和Hennessy对包含于奂~的最大前同余关系的研究中未涉及递归算子,因此不能描述进程的无限行为。文中研究了CLT诱导出的精化关系在包含递归算子情形下的前同余性。在讨论了环境( context)、递归进程以及一步转换内在联系的基础上,给出包含于奂~的最大前同余关系。

关键词：进程代数;must-testing语义;精化关系;递归算子;最大前同余