A flexible framework for verifying agent programs

ABSTRACT

There is an increasing number of agent-oriented programming languages that have working interpreters and platforms, with significant progress in the quality of such platforms over the last few years. With these platforms becoming more popular, and multi-agent systems being increasingly used for safety-critical applications, the need for verification techniques that apply to systems written in such languages is proportionally intensified. Building on our previous work on model checking for a particular agent-oriented programming language, we have developed a new approach whereby model checking techniques can be used directly on a variety of such languages. The approach also supports the verification of multi-agent systems where individual agents have been programmed in different agent languages.

REFERENCES

• 1: Rafael H. Bordini , Michael Fisher , Willem Visser , Michael Wooldridge, Model Checking Rational Agents, IEEE Intelligent Systems, v.19 n.5, p.46-52, September 2004 [doi>10.1109/MIS.2004.47]
• 2: Rafael H. Bordini , Michael Fisher , Willem Visser , Michael Wooldridge, State-Space Reduction Techniques in Agent Verification, Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, p.896-903, July 19-23, 2004, New York, New York [doi>10.1109/AAMAS.2004.252]
• 3: Rafael H. Bordini , Michael Fisher , Willem Visser , Michael Wooldridge, Verifying Multi-agent Programs by Model Checking, Autonomous Agents and Multi-Agent Systems, v.12 n.2, p.239-256, March 2006 [doi>10.1007/s10458-006-5955-7]
• 4: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 5: L. A. Dennis, B. Farwer, R. H. Bordini, M. Fisher, and M. Wooldridge. A Common Semantic Basis for BDI Languages. In Proc. 7th Int. Workshop on Programming Multiagent Systems (ProMAS), 2007.
• 6: Michael Fisher, Temporal Development Methods for Agent-Based, Autonomous Agents and Multi-Agent Systems, v.10 n.1, p.41-66, January 2005 [doi>10.1007/s10458-004-3140-4]
• 7: John Hatcliff , Matthew B. Dwyer, Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software, Proceedings of the 12th International Conference on Concurrency Theory, p.39-58, August 20-25, 2001
• 8: A. Hepple, L. A. Dennis, and M. Fisher. A Common Basis for Agent Organisations in BDI Languages. In Proc. Int. Workshop on LAnguages, methodologies and Development tools for multi-agent systemS (LADS), 2007.
• 9: Gerard Holzmann, Spin model checker, the: primer and reference manual, Addison-Wesley Professional, 2003
• 10: http://javapathfinder.sourceforge.net.
• 11: Magdalena Kacprzak , Alessio Lomuscio , Wojciech Penczek, Verification of Multiagent Systems via Unbounded Model Checking, Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, p.638-645, July 19-23, 2004, New York, New York [doi>10.1109/AAMAS.2004.296]
• 12: F. Raimondi and A. Lomuscio. Automatic Verification of Multi-agent Systems by Model Checking Ordered Binary Decision Diagrams. J. Applied Logic, 5(2):235--251, 2007.
• 13: Anand S. Rao, AgentSpeak(L): BDI agents speak out in a logical computable language, Proceedings of the 7th European workshop on Modelling autonomous agents in a multi-agent world : agents breaking away: agents breaking away, p.42-55, February 1996, Einhoven, The Netherlands
• 14: Robby , Matthew B. Dwyer , John Hatcliff, Bogor: an extensible and highly-modular software model checking framework, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 15: Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]
• 16: M. Wooldridge, M. Fisher, M.-P. Huget, and S. Parsons. Model Checking for Multiagent Systems: The MABLE Language and its Applications. Int. J. Artificial Intelligence Tools, 15(2):195--225, 2006.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence
            Subjects: Multiagent systems

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.5 Programming Languages and Software

General Terms:
Languages, Verification

Keywords:
BDI agents, Java pathfinder, agent-oriented programming languages, model checking, verification