Verifying multi-agent programs by model checking

被引：94
作者：
Bordini, RH [1 ]
Fisher, M
Visser, W
Wooldridge, M
机构：
[1] Univ Durham, Durham DH1 3HP, England
[2] Univ Liverpool, Liverpool L69 3BX, Merseyside, England
[3] NASA, Ames Res Ctr, RIACS, Moffett Field, CA 94035 USA
来源：
AUTONOMOUS AGENTS AND MULTI-AGENT SYSTEMS | 2006年 / 12卷 / 02期
关键词：
agent-oriented programming; AgentSpeak; model checking; spin; JPF;
D O I：
10.1007/s10458-006-5955-7
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
This paper gives an overview of our recent work on an approach to verifying multi-agent programs. We automatically translate multi-agent systems programmed in the logic-based agent-oriented programming language AgentSpeak into either Promela or Java, and then use the associated Spin and JPF model checkers to verify the resulting systems. We also describe the simplified BDI logical language that is used to write the properties we want the systems to satisfy. The approach is illustrated by means of a simple case study.
引用
收藏
页码：239 / 256
页数：18
相关论文
共 36 条
[1]  
BENERECETTI M, P MOD CHECK ART INT, P1
[2]  
BIESIADECKI J, 2001, 6 INT S AI ROB AUT S
[3]  
Bordini R.H., 2004, LNCS LNAI, V3067, P72, DOI [10.1007/978-3- 540- 25936-7 4, DOI 10.1007/978-3-540-25936-74]
[4]  
Bordini RafaelH., 2003, AAMAS 03, P409
[5]   Proving BDI properties of agent-oriented programming languages - The asymmetry thesis principles in AgentSpeak(L) [J].
Bordini, RH ;
Moreira, AF .
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2004, 42 (1-3) :197-226
[6]   Model checking rational agents [J].
Bordini, RH ;
Fisher, M ;
Wooldridge, M ;
Visser, W .
IEEE INTELLIGENT SYSTEMS, 2004, 19 (05) :46-52
[7]  
Bordini RH, 2003, LECT NOTES COMPUT SC, V2725, P110
[8]  
BORDINI RH, 2005, MULTIAGENT PROGRAMMI, pCH1
[9]  
BORDINI RH, 2004, P 3 INT JOINT C AUT, P896
[10]  
Clarke E, 2001, Model checking
1234