程序设计与子博弈完善机制
Programming and Verifying Subgame Perfect Mechanisms
摘要：
扩展的WHILE语言的编程涉及多个代理的博弈论机制。这种机制的例子包括拍卖、投票程序和协商协议。一个结构化的操作语义提供了广泛的游戏几乎完美的信息。Hoare风格的部分正确性断言提出的原因，这些机制的正确性，正确性被解释为存在一个子博弈完美均衡。使用一个扩展的方法，前，后条件，我们表明，Hoare的原始演算的扩展是健全的和完整的推理子博弈完美均衡的博弈论机制。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
