Logic for Automated Mechanism Design and Analysis (LAMDA)

近年来，人们对计算机科学中的经济机制的研究和应用的兴趣急剧增加，特别是社会选择机制，如投票程序，这是由一组自利的代理人从一些候选人中选择结果。这个项目的主要目标是开发形式主义和相关技术，以帮助社会选择机制的自动验证和合成。为此，我们将首先开发一个社会选择逻辑，（SCL），旨在正式规范的socialchoice机制，结合功能，从几个形式主义，我们以前开发的规范的cooperativesystems。我们将探索SCL的属性，然后开发一种社会选择机制语言（SCML），旨在允许特定的社会选择机制的程序化建模。然后，我们将开发针对SCL定义的机制的模型检查SCL指定的需求的技术，并研究这个问题的复杂性。为了证明这种方法的可行性，我们将应用我们的形式主义和建模语言，从文献标准的社会选择机制。最后，我们将研究从规范的机制的合成，通过建设性的可满足性testing.Overall，该项目有可能带来相同的好处，社会选择机制的设计和分析，使用时序逻辑和模型检查带来了反应系统的规范和分析。

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.