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:
- Symbolic Model Checking Full Branching Time Epistemic Specifications (14 Jul 2016)
- Symbolic Model Checking Linear Dynamic Logic and Extensions (28 Jul 2016)
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).