Model Checking Agent Programming Languages
Lead Research Organisation:
University of Liverpool
Department Name: Computer Science
Abstract
Our overall goal in this project is to develop model checkingtechniques that can be applied to various agent-oriented programminglanguages. Building on our previous work on model checking forAgentSpeak, we will investigate the key aspects underlying not only AgentSpeak but other agent-oriented programming languages based on Java, such as 3APL, Concurrent MetateM, and Jadex. Based on that, wewill develop a Java infrastructure layer that is (a) relevant to theimplementation 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.As a result of this investigation, we will be able to develop bothformal semantics for these major constructs of agent programming aswell as Java libraries that implement them (based on the semantics)- the resulting intermediate agent language will be called the AgentInfrastructure Layer (AIL). As in our existing body of work, JPF is tobe used as the model checker with which to carry out formalverification of implemented agent-based systems. The idea is then toprovide automatic (and provably correct) translations from variousexisting agent-oriented programming languages.
Organisations
Publications
Dennis L
(2010)
Computational Logic in Multi-Agent Systems
Dennis L
(2011)
Model checking agent programming languages
in Automated Software Engineering
Dennis L
(2008)
Programming Multi-Agent Systems
Dennis L
(2009)
Programming Multi-Agent Systems
Fisher M
(2009)
Multi-Agent Programming
Fisher M
(2013)
Verifying autonomous systems
in Communications of the ACM
| Description | This project provided a way to automatically analyse properties of "intelligent" software. The "intelligence" is provided by an agent, being able to decide its own course of action, while the analysis is provided by strong methods based on formal logic. We provided an open source framework for defining such agent languages, for automatically verifying logical properties of the agent, and for using these techniques in the verification of complex systems which have such "intelligent" agents emb |
| Exploitation Route | Potential use in autonomous systems verification. Leads on to further academic/industrial projects. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| URL | http://cgi.csc.liv.ac.uk/MCAPL |
| Description | Foundational methods developed here have been used in subsequent research projects, to collaborate with industry, and to tackle certification and safety problems in general. An example of the latter is the subsequent development of model-checking technology to assist in the certification of unmanned air vehicles. |
| First Year Of Impact | 2007 |
| Sector | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Energy |
| Impact Types | Economic |
| Description | Trustworthy Robotic Assistants |
| Amount | £378,892 (GBP) |
| Funding ID | EP/K006193/1 |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 03/2013 |
| End | 09/2016 |