关键词：三值抽象；模型检测；概率时态认知逻辑；反例
摘 要：为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题,提出了概率时态认知逻辑的三值抽象技术.具体研究内容包括:定义抽象模型及模型上概率时态认知逻辑的三值语义,依据状态空间等价划分建立初始抽象模型,并证明抽象技术对概率时态认知逻辑的满足性保持关系；提出概率时态认知逻辑模型检测算法；依据初始模型检测的结果,给出利用最小证据和最小反例引导的抽象系统的求精过程.最后通过Dining Cryptographer协议说明了抽象技术的应用,及其在约简系统状态空间方面的效果.