Title :
Model Checking Multi-agent Systems
Author :
Mengting, Yuan ; Chao, Yu
Author_Institution :
Wuhan Univ., Wuhan
Abstract :
In this paper, we consider a multi-agent system as a set of interacting objects. A model of object oriented automata, MOOA, is used to specify multi-agent systems. Under the framework of MOOA, each agent is modeled as an object oriented automaton. The formal syntax and semantics of MOOA are given in this paper. We first extend the PLTL logic so as to describe the dynamic properties of agents, then provide a model checking algorithm base on automata theory to verify the behaviors of MOOA model.
Keywords :
automata theory; multi-agent systems; object-oriented methods; automata theory; interacting objects; model checking; multiagent systems; object oriented automata; oriented formal syntax; Automata; Chaos; Computer science; Logic; Multiagent systems; Object oriented modeling; Tree data structures; Unified modeling language; Agent; Formal Method; Model Checking;
Conference_Titel :
Service Systems and Service Management, 2007 International Conference on
Conference_Location :
Chengdu
Print_ISBN :
1-4244-0885-7
Electronic_ISBN :
1-4244-0885-7
DOI :
10.1109/ICSSSM.2007.4280183
