EPSRC logo

Details of Grant 

EPSRC Reference: EP/E061397/1
Title: Logic for Automated Mechanism Design and Analysis (LAMDA)
Principal Investigator: Wooldridge, Professor M
Other Investigators:
van der Hoek, Professor W
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