Paper deep dive
Strategies in Sabotage Games: Temporal and Epistemic Perspectives
Nina Gierasimczuk, Katrine B. P. Thoft
Intelligence
Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 93%
Last extracted: 4/10/2026, 1:57:47 AM
Summary
This paper introduces a formal framework for analyzing sabotage games—dynamic graph games where a runner attempts to reach a goal while a demon removes edges—by integrating Alternating-time Temporal Logic (ATL*) and epistemic extensions. It defines turn-based, concurrent, and general sabotage game structures, providing a unified logical approach to strategic temporal reasoning and imperfect information in dynamic graphs.
Entities (5)
Relation Signals (3)
Runner → playsagainst → Demon
confidence 100% · one agent, called a runner, attempts to reach a goal state, while being obstructed by a demon
Sabotage Games → reconstructedin → Alternating-time Temporal Logic (ATL*)
confidence 95% · we reconstruct Sabotage Games in Alternating-time Temporal Logic setting
Sabotage Games → analyzedusing → Sabotage Modal Logic (SML)
confidence 90% · Sabotage modal logic was proposed to carry out reasoning about such games.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2604.03872v1
- Canonical: https://arxiv.org/abs/2604.03872v1
Trouble viewing inline? Open PDF directly →
Full Text
78,847 characters extracted from source content.
Expand or collapse full text
Strategies in Sabotage Games: Temporal and Epistemic Perspectives Nina Gierasimczuk Katrine B. P. Thoft Technical University of Denmark Kgs. Lyngby, Denmark 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. 1 Introduction Many real-world problems can be modelled as graphs undergoing structural changes. A common example is the connectivity of a train transportation network: Can I reach Copenhagen from Amsterdam despite a train connection being cancelled? Being able to answer such questions is crucial for making sense of agents’ behaviour in a network. Sabotage games are an abstract model of such scenarios: one player (the runner) attempts to reach a specified target vertex in a graph, while an adversary (the blocker) removes edges in the graph. Traditionally, sabotage games have been analyzed using Sabotage Modal Logic (SML) introduced in [27, 22]. Returning to our train network example, in SML the possibility of travelling to Copenhagen (CphCph) from Amsterdam, after a cancellation of a train connection, is expressed as ◆◆Cph Cph being true while in Amsterdam, which says: after a deleting an arbitrary edge in the train network, there will (still) be a connection between Amsterdam and Copenhagen. The elegant approach of SML does not account of temporal and epistemic aspects of sabotage games (see [28]). The overall aim of this paper is to provide a unified logical framework where the strategic temporal reasoning native to Alternating-time Temporal Logic (ATL, [1]), and the adversarial structural change in SML interact, in order to study how sabotage unfolds over time in dynamic games with imperfect information. The paper proceeds as follows. In Section 2 we present Sabotage Games: the classical (reachability) version and the newly introduced liveness sabotage game. We also present SML characterizations of the existence of winning strategies. In Section 3 we reconstruct Sabotage Games in Alternating-time Temporal Logic setting, as sabotage game structures, and we show how to express the existence of winning strategies ATL∗. We also discuss how the strategic temporal setting of ATL∗ allows expressing the graph-theoretical notion of (dynamic) minimal s−ts-t cut of a graph. We also discuss an extension to angelic sabotage games that feature the addition of edges. In Section 4, we show how the epistemic extension of ATL can be used to reason about knowledge of strategic ability in sabotage games. Finally, in Section 5, we conclude and outline several directions of future work. 2 Sabotage games: reachability and liveness The classic sabotage game was first introduced in [27] and [22] as a turn-based two-player game (G,v0,vg)(G,v_0,v_g) played on a graph G=(V,E)G=(V,E), with v0,vg∈Vv_0,v_g∈ V being some pre-specified start and goal vertices. The first player in the game is the runner, who is positioned at the designated start vertex and continues moving along the edges of the graph until she reaches either the goal vertex vgv_g or she arrives at a dead-end. The runner can move along exactly one edge in each turn. The second player is the demon (often called ‘blocker’), who acts as a saboteur and, in each turn, removes an arbitrary edge from the graph. Since the aim of the runner is to reach the goal, in this paper we will call such games reachability sabotage games (RSG, for short). Motivated by concurrency theory [24, 6], apart from the the RSGs, in this paper we introduce and study another variant of the game: liveness sabotage games (LSG, for short). Instead of the pre-specified goal vertex, LSG has a liveness parameter b∈ℕb , that denotes the number of moves the runner should (at least) be able to make before she gets completely blocked by the demon, i.e., a lower bound of how long the runner can stay ‘alive’. An LSG is then specified by (G,v0,b)(G,v_0,b), where G=(V,E)G=(V,E), v0∈Vv_0∈ V is the start vertex, and b is the liveness parameter. Throughout this paper we will assume the underlying G=(V,E)G=(V,E) to be a directed graph with V and E non-empty, we designate some v0∈Vv_0∈ V to be the starting vertex and sometimes vg∈Vv_g∈ V to be the goal vertex. We will use |⋅||·| to denote the cardinality of a set. We will also assume a fixed enumeration of vertices from V∖v0V \v_0\, (vi)i∈1,…,|V|−1(v_i)_i∈\1,…,|V|-1\, and a fixed enumeration of edges from E, (ej)j∈1,…,|E|(e_j)_j∈\1,…,|E|\. The sabotage game proceeds through a sequence of game-states—each can be characterized by a set of (remaining) edges and a distinguished vertex corresponding to runner’s current position. Definition 2.1. The set of sabotage game-states of G=(V,E)G=(V,E) is (G)=(E′,v)∣E′⊆E,v∈VS(G)=\(E ,v) E E,v∈ V\.111Whenever G is clear from context, we will drop the argument G and refer to the set of game-states with S. A sabotage play is a specific sequence of such game-states. Definition 2.2. Let G=(V,E)G=(V,E) and v0∈Vv_0∈ V be a starting vertex. A strictly turn-based sabotage v0v_0-play is a sequence of game-states s0,…,sns^0,…,s^n, such that s0=(E0,v0)s^0=(E^0,v^0) is given by (E,v0)(E,v_0), and for any k, such that 0<k≤n0<k≤ n: sk=(Ek−1,vk), s.t. (vk−1,vk)∈Ek−1if k odd,(Ek−1∖(x,y),vk−1), s.t. (x,y)∈Ek−1otherwise.s^k= cases(E^k-1,v^k), s.t. (v^k-1,v^k)∈ E^k-1&if k odd,\\ (E^k-1 \(x,y)\,v^k-1), s.t. (x,y)∈ E^k-1&otherwise.\\ cases A sabotage match is a sabotage play whose final game-state is the first one in the play that satisfies the winning conditions of the game, different for reachability and liveness versions of the game. Definition 2.3. A turn-based sabotage match is a turn-based sabotage play s0,…,sns^0,…,s^n, with sn=(En,vn)s^n=(E^n,v^n) such that: 1. for RSGRSG (G,v0,vg)(G,v_0,v_g): for all k<nk<n we have vk≠vgv^k≠ v_g, and either vn=vgv^n=v_g (i.e., runner wins), or vn≠vgv^n≠ v_g and there is no v∈Vv∈ V such that (vn,v)∈En(v^n,v)∈ E^n (i.e., demon wins); 2. for LSGLSG (G,v0,b)(G,v_0,b): either n≥bn≥ b (runner wins), or n<bn<b and there is no v∈Vv∈ V such that (vn,v)∈En(v^n,v)∈ E^n (i.e., demon wins). Sabotage Modal Logic After establishing some preliminary intuitions about reachability and liveness turn-based sabotage games, we are now ready to talk about the logic customarily used to describe them. Let us briefly recall the classical Sabotage Modal Logic (SML, [27, 22]). SML Syntax Let Φ be a finite set of propositions and p∈Φp∈ . The syntax of SML is given by: φ::=⊤|p|¬φ|φ∧φ|◆φ|◆φ ::= \,|\,p\,|\, \,|\, \,|\, \,|\, . Standardly, we will also use ⊥ for ¬⊤ , φ∨ψ ψ for ¬(¬φ∧¬ψ) ( ψ), □φ for ¬◆¬φ , and ■φ for ¬◆¬φ . As usual, the formula ◆φ stands for the possibility of transitioning to an accessible vertex where φ holds. The ◆ -operator, the sabotage modality, denotes the removal of an arbitrary edge in the graph. SML Semantics The language of SML is interpreted over sabotage models M=(W,R,Val)M=(W,R, Val), where W is a finite non-empty set of worlds, R⊆W×WR W× W is a binary relation over W, and Val:Φ→(W) Val: (W). The truth of the formulas of SML is defined locally at pairs (M,s)(M,s). Let M=(W,R,Val)M=(W,R, Val) be a sabotage model, v∈Wv∈ W and p∈Φp∈ . The clauses for the standard ML part of the language are as usual, and for ◆ we have: M,v⊧◆φ iff there is a (x,y)∈R s.t. M(x,y)−,v⊧φ,M,v iff there is a (x,y)∈ R s.t. M^-_(x,y),v , where M(x,y)−M^-_(x,y) is the updated model after deleting an edge between x and y, i.e., M(x,y)−=(W,R∖(x,y),V)M^-_(x,y)=(W,R \(x,y)\,V). In other words, the formula ◆φ is true in a model M and a state v if, after removing some edge, φ is true at the resulting model at the state v. SML can be used to express properties of sabotage games. Let the set of propositions be Φ=r,g =\r,g\. Any game-state s=(E,v)s=(E,v) of a sabotage game can be transformed into a sabotage model M(s)=(V,E,Val)M(s)=(V,E, Val), where Val(r)=v Val(r)=\v\, and (in the case of RSGRSG where a goal vertex is specified) Val(g)=vg Val(g)=\v_g\. Intuitively speaking, g labels the goal vertex, and r stands for the current position of the runner.222Since these propositions are true in unique worlds, they can be seen as index propositions of hybrid logic (see, e.g., [4]). Note however that multiple worlds making g and r true could, in a natural way, represent distributed goals and multiple runners. In [27], it was observed that, given this represention, SML allows expressing the existence of a winning strategy for the runner starting at the initial vertex v0v_0. Proposition 2.4 ([27]). Let G=(V,E)G=(V,E) with |E|=k|E|=k. Runner has a winning strategy in RSGRSG ((V,E),v0,vg)((V,E),v_0,v_g) iff M(s0),v0⊧ρkM(s^0),v_0 _k, where ρi _i (for i∈ℕi ) is defined inductively as ρ0:=g,ρn+1:=g∨◆■ρn _0:=g,\ _n+1:=g _n.333The proof of this proposition, together with different interpretations and variations of this game can be found in [11]. A similar SML characterization be obtained for our newly introduced liveness sabotage game. Proposition 2.5. Let G=(V,E)G=(V,E) and b∈ℕ+b ^+. Runner has a winning strategy in LSG=((V,E),v0,b)LSG=((V,E),v_0,b) iff M((E,v0)),v0⊧γbM((E,v_0)),v_0 _b, with γi _i (for i∈ℕi ) given by: γ1:=◆⊤,γn+1:=◆■γn. _1:= ,\ _n+1:= _n.444The proofs of propositions can be found in Appendix. The alternating structure of the modal prefix in the formulae used in Prop. 2.4 and 2.5 is specific to strictly turn-based sabotage games. While expressing the winning conditions for different sequences of moves (e.g., allowing several moves of runner before demon moves), can be easily expressed in SML by iterating modalities of one kind, but each such protocol requires a different SML formula. To gain a more general perspective, it would be useful to be able to refer the strategies directly in the logical language. The inductively defined formulae ρ and γ indicate that interesting properties of sabotage games hide in the time-progression of the game. After all, in theoretical computer science, ‘reachability’ (as in RSG) and ‘liveness’ (as in LSG) are considered temporal properties. All this motivates the use of temporal logic to study sabotage games. Our focus on Alternating-time Temporal Logic is additionally justified by a limitation of the traditional approach—simultaneous moves of the players are beyond the scope of SML. 3 Temporal perspective on sabotage games In ATL and ATL∗, branching-time logic is enriched with strategic operators that allow quantifying over paths (or plays) resulting from players’ strategies. ATL∗ is a multi-agent extension of CTL∗ (just as ATL is a multi-agent extension of CTL). We will now reconstruct sabotage games in the setting of alternating time temporal logic ATL∗, as sabotage game structures. Intuitively, the main difference with sabotage models is that the states of the sabotage game structures represent the whole game-state, rather than a concrete vertex in the graph. Sabotage game structures We will distinguish two basic kinds of sabotage games: strictly turn-based (just as the classical sabotage game discussed in Section 2) and concurrent (in which the agents move simultaneously). Two componenents will be fixed and the same across the different types: the set of agents containing runner and demon, =r,dAG=\r,d\, and the set of actions. The crucial observation about sabotage games is that both players act on the edges of the graph. Of course, their actions have different effects: the demon choosing an edge results in a deletion of that edge, while the runner choosing an edge results in updating the runners position in the graph. We will then take the set of action to be Act=e∣e∈EAct=\e e∈ E\ (when we allow an agent to be inactive, we will extend the set with a special skip-symbol: Actskip=Act∪skipAct^skip=Act∪\ skip\). We will address the qualitative difference between the outcomes of the two players edge-choices when defining the transition function. To be able to ‘extract’ vertices from our edge-notation we will at times use the projection function, so that if e=(x,y)e=(x,y), then π1(e)=x _1(e)=x and π2(e)=y _2(e)=y. Definition 3.1. A turn-based (tb-)sabotage game structure based on G=(V,E)G=(V,E) is a tuple: tb(G)=(,Actskip,Stb,acttb,δtb),S tb(G)=(AG,Act skip,S tb,act tb,δ tb), where: Stb=(G)×S tb=S(G)×AG is a finite set of (duplicated) game-states, each labeled with either runner or demon; acttb:×Stb→(Act)act tb:AG× S tb (Act) is the function that determines which actions are allowed to be performed by each agent in a game-state. Specifically, given a state t=((E′,v),a)t=((E ,v),a): • if a=ra=r, then acttb(r,t)=e∈E′∣π1(e)=vact tb(r,t)=\e∈ E _1(e)=v\ and acttb(d,t)=skipact tb(d,t)=\ skip\; • if a=da=d, then acttb(d,t)=E′act tb(d,t)=E and acttb(r,t)=skipact tb(r,t)=\ skip\; Finally, δtbδ tb is a transition function that assigns to any t=((E′,v),a)t=((E ,v),a) in StbS tb and action profile (er,ed)(e_r,e_d), such that ei∈act(i,t)e_i∈ act(i,t) for i∈r,di∈\r,d\, a unique successor state: δtb(t,(er,ed))=((E′∖ed,v),r)if er=skip;((E′,π2(er)),d)otherwise.δ tb(t,(e_r,e_d))= cases((E e_d,v),r)&if e_r= skip;\\ ((E , _2(e_r)),d)&otherwise. cases The above definition enforces the ‘turn-based’ form by marking states with their ‘owners’. Then, the ‘forced’ skip is used by runner in a game-state owned by demon (and vice versa). The ATL-framework is naturally well-suited to analyze concurrent game structures, which formalize situations were players (attempt to) move simultaneously. We will assume that the conflicting choice of selecting the same edge results in mutual cancellation and has no effect. Definition 3.2. A concurrent (con-)sabotage game structure based on a graph G=(V,E)G=(V,E) is a tuple: con(G)=(,Act,Scon,actcon,δcon),S con(G)=(AG,Act,S con,act con,δ con), where: Scon=(G)S con=S(G); actcon:×Scon→(Act)act con:AG× S con (Act), s.t. given an s=(E′,v)s=(E ,v): act(d,s)=E′act(d,s)=E , and act(r,s)=e∈E′∣π1(e)=vact(r,s)=\e∈ E _1(e)=v\; δconδ con is a transition function assigning to s and action profile (er,ed)(e_r,e_d), s.t. ei∈act(i,s)e_i∈ act(i,s) (for i∈r,di∈\r,d\) a unique state: δcon((E,v),(e,e′))=(E,v)if e=e′;(E∖e′,π2(e))otherwise.δ con((E,v),(e,e ))= cases(E,v)&if e=e ;\\ (E \e \, _2(e))&otherwise. cases S tb and S con enforce the agents to enact a very strict protocol of moves, with the skip-action used in to account for an agent ‘making way’ for the other to move in a turn-based game. We can also use a skip-type of action to allow for the active choice of ‘doing nothing’. This would enable us to simulate any order of play: agents taking turns strictly, acting concurrently, but also many other scenarios, for instance: one agent making a couple of moves while the other does nothing, or both agents moving simultaneously for a while, before entering the stage of indefinite inactivity. We will now define such a general sabotage game structure. Definition 3.3. A general (gen-)sabotage games structure based on a graph G=(V,E)G=(V,E) is gen(G)=(,Actskip,Sgen,actgen,δgen),S gen(G)=(AG,Act skip,S gen,act gen,δ gen), where Sgen=(G)S gen=S(G); for any agent i∈i and game-state s∈Sgens∈ S gen, actgen(i,s)=actcon(i,s)∪skipact gen(i,s)=act con(i,s)∪\ skip\; and the transition function δgenδ gen is defined as follows: δgen((E,v),(e,e′))=(E,v)if e=e′;(E∖e′,v)if e≠e′and e=skip;(E,π2(e))if e≠e′and e′=skip;(E∖e′,π2(e))otherwise.δ gen((E,v),(e,e ))= cases(E,v)&if e=e ;\\ (E \e \,v)&if e≠ e and e= skip;\\ (E, _2(e))&if e≠ e and e = skip;\\ (E \e \, _2(e))&otherwise. cases In S gen, at each game-state s each agent can choose to do noting or to make a move. That joint choice will result in either the game progressing to a new state t, in which the position or the set of edges (or both) are updated, or the game remaining in s (if the agents choose the same edge or both decide to skip).555Illustrations of the three kinds of sabotage game structures are given in Appendix B. All of the above sabotage games structures assume the usual asymmetry between the powers of the players: demons’ choices are global (demon can pick any edge in the graph at any round), and runner’s actions are local (runner can only pick an edge sourced at the runner’s current position). In our setting, this is rendered in the following way: for any x∈,, x∈\ tb, con, gen\, and any s∈Sxs∈ S x, actx(r,s)⊆actx(d,s)act x(r,s) act x(d,s). Definition 3.4. Given x∈,, x∈\ tb, con, gen\, a play λ in x(G)S x(G) is a maximal sequence of game-states s0,s1,…s_0,s_1,…, such that for all i≥0i≥ 0, sis_i is a δxδ x-successor of si−1s_i-1 in x(G)S x(G); λ[i]λ[i] is the i-th state in λ; λ[i,j]λ[i,j] is the finite segment λ[i],…,λ[j]λ[i],…,λ[j], which is also called a ‘history’ and denoted by h (with last[h]last[h] being the last element in h, and length[h]length[h] being the length of h);666Note that the lengthlength will be also applied to finite plays. λ[i,∞]λ[i,∞] is the suffix λ[i],λ[i+1],…λ[i],λ[i+1],…; if λ[0]=sλ[0]=s, λ is called s-play. The set of all plays of x(G)S x(G) will be denoted by Plays(x(G))Plays(S x(G)), and the set of all s-plays of x(G)S x(G) by Plays(x(G),s)Plays(S x(G),s). Proposition 3.5. Let G=(V,E)G=(V,E) be a graph. (1.) Plays(tb(G))Plays(S tb(G)) is a finite set of plays of finite length. (2.) For any λ∈Plays(con(G))λ∈ Plays(S con(G)), there is a λ′∈Plays(gen(G))λ ∈ Plays(S gen(G)), s.t. for all i<length(λ)i<length(λ), λ[i]=λ′[i]λ[i]=λ [i]. (3.) Plays(con(G))Plays(S con(G)) and Plays(gen(G))Plays(S gen(G)) are infinite and contain infinite plays. Structural labeling functions and computations Labeling functions assign propositions to game-states in sabotage game structures. Given a graph G=(V,E)G=(V,E), we define the set of graph propositions which includes one dedicated proposition for each vertex, and one proposition for each edge in G, i.e., ΦG=ΦV∪ΦE ^G= ^V∪ ^E, where ΦV=pi∣vi∈V ^V=\p_i v_i∈ V\ and ΦE=qi∣ei∈E ^E=\q_i e_i∈ E\. Intuitively, the elements of ΦG ^G will account for the position of the runner and the remaining edges at a given game-state. Definition 3.6. A structural labeling function :(G)→(ΦG)L:S(G) ( ^G) is defined as ((E′,v))=qi∣ei∈E′∪pi∣v=viL((E ,v))=\q_i e_i∈ E \∪\p_i v=v_i\. A structural computation of a sabotage game structure (G)S(G) is a sequence (λ[0])L(λ[0]), (λ[1]),…L(λ[1]),… such that λ∈Plays((G))λ∈ Plays(S(G)). Proposition 3.7. (1.) For any λ∈Plays(tb(G),((E,v),r))λ∈ Plays(S tb(G),((E,v),r)) and an odd i<length(λ)i<length(λ), (λ[i])≠(λ[i+1])L(λ[i]) (λ[i+1]). (2.) For any λ∈Plays(tb(G))λ∈ Plays(S tb(G)), there is a λ′∈Plays(gen(G))λ ∈ Plays(S gen(G)), such that for all i<length(λ)i<length(λ), (λ[i])=(λ′[i])L(λ[i])=L(λ [i]). While the set of turn-based computations and the set of concurrent computations are in general incomparable, we can easily see that any (different from the predecessor) game-state reachable in the concurrent game structure is reachable in the turn-based game, only it takes two steps instead of one. Example 3.8. Consider a graph G=(V,E)G=(V,E) such that V=0,1,2V=\0,1,2\ and E=(0,1),(0,2),(1,2)E=\(0,1),(0,2),(1,2)\, and the runner starts in 0, see Fig. 1a. Runner and demon now choose an edge each—if this joint action contains the same edge twice (runner moves on the edge the demon attempts to delete), it will have no effect. Fig. 1b, shows the effect of a harmonious choice: runner moves from 0 to 11, while demon deletes (0,2)(0,2). Next, runner moves to 22 and demon deletes the edge (0,1)(0,1), Fig. 1c. The the runner is now stuck in v2v_2 so he has no executable action and the concurrent play ends. This play is not a play in turn-based structure, but it can be transformed into one by ‘unraveling’ every concurrent action profile (er,ed)(e_r,e_d) into a sequence of action profiles in a turn-based play: (er,skip),(skip,ed)(e_r, skip),( skip,e_d). 02211 (a) 02211 (b) 02211 (c) 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,v0,b)(G,v_0,b) be an LSG, and x∈tb,con,gen x∈\ tb, con, gen\. A liveness x-sabotage game model is Lx(G)=(x(G),)M^L x(G)=(S x(G),L), where x(G)S x(G) is an x-sabotage game structure based on G and :Sx→(ΦG)L:S x ( ^G) is the structural labeling function, as in Def. 3.6. Let (G,v0,vg)(G,v_0,v_g) be an RSG, and x∈tb,con,gen x∈\ tb, con, gen\. A reachability x-sabotage game model is Rx(G,vg)=(x(G),g)M^R x(G,v_g)=(S x(G),L^g), where x(G)S x(G) is an x-sabotage game structure and g:Sx→(ΦG∪g)L^g:S x ( ^G∪\g\), such that for any s∈Sxs∈ S x, g(s)=(s)∪gL^g(s)=L(s)∪\g\ if vg=v_g=v, and g(s)=(s)L^g(s)=L(s) otherwise.777When G and vgv_g is clear from context, we will write LxM^L x instead of Lx(G)M^L x(G), and RxM^R x instead of Rx(G,vg)M^R x(G,v_g). Alternating-time Temporal Logic, ATL∗ Let us recall the setting of ATL∗ (following the standard approach in [8]). We will interpret its language on sabotage game models. Definition 3.10 (Syntax of ATL∗). Let Φ be a set of propositions, p∈Φp∈ , and let AG be a set of agents with C⊆C . The syntax of ATL∗ is given by: φ::=⊤|p|¬φ|φ∧φ|Xφ|Gφ|φUφ|⟨C⟩φ ::= \,|\,p\,|\, \,|\, \,|\,X \,|\,G \,|\, U \,|\, \! C \! . We also define Fφ:=⊤UφF := U , ⟦C⟧φ:=¬⟨C⟩¬φ C := \! C \! , and ⊥ as ¬⊤ . We will interpret the language ATL∗ on sabotage models, using the standard ATL∗ semantics. The formulae are interpreted on states and plays of a sabotage game model. Accordingly, a distinction between state and path formulae is made, with state formulae given by: φ::=⊤|p|¬φ|φ∧φ|⟨C⟩γ ::= \,|\,p\,|\, \,|\, \,|\, \! C \! γ, and path formulae by: γ::=φ|¬γ|γ∧γ|Xγ|Gγ|γUγ::= \,|\, γ\,|\,γ γ\,|\,Xγ\,|\,Gγ\,|γ Uγ. Definition 3.11. A positional strategy in xS x of a∈a is stra:Sx→Actskipstr_a:S x→ Act skip, s.t. stra(s)∈acttb(a,s)str_a(s)∈ act tb(a,s). We will refer to any C⊆C as coalition C. A strategy in xS x for a coalition C is a tuple of strategies, one for every a∈Ca∈ C. The set of executable action profiles at s is actx(s)=Πa∈actx(a,s)act x(s)= _a act x(a,s). A C-action is a tuple αC _C such that αC(a)∈actx(a,s) _C(a)∈ act x(a,s) for every a∈Ca∈ C, and αC(a′)=#a′ _C(a )=\#_a for every a′∉Ca ∉ C. An action profile α∈actx(s)α∈ act x(s) extends a C-action αC _C, denoted αC⊑α _C α, if α(a)=αC(a)α(a)= _C(a) for every a∈Ca∈ C. The outcome set of the C-action, αC _C at s in xS x is the set of states postx(s,αC):=δx(s,α)∣α∈actx(s) and αC⊑αpost_S x(s, _C):=\δ x(s,α) α∈ act x(s) and _C α\. Finally, the set of plays that can be realized by C when following the strategies in C str_C is defined as: Plays(x(G),s,C):=λ∈Plays(x(G),s)∣λ[j+1]∈postx(λ[j],C) for all j<length(λ)Plays(S x(G),s, str_C):=\λ∈ Plays(S x(G),s) λ[j+1]∈ post_S x(λ[j], str_C) for all j<length(λ)\. Definition 3.12. Let yxM yx be a sabotage game model with y∈R,L y∈\ R, L\ and x∈tb,con,gen x∈\ tb, con, gen\, s a game-state in SxS x, λ∈Plays(x(G))λ∈ Plays(S x(G)) and let Φ be a set of propositions with p∈Φp∈ . The semantics ATL∗ is defined inductively for the state and path formulae in the following way: State formulae: yx,s⊧pM yx,s p iff p∈g(s)p ^g(s), for all p∈Φp∈ yx,s⊧¬φM yx,s iff yx,s⊧̸φM yx,s yx,s⊧φ∧ψM yx,s ψ iff yx,s⊧φM yx,s and yx,s⊧ψM yx,s ψ yx,s⊧⟨C⟩φM yx,s \! C \! iff there is a C-strategy C str_C s.t. yx,λ⊧φM yx,λ holds for all λ∈Plays(x(G),s,C)λ∈ Plays(S x(G),s, str_C) Path formulae: yx,λ⊧φM yx,λ iff yx,λ[0]⊧φM yx,λ[0] for every state formula φ yx,λ⊧¬ψM yx,λ ψ iff yx,λ⊧̸ψM yx,λ ψ yx,λ⊧ψ1∧ψ2M yx,λ _1 _2 iff yx,λ⊧ψ1M yx,λ _1 and yx,λ⊧ψ2M yx,λ _2 yx,λ⊧XψM yx,λ Xψ iff yx,λ[1,∞)⊧ψM yx,λ[1,∞) ψ yx,λ⊧GψM yx,λ Gψ iff yx,λ[i,∞)⊧ψM yx,λ[i,∞) ψ for all i≥0i≥ 0 yx,λ⊧ψ1Uψ2M yx,λ _1U _2 iff there is a position i≥0i≥ 0 s.t. yx,λ[i,∞)⊧ψ2M yx,λ[i,∞) _2 and yx,λ[j,∞)⊧ψ1M yx,λ[j,∞) _1 for all 0≤j<i0≤ j<i Existence of winning strategies in Reachability Sabotage Games When considering winning conditions in reachability sabotage games, the plays of interest are those in which the goal vertex is eventually reached, i.e., at some point in the play arrives at a game-state in which g true. In the initial game-states of such plays ⊤Ug Ug holds (or equivalently, using the future operator, FgFg). The existence of a winning strategy for the runner in an RSG can be then expressed by: ⟨r⟩Fg \! \r\ \! Fg, which says that runner can enforce that (has a strategy such that on all plays in that strategy) g will eventually hold. Let us first consider turn-based reachability sabotage games. Proposition 3.13. Let G=(V,E)G=(V,E) be a graph. Runner has a winning strategy in a turn-based RSG (G,v0,vg)(G,v_0,v_g) iff Rtb,((E,v0),r)⊧⟨r⟩FgM^R tb,((E,v_0),r) \! \r\ \! Fg. The classical winning conditions of the RSG assume specific incentives of the two players. Motivated by modeling the interaction between teacher (demon) and learner (runner) in learning scenarios, [11] introduced variations of the classical winning conditions of the sabotage game: runner could be eager or unwilling to get to the goal and demon could be helpful or unhelpful in the process. Accordingly, we get four different turn-based sabotage games: the classical RSGEURSG^EU (eager runner and unhelpful demon), RSGEHRSG^EH (eager runner and helpful demon), RSGUHRSG^UH (unwilling runner and helpful demon), and RSGUURSG^U (unhelpful demon and unwilling runner). Tab. 1 shows the ATL formulae expressing winning conditions in these games (in the sense of Prop. 3.13), and compare them to way they can be expressed in SML. Type of RSG Implied winner SML formula (ρk _k, k=|E|k=|E|) ATL formula RSGEURSG^EU runner ρ0:=g,ρn+1:=g∨◆■ρn _0:=g,\ _n+1:=g _n [27] ⟨r⟩Fg \! \r\ \! Fg RSGEHRSG^EH runner and demon ρ0:=g,ρn+1:=g∨◆◆ρn _0:=g,\ _n+1:=g _n [11] ⟨r,d⟩Fg \! \r,d\ \! Fg RSGUHRSG^UH demon ρ0:=g,ρn+1:=g∨(◆⊤∧□◆ρn) _0:=g,\ _n+1:=g ( _n) [11] ⟨d⟩Fg \! \d\ \! Fg RSGUURSG^U runner and demon ρ0:=¬g,ρn+1:=¬g∨◆◆ρn _0:= g,\ _n+1:= g _n ⟨r,d⟩¬Fg \! \r,d\ \! Fg Table 1: Comparison of SML and ATL formulae expressing winning conditions in sabotage games with various incentives Additionally, note that the winning condition for demon in the standard RSGEURSG^EU can be expressed by ⟨d⟩G¬g \! \d\ \! G g (demon has a strategy such that in all resulting plays the runner does not eventually reach the goal). Note that in turn-based sabotage games this is equivalent to ⟦r⟧G¬g \r\ G g, which expresses that runner cannot avoid losing. This duality property is an instance of the fact that turn-based zero-sum games are determined (see [5, 13, 1]). In general, any ATL formulae ⟨C⟩φ \! C \! in Tab. 1 is equivalent to ⟦∖C⟧¬φ C , e.g., the ATL formula for RSGEHRSG^EH is equivalent to ⟦∅⟧Fg Fg, stating the CTL-expressible condition that there is a play on which runner reaches the goal. As a matter of fact we can show that runner can (almost) never win a turn-based RSG. Proposition 3.14. Let ((V,E),v0,vg)((V,E),v_0,v_g) be a RSG with v0≠vgv_0≠ v_g and (v0,vg)∉E(v_0,v_g)∉ E. Then we have that Rtb,((E,v0),r)⊧̸⟨r⟩FgM^R tb,((E,v_0),r) \! \r\ \! Fg. In other words, unless runner begins in the goal vertex, or the goal vertex is reachable from the start vertex in one step, demon will always be able to prevent runner from reaching the goal. The argument goes as follows. Assume that up to and including the point i in the play the goal has not been reached, and that λ[i]=((E′,v),d)λ[i]=((E ,v),d) (it is demon’s turn to move). Demon’s winning strategy is: if there is an e∈E′e∈ E s.t. e=(v,vg)e=(v,v_g), then play e; otherwise play any e′∈E′e ∈ E . The strategy works because in a simple graph there can only be one edge between any two vertices. This handicap of the runner is why sabotage games are often studied in the context of multi-graphs, which allow multiple edges between any two vertices. Our temporal setting can be easily extended to that setup, by extending the set of actions with indexed pairs of vertices, see e.g., [11]. In this paper we decided to keep to simple (and directed) graphs for ease of exposition. Switching to concurrent games does not change the winning conditions for different types of RSG listed in Tab. 1. It does however, further limit the runner’s power. In concurrent games any action taken by runner can be in principle ‘canceled’ by demon choosing the same edge, preventing it from ever leaving the initial game-state. Moreover, note that even though both turn-based and concurrent sabotage games afford cooperative strategies, they have different scopes in the two types. First, the following proposition expresses that if there is a joint winning strategy in the concurrent version of the game, then there is one in the turn-based version of the same game. Proposition 3.15. Let ((V,E),v0,vg)((V,E),v_0,v_g) be a RSG. If Rcon,(E,v0)⊧⟨r,d⟩FgM^R con,(E,v_0) \! \r,d\ \! Fg, then Rtb,((E,v0),r)⊧⟨r,d⟩FgM^R tb,((E,v_0),r) \! \r,d\ \! Fg. The opposite implication however does not hold. To see this, consider the following example. Example 3.16. In the graph G∞=(V,E)G^∞=(V,E) with V=v0,vgV=\v_0,v_g\ and E=(v0,vg)E=\(v_0,v_g)\ there is a winning strategy for the coalition of runner and demon in a turn-based sabotage game, but there is no such strategy in the concurrent game played on G∞G^∞. In the concurrent play, the only joint choice for the players is to select the same edge (v0,vg)(v_0,v_g) at the start of the game, and that will keep them from ever reaching vgv_g. Example 3.16 also demonstrates that in general neither demon nor runner, and not even the coalition of the two players, is guaranteed to be able to force a concurrent game to end. In other words, in RSG (G∞,v0,vg)(G^∞,v_0,v_g) we have that Rcon,(E,v0)⊧̸⟨r,d⟩FX⊥.M^R con,(E,v_0) \! \r,d\ \! FX . Existence of winning strategies in Liveness Sabotage Games The goal in liveness sabotage isn’t to reach the goal state. Instead, we want runner to stay ‘alive’ for (at least) a given number of moves. While the existence of a possible move that a runner can make can be expressed by the formula X⊤X being true in a game-state controlled by runner, we want it to be at a specific time-point, after each player moved b-times. In order to be able to do this we extend the language of ATL∗ with the parametrized until-operator borrowed from metric temporal logic [19], allowing a new path-formula, ψUiφψ U_i for i∈ℕi with the following meaning: ,λ⊧ψUiφ iff ,λ[i,∞)⊧φ and for all j s.t. 0≤j<i, ,λ[j,∞)⊧ψ.$ M,λ ψ U_i $ iff $M,λ[i,∞) $ and for all $j$ s.t. $0≤ j<i$, $M,λ[j,∞) ψ$. It allows expressing the condition of runner having ‘somewhere to go’ for i or its rounds, and so that the coalition of players C has a strategy to make the game last at least i-rounds. In the case of turn-based sabotage games the following formula will suffice: ⟨r⟩⊤U2b(X⊤) \! \r\ \! U_2b(X ), since at even rounds of the turn-based RSG it is always runner’s turn. Proposition 3.17. Let G=(V,E)G=(V,E) be a graph. Runner has a winning strategy in a turn-based LSG (G,v0,b)(G,v_0,b) iff Rtb,((E,v0),r)⊧⟨r⟩⊤U2b(X⊤)M^R tb,((E,v_0),r) \! \r\ \! U_2b(X ). Note that the above formula also implies that ⟨r⟩(X⊤)U2b(X⊤) \! \r\ \! (X )U_2b(X ), i.e., that runner can enforce the play λ, s.t. for all i≤2bi≤ 2b, λ[i]λ[i] has a δtbδ tb-successor. In concurrent LSGs ((V,E),v0,b)((V,E),v_0,b), as long as E≠∅E≠ , runner and demon can jointly enforce that the game is live forever, i.e., Lcon,(E,v0)⊧⟨r,d⟩GX⊤M^L con,(E,v_0) \! \r,d\ \! GX , by indefinitely applying (er,ed)(e_r,e_d), s.t. er=ede_r=e_d. A somewhat surprising observation is that what constitutes a problem for runner in an RSG, is an advantage in LSG. Namely, as long as demon chooses the same edge as the runner, runner remains alive, i.e., she retains a position with a successor. In RSG, the canceling choice prevents the runner from progressing towards the goal. Sabotage games and the minimum cut of a graph A strategy to destroy the edge-connectivity of a graph could be to find and sever the minimum cut of the graph. The problem of finding minimum cuts in graphs is well-studied in the field of graph theory (see, e.g., [10, 9, 17]). Finding such cuts is often relevant with respect to two specific vertices of the graph, in such a case the problem is called a minimal s−ts-t cut. Definition 3.18 (Minimum cut [7], see also [18]). The minimum cut of a graph G=(V,E)G=(V,E) is the minimum number of edges in E that, when removed from the graph, partition the vertices into two disjoint sets, V′V and V′V , such that no vertex from V′V is reachable from V′V . The minimum-cut of a graph G=(V,E)G=(V,E) with respect to the vertices s,t∈Vs,t∈ V is the minimum number of edges in E that after their removal from G s is not reachable from t. The minimum s−ts-t cut has been characterized in terms of paths in the graph in the following way. Theorem 3.19 (Menger’s theorem [23]). Let G=(V,E)G=(V,E) and let x,y∈Vx,y∈ V with x≠yx≠ y. The size of the minimum cut for x and y (the minimum number of edges whose removal disconnects x and y) is equal to the maximum number of pairwise edge-independent paths from x to y. Such minimum s−ts-t cuts are useful when working with static s which can be seen as unmoving runner. If however the runner moves (as she should), in some cases she can ‘escape’ the execution of a static min-cut before demon manages to complete it. So, a question of dynamic minimum s−ts-t cut appears: What is the minimal number of rounds demon must play in order to prevent the runner to be able to reach the goal? To see that the standard notion of (static) minimum s−ts-t cut and the sabotage-based notion of the dynamic minimum s−ts-t cut are different, consider the following example. Example 3.20. Let us play a turn-based RSG (G,s,t)(G,s,t) on the graph G depicted below. Firstly, note that the minimum static s−ts-t cut of the graph is of size 22 and contains the edges (s,u),(s,w)\(s,u),(s,w)\. A naive demon could think that removing these edges one by one would allow him to win the game in two moves. Unfortunately, runner is allowed to move in-between the demon’s moves, so she would manage to escape the static min-cut by either moving to u or w in its first move. The min-cut from both u or w to t is of size 33, so the demon has underestimated the number of edges to be deleted, and must reconsider which edge should be cut. There are in fact three dynamic minimal s−ts-t cuts of the graph (depending on how the runner moves): (s,u),(u,v),(u,t),(s,w),(w,v),(w,t),(v,t),(u,t),(w,t)\\(s,u),(u,v),(u,t)\,\(s,w),(w,v),(w,t)\,\(v,t),(u,t),(w,t)\\ and the demon cannot expect to win in less than three rounds. vvuuwwsstt The set of edges mentioned last in the enumeration in the Example above is of particular importance. Unlike in the setting of multi-graphs, which are often studied in the context of sabotage games, in standard graphs demon always has a winning strategy in the sabotage game: remove an arbitrary edge (or do nothing) until the runner is at some v that is one step away from the goal vertex vgv_g, then remove (v,vg)(v,v_g); and repeat that procedure as long as the runner’s position is disconnected from the goal. To minimize the number of removals that disconnect the goal vertex from the rest of the graph, it is enough if demon focuses on only the edges that end at vgv_g. Even in that case however, the order of removals makes a difference, and must depend on the position of the runner. To capture the dynamic s−ts-t cuts (v0−vgv_0-v_g cuts, in our case) we are interested in those v0v_0-plays that validate the formula F⟨∅⟩G¬gF \! \! G g, which states that there is a point at which in all futures the goal will never be reached (equivalently stated as ⊤U(⟨∅⟩G¬g U( \! \! G g)). With the parametrized until-operator we can put a time-stamp on that moment, and require that it is obtained by the demon as soon as possible. Demon’s strategy (set of plays) corresponding to the minimal dynamic v0−vgv_0-v_g cut then can be expressed in the following way. Definition 3.21. The minimal tb-dynamic v0−v0v_0-v_0 cut of the graph G=(V,E)G=(V,E) is k iff v0=sv_0=s and vg=tv_g=t and k is the smallest such that Rtb,((E,v0),r)⊧⟨d⟩(⊤Uk(⟨∅⟩G¬g))M^R tb,((E,v_0),r) \! \d\ \! ( U_k( \! \! G g)). Let us mention, that a number of classical results address variants of the minimum s−ts-t cut problem where the source (or the pair s,ts,t) is not fixed in advance. The classical solution is the Gomory–Hu tree [12], which represents all pairwise minimum s−ts-t cuts of an undirected graph using only n−1n-1 maximum-flow computations. Later work by Gusfield simplified the construction and analysis of such cut trees [14]. In addition, research on dynamic graph algorithms studies data structures that maintain connectivity and cut-related information while the graph changes or while queries for arbitrary terminal pairs are issued [15]. Our ATL∗-based rendering of Sabotage Games brings logic and the algorithmic graph theory closer, and we plan to deepen this connection in a follow-up work. Angelic Sabotage Games To make a proper use of the power of ATL∗ it would be interesting to consider more complex infinite sabotage games. This can be done if apart from deletion of edges, we allow also their addition. In fact, many authors allow also for a ‘positive’ type of dynamics of the graph (see, e.g., [3]). Angelic sabotage games, apart from runner and demon, also include an agent of positive change—a builder of edges. The following could be one example of such an extension. Definition 3.22. A strictly turn-based angelic sabotage play is a (possibly infinite) sequence of game-states s0,…,sns^0,…,s^n, such that s0=(E0,v0)s^0=(E^0,v^0) is given by (E,v0)(E,v_0), and for any k s.t. 0<k≤n0<k≤ n: sk=(Ek−1,vk), s.t. (vk−1,vk)∈Ek−1if k≡1(mod3);(Ek−1∖(x,y),vk−1), s.t. (x,y)∈Ek−1if k≡2(mod3);(Ek−1∪(x,y),vk−1), s.t. (x,y)∈V2∖Ek−1if k≡0(mod3).s^k= cases(E^k-1,v^k), s.t. (v^k-1,v^k)∈ E^k-1&if k≡ 1 3;\\ (E^k-1 \(x,y)\,v^k-1), s.t. (x,y)∈ E^k-1&if k≡ 2 3;\\ (E^k-1∪\(x,y)\,v^k-1), s.t. (x,y)∈ V^2 E^k-1&if k≡ 0 3.\\ cases The winning conditions for runner and demon in RSG and LSG are as before, while the angel can be most naturally seen as runner’s ally, but various coalitions of players with various incentives can be studied, similarly to the approach presented in Tab. 1. The definitions of the tb, con, and gen angelic sabotage game structures are straight-forward extensions of the ones in Def. 3.1,3.2, and 3.3. The general difference with the non-angelic kind of sabotage game structures is that the play can recover from breaking the connectivity of the graph and from the runner finding themselves in a dead-end vertex. Since the angelic plays are infinite, we can consider more complex properties, in particular the requirement that a coalition can enforce visiting the goal vertex infinitely many times, ⟨C⟩GFg \! C \! GFg, a property that, due to nested temporal operators cannot be expressed in simple ATL, and requires ATL∗. 4 Knowledge in Sabotage Games To capture cooperative strategic behavior under uncertainty an epistemic extension of ATL was proposed, namely the Alternating-time Temporal Epistemic Logic (ATEL, [29]). It extends the language with knowledge modality K and with the group knowledge modalities E (everybody knows) and C (common knowledge). Combining the strategic operators of ATL with the epistemic operators enables us to express statements about what coalitions of agents can enforce through their joint strategies, while explicitly accounting for what agents know about the game-state and the actions of others. ATEL extends ATL with the following formulae: KaφK_a (a knows that φ ), EΓφE_ (everyone in Γ knows that φ ) and CΓφC_ (it’s common knowledge among Γ that φ ), where a∈a and Γ⊆ . Interpreting the above formulae in sabotage game models requires enriching them with accessibility relations for the agents. We will refer to such epistemic sabotage game models with yxE y x, with y∈L,R y∈\ L, R\ and x∈tb,con,gen x∈\ tb, con, gen\. The accessibility relations ∼i⊆Sx×Sx _i S x× S x, specify for each i∈i the scope of their uncertainty in a given game-state, by relating it to those that the agent can not distinguish, given her knowledge, from the current game-state.888We hence specify the uncertainty of agents to range over game-states (as done e.g. in [29]), rather than on histories (as in [25]). Since classical sabotage games are history-free, we can say quite a lot following this assumption. We will assume the accessibility relations to be equivalence relations. The semantics of the above operators is defined as usual, with the epistemic formulas taken to be state formulas: ,s⊧Kaφ iff for all t, s.t. s∼at,M,t⊧φM,s K_a iff for all t, s.t. s _at,M,t ; ,s⊧EΓφ iff for all t, s.t. s∼ΓEt,M,t⊧φM,s E_ iff for all t, s.t. s _ ^Et,\,M,t ; ,s⊧CΓφ iff for all t, s.t. s∼ΓCt,M,t⊧φM,s C_ iff for all t, s.t. s _ ^Ct,M,t , where ∼ΓE=⋃a∈Γ∼a _ ^E= _a∈ _a, and ∼ΓC _ ^C is the transitive closure of ∼ΓE _ ^E. In the original ATEL [1], the epistemic part was simply added ‘on top of’ the existing ATL semantics, and the definition of the strategies didn’t take into account the actual epistemically-based ability to execute them. This simple approach allows talking about some simple aspects of knowledge in sabotage games. The simplest approach is to assume that the have perfect information, i.e., all agents see everything in a state: the edges present and the runner’s position. Here we assume that ∼i _i for each i∈i are identity relations. We can then say, following Prop. 3.14, that if ((V,E),v0,vg)((V,E),v_0,v_g) is RSG with v0≠vgv_0≠ v_g and (v0,vg)∉E(v_0,v_g)∉ E, then we have that Rtb,((E,v0),r)⊧E⟨d⟩G¬gE^R tb,((E,v_0),r) E_AG \! \d\ \! G g. Imperfect information can be imparted on agents in many different ways, for instance we could assume that they can only see immediate neighbors of the runner’s current position, i.e, (E,v)∼i(E′,v′)(E,v) _i(E ,v ) iff |E(v)|=|E′(v′)||E(v)|=|E (v )|, where E(v)=e∈E∣π1(e)=vE(v)=\e∈ E _1(e)=v\.999This specification is somewhat inconsistent with demon’s global powers over G. This discrepancy could be remedied by restricting the function actact in the sabotage game structures, so that act(d,(E,v))=e∈E′∣π1(e)=vact(d,(E,v))=\e∈ E _1(e)=v\, by making the demon local [20, 21, 2]). In such games we an agent might have a winning strategy but she might not know that. Example 4.1. Let us assume that a turn-based reachability sabotage game between runner and demon is played on the following graph G. vvuuvgv_g Clearly, if the starting node is u, runner has a winning strategy in RSG: the first move she makes will lead her to the goal vertex. However, given the fact that she can only observe the number of edges leading out of the current node, she can’t be sure if she is not in fact in the vertex v. If that was the case, she would not be able to win: after moving to u, demon can remove the edge (u,g)(u,g), and the runner loses the game. We then have that Rtb(G,vg),((E,u),r)⊧⟨r⟩Fg∧¬Kr⟨r⟩FgE^R tb(G,v_g),((E,u),r) \! \r\ \! Fg K_r \! \r\ \! Fg. The above observation might make the reader uneasy—how can we claim something is an agent’s strategic range, but they do not know it? This effect is the topic of an important discussion in existing literature on logics of games, which is even more pronounced in the example below. Let us give runner perfect information, but obscure from demon the location of runner after the first step is made, i.e., for any two v0v_0-plays λ and λ′λ , and any i>0i>0, λ[i]∼dλ′[i]λ[i] _dλ [i], if λ[i]=((E1,v),a)λ[i]=((E_1,v),a),λ′[i]=((E2,v′),a)λ [i]=((E_2,v ),a) and E1=E2E_1=E_2. In this setting, demon might have a winning strategy, but since he cannot know where runner is at a given time, he might not be able to apply it during the play. Example 4.2. Consider the graph G below. Runner starts at v0v_0 and both agents know that, and they know the structure of the graph. Runner makes a move hidden to demon. v0v_0uuwwgg Demon now knows that runner is either in u or in w. This is not enough information to apply the strategy that would guarantee winning in the turn-based game with perfect information, i.e., blocker has to chose one of the (u,g)(u,g) or (w,g)(w,g), but might get unlucky with that choice, and the runner will still be able to get to g. To be able to express this in ATEL, we have to augment the semantics to account for demon’s ‘belief-states’ (∼d _d abstraction classes). Such adjustment was first proposed in [16], to account for imperfect information strategies. Under this new ‘imperfect’ semantics for the turn-based sabotage game on G, we have that Rtb(G,v0),((E,v0),r)⊧̸imp⟨d⟩FgE Rtb(G,v_0),((E,v_0),r) _imp \! \d\ \! Fg, while on the original ATEL semantics we would, counterintuitively, get that Rtb(G,v0),((E,v0),r)⊧Kd⟨d⟩FgE Rtb(G,v_0),((E,v_0),r) K_d \! \d\ \! Fg. 5 Conclusions and future work We examined various kinds of sabotage games from the perspective of ATL. We have studied the classical reachability sabotage game, and introduced liveness sabotage games. Apart from the standard turn-based version, we introduced concurrent sabotage games, which are very natural for the ATL framework. We characterized the existence of winning strategies in these kinds of games. We further related those characterizations to the graph-theoretical problem of minimal s−ts-t cut, and discussed a dynamic version of that problem. We also connected to angelic sabotage games, in which edges can be built. Finally, we have shown how epistemic extensions of ATL can account for knowledge in sabotage games, a need that was highlighted in a recent survey by van Benthem and Liu [26]. There are many possible follow-up directions of this work: studying possible extensions of classical sabotage games, such as multiple runners, distributed goals, and infinite sabotage games (especially in the context of angelic games). We are interested in strengthening the relationship with algorithmic graph theory, by linking to various kinds of dynamic min-cut and max-flow problems. Moreover, extending our preliminary epistemic account od Sabotage Games holds special promise. Sabotage Games can be viewed as a natural playground for various notions of strategic ability, e.g., making use of positional and memory-based strategies would allow comparing the power of the players on another level. References [1] R. Alur, T. A. Henzinger, and O. Kupferman (2002) Alternating-time temporal logic. Journal of the ACM 49, p. 672–713. External Links: Document Cited by: §1, §3, §4. [2] G. Aucher, J. van Benthem, and D. Grossi (2018) Modal logics of sabotage revisited. Journal of Logic and Computation 28, p. 269–303. Cited by: footnote 9. [3] A. Baltag, D. Li, and M. Y. Pedersen (2022/06/01) A modal logic for supervised learning. Journal of Logic, Language and Information 31 (2), p. 213–234. External Links: Document, ISBN 1572-9583, Link Cited by: §3. [4] P. Blackburn and J. Seligman (1995) Hybrid languages. Journal of Logic, Language and Information 4 (3), p. 251–272. Cited by: footnote 2. [5] J. R. Buchi and L. H. Landweber (1969) Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society 138, p. 295–311. External Links: ISSN 00029947, Link Cited by: §3. [6] K. Chatterjee, T. A. Henzinger, and N. Piterman (2007) Algorithms for Büchi games. Information and Computation 205 (3), p. 466–492. External Links: Document Cited by: §2. [7] G. B. Dantzig and D. R. Fulkerson (1956) On the max-flow min-cut theorem of networks. In Linear Inequalities and Related Systems, H. W. Kuhn and A. W. Tucker (Eds.), Annals of Mathematics Studies, Vol. 38, p. 215–221. Cited by: Definition 3.18. [8] S. Demri, V. Goranko, and M. Lange (2016) Temporal logics in computer science. Cambridge University Press. Cited by: §3. [9] E. A. Dinitz, A. V. Karzanov, and M. V. Lomonosov (1976) On the structure of a family of minimal weighted cuts in a graph. In Studies in Discrete Optimization (in Russian), p. 290–306. Note: Original in Russian Cited by: §3. [10] L. R. Ford and D. R. Fulkerson (1956) Maximal flow through a network. Canadian Journal of Mathematics 8, p. 399–404. Cited by: §3. [11] N. Gierasimczuk, L. Kurzen, and F. R. Velázquez-Quesada (2009) Learning and teaching as a game: a sabotage approach. In Logic, Rationality, and Interaction, X. He, J. Horty, and E. Pacuit (Eds.), Berlin, Heidelberg, p. 119–132. External Links: ISBN 978-3-642-04893-7 Cited by: §3, §3, Table 1, Table 1, footnote 3. [12] R. E. Gomory and T. C. Hu (1961) Multi-terminal network flows. Journal of the Society for Industrial and Applied Mathematics 9 (4), p. 551–570. Cited by: §3. [13] Y. Gurevich and L. Harrington (1982) Trees, automata, and games. In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC ’82, New York, NY, USA, p. 60–65. External Links: Document, ISBN 0897910702, Link Cited by: §3. [14] D. Gusfield (1990) Very simple methods for all pairs network flow analysis. SIAM Journal on Computing 19 (1), p. 143–155. Cited by: §3. [15] J. Holm, K. de Lichtenberg, and M. 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, p. 79–89. Cited by: §3. [16] W. Jamroga (2003) Some remarks on alternating temporal epistemic logic. In Proceedings of Formal Approaches to Multi-Agent Systems (FAMAS 2003), B. Dunin-Keplicz and R. Verbrugge (Eds.), p. 133–139. Note: Early workshop contribution on ATEL semantics and issues Cited by: Example 4.2. [17] D. 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), p. 21–30. Cited by: §3. [18] J. Kleinberg and É. Tardos (2013) Algorithm design. New International Edition edition, Pearson. External Links: ISBN 9781292023236 Cited by: Definition 3.18. [19] R. Koymans (1990/11/01) Specifying real-time properties with metric temporal logic. Real-Time Systems 2 (4), p. 255–299. External Links: Document, ISBN 1573-1383, Link Cited by: §3. [20] D. Kvasov (2015) From sabotage games to border protection. Technical report Technical Report 2015-2, CEI Working Paper Series, Center for Economic Institutions, Institute of Economic Research, Hitotsubashi University. External Links: Link Cited by: footnote 9. [21] D. Kvasov (2016) On sabotage games. Operations Research Letters 44 (2), p. 250–254. External Links: Document Cited by: footnote 9. [22] C. Löding and P. Rohde (2003) Solving the sabotage game is PSPACE-hard. In Mathematical Foundations of Computer Science, Vol. 2747, p. 531–540. Cited by: §1, §2, §2. [23] K. Menger (1927) Zur allgemeinen kurventheorie. Fundamenta Mathematicae 10 (1), p. 96–115 (ger). External Links: Link Cited by: Theorem 3.19. [24] T. Murata (1989) Petri nets: properties, analysis and applications. Proceedings of the IEEE 77 (4), p. 541–580. External Links: Document Cited by: §2. [25] J. van Benthem, J. Gerbrandy, T. Hoshi, and E. Pacuit (2009) Merging frameworks for interaction. Journal of Philosophical Logic 38 (5), p. 491–526. External Links: ISSN 00223611, 15730433, Link Cited by: footnote 8. [26] J. van Benthem and F. Liu (Eds.) (2025) Graph games and logic design: recent developments and further directions. Trends in Logic, Vol. 66, Springer International Publishing, Cham. External Links: ISBN 978-3-031-91360-0 Cited by: §5. [27] J. 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 Science, Vol. 2605, p. 268–276. External Links: Document Cited by: §1, §2, §2, Proposition 2.4, §2, Table 1. [28] J. van Benthem (2010) Modal logic for open minds. CSLI Publications. External Links: ISBN 978-1575865980 Cited by: §1. [29] W. van der Hoek and M. Wooldridge (2003-11) Cooperation, knowledge, and time: alternating-time temporal epistemic logic and its applications. Studia Logica 75 (1), p. 125–157. External Links: Document Cited by: §4, footnote 8. Appendix Proposition 2.5 Let G=(V,E)G=(V,E) and b∈ℕ+b ^+. Runner has a winning strategy in LSG=((V,E),v0,b)LSG=((V,E),v_0,b) iff M((E,v0)),v0⊧γbM((E,v_0)),v_0 _b, with γi _i (for i∈ℕi ) given by: γ1:=◆⊤,γn+1:=◆■γn. _1:= ,\ _n+1:= _n. Proof. By induction on b. Base case, b=1b=1. The following are equivalent: (1.) runner has a winning strategy in the LSG=(V,E,v0,1)LSG=(V,E,v_0,1); (2.) there is a v1∈Vv_1∈ V, such that (v0,v1)∈E(v_0,v_1)∈ E (runner can use it in the present round); (3.) M((E,v0)),v1⊧⊤M((E,v_0)),v_1 ; (4.) M((E,v0)),v0⊧◆⊤M((E,v_0)),v_0 ; (5.) M((E,v0)),v0⊧γ1M((E,v_0)),v_0 _1. Inductive hypothesis: runner has a winning strategy in LSG=(V,E,v0,n)LSG=(V,E,v_0,n) iff M((E,v0)),v0⊧γnM((E,v_0)),v_0 _n. Take b=n+1b=n+1. (⇒ ) Assume that the runner has a winning strategy in LSG (V,E,v0,n+1)(V,E,v_0,n+1). Then there is v′∈Vv ∈ V, such that (v,v′)∈E(v,v )∈ E and for any (x,y)∈E(x,y)∈ E, runner has a winning strategy in the LSG (V,E∖x,y,v′,n)(V,E \x,y\,v ,n). By the inductive hypothesis: for any (x,y)∈E(x,y)∈ E, M((E∖(x,y),v′)),v′⊧γnM((E \(x,y)\,v )),v _n. Then, by the semantics of ■ , M((E,v0)),v′⊧■γnM((E,v_0)),v _n. Finally, by our choice of v′v and the semantics of ◆ , we get that M((E,v0)),v0⊧◆■γnM((E,v_0)),v_0 _n, i.e., M((E,v0)),v0⊧γn+1M((E,v_0)),v_0 _n+1. (⇐ ) Assume that M((E,v0)),v0⊧γn+1M((E,v_0)),v_0 _n+1, i.e., M((E,v0)),v0⊧◆■γnM((E,v_0)),v_0 _n. Then, there is a v′∈Vv ∈ V such that (v,v′)∈E(v,v )∈ E and M((E,v0)),v′⊧■γnM((E,v_0)),v _n. Then for all (x,y)∈E(x,y)∈ E, M((E∖(x,y),v0)),v′⊧γnM((E \(x,y)\,v_0)),v _n, which (by inductive hypothesis) means that for all (x,y)∈E(x,y)∈ E, runner has a winning strategy in (V,E∖(x,y),v′,n)(V,E \(x,y)\,v ,n). But then the runner has a winning strategy in LSG=(V,E,v0,n+1)LSG=(V,E,v_0,n+1) by moving first from v0v_0 to v1v_1. ∎ Proposition 3.5 (1.) Plays(tb(G))Plays(S tb(G)) is a finite set of plays of finite length. Proof. Take G=(V,E)G=(V,E). We show that for any λ∈Plays(tb(G))λ∈ Plays(S tb(G)), length(λ)≤2|E|−1length(λ)≤ 2|E|-1. For contradiction assume that there is a λ∈Plays(tb(G))λ∈ Plays(S tb(G)), s.t. length(λ)≥2|E|length(λ)≥ 2|E| and λ[2|E|−1]=((E′,v),a)λ[2|E|-1]=((E ,v),a), for some a∈a . This means that acttb(λ[2|E|−1])≠∅act tb(λ[2|E|-1])≠ , i.e., E′≠∅E ≠ . But between λ[0]λ[0] and λ[2|E|−1]λ[2|E|-1] demon must have made |E||E| moves, i.e., deleted |E||E| edges, since the game is strictly turn-based, so E′=∅E = . Contradiction. Moreover, Plays(tb(G))Plays(S tb(G)) is a finite set because it corresponds to a set of finite (as we’ve just shown) sequences over a finite alphabet E.∎ (2.) For any λ∈Plays(con(G))λ∈ Plays(S con(G)), there is a λ′∈Plays(gen(G))λ ∈ Plays(S gen(G)), s.t. for all i≤length(λ)i≤ length(λ), λ[i]=λ′[i]λ[i]=λ [i]. Proof. Take a λ∈Plays(con(G))λ∈ Plays(S con(G)). We want to show that λ∈Plays(gen(G))λ∈ Plays(S gen(G)). Firstly, λ[0]∈Sgenλ[0]∈ S gen because Scon=SgenS con=S gen. Secondly, for every i>0i>0, λ[i]=δgen(λ[i−1],(er,ed))λ[i]=δ gen(λ[i-1],(e_r,e_d)) for some (er,ed)∈actgen(λ[i−1])(e_r,e_d)∈ act gen(λ[i-1]), because for any s, actcon(s)⊆actgen(s)act con(s) act gen(s) and for any s and e,e′∈Acte,e ∈ Act, δcon(s,(e,e′))=δgen(s,(e,e′))δ con(s,(e,e ))=δ gen(s,(e,e )). ∎ (3.) Plays(con(G))Plays(S con(G)) and Plays(gen(G))Plays(S gen(G)) are infinite and contain infinite plays. Proof. For contradiction assume that Plays(con(G))Plays(S con(G)) is a finite set, and that its longest play is of length n∈Nn∈ N. Take such a longest λ. Let us construct λ′λ in the following way: λ′[0]:=λ[0]λ [0]:=λ[0] and for i∈0,…,n−1i∈\0,…,n-1\, λ′[i+1]:=λ[i]λ [i+1]:=λ[i]. It is clear that length(λ′)=n+1length(λ )=n+1. To see that λ′∈Plays(con(G))λ ∈ Plays(S con(G)), consider that λ′[0]∈Sconλ [0]∈ S con, λ′[1]=δcon(λ′[0],(e,e))λ [1]=δ con(λ [0],(e,e)) for any choice of e∈Acte∈ Act, and for i∈2,…,ni∈\2,…,n\, λ′[i]=δcon(λ′[i−1],(er,ed))λ [i]=δ con(λ [i-1],(e_r,e_d)), for er,ede_r,e_d such that λ[i−1]=δcon(λ[i−2],(er,ed))λ[i-1]=δ con(λ[i-2],(e_r,e_d)). We get a contradiction. To see that Plays(con(G))Plays(S con(G)) contains an infinite play. Take an e∈Acte∈ Act, then (E,π1(e)),(E,π1(e)),…(E, _1(e)),(E, _1(e)),… is a play in Plays(con(G))Plays(S con(G)) generated by the infinite repetition of the action profile (e,e)(e,e). We conclude that Plays(con(G))Plays(S con(G)) must be infinite and contains an infinite play, and so, by (2.), Plays(gen(G))Plays(S gen(G)) must be an infinite set and contain an infinite play. ∎ Proposition 3.7 (1.) For any λ∈Plays(tb(G),((E,v),r))λ∈ Plays(S tb(G),((E,v),r)) and an odd i<length(λ)i<length(λ), (λ[i])≠(λ[i+1])L(λ[i]) (λ[i+1]). Proof. In turn-based sabotage games, at odd i in ((E,v),r)((E,v),r)-play λ it is demon’s turn to move, say that it removes e. Then (λ(i))∖(λ(i+1))=qeL(λ(i)) (λ(i+1))=q_e. ∎ (2.) For any λ∈Plays(tb(G))λ∈ Plays(S tb(G)), there is a λ′∈Plays(gen(G))λ ∈ Plays(S gen(G)), such that for all i≤length(λ)i≤ length(λ), (λ[i])=(λ′[i])L(λ[i])=L(λ [i]). Proof. Take λ∈Plays(tb(G))λ∈ Plays(S tb(G)). W.l.o.g., assume that runner moves first, then, by Prop. 3.5.1., λ is a finite sequence ((E0,v0),r),…,((En,vn),r)((E^0,v^0),r),…,((E^n,v^n),r). We claim that the required play is any λ′λ such that λ′[0,n]=(E0,v0),…,(En,vn)λ [0,n]=(E^0,v^0),…,(E^n,v^n). We need to show that for all i≤length(λ)i≤ length(λ), λ′[i+1]=δgen(λ′[i],α)λ [i+1]=δ gen(λ [i],α), for some α∈actgen(λ′[i])α∈ act gen(λ [i]). In fact, for each a∈a and for all t=((E,v),a)∈Stbt=((E,v),a)∈ S tb and s=(E,v)∈Sgens=(E,v)∈ S gen, acttb(t)⊆actgen(s)act tb(t) act gen(s) (for any state all action profiles allowed in the turn-based game are allowed in the general game), and that for all α∈acttb(((E,v),a))α∈ act tb(((E,v),a)) and δtb(((E,v),a),α))=(((E′v′),a′))δ tb(((E,v),a),α))=(((E v ),a )) then δgen((E,v),α))=((E′,v′))δ gen((E,v),α))=((E ,v )). Finally, observe that for all a∈a , ((E,v),a)∈Stb((E,v),a)∈ S tb and (E,v)∈Sgen(E,v)∈ S gen, (((E,v),a))=((E,v))L(((E,v),a))=L((E,v)) (structural labeling L only takes into account the graph structure, edges and runner’s position, of the game-state). ∎ Proposition 3.13 Let G=(V,E)G=(V,E) be a graph. Runner has a winning strategy in a turn-based RSG (G,v0,vg)(G,v_0,v_g) iff Rtb,((E,v0),r)⊧⟨r⟩FgM^R tb,((E,v_0),r) \! \r\ \! Fg. Proof. The following are equivalent: 1. Rtb,((E,v0),r)⊧⟨r⟩FgM^R tb,((E,v_0),r) \! \r\ \! Fg 2. there is an r-strategy strrstr_r, s.t. Rtb,λ⊧FgM^R tb,λ Fg for all λ∈Plays(tb(G),v0,str)λ∈ Plays(S tb(G),v_0,str_r); 3. there is an r-strategy strrstr_r, s.t. Rtb,λ⊧⊤UgM^R tb,λ Ug for all λ∈Plays(tb(G),v0,str)λ∈ Plays(S tb(G),v_0,str_r); 4. there is an r-strategy strrstr_r, s.t. for all λ∈Plays(tb(G),v0,str)λ∈ Plays(S tb(G),v_0,str_r) there is i≥0i≥ 0, s.t. Rtb,λ[i]⊧gM^R tb,λ[i] g; 5. there is an r-strategy strrstr_r, s.t. for all λ∈Plays(tb(G),v0,str)λ∈ Plays(S tb(G),v_0,str_r) there is i≥0i≥ 0, s.t. g∈(λ[i])g (λ[i]); 6. there is an r-strategy strrstr_r, s.t. for all λ∈Plays(tb(G),v0,str)λ∈ Plays(S tb(G),v_0,str_r) there is i≥0i≥ 0, s.t. λ[i]=((E,v),a)λ[i]=((E,v),a) for some a∈a with v=vgv=v_g; 7. there is a function str:Stb→Actskipstr_r:S tb→ Act skip with str(s)∈acttb(r,s)str_r(s)∈ act tb(r,s), s.t. for all λ∈Plays(tb(G),v0,str)λ∈ Plays(S tb(G),v_0,str_r) there is i≥0i≥ 0, s.t. λ[i]=((E,v),a)λ[i]=((E,v),a) for some a∈a with v=vgv=v_g; 8. there is a function str:Stb→Actskipstr_r:S tb→ Act skip with str(s)∈acttb(r,s)str_r(s)∈ act tb(r,s), s.t. for all λ∈Plays(tb(G),v0)λ∈ Plays(S tb(G),v_0) such that λ[j+1]∈δtb(λ[j],α)∣α∈acttb(λ[j]) and str(λ[j])⊑αλ[j+1]∈\δ tb(λ[j],α) α∈ act tb(λ[j]) and str_r(λ[j]) α\ there is an i≥0i≥ 0, s.t. λ[i]=((E,v),a)λ[i]=((E,v),a) for some a∈a with v=vgv=v_g; 9. there is a function str:Stb→Actskipstr_r:S tb→ Act skip with str(s)∈acttb(r,s)str_r(s)∈ act tb(r,s), s.t. for all λ∈Plays(tb(G),v0)λ∈ Plays(S tb(G),v_0) such that for even j<length(λ)−1j<length(λ)-1, λ[j+1]=δtb(λ[j],(str(λ[j]),skip))λ[j+1]=δ tb(λ[j],(str_r(λ[j]), skip)) and for odd j<length(λ)−1j<length(λ)-1, λ[j+1]∈δtb(λ[j],(skip,e))∣e∈Edges(λ[j])λ[j+1]∈\δ tb(λ[j],( skip,e)) e∈ Edges(λ[j])\ there is an i≥0i≥ 0, s.t. λ[i]=((E,v),a)λ[i]=((E,v),a) for some a∈a with v=vgv=v_g; 10. there is a function win:(G)→Ewin:S(G)→ E that runner can apply at her choice point sks^k such that whichever remaining edge is removed from, runner retains the connectivity to the goal from π2(win(s)) _2(win(s)) in sk+1s^k+1. Namely: win((E′,v))=str((E′,v),r)win((E ,v))=str_r((E ,v),r). So, runner has a winning strategy in RSG (G,v0,vg)(G,v_0,v_g). ∎ Proposition 3.15 Let ((V,E),v0,vg)((V,E),v_0,v_g) be a RSG. If Rcon,(E,v0)⊧⟨r,d⟩FgM^R con,(E,v_0) \! \r,d\ \! Fg, then Rtb,((E,v0),r)⊧⟨r,d⟩FgM^R tb,((E,v_0),r) \! \r,d\ \! Fg. Proof. Assume that Rcon,(E,v0)⊧⟨r,d⟩FgM^R con,(E,v_0) \! \r,d\ \! Fg, which means that there is pair of strategies (str,strd)(str_r,str_d), with stra:Scon→Actstr_a:S con→ Act, and stra∈actcon(s)str_a∈ act con(s) (for a∈a ), s.t. for all λ∈Plays(con(G),v0)λ∈ Plays(S con(G),v_0) such that λ[j+1]=δcon(λ[j],(str(λ[j]),strd(λ[j])))λ[j+1]=δ con(λ[j],(str_r(λ[j]),str_d(λ[j]))), there is an i≥0i≥ 0, s.t. λ[i]=(E,v)λ[i]=(E,v) with v=vgv=v_g. Let us define str′,strd′str _r,str _d with stra′:Stb→Actskipstr _a:S tb→ Act skip, and stra′∈acttb(s)str _a∈ act tb(s) (for a∈a ) in the following way: • str′(((E,v),r)):=str((E,v))str _r(((E,v),r)):=str_r((E,v)) and str′(((E,v),d)):=skipstr _r(((E,v),d)):= skip; • strd′(((E,v),d)):=strd((E,v))str _d(((E,v),d)):=str_d((E,v)) and strd′(((E,v),r)):=skipstr _d(((E,v),r)):= skip. First, note that stra′:Stb→Actskipstr _a:S tb→ Act skip, and stra′∈acttb(s)str _a∈ act tb(s) (for a∈a ). We also have that for all λ∈Plays(tb(G),v0)λ∈ Plays(S tb(G),v_0), such that λ[j+1]=δtb(λ[j],(str′(λ[j]),strd′(λ[j])))λ[j+1]=δ tb(λ[j],(str _r(λ[j]),str _d(λ[j]))), there is an i≥0i≥ 0, s.t. λ[i]=((E,v),a)λ[i]=((E,v),a) for some a∈a with v=vgv=v_g. ∎ Proposition 3.16 Let G=(V,E)G=(V,E) be a graph. Runner has a winning strategy in a turn-based LSG (G,v0,b)(G,v_0,b) iff Rtb,((E,v0),r)⊧⟨r⟩⊤U2b(X⊤)M^R tb,((E,v_0),r) \! \r\ \! U_2b(X ). Proof. Analogous to the proof of Prop. 3.13. ∎ Examples of rooted sabotage game structures v0v_0v1v_1v2v_2v0v_0v0v_0v1v_1v2v_2v1v_1v0v_0v1v_1v2v_2v1v_1v0v_0v1v_1v2v_2v2v_2v0v_0v1v_1v2v_2v2v_2v0v_0v1v_1v2v_2v1v_1 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 v0v_0v1v_1v2v_2v0v_0v0v_0v1v_1v2v_2v1v_1v0v_0v1v_1v2v_2v2v_2v0v_0v1v_1v2v_2v1v_1v0v_0v1v_1v2v_2v1v_1v0v_0v1v_1v2v_2v1v_1v0v_0v1v_1v2v_2v2v_2v0v_0v1v_1v2v_2v2v_2v0v_0v1v_1v2v_2v2v_2v0v_0v1v_1v2v_2v1v_1v0v_0v1v_1v2v_2v1v_1v0v_0v1v_1v2v_2v1v_1v0v_0v1v_1v2v_2v1v_1v0v_0v1v_1v2v_2v1v_1 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