Projects per year
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.
Original language | English |
---|---|
Title of host publication | 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
Place of Publication | Piscataway, NJ. |
Publisher | IEEE |
Pages | 1-23 |
Number of pages | 23 |
ISBN (Print) | 9781728136097 |
DOIs | |
Publication status | Published - 5 Aug 2019 |
Event | 2019 34th Annual ACM/IEEE Symposium on Logic in computer Science (LICS) - Vancouver, Canada Duration: 24 Jun 2019 → 27 Jun 2019 Conference number: 34 |
Conference
Conference | 2019 34th Annual ACM/IEEE Symposium on Logic in computer Science (LICS) |
---|---|
Country/Territory | Canada |
City | Vancouver |
Period | 24/06/19 → 27/06/19 |
Keywords
- game logic
- propositional dynamic logic
- Kripke
- Rohit Parikh
Fingerprint
Dive into the research topics of 'Completeness for game logic'. Together they form a unique fingerprint.Profiles
Projects
- 1 Finished
-
Coalgebraic Foundations of Semi-Structured Data (EPSRC First Grant)
Kupke, C. (Principal Investigator)
EPSRC (Engineering and Physical Sciences Research Council)
1/02/16 → 31/01/18
Project: Research