论文标题
一阶游戏逻辑和模态MU-Calculus
First-Order Game Logic and Modal Mu-Calculus
论文作者
论文摘要
本文研究了一阶游戏逻辑和一阶模态mu-calculus，该逻辑将其命题模态逻辑对应物扩展，并具有解释效果的一阶模态，例如可变分配。与命题情况不同，两种逻辑都具有相同的表达能力，并且其证明表述具有相同的演绎能力。两种结石也相对完整。 在存在微分方程的情况下，推论可在差异游戏逻辑，混合游戏的演绎验证的逻辑和差异MU-Calculus（混合系统的模态MU-Calculus）之间获得可用且完整的翻译。相对于一阶FixPoint逻辑，差异MU-Calculus与其无ode的片段相对于一阶固定点逻辑而完成。
This paper investigates first-order game logic and first-order modal mu-calculus, which extend their propositional modal logic counterparts with first-order modalities of interpreted effects such as variable assignments. Unlike in the propositional case, both logics are shown to have the same expressive power and their proof calculi to have the same deductive power. Both calculi are also mutually relatively complete. In the presence of differential equations, corollaries obtain usable and complete translations between differential game logic, a logic for the deductive verification of hybrid games, and the differential mu-calculus, the modal mu-calculus for hybrid systems. The differential mu-calculus is complete with respect to first-order fixpoint logic and differential game logic is complete with respect to its ODE-free fragment.
