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.
@article{7235,
title = {A Library for Algorithmic Game Theory in Ssreflect/Coq},
journal = {Journal of Formalized Reasoning},
volume = {10},
year = {2017},
doi = {10.6092/issn.1972-5787/7235},
language = {EN},
url = {http://dml.mathdoc.fr/item/7235}
}
Bagnall, Alexander; Merten, Samuel; Stewart, Gordon. A Library for Algorithmic Game Theory in Ssreflect/Coq. Journal of Formalized Reasoning, Tome 10 (2017) . doi : 10.6092/issn.1972-5787/7235. http://gdmltest.u-ga.fr/item/7235/