Logic for Automated Mechanism Design — A Progress Report

Michael Wooldridge, Thomas Agotnes, Paul E. Dunne, Wiebe van der Hoek

Over the past half decade, we have been exploring the use of logic in the specification and analysis of computational economic 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 temporal logics and model checking have brought to the specification 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 discuss 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.

Subjects: 7.1 Multi-Agent Systems; 11. Knowledge Representation

Submitted: Apr 24, 2007

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.