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

Abstraction in Model Checking Probabilistic Real-Time Temporal Logic of Knowledge

作　　者：刘志锋[1] 孙博[1] 周从华[1] 

机构地区：[1]江苏大学计算机科学与通信工程学院,江苏镇江212013

出　　处：《电子学报》2013年第7期1343-1351,共9页Acta Electronica Sinica

基　　金：国家自然科学基金(No.61003288;No.6111130184);江苏省自然科学基金(No.BK2010192);教育部博士点基金(No.20093227110005);江苏大学高级人才科研启动基金(No.12JDG061)

摘　　要：概率实时时态认知逻辑PTACTLK模型检测面临着与传统模型检测同样的挑战,即状态空间爆炸问题.抽象是缓解状态空间爆炸问题的最为有效的方法之一.为了缓解概率实时时态认知逻辑模型检测中的状态空间爆炸问题,我们给出了一种抽象技术:对于PTACTLK中的实时部分PTACTL,采用抽象离散时钟赋值,把概率实时解释系统的无限状态空间转化成有限形式;对于PTACTLK中的认知算子K,给出了抽象状态关于智体认知等价的定义.定义了概率实时解释系统的抽象模型,给出了抽象模型上概率实时时态认知逻辑的语义,并证明了由抽象技术演绎得到的抽象模型是原始模型的上近似.最后通过一个通信协议来说明抽象技术的有效性.The same challengs facing model checkings in probabilistic real-time temporal logic of knowledge PTACTLK is the same as traditional model one.That is the state space explosion problem.Abstraction is one of the most effective methods to alleviate the state space explosion problem.In order to alleviate the problem of the state space explosion in model checking probabilistic real-time temporal logic of knowledge,an Abstraction technique is presented.For the real time part of PTACTLK,that is PTACTL,we adopt the Abstract discrete clock valuations,and the infinite state space of a probabilistic real time was interpreted into a finite form.For the epistemic operator K in PTACTLK,the definition of epistemic equivalent to an agent between Abstract states is given.We define the Abstract model of the interpreted system in a probabilistic real time and present the semantics of PTACTLK on the Abstract model.We prove that the Abstract model obtained by using the Abstraction techniques is the upper approximation of the original model.At last,a simple communication protocol is adopted to illustrate the effectiveness of our Abstraction techniques.

关 键 词：模型检测 概率实时时态认知逻辑 PTACTLK 状态空间爆炸 抽象 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]