面向传值进程的一阶模态逻辑的可判定性与模型检测

摘要：

对于面向传值进程的Hennessy-Milner逻辑的一阶扩充HML(FO),给出了基于带赋值的符号迁移图的语义解释.证明了HML(FO)的子逻辑HML(FO2)是满足性可判定的,并且讨论了判定的复杂性.最后给出传值进程关于HML(FO2)的模型检测的可判定性结果.

关键词：一阶模态逻辑、可判定性、模型检测、传值进程

所属期刊栏目：33

分类号：TP3(计算技术、计算机技术)

资助基金：国家自然科学基金69833020;国家高技术研究发展计划863计划2002AA144050;国家重点基础研究发展计划973计划G1999035802;山西师范大学校科研和教改项目

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共14页

页码：97-110