面向传值进程的一阶模态逻辑的可判定性与模型检测 |
| |
引用本文: | 薛锐,林惠民.面向传值进程的一阶模态逻辑的可判定性与模型检测[J].中国科学(E辑),2003,33(2):97-110. |
| |
作者姓名: | 薛锐 林惠民 |
| |
作者单位: | 1. 中国科学院软件研究所计算机开放实验室,北京,100080 2. 中国科学院软件研究所信息安全国家重点实验室,北京,100080 |
| |
基金项目: | 国家自然科学基金(批准号:69833020),国家高技术研究发展计划(863计划,2002AA144050),国家“九七三”重点研究发展规划(G1999035802),山西师范大学山西省归国留学生基金资助项目 |
| |
摘 要: | 对于面向传值进程的Hennessy-Milner逻辑的一阶扩充HML(FO), 给出了基于带赋值的符号迁移图的语义解释. 证明了HML(FO)的子逻辑HML(FO2)是满足性可判定的, 并且讨论了判定的复杂性. 最后给出传值进程关于HML(FO2)的模型检测的可判定性结果.
|
关 键 词: | 可判定性 模型检测 传值进程 一阶模态逻辑 |
收稿时间: | 2001-06-13 |
修稿时间: | 2002-06-07 |
本文献已被 CNKI 维普 万方数据 等数据库收录! |
| 点击此处可从《中国科学(E辑)》浏览原始摘要信息 |
| 点击此处可从《中国科学(E辑)》下载免费的PDF全文 |
|