A Formal Study of Boolean Games with Random Formulas as Payoff Functions

Érik Martin-Dorel (1, 2) , Sergei Soloviev (1, 3)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 UT3 - Université Toulouse III - Paul Sabatier
3 ITMO - National Research University of Information Technologies, Mechanics and Optics [St. Petersburg]

A probabilistic analysis of Boolean games is presented. The class of Boolean games with payoff functions given by random Boolean formulas is studied. This permits to study certain properties of this class in its totality, such as the probability of the existence of a winning strategy, including its asymptotic behavior. With the help of the Coq proof assistant, we develop a Coq library of Boolean games, to provide a formal proof of our results, and a basis for future development.

Mots clés: Boolean Games; Random process; Coq formal proofs

Domaines: Génie logiciel [cs.SE]; Systèmes embarqués; Cryptographie et sécurité [cs.CR]; Interface homme-machine [cs.HC]; Architectures Matérielles [cs.AR]; Modélisation et simulation

Érik Martin-Dorel, Sergei Soloviev. A Formal Study of Boolean Games with Random Formulas as Payoff Functions. 22nd International Conference on Types for Proofs and Programs (TYPES 2016), May 2016, Novi Sad, Serbia. pp.1-22, ⟨10.4230/LIPIcs.TYPES.2016.14⟩. ⟨hal-02651342⟩