Strategies in Sabotage Games: Temporal and Epistemic Perspectives

Katrine B.P. Thoft; Nina Gierasimczuk

arxiv: 2604.03872 · v1 · submitted 2026-04-04 · 💻 cs.LO · cs.MA

Strategies in Sabotage Games: Temporal and Epistemic Perspectives

Nina Gierasimczuk , Katrine B.P. Thoft This is my paper

Pith reviewed 2026-05-13 16:55 UTC · model grok-4.3

classification 💻 cs.LO cs.MA

keywords sabotage gamesalternating-time temporal logicepistemic logicdynamic graphswinning strategiestemporal propertiesmodal logic

0 comments

The pith

ATL* with epistemic extensions models winning strategies in sabotage games on dynamic graphs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proposes shifting from sabotage modal logic to alternating-time temporal logic with epistemic operators to study games in which one player tries to reach a goal while the other deletes edges from the graph at each step. This lets formulas directly describe sequences of moves and what each player knows about the remaining graph. A sympathetic reader would see the value in obtaining a language that can verify whether a player has a strategy that works against every possible sequence of removals, including cases with incomplete information. The approach also aims to handle general temporal properties that arise when graphs evolve through adversarial changes.

Core claim

The central claim is that ATL* interpreted over alternating game models, together with epistemic modalities for knowledge about the current graph, supplies a complete framework for expressing and reasoning about winning strategies in sabotage games without the need for new axioms beyond those already established for these logics.

What carries the argument

ATL* formulas over two-player game arenas that alternate runner and demon moves, extended with epistemic operators that track each player's information about which edges remain.

If this is right

Formulas can state that the runner possesses a strategy to reach the goal regardless of which edges the demon removes at each turn.
Epistemic operators distinguish strategies that succeed under full visibility from those that succeed when players only know partial information about the graph.
The same language can express other temporal reachability and safety properties that hold for any sequence of adversarial graph changes.
Model-checking procedures already available for ATL* can in principle decide existence of winning strategies for given starting graphs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The framework might transfer directly to model-checking tools used for multi-agent planning under uncertainty.
Similar edge-removal dynamics appear in network interdiction problems, so the logic could supply decision procedures for those domains.
Small explicit examples could be checked by hand or by existing ATL model checkers to compare strategy expressiveness with the original sabotage modal logic.

Load-bearing premise

The standard semantics of ATL* and epistemic logic already suffice to represent the sequential edge deletions and partial information states of sabotage games without losing decidability or completeness.

What would settle it

A concrete finite graph and starting position where an ATL* formula asserts that the runner has a winning strategy, yet exhaustive enumeration of all demon moves shows the runner is blocked.

Figures

Figures reproduced from arXiv: 2604.03872 by Katrine B.P. Thoft, Nina Gierasimczuk.

**Figure 1.** 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. Sabotage game models Labeling functions turn our sabotage game structures into sabotage game models, which will in turn allow interpreting the language of ATL∗ . Definition 3.9. Let (G… view at source ↗

**Figure 2.** Figure 2: Concurrent sabotage game structure rooted in (E,v0). 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 [PITH_FULL_IMAGE:figures/full_fig_p017_2.png] view at source ↗

**Figure 3.** Figure 3: Turn-based sabotage game structure rooted in (E, v0). 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 [PITH_FULL_IMAGE:figures/full_fig_p018_3.png] view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper sketches an ATL* approach to sabotage games but skips the technical verification.

read the letter

The main takeaway is that this paper proposes shifting the analysis of sabotage games from sabotage modal logic to ATL* with epistemic extensions to better handle temporal strategies and player uncertainty. The new angle is treating the game as an alternating-time temporal system where the runner and demon have opposing goals over sequences of moves, with epistemic operators to model what each knows about the changing graph. This could let them reuse existing ATL* model checkers for strategy synthesis in these dynamic settings, which is a practical plus if it works. It does a good job laying out the motivation: sabotage games involve dynamic graphs where edges are removed, and prior modal logic work has been analyzed for complexity and completeness, but a temporal view might capture the step-by-step evolution more naturally. The abstract ties it to broader temporal properties of dynamic graphs. The soft spot is that there's no concrete encoding shown, no example formulas, and no discussion of whether the standard ATL* axioms suffice or if new ones are needed to preserve the game semantics. The concern about potentially losing decidability or completeness from the original logic is reasonable and not addressed here. Without those details, it's hard to tell if the framework actually supports the claimed reasoning about winning strategies. This paper is for logicians and computer scientists working on epistemic game logics and verification of dynamic systems. Someone already familiar with ATL* might see value in the application idea, but it would need the technical development to be useful for most readers. I would send it for peer review to give the authors a chance to fill in the encodings and proofs, as the high-level idea has enough promise to warrant a closer look.

Referee Report

1 major / 0 minor

Summary. The manuscript proposes analyzing sabotage games—where a runner seeks a goal on a dynamic graph while a demon removes edges—using alternating-time temporal logic (ATL*) from a temporal perspective, together with epistemic extensions to model players' uncertainty. It claims this approach supports reasoning about winning strategies and enables study of temporal properties of dynamic graphs more generally, as an alternative or complement to existing sabotage modal logic.

Significance. If a faithful embedding of sabotage-game dynamics into ATL* and its epistemic variants can be established while preserving decidability and completeness, the work would allow reuse of ATL* model-checking tools and results for these games. This could meaningfully extend applications in formal learning and verification of evolving graphs, providing temporal expressiveness that sabotage modal logic lacks.

major comments (1)

Abstract: The central claim that ATL* 'supports reasoning about winning strategies' and preserves key properties of sabotage modal logic rests on an unverified assumption of faithful modeling without new axioms or loss of decidability. No embedding, translation, example encoding, or proof sketch is supplied to substantiate this, rendering the proposal unverifiable from the given text.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful review and constructive feedback. We address the single major comment below and will revise the manuscript accordingly to improve verifiability.

read point-by-point responses

Referee: Abstract: The central claim that ATL* 'supports reasoning about winning strategies' and preserves key properties of sabotage modal logic rests on an unverified assumption of faithful modeling without new axioms or loss of decidability. No embedding, translation, example encoding, or proof sketch is supplied to substantiate this, rendering the proposal unverifiable from the given text.

Authors: We agree that the abstract asserts support for reasoning about winning strategies without supplying an explicit embedding or proof sketch, which leaves the claim insufficiently substantiated in the current text. The manuscript is framed as a conceptual proposal that reuses the established semantics and model-checking results of ATL* (and its epistemic variants) to capture sabotage-game dynamics and player uncertainty. In the revised version we will add a short subsection containing (i) a concrete example encoding of a small sabotage game as an ATL* model, (ii) a high-level translation sketch from game positions and demon/runner moves to ATL* state and strategy quantifiers, and (iii) a brief argument that no new axioms are required and that decidability is inherited from ATL*. These additions will make the central claim verifiable while preserving the paper’s focus on the temporal-epistemic perspective. revision: yes

Circularity Check

0 steps flagged

No circularity: proposal applies existing ATL* without self-referential reductions

full rationale

The paper proposes applying ATL* and epistemic extensions to model sabotage games on dynamic graphs, citing prior analysis of sabotage modal logic for complexity and completeness. No equations, fitted parameters, or derivations appear that reduce to self-definition or self-citation chains. The central claim that the framework supports reasoning about winning strategies is presented as an application of established logics rather than a result derived from inputs within the paper itself. No load-bearing uniqueness theorems or ansatzes are smuggled via self-citation; the work remains self-contained as an exploratory extension.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The proposal rests on the standard semantics of ATL* and epistemic logic; no free parameters, new invented entities, or ad-hoc axioms are introduced in the abstract.

axioms (2)

standard math Standard ATL* semantics for alternating moves and path quantifiers
Invoked implicitly when the paper states that ATL* supports reasoning about winning strategies.
domain assumption Epistemic logic operators can be added to ATL* without breaking its core properties
Assumed when the paper proposes epistemic extensions for player uncertainty.

pith-pipeline@v0.9.0 · 5434 in / 1201 out tokens · 24493 ms · 2026-05-13T16:55:38.504254+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We propose examining the game from a temporal perspective using alternating time temporal logic (ATL∗), and address the players’ uncertainty in its epistemic extensions.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

[1]

Henzinger & Orna Kupferman (2002):Alternating-Time Temporal Logic.Journal of the ACM49, pp

Rajeev Alur, Thomas A. Henzinger & Orna Kupferman (2002):Alternating-Time Temporal Logic.Journal of the ACM49, pp. 672–713, doi:10.1145/585265.585270

work page doi:10.1145/585265.585270 2002
[2]

Guillaume Aucher, Johan van Benthem & Davide Grossi (2018):Modal Logics of Sabotage Revisited.Jour- nal of Logic and Computation28, pp. 269–303

work page 2018
[3]

213–234, doi:10.1007/s10849-022-09359-w

Alexandru Baltag, Dazhu Li & Mina Young Pedersen (2022):A Modal Logic for Supervised Learning.Jour- nal of Logic, Language and Information31(2), pp. 213–234, doi:10.1007/s10849-022-09359-w. Available at https://doi.org/10.1007/s10849-022-09359-w

work page doi:10.1007/s10849-022-09359-w 2022
[4]

In:Logic and the Foundations of Game and Decision Theory (LOFT 7),Lecture Notes in Computer Science2605, Springer, pp

Johan van Benthem (2005):An Essay on Sabotage and Obstruction. In:Logic and the Foundations of Game and Decision Theory (LOFT 7),Lecture Notes in Computer Science2605, Springer, pp. 268–276, doi:10.1007/978-3-540-32254-2_16

work page doi:10.1007/978-3-540-32254-2_16 2005
[5]

CSLI Publications

Johan van Benthem (2010):Modal Logic for Open Minds. CSLI Publications

work page 2010
[6]

Johan van Benthem, Jelle Gerbrandy, Tomohiro Hoshi & Eric Pacuit (2009):Merging Frameworks for Inter- action.Journal of Philosophical Logic38(5), pp. 491–526. Available athttp://www.jstor.org/stable/ 40344078

work page 2009
[7]

Trends in Logic, V ol

Johan van Benthem & Fenrong Liu, editors (2025):Graph Games and Logic Design: Recent Developments and Further Directions. Trends in Logic, V ol. 66, Springer International Publishing, Cham

work page 2025
[8]

Patrick Blackburn & Jerry Seligman (1995):Hybrid Languages.Journal of Logic, Language and Information 4(3), pp. 251–272

work page 1995
[9]

Richard Buchi & Lawrence H

J. Richard Buchi & Lawrence H. Landweber (1969):Solving Sequential Conditions by Finite-State Strategies. Transactions of the American Mathematical Society138, pp. 295–311. Available athttp://www.jstor. org/stable/1994916

work page arXiv 1969
[10]

Henzinger & Nir Piterman (2007):Algorithms for Büchi Games.Infor- mation and Computation205(3), pp

Krishnendu Chatterjee, Thomas A. Henzinger & Nir Piterman (2007):Algorithms for Büchi Games.Infor- mation and Computation205(3), pp. 466–492, doi:10.1016/j.ic.2006.07.003

work page doi:10.1016/j.ic.2006.07.003 2007
[11]

Dantzig & Delbert R

George B. Dantzig & Delbert R. Fulkerson (1956):On the Max-Flow Min-Cut Theorem of Networks. In H. W. Kuhn & A. W. Tucker, editors:Linear Inequalities and Related Systems,Annals of Mathematics Studies38, Princeton University Press, pp. 215–221

work page 1956
[12]

Cam- bridge University Press

Stéphane Demri, Valentin Goranko & Martin Lange (2016):Temporal Logics in Computer Science. Cam- bridge University Press

work page 2016
[13]

E. A. Dinitz, A. V . Karzanov & M. V . Lomonosov (1976):On the structure of a family of minimal weighted cuts in a graph. In:Studies in Discrete Optimization (in Russian), pp. 290–306. Original in Russian

work page 1976
[14]

L. R. Ford & D. R. Fulkerson (1956):Maximal Flow Through a Network.Canadian Journal of Mathematics 8, pp. 399–404

work page 1956
[15]

Velázquez-Quesada (2009):Learning and Teaching as a Game: A Sabotage Approach

Nina Gierasimczuk, Lena Kurzen & Fernando R. Velázquez-Quesada (2009):Learning and Teaching as a Game: A Sabotage Approach. In Xiangdong He, John Horty & Eric Pacuit, editors:Logic, Rationality, and Interaction, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 119–132

work page 2009
[16]

Gomory & T

Ralph E. Gomory & T. C. Hu (1961):Multi-Terminal Network Flows.Journal of the Society for Industrial and Applied Mathematics9(4), pp. 551–570

work page 1961
[17]

In:Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC ’82, Association for Computing Machinery, New York, NY , USA, pp

Yuri Gurevich & Leo Harrington (1982):Trees, automata, and games. In:Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC ’82, Association for Computing Machinery, New York, NY , USA, pp. 60–65, doi:10.1145/800070.802177. Available athttps://doi.org/10.1145/ 800070.802177

work page doi:10.1145/800070.802177 1982
[18]

Dan Gusfield (1990):Very Simple Methods for All Pairs Network Flow Analysis.SIAM Journal on Comput- ing19(1), pp. 143–155. 14Strategies in Sabotage Games

work page 1990
[19]

125–157, doi:10.1023/A:1026185103185

Wiebe van der Hoek & Michael Wooldridge (2003):Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications.Studia Logica75(1), pp. 125–157, doi:10.1023/A:1026185103185

work page doi:10.1023/a:1026185103185 2003
[20]

In:Proceedings of the 33rd Annual ACM Symposium on Theory of Computing, pp

Jacob Holm, Kristian de Lichtenberg & Mikkel Thorup (2001):Poly-logarithmic Deterministic Fully- Dynamic Algorithms for Connectivity, Minimum Spanning Tree, 2-Edge, and Biconnectivity. In:Proceedings of the 33rd Annual ACM Symposium on Theory of Computing, pp. 79–89

work page 2001
[21]

Wojciech Jamroga (2003):Some Remarks on Alternating Temporal Epistemic Logic. In B. Dunin-Keplicz & R. Verbrugge, editors:Proceedings of Formal Approaches to Multi-Agent Systems (FAMAS 2003), pp. 133–139. Early workshop contribution on ATEL semantics and issues

work page 2003
[22]

Karger (1993):Global Min-Cuts in RNC and Other Ramifications of a Simple Mincut Algorithm

David R. Karger (1993):Global Min-Cuts in RNC and Other Ramifications of a Simple Mincut Algorithm. In:Proceedings of the Fourth Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), SIAM, pp. 21–30

work page 1993
[23]

Jon Kleinberg & Éva Tardos (2013):Algorithm Design, New International Edition edition. Pearson

work page 2013
[24]

255–299, doi:10.1007/BF01995674

Ron Koymans (1990):Specifying real-time properties with metric temporal logic.Real-Time Systems2(4), pp. 255–299, doi:10.1007/BF01995674. Available athttps://doi.org/10.1007/BF01995674

work page doi:10.1007/bf01995674 1990
[25]

Technical Report 2015-2, Center for Economic Institutions, Institute of Economic Research, Hitotsubashi University

Dmitriy Kvasov (2015):From sabotage games to border protection. Technical Report 2015-2, Center for Economic Institutions, Institute of Economic Research, Hitotsubashi University. Available athttps:// hit-u.repo.nii.ac.jp/record/2057416/files/wp2015-2.pdf

work page arXiv 2015
[26]

250–254, doi:10.1016/j.orl.2016.02.002

Dmitriy Kvasov (2016):On sabotage games.Operations Research Letters44(2), pp. 250–254, doi:10.1016/j.orl.2016.02.002

work page doi:10.1016/j.orl.2016.02.002 2016
[27]

In:Mathematical Foundations of Computer Science, 2747, pp

Christof Löding & Patrick Rohde (2003):Solving the Sabotage Game Is PSPACE-Hard. In:Mathematical Foundations of Computer Science, 2747, pp. 531–540

work page 2003
[28]

Karl Menger (1927):Zur allgemeinen Kurventheorie.Fundamenta Mathematicae10(1), pp. 96–115. Avail- able athttp://eudml.org/doc/211191

work page 1927
[29]

Petri nets: Properties, analysis and applications

Tadao Murata (1989):Petri Nets: Properties, Analysis and Applications.Proceedings of the IEEE77(4), pp. 541–580, doi:10.1109/5.24143. N. Gierasimczuk & K.B.P . Thoft15 Appendix Proposition 2.5LetG= (V,E)andb∈N +. Runner has a winning strategy inLSG= ((V,E),v 0,b)iff M((E,v 0)),v 0 |=γb, withγ i (fori∈N) given by:γ 1 :=♢⊤,γ n+1 :=♢■γ n. Proof.By induction ...

work page doi:10.1109/5.24143 1989
[30]

there is anr-strategystr r, s.t.M Rtb,λ|=Fgfor allλ∈Plays(S tb(G),v 0,str r)

work page
[31]

there is anr-strategystr r, s.t.M Rtb,λ|=⊤Ugfor allλ∈Plays(S tb(G),v 0,str r)

work page
[32]

for allλ∈Plays(S tb(G),v 0,str r)there isi≥0, s.t.M Rtb,λ[i]|=g

there is anr-strategystr r, s.t. for allλ∈Plays(S tb(G),v 0,str r)there isi≥0, s.t.M Rtb,λ[i]|=g

work page
[33]

for allλ∈Plays(S tb(G),v 0,str r)there isi≥0, s.t.g∈L(λ[i])

there is anr-strategystr r, s.t. for allλ∈Plays(S tb(G),v 0,str r)there isi≥0, s.t.g∈L(λ[i])

work page
[34]

for allλ∈Plays(S tb(G),v 0,str r)there isi≥0, s.t.λ[i] = ((E,v),a) for somea∈Awithv=v g

there is anr-strategystr r, s.t. for allλ∈Plays(S tb(G),v 0,str r)there isi≥0, s.t.λ[i] = ((E,v),a) for somea∈Awithv=v g

work page
[35]

for allλ∈Plays(S tb(G),v 0,str r) there isi≥0, s.t.λ[i] = ((E,v),a)for somea∈Awithv=v g

there is a functionstr r :S tb →Act skip withstr r(s)∈act tb(r,s), s.t. for allλ∈Plays(S tb(G),v 0,str r) there isi≥0, s.t.λ[i] = ((E,v),a)for somea∈Awithv=v g

work page
[36]

for allλ∈Plays(S tb(G),v 0) such thatλ[j+1]∈ {δ tb(λ[j],α)|α∈act tb(λ[j])andstr r(λ[j])⊑α}there is ani≥0, s.t

there is a functionstr r :S tb →Act skip withstr r(s)∈act tb(r,s), s.t. for allλ∈Plays(S tb(G),v 0) such thatλ[j+1]∈ {δ tb(λ[j],α)|α∈act tb(λ[j])andstr r(λ[j])⊑α}there is ani≥0, s.t. λ[i] = ((E,v),a)for somea∈Awithv=v g

work page
[37]

there is a functionstr r :S tb →Act skip withstr r(s)∈act tb(r,s), s.t. for allλ∈Plays(S tb(G),v 0) such that for evenj<length(λ)−1,λ[j+1] =δ tb(λ[j],(str r(λ[j]),skip))and for oddj< length(λ)−1,λ[j+1]∈ {δ tb(λ[j],(skip,e))|e∈Edges(λ[j])}there is ani≥0, s.t.λ[i] = ((E,v),a)for somea∈Awithv=v g

work page
[38]

Namely:win((E ′,v)) =str r((E′,v),r)

there is a functionwin:S(G)→Ethat runner can apply at her choice points k such that whichever remaining edge is removed from, runner retains the connectivity to the goal fromπ 2(win(s))in sk+1. Namely:win((E ′,v)) =str r((E′,v),r). So, runner has a winning strategy in RSG(G,v 0,v g). N. Gierasimczuk & K.B.P . Thoft17 Proposition 3.15Let((V,E),v 0,v g)be a...

work page

[1] [1]

Henzinger & Orna Kupferman (2002):Alternating-Time Temporal Logic.Journal of the ACM49, pp

Rajeev Alur, Thomas A. Henzinger & Orna Kupferman (2002):Alternating-Time Temporal Logic.Journal of the ACM49, pp. 672–713, doi:10.1145/585265.585270

work page doi:10.1145/585265.585270 2002

[2] [2]

Guillaume Aucher, Johan van Benthem & Davide Grossi (2018):Modal Logics of Sabotage Revisited.Jour- nal of Logic and Computation28, pp. 269–303

work page 2018

[3] [3]

213–234, doi:10.1007/s10849-022-09359-w

Alexandru Baltag, Dazhu Li & Mina Young Pedersen (2022):A Modal Logic for Supervised Learning.Jour- nal of Logic, Language and Information31(2), pp. 213–234, doi:10.1007/s10849-022-09359-w. Available at https://doi.org/10.1007/s10849-022-09359-w

work page doi:10.1007/s10849-022-09359-w 2022

[4] [4]

In:Logic and the Foundations of Game and Decision Theory (LOFT 7),Lecture Notes in Computer Science2605, Springer, pp

Johan van Benthem (2005):An Essay on Sabotage and Obstruction. In:Logic and the Foundations of Game and Decision Theory (LOFT 7),Lecture Notes in Computer Science2605, Springer, pp. 268–276, doi:10.1007/978-3-540-32254-2_16

work page doi:10.1007/978-3-540-32254-2_16 2005

[5] [5]

CSLI Publications

Johan van Benthem (2010):Modal Logic for Open Minds. CSLI Publications

work page 2010

[6] [6]

Johan van Benthem, Jelle Gerbrandy, Tomohiro Hoshi & Eric Pacuit (2009):Merging Frameworks for Inter- action.Journal of Philosophical Logic38(5), pp. 491–526. Available athttp://www.jstor.org/stable/ 40344078

work page 2009

[7] [7]

Trends in Logic, V ol

Johan van Benthem & Fenrong Liu, editors (2025):Graph Games and Logic Design: Recent Developments and Further Directions. Trends in Logic, V ol. 66, Springer International Publishing, Cham

work page 2025

[8] [8]

Patrick Blackburn & Jerry Seligman (1995):Hybrid Languages.Journal of Logic, Language and Information 4(3), pp. 251–272

work page 1995

[9] [9]

Richard Buchi & Lawrence H

J. Richard Buchi & Lawrence H. Landweber (1969):Solving Sequential Conditions by Finite-State Strategies. Transactions of the American Mathematical Society138, pp. 295–311. Available athttp://www.jstor. org/stable/1994916

work page arXiv 1969

[10] [10]

Henzinger & Nir Piterman (2007):Algorithms for Büchi Games.Infor- mation and Computation205(3), pp

Krishnendu Chatterjee, Thomas A. Henzinger & Nir Piterman (2007):Algorithms for Büchi Games.Infor- mation and Computation205(3), pp. 466–492, doi:10.1016/j.ic.2006.07.003

work page doi:10.1016/j.ic.2006.07.003 2007

[11] [11]

Dantzig & Delbert R

George B. Dantzig & Delbert R. Fulkerson (1956):On the Max-Flow Min-Cut Theorem of Networks. In H. W. Kuhn & A. W. Tucker, editors:Linear Inequalities and Related Systems,Annals of Mathematics Studies38, Princeton University Press, pp. 215–221

work page 1956

[12] [12]

Cam- bridge University Press

Stéphane Demri, Valentin Goranko & Martin Lange (2016):Temporal Logics in Computer Science. Cam- bridge University Press

work page 2016

[13] [13]

E. A. Dinitz, A. V . Karzanov & M. V . Lomonosov (1976):On the structure of a family of minimal weighted cuts in a graph. In:Studies in Discrete Optimization (in Russian), pp. 290–306. Original in Russian

work page 1976

[14] [14]

L. R. Ford & D. R. Fulkerson (1956):Maximal Flow Through a Network.Canadian Journal of Mathematics 8, pp. 399–404

work page 1956

[15] [15]

Velázquez-Quesada (2009):Learning and Teaching as a Game: A Sabotage Approach

Nina Gierasimczuk, Lena Kurzen & Fernando R. Velázquez-Quesada (2009):Learning and Teaching as a Game: A Sabotage Approach. In Xiangdong He, John Horty & Eric Pacuit, editors:Logic, Rationality, and Interaction, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 119–132

work page 2009

[16] [16]

Gomory & T

Ralph E. Gomory & T. C. Hu (1961):Multi-Terminal Network Flows.Journal of the Society for Industrial and Applied Mathematics9(4), pp. 551–570

work page 1961

[17] [17]

In:Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC ’82, Association for Computing Machinery, New York, NY , USA, pp

Yuri Gurevich & Leo Harrington (1982):Trees, automata, and games. In:Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC ’82, Association for Computing Machinery, New York, NY , USA, pp. 60–65, doi:10.1145/800070.802177. Available athttps://doi.org/10.1145/ 800070.802177

work page doi:10.1145/800070.802177 1982

[18] [18]

Dan Gusfield (1990):Very Simple Methods for All Pairs Network Flow Analysis.SIAM Journal on Comput- ing19(1), pp. 143–155. 14Strategies in Sabotage Games

work page 1990

[19] [19]

125–157, doi:10.1023/A:1026185103185

Wiebe van der Hoek & Michael Wooldridge (2003):Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications.Studia Logica75(1), pp. 125–157, doi:10.1023/A:1026185103185

work page doi:10.1023/a:1026185103185 2003

[20] [20]

In:Proceedings of the 33rd Annual ACM Symposium on Theory of Computing, pp

Jacob Holm, Kristian de Lichtenberg & Mikkel Thorup (2001):Poly-logarithmic Deterministic Fully- Dynamic Algorithms for Connectivity, Minimum Spanning Tree, 2-Edge, and Biconnectivity. In:Proceedings of the 33rd Annual ACM Symposium on Theory of Computing, pp. 79–89

work page 2001

[21] [21]

Wojciech Jamroga (2003):Some Remarks on Alternating Temporal Epistemic Logic. In B. Dunin-Keplicz & R. Verbrugge, editors:Proceedings of Formal Approaches to Multi-Agent Systems (FAMAS 2003), pp. 133–139. Early workshop contribution on ATEL semantics and issues

work page 2003

[22] [22]

Karger (1993):Global Min-Cuts in RNC and Other Ramifications of a Simple Mincut Algorithm

David R. Karger (1993):Global Min-Cuts in RNC and Other Ramifications of a Simple Mincut Algorithm. In:Proceedings of the Fourth Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), SIAM, pp. 21–30

work page 1993

[23] [23]

Jon Kleinberg & Éva Tardos (2013):Algorithm Design, New International Edition edition. Pearson

work page 2013

[24] [24]

255–299, doi:10.1007/BF01995674

Ron Koymans (1990):Specifying real-time properties with metric temporal logic.Real-Time Systems2(4), pp. 255–299, doi:10.1007/BF01995674. Available athttps://doi.org/10.1007/BF01995674

work page doi:10.1007/bf01995674 1990

[25] [25]

Technical Report 2015-2, Center for Economic Institutions, Institute of Economic Research, Hitotsubashi University

Dmitriy Kvasov (2015):From sabotage games to border protection. Technical Report 2015-2, Center for Economic Institutions, Institute of Economic Research, Hitotsubashi University. Available athttps:// hit-u.repo.nii.ac.jp/record/2057416/files/wp2015-2.pdf

work page arXiv 2015

[26] [26]

250–254, doi:10.1016/j.orl.2016.02.002

Dmitriy Kvasov (2016):On sabotage games.Operations Research Letters44(2), pp. 250–254, doi:10.1016/j.orl.2016.02.002

work page doi:10.1016/j.orl.2016.02.002 2016

[27] [27]

In:Mathematical Foundations of Computer Science, 2747, pp

Christof Löding & Patrick Rohde (2003):Solving the Sabotage Game Is PSPACE-Hard. In:Mathematical Foundations of Computer Science, 2747, pp. 531–540

work page 2003

[28] [28]

Karl Menger (1927):Zur allgemeinen Kurventheorie.Fundamenta Mathematicae10(1), pp. 96–115. Avail- able athttp://eudml.org/doc/211191

work page 1927

[29] [29]

Petri nets: Properties, analysis and applications

Tadao Murata (1989):Petri Nets: Properties, Analysis and Applications.Proceedings of the IEEE77(4), pp. 541–580, doi:10.1109/5.24143. N. Gierasimczuk & K.B.P . Thoft15 Appendix Proposition 2.5LetG= (V,E)andb∈N +. Runner has a winning strategy inLSG= ((V,E),v 0,b)iff M((E,v 0)),v 0 |=γb, withγ i (fori∈N) given by:γ 1 :=♢⊤,γ n+1 :=♢■γ n. Proof.By induction ...

work page doi:10.1109/5.24143 1989

[30] [30]

there is anr-strategystr r, s.t.M Rtb,λ|=Fgfor allλ∈Plays(S tb(G),v 0,str r)

work page

[31] [31]

there is anr-strategystr r, s.t.M Rtb,λ|=⊤Ugfor allλ∈Plays(S tb(G),v 0,str r)

work page

[32] [32]

for allλ∈Plays(S tb(G),v 0,str r)there isi≥0, s.t.M Rtb,λ[i]|=g

there is anr-strategystr r, s.t. for allλ∈Plays(S tb(G),v 0,str r)there isi≥0, s.t.M Rtb,λ[i]|=g

work page

[33] [33]

for allλ∈Plays(S tb(G),v 0,str r)there isi≥0, s.t.g∈L(λ[i])

there is anr-strategystr r, s.t. for allλ∈Plays(S tb(G),v 0,str r)there isi≥0, s.t.g∈L(λ[i])

work page

[34] [34]

for allλ∈Plays(S tb(G),v 0,str r)there isi≥0, s.t.λ[i] = ((E,v),a) for somea∈Awithv=v g

there is anr-strategystr r, s.t. for allλ∈Plays(S tb(G),v 0,str r)there isi≥0, s.t.λ[i] = ((E,v),a) for somea∈Awithv=v g

work page

[35] [35]

for allλ∈Plays(S tb(G),v 0,str r) there isi≥0, s.t.λ[i] = ((E,v),a)for somea∈Awithv=v g

there is a functionstr r :S tb →Act skip withstr r(s)∈act tb(r,s), s.t. for allλ∈Plays(S tb(G),v 0,str r) there isi≥0, s.t.λ[i] = ((E,v),a)for somea∈Awithv=v g

work page

[36] [36]

for allλ∈Plays(S tb(G),v 0) such thatλ[j+1]∈ {δ tb(λ[j],α)|α∈act tb(λ[j])andstr r(λ[j])⊑α}there is ani≥0, s.t

there is a functionstr r :S tb →Act skip withstr r(s)∈act tb(r,s), s.t. for allλ∈Plays(S tb(G),v 0) such thatλ[j+1]∈ {δ tb(λ[j],α)|α∈act tb(λ[j])andstr r(λ[j])⊑α}there is ani≥0, s.t. λ[i] = ((E,v),a)for somea∈Awithv=v g

work page

[37] [37]

there is a functionstr r :S tb →Act skip withstr r(s)∈act tb(r,s), s.t. for allλ∈Plays(S tb(G),v 0) such that for evenj<length(λ)−1,λ[j+1] =δ tb(λ[j],(str r(λ[j]),skip))and for oddj< length(λ)−1,λ[j+1]∈ {δ tb(λ[j],(skip,e))|e∈Edges(λ[j])}there is ani≥0, s.t.λ[i] = ((E,v),a)for somea∈Awithv=v g

work page

[38] [38]

Namely:win((E ′,v)) =str r((E′,v),r)

there is a functionwin:S(G)→Ethat runner can apply at her choice points k such that whichever remaining edge is removed from, runner retains the connectivity to the goal fromπ 2(win(s))in sk+1. Namely:win((E ′,v)) =str r((E′,v),r). So, runner has a winning strategy in RSG(G,v 0,v g). N. Gierasimczuk & K.B.P . Thoft17 Proposition 3.15Let((V,E),v 0,v g)be a...

work page