Model Checking Communicative Agent- Based Systems
H. Fujita, D. Pisanelli (eds, Jamal Bentahar, John‐Jules Ch. Meyer · 2013
Abstract. Model checking is a formal technique used to verify communication protocols against given properties. In this paper, we address the problem of verifying systems designed as a set of autonomous interacting agents using such a technique. These software agents are equipped with knowledge and beliefs and interact with each other according to protocols governed by a set of logical rules. We present a tableau-based model checking algorithm for these systems and provide the termination and complexity results.