MCAPL:Model Checking Agent Programming Languages

Contents

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

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

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


Outputs Produced

Publications

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