Programming and Verifying Subgame-Perfect Mechanisms

DOI10.1093/LOGCOM/EXI014MaRDI QIDQ3025339zbMATH OpenOpenAlexFDO

Authors Mark Pauly

Publication date 13 July 2005

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/cs/0211002

zbMATH Keywords

game theorysemanticsprogram verification

Mathematics Subject Classification ID

Applications of game theory (91A80) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: An extension of the WHILE-language is developed for programming game-theoretic mechanisms involving multiple agents. Examples of such mechanisms include auctions, voting procedures, and negotiation protocols. 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.

Recommendations

• Program equilibrium -- a program reasoning approach
• Computer-aided verification for mechanism design
• Subgame perfection in recursive perfect information games
• A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria
• Subgame Perfect Implementation

Cited in

(4)

• Computational complexity of some intelligent computing systems
• Abstracting and Verifying Strategy-Proofness for Auction Mechanisms
• Rationality authority for provable rational behavior
• Some comments on history based structures

This page was built for publication: Programming and Verifying Subgame-Perfect Mechanisms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3025339)