26 November 2002, Zuidelijk Interuniversitair Colloquium (ZIC), Marc Pauly

Game theory and logic can provide the tools for a more formal analysis of the social mechanisms we are involved in, such as voting procedures, auctions, and negotiation. After spending some time to motivate this research program in general, I will focus on a particular technical example, an extension of the WHILE-language for programming game-theoretic mechanisms involving multiple agents. A structured operational semantics is provided in terms of extensive games of almost perfect information. Hoare-style partial correctness assertions are proposed to reason about the correctness of these mechanisms, where correctness is interpreted as the existence of a subgame perfect equilibrium. Using an extensional approach to pre- and postconditions, we show that an extension of Hoare's original calculus is sound and complete for reasoning about subgame perfect equilibria in game-theoretic mechanisms.

For more information, see http://www.win.tue.nl/zic/ or contact Francien Dechesne (f.dechesne at uvt.nl).