A verification framework for agent communication
In this paper, we introduce a veri. cation method for the correctness of multiagent systems as described in the framework of ACPL (Agent Communication Programming Language). The computational model of ACPL consists of an integration of the two different paradigms of CCP (Concurrent Constraint Programming) and SCP (Communicating Sequential Processes). The constraint programming techniques are used to represent and process information, whereas the communication mechanism of ACPL is described in terms of the synchronous handshaking mechanism of CSP. Consequently, we show how to de. ne a veri. cation method for ACPL in terms of an integration of the veri. cation methods for CCP and CSP. We prove formally the soundness of the method and discuss its completeness.
agent communication semantics verification methods specification agent communication language multi-agent systems