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

摘要

Process algebra aims to provide algebraic theories for concurrent communication system,where the notions of behavioral equiv-alence and refinement play central roles. In particular,congruence or precongruence of behavioral relations provide theoretical foundation for compositional reasoning and modular designing and verifying. In order to capture the concurrent behavior of the server and the client, Bernardi and Hennessy present a Web Service-oriented semantic CLT (Client Must Testing). They studied the largest precongurence contained in the refinement relation奂~ induced by CLT without considering recursive. Recursive operator is important and fundamental in specification theory. Bernardi and Hennessy have studied the largest precongurence contained in奂~ . However,infinite processes cannot be expressed in such framework due to lacking recursive operator. Based on the exploring relationship among contexts,recursive processes and one step transition,a characterization for the largest precongurence contained in奂~ in the presence of recursive operator is presented.%进程之间的等价关系或精化关系的同余或前同余性(congruence或precongruence)是组合式推理和模块化设计验证的理论基础。针对面向Web Service的进程演算,Bernardi和Hennessy提出了Client-Must-Testing( CLT)语义及相关的测试前序偃用于描述进程的精化关系,并对包含于奂~的最大前同余关系奂~+进行了研究。递归算子是规范理论中重要而且是基础性的算子,Bernardi和Hennessy对包含于奂~的最大前同余关系的研究中未涉及递归算子,因此不能描述进程的无限行为。文中研究了CLT诱导出的精化关系在包含递归算子情形下的前同余性。在讨论了环境( context)、递归进程以及一步转换内在联系的基础上,给出包含于奂~的最大前同余关系。