Complete First-Order Game Logic
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915228293267456 |
|---|---|
| author | Wafa, Noah Abou El Platzer, André |
| author_facet | Wafa, Noah Abou El Platzer, André |
| contents | 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. Rational gameplay provably collapses the games into single-player games to yield a strong arithmetical completeness theorem for dGL with rational-time ODEs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_03495 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Complete First-Order Game Logic Wafa, Noah Abou El Platzer, André Logic in Computer Science 03B70, 03B45, 91A44, 34A38, 68Q60, 34A45 F.3.1; F.4.1; G.1.7 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. Rational gameplay provably collapses the games into single-player games to yield a strong arithmetical completeness theorem for dGL with rational-time ODEs. |
| title | Complete First-Order Game Logic |
| topic | Logic in Computer Science 03B70, 03B45, 91A44, 34A38, 68Q60, 34A45 F.3.1; F.4.1; G.1.7 |
| url | https://arxiv.org/abs/2504.03495 |