cs.LOApr 4, 2026

Strategies in Sabotage Games: Temporal and Epistemic Perspectives

Authors: Nina Gierasimczuk, Katrine B. P. Thoft

Organizations: Technical University of Denmark Kgs. Lyngby, Denmark

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

Sabotage games are played on a dynamic graph, in which one agent, called a runner, attempts to reach a goal state, while being obstructed by a demon who at each round removes an edge from the graph. Sabotage modal logic was proposed to carry out reasoning about such games. Since its conception, it has undergone a thorough analysis (in terms of complexity, completeness, and various extensions) and has been applied to a variety of domains, e.g., to formal learning. In this paper, we propose examining the game from a temporal perspective using alternating time temporal logic (ATL∗^\ast), and address the players' uncertainty in its epistemic extensions. This framework supports reasoning about winning strategies for those games, and opens ways to address temporal properties of dynamic graphs in general.

Figures & tables

Figure 1: A play of a concurrent sabotage game structure. The circle marks the runner’s position in the graph, the consecutive game-states (b) and (c) are produced by a joint action of runner and demon executed in the previous state.
Type of RSGImplied winnerSML formula ( ρk\rho_{k} , k=∣E∣k=|E| )ATL formula
RSGEURSG^{EU}runnerρ0:=g, ρn+1:=g∨◊■ρn\rho_{0}:=g,\ \rho_{n+1}:=g\vee\lozenge\blacksquare\rho_{n} [ 27 ]⟨ ⁣⟨{r}⟩ ⁣⟩Fg\langle\!\langle\{r\}\rangle\!\rangle Fg
RSGEHRSG^{EH}runner and demonρ0:=g, ρn+1:=g∨◊⧫ρn\rho_{0}:=g,\ \rho_{n+1}:=g\vee\lozenge\blacklozenge\rho_{n} [ 11 ]⟨ ⁣⟨{r,d}⟩ ⁣⟩Fg\langle\!\langle\{r,d\}\rangle\!\rangle Fg
RSGUHRSG^{UH}demonρ0:=g, ρn+1:=g∨(◊⊤∧□⧫ρn)\rho_{0}:=g,\ \rho_{n+1}:=g\vee(\lozenge\top\wedge\square\blacklozenge\rho_{n}) [ 11 ]⟨ ⁣⟨{d}⟩ ⁣⟩Fg\langle\!\langle\{d\}\rangle\!\rangle Fg
RSGUURSG^{UU}runner and demonρ0:=¬g, ρn+1:=¬g∨◊⧫ρn\rho_{0}:=\neg g,\ \rho_{n+1}:=\neg g\vee\lozenge\blacklozenge\rho_{n}⟨ ⁣⟨{r,d}⟩ ⁣⟩¬Fg\langle\!\langle\{r,d\}\rangle\!\rangle\neg Fg
Table 1: Comparison of SML and ATL formulae expressing winning conditions in sabotage games with various incentives
Figure 2: Concurrent sabotage game structure rooted in (E,v0)(E,v_{0}) . Red circle marks runner’s position in a game-state. Each transition corresponds to a concurrent action in a game-state. Note that whenever both agents choose the same edge in a joint concurrent move, the action is canceled, hence the reflexive arrows. It is easy to see there are finite and infinite plays
Figure 3: Turn-based sabotage game structure rooted in (E,v0)(E,v_{0}) . Red circle marks the runner’s position in a state. The control over the levels of the structure alternates between runner and demon, starting with runner at the top
More in this topic

Imperfect-Information Games

Imperfect-information games study strategic decisions when players have private information or cannot fully observe the state or actions.

See all 88 papers

Explore similar work

CardsList

  1. Alternating-Time Temporal Logic with Mean-Payoff Guarantees

    Aug 2, 2026Muhammad NajibGame TheoryFormal Verification

    Heriot-Watt University, Edinburgh, UK

  2. I Would If I Could: Reasoning about Dynamics of Actions in Multi-Agent Systems

    Apr 28, 2026Rustam Galimullin, Hermine Grosinger, Munyque MittelmannMulti-Agent SystemsMulti-Agent Reasoning

    University of Bergen, Bergen, Norway · Örebro University, Örebro, Sweden · CNRS, UMR 7030, F-93430, Villetaneuse, France +1

  3. An Algebraic Framework for Quantitative Semantics of Spatio-Temporal Logic with Graph Operators

    Jun 25, 2026Sheryl Paul, Vidisha Kudalkar, Anand Balakrishnan +3Signal Temporal LogicMulti-Agent Systems

    University of Southern California, Los Angeles, CA, USA · University of Texas at Austin, Austin, TX, USA · ETH Zürich, Zürich, Switzerland