Research Perspectives - Tools for Visualisation of Portfolios
EPSRC logo

EPSRC Database


Source RCUK EPSRC Data

EP/G012962/1 - Solving Parity Games and Mu-Calculi

Research Perspectives grant details from EPSRC portfolio

http://www.researchperspectives.org/gow.grants/grant_EPG0129621.png

Dr J Bradfield EP/G012962/1 - Solving Parity Games and Mu-Calculi

Principal Investigator - Lab. for Foundations of Computer Science, University of Edinburgh

Scheme

Standard Research

Research Areas

Maths of Computing Maths of Computing

Start Date

01/2009

End Date

12/2012

Value

£279,162

Similar Grants

Automatic generation of similar EPSRC grants

Similar Topics

Topic similar to the description of this grant

Grant Description

Summary and Description of the grant

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.

Structured Data / Microdata


Grant Event Details:
Name: Solving Parity Games and Mu-Calculi - EP/G012962/1
Start Date: 2009-01-01T00:00:00+00:00
End Date: 2012-12-31T00:00:00+00:00

Organization: University of Edinburgh

Description: 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 ...