电子学报 ›› 2013, Vol. 41 ›› Issue (7): 1343-1351.DOI: 10.3969/j.issn.0372-2112.2013.07.016

• 学术论文 • 上一篇    下一篇

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

刘志锋, 孙博, 周从华   

  1. 江苏大学计算机科学与通信工程学院, 江苏镇江 212013
  • 收稿日期:2012-09-27 修回日期:2012-12-03 出版日期:2013-07-25 发布日期:2013-07-25
  • 作者简介:刘志锋 男,1981年生,江苏无锡人.2011年在南京大学获得博士学位,现为江苏大学计算机科学与通信工程学院讲师.主要研究方向为模型检测,形式化方法,模态逻辑.E-mail:liuzf@ujs.edu.cn
  • 基金资助:

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

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

LIU Zhi-feng, SUN Bo, ZHOU Cong-hua   

  1. School of Computer Science and Telecommunication Engineering, Jiangsu University, Jiangsu, Zhenjiang 212013, China
  • Received:2012-09-27 Revised:2012-12-03 Online:2013-07-25 Published:2013-07-25

摘要: 概率实时时态认知逻辑PTACTLK模型检测面临着与传统模型检测同样的挑战,即状态空间爆炸问题.抽象是缓解状态空间爆炸问题的最为有效的方法之一.为了缓解概率实时时态认知逻辑模型检测中的状态空间爆炸问题,我们给出了一种抽象技术:对于PTACTLK中的实时部分PTACTL,采用抽象离散时钟赋值,把概率实时解释系统的无限状态空间转化成有限形式;对于PTACTLK中的认知算子K,给出了抽象状态关于智体认知等价的定义.定义了概率实时解释系统的抽象模型,给出了抽象模型上概率实时时态认知逻辑的语义,并证明了由抽象技术演绎得到的抽象模型是原始模型的上近似.最后通过一个通信协议来说明抽象技术的有效性.

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

Abstract: 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.

Key words: model checking, probabilistic real-time temporal logic of knowledge, PTACTLK, state space explosion, abstraction

中图分类号: