The Modal Logics of the Poison Game

F. Zaffora Blando, K. Mierzewski, and C. Areces. The Modal Logics of the Poison Game. In F. Liu, H. Ono, and J. Yu, editors, Knowledge, Proof and Dynamics, pp. 3–23, Springer Singapore, Singapore, 2020.

Download

[pdf] 

Abstract

The poison game is a two-player zero-sum game played on directed graphs, first introduced by Duchet and Meyniel (1993) in the context of graph theory, where one of the players travels along the edges of a graph, while the other modifies the underlying structure by marking vertices. In this paper, we investigate the poison game from the perspective of modal logic, as a natural case study of the use of modal languages equipped with model-changing operators to describe evolving relational structures. In particular, to model the poison game, we consider three memory logics of decreasing expressive power but increasing fit with the game. We begin with ML\emptyset, the basic memory logic restricted to the initial class of models with an empty memory (see Areces et al. 2011). We then identify two fragments of ML\emptyset, which we respectively, denote as PML and PSL, and whose modal operators capture operations on models that mimic more closely the moves of both players. We show that these logics form a chain in expressive power with PML < ML\emptyset, and we introduce suitable notions of bisimulation for the two new logics presented in this paper. We then show that model checking for both PML and PSL is PSPACE-complete. The construction also establishes that determining the existence of a winning strategy in the poison game is PSPACE-hard. We conclude by proving that PML, while strictly less expressive than ML\emptyset, nonetheless has an undecidable satisfiability problem.

BibTeX

@InCollection{978-981-15-2221-5_1,
  author =       "F. Zaffora Blando and K. Mierzewski and C. Areces",
  editor =       "F. Liu and H. Ono and J. Yu",
  title =        "The Modal Logics of the {Poison} Game",
  booktitle =    "Knowledge, Proof and Dynamics",
  year =         "2020",
  abstract =     "The poison game is a two-player zero-sum game played
                 on directed graphs, first introduced by Duchet and
                 Meyniel (1993) in the context of graph theory, where
                 one of the players travels along the edges of a graph,
                 while the other modifies the underlying structure by
                 marking vertices. In this paper, we investigate the
                 poison game from the perspective of modal logic, as a
                 natural case study of the use of modal languages
                 equipped with model-changing operators to describe
                 evolving relational structures. In particular, to model
                 the poison game, we consider three memory logics of
                 decreasing expressive power but increasing fit with the
                 game. We begin with ML\emptyset, the basic memory logic
                 restricted to the initial class of models with an empty
                 memory (see Areces et al. 2011). We then identify two
                 fragments of ML\emptyset, which we respectively, denote
                 as PML and PSL, and whose modal operators capture
                 operations on models that mimic more closely the moves
                 of both players. We show that these logics form a chain
                 in expressive power with PML < ML\emptyset, and we
                 introduce suitable notions of bisimulation for the two
                 new logics presented in this paper. We then show that
                 model checking for both PML and PSL is PSPACE-complete.
                 The construction also establishes that determining the
                 existence of a winning strategy in the poison game is
                 PSPACE-hard. We conclude by proving that PML, while
                 strictly less expressive than ML\emptyset, nonetheless
                 has an undecidable satisfiability problem.",
  publisher =    "Springer Singapore",
  address =      "Singapore",
  pages =        "3--23",
  ISBN =         "978-981-15-2220-8",
}