OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

An Existence Theorem of Nash Equilibrium in Coq and Isabelle

Le Roux, Stéphane and Martin-Dorel, Erik and Smaus, Jan-Georg An Existence Theorem of Nash Equilibrium in Coq and Isabelle. (2017) In: 8th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2017), 20 September 2017 - 22 September 2017 (Rome, Italy).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://doi.org/10.4204/EPTCS.256.4


Nash equilibrium (NE) is a central concept in game theory. Here we prove formally a published theorem on existence of an NE in two proof assistants, Coq and Isabelle: starting from a game with finitely many outcomes, one may derive a game by rewriting each of these outcomes with either of two basic outcomes, namely that Player 1 wins or that Player 2 wins. If all ways of deriving such a win/lose game lead to a game where one player has a winning strategy, the original game also has a Nash equilibrium. This article makes three other contributions: first, while the original proof invoked linear extension of strict partial orders, here we avoid it by generalizing the relevant definition. Second, we notice that the theorem also implies the existence of a secure equilibrium, a stronger version of NE that was introduced for model checking. Third, we also notice that the constructive proof of the theorem computes secure equilibria for non-zero-sum priority games (generalizing parity games) in quasi-polynomial time.

Item Type:Conference or Workshop Item (Paper)
Additional Information:EPTCS 256 : Proceedings of 8th International Symposium on Games, Automata, Logics and Formal Verification ISSN: 2075-2180 https://arxiv.org/abs/1709.02096
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Université Libre de Bruxelles - ULB (BELGIUM)
Laboratory name:
FAGames project of LabEx CIMI - ERC inVEST (279499) project
Deposited On:17 Oct 2018 14:16

Repository Staff Only: item control page