Complete Game Logic with Sabotage
Noah Abou El Wafa, André Platzer
TL;DR
The paper presents GL_s, a minimal yet powerful extension of Parikh's Game Logic by introducing a sabotage operator that lets players dynamically alter rules. It establishes a precise equivalence in expressive power between GL_s and the modal $\mu$-calculus, and provides a complete Hilbert-style calculus for GL_s by translating into or from fixpoint logics. Through the intermediary Recursive Game Logic (RGL) and the Fixpoint Logic with Chop (FLC), the authors construct modular equiexpressiveness proofs and translations that unify games, recursion, and fixpoints. They further show that GL_s inherits decidability and the small model property from the modal $\mu$-calculus, and they develop mechanisms such as sabotage memory to encode complex state information, while demonstrating that GL_s remains a natural and succinct specification language for adversarial dynamics. Overall, the work solidifies the tight correspondence between game-theoretic reasoning and fixpoint logics, enabling efficient reasoning, completeness results, and practical succinctness benefits for sabotage-enabled game modeling.
Abstract
Game Logic with sabotage ($\mathsf{GL_s}$) is introduced as a simple and natural extension of Parikh's game logic with a single additional primitive, which allows players to lay traps for the opponent. $\mathsf{GL_s}$ can be used to model infinite sabotage games, in which players can change the rules during game play. In contrast to game logic, which is strictly less expressive, $\mathsf{GL_s}$ is exactly as expressive as the modal $μ$-calculus. This reveals a close connection between the entangled nested recursion inherent in modal fixpoint logics and adversarial dynamic rule changes characteristic for sabotage games. A natural Hilbert-style proof calculus for $\mathsf{GL_s}$ is presented and proved complete using syntactic equiexpressiveness reductions. The completeness of a simple extension of Parikh's calculus for game logic follows.