| 面向传值进程的一阶模态逻辑的可判定性与模型检测 |
| |
| 引用本文： | 薛锐,林惠民.面向传值进程的一阶模态逻辑的可判定性与模型检测[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全文 |
|
