Complete Game Logic with Sabotage
<|reference_start|>Complete Game Logic with Sabotage: 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 $\mu$-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.<|reference_end|>
@article{wafa2024complete,
    title={Complete Game Logic with Sabotage},
    author={Noah Abou El Wafa and Andr'e Platzer},
    journal={arXiv preprint arXiv:2404.09873},
    year={2024},
    doi={10.1145/3661814.3662121},
    archivePrefix={arXiv},
    eprint={2404.09873},
    primaryClass={cs.LO cs.GT math.LO}
}