Programming and Verifying Subgame Perfect Mechanisms
| dc.creator | Pauly, Marc | |
| dc.date | 2002-11-01 | |
| dc.date | 2005-03-08 | |
| dc.date.accessioned | 2026-07-07T03:18:58Z | |
| dc.date.available | 2026-07-07T03:18:58Z | |
| dc.description | 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. | |
| dc.description | 26 pages, 3 figures A section has been added which applies the calculus to an auction mechanism | |
| dc.identifier | https://arxiv.org/abs/cs/0211002 | |
| dc.identifier | http://arxiv.org/abs/cs/0211002 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/31331 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | Computer Science and Game Theory | |
| dc.subject | F.3.1; F.3.2; F.4.1; I.2.11 | |
| dc.title | Programming and Verifying Subgame Perfect Mechanisms | |
| dc.type | text |