论文部分内容阅读
Clarke和McMillan提出了利用mu演算和OBDDs符号模型检测时态逻辑的方法,这些方法是非常有效的，能用于验证许多具有极大状态空间的实际系统（状态个数可以超过10^20）．但是，这些方法不能检测知识逻辑．而时态认知逻辑能更精确地描述分布式领域中系统和协议的规范．文章首先讨论了Kripke结构和mu演算的扩展，然后提出了利用扩展mu演算和OBDDs符号模型检测时态认知逻辑的方法。