Solving Parity Games and Mu-Calculi

Modal mu-calculus is a logical language used for describing the behaviour of hardware and software systems. It is widely used, but we still don't know some of its main mathematical properties. In particular, we don't know whether it's always cheap to work out whether a system has some behaviour described in this language, or whether very complicated properties are really expensive to check. People have been trying to solve this problem for more than 20 years now.In this grant proposal, we want to explore some new approaches to this problem. Our main aim is to use a branch of mathematics called descriptive set theory, which looks at the difficulty of describing - writing down in mathematical notation - sets of numbers. Some sets require very complicated formulae to write them down, whereas others have simple descriptions. In earlier work, we have made a connection between this difficulty of describing sets, and the complexity of properties in modal mu-calculus, which let us solve another well known problem about modal mu-calculus. Now we want to take these ideas much further, and see if we can get closer to a solution to the problem described above.Another of the surprising things about this problem is that there are ways of solving it which look as though they are fast, but which nobody can yet prove really are fast. So we will also try to understand these solutions more deeply, hoping to show either that they really are always fast, or that we can come up with bad examples on which they take a long time.We are also trying to solve another problem about modal mu-calculus, which is basically this: if you give me a formula that looks very complicated, can I work out whether it is really a complicated property, or whether it can be turned into an equivalent but much simpler formula? This has also been around for a long time, with only limited answers. We think that this problem is well suited to an approach with our techniques, and we are optimistic about solving it.