Feel free to mail me if you want to contact me on any of these projects.
Model checking is an automated verification technique that asks the user to specify a system (the model) and then allows the user to input properties in a logical language, which are then checked against the model: do they hold or not? Until recently, those properties were mainly temportal (can be guarantee that eventually P holds, or is it always the case that Q is true?).
Recently, however, especially in the Multi-Agent Systems research community, there is an increasing interest in also verifying knowledge properties (Does i know that j will eventually come to know that P?, or does the system guarantee that i will never know Q before j?)
Epistemic logic is the logic of knowledge, in which one can express properties like the above, if a proper temporal dimension is added to the language. Model checkers for knowledge and time have been developped and studied in the last 10 years, see the references in the paper cited below.
In Dynamic Epistemic Logic (DEL), knowledge not just develops over time, but there is an arsenal of actions that have an epistemic flavour, like public announcements, or private communication. A model checker for DEL recently developped is DEMO.
DEMO will be the tool of research in this MsC project. First of all, the student will make him/her self familiar with the tool and read about implementations of some well-known epistemic puzzles. Then, the student and the supervisors will together decide about another dynamic epistemic problem of which the implementation in DEMO is the second part of this project.
Model Checking Russian Cards
H.P. van Ditmarsch, W. van der Hoek, R. van der Meyden, and J. Ruan
Electronic Notes in Theoretical Computer Science
Volume 149, Issue 2, 2006, Pages 105-123