概率和实时时态认知逻辑模型检测中的抽象技术

摘要

模型检测是一种很重要的有限状态系统的自动验证技术,已经应用到了通信协议、硬件检测、控制系统等领域的验证中并受到了广泛的关注。时态认知逻辑是一种属性规范描述语言,用模型检测的方法对时态认知逻辑描述的属性进行验证对确保系统的可靠性具有重要的意义。在时态认知逻辑中加入概率因素可得到概率时态认知逻辑,时态认知逻辑与实时因素结合可得到实时时态认知逻辑。
　　 与传统模型检测一样,概率时态认知逻辑和实时时态认知逻辑模型检测也面临着状态空间爆炸问题。在为缓解状态空间爆炸问题所提出的诸多理论和方法中,抽象技术是克服状态空间爆炸问题的最为有效的方法之一。本文对概率和实时时态认知逻辑模型检测中的抽象技术进行了系统的研究,有效的缓解了状态空间爆炸问题。
　　 本文的主要研究内容包括:
　　 1.为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题,提出了三值抽象技术。建立了概率Kripke结构的抽象模型,它的主要特点是利用概率转换区间替换了原始模型中的概率转换。证明了由抽象技术演绎得到的抽象模型既是原始模型的上近似,又是它的下近似。开发了在抽象状态空间上检测概率时态认知逻辑属性的算法。为了确保抽象技术的完备性,给出了最小证据和最小反例引导的抽象系统求精的算法。最后通过Dining Cryptographer协议来说明抽象技术在约简系统状态空间方面的效果。
　　 2.为解决实时时态认知逻辑模型检测中的状态空间爆炸问题,提出了一种二值抽象技术:对于实时时态认知逻辑TACTLK中的实时部分TACTL,采用抽象离散时钟赋值;对于TACTLK中的认知算子K,提出了抽象状态关于智体认知等价的定义。建立了实时解释系统的抽象模型,并证明了由抽象技术演绎得到的抽象模型是原始模型的上近似。最后,通过对铁路道口系统的状态空间的简化来说明抽象技术的有效性。
　　 3.由于在二值抽象技术下,由抽象技术演绎得到的抽象模型只是原始模型的上近似。若待验证的属性在抽象模型中不成立,不能推出该属性在原始模型中也是不成立的。三值抽象技术可有效克服这一不足,将上面的二值抽象推广到了三值抽象。建立了实时解释系统的三值抽象模型,提出了抽象模型上实时时态认知逻辑的三值语义,并证明了抽象技术对实时时态认知逻辑公式满足性的保持关系。最后通过对标准铁路道口系统和主动结构控制系统这两个实例来说明三值抽象技术的有效性。