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

• 作者: 张晋津 邓鹏辉
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: 进程代数 must-testing语义 精化关系 递归算子 最大前同余
• 年，卷（期）: 2016,（9）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 143-148
• 页数: 6页
• 分类号: TP301
• 字数: 6957字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2016.09.032

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	邓鹏辉	南京航空航天大学计算机科学与技术学院	3	0	0.0	0.0
2	张晋津	南京航空航天大学计算机科学与技术学院	5	0	0.0	0.0