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

来源 :江苏大学 | 被引量 : 0次 | 上传用户:yangzexv001
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
模型检测是一种很重要的有限状态系统的自动验证技术,已经应用到了通信协议、硬件检测、控制系统等领域的验证中并受到了广泛的关注。时态认知逻辑是一种属性规范描述语言,用模型检测的方法对时态认知逻辑描述的属性进行验证对确保系统的可靠性具有重要的意义。在时态认知逻辑中加入概率因素可得到概率时态认知逻辑,时态认知逻辑与实时因素结合可得到实时时态认知逻辑。   与传统模型检测一样,概率时态认知逻辑和实时时态认知逻辑模型检测也面临着状态空间爆炸问题。在为缓解状态空间爆炸问题所提出的诸多理论和方法中,抽象技术是克服状态空间爆炸问题的最为有效的方法之一。本文对概率和实时时态认知逻辑模型检测中的抽象技术进行了系统的研究,有效的缓解了状态空间爆炸问题。   本文的主要研究内容包括:   1.为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题,提出了三值抽象技术。建立了概率Kripke结构的抽象模型,它的主要特点是利用概率转换区间替换了原始模型中的概率转换。证明了由抽象技术演绎得到的抽象模型既是原始模型的上近似,又是它的下近似。开发了在抽象状态空间上检测概率时态认知逻辑属性的算法。为了确保抽象技术的完备性,给出了最小证据和最小反例引导的抽象系统求精的算法。最后通过Dining Cryptographer协议来说明抽象技术在约简系统状态空间方面的效果。   2.为解决实时时态认知逻辑模型检测中的状态空间爆炸问题,提出了一种二值抽象技术:对于实时时态认知逻辑TACTLK中的实时部分TACTL,采用抽象离散时钟赋值;对于TACTLK中的认知算子K,提出了抽象状态关于智体认知等价的定义。建立了实时解释系统的抽象模型,并证明了由抽象技术演绎得到的抽象模型是原始模型的上近似。最后,通过对铁路道口系统的状态空间的简化来说明抽象技术的有效性。   3.由于在二值抽象技术下,由抽象技术演绎得到的抽象模型只是原始模型的上近似。若待验证的属性在抽象模型中不成立,不能推出该属性在原始模型中也是不成立的。三值抽象技术可有效克服这一不足,将上面的二值抽象推广到了三值抽象。建立了实时解释系统的三值抽象模型,提出了抽象模型上实时时态认知逻辑的三值语义,并证明了抽象技术对实时时态认知逻辑公式满足性的保持关系。最后通过对标准铁路道口系统和主动结构控制系统这两个实例来说明三值抽象技术的有效性。
其他文献
运动目标的检测和跟踪作为数字图像处理和计算机视觉领域的热点,在自动导航、交通监控、国防军工等领域都具有十分高的应用价值。过去几十年,众多研究者在目标检测和跟踪领域
从上世纪70年代以来,我国的经济得到了迅速的发展,对能源的需求也成倍的增长,国家和地方政府都积极的在矿井建设上投入了大批的资金,以满足国民对能源的需求。而矿井建设是一
近年来,网络编码技术得到了飞速的发展,研究已表明,网络编码技术能够为无线网络带来更高的吞吐率、可靠性和鲁棒性。网络编码的最大优点是使组播传输速率达到最大流最小割定
车牌检测与识别技术是智能交通系统的重要环节,在交通监管、交通控制和车辆管理等方面发挥了重要的作用。在低照度图像中,车牌等重要信息不明显,难以直接进行检测和识别。针对这
Web Service是建立可互操作的分布式应用程序的新平台,引入了一种全新的Web应用开发、部署和集成的模式。由于WebService通常包含应用系统关键的业务,若其安全性出现问题可能
随着计算机网络的发展与普及,包交换网络中的IP隐通道逐渐成为近期的研究热点。根据信息隐藏的方式,可将IP隐通道分为IP存储隐通道和IP时间隐通道。IP存储隐通道利用数据包的
人体姿态估计是计算机视觉领域中一个关键问题,可以应用于人体活动分析,人机交互以及视频监视等方面,其主要是指从图像中检测出人体各部件位置以及方向和尺度信息。人体姿态估计
无线传感器网络(Wireless Senor Network,WSN)依据其低成本、低能耗、自组织、高容错等优点在军事国防、环境监测以及商业应用等领域具有广阔的应用前景。它集成了传感器技术
直升机对输电线路进行巡检,具有高效、可靠、快捷、成本低、不受地域影响等优点,现已成为我国输电线路巡检的一种重要方式。“直升机巡视为主,人工巡视为辅”是我国高压、超
在传统的单服务器认证方案中,如果用户想通过访问不同种类的服务器的方式来满足自己所需要访问的网络服务,用户需要分别注册他所需要访问的所有网络服务,这个操作过程对于用