多智能体协同的认知规范模型检测算法  

Model Checking Algorithms for Epistemic Goals in Cooperative Multi-Agent Systems

作　　者：陈清亮[1] 朱可宜[1] 

机构地区：[1]暨南大学计算机科学系,广东广州510632

出　　处：《中山大学学报（自然科学版）》2009年第1期110-112,共3页Acta Scientiarum Naturalium Universitatis Sunyatseni

基　　金：国家重点基础研究发展规划项目973资助项目(2005CB321902);暨南大学引进人才基金资助项目

摘　　要：在Wooldridge提出的利用不变式特征的方法来模型检测时态认知逻辑的基础上,研究多智能体协同逻辑ATEL(Alternating Temporal Epistemic Logic)中认知算子的模型检测算法,包括多层的认知算子,分布式认知算子和公共知识算子等等。研究结果表明,加入认知算子后的ATEL的在增加系统描述能力的同时并没有明显增加其计算复杂性。The model of checking algorithms was studied for epistemic specifications in ATEL （ Alternating Temporal Epistemic Logic） for multi-agent systems, including nested knowledge modalities, distributed knowledge and common knowledge modalities, based on the invariant property checking approach proposed by Wooldridge. The results showed that ATEL maintains a good balance between the expressive power and computational complexity.

关 键 词：时态逻辑 认知逻辑 模型检测 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]