Complete Game Logic with Sabotage

我们介绍了Sabotage Game Logic ($\mathsf{GL_s}$)，这是Parikh的Game Logic的一个简单而自然的扩展，增加了一个额外的原语，允许玩家设置陷阱来避免对手。$\mathsf{GL_s}$可用于建模无限的破坏游戏，在这种游戏中，玩家可以在游戏过程中改变规则。与Game Logic严格不同的是，GLs的表达能力与模态$\mu$-演算完全相同。这揭示了模态定点递归内在的纠缠嵌套递归与破坏游戏的对手动态规则变化之间的密切联系。此外，我们提供了一个自然的Hilbert风格的证明演算法用于$\mathsf{GL_s}$，并证明了完备性。Game Logic的Parikh演算法的扩展的完备性也随之得出。

论文试图探讨如何使用Sabotage Game Logic（GLs）来建模无限的破坏游戏，并解决其中的动态规则变化问题。同时，论文还试图证明GLs与模态μ-演算具有密切联系。

论文提出了一种名为Sabotage Game Logic（GLs）的扩展模型，通过新增加一个基本操作来允许玩家设置陷阱，从而建模无限的破坏游戏。同时，GLs与模态μ-演算具有等价性，这揭示了模态固定点递归逻辑与破坏游戏中的对手动态规则变化之间的密切联系。

论文提出了一种自然的Hilbert样式证明演算法，并证明了其完备性。此外，论文还证明了对于Game Logic的扩展Parikh演算法的完备性。实验方面，论文主要是理论研究，没有使用具体的数据集或开源代码。值得深入研究的是，GLs的应用范围是否可以拓展到其他领域。

最近在这个领域中，还有一些相关研究，例如《Game Logic and Verification for Learning and Neural Networks》、《A Survey of Game Theory as Applied to Network Security》等。