EPSRC Reference: 
EP/G012962/1 
Title: 
Solving Parity Games and MuCalculi 
Principal Investigator: 
Bradfield, Dr J 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Lab. for Foundations of Computer Science 
Organisation: 
University of Edinburgh 
Scheme: 
Standard Research 
Starts: 
01 January 2009 
Ends: 
31 December 2012 
Value (£): 
279,162

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
17 Jul 2008

ICT Prioritisation Panel (July 2008)

Announced


Summary on Grant Application Form 
Modal mucalculus 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 mucalculus, which let us solve another well known problem about modal mucalculus. 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 mucalculus, 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.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 

Further Information: 

Organisation Website: 
http://www.ed.ac.uk 