Reasoning about Games via a First-order Modal Model Checking Approach

TL;DR

This paper introduces Game Analysis Logic (GAL), a first-order CTL-based logic for modeling and analyzing extensive games, including solution concepts like Nash and subgame perfect equilibria, with an automated model checker.

Contribution

The paper develops GAL, a novel logical framework for formal reasoning about games, and provides a model checker for automatic analysis of game solutions and AI algorithms.

Findings

GAL effectively models extensive games with perfect information.

The model checker can identify game solution concepts automatically.

GAL can analyze AI algorithms like minimax within game models.

Abstract

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.