Created: 17th October 2018

In the summer after my first year at Imperial, I was able to undertake a UROP (undergraduate research opportunities programme) under the supervision of Prof. Alessio Lomuscio as part of the VAS research group. I was also supported by Dr. Panagiotis Kouvaros. The UROP programme affords undergraduates the opportunity to experience academic research. The VAS research group studies techniques to formally verify multi-agent systems, where agents behave autonomously.

A key piece of work produced by the group is the MCMAS model checker. A model checker is a tool in formal verification, that makes it possible to see if a system satisfies a property automatically. It either finds that the system does satisfy the property, or finds a counter-example, demonstrating that the system does not satisfy the property. It does this by efficiently representing the state space using a data structure, called a binary decision diagram. MCMAS uses the implementation of binary decision diagrams, provided by the CUDD library, which I talk more about here.

My project was to extend the MCMAS model checker to implement a parameterised model-checking algorithm. Previously, the MCMAS model-checker only allowed the verification of a multi-agent system with a concrete number of agents. A parameterised model-checking algorithm allows a property to be verified on a multi-agent system, consisting of an arbitrary number of agents. This is done by finding a cutoff \(c\), where if the property holds for \(c\) agents, then it holds for any \(n\) agents, where \(n \geq c\). I extended the implementation further to support open systems, where agents can enter and exit the system arbitrarily.

Overall, the experience was challenging but also rewarding. I was especially pleased that the work led me to co-authoring a paper presented at AAMAS19.