计算机技术与发展2016，Vol.26Issue(9)：143-148,6.DOI:10.3969/j.issn.1673-629X.2016.09.032
CLT含递归算子的最大前同余性
Largest Precongurence with Recursive Operator in CLT
摘要
Abstract
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.关键词
进程代数/must-testing语义/精化关系/递归算子/最大前同余Key words
process algebra/must-testing semantic/refinement/recursive operator/largest precongurence分类
信息技术与安全科学引用本文复制引用
邓鹏辉,张晋津..CLT含递归算子的最大前同余性[J].计算机技术与发展,2016,26(9):143-148,6.基金项目
国家自然科学基金资助项目(11426136,60973045) （11426136,60973045）
江苏省高校自然科学基金(13KJB520012) （13KJB520012）
