A Library for Algorithmic Game Theory in Ssreflect/Coq
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2017-12-01
|
| Series: | Journal of Formalized Reasoning |
| Subjects: | |
| Online Access: | https://jfr.unibo.it/article/view/7235 |
| _version_ | 1818598961928208384 |
|---|---|
| author | Alexander Bagnall Samuel Merten Gordon Stewart |
| author_facet | Alexander Bagnall Samuel Merten Gordon Stewart |
| author_sort | Alexander Bagnall |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-16T12:12:01Z |
| format | Article |
| id | doaj.art-5e7a964144cd4970985e87ca4e5c166c |
| institution | Directory Open Access Journal |
| issn | 1972-5787 |
| language | English |
| last_indexed | 2024-12-16T12:12:01Z |
| publishDate | 2017-12-01 |
| publisher | University of Bologna |
| record_format | Article |
| series | Journal of Formalized Reasoning |
| spelling | doaj.art-5e7a964144cd4970985e87ca4e5c166c2022-12-21T22:32:10ZengUniversity of BolognaJournal of Formalized Reasoning1972-57872017-12-01101679510.6092/issn.1972-5787/72356788A Library for Algorithmic Game Theory in Ssreflect/CoqAlexander BagnallSamuel MertenGordon StewartWe 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.https://jfr.unibo.it/article/view/7235CoqSsreflectAlgorithmic Game Theory |
| spellingShingle | Alexander Bagnall Samuel Merten Gordon Stewart A Library for Algorithmic Game Theory in Ssreflect/Coq Journal of Formalized Reasoning Coq Ssreflect Algorithmic Game Theory |
| title | A Library for Algorithmic Game Theory in Ssreflect/Coq |
| title_full | A Library for Algorithmic Game Theory in Ssreflect/Coq |
| title_fullStr | A Library for Algorithmic Game Theory in Ssreflect/Coq |
| title_full_unstemmed | A Library for Algorithmic Game Theory in Ssreflect/Coq |
| title_short | A Library for Algorithmic Game Theory in Ssreflect/Coq |
| title_sort | library for algorithmic game theory in ssreflect coq |
| topic | Coq Ssreflect Algorithmic Game Theory |
| url | https://jfr.unibo.it/article/view/7235 |
| work_keys_str_mv | AT alexanderbagnall alibraryforalgorithmicgametheoryinssreflectcoq AT samuelmerten alibraryforalgorithmicgametheoryinssreflectcoq AT gordonstewart alibraryforalgorithmicgametheoryinssreflectcoq AT alexanderbagnall libraryforalgorithmicgametheoryinssreflectcoq AT samuelmerten libraryforalgorithmicgametheoryinssreflectcoq AT gordonstewart libraryforalgorithmicgametheoryinssreflectcoq |