A modeling and verification method to multi-agent systems based on KQML

Author

Xiangyu Luo ; Mengmeng Zou ; Lingjie Luo

Author_Institution

Coll. of Comput. Sci. & Technol., Huaqiao Univ., Xiamen, China

fYear

2012

fDate

24-27 June 2012

Firstpage

690

Lastpage

693

Abstract

The Knowledge Query Manipulation Language (KQML) has become a de-facto standard of agent communication languages. To be able to guarantee the correctness and reliability of a KQML code, in this paper we propose an intermediate formal model transition seven-tuple for modeling KQML, develop a modeling approach for converting the KQML language to the input language ISPL of the model checker MCMAS for multi-agent systems, which enable us to verify temporal and epistemic properties. The validity of the proposed verification approach is demonstrated by a case study of train-controller system.

Keywords

formal verification; knowledge representation languages; multi-agent systems; query languages; railway engineering; software agents; software reliability; ISPL; KQML code correctness; KQML code reliability; KQML modeling; MCMAS; agent communication languages; de-facto standard; epistemic properties; formal model transition; knowledge query manipulation language; model checker; modeling method; multiagent systems; temporal properties; train-controller system; verification method; Indium phosphide; Lead; Multiagent systems; Protocols; KQML; MCMAS; model checking; multi-agent systems;

fLanguage

English

Publisher

ieee

Conference_Titel

Electrical & Electronics Engineering (EEESYM), 2012 IEEE Symposium on

Conference_Location

Kuala Lumpur

Print_ISBN

978-1-4673-2363-5

Type

conf

DOI

10.1109/EEESym.2012.6258753

Filename

6258753