Modal mu-calculus: A study in descriptive complexity

The project is part of a broader research programme with the purpose to deepen our understanding of the mathematical theory underpinning "reactive computer systems''. These systems are designed to maintain an ongoing interaction with their environment and, as in the case of automated railway signalling, are often safety critical. The key properties of reactive systems, such as correctness of signalling, can be readily specified and tested within an abstract logical system known as mu-calculus.

The aim of the research project is to develop fresh techniques for solving questions concerning expressibility (which properties can/cannot be expressed?), strength (how much recursion is required?), decidability (do reasonable algorithms exist?) and complexity (what resources are needed in computation?).