My Master’s thesis at Imperial involved the development, implementation and evaluation of symbolic model checking algorithms for various temporal-epistemic logics (and suitable extensions). These included CTL*K, a well-known specification logic that MCMAS previously did not support. More interestingly, I developed novel algorithms for Linear Dynamic Logic (LDL) with epistemic modalities, and for a variant over finite traces. I also implemented these algorithms as an extension of the state-of-the-art MCMAS model checker.
For a 20-minute overview of what I’ve done (and admittedly some of the gory details of the LDL algorithm), see this youtube video.
My supervisor, Prof. Alessio Lomuscio and I have published several papers based on work done as part of the project.
- J. Kong, A. Lomuscio. Symbolic Model Checking Multi-Agent Systems against CTL*K Specifications. Proceedings of the 16th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS17). Sao Paolo, Brazil. pp 114-122. IFAAMAS Press.
- J. Kong, A. Lomuscio. Model Checking Multi-Agent Systems against LDLK Specifications. Proceedings of the 26th Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. pp 1138-1144. AAAI Press.
- J. Kong, A. Lomuscio. Model Checking Multi-Agent Systems against LDLK Specifications on Finite Traces. Proceedings of the 17th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS18). Stockholm, Sweden. pp 166-174. IFAAMAS Press.
The project received several awards:
- IBM Project Prize at Imperial (2016), awarded to the best final-year undergraduate project;
- grade of 100% (2016), which is the second occurrence in the history of the Department;
- VCLA Outstanding Master Thesis Award (2018), awarded for works “which ask innovative questions and meet the highest academic standards for scientific research in the field of Logic and Computer Science”.
The implementations for LTLK and CTL*K have been merged into the mainline branch of MCMAS (released in v1.3.0; I oversaw the release process for that version). The extensions of the model checker to support properties specified in LDLK (and on finite traces) are also available on the MCMAS website.
I’ve also given two talks at Imperial (in addition to presenting at the conferences above) on the work I’ve done as part of the thesis: