时态认知逻辑CTL＊K的符号化模型检查算法

计算机科学 ›› 2009, Vol. 36 ›› Issue (5): 214-219.

时态认知逻辑CTL＊K的符号化模型检查算法

陈彬王智学

解放军理工大学指挥自动化学院,南京210007

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本文受863高技术计划基金项目（2007AA012126）,国防预研基金项目（9140A06020206JB8101）资助.

CHEN Bin WANG Zhi-xue （Institute of Command Automation, PLA University of Science and Technology, Nanjing 210007, China）

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

摘要： 时序认知逻辑是由时序逻辑和认知逻辑组合而成的逻辑，主要应用于多主体系统的规范定义。大多数时序认知逻辑是基于CTL的，表达能力有限。并且已知的一些模型检查算法存在内存不足和状态爆炸等问题。讨论了基于CTL＊的时态认知逻辑CTL＊K的语法、语义和模型，它能够在表达力很强的时态逻辑CTL＊基础上描述智能体的知识、目标等意向特征。并给出了CTL＊K的模型检查算法，其核心思想就是将CTL＊K公式的检查问题转化为CTL＊公式的模型检查问题，可以使检查的系统规模得以大幅度提高。并且将算法编码后容易集成到NuSMV模型检

关键词: 符号模型检测多主体系统时态认知逻辑

Abstract: Temporal epistemic logics have been gradually used in specification of multiple agents system, which are composed by temporal logics and epistemic logics. Most of temporal epistemic logics are based on CTL, which have a limited expressivity. And some mode

Key words: Symbolic model checking, Multiple agent system, Temporal epistemic logic

陈彬王智学. 时态认知逻辑CTL＊K的符号化模型检查算法[J]. 计算机科学, 2009, 36(5): 214-219. https://doi.org/

CHEN Bin WANG Zhi-xue （Institute of Command Automation, PLA University of Science and Technology, Nanjing 210007, China）. [J]. Computer Science, 2009, 36(5): 214-219. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed