Model checking agent programs by using the program interpreter

Model checking agent programs is a challenge and it is still a question which approaches can suitably be applied to effectively model check such programs. We present a new approach to explicit-state, on-the-fly model checking for agent programs. In this approach we use the agent program interpreter for generating the state space. A model checker is built on top of this interpreter by implementing efficient transformations of temporal properties to Büchi automata and an efficient bookkeeping mechanism that maintains track of states that have been visited. The proposed approach is generic and can be applied to different agent programming frameworks. We evaluate this approach to model checking by comparing it empirically with an approach based on the Maude model checker, and one based on the Agent Infrastructure Layer (AIL) intermediate language in combination with JPF. It turns out that although our approach does not use state-space reduction techniques, it shows significantly improved performance over these approaches. To the best of our knowledge, no such comparisons of approaches to model checking agent programs have been done before.