Model checking cooperative multi-agent systems in BDI logic

CORC > 北京大学 > 信息科学技术学院

	Model checking cooperative multi-agent systems in BDI logic
	Chen, Qingliang ; Su, Kaile ; Wu, Lijun ; Xu, Zhaocheng
刊名	journal of information and computational science
	2012
英文摘要	Traditional temporal logics such as LTL (Linear Temporal Logic) and CTL (Computation Tree Logic) have shown tremendous success in specifying and verifying hardware and software systems. However, this kind of logic can only model the dynamic behaviors for a single system, and fall short in capturing the joint and concurrent aspects in the composition of systems, such as the interactions and coordinations of agents in Multi-agent Systems. Although ATL (Alternating-time Temporal Logic) can solve the problem to a certain extent, by preceding the temporal operators with a selective path quantifier, to specify that the interactions between entities inside the system can make sure that there is a strategy to reach a certain state, it can not formalize the rational mental attitudes of the agents such as the Belief, Desire and Intention (BDI) which plays an essential role in decision making during cooperation with other agents. This paper will investigate this problem by proposing a logic of ATLBDI (Alternating-time Temporal Logic of Belief Desire and Intention) and discuss the algorithmic issues such as model checking algorithms and the computational complexity, along with examples to show its effectiveness. We conclude that model checking for ATLBDI is completely tractable and is in PTIME-Complete, which is quite an optimistic and promising result for further applications. ? 2012 by Binary Information Press.; EI; 0; 5; 1185-1194; 9
语种	英语
内容类型	期刊论文
源URL	[http://ir.pku.edu.cn/handle/20.500.11897/294517]
专题	信息科学技术学院
推荐引用方式 GB/T 7714	Chen, Qingliang,Su, Kaile,Wu, Lijun,et al. Model checking cooperative multi-agent systems in BDI logic[J]. journal of information and computational science,2012.
APA	Chen, Qingliang,Su, Kaile,Wu, Lijun,&Xu, Zhaocheng.(2012).Model checking cooperative multi-agent systems in BDI logic.journal of information and computational science.
MLA	Chen, Qingliang,et al."Model checking cooperative multi-agent systems in BDI logic".journal of information and computational science (2012).