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