基于空间逻辑和计算树逻辑的模型检测

摘要

模型检测是一种很重要的自动验证技术.在已有的对移动进程演算的研究中,用于刻画移动环境演算系统性质大多使用的是空间逻辑,而时序逻辑作为形式化方法中一个十分重要的应用分支当然也可用于刻画移动环境演算系统的性质.本文采用空间逻辑与时序逻辑中的计算树逻辑等知识,研讨了移动环境演算的模型检测问题.本文把空间逻辑和CTL结合起来，提出了一个适用于Mobile Ambients检测有穷状态进程的模型检测算法。下一步的工作将研究算法的复杂性以及不同模态算子的可判定性和有限控制Ambients等问题。另外，MA演算系统有各种变形(比如安全的Ambients系统SA、盒子Ambients系统BA等)有着丰富的表达能力，它们的模型检测问题可以作为进一步研究的方向。