Description of field of research:
Temporal epistemic logics model reasoning over time and knowledge and have paractical applications in ComputerScience for reasoning about, for example, the correctness of knowledge-sensitive protocols. Recent work by van der Meyden and Patra have identified a large class of probabilistic temporal epistemic logics where the model chekcing problem is undecidable, but this result is contingent on an open problem related to the probabilistic aspect of these logics. This project aims to resolve the results of van der Meyden and Patra in the non-probabilistic setting.
School
Research Area
Formal methods | Theoretical computer science
- Research Environment
- Expected Outcomes
- Reference Material/Links
- Our team
The work will be carried out under the supervision of Dr Paul Hunter as part of the Formal Methods group Students will meet at a minimum weekly to discuss progress, but are encouraged to work independently towards resolving the problems.
Students will experience working in a small team towards resolving open problems in Theoretical Computer Science. They will learn about the complexity of model checking logics, and learn about producing work using formal mathematical writing.
van der Meyden, R. and Patra M.; "Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic", 2018, Available at http://arxiv.org/abs/1511.03003
