Automated verification of multi-agent programs

Berndt Muller, M. Fisher, R.H. Bordini, L.A. Dennis

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


In this paper, we show that the flexible model-checking of multi-agent systems, implemented using agent-oriented programming languages, is viable thus paving the way for the construction of verifiably correct applications of autonomous agents and multi-agent systems. Model checking experiments were carried out on AJPF (agent JPF), our extension of Java PathFinder that incorporates the agent infrastructure layer, our unifying framework for agent programming languages. In our approach, properties are specified in a temporal language extended with (shallow) agent-related modalities. The framework then allows the verification of programs written in a variety of agent programming languages, thus removing the need for individual languages to implement their own verification framework. It even allows the verification of multi-agent systems comprised of agents developed in a variety of different (agent) programming languages. As an example, we also provide model checking results for the verification of a multi-agent system implementing a well-known task sharing protocol.
Original languageEnglish
Title of host publicationN/A
Publication statusPublished - 1 Oct 2008
Event 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008) - Italy
Duration: 15 Sept 200819 Sept 2008


Conference 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008)


  • ai
  • multi-agent systems
  • verification
  • model checking


Dive into the research topics of 'Automated verification of multi-agent programs'. Together they form a unique fingerprint.

Cite this