Abstract: Model checking has being used mainly to check if a system satisfies the specifications expressed in temporal logic. People pay little attention to the model checking problem for multi-agent logics of knowledge. However, in the distributed systems community, the desirable specifications of systems and protocols have been expressed widely in logics of knowledge. A Web service is an abstract notion that must be implemented by a concrete agent. hhe agent is the conCrete piece of software or hardware that sends and receives messages. hhus a Web services composition can be viewed as a multi-agent system We applied our model checker MCTK for temporal logic of knowledge to verified the Web services example of the SAS protocol. We also verified the example with three model checkers WSAh, W}Enginecr and SPIN. The experimental results show that the performance of our model checking method for verifying Web services is higher than these three model checkers.

Key words: Model checking, Temporal logics of knowledge, Multi-agent system, Web service