A Library for Algorithmic Game Theory in Ssreflect/Coq

Authors

  • Alexander Bagnall
  • Samuel Merten
  • Gordon Stewart Ohio University

DOI:

https://doi.org/10.6092/issn.1972-5787/7235

Keywords:

Coq, Ssreflect, Algorithmic Game Theory

Abstract

We report on the formalization in Ssreflect/Coq of a number of concepts and results from algorithmic game theory, including potential games, smooth games, solution concepts such as Pure and Mixed Nash Equilibria, Coarse Correlated Equilibria, epsilon-approximate equilibria, and behavioral models of games such as best-response dynamics. We apply the formalization to prove  Price of Stability bounds for, and convergence under best-response dynamics of, the Atomic Routing game, which has applications in computer networking. Our second application proves that Affine Congestion games are (5/3, 1/3)-smooth, and therefore have Price of Anarchy 5/2. Our formalization is available online.

Downloads

Published

2017-12-21

How to Cite

Bagnall, A., Merten, S., & Stewart, G. (2017). A Library for Algorithmic Game Theory in Ssreflect/Coq. Journal of Formalized Reasoning, 10(1), 67–95. https://doi.org/10.6092/issn.1972-5787/7235

Issue

Section

Articles