New aspects of the mu-calculus

点击翻译按钮获取中文摘要

Formal logic provides us with a mathematical language for specifying and describing systems, as well as powerful methods for reasoning about whether a logical statement is true in a given situation, which logical statements follow from which, and so on - and these methods can often be automated. Model checking applies these ideas to provide powerful automated tools for verifying that software meets its specification. This can save companies money and provide confidence to wide society of the reliability of software. Conventional model checking has been enormously successful industrially, but much of it has considered time as discretely ticking - 0, 1, 2, and so on. For some computer systems, continuous time as used in physics is more appropriate. Part of this project will study the possibilities for model checking in situations concerning real-time models, using a very powerful logic, the temporal mu-calculus. In the long term, it may lead to new ways of model checking more sophisticated systems.As well as time, space is an important aspect of many modern applications, including databases, geographic information systems, and geometrical reasoning. Logic can also be used to make statements about space, and reason with them. Many different logical systems have been used, but again the very powerful mu-calculus has not been greatly investigated in this context. This project aims to study the modal mu-calculus in spatial contexts, trying to ascertain its expressiveness, and what machinery is needed to reason correctly with it. The work has the potential in the long run to improve our ability to specify and reason about situations involving space.We will also take the opportunity to try to establish some fundamental facts about the mu-calculus's power to define classes of situations, echoing the so-called Goldblatt-Thomason theorem for simpler logics. If successful, this will provide researchers with a basic tool usable in many areas requiring the mu-calculus.Only three months is available for the research on this ambitious project, and it is likely that not all problems will be solved, but we hope that good progress will be made.