2014/02/06 by Davi Romero de Vasconcelos, Edward Hermann Haeusler, Edward Hermann Hæusler +2 · 1 citation
Computer Science · Mathematics · #Combinatorial game theory #Computer science #Economics #FOS: Computer and information sciences #Formal Methods in Verification #Game theory #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematical economics #Mathematics #Minimax #Model checking #Nash equilibrium #Normal-form game #Order (exchange) #Repeated game #Sequential game #Subgame perfect equilibrium #Theoretical computer science #cs.LO
paper · pdf · doi:10.48550/arxiv.1402.1377
published in arXiv (Cornell University) 194, 116917 (Cornell University) · Extended version of article published in the SBMF 2007. Accepted to ENTCS. Withdrawn from ENTCS in 2014 in virtue to submission to other venue
openalex publication_date 2014/02/06 · arxiv created 2014/04/14 · arxiv updated 2014/04/15 · openalex created_date 2016/06/24 · openalex updated_date 2026/08/05
In this work, we present a logic based on first-order CTL, namely Game Analysis Logic (GAL), in order to reason about games. We relate models and solution concepts of Game Theory as models and formulas of GAL, respectively. Precisely, we express extensive games with perfect in- formation as models of GAL, and Nash equilibrium and subgame perfect equilibrium by means of formulas of GAL. From a practical point of view, we provide a GAL model checker in order to analyze games automatically. We use our model checker in at least two directions: to find solution con- cepts of Game Theory; and, to analyze players that are based on standard algorithms of the AI community, such as the minimax procedure.