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

关键词：三值抽象 模型检测 概率时态认知逻辑 反例 

单位：江苏大学计算机科学与通信工程学院; 镇江212013; 南京大学电子科学与工程学院; 南京210093