-
题名CLT含递归算子的最大前同余性
- 1
-
-
作者
邓鹏辉
张晋津
-
机构
南京航空航天大学计算机科学与技术学院
-
出处
《计算机技术与发展》
2016年第9期143-148,共6页
-
基金
国家自然科学基金资助项目(11426136
60973045)
江苏省高校自然科学基金(13KJB520012)
-
文摘
进程之间的等价关系或精化关系的同余或前同余性(congruence或precongruence)是组合式推理和模块化设计验证的理论基础。针对面向Web Service的进程演算,Bernardi和Hennessy提出了Client-Must-Testing(CLT)语义及相关的测试前序ㄈ用于描述进程的精化关系,并对包含于的最大前同余关系+进行了研究。递归算子是规范理论中重要而且是基础性的算子,Bernardi和Hennessy对包含于的最大前同余关系的研究中未涉及递归算子,因此不能描述进程的无限行为。文中研究了CLT诱导出的精化关系在包含递归算子情形下的前同余性。在讨论了环境(context)、递归进程以及一步转换内在联系的基础上,给出包含于的最大前同余关系。
-
关键词
进程代数
must-testing语义
精化关系
递归算子
最大前同余
-
Keywords
process algebra
must-testing semantic
refinement
recursive operator
largest precongurence
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名CLT树型指称语义的研究
- 2
-
-
作者
邓鹏辉
张晋津
-
机构
南京航空航天大学计算机科学与技术学院
-
出处
《电子世界》
2016年第6期137-139,共3页
-
基金
国家自然科学基金11426136
60973045
江苏省高校自然科学基金13KJB520012
-
文摘
在面向服务器的进程代数理论中,为了描述服务器和客户之间的并发行为,Bernardi和Hennessy等人提出了client must-testing(CLT)语义,service must-testing(SVR)语义用于描述进程的精化关系,并对SVR的前缀封闭集以及树型指称语义进行了的研究。但关于CLT语义的指称语义并未涉及,本文将基于此语义,通过建立标准型的方法,对此语义的树型指称语义进行研究。
-
关键词
进程代数
并发行为
must-testing语义
指称语义
标准型
-
分类号
TP312
[自动化与计算机技术—计算机软件与理论]
-
