Logic for automated mechanism design - a progress report

Over the past half decade, we have been exploring the use of logic in the specification and analysis of computational eco-nomic mechanisms. We believe that this approach has the potential to bring the same benefits to the design and analysis of computational economic mechanisms that the use of tem-poral logics and model checking have brought to the specifi-cation and analysis of reactive systems. In this paper, we give a survey of our work. We first discuss the use of cooperation logics such as Alternating-time Temporal Logic (ATL) for the specification and verification of mechanisms such as social choice procedures. We motivate the approach, and then dis-cuss the work we have done on extensions to ATL to support incomplete information, preferences, and quantification over coalitions. We then discuss is the use of ATL-like cooperation logics in the development of social laws