MCMAS-Dynamic

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). I implemented these algorithms as an extension of the state-of-the-art MCMAS model checker.

I’ve given two talks on the work I’ve done as part of the thesis:

My supervisor, Prof. Alessio Lomuscio and I have also published some work based on 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. To appear. AAAI Press.

I was awarded the IBM Project Prize for my work, and received a grade of 100% (making me the second student in the history of the Department to accomplish that).