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

作　　者：薛锐[1] 林惠民[2] 

机构地区：[1]中国科学院软件研究所计算机开放实验室,北京100080 [2]中国科学院软件研究所信息安全国家重点实验室,北京100080

出　　处：《中国科学（E辑）》2003年第2期97-110,共14页Science in China(Series E)

基　　金：国家自然科学基金(批准号:69833020);国家高技术研究发展计划(863计划;2002AA144050);国家"九七三"重点研究发展规划(G1999035802);山西师范大学山西省归国留学生基金资助项目

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

关 键 词：一阶模态逻辑 可判定性 模型检测 传值进程 Hennessy-Milner逻辑 符号迁移图 

分 类 号：O142[理学—数学]