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

• 作者: 刘志锋 周从华 孙博
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 模型检测 概率实时时态认知逻辑 PTACTLK 状态空间爆炸 抽象
• 年，卷（期）: 2013,（7）
• 所属期刊栏目: 学术论文
• 页码范围: 1343-1351
• 页数: 9页
• 分类号: TP301
• 字数: 12646字
• 语种: 中文
• DOI: 10.3969/j.issn.0372-2112.2013.07.016

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	孙博	江苏大学计算机科学与通信工程学院	2	5	1.0	2.0
2	周从华	江苏大学计算机科学与通信工程学院	46	193	7.0	11.0
3	刘志锋	江苏大学计算机科学与通信工程学院	29	118	5.0	10.0