MCAPL:Model Checking Agent Programming Languages

Contents 1 Overview 1.1 Investigators 1.2 Researchers 1.3 Associated PhD Students 1.4 Aims 1.5 Project Details 2 Outputs Produced 2.1 Publications 2.2 Software 3 Relevant Links

Overview

The "Model Checking Agent Programming Languages" project was an EPSRC-funded collaboration between the Universities of Durham and Liverpool in the UK. Specifically, the people involved are:

Investigators

• Rafael H. Bordini, University of Durham, UK. [Principal Investigator at Durham]
• Michael Fisher, University of Liverpool, UK. [Principal Investigator at Liverpool]
• Michael Wooldridge, University of Liverpool, UK

Researchers

• Louise Dennis, University of Liverpool, UK. [Post-doctoral Researcher at Liverpool]
• Berndt Farwer, University of Durham, UK. [Post-doctoral Researcher at Durham]
• Matt Webster, University of Liverpool, UK. [Post-doctoral Researcher at Liverpool]

Associated PhD Students

• Anthony Hepple, University of Liverpool, UK.

Aims

Our overall goal in this project is to develop model checking techniques that can be applied to various agent-oriented programming languages. Building on our previous work on model checking for AgentSpeak [2, 3, 1, 4, 5] we will investigate the key aspects underlying not only AgentSpeak but other agent-oriented programming languages based on Java, such as 3APL [6], Concurrent MetateM, and Jadex. Based on that, we will provide a Java infrastructure layer that is (a) relevant to the implementation of these agent languages (b) has clear semantics, and (c) is able to be verified through an extended version of JPF, an open source Java model checker [7].

As a result of this investigation, we will be able to develop both formal semantics for these major constructs of agent programming as well as Java libraries that implement them (based on the semantics) - the resulting intermediate agent language will be called the Agent Infrastructure Layer (AIL). As in our existing body of work, JPF is to be used as the model checker with which to carry out formal verification of implemented agent-based systems. The idea is then to provide automatic (and provably correct) translations from various existing agent-oriented programming languages.

1. R. H. Bordini, M. Fisher, W. Visser, and M. Wooldridge. Verifiable multi-agent programs. In Proceedings of the First International Workshop on Programming Multiagent Systems: languages, frameworks, techniques and tools (ProMAS-03), held with AAMAS-03, 15 July, 2003, Melbourne, Australia. Volume 3067 of Lecture Notes in Artificial Intelligence, Springer Verlag.
2. R. H. Bordini, M. Fisher, W. Visser, and M. Wooldridge. Model Checking Rational Agents. IEEE Intelligent Systems 19(5):46-52, September/October 2004.
3. R. H. Bordini, M. Fisher, W. Visser, and M. Wooldridge. State-Space Reduction Techniques in Agent Verification. In Proceedings of the Third International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS-2004), New York, USA. ACM Press.
4. R. H. Bordini, W. Visser, M. Fisher, C. Pardavila, and M. Wooldridge. Model Checking Multi-Agent Programs with CASP. In Proceedings of the Fifteenth Conference on Computer-Aided Verification (CAV-2003). Tool description. Volume 2725 in LNCS, pages 110-113, Berlin, 2003. Springer-Verlag.
5. R. H. Bordini, M. Fisher, W. Visser, and M. Wooldridge. Verifying Multi-Agent Programs by Model Checking. Journal of Autonomous Agents and Multi-Agent Systems 12(2):239-256, March 2006.
6. W. Visser, K. Havelund, G. Brat, and S. Park. Model checking programs. In Proc. 15th Int. Conf. on Automated Software Engineering (ASE'00), pages 3-12. IEEE Computer Society, 2000.
7. M. Dastani, B. van Riemsdijk, F. Dignum, and J.-J. C. Meyer. A programming language for cognitive agents: Goal directed 3APL. In Proc. 1st Int. Workshop on Programming Multiagent Systems: languages, frameworks, techniques and tools (ProMAS-03), held with AAMAS-03, 2003.

Project Details

• Project duration: 30 months
• Expected start date: 1st September 2006
• EPSRC grant references
  • Durham - EP/D054788/1
  • Liverpool - EP/D052548/1

Outputs Produced

Publications

• Agent Infrastructure Layer (AIL): Design and Operational Semantics. L. A. Dennis. Technical Report ULCS-07-001, University of Liverpool, 2007.
• A Common Semantic Basis for BDI Languages. L. A. Dennis, R. H. Bordini, B. Farwer, M. Fisher and M. Wooldridge. In Proc. Fifth International Workshop on Programming in Multi-Agent Systems (ProMAS'07), 2007.
• Translating into an intermediate agent layer: A prototype in Maude. B. Farwer and L. A. Dennis. In Proc. Workshop on Concurrency, Specification and Programming (CS&P'07), 2007.
• A Common Basis for Agent Organisation in BDI Languages. A. Hepple, L. A. Dennis and M. Fisher. To appear in Proc. 1st International Workshop on LAnguages, methodologies and Development tools for multi-agent systemS (LADS'007), 2007.
• Foundations of Flexible Multi-Agent Programming. L. A. Dennis, M. Fisher and A. Hepple. To appear in Proc. 8th Workshop on Computational Logic in Multi-Agent Systems (CLIMA-VIII), 2007.
• A Flexible Framework for Verifying Agent Programs. L. A. Dennis, B. Farwer, R. H. Bordini, and M. Fisher. In Proc. 7th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), 2008. (Short paper)
• Programming Verifiable Heterogeneous Agent Systems. L. A. Dennis and M. Fisher. In Proc. Sixth International Workshop on Programming in Multi-Agent Systems (ProMAS), 2008.
• Gwendolen: A BDI Language for Verifiable Agents. L. A. Dennis and B. Farwer. In Logic and the Simulation of Interaction and Reasoning, 2008.
• Model-Checking Auctions, Coalitions and Trust M. Webster, L. A. Dennis and M. Fisher. Technical Report ULCS-09-004, University of Liverpool, 2009.
• Automated Verification of Multi-Agent Programs. R. H. Bordini, L. A. Dennis, B. Farwer and M. Fisher. In Automated Software Engineering (ASE 2008), 2008. IEEE.
• Model Checking Normative Agent Organisations. L. A. Dennis, N. Tinnemeier and J.-J. Meyer. Proc. 10th Workshop on Computational Logic in Multi-Agent Systems (CLIMA-X), Jürgen Dix, Michael Fisher and Peter Novák (eds), pp. 64-82. LNCS 6214. Springer, 2009.
• Directions for Agent Model Checking. R. H. Bordini, L. A. Dennis, B. Farwer and M. Fisher. Chapter 4 in Specification and Verification of Multi-agent Systems by M. Dastani, K. Hindriks and J.-J. Meyer (eds). Springer, 2010.
• Model checking agent programming languages, Louise A. Dennis, Michael Fisher, Matthew P. Webster and Rafael H. Bordini, Automated Software Engineering, 2011.

Software

The software (with documentation) created by the project is available from our SourceForge Project

Relevant Links

• GOAL, a BDI language with Declarative Goals.
• JASON, a Java-based interpreter for an extended version of AgentSpeak.
• 3APL, an Abstract Agent Programming Language.
• JavaPathfinder
• Jadex, a BDI agent system