Document Open Access Logo

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

Authors Érik Martin-Dorel, Sergei Soloviev

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2016.14.pdf
  • Filesize: 0.6 MB
  • 22 pages

Document Identifiers

Author Details

Érik Martin-Dorel
Sergei Soloviev

Cite As Get BibTex

Érik Martin-Dorel and Sergei Soloviev. A Formal Study of Boolean Games with Random Formulas as Payoff Functions. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.TYPES.2016.14

Abstract

In this paper, we present a probabilistic analysis of Boolean games. We consider the class of Boolean games where payoff functions are given by random Boolean formulas. This permits to study certain properties of this class in its totality, such as the probability of existence of a winning strategy, including its asymptotic behaviour. 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 further developments.

Subject Classification

Keywords
  • Boolean games
  • Random process
  • Coq formal proofs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Reynald Affeldt, Manabu Hagiwara, and Jonas Sénizergues. Formalization of Shannon’s theorems. J. Autom. Reasoning, 53(1):63-103, 2014. URL: http://dx.doi.org/10.1007/s10817-013-9298-1.
  2. Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. Sci. Comput. Program., 74(8):568-589, 2009. URL: http://dx.doi.org/10.1016/j.scico.2007.09.002.
  3. Élise Bonzon. Modélisation des interactions entre agents rationnels : les jeux booléens. PhD thesis, Université Toulouse III - Paul Sabatier, Toulouse, France, 2007. Google Scholar
  4. Julian C. Bradfield, Julian Gutierrez, and Michael Wooldridge. Partial-order Boolean games: informational independence in a logic-based model of strategic interaction. Synthese, 193(3):781-811, 2016. URL: http://dx.doi.org/10.1007/s11229-015-0991-y.
  5. The Coq Development Team. The Coq Proof Assistant: Reference Manual: version 8.8, 2018. URL: https://coq.inria.fr/distrib/V8.8.0/refman/.
  6. Evgeny Dantsin, Jan-Georg Smaus, and Sergei Soloviev. Algorithms in Games Evolving in Time: Winning Strategies Based on Testing. In Isabelle Users Workshop - ITP 2012, 2012. 18 pages. Google Scholar
  7. Paul E. Dunne and Wiebe van der Hoek. Representation and complexity in boolean games. In José Júlio Alferes and João Alexandre Leite, editors, Logics in Artificial Intelligence, 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27-30, 2004, Proceedings, volume 3229 of Lecture Notes in Computer Science, pages 347-359. Springer, 2004. URL: http://dx.doi.org/10.1007/978-3-540-30227-8_30.
  8. Danièle Gardy. Random Boolean expressions. In René David, Danièle Gardy, Pierre Lescanne, and Marek Zaionc, editors, Computational Logic and Applications, CLA '05, volume AF of DMTCS Proceedings, pages 1-36, Chambéry, France, 2006. Discrete Mathematics and Theoretical Computer Science. Google Scholar
  9. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A Machine-Checked Proof of the Odd Order Theorem. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science, pages 163-179. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-39634-2_14.
  10. Paul Harrenstein. Logic in Conflict. Logical Explorations in Strategic Equilibrium. PhD thesis, Utrecht University, 2004. Google Scholar
  11. Paul Harrenstein, Wiebe van der Hoek, John-Jules Meyer, and Cees Witteveen. Boolean Games. In J. van Benthem, editor, Proceedings of the 8th International Conference on Theoretical Aspects of Rationality and Knowledge (TARK'01), pages 287-298, San Francisco, 2001. Morgan Kaufmann. Google Scholar
  12. Osman Hasan and Sofiène Tahar. Using theorem proving to verify expectation and variance for discrete random variables. J. Autom. Reasoning, 41(3-4):295-323, 2008. URL: http://dx.doi.org/10.1007/s10817-008-9113-6.
  13. Joe Hurd. Formal verification of probabilistic algorithms. PhD thesis, University of Cambridge, 2002. Google Scholar
  14. Erik Martin-Dorel and Sergei Soloviev. erikmd/coq-bool-games: BoolGames, 2018. URL: http://dx.doi.org/10.5281/zenodo.1317609.
  15. Tarek Mhamdi, Osman Hasan, and Sofiène Tahar. On the formalization of the Lebesgue integration theory in HOL. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pages 387-402. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14052-5_27.
  16. John Riordan and C. E. Shannon. The number of two-terminal series-parallel networks. Journal of Mathematics and Physics, 21:83-93, 1942. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact