Model checking agent programs by using the program interpreter

Sung Shik T.Q. Jongmans, Koen V. Hindriks, M. Birna Van Riemsdijk

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review


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.

Original languageEnglish
Title of host publicationComputational Logic in Multi-Agent Systems - 11th International Workshop, CLIMA XI, Proceedings
Number of pages19
Publication statusPublished - 17 Sep 2010
Externally publishedYes
Event11th International Workshop on Computational Logic in Multi-Agent Systems, CLIMA XI - Lisbon, Portugal
Duration: 16 Aug 201017 Aug 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6245 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference11th International Workshop on Computational Logic in Multi-Agent Systems, CLIMA XI


Dive into the research topics of 'Model checking agent programs by using the program interpreter'. Together they form a unique fingerprint.

Cite this