Sixth Asia-Pacific Software Engineering Conference (APSEC'99)
Analysis and Verification of Multi-Agent Interaction Protocols
Takamatsu, Japan
December 07-December 10
ISBN: 0-7695-0509-0
This paper describes our initial study on analysis and verification of agent interaction protocols using model checking. We use the symbolic model checker SMV to analyze and verify two examples of agent interaction protocols. We show that proofs obtained using belief logic and theorem proving for a simple provider- consumer multi-agent system can be trivially proven using model checking method. Furthermore, the verification results identify inadequacies in the original proof. A study on a more complex multi-agent interaction protocol is also presented with discussion on how model checking can complement specification based verification methods.