中文摘要：

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

英文摘要：

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, Bemardi and Hennessy present a Web Service-oriented semantic CLT （Client Must Testing）. They studied the largest precongurence contained in the refinement relation C induced by CLT without considering recursive. Recursive operator is important and fundamental in specification theory. Bemardi and Hennessy have studied the largest precongurence contained in C . 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 C in the presence of recursive operator is presented.