A Game Characterisation for Inflationary Modal Logics
|
Supervisor |
|
|
Suitable for |
Abstract
Background
Extensions of modal logic by temporal or recurrence operators are widely used in the theory and practise of verification. Temporal logics can often also be described in terms of automata and games, a connection that has proved fruitful both for theoretical research as well as for actual implementations.
Whereas game characterisations of logics such as the modal mu-calculus are well-known, characterisations of logics exceeding the mu-calculus in expressive power are less understood.
Project aim
The aim of this project is to develop a game characterisation of an extension of the model mu-calculus in terms of so-called visibly pushdown games.
Prerequisites
Ideally the candidate should have taken a course on Logic, Games, and Automata and should have a strong interest in logic.