面向传值进程的谓词μ-演算与FO(HML)的完备推演系统

• 作者: 林惠民 薛锐
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 传值进程 μ-演算 模型检测 Tableau 推演完备
• 年，卷（期）: 2002,（6）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 561-569
• 页数: 9页
• 分类号: TP301
• 字数: 11615字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2002.06.001

摘要

作者提出一个谓词μ-演算系统,目的在于描述传值进程的性质.该系统的公式和谓词相互递归定义,谓词中含有抽象式、谓词变元以及最大和最小不动点.其语义模型是带赋值的符号迁移图所诱导的迁移系统.并且该系统包含Hennessy-Milner逻辑的一阶扩充FO(HML)作为子系统.作者用例子说明了本演算系统在表达传值进程性质方面的优越性.该文后半部分主要给出了FO(HML)的一个推演系统,并运用判定树(Tableau)的方法,证明了所给的推演系统是完备的.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	薛锐	中国科学院软件研究所计算机科学实验室	20	275	7.0	16.0
2	林惠民	中国科学院软件研究所计算机科学实验室	11	360	5.0	11.0