Completeness for game logic

Sebastian Enqvist, Helle Hvid Hansen, Clemens Kupke, Yde Venema, Johannes Marti

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Abstract

Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of propositional dynamic logic (PDL) for reasoning about outcomes that players can force in determined 2-player games. Semantically, the generalisation from programs to games is mirrored by moving from Kripke models to monotone neighbourhood models. Parikh proposed a natural PDL-style Hilbert system which was easily proved to be sound, but its completeness has thus far remained an open problem. In this paper, we introduce a cut-free sequent calculus for game logic, and two cut-free sequent calculi that manipulate annotated formulas, one for game logic and one for the monotone mu-calculus, the variant of the polymodal mu-calculus where the semantics is given by monotone neighbourhood models instead of Kripke structures. We show these systems are sound and complete, and that completeness of Parikh's axiomatization follows. Our approach builds on recent ideas and results by Afshari & Leigh (LICS 2017) in that we obtain completeness via a sequence of proof transformations between the systems. A crucial ingredient is a validity-preserving translation from game logic to the monotone mu-calculus.
LanguageEnglish
Title of host publicationProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019
Number of pages23
Publication statusAccepted/In press - 28 Mar 2019
Event2019 34th Annual ACM/IEEE Symposium on Logic in computer Science (LICS) - Vancouver, Canada
Duration: 24 Jun 201927 Jun 2019
Conference number: 34

Conference

Conference2019 34th Annual ACM/IEEE Symposium on Logic in computer Science (LICS)
CountryCanada
CityVancouver
Period24/06/1927/06/19

Fingerprint

Acoustic waves
Semantics

Keywords

  • game logic
  • propositional dynamic logic
  • Kripke
  • Rohit Parikh

Cite this

Enqvist, S., Hansen, H. H., Kupke, C., Venema, Y., & Marti, J. (Accepted/In press). Completeness for game logic. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019
Enqvist, Sebastian ; Hansen, Helle Hvid ; Kupke, Clemens ; Venema, Yde ; Marti, Johannes . / Completeness for game logic. Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. 2019.
@inproceedings{7727779a42a744629a65ea8be256db51,
title = "Completeness for game logic",
abstract = "Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of propositional dynamic logic (PDL) for reasoning about outcomes that players can force in determined 2-player games. Semantically, the generalisation from programs to games is mirrored by moving from Kripke models to monotone neighbourhood models. Parikh proposed a natural PDL-style Hilbert system which was easily proved to be sound, but its completeness has thus far remained an open problem. In this paper, we introduce a cut-free sequent calculus for game logic, and two cut-free sequent calculi that manipulate annotated formulas, one for game logic and one for the monotone mu-calculus, the variant of the polymodal mu-calculus where the semantics is given by monotone neighbourhood models instead of Kripke structures. We show these systems are sound and complete, and that completeness of Parikh's axiomatization follows. Our approach builds on recent ideas and results by Afshari & Leigh (LICS 2017) in that we obtain completeness via a sequence of proof transformations between the systems. A crucial ingredient is a validity-preserving translation from game logic to the monotone mu-calculus.",
keywords = "game logic, propositional dynamic logic, Kripke, Rohit Parikh",
author = "Sebastian Enqvist and Hansen, {Helle Hvid} and Clemens Kupke and Yde Venema and Johannes Marti",
year = "2019",
month = "3",
day = "28",
language = "English",
booktitle = "Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019",

}

Enqvist, S, Hansen, HH, Kupke, C, Venema, Y & Marti, J 2019, Completeness for game logic. in Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. 2019 34th Annual ACM/IEEE Symposium on Logic in computer Science (LICS), Vancouver, Canada, 24/06/19.

Completeness for game logic. / Enqvist, Sebastian; Hansen, Helle Hvid; Kupke, Clemens; Venema, Yde ; Marti, Johannes .

Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. 2019.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - Completeness for game logic

AU - Enqvist, Sebastian

AU - Hansen, Helle Hvid

AU - Kupke, Clemens

AU - Venema, Yde

AU - Marti, Johannes

PY - 2019/3/28

Y1 - 2019/3/28

N2 - Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of propositional dynamic logic (PDL) for reasoning about outcomes that players can force in determined 2-player games. Semantically, the generalisation from programs to games is mirrored by moving from Kripke models to monotone neighbourhood models. Parikh proposed a natural PDL-style Hilbert system which was easily proved to be sound, but its completeness has thus far remained an open problem. In this paper, we introduce a cut-free sequent calculus for game logic, and two cut-free sequent calculi that manipulate annotated formulas, one for game logic and one for the monotone mu-calculus, the variant of the polymodal mu-calculus where the semantics is given by monotone neighbourhood models instead of Kripke structures. We show these systems are sound and complete, and that completeness of Parikh's axiomatization follows. Our approach builds on recent ideas and results by Afshari & Leigh (LICS 2017) in that we obtain completeness via a sequence of proof transformations between the systems. A crucial ingredient is a validity-preserving translation from game logic to the monotone mu-calculus.

AB - Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of propositional dynamic logic (PDL) for reasoning about outcomes that players can force in determined 2-player games. Semantically, the generalisation from programs to games is mirrored by moving from Kripke models to monotone neighbourhood models. Parikh proposed a natural PDL-style Hilbert system which was easily proved to be sound, but its completeness has thus far remained an open problem. In this paper, we introduce a cut-free sequent calculus for game logic, and two cut-free sequent calculi that manipulate annotated formulas, one for game logic and one for the monotone mu-calculus, the variant of the polymodal mu-calculus where the semantics is given by monotone neighbourhood models instead of Kripke structures. We show these systems are sound and complete, and that completeness of Parikh's axiomatization follows. Our approach builds on recent ideas and results by Afshari & Leigh (LICS 2017) in that we obtain completeness via a sequence of proof transformations between the systems. A crucial ingredient is a validity-preserving translation from game logic to the monotone mu-calculus.

KW - game logic

KW - propositional dynamic logic

KW - Kripke

KW - Rohit Parikh

UR - https://www.aconf.org/conf_172076.html

UR - https://arxiv.org/abs/1904.07691

M3 - Conference contribution book

BT - Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019

ER -

Enqvist S, Hansen HH, Kupke C, Venema Y, Marti J. Completeness for game logic. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. 2019