核心概念
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.
要約
The paper introduces Sabotage Game Logic (GLs), a new extension of Parikh's Game Logic (GL) that adds a single primitive to allow players to lay traps for their opponent. This simple and natural mechanism of imperative game play is shown to be expressively equivalent to the functional mechanism of unstructured nested named recursion with fixpoint variables in the alternating fixpoints of the modal μ-calculus.
The key insights are:
- GLs can express sufficient adversarial dynamics to capture the alternating fixpoints of the modal μ-calculus, but lacks a suitable way to refer to fixpoints by their respective fixpoint variables.
- GLs remedies this by allowing players to dynamically change the rules of the game by laying traps, which can be used to change the meaning of atomic games.
- The role the sabotage operator ∼a plays in establishing the equiexpressiveness reveals an interesting connection between games with sabotage and the nesting of fixpoints in the modal μ-calculus.
- By the equivalence of the modal μ-calculus and GLs, many desirable properties of the modal μ-calculus, such as decidability and small model property, can be transferred to GLs.
- The paper also presents a sound and complete proof calculus for GLs, and uses this to obtain the first complete proof calculus for the original Game Logic.
引用
"GLs promises to be a useful tool for understanding GL. This is evidenced by the completeness of an extension of Parikh's axiomatization for GL obtained from the complete proof calculus for GLs."
"The embedding from sabotage game logic to the modal μ-calculus also suggests the possibility that the same property can be expressed significantly more concisely in sabotage game logic than in the modal μ-calculus."