Model checking GOAL agents

This thesis presents a novel approach to model checking of agent programs written in an agent programming language. The language we consider is GOAL. The novelty of the approach is that we implement model checking algorithms from scratch on top of the standard language interpreter. In contrast, in the literature on agent program verification, agents are translated to the input language of an existing model checker, after which this verification tool is used as usual for actual model checking. We present an implementation, and show that our approach performs substantially better in terms of resource consumption than existing model checkers for GOAL. Moreover, our approach allows for more expressive property specification languages and has benefits from a software engineering point of view: the implementation of a language interpreter is gained for free. Both conceptually and on the implementation level, our approach is generic and can be applied to other agent programming languages as well. Additionally, we investigate state space reduction techniques tailored to GOAL, namely property-based slicing and partial order reduction, to further optimise our model checker's performance. To this end, we develop a static source code analysis method for GOAL agents. Case studies with both techniques show that substantial reductions can be gained when certain conditions are met.

Subject

model checking
GOAL
agents
formal verification
agent programming language

To reference this document use:

http://resolver.tudelft.nl/uuid:25d88441-7ecb-4327-9271-19fc76fb0a61

Embargo date

2010-08-28

Part of collection

Student theses

Document type

master thesis

Rights

Files

PDF

Model_Checking_GOAL_Agents.pdf

2.09 MB

Close viewer