First-Order Game Logic and Modal Mu-Calculus

TL;DR

This paper explores the expressive power and proof systems of first-order game logic and modal mu-calculus, establishing their equivalence and completeness, especially in the context of hybrid systems with differential equations.

Contribution

It demonstrates the equivalence of first-order game logic and modal mu-calculus in expressive and deductive power, and provides translations between differential game logic and differential mu-calculus.

Findings

Both logics have the same expressive power.

Their proof calculi are mutually relatively complete.

Complete translations exist between differential game logic and differential mu-calculus.

Abstract

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.