Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Strategies in Sabotage Games: Temporal and Epistemic Perspectives

Nina Gierasimczuk, Katrine B. P. Thoft

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.

Strategies in Sabotage Games: Temporal and Epistemic Perspectives

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), 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.

Paper Structure

This paper contains 14 sections, 9 theorems, 5 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Sabotage games: reachability and liveness
  3. Sabotage Modal Logic
  4. Temporal perspective on sabotage games
  5. Sabotage game structures
  6. Structural labeling functions and computations
  7. Sabotage game models
  8. Alternating-time Temporal Logic, ATL$^\ast$
  9. Existence of winning strategies in Reachability Sabotage Games
  10. Existence of winning strategies in Liveness Sabotage Games
  11. Sabotage games and the minimum cut of a graph
  12. Angelic Sabotage Games
  13. Knowledge in Sabotage Games
  14. Conclusions and future work

Key Result

Proposition 2.4

Let $G=(V,E)$ with $|E|=k$. Runner has a winning strategy in $RSG$$((V,E),v_0,v_g)$ iff $M(s^0),v_0\models \rho_k$, where $\rho_i$ (for $i\in \mathbb{N}$) is defined inductively as $\rho_0:=g, \ \rho_{n+1}:= g\vee \lozenge\blacksquare\rho_n$.The proof of this proposition, together with different int

Figures (3)

  • 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.
  • Figure 2: Concurrent sabotage game structure rooted in $(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,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

Theorems & Definitions (38)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Proposition 2.4: Benthem:2005
  • Proposition 2.5
  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Definition 3.4
  • Proposition 3.5
  • ...and 28 more