Logic of the Hide and Seek Game: Characterization, Axiomatization, Decidability

Authors: Qian Chen and Dazhu Li
Published on: Dynamic Logic. New Trends and Applications 2023.

The logic of the hide and seek game $\mathsf{LHS}$ was proposed to reason about search missions and interactions between agents in pursuit-evasion environments. As proved in [Li, 2021], having an equality constant in the language of $\mathsf{LHS}$ drastically increases its computational complexity: the satisfiability problem for $\mathsf{LHS}$ with multiple relations is undecidable. In this work, we improve the existing proof for the undecidability by showing that $\mathsf{LHS}$ with a single relation is undecidable. With the findings of [Li, 2021], we provide a van Benthem style characterization theorem for the expressive power of the logic. Finally, by ‘splitting’ the language of $\mathsf{LHS}^-$, a crucial fragment of $\mathsf{LHS}$ without the equality constant, into two `isolated parts’, we provide a complete Hilbert style proof system for $\mathsf{LHS}^-$ and prove that its satisfiability problem is decidable, whose proofs would indicate significant differences between the proposals of $\mathsf{LHS}^-$ and of ordinary product logics. Although $\mathsf{LHS}$ and $\mathsf{LHS}^-$ are frameworks for interactions of 2 agents, all results in the article can be easily transferred to their generalizations for settings with any $n>2$ agents.