Analysis and verification of multi-agent interaction protocols

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 the 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