Programming and Verifying Subgame-Perfect Mechanisms
Copyright policy )Programming and Verifying Subgame-Perfect Mechanisms
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.
26 pages, 3 figures A section has been added which applies the calculus to an auction mechanism
game theory, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Specification and verification (program logics, model checking, etc.), I.2.11, F.3.1; F.3.2; F.4.1; I.2.11, Logic in Computer Science (cs.LO), program verification, Computer Science - Computer Science and Game Theory, Applications of game theory, F.3.2, F.4.1, F.3.1, semantics, Computer Science and Game Theory (cs.GT)
game theory, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Specification and verification (program logics, model checking, etc.), I.2.11, F.3.1; F.3.2; F.4.1; I.2.11, Logic in Computer Science (cs.LO), program verification, Computer Science - Computer Science and Game Theory, Applications of game theory, F.3.2, F.4.1, F.3.1, semantics, Computer Science and Game Theory (cs.GT)
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).10 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Top 10% impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Top 10%
Citations provided by BIP!Popularity provided by BIP!