Complete Game Logic with Sabotage: A Unification of Logic, Games, and Fixpoints

Sabotage Game Logic (GLs) is a simple and natural extension of Parikh's Game Logic that allows players to lay traps for the opponent to avoid. GLs is expressively equivalent to the modal μ-calculus, revealing a close connection between the nested recursion inherent in modal fixpoint logics and adversarial dynamic rule changes characteristic for sabotage games.