Model Checking Agent Programming Languages

Lead Research Organisation: University of Liverpool
Department Name: Computer Science


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.


10 25 50

publication icon
Dennis L (2011) Model checking agent programming languages in Automated Software Engineering

publication icon
Fisher M (2009) Multi-Agent Programming

publication icon
Fisher Michael (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)

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 Academic/University
Country United Kingdom
Start 03/2013 
End 09/2016