面向传值进程的一阶模态逻辑的可判定性与模型检测
| Data(s) |
2003
|
|---|---|
| Resumo |
对于面向传值进程的Hennesssy-Milner逻辑的一阶扩充HML(FO)，给出了基于带赋值的符号迁移图的语义解释。证明了HML(FO)的子逻辑HML(FO^2)是满足性可判定的，并且讨论了判定的复杂性。最后给出了传值进程关于HML(FO^2)的模型检测的可判定性结果。 National Natural Science Foundation of China; Public Administration and Civil Service Bureau of Macau SAR; Companhia de Telecomunicacoes de Macau S.A.R.L.; Macau SAR Government Tourist Office |
| Identificador | |
| Idioma(s) |
中文 |
| Fonte |
薛锐; 林惠民.面向传值进程的一阶模态逻辑的可判定性与模型检测,中国科学E辑,2003,33(2):97-110 |
| Palavras-Chave | #一阶模态逻辑 #可判定性 #模型检测 #传值进程 |
| Tipo |
期刊论文 |
