| EPSRC Reference: |
EP/E061397/1 |
| Title: |
Logic for Automated Mechanism Design and Analysis (LAMDA) |
| Principal Investigator: |
Wooldridge, Professor M |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Liverpool |
| Scheme: |
Standard Research |
| Starts: |
01 October 2007 |
Ends: |
30 September 2010 |
Value (£): |
271,317
|
| EPSRC Research Topic Classifications: |
| Artificial Intelligence |
Fundamentals of Computing |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
In recent years, there has been a dramatic increase of interest in thestudy and application of *economic mechanisms* in computerscience, particularly social choice mechanisms such as votingprocedures, which are used by a group of self-interested agents toselect an outcome from some set of candidates. The *primary aim*of this project is to develop formalisms and associated techniques toassist in the automated verification and synthesis of social choicemechanisms. To this end, we will first develop a social choicelogic, (SCL), intended for the formal specification of socialchoice mechanisms, combining features from several formalisms that wehave previously developed for the specification of cooperativesystems. We will explore the properties of SCL, and thendevelop a social choice mechanism language, (SCML),intended to allow the programmatic modelling of particular socialchoice mechanisms. We will then develop techniques for model checkingSCL-specified requirements against SCML-definedmechanisms, and investigate the complexity of this problem. Todemonstrate the viability of the approach, we will apply our formalismand modelling language to standard social choice mechanisms from theliterature. Finally, we will investigate the synthesis of mechanismsfrom specifications, by means of constructive satisfiability testing.Overall, the project has the potential to bring the samebenefits to the design and analysis of social choice mechanisms thatthe use of temporal logics and model checking have brought to reactivesystems specification and analysis.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic 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.liv.ac.uk |