文献类型：期刊文献

中文题名：带Mismatch算子的高阶π演算

英文题名：Higher-Order π-Calculus with the Mismatch Operator

作者：徐贤[1,2]

机构：[1]华东理工大学计算机科学与工程系,上海200237;[2]上海交通大学计算机科学与技术系,上海200240

年份：2014

卷号：25

期号：11

起止页码：2433

中文期刊名：软件学报

外文期刊名：Journal of Software

收录：CSTPCD;;EI(收录号：20144900301285);Scopus;北大核心:【北大核心2011】；CSCD:【CSCD2013_2014】；

基金：国家自然科学基金-法国国家科研署联合项目PACE(61261130589;12IS02001);国家自然科学基金(61202023;61173048)

语种：中文

中文关键词：公理化;互模拟;mismatch;线性;高阶;π演算;进程演算

外文关键词：axiomatization; bisimulation; mismatch; linear; higher-order; π-calculus; process calculus

摘要：主要研究带mismatch的高阶进程演算的公理化问题.首先,建立存在mismatch时高阶进程的开弱高阶互模拟理论,证明了等价关系、同余性等重要性质;其次,沿用线性的方法,构建得到带mismatch的有限进程上的公理系统;最后,基于对开弱高阶互模拟的刻画,证明了该公理系统的完备性定理.该工作为带mismatch的高阶进程上互模拟判定的有效算法的设计与实现,进而为相关的应用建模工作提供了理论借鉴.
This paper mainly studies the axiomatization of higher-order process calculi with the mismatch operator. Firstly, it formulates the theory of open weak higher-order bisimulation, and shows important properties such as equivalence and congruence. Secondly, following the method on linearity, it builds up an axiom system for finite processes. Finally, based on the characterization of open weak higher-order bisimulation, it proves the completeness of the axiom system. The work of this paper provides the basis for designing and implementing an effective algorithm for checking the bisimulation equivalence of higher-order processes with the mismatch operator, and a theoretical reference for relevant applications of modeling with higher-order processes.