2025/04/04 by Noah Abou El Wafa, André Platzer, Wafa, Noah Abou El +1 · 1 citation
Computer Science · #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO
paper · pdf · doi:10.48550/arxiv.2504.03495
openalex publication_date 2025/04/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Games and fixpoints are unified by proving that first-order game logic GL and the first-order modal mu-calculus Lmu are proved to be equiexpressive and equivalent, thereby fully aligning their expressive and deductive power. That is, there is a semantics-preserving translation from GL to Lmu, and vice versa. And both translations are provability-preserving, while equivalence with there-and-back-again roundtrip translations are provable in both calculi. This is to be contrasted with the propositional case, where game logic is strictly less expressive than the modal mu-calculus (without adding sabotage games). The extensions with differential equations, differential game logic (dGL) and differential modal mu-calculus, are also proved equiexpressive and equivalent. Moreover, as the continuous dynamics are definable by fixpoints or via games, ODEs can be axiomatized completely and, as a consequence, infinitesimally robust properties of ODEs can be decided via proof search. Rational gameplay provably collapses the games into single-player games to yield a strong arithmetical completeness theorem for dGL with rational-time ODEs.