Logic for Automated Mechanism Design and Analysis (LAMDA)

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.