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

• 作 者: 刘志锋 孙博 周从华
• 机 构: 江苏大学计算机科学与通信工程学院
• 出 处: 电子学报
• 发表日期: 2013年7期
• 关键词: 模型检测 概率实时时态认知逻辑 PTACTLK 状态空间爆炸 抽象 model checking probabilistic real-time tempor
• 基金项目: 国家自然科学基金（No.61003288,No.6111130184）, 江苏省自然科学基金（No.BK2010192）, 教育部博士点基金（No.20093227110005）, 江苏大学高级人才科研启动基金（No.12JDG061）

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