Guillaume Aucher
email: guillaume.aucher@irisa.fr

Johan Van Benthem
email: j.vanbenthem@uva.nl

Davide Grossi
email: d.grossi@liverpool.ac.uk

Modal Logics of Sabotage Revisited

Sabotage modal logic was proposed in 2003 as a format for analyzing games that modify graphs they are played on. We investigate some model-theoretic and proof-theoretic aspects of sabotage modal logic, which has come to be viewed as an early dynamic logic of graph change. Our first result is a characterization theorem for sabotage modal logic as a fragment of first-order logic which is invariant with respect to a natural notion of 'sabotage bisimulation'. Next, we offer a sound and complete tableau method and its associated labeled sequent calculus for analyzing reasoning in sabotage modal logic. Finally, we identify and briefly explore a number of open research problems concerning sabotage modal logic that illuminate its complexity, placing it within the current landscape of modal logics that analyze model update, and, returning to the original motivation of sabotage, fixed-point logics for network games.

Introduction

Sabotage modal logic (SML), first introduced in [START_REF] Van Benthem | An essay on sabotage and obstruction[END_REF], expands basic modal logic with a modality ϕ saying "after the deletion of at least one edge in the frame, it holds that ϕ". This minimal modal logic of arbitrary edge deletion stands at the start of a line of systems in a dynamic-epistemic spirit [START_REF] Van Benthem | Logical Dynamics of Information and Interaction[END_REF], such as 'graph modifier logic' [START_REF] Aucher | Global and local graph modifiers[END_REF], 'swap logic' [START_REF] Areces | Swap logic[END_REF], or 'arrow update logic' [START_REF] Kooi | Arrow update logic[END_REF][START_REF] Areces | Moving arrows and four model checking results[END_REF]. SML is also directly related to recent work in theoretical computer science [START_REF] Radmacher | A game theoretic approach to the analysis of dynamic networks[END_REF][START_REF] Gruener | Connectivity games over dynamic networks[END_REF], learning theory [START_REF] Gierasimczuk | Learning and teaching as a game: a sabotage approach[END_REF], logics of social networks [START_REF] Seligman | Facebook and epistemic logic of friendship[END_REF][START_REF] Liu | Logical dynamics of belief change in the community[END_REF], and argumentation [START_REF] Grossi | On the logic of argumentation theory[END_REF][START_REF] Grossi | Argumentation theory in the view of modal logic[END_REF].

Only a few properties of sabotage modal logic have been studied in depth so far. The source paper [START_REF] Van Benthem | An essay on sabotage and obstruction[END_REF] showed how SML can formulate solution concepts for sabotage games, it gave a SPACE upper bound for model checking, and it sketched how the SML language can be translated into first-order logic, though the validities are not closed under substitutions. More incisive results are in [START_REF] Löding | Solving the sabotage game is PSPACE-hard[END_REF][START_REF] Löding | Model checking and satisfiability for sabotage modal logic[END_REF], where multi-modal SML is shown to have an undecidable satisfiability problem and a PSPACE-complete model-checking problem. A main open problem mentioned in [START_REF] Löding | Solving the sabotage game is PSPACE-hard[END_REF][START_REF] Löding | Model checking and satisfiability for sabotage modal logic[END_REF] is a bisimulation invariance characterization for SML. This was solved independently in the proceedings version of the present article [START_REF] Aucher | Sabotage modal logic: Some model and proof theoretic aspects[END_REF] and in the work of an Argentinean team [START_REF] Areces | Relation-changing modal operators[END_REF]. Also independently, both teams developed tableau systems to analyze the structure of validity in SML, cf. [START_REF] Areces | Tableaux for relation-changing modal logics[END_REF][START_REF] Areces | Relation-changing modal operators[END_REF]. We will discuss some connections in Section 8.1 at the end of this paper.

Outline Our paper has two parts. The first, comprising Sections 2 to 5, extends the material in [START_REF] Aucher | Sabotage modal logic: Some model and proof theoretic aspects[END_REF] with proofs left out there, while adding a labeled sequent calculus, several new examples and a few small novel observations. The two main contributions are a characterization result for SML (Section 4) as that fragment of first-order logic which is invariant for a natural notion of 'sabotage bisimulation' (Section 3) and a novel tableau system and matching sequent calculus in Section 5. The second part of the paper is more exploratory. Sections 6 to 7 present new material addressing the issue of what makes SML tick among current modal logics of model change, where we identify the sources of its undecidability in a way that also sheds new light on current dynamic-epistemic logics. Moreover, we make a systematic connection with fixed-point logics of sabotage for analyzing graph games, and revisit the original motivation for SML in sabotage games. Section 8 discusses related work. Section 9 concludes and emphasizes once more how sabotage modal logics can serve as a laboratory for broader graph games.

Preliminaries

In this section, we introduce the syntax and semantics of SML, recapitulate some key results from [START_REF] Löding | Model checking and satisfiability for sabotage modal logic[END_REF], and present a standard translation from SML into FOL.

Syntax and semantics

Let P be a countable set of propositional atoms. The sabotage modal language L s is the set of 'sabotage formulas' defined by the following grammar in BNF:

L s : ϕ ::= p | ¬ϕ | (ϕ ∧ ϕ) | ♦ϕ | ϕ
where p ∈ P. We add some useful notation. For all ϕ, ψ ∈ L s , we define the usual abbreviations: ϕ ¬ ¬ϕ, ϕ ∨ ψ ¬(¬ϕ ∧ ¬ψ), ϕ → ψ ¬ϕ ∨ ψ, ⊥ p ∧ ¬p, ¬⊥ (for an arbitrary p ∈ P). For all ϕ ∈ L s , we define iterated formulas as follows: for all M ∈ { , ♦, , }, M 0 ϕ ϕ and for all n ∈ N, M n+1 ϕ MM n ϕ. To save parentheses, binding strength is in this order: , , , ♦, ¬, ∧, ∨, →. Also, we will use the 'sabotage depth' sd(ϕ) of formulas ϕ, [START_REF] Löding | Model checking and satisfiability for sabotage modal logic[END_REF], defined inductively by: sd(p) 0, sd(¬ϕ) sd(ϕ), sd(ϕ 1 ∧ ϕ 2 ) max{sd(ϕ 1 ), sd(ϕ 2 )}, sd(♦ϕ) sd(ϕ) and sd( ϕ) sd(ϕ) + 1. Hence, in particular, sd( ) = 0.

We work with standard relational models M = (W, R, V ) for modal logic ('models', for short), with W a non-empty set; R ⊆ W × W , and V : P -→ 2 W . A pair F = (W, R) is called a frame. We write w ∈ M for w ∈ W , and call a pair (M, w) a 'pointed model', the class of which is M. The satisfaction relation |= ⊆ M × L s is defined inductively by truth conditions. Those for the Boolean and modal connectives ¬, ∧, ♦ are as usual, and the truth condition for is:

(W, R, V ), w |= ϕ iff there is (u, v) ∈ R s.t. (W, R \ {(u, v)}, V ), w |= ϕ.
Thus, ϕ is true in a pointed model if there are two R-related (possibly identical) states such that, if the edge between these states is removed from R, ϕ holds at the distinguished state. (If no such pair exists, ϕ is false for any ϕ.) The triple SML (L s , M, |=) is called sabotage modal logic. Satisfiability, validity and logical consequence for SML are defined as usual.

We can also restate this slightly differently to emphasize the bimodal flavor of our logic. Define a relation r ⊆ M×M with ((W, R, V, w), (W , R , V , w )) ∈ r iff W = W ; R = R \ {(u, v)} for some u, v ∈ W ; V = V and w = w. Then the above truth condition for the sabotage modality makes it a standard existential modality referring to this ordering between models. We can also iterate this order in the obvious way, to talk about models reachable in finitely many rsteps, obtaining the relation r * .

As usual, our standard relational models can also be interpreted as models for the binary fragment of FOL with equality1 denoted L 1 . Sometimes in the proofs to follow we will use the following first-order terminology and notation. We say that a model M satisfies a formula ϕ(x) ∈ L 1 (or a set Γ (x) ⊆ L 1 ) with one free variable x under the assignment of w to x if, and only if, ϕ (respectively Γ ) is true of w -or in symbols, M |= ϕ(x) [w] (respectively, M |= Γ (x) [w]). We say that a model M realizes a set Γ (x) ⊆ L 1 with one free variable x (also called a 'type') if there exists an element w ∈ W such that M |= Γ (x) [w].

If (M, w) ∈ M, the sabotage modal theory of (M, w) is the set T s (M, w) {ϕ ∈ L s | M, w |= ϕ}. We also define the binary relation s ⊆ M×M as follows: (M, w) s (M , w ) (for ((M, w), (M , w )) ∈ s ) iff for all ϕ ∈ L s , M, w |= ϕ iff M , w |= ϕ. In that case, we say that (M, w) and (M , w ) are sabotage modally equivalent (that is, they satisfy the same sabotage modal formulas).

Some notable validities and expressible properties

We list some validities of SML that demonstrate how the deletion modality works:

⊥ → ⊥ (1)
⊥ → ⊥ (2)
p → p (3)
( p ∧ ¬ ⊥) → p (4)
p → (♦ → ♦p)

♦ϕ ∧ ♦¬ϕ → (5)
The fact that we are using propositional atoms instead of variables for formulas in the first five of the above validities is not accidental. Surprisingly, many prima facie valid-looking principles fail for SML in their full schematic form with all complex substitution instances once we realize that under a deletion modality, ordinary modalities can change their truth values.

A good example is principle [START_REF] Areces | Hybrid logics[END_REF]. Consider its schematic formulation which states that if every accessible state satisfies ϕ, then after any link deletion, if the evaluation state still has a successor, it still has a ϕ-successor. The formula may fail if ϕ is modal, since deletion may happen deeper in the model and disrupt the truth of ϕ at successor states. See Figure 1 for an illustration.

ϕ → (♦ → ♦ϕ), (7)
In the above list, only the last item ( 6) is a schematic validity. 2 Still, any logic has a 'substitution core' consisting of its schematically valid principles, cf. [START_REF] Van Benthem | Logical Dynamics of Information and Interaction[END_REF], and it is an interesting open problem whether SML has a decidable, or even an axiomatizable substitution core. 3Next, SML can express properties beyond the reach of standard modal logic. Examples are: "there are at most n successors of the current state" with 1 ≤ n (Expression [START_REF] Aucher | Global and local graph modifiers[END_REF], but see also Example 2 of Section 4 below); "there exist at least two successors or, there exists at most one successor and at least another state with at least one successor" (Expression (9)); "there exists no successor but there is at least one state with at least one successor" (Expression [START_REF] Baltag | Logics for epistemic programs[END_REF]). All these properties have FOL formulations using counting quantifiers:

∃ ≤n y (xRy) (8)
∃ ≥2 y (xRy) ∨ ∃ ≤1 y (xRy) ∧ ∃y(x = y ∧ ∃z(yRz) (9)
¬∃y(xRy) ∧ ∃y(∃z(yRz))

These properties can be expressed in SML by, in the same order:

⊥ ∨ 1≤i≤n i ⊥ (11)
♦ (12) ⊥ ∧ (13)
None of the above properties is expressible in the standard modal language, and defining them involves various hybrid extensions, such as graded modalities [START_REF] De Rijke | A note on graded modal logic[END_REF], the difference modality, and the universal modality [START_REF] Blackburn | Modal Logic[END_REF]Ch. 7].

Another sign of strength for SML is its power to define frames up to isomorphism. For instance, it is a simple exercise to show that the formula

♦ ∧ ♦ ∧ ⊥ (14)
is true in a model if and only if its underlying frame consists of one reflexive point. This observation can be generalized to cycles of any length.

Fact 1 For each positive natural number n, there exists an SML formula ϕ such that, for any model M = (W, R, V ) and state s: M, s |= ϕ if, and only if, the frame (W, R) is a cycle of length n.

Proof. We show how to build the desired formula. Define first:

PATH (n) 0≤i≤n i ♦ ∧   0≤i≤n-1 ♦ i ⊥  
Each such formula forces the existence of exactly one path of length n + 1 from the evaluation point. The desired formula is then defined inductively as follows:

CYCLE (1) PATH (1) = ( 14)

CYCLE (n + 1) PATH (n) ∧ 1≤i≤n (¬♦ n-i n-i CYCLE (i))
The base case is immediate. As to the induction step, the first conjunct forced existence of a unique path of length at least n from the current state. The second conjunct forces the (n -1) th -step in such a path to end in the current state.

A First-Order Translation for SML

A standard first-order translation for SML was sketched in [START_REF] Van Benthem | An essay on sabotage and obstruction[END_REF] and [START_REF] Löding | Solving the sabotage game is PSPACE-hard[END_REF]. Later on, a detailed translation was independently given in the proceedings version of this paper [START_REF] Aucher | Sabotage modal logic: Some model and proof theoretic aspects[END_REF] and in [START_REF] Areces | Relation-changing modal operators[END_REF]. In this section we describe the translation and its correctness in detail. This prepares for the later sections of the article.

Setting up the translation In order to define a translation from the language of SML into the free variable fragment of FOL with equality one needs to keep track of the changes that the sabotage operators introduce in the model. This is achieved by indexing the standard translation with a set E of pairs of variables. When the translation is applied to the outermost operator of a given formula, this set is empty. As analysis proceeds towards inner operators, each sabotage operator in the formula will introduce a new pair of variables in E, which is bound by an existential quantifier. Here is the formal definition: Definition 1 (Standard translation for SML). Let E be a set of pairs (y, z) of variables-standing for edges-and let x be a designated variable. The translation ST E x : L s -→ L 1 is recursively defined as follows:

ST E x (p) P (x) ST E x (⊥) ¬(x = x) ST E x (¬ϕ) ¬ST E x (ϕ) ST E x (ϕ 1 ∧ ϕ 2 ) ST E x (ϕ 1 ) ∧ ST E x (ϕ 2 ) ST E x (♦ϕ) ∃y   xRy ∧ (v,w)∈E ¬(x = v ∧ y = w) ∧ ST E y (ϕ)   ST E x ( ϕ) ∃y, z   yRz ∧ (v,w)∈E ¬(y = v ∧ z = w) ∧ ST E∪{(y,z)} x (ϕ)  
In the inductive clauses, a standard modality ♦ϕ translates as a first-order formula with x free, stating there exists a state y accessible from x via an edge different from all edges in the set E, with the translation of ϕ holding at y. Formula ϕ becomes a first-order formula saying there is some R-edge (y, z) different from any edge already in E, that the translation of ϕ should now be taken with respect to the set E ∪ {(y, z)}, and that the result holds at x. Setting up the translation like this lets one book-keep removal of edges in a perspicuous manner via E, forcing modalities to access ever smaller relations.

It is important to notice the following feature of this procedure. Depending on the chosen E, ST E can possibly yield formulas with several free variables, e.g.:

ST {(v,w)} x (♦p) = ∃y (xRy ∧ ¬(x = v ∧ y = w) ∧ P (y))
. However, if ST E is applied to a formula ϕ by setting E = ∅, that is to say, if the translation is initiated with an empty E, then, at each successive application of ST E to subformulas of ϕ, the variables occurring in W will be bound by some quantifiers introduced at previous steps. For any ϕ, ST ∅

x (ϕ) yields a FOL formula with only x free.

Example 1. We illustrate the translation by means of an example:

ST ∅ x ( ♦ ♦p) = ∃y, z yRz ∧ ST {(y,z)} x (♦ ♦p) = ∃y, z yRz ∧ ∃v xRv ∧ ¬(x = y ∧ v = z) ∧ ST {(y,z)} v ( ♦p) = ∃y (xRy ∧ ∃v (xRv ∧ ¬(x = x ∧ y = z)∧ ∃y , z y Rz ∧ ¬(y = y ∧ z = z) ∧ ST {(y,z),(y ,z )} v (♦p) = ∃y, z (yRz ∧ ∃v (xRv ∧ ¬(x = x ∧ y = z)∧ ∃y , z (y Rz ∧ ¬(y = y ∧ z = z)∧ ∃v (vRv ∧ ¬(v = y ∧ v = z) ∧ ¬(v = y ∧ v = z )∧ ST {(y,z),(y ,z )} v (p))))) = ∃y, z (yRz ∧ ∃v (xRv ∧ ¬(x = x ∧ y = z)∧ ∃y , z (y Rz ∧ ¬(y = y ∧ z = z)∧ ∃v (vRv ∧ ¬(v = y ∧ v = z) ∧ ¬(v = y ∧ v = z ) ∧ P (v )))))
This formula states that after some sabotage it is still possible to reach a state where, after a second sabotage, a p-state can be reached.

Correctness of the translation

To check this complex syntax, we now sketch a proof of the correctness of the translation proposed in Definition 1.

Theorem 1. Let (M, w) be a pointed model and ϕ ∈ L s :

M, w |= ϕ iff M |= ST ∅ x (ϕ)[w]
Proof. This goes by induction on the structure of ϕ. The key inductive step for the sabotage operator is proven by the equivalences that use the inductive hypothesis plus the semantics of and the definition of our translation ST: M, w |= ϕ iff there exists M with (M, w)r(M , w) and M , w |= ϕ iff there exists M with (M, w)r(M , w) and

M |= ST ∅ x (ϕ)[w] iff M |= ST ∅ x ( ϕ)[w]
While this translation is mainly a tool for us, it does exhibit some interesting features. The standard translation for modal logic takes formulas into the twovariable fragment of first-order logic. Here, however, things are different.

Proposition 1. SML is not contained in any fixed variable fragment of FOL.

Proof. Consider the SML formulas of Section 2 with counting quantifiers for at most n accessible worlds. It is well-known that no fixed finite-variable fragment F O(k) of FOL can define all of these, since the Ehrenfeucht k-pebble game that is characteristic for such a fragment, cf. [START_REF] Van Benthem | Logic in Games[END_REF]Ch. 14], cannot distinguish between pointed models having at most k and at most k + 1 accessible worlds.

Finally, it may be pointed out that our translation can be viewed in two ways. It may be seen as showing that SML formulas are pretty messy first-order formulas, involving a lot of variable binding. But it may also be seen as showing that SML is a quite succinct variable-free notation for a complex part of FOL. 43 Bisimulation for SML In this section, we introduce a notion of 'sabotage bisimulation' for SML, a task left open in [START_REF] Löding | Solving the sabotage game is PSPACE-hard[END_REF][START_REF] Löding | Model checking and satisfiability for sabotage modal logic[END_REF]. The invariance results enabled by this new notion of bisimulation (that is, Propositions 2 and 3 below) were independently proven in [START_REF] Aucher | Sabotage modal logic: Some model and proof theoretic aspects[END_REF] and [START_REF] Areces | Relation-changing modal operators[END_REF], albeit in slightly different formulations.

Sabotage bisimulation

Definition 2 (s-bisimulation). Let M 1 = (W 1 , R 1 , V 1 ), M 2 = (W 2 , R 2 , V 2 )
be two relational models. A non-empty relation Z ⊆ r * (M 1 , w)×r * (M 2 , v) is an s-bisimulation between the two pointed models (M 1 , w) and (M 2 , v)-notation, Z : (M 1 , w) s (M 2 , v)-if the following conditions are satisfied:

Atom: If (M 1 , w)Z(M 2 , v) then M 1 , w |= p iff M 2 , v |= p,
If (M 1 , w)Z(M 2 , v) and there exists M 1 such that (M 1 , w)r(M 1 , w),
then there exists

M 2 such that (M 2 , v)r(M 2 , v) and (M 1 , w)Z(M 2 , v); Zag : If (M 1 , w)Z(M 2 , v) and there exists M 2 such that (M 2 , v)r(M 2 , v),
then there exists M 1 such that (M 1 , w)r(M 1 , w) and (M 1 , w)Z(M 2 , v).

For brevity we write (M 1 , w) s (M 2 , v) if there exists an s-bisimulation Z such that (M 1 , w)Z(M 2 , v).

The notion of s-bisimulation strengthens the standard modal bisimulation with back and forth conditions for the sabotage modality. Here, just as the sabotage modality is an 'external' modality looking across different models, so is s-bisimulation an 'external' notion of bisimulation. Standard bisimulation keeps a relational graph model fixed and changes the evaluation point along the accessibility relation of the model, s-bisimulation keeps the evaluation point fixed but changes the model by picking one among the sabotage-accessible ones.

Bisimulation and modal equivalence in SML

We first show that s-bisimulation implies SML equivalence.

Proposition 2 ( s ⊆ s ). For any two pointed models (M 1 , w) and

(M 2 , v), if (M 1 , w) s (M 2 , v), then (M 1 , w) s (M 2 , v).
Proof. The proof is by induction on the syntax of ϕ. Let (M Just as for the standard modal language, the converse of Proposition 2 can be proven in case the models at issue are 'ω-saturated'. To introduce this notion, we need some notation. Given a finite set Y , the expansion of L 1 with a finite set of constants Y is denoted by L 1 Y , and the expansion of a relational model M to L 1 Y is denoted by M Y . 5 In what follows, x is a finite tuple of variables.

Definition 3 (ω-saturation). A model M = (W, R, V ) is ω-saturated if, for every Y ⊆ W such that |Y | < ω, the expansion M Y realizes every set Γ (x) of L 1 Y -formulas whose finite subsets Γ (x) ⊆ Γ (x) are all realized in M Y .
Thus, a model M is ω-saturated if for any set of formulas Γ (x, y 1 , . . . , y n ) over a finite set of 'running variables' x and 'parameters' y 1 , ..., y n , once some interpretation of the y 1 , . . . , y n is fixed to, say, w 1 , . . . , w n , and all finite subsets of Γ (x)[w 1 , . . . , w n ] are realizable in M, then the whole of Γ (x)[w 1 , . . . , w n ] is realizable in M. From a standard modal point of view, Definition 3 requires that, if for any subset of Γ there are accessible states satisfying it at the evaluation point, then there are accessible states satisfying the whole of Γ at the evaluation point. However, what we need for SML is slightly stronger, since we need to find pairs of states so as to satisfy a given type involving deletion, as we shall see.

Proposition 3 ( s ⊆ s ). For any two ω-saturated pointed models (M 1 , w 1 ) and (M 2 , w 2 ), if (M 1 , w 1 ) s (M 2 , w 2 ), then (M 1 , w 1 ) s (M 2 , w 2 ).
Proof. We show that the relation s itself is an s-bisimulation (cf. Definition 2). Base Case: The condition Atom is straightforwardly satisfied, being a special case of modal equivalence of points. Back and Forth Conditions: The proof for conditions Zig ♦ and Zag ♦ proceeds as usual for basic modal languages. Next, we prove that the condition Zig is satisfied. Assume that (M 1 , w 1 ) s (M 2 , w 2 ) and (M 1 , w 1 )r(M 1 , w 1 ). We show there must be a model (M 2 , w 2 ) such that (M 2 , w 2 )r(M 2 , w 2 ) and (M 1 , w 1 ) s (M 2 , w 2 ). For a start, we have that for any finite Γ ⊆ T s (M 1 , w 1 ) the following sequence of equivalences holds:

M 1 , w 1 |= Γ iff M 2 , w 2 |= Γ iff M 2 |= ST ∅ x Γ [w 2 ] iff M 2 |= ∃y, z yRz ∧ ST {(y,z)} x Γ [w 2 ]
The first equivalence holds by the assumption of sabotage equivalence between (M 1 , w 1 ) and (M 2 , w 2 ). The second follows by Theorem 1 and the third one by Definition 1. From this, by ω-saturation of M 2 with respect to types having pairs of running variables as mentioned above, we can conclude that:

There are y, z ∈ M 2 such that yRz and

M 2 |= ST {(y,z)} x (T s (M 1 , w 1 )) [w 2 ]
. 5 For basic facts on ω-saturation we refer the reader to [12, Ch. 2] and [START_REF] Chang | Model Theory[END_REF]Ch. 2]. The first use of the following proof method for modal logic is found in [START_REF] Van Benthem | Modal Logic and Classical Logic[END_REF].

Using Theorem 1, it follows that there is a pointed model (M 2 , w 2 ) with (M 2 , w 2 )r(M 2 , w 2 ) and

M 2 |= ST ∅ x (T s (M 1 , w 1 )) [w 2 ]. Finally, it is immediate that (M 1 , w 1 )
s (M 2 , w 2 ), which completes the proof of the Zig clause. In the same way it can be shown that also the condition Zag is satisfied.

6

We have thus established a precise match between sabotage modal equivalence and sabotage bisimulation for the special class of ω-saturated models. 7

Characterization of SML by Invariance

We now extend a classical result for basic modal logic. We characterize SML as the one free variable fragment of FOL that is invariant under s-bisimulation. 8 Theorem 2 (Characterization of SML by s-bisimulation invariance). An L 1 -formula is equivalent to the translation of an L s formula if, and only if, it is invariant for sabotage bisimulation.

Proof. The direction from left to right follows from Proposition 2. In the opposite direction, we proceed as customary. Let ϕ ∈ L 1 with one free variable x. Assume that ϕ is invariant under s-bisimulation and consider the following set:

C s (ϕ) {ST ∅ x (ψ) | ψ ∈ L s and ϕ |= ST ∅ x (ψ)}.
The result is a direct consequence of the following two claims: Claim (b). Take any pointed model M, w such that M |= C s (ϕ)[w] and consider its sabotage modal theory T s (M, w). Now consider the set of formulas Σ = ST ∅ x (T s (M, w)) ∪ {ϕ}. We first show that:

(c) Σ is consistent. 6 One final thing to check is that the new models obtained are still ω-saturated. This requires a small additional argument translating formulas satisfied at points s in the models M after the link deletion into formulas satisfied at s in the original M. 7 Obtaining this result for any two models requires using an infinitary version of SML. 8 Recall that the standard translation ST ∅ of a sabotage modal logic formula always produces a FOL formula with only one free variable. To prove (c), assume, towards a contradiction, that Σ is inconsistent. By the compactness of FOL we then obtain that |= ϕ → ¬ Γ for some finite Γ ⊆ ST ∅ x (T s (M, w)). But then, by the definition of C s (ϕ), we have that

¬ Γ ∈ C s (ϕ), and hence ¬ Γ ∈ ST ∅ x (T s (M, w)), which is impossible since Γ ⊆ ST ∅ x (T s (M, w)). Now Claim (b) follows if we can show that (d) M |= ϕ[w].
Here is a proof for (d). As Σ is consistent, it can be satisfied by a pointed model, say, (M , w ). Observe first that (M, w) s (M , w ) as both have the same SML theory. Now take two ω-saturated elementary extensions (M ω , w) and (M ω , w ) of (M, w) and (M , w ). That such extensions exist can be proven by a standard chain construction argument, [13, Proposition 3. Definable and undefinable properties in SML. So which FOL properties belong to the fragment identified by Theorem 2 and which ones do not? We provide examples of SML-definable and undefinable properties of models.

Example 2 (Counting successors). Consider the earlier-discussed FOL property "there exist at most n successors" of the current point. This property is not standard modal bisimulation invariant, but it is easy to see that it is invariant with respect to sabotage bisimulation. It is therefore definable in SML, something that we had established already by a direct argument.

Example 3 (Confluence). Consider the FOL property "every two successors of the current point have a shared successor". This property is not invariant for sabotage bisimulation, witness Figure 2, and hence it is not definable in SML. Caveat. Technically, some care is needed here, because SML works in a universe of changing models. For a sabotage bisimulation, one should draw not only the two base models, but also all sub-models obtainable by one edge deletion, two edge deletions, and so forth. So it is worth spending some time to see why the dashed lines in the relatively simple Figure 2 indeed form a sabotage bisimulation Z between the model M on the left and M on the right.

Notice that the accessibility relations in both models have the same cardinality, that is, 4. We proceed inductively as follows. 9 Consider r i (M, d) and r i (M , d ) with 1 ≤ i ≤ 4, that is the submodels that can be reached on the left, respectively right, model via exactly i edge deletions.

For the base case, with (M 4 , s) ∈ r 4 (M, d) and (M 4 , s ) ∈ r 4 (M , d ), it is obvious that (M 4 , s)Z(M 4 , s ) is a sabotage bisimulation for any s, s with sZs as in the picture: no successors exist, no further deletion can be carried out. For the induction step, first notice that, for any 1 ≤ i ≤ 4, for any (M i-1 , s) ∈ r i-1 (M, d), there exists (M i-1 , s ) ∈ r i-1 (M , d ) such that (M i-1 , s)Z(M i-1 , s ), with sZs as in the picture, is a standard bisimulation. That is, for any pointed submodel reachable on the left with i deletions, there exists a pointed submodel on the right for which Z is a standard modal bisimulation. Then, to complete the induction step, we need to show that, if (M i , s)Z(M i , s ) is a sabotage bisimulation, with sZs as in the picture, then for any

(M i-1 , s) ∈ r i-1 (M, d), there exists (M i-1 , s ) ∈ r i-1 (M , d ) such that (M i-1 , s)Z(M i-1 , s
) is a sabotage bisimulation, and vice versa. In words, if two pointed submodels reachable via i deletions are sabotage bisimilar, then for any pointed submodel reachable by i -1 deletions on the left, there is a pointed submodel reachable by i -1 deletions on the right such that Z is a sabotage bisimulation connecting the two.

A visual inspection of the bisimulation relation depicted in Figure 2 shows that this is indeed the case. Hence confluence is not SML-definable.

Example 4 (Reflexive states). Consider the FOL property xRx. This property is not invariant with respect to sabotage bisimulation. To witness this fact take two models M = (N, ≥) and M = (N, >) on the set of natural numbers (with 0 as the distinguished point in each case) where the accessibility relations are: (a) on the first model, the 'greater or equal' relation (reflexive), and (b) on the second model, the strictly greater relation (irreflexive). Now we have that (M, 0) s (M , 0). Figure 3 shows this fact by depicting (part of) a relation which is a standard modal bisimulation Z between the two models, but which in addition has the property that any edge deletion on one model can be 'mirrored' on the other model to obtain pointed models that are still connected by Z (in the sense of Definition 2). In particular, in the picture, observe that deletion of a reflexive edge in M at point i can be 'mirrored' by the deletion of edge (i, i + 1) in M (here, note that the accessibility relations are transitive in both models). However,

M |= xRx[0], whereas M |= xRx[0].
The reflexivity property xRx is therefore not definable in SML.

Proof Systems for SML

What about explicit proof calculi for reasoning in sabotage modal logic? As we shall see later, unlike dynamic-epistemic logics, SML does not support recursion axioms that can be added in a straightforward manner to a standard modal base logic to axiomatize the dynamic system. Indeed, we have not been able to find a natural Hilbert-style formulation for SML. Therefore, we turn to methods that are easier to formulate staying close to the semantics. This flexibility is provided when we deal with the satisfiability problem by semantic tableaux and when we deal with the validity problem by their dual, the labeled sequent calculi.

A Tableau Method for SML

Tableaux for SML cannot be quite like their standard modal counterparts for systems like K, since there are some obvious background differences. For instance, SML does not have the tree-model property: there are specific SML formulas satisfied in relational models whose underlying frames can not be trees. 10 The following procedure is the adaptation that we need. Definition 4 (Label, (extended) labeled formula and (relation) term). Let S be an infinite set whose elements are called labels. A labeled formula is an expression of the form x : ϕ where x is a label and ϕ ∈ L s . A term is a pair (x 1 , x 2 ), where x 1 , x 2 ∈ S. A relation term is an expression of the form x 1 Rx 2 where x 1 , x 2 ∈ S. An extended label is an expression of the form x E where x ∈ S and E is a finite set of terms. An extended labeled formula is an expression of the form x E : ϕ where x E is an extended label and ϕ ∈ L s .

Input: A formula ϕ ∈ L s .

Output: A tableau T for ϕ: each branch may be infinite, finite and labeled open, or finite and labeled closed.

1. Initially, T is a tree consisting of a single root node labeled with x ∅ : ϕ. 2. Repeat the following steps as long as possible:

(a) Choose a branch which is neither closed nor open and choose an extended labeled formula x E : ψ (or a pair of extended labeled formula x E : ψ and relation term x1Rx2) not selected before on this branch. (b) Apply the appropriate tableau rule of Figure 5 We briefly discuss the modal and sabotage rules, those for the propositional connectives being as usual. The rules ¬♦ and ¬ are natural adaptations of the standard rule ¬♦ of modal logic. The only difference is that they can be applied only to relation terms representing edges not already removed by the sabotage modality, and therefore not present in E. For the rule ¬ , moreover, the edge removed is added to the set E of the edges already removed. The rule ♦ is more complex than the standard modal rule, because SML does not have the treemodel property, unlike standard modal logic. So, we have to consider not only that a new world/label x 0 , which is accessible from x, may satisfy ϕ, but also

x E : ϕ ∧ ψ x E : ϕ x E : ψ ∧ x E : ¬(ϕ ∧ ψ) x E : ¬ϕ | x E : ¬ψ ¬∧ x E : ¬¬ϕ x E : ϕ ¬¬ x E 1 : ¬♦ϕ x1Rx2 x E 2 : ¬ϕ ¬♦ x E : ¬ ϕ x1Rx2
x E∪{(x 1 ,x 2 )} : ¬ϕ ¬ where (x1, x2) / ∈ E in both rules above.

x E : ♦ϕ xRx1 , x E 1 : ϕ | . . . | xRxn , x E n : ϕ | xRx0 , x E 0 : ϕ ♦
where {x1, . . . , xn} are all the labels occurring in the current branch such that (x, xi) / ∈ E for all i ∈ {1, . . . , n} and x0 is a 'fresh' label not occurring in the current branch. that one of the worlds/labels x i of the current model, which have already been introduced, may satisfy ϕ. In that case we also put an accessibility relation from x to this old world/label x i . The rule follows the same kind of resasoning: we may remove an edge represented by a pair of worlds/labels which has already been introduced or which contains either one or two 'fresh' worlds/labels. The construction of a tableau need not terminate: see Example 5. This is in line with the fact that the satisfiability problem of SML is undecidable. 11Example 5. In Figure 6, on the right, we display the execution of the tableau method of Figure 4 on the formula ♦ ∧ ♦ ∧ ⊥. We obtain a single open branch (labeled with ) from which we can extract a model whose frame is a single reflexive point. This formula is thus satisfiable, and in fact only in this frame. In Figure 6, on the left, we show that the tableau construction may not necessarily terminate by exhibiting an infinite branch in the tableau for the formula ♦ ∧ ♦ . Even if the formula holds in finite pointed models having at least two successors, our tableau method does not terminate with this formula as input, and it produces a pointed model with infinitely many successors.

x E : ϕ x1Rx 1 , x E∪{(x 1 ,x 1 )} : ϕ | . . . | xnRx n , x E∪{(xn,x n )} : ϕ where {(x1, x 1 ), . . . , (xn, x n )} = (M × M ) ∪ {(x+, x++)} \ E,
x ∅ 1 : ♦ ∧ ♦ x ∅ 1 : ♦ x ∅ 1 : ♦ x1Rx2 x ∅ 2 :
x

{(x1,x2)} 1 : ♦ x1Rx3 x {(x1,x2)} 3 : x {(x1 x3)} 1 : ♦ x ∅ 1 : ♦ ∧ ♦ ∧ ⊥ x ∅ 1 : ♦ x ∅ 1 : ♦ x ∅ 1 : ⊥ x1Rx2 x ∅ 2 : x1Rx1 x ∅ 1 : x ∅ 2 : ♦ x ∅ 1 : ♦ x2Rx3 x ∅ 3 : x {(x1,x1)} 1 : ⊥ x {(x2,x3)} 1 : ⊥ x1Rx3 x {(x1,x1)} 3 : x1Rx1 x {(x1,x1)} 1 : x {(x2,x3)} 2 : ⊥ × x {(x1,x1)} 3 : ⊥ × x2Rx1 x ∅ 1 : x2Rx2 x ∅ 2 :
x

{(x2,x1)} 1 : ⊥ x {(x2,x2)} 1 : ⊥ x {(x2,x1)} 2 : ⊥ × x {(x2,x2)} 2 : ⊥ × ∧ ♦ ¬ ♦ ¬ ∧ ♦ ♦ ¬♦ ¬♦ ♦ ¬ ¬ ♦ ♦ ¬♦ ¬♦ ¬ ¬ ¬♦ ¬♦ ♦ ♦
Fig. 6. Two extreme scenarios. An infinite branch arising in the tableau for the formula ♦ ∧ ♦ (left). A finite tableau for ♦ ∧ ♦ ∧ ⊥ (right).

Finally, the reader may find it of interest to create a tableau for a formula that really requires infinite models. Instead of doing this in tableau format, we end by noting a particularly easy case where the Finite Model Property fails.

Example 6 (Failure of FMP in an extended logic). A somewhat complex failure of FMP is given in [START_REF] Fervari | Relation-Changing Modal Operators[END_REF]. Here we give a more concise formula that uses some extra expressivity resources. Extend the SML language with a converse modality P (for 'past'-we can think of the above ♦ as 'future') plus a universal modality U over all states. The successive conjuncts of the following formula then say that the accessibility relation is a function, that is one-to-one, but not surjective:

U ((♦ ∧ ⊥) ∧ (P → ¬P ) ∧ E¬P ). (15)
Obviously, this statement can only be true in infinite models.

Soundness and Completeness of the Tableau Method

The following result states the adequacy of our tableau method.

Theorem 3 (Soundness and completeness). Let ϕ ∈ L s . If ϕ is unsatisfiable, then the tableau for ϕ closes (completeness). If the tableau for ϕ closes then ϕ is unsatisfiable (soundness).

Soundness Soundness is proved using the notion of interpretability. A set of extended labeled formulas L is interpretable if there is a Kripke model M = (W, R, V ) and a mapping f : S -→ W (recall that elements of S are used as labels) such that for all x E : ϕ ∈ L, we have that (W,

R \ f (E), V ), f (x) |= ϕ, where f (E) = {(f (x 1 ), f (x 2 )) | (x 1 , x 2 ) ∈ E}.
Then, we prove two facts:

Fact 2 If ϕ is satisfiable, then, at any step of the construction of the tableau for ϕ, the set of extended labeled formulas of some branch is interpretable.

Fact 3 If ϕ is satisfiable, then any branch whose set of extended labeled formulas is interpretable cannot close. That is, there is an extension of this interpretable branch which does not close (so this extended branch is either open or infinite).

These two facts combined prove that, if ϕ is satisfiable, the tableau for ϕ cannot close. Hence, if the tableau for ϕ closes, then ϕ is unsatisfiable (soundness).

Proof (Fact 2). We prove the first fact by induction on the number n of times we use inference rules in the construction of the tableau for ϕ. The case n = 0 holds trivially: in that case L is a singleton {x : ϕ} and it suffices to define f so that it assigns to x the world of the Kripke model where ϕ is satisfiable. The induction step n + 1 is proved by examining each rule on a case by case basis. We show that for each rule we can extend the mapping f , which is associated to an interpretable branch, in order to assign world(s) to the new label(s) created by the application of the rule. We show then that we can also extend the range of the accessibility relation R to assign a pair of worlds to the new relation term created by the rule. In fact, we know by the Induction Hypothesis that there is a branch of the tableau whose terms are all interpretable by this mapping f . The key steps to consider concern the rules ♦ and .

-Rule ♦: Let the interpretable branch contain an extended labeled formula

x E : ♦ϕ (not chosen before when executing the tableau method). Applying the rule ♦ to this interpretable branch, we obtain n + 1 extended branches.

We must show that one of them is interpretable. By assumption, we have

(W, R \ f (E), V ), f (x) |= ♦ϕ.
Hence, there is w ∈ W such that f (x)Rw and M, w |= ϕ. If w already corresponds to a label x such that f (x ) = w, then we are in one of the first n extensions of the interpretable branch. In that case, the map f need not be extended and the label x has already been introduced in a rule earlier in the execution of the tableau method. Otherwise, we are in the last case of the rule ♦ and we need to extend the mapping f and assign to the 'fresh' label x n+1 the possible world w: we set f (x n+1 ) w.

-Rule : Let the interpretable branch contain an extended labeled formula x E : ϕ (not chosen before in the execution of the tableau method). Applying Rule to this interpretable branch, we get n extended branches corresponding to the n elements of (M × M ) ∪ {(x + , x ++ )} \ E. We show that one of them is interpretable. By assumption, we have (

W, R \ f (E), V ), f (x) |= ϕ. Therefore, there is a pair (w, v) ∈ R \ f (E) such that (W, R \ (f (E) ∪ {(w, v)}), V ), f (x) |= ϕ.
This pair of worlds (w, v) is either of the form (f (x), f (x )), (f (x), f (x)), (f (x), w 0 ), (w 0 , f (x)), (w 0 , w 0 ) or simply (w + , w ++ ), for some labels x, x already introduced in this interpretable branch. The first five cases are covered by some of the cases corresponding to the elements of M × M of rule and the last case is covered by the case corresponding to (x + , x ++ ) of rule . So, at least one of the extended branches is interpretable and we can extend the mapping f accordingly.

Proof (Fact 3). We proceed by contraposition. Assume that any extension of the initial interpretable branch closes. Then, any such extension contains an extended labeled formula x E : ϕ and its negation x E : ¬ϕ or two extended labeled formulas x E : p and x F : ¬p. Hence the set of extended labeled formulas of any extended branch is not interpretable. So, by Fact 2, since ϕ is satisfiable by assumption, this entails that the set of extended labeled formulas of the initial branch is also not interpretable, which is impossible by assumption.

Completeness We prove completeness by contraposition. Assume that the tableau for ϕ does not close. Then, there is an open branch in the tableau for ϕ. Let L be the set of extended labeled formulas appearing on this open branch and let T be the set of relation terms appearing on this open branch. We build the Kripke model M = (W, R, V ) as follows:

-W = x | x E : ϕ ∈ L for some ϕ ∈ L s and E ∈ 2 S×S ; -R = {(x 1 , x 2 ) | x 1 Rx 2 ∈ T } and -V (p) = x ∈ W | x E : p ∈ L , for all p ∈ P.
Then, we have the following fact:

Fact 4 For all extended labeled formulas x E : χ,

if x E : χ ∈ L then (W, R \ E, V ), x |= χ. ( 16
)
Proof. We prove Expression ( 16) by induction on the size of χ. The base case χ = p holds by definition of V . We prove the induction steps:

-χ = ϕ ∧ ψ: Assume that x E : ϕ ∧ ψ ∈ L.
Then, by saturation of the tableau rules, we also have that x E : ϕ and x E : ψ are in L. Then, by Induction Hypothesis, we must have that (W, R\E, V ), x |= ϕ and (W, R\E, V ), x |= ψ. Hence, we obtain that (W,

R \ E, V ), x |= ϕ ∧ ψ. -χ = ♦ϕ: Assume that x E : ♦ϕ ∈ L. Then, by saturation of the tableau rules, there is xRx ∈ T such that (x, x ) / ∈ E and x E : ϕ ∈ L. Then, by Induction Hypothesis, (W, R \ E, V ), x |= ϕ and (x, x ) ∈ R \ E. Hence, we have that (W, R \ E, V ), x |= ♦ϕ. -χ = ϕ: Assume that x E : ϕ ∈ L.
Then, by saturation of the tableau rules, there is xRx ∈ T such that (x, x ) / ∈ E and x E∪{(x,x )} : ϕ ∈ L. Then, by Induction Hypothesis, (W, R \ (E ∪ {(x, x )}), V ), x |= ϕ and (x, x ) ∈ R \ E. Hence, we have that (W, R \ E, V ), x |= ϕ.

χ = ¬p: Assume that x E : ¬p ∈ L and assume towards a contradiction that (W, R\E, V ), x |= p. Then, by definition of M, there is a set of pairs of labels F such that x F : p ∈ L. However, if both x E : ¬p and x F : p belong to the same branch, the branch cannot be open, which is impossible by assumption. χ = ¬(ϕ ∧ ψ): Assume that x E : ¬(ϕ ∧ ψ) ∈ L. By saturation of the tableau rules, we have either that x E : ¬ϕ ∈ L or x E : ¬ψ ∈ L. Then, by Induction Hypothesis, we have either that (W, R \ E, V ), x |= ¬ϕ or (W, R \ E, V ), x |= ¬ψ. In both cases, we obtain that (W, R \ E, V ), x |= ¬(ϕ ∧ ψ). χ = ¬¬ϕ: Assume that x E : ¬¬ϕ ∈ L. Then, by saturation of the tableau rules, we obtain that x E : ϕ ∈ L. So, by Induction Hypothesis, we have that (W, R \ E, V ), x |= ϕ, and therefore also (

W, R \ E, V ), x |= ¬¬ϕ. -χ = ¬♦ϕ: Assume that x E : ¬♦ϕ ∈ L.
Then, for all xRx ∈ T such that (x, x ) / ∈ E, x E : ¬ϕ ∈ L by saturation of the tableau rules. Therefore, by Induction Hypothesis, (W,

R \ E, V ), x |= ¬ϕ, for all (x, x ) ∈ R \ E. So, (W, R \ E, V ), x |= ¬♦ϕ. -χ = ¬ ϕ. Assume that x E : ¬ ϕ ∈ L.
Then, by saturation of the rule ¬ of the tableau rules, for all x 1 Rx 2 ∈ T such that (x 1 , x 2 ) / ∈ E, we must have that x E∪{(x1,x2)} : ¬ϕ ∈ L. So, by Induction Hypothesis, this entails that

(W, R \ (E ∪ {(x 1 , x 2 )}), V ), x |= ¬ϕ for all (x 1 , x 2 ) ∈ R \ E. That is, (W, R \ E, V ), x |= ¬ ϕ.
Thus, in particular, since x ∅ : ϕ ∈ L is the root of the tableau for ϕ, we have from Expression (16) that M, x |= ϕ. Hence, ϕ is satisfiable.

This proves the completeness of our tableau method.

A Labeled Sequent Calculus for SML

In classical logic, it is well-known that tableau methods and sequent calculi are interdefinable: proof trees are negated tableau trees turned upside down. Given that our tableau method is based on labeled formulas, we provide a labeled sequent calculus for SML [START_REF] Gabbay | Labelled Deductive Systems[END_REF][START_REF] Negri | Proof analysis in modal logic[END_REF]. First, we define the set of structures L X :

L X : X ::= x : ϕ | xRx | (x, x) | X , X
where x ∈ S and ϕ ∈ L s . We write x ∈ X when x is a label occurring in X and X ∪ {x 0 } is the set of labels occurring in X to which we add the fresh label x 0 . A sequent is an expression of the form X Y , X or X , where X, Y ∈ L X .

Theorem 4 (Soundness and completeness). Let ϕ ∈ L s . Then, ϕ is valid in SML if, and only if, x : ϕ is provable in L SML (defined in Figure 7).

Proof (sketch). Soundness is standard. Completeness follows from Theorem 3 and the following fact: if the tableau for ¬ϕ closes then x : ϕ is provable in L SML . Indeed, a closed tableau tree can be transformed into a proof tree in L SML . Each closed tableau branch is transformed into a branch of the proof tree whose leaf is the axiom x : p , X

x : p, where X gathers all the terms occuring in the tableau branch. Each tableau rule is transformed into a labeled

A , X Y , A A is either x : p, x1Rx2 or (x1, x2) x : ϕ , x : ψ , X Y x : ϕ ∧ ψ , X Y ∧A X Y , x : ϕ X Y , x : ψ X Y , x : ϕ ∧ ψ ∧K X Y , x : ϕ x : ¬ϕ , X Y ¬A x : ϕ , X Y X Y , x : ¬ϕ ¬K x1Rx2 , x2 : ϕ , X Y x2 ∈ X ∪ {x0} x1 : ♦ϕ , X Y ♦A X Y , x2 : ϕ x1Rx2 , X Y , x1 : ♦ϕ ♦K x1Rx2 , (x1, x2) , x : ϕ , X Y (x1, x2) ∈ (X ∪ {x0}) 2 ∪ {(x+, x++)} x : ϕ , X Y A (x1, x2) , X Y , x : ϕ x1Rx2 , X Y , x : ϕ K X , X , Y Z X , Y Z CA
In all rules, (x1, x2) / ∈ X, X, Y can be empty, x2 is not in the conclusion of ♦A.

Fig. 7. Cut-free labeled sequent calculus L SML for SML.

sequent calculus rule via the following correspondences: rules ∧, ¬∧, ¬¬ correspond repectively to

∧ A , ¬ K ∧ K ¬ A , ¬ K ¬ A , and rules ♦, ¬♦, , ¬ correspond respectively to ♦ A , ¬ K ♦ K ¬ A , A , ¬ K A ¬ A .
Moreover, each time the same term is used at several occasion in a tableau branch, we resort in the corresponding proof tree of the sequent calculus L SML to the rule of contraction C A .

Corollary 1. The cut rule and the weakening rule are admissible in L SML .

SML and Other Logics for Relation Change

In the remainder of this paper, we present no further concrete results about SML, but rather place sabotage modal logic against a broader background of logics for relation change, or more generally, model change. We hope that the points to be raised in this way lead toward a better understanding of a landscape of options here that is slowly emerging in the many systems available today.

What is special about SML? Sabotage modal logic has a number of features that make it like a modal logic. It is effectively axiomatizable via translation into first-order logic, even by means of a first-order tableau system, and its expressive power can be measured by invariance under a suitable notion of bisimulation. But perhaps surprisingly, given its simple-looking syntax and semantics, its complexity is high, validity being undecidable. What is the reason for this?

Dynamic-epistemic logic of relation change

One good way of approaching this issue is by comparison with another, and much more widely known modal logic of relation change, namely dynamic-epistemic logic of relation transformers. For a concrete example, think of the operation |ϕ of 'link cutting' for a formula ϕ where, in the current accessibility relation R of a given model, we follow this instruction: Remove all pairs (s, t) where s, t disagree on the truth value of ϕ.

The following result is well-known (cf. for instance [START_REF] Van Benthem | Dynamic logic of preference upgrade[END_REF]).

Fact 5

The dynamic-epistemic logic of link cutting added on top of the basic modal logic is completely axiomatizable, and it is also decidable.

The proof for this result goes by providing 'recursion axioms' in the typical DEL style, that show how to recursively push dynamic modalities inside through standard modalities. The key recursion axiom for link cutting looks as follows:

[|ϕ] ψ ↔ ((ϕ ∧ (ϕ → [|ϕ]ψ)) ∨ (¬ϕ ∧ (¬ϕ → [|ϕ]ψ))) .
Behind this result lies a much more general method, first presented in [START_REF] Van Benthem | Dynamic logic of preference upgrade[END_REF]. Any operation that replaces a relation R in a model by a new relation δ(R) (definable sub-relations are an important special case) automatically generates complete recursion axioms, provided that the transformation to δ(R) be definable in the format of a program in propositional dynamic logic, PDL. 12So, what is the difference between the logics SML and DEL-style logics that accounts for this different complexity behavior? Three contrasts One clear difference is that DEL-style logics say precisely how the new relation is to arise from the old ones: it concerns definable deletions, as opposed to the arbitrary deletions of SML. Another contrast is that SML is about global deletion anywhere in the model, whereas one might think that things improve qua complexity when we work with local relation change only at the current distinguished point of the model. But there is yet one more distinction that may well turn out to be the most crucial one. Definable DEL-style relation change is simultaneous: all pairs not satisfying the given description are eliminated. By contrast, SML works stepwise: it removes links one by one.

In what follows we make a few observations on the last two contrasts, since the first one can be subsumed under these: SML performs stepwise deletions from the universal (and hence definable) relation W × W .

Stepwise versions of DEL

Intuitively, the stepwise nature of SML is a source of complexity, since it blocks any obvious recursion axioms in the DEL style. The main reason is that dynamic modalities cannot be pushed through negations the way they are in DEL, since there can be many ways of performing an SML-deletion, whereas DEL style updates are usually (partial) functions allowing for modality/negation interchanges, as explained for instance in [START_REF] Van Benthem | Logical Dynamics of Information and Interaction[END_REF].

But also in more practical settings, it is well-known that changing classical simultaneous update scenarios such as the Puzzle of the Muddy Children into sequential ones (where children speak in turn) can completely change what happens in the long run, often even blocking any solution to the puzzle.

A good way of understanding the simultaneous/stepwise contrast is by importing the latter into the heartland of dynamic-epistemic logic. We could do this with the above link-cutting |ϕ, but an even simpler way of making the point concerns 'public announcement logic' PAL whose actions !ϕ consists in removing all ¬ϕ-worlds from the current model, assuming that the formula ϕ is true in the distinguished 'actual world' of the current model. As above, PAL is completely axiomatizable using recursion axioms, and it is a decidable logic. Now let us introduce a new action -ϕ into this system that works stepwise:

-ϕ ψ is true at (M, s) iff, after removing some ¬ϕ-point, ψ holds in s.

It is easy to see that this new system, let us call it PAL step , changes the nature of PAL considerably. As explained above, there are no obvious recursion axioms, and even the basic modal invariance property fails.

Fact 6 PAL step is not invariant for standard modal bisimulation.

To see that this is so, just consider one model where point s has one successor t that is ¬p and another model where s has two successors t, t each having ¬p. There is an obvious modal bisimulation between the two models, but -p ♦¬p is true in the second model, but not in the first.

Even so, PAL step is clearly still translatable into first-order logic. However, its behavior in terms of validity is much more opaque than that of PAL itself. In fact, here is an obvious Open Problem Is PAL step decidable?

Truly new semantic methods may be needed for solving problems like this, and it may even be the case that PAL step sides with SML rather than PAL qua complexity 13 -and in that case, stepwiseness would override definability.

A local version of SML

Next, let us briefly consider another dimension of relation change, that might be thought to mitigate the high complexity. Instead of global versions, let us now look at local versions of our systems. For a start consider locSML, a system that arises by specializing everything that we have defined for SML to deletions of links that start at the distinguished point of the current model. 14 Here we provide a few observations to increase familiarity with this system. Some validities All the principles listed earlier (Formulas (1) to ( 6)) as validities of SML are also valid in locSML. Now we exhibit some differences.

Fact 7

The following formula is valid in locSML, but not in SML:

⊥ → ⊥ ( 17
)
And the following formula is valid in SML, but not in locSML:

(♦♦ ∧ ⊥) → ( ϕ → ϕ) (18)
We leave the easy verifications to the reader. In the second formula, the global reading of the deletion modality in the antecedent enforces that the current point is reflexive (cf. formula ( 14)), whereas a local reading would not.

Local locSML vs. global SML. The above remarks highlight the interest of the relation between global sabotage modal logic and its local variant. Within the compass of this paper, we merely provide a few observations.

In one direction, it seems that locSML comes close to being inside SML. We have not been able to settle this in complete detail, but here is one observation about the special class of finitely-branching models.

Fact 8 With finite branching, locSML is invariant under sabotage bisimulation.

Proof. Let Z be a sabotage bisimulation between two finitely-branching models (M, w) and (M , w ). The atomic and Boolean cases are routine. The Zig ♦ and Zag ♦ clauses of Definition 2 take care of ♦-formulas in a standard way familiar from basic modal logic. As for -formulas (where denotes now the local variant of sabotage), assume that M, w |= ϕ. By the semantics of , we have (M, w)r(M 1 , w) and M 1 , w |= ϕ where M 1 is obtained via a local deletion and, by clause Zig of Definition 2, it follows that (M , w )r(M 1 , w ) and (M 1 , w)Z(M 1 , w ). Here the second deletion could be non-local in general, but in our special class, it cannot be. There must be a local deletion that witnesses the transition to M 1 , for otherwise the finite number of successors in (M, w) and (M , w ) would differ, which is not possible under the sabotage bisimulation that still obtains between (M, w) and (M , w )-as we have shown in our discussion of the expressive power of SML. 15 By the induction hypothesis, we then conclude that M 1 , w |= ϕ and, consequently, M , w |= ϕ. Completely similarly, from M , w |= ϕ, we conclude M, w |= ϕ by clause Zag of Definition 2.

If we could show that locSML is invariant for all sabotage bisimulations, then, by the obvious first-order translation of locSML-formulas, our main characterization in Theorem 2 would imply that locSML is embeddable into SML.

Next, we consider the opposite direction. We show how to translate SMLformulas into locSML-formulas, when some extra expressivity typical of hybrid logics [START_REF] Areces | Hybrid logics[END_REF] is added: the universal modality and the binder ↓. Let us first fix the translation (with the atomic case and Boolean clauses omitted):

16 t( ϕ) ↓ x.(x ∧ E l E(x ∧ t(ϕ)))
where E is the diamond of the universal modality, x is a state variable and l denotes the local sabotage operator. It is easy to see that:

M, w |= ϕ iff M, w |= t(ϕ).
where t is the translation defined above.

However, the price is high. It is known that standard modal logic plus the binder and the universal modality is equivalent to the first-order correspondence language itself (cf. [START_REF] Areces | Hybrid logics[END_REF]). Perhaps much weaker means would suffice. So, the direct relation from SML into locSML remains unresolved.

Given this uncertainty about the precise relation between global and local sabotage logic, the complexity of reasoning in the latter also poses questions:

Open Problem Is locSML decidable?

Our inclination is to doubt this, but we have not been able to give a proof.

Excursion: local DEL

Instead of pursuing the issues raised so far, we merely note that 'going local' need not be a force for simplicity in the other realm that we have contrasted with SML, namely, dynamic-epistemic logic DEL.

Suppose that we define a local version of link-cutting |ϕ loc as cutting links only between the current world and its accessible worlds. There are many concrete scenarios where this makes sense, for instance, when describing some local event of changing a communication link between agents in a network (cf. [START_REF] Seligman | Facebook and epistemic logic of friendship[END_REF]). 17Again we will see immediately that the typical DEL method of recursion axioms is going to fail. For, when we push a dynamic modality under a standard modality over successors of the current world, the link-cutting change is no longer local in these successors: it takes place somewhere else.

Localization and hybrid logic Now, this problem can be solved, since, as in all logics that we are discussing here, all changes take place definably inside first-order logic. But in order to find recursion axioms for local link-cutting, or similar local relation-changing operations, we will have to be able to refer back to other worlds where local changes took place. In first-order terms, this means that we need a mechanism for variable binding. In modal terms, we can use devices from hybrid logics [START_REF] Areces | Hybrid logics[END_REF], such as the universal modality, and especially the 'binder' ↓, to which we referred also in the previous section. It is a relatively standard exercise to provide recursion axioms for local link-cutting in a hybrid modal language, but we will not do so here. However, there is no guarantee that such a hybrid extension of the modal base logic is still decidable, since hybrid logic with a universal modality plus downarrow is undecidable. 18 In all, we conclude that introducing locality may be natural, but its complexity effects on logics of relation change are still ill-understood.

General logics of model change

We have identified a few general dimensions that affect design and complexity of logics for relation change. Clearly, there are many more systems of this sort that we could discuss here: even DEL itself has developed more sophisticated update mechanisms than those that we presented. But we hope to return to the more general structure of this landscape in followup work. Here, we will just make a few references to further modal and first-order logics of relation change in Section 8, and give a first rough road map.

Sabotage Games and Fixpoint Logics

So far, we have looked at dynamic logics that describe single steps of model change, or more concretely, relation change. But the original sabotage game motivating a logic like SML was a many-step scenario unfolding over time, and these games have strategic global structure in the long run, going beyond local steps. What logic would naturally represent this structure? In this section we offer a few remarks that may clarify this issue, and show its interest.

The sabotage game

The sabotage game was introduced in [START_REF] Van Benthem | An essay on sabotage and obstruction[END_REF], further studied in [START_REF] Löding | Solving the sabotage game is PSPACE-hard[END_REF], and more recently in [START_REF] Gierasimczuk | Learning and teaching as a game: a sabotage approach[END_REF][START_REF] Velázquez-Quesada | Small Steps in the Dynamics of Information[END_REF], and [START_REF] Van Benthem | Logic in Games[END_REF]Ch. 23]. It can be viewed as a game variant of a reachability problem where a player, Traveler, aims at reaching a predefined goal state (or goal region), while obstructed by the second player, Demon. We provide a short presentation of the game but we refer the reader to the above literature for more details and motivations, which range from studying the performance of algorithms under adverse circumstances to scenarios in learning theory. 18 As we observed earlier, hybrid logic with a universal modality plus the binder ↓ is equivalent to the first-order correspondence language. It would be of interest to push things down to, say, hybrid logic with the 'at-operator' @ plus the binder, but even then we are in the undecidable 'Bounded Fragment' of the first-order language.

The game is played on a frame (W, R) with a designated point w corresponding to the starting position of Traveler, and a designated non-empty subset G ⊆ W (typically, a singleton for some designated point to be reached) corresponding to the 'goal' region of Traveler. Traveler moves locally by navigating the edges of R, one at the time, thereby constructing a path. Demon moves by deleting edges from R. The game proceeds in turns with Demon moving first. Traveler wins if she has reached her goal region. Otherwise Demon wins.

The sabotage game as defined above is a, possibly infinite, two-player, zerosum, perfect information extensive form game. As such it is determined, that is, either Traveler or Demon has a winning strategy. In the case in which the graph W is finite, this determinacy is a consequence of Zermelo's theorem [START_REF] Zermelo | Über eine anwendung der mengenlehre auf die theorie des schachspiels[END_REF]. In the general case, determinacy follows from the Gale-Stewart theorem [START_REF] Gale | Infinite games with perfect information[END_REF], as it is easy to see that the set of runs of the sabotage game where Traveler wins by reaching the goal is an open set in a standard topological sense. 19However, the case of reachability in standard directed graphs that has been paradigmatic for this paper trivializes the sabotage game. In the case in which Traveler's goal region is represented by a single state (that is, the original sabotage scenario), we have the following simple fact: Fact 10 Let (W, R) be a directed graph. If the goal region G ⊆ W is a singleton not containing the initial position of Traveler, then the Demon has a winning strategy in the sabotage game played on (W, R).

Proof. Unless Traveler started in the exit point, Demon has a winning strategy. Demon cuts the link between the current position of the Traveler and the exit node if there is such a link, otherwise he cuts an arbitrary link. If Demon keeps doing this, Traveler never reaches the exit node. In a finite game, this is enough. On an infinite graph, this game can be infinite, but Demon will always produce infinite histories where Traveler does not reach the exit. This is enough.

Obviously this trivialization does not go through if Traveler's goal region contains more than one state, perhaps defined by some goal formula, and this is the more general setting that we will assume in what follows. 20As we will see now, a natural extension of the language of SML can yield the expressivity to characterize winning positions in the sabotage game. It reflects a much more general point about game solutions, developed at length in [START_REF] Van Benthem | Logic in Games[END_REF]: game-theoretic equilibria are definable in fixed-point logics for induction and recursion, and often even, in modal fixed-point logics.

Expressing winning regions in the sabotage game

Our earlier observations pose tests for logics of sabotage games. In particular, Fact 10 suggests that the basic sabotage modal logic SML, possibly with some extra resources, should be able to express the existence of Demon's winning strategy as a validity. Here is such a formula, using two additional modal devices:

U ((¬goal ∧ ♦ ) → ¬goal) (19)
with U the universal modality and goal a nominal for the goal point.

Next, for arbitrary goal regions (singletons or not) defined by the formula goal, the original paper [START_REF] Van Benthem | An essay on sabotage and obstruction[END_REF] observes how the existence of winning strategies for Traveler can be expressed in a PDL-format over SML. At least on finite graphs, the winning positions for Traveler can be defined using an operator for finite iteration, by the formula:

(♦ ∧ ♦) * goal (20)
capturing the infinitary disjunction goal ∨ (♦ ∧ ♦goal) ∨ (♦ ∧ ♦(♦ ∧ ♦goal)) . . . and so forth. Notice that the conjunct ♦ is required to rule out as a winning position the situation in which there are no edges to be deleted in the model but Traveler is not in a goal state. This characterization of Traveler's winning positions, however, does not work on infinite graphs, and in general, a more expressive language is needed.

Let us consider a µ-calculus language µSML in order to define winning positions for Traveler (and Demon) with formulas whose syntax matches the chosen definition of winning positions. Let P be a set of propositional atoms. Formulas of the sabotage modal language L µ have the following grammar in BNF:

L µ : ϕ ::= p | ¬ϕ | (ϕ ∧ ϕ) | ♦ϕ | ϕ | µp.ϕ(p)
where p ∈ P and ϕ(p) indicates that p occurs free in ϕ (i.e., it is not bounded by fixpoint operators) and under an even number of negations. Here, just as ordinary modalities, sabotage modalities do not affect positive or negative occurrence. Fixpoint operators allow us to generalize Formula (20) and characterize the set of Traveler's winning positions in its full generality, via the formula:

µp.(goal ∨ (♦ ∧ ♦p)) (21)
We have not given a precise semantics for µSML yet, but intuitively the formula makes sense for our game. Traveler is in a region that includes the goal points or to which she can return no matter what Demon deletes.

By the determinacy of the sabotage game, the dual formula of ( 21) should then define the winning region for Demon, which is therefore the largest fixpoint of the equation p ↔ ¬goal∧( ⊥∨ p). Viewed in this light, the earlier Formula [START_REF] Fervari | Relation-Changing Modal Operators[END_REF] for Demon stated that ¬goal is such greatest fixpoint for singleton goals.

Notice how the very shape of the above fixed-point formula mirrors the precise winning conventions of the game for the players. Clearly, this is a general and flexible feature of logical syntax, to which we will return later on.

The sabotage µ-calculus: µSML

To make the preceding precise, we need to specify the semantics of µSML. This may seem obvious: one copies the standard definitions for the µ-calculus 21 and adds a clause for , noting that this new operator does not affect positive occurrence. The logic resulting from this obvious extension of the µ-calculus semantics has indeed been studied in [START_REF] Rohde | On the mu-calculus augmented with sabotage[END_REF]. However, this does not yield the intended semantics for analyzing our games, as shown by the following example.

Example 7. Consider a graph as depicted concretely in Figure 8 with vertices W = {1, 2, 3, 4, 5}, and directed edges R = {(3, 1), (3, 2), (4, 3), (4, 2), [START_REF] Areces | Hybrid logics[END_REF][START_REF] Areces | Relation-changing modal operators[END_REF], (5, 3)}, whose goal region goal is {1, 2}. Computing, bottom up, the successive approximation stages for the function denoted by goal ∨ (♦ ∧ ♦p) yields this sequence of subsets of the graph: ∅, {1, 2}, {1, 2, 3}, {1, 2, 3, 4}, {1, 2, 3, 4, 5} which ends in the fixpoint {1, 2, 3, 4, 5}. The reason is that, as the set grows, further points get at least two successors inside it, so one link deletion can never prevent them from getting there. However, this outcome is wrong, since point 5 is not a winning position for Traveler in the graph game as we have defined it. Demon can win by starting with cutting the link (3, 1) and then continuing to cut appropriately as Traveler tries to move to a goal point.

What has gone wrong here? The problem is the model-changing character of the modality : the same formula may get different truth values at the same points in the two models before and after a link deletion. Using a mere set of points as the current approximation does not keep track of this in the right way. An improved semantics that does work will only be sketched here.

One direct approach defines syntactic approximation formulas ϕ α for each ordinal α, in an infinitary version of sabotage modal logic SML. In any given model, this sequence will stabilize at some stage after which all later formulas in the sequence have the same truth-set, thereby computing the smallest fixpoint. Of course, the formula at that stage may depend on the size of the model. 22 But our preferred approach is semantic, changing the relevant universe of evaluation to better fit our intuitions, and in line with the notion of sabotage bisimulation (Definition 2). Instead of working on just the original graph, we consider a dynamic model M consisting of this graph and all those obtainable from it by edge deletions. We take the points of this new model to be pointed models (M, s), and let the modality ♦ access the relation between (M, s), (M, t) with (s, t) ∈ R M , and access the sabotage relation r between (M, s) and (M -, s) where M -arises from M by deleting one directed edge. 23 Now we can just compute on this model with the original formula, and get an increasing family of sets that yields the same results as the syntactic procedure.

We leave it to the reader to recompute the earlier example in terms of pointed models, and check that we now get the intended interpretation.

The system obtained in this way is not a simple extension of the µ-calculus. It is still easy to show that µSML formulas are invariant under sabotage bisimulation. It is less clear, however, how to extend the earlier standard translation ST . It might seem to extend immediately to a translation into FO(LFP), the extension of first-order logic with fixed-point operations, by taking modal µp to first-order µP, x. But this fails to capture evaluation with different truth values across models. Finally, there is a major issue of complexity. This can be illustrated with the logic PAL * of public announcement logic with finitely iterated announcements. Its formulas (!ϕ) * ψ may be seen as solutions for a fixpoint formula µp.ψ ∨ !ϕ p computed in our sense across different models. But [START_REF] Miller | The undecidability of iterated modal relativization[END_REF] shows that, unlike the µ-calculus, this system is undecidable, in fact its satisfiability problem is Π 1 1 -complete. We leave these matters for future investigation.

Coda Our semantic view with pointed models as the new indices of evaluation also has some independent interest, in that it suggests a natural generalization. A universe need not be a full 'standard model' with all possible variants, say some initial model plus the family of all its sub-models. We could also allow only 'admissible models' in the universe according to some criterion, giving us much more variety in patterns for the model shifts. 24 On such more general models, the complexity of our logical systems might well decrease. 22 One might think that this is the same as working with just sets, since in the standard µ-calculus, 'call by name' and 'call by value' are equivalent in the approximation procedure. But this only holds in one fixed model, not across models where, as we saw in the above example, truth values can differ. 23 Essentially, we are now in a bimodal model of a special sort, where the atomic goal formula holds for the same points across different sub-graphs. 24 Such universes are studied in dynamic-epistemic logic as 'protocol models', cf. [START_REF] Van Benthem | Merging frameworks for interaction[END_REF].

General graph games

The general background for the topic of this section is that of graph games. To put the sabotage game in perspective, we briefly consider two more such games.

The travel game For a start, here is a simple game that leaves a given graph unchanged. In the Travel Game, Demon picks an outgoing edge of the current point, Traveler has to pick an edge to move from there, and so forth. This time, Traveler wins if Demon cannot issue a challenge (i.e., we are at an endpoint that is Demon's turn), or if Traveler can keep moving forever. This game has been applied widely to model-checking or other logical tasks (cf. [START_REF] Van Benthem | Modal Logic for Open Minds[END_REF]), given the great freedom in what we can define to be a graph for the task at hand. The game is determined, and winning positions can be described simply in the modal µ-calculus. In particular, those for Traveler are given by the greatest fixed-point formula

νp. ♦p (22)
The modal µ-calculus is a high-level theory of this, and similar graph games.

In contrast with the above, the Sabotage Game changes the underlying graph drastically. 25 Accordingly, winning conditions required using a µ-calculus extended with sabotage modalities (cf. Section 7.3).

The poison game Finally, consider a game that does not change graph links, but that changes the 'annotation' of a graph: i.e., unary properties of its nodes. The Poison Game of [START_REF] Duchet | Kernels in directed graphs: A poison game[END_REF] has Demon issuing a challenge as in the Travel Game, while Traveler has to respond. However, now Demon 'poisons' each node that he visits, making it inaccessible to Traveler: she loses if she visits a poisoned node. Traveler wins this game if she can keep going. In the game of the cited paper, the first move is for Traveler, who picks any node as a starting point.

This game captures an important graph-theoretic notion. A 'local kernel' is a non-empty set of nodes that has no internal edges (a so-called independent set), while for every edge leading outside the set, there is a follow-up edge returning into the set. 26 It can be proved relatively easily that, on finite branching and upward well founded graphs, there is a local kernel if and only if Traveler has a winning strategy.

But the Poison Game also has independent interest, and describing winning positions for Traveler suggests the following definition for the winning positions of the Traveler. Consider a µ-calculus with a special predicate P for 'poisoned', and an added modality [+P ]ϕ which says that ϕ holds at the current point s of the model after this has been poisoned. That is, the operation +P changes the current interpretation for P to add the singleton s. νq.¬P ∧ [+P ]♦q [START_REF] Gale | Infinite games with perfect information[END_REF] Intuitively, this language with a dynamic poison modality seems intermediate between the pure µ-calculus and the sabotage µ-calculus. 27 The poison modality involves only what is called 'factual change' of propositional valuations in dynamic-epistemic logic [START_REF] Van Benthem | Logics of communication and change[END_REF]. There are recursion axioms for this modality pushing it through all other operators, turning formulas into equivalent static ones. Still, even though the modal µ-calculus is closed under DEL product update [START_REF] Van Benthem | Modal fixed-point logic and changing models[END_REF], we believe that our caveat for µSML applies also to the a µ-calculus extended with the poison modality, and a new semantics is needed.

8 Related Work

Other recent studies of sabotage logic

As we have noted right at the start, the complexity and model-theory of SML has been studied extensively in a recent series of works [START_REF] Areces | Moving arrows and four model checking results[END_REF][START_REF] Areces | Swap logic[END_REF][START_REF] Areces | Tableaux for relation-changing modal logics[END_REF][START_REF] Areces | Relation-changing modal operators[END_REF] and [START_REF] Fervari | Relation-Changing Modal Operators[END_REF]. In particular [START_REF] Fervari | Relation-Changing Modal Operators[END_REF][START_REF] Areces | Relation-changing modal operators[END_REF] established that the model-checking problem of SML is PSPACE-complete, that SML lacks the finite model property, the tree-model property and that its satisfiability problem is undecidable. This considerably improved the same results obtained for the multi-modal variant of SML in [START_REF] Löding | Solving the sabotage game is PSPACE-hard[END_REF][START_REF] Löding | Model checking and satisfiability for sabotage modal logic[END_REF]. Our paper contributes further results-specifically, a charaterization theorem-to this specific line of research on the model-theory of SML.

The cited authors also introduce a tableau method for SML in [START_REF] Areces | Tableaux for relation-changing modal logics[END_REF]. They use a special system of nominals in their tableaux, which represent possible worlds. This allows more control over the application of the tableau rules than the calculus in this paper. Indeed, in the rules and ♦, instead of considering all possible combinations of nominals as we do, their method uses a refinement of the usual diamond rule of modal logic with nominals, together with an extra rule called (ub) that suitably 'controls' the combination of all the nominals. Even though these features may make the tableaux in [START_REF] Areces | Tableaux for relation-changing modal logics[END_REF] slightly less transparent in terms of how the rules relate to the underlying semantics of SML it may well make the system more efficient than ours from a computational standpoint.

Argumentation games

Abstract argumentation theory [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] studies criteria for tenability of positions in argumentation. Its key structures are directed 'attack graphs' (frames) G = (W, R) where W is a non-empty set of arguments and R is a binary relation aRb interpreted intuitively as saying that argument b attacks (is stronger than)

X is conflict-free iff a, b ∈ X s.t. aRb X is self-defended iff ∀a, b if a ∈ X and aRb then ∃c ∈ X s.t. bRc
X is a complete set iff X is conflict-free and X = {a | ∀b, if aRb then ∃c ∈ X and bRc} X is the grounded set iff X is the smallest complete set Table 1. Some key notions of abstract argumentation theory from [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF].

argument a. 28 All graphs illustrated in this paper can therefore be interpreted as attack graphs, but we provide a further example in Figure 9.

A basic question is: given an attack graph, which set of can be rationally upheld? Answers give rise to different criteria for the 'quality' of sets of arguments. We list some basic ones in Table 1. As shown in a series of works [START_REF] Grossi | On the logic of argumentation theory[END_REF][START_REF] Grossi | Argumentation theory in the view of modal logic[END_REF][START_REF] Grossi | Fixpoints and iterated updates in abstract argumentation[END_REF][START_REF] Gabbay | When are two arguments the same? equivalence in abstract argumentation[END_REF], all these notions have a modal character, making modal (fixpoint) logics a natural tool for argumentation theory. In particular, µp. ♦p [START_REF] Gierasimczuk | Learning and teaching as a game: a sabotage approach[END_REF] defines the notion of grounded set [START_REF] Grossi | On the logic of argumentation theory[END_REF][START_REF] Grossi | Argumentation theory in the view of modal logic[END_REF][START_REF] Gabbay | When are two arguments the same? equivalence in abstract argumentation[END_REF], that is, the set of arguments that can always be ultimately defended by a set of unattacked arguments. This intuition is naturally illustrated by the stages of approximation of Formula (24): the empty set; the set of arguments whose attackers are in turn attacked by arguments in the empty set, that is, the unattacked arguments; and so forth. Formula (24) defines the winning positions in a game for Traveler (the 'Proponent' in argumentation theory) who wins if, and only if, she reaches an argument that is unattacked, while Demon (the 'Opponent') is out of counter-arguments. 29Games played on attack graphs occur in the argumentation literature as 'dialectical' procedures for 'static' structural criteria of acceptability of arguments (see [START_REF] Modgil | Proof theories and algorithms for abstract argumentation frameworks[END_REF] for an overview). For instance, a close relative of our earlier poison game is the game for 'credulous admissibility' in [START_REF] Vreeswijk | Credulous and sceptical argument games for preferred semantics[END_REF]. Traveler selects attacks to the last argument selected by Demon and, as in the poison game, cannot select any argument previously selected by Demon. Demon plays by selecting attacks to any argument previously selected by being allowed to backtrack. Demon starts. Traveler wins if she does not run out of counter-arguments. It can be shown [START_REF] Vreeswijk | Credulous and sceptical argument games for preferred semantics[END_REF] that Traveler has a winning strategy if, and only if, the initial argument is included in a conflict-free and self-defended set (that is, a semi-kernel).

Again, suitably enriched fixpoint logics can capture such games. For instance, using the notation of Section 7.4, Traveler's winning positions are defined by

νq.((V ∧ ¬P ) ∧ U (V → [+P ]♦[+V ]q)) (25)
with U the universal modality, P the 'poison' predicate, while V keeps track of the points visited by Traveler. A modal logic of graph games as envisioned in our paper may well have significant applications to abstract argumentation theory.

Landscape of logics for model change

Often triggered directly by the initial work on dynamic-epistemic logic and sabotage modal logic, many further logics of graph modifiers have been proposed in the recent literature than what we have covered here. Besides the above mentioned series of work [START_REF] Areces | Moving arrows and four model checking results[END_REF][START_REF] Areces | Swap logic[END_REF][START_REF] Areces | Tableaux for relation-changing modal logics[END_REF][START_REF] Areces | Relation-changing modal operators[END_REF], relevant systems include local and global graph modifiers [START_REF] Aucher | Global and local graph modifiers[END_REF], dynamic epistemic modifiers [START_REF] Baltag | The logic of public announcements and common knowledge and private suspicions[END_REF][START_REF] Baltag | Logics for epistemic programs[END_REF], dynamic modal logic DML [START_REF] De Lavalette | Changing modalities[END_REF], arrow logic [START_REF] Kooi | Arrow update logic[END_REF], logics of copy and remove [START_REF] Areces | Logics with copy and remove[END_REF], the logic of preference upgrade [START_REF] Van Benthem | Dynamic logic of preference upgrade[END_REF], and general dynamic dynamic logic [START_REF] Girard | General dynamic dynamic logic[END_REF]. 30 Instead of discussing the above terrain in detail, we give a small 'expressiveness map' based on what can readily be observed, and on what authors have claimed. 31 In Figure 10, an arrow L 1 → L 2 means that logic L 1 is strictly more expressive than L 2 . When there is no arrow between two logics, they are incomparable in terms of expressiveness. Here is how one can read the map.

At the bottom level, there is just basic modal logic, which is expressively equivalent to dynamic modal logic DML (cf. [START_REF] De Lavalette | Changing modalities[END_REF]), arrow logic (cf. [START_REF] Kooi | Arrow update logic[END_REF]) and preference upgrade logic (cf. [START_REF] Van Benthem | Dynamic logic of preference upgrade[END_REF]). One step up, at the middle level of our map, we find SML and the other logics inspired by it later, such as swap logic, bridging logic, and local sabotage logic in the sense of [START_REF] Areces | Moving arrows and four model checking results[END_REF][START_REF] Areces | Swap logic[END_REF]. 32 From the cited publications, 30 Also relevant here is [START_REF] Gabbay | Reactive Kripke Semantics[END_REF] on 'reactive logics', where the accessibility relation of modal models is changed during the interpretation process of formulas. 31 Here we disregard logics with Kleene * or fixed-point extensions, where things can be different. In particular, we do not treat general dynamic dynamic logic, cf. [START_REF] Girard | General dynamic dynamic logic[END_REF], which is equivalent to P DL. Also, we were unable to fit in the logics of copy and remove. 32 As observed earlier (footnote 14) the system of 'local' sabotage from [START_REF] Areces | Moving arrows and four model checking results[END_REF][START_REF] Areces | Swap logic[END_REF] is subtly different from the one we considered in this paper.

LocGM L [START_REF] Aucher | Global and local graph modifiers[END_REF] SML [START_REF] Van Benthem | An essay on sabotage and obstruction[END_REF] Swap [START_REF] Areces | Moving arrows and four model checking results[END_REF][START_REF] Areces | Relation-changing modal operators[END_REF] Bridging [START_REF] Areces | Moving arrows and four model checking results[END_REF][START_REF] Areces | Relation-changing modal operators[END_REF] Local sabotage à la [START_REF] Areces | Moving arrows and four model checking results[END_REF][START_REF] Areces | Relation-changing modal operators[END_REF] Arrow logic [START_REF] Kooi | Arrow update logic[END_REF] Preference upgrade logic [START_REF] Van Benthem | Dynamic logic of preference upgrade[END_REF] DML [START_REF] De Lavalette | Changing modalities[END_REF], DEL [START_REF] Baltag | The logic of public announcements and common knowledge and private suspicions[END_REF][START_REF] Baltag | Logics for epistemic programs[END_REF] Fig. 10. Expressiveness map of some dynamic modal logics for graph modifiers.

we know that these mid-level systems are incomparable in terms of expressivity, that they are also strictly more expressive than the basic modal logic (cf. [START_REF] Areces | Relation-changing modal operators[END_REF]) and, at the same time, strictly less expressive than the full hybrid language with universal modality plus binders (cf. [START_REF] Areces | Tableaux for relation-changing modal logics[END_REF]). Incidentally, some of these intermediate systems (e.g., swap logic) have been also shown to be strictly less expressive than the so-called Bounded Fragment of FOL, which is undecidable, but still natural, cf. [START_REF] Areces | Swap logic[END_REF]. Finally, the logic of local and global graph modifiers proposed in [START_REF] Aucher | Global and local graph modifiers[END_REF] arose from combining features of all these systems, and it has been shown to be at least as expressive as hybrid logic with the universal modality plus binders-that is, the full FOL correspondence language.

A similar map would make sense for fixed-point extensions of the logics in this paper. In Section 7, we used the modal µ-calculus, and extensions with DEL-style dynamic modalities. Another natural extension given our comparison of sabotage logics and dynamic-epistemic logics is a fixed-point logic µ(↓, U ) containing the base modalities plus the universal modality and the hybrid binders. This provides the expressive power needed to deal with local sabotage and other dynamic operations that have embedded references to earlier points of evaluation. The literature on graph change also contains other such systems, 33 many of them in between the modal µ-calculus and the logic LFP(FO), first-order logic with fixed-point operators. The latter system is Π 1 1 -complete, but it forms a natural limit for many fixpoint logics. However, we have also introduced a sabotage µcalculus that seemed a much more radical expressive extension. Even lacking a road map like our earlier one, we believe that just an awareness of this realm beyond first-order logic poses interesting challenges, such as exploring the reach of current automata-theoretic methods for fixpoint logics.

Of course, comparing logics by mere expressiveness is a drastic projection of their different dynamic motivations, and our map is only a first step. We can compare these systems in other ways, and in particular, the stated equivalences are all up for further investigation if we generalize to temporal protocol models, where the usual reduction axioms become invalid. We leave a more sensitive and detailed analysis of the area of logic for model change to future work. 34

Conclusions and Future Work

In this paper, we have dusted off sabotage modal logic, and looked at its broader current relevance. We gave a first-order translation for this logic, proved a novel characterization theorem in terms of a new notion of sabotage bisimulation, and introduced a sound and complete tableau system and sequent calculus.

Still, SML remains an under-investigated system. For instance, we noted that the schematic validities of SML form a natural subset whose axiomatizability, or decidability, is an open problem. Another natural theme is modal correspondence theory, whose techniques extend into higher-order logic [START_REF] Van Benthem | Modal Logic and Classical Logic[END_REF]. In particular, can the Sahlqvist theorem be generalized to SML? Also, in this paper, we arrived at natural variations of SML, such as its version with only local deletions, whose decidability is open. 35 Next, given the apparent complexity of the system, it makes sense to look at natural fragments, such as the closed formulas that formed many of our examples, or the formulas of sabotage depth 1. Alternatively, in line with a suggestion in Section 8.3, we could look at 'protocol models' [START_REF] Van Benthem | Merging frameworks for interaction[END_REF], that restrict the sequences of available link deletions between graphs, giving rise to bimodal models with an 'internal' accessibility relation R for ♦ and an 'external' relation r for . Finally, we also found SML-inspired new versions of dynamicepistemic logics, such as stepwise PAL, whose properties seem unknown.

Next, we have presented sabotage modal logic as a member of a species, that of modal logics describing model changes. We have identified some of its basic features, and in particular, its arbitrary non-definable and stepwise character, setting it apart, for instance, from the better-studied DEL world. We see our way of looking as the start of something more ambitious, finding a better map of the 34 Our discussion here has been model-theoretic, in terms of semantic invariances and expressive power. But there are also other ways of achieving generality in the rich and growing landscape of dynamic logics for model change. Alternatively, one could use algebraic methods, category-theoretic methods, or proof-theoretic perspectives, which might suggest systematizations of their own. One such alternative approach that we would like to mention specifically for its general power, is the framework of 'update logic' [START_REF] Aucher | Displaying updates in logic[END_REF], based on display-style substructural proof theory. 35 Other natural variations include multi-modal SML with indices for the relations to be cut, [START_REF] Löding | Solving the sabotage game is PSPACE-hard[END_REF][START_REF] Löding | Model checking and satisfiability for sabotage modal logic[END_REF], or logics of adding links, like the aforementioned modal logics of bridging [START_REF] Areces | Relation-changing modal operators[END_REF]. In this connection, note that adding links to R is the same as deleting links from the complement -R, so there are connection laws to be had.

whole field of logics for model change, and the major parameters that determine their complexity. But to us, the greatest challenge would be a general perspective on dynamic logics of model change that leads to general theorems beyond those for specific logics. We made some suggestions to this effect in Section 8, but clearly this was just a start. Next, returning to the games that motivated SML in the first place, we discussed sabotage µ-calculus as a system for defining strategic powers of players, and as a testing ground for introducing model-changing modalities that can affect the process of approximation leading to the usual smallest or greatest fixed-points. The system we define seems a very natural object of study in its own right. And as we have seen in Section 8, it suggests broader issues about the landscape of further fixed-point logics for model change.

But more importantly than just studying logics, the sabotage game reminds us of a general issue of gamification: the use of newly designed games to model significant computational or social scenarios, as argued for in [START_REF] Van Benthem | Logic in Games[END_REF].

Sabotage games model real dynamic scenarios unfolding over time, beyond one-step model changes. There are many natural variations on the original scenario in [START_REF] Van Benthem | An essay on sabotage and obstruction[END_REF] -and these may serve as pilots for more general games played over networks, such as the argumentation games of [START_REF] Grossi | On the logic of argumentation theory[END_REF][START_REF] Gabbay | When are two arguments the same? equivalence in abstract argumentation[END_REF] discussed earlier, or the social network games of [START_REF] Van Benthem | Oscillation, logic and dynamical systems[END_REF] and [START_REF] Christoff | Dynamic Logics of Networks[END_REF]. 36 Such network games need not be about 'sabotage' at all, and the general area becomes that of games that may change their own playground, for which this paper has provided some logical tools.

Fig. 1 .

 1 Fig. 1. A model showing that the general schema ϕ → (♦ → ♦ϕ) fails in SML. Let ϕ ♦♦p, let V (p) = {a}, and let the evaluation point be e.

  (a) If C s (ϕ) |= ϕ, then ϕ is equivalent to the translation of an L s -formula. (b) C s (ϕ) |= ϕ -that is, for any pointed model (M, w): if M |= C s (ϕ)[w], then M |= ϕ[w]. Claim (a). Assume that C s (ϕ) |= ϕ. From the deduction and compactness theorems for FOL, we have that |= Γ → ϕ for some finite Γ ⊂ C s (ϕ). The converse holds by the definition of C s (ϕ): |= ϕ → Γ . We thus have that |= ϕ ↔ Γ , proving the claim.

Fig. 2 .

 2 Fig.2. Two s-bisimilar models (the s-bisimulation runs via the dashed lines). At state d to the left, the property "every two successors share a joint successor" is true. But it fails at point d in the model to the right.

  2.6]. Then, by the invariance of FOL under elementary extensions, from M |= ϕ[w] (by the construction of Σ), we get that M ω |= ϕ[w]. By the assumption that ϕ is invariant for s-bisimulation and Proposition 3, we get M ω |= ϕ[w] -and then, by elementary extension, M |= ϕ[w]. This completes the proof.

Fig. 3 .

 3 Fig. 3. Two infinite chains (N, ≥) and (N, >), with transitive edges omitted in both frames. Only the part of the s-bisimulation relation originating in points 1 and 2 is depicted. The remaining edges at other points are positioned similarly.

Fig. 4 .

 4 Fig. 4. Construction of a SML tableau.

Fig. 5 .

 5 Fig. 5. Tableau rules for SML.

Fact 9

 9 For any formula ϕ of SML and pointed model (M, w):

Fig. 8 .

 8 Fig. 8. Graph on which the sabotage game is played in Example 7.

Fig. 9 .

 9 Fig. 9. An attack graph.

  for any atom p. Zig ♦ : If (M 1 , w)Z(M 2 , v) and there exists w ∈ W 1 s.t. wR 1 w then there exists v ∈ W 2 s.t. vR 2 v and (M 1 , w )Z(M 2 , v ); Zag ♦ : If (M 1 , w)Z(M 2 , v) and there exists v ∈ W 2 s.t. vR 2 v then there exists w ∈ W 1 s.t. wR 1 w and (M 1 , w )Z(M 2 , v ); Zig :

  to x E : ψ (or the pair x E : ψ, x1Rx2):if the tableau rule is rule ¬∧ (or rules ♦, ), add two successor nodes (resp. n + 1, n successor nodes) to the branch labeled with the instantiations of the denominators of that rule, otherwise, add a unique successor node labeled with the instantiation of the denominator(s) of that rule. (c) i. Label by × (closed ) the (new) branches which contain two extended labeled formulas x

E : p and x F : ¬p (where E and F may possibly be different sets) or two extended labeled formulas x E : ϕ and x E : ¬ϕ. ii. Label by (open) the (new) branches where there are no more formulas to decompose.

One can check[START_REF] Blackburn | Modal Logic[END_REF] Ch.

2.4] for basics of this first-order correspondence language.

A formula ϕ of a language L is a schematic validity on a class of models if σ(ϕ) is valid in that class for any substitution σ of arbitrary formulas for proposition letters.

The analogous open problem for the much simpler dynamic-epistemic logic PAL of public announcement was only solved in[START_REF] Holliday | Schematic validity in dynamic epistemic logic: Decidability[END_REF]: it turned out to be decidable.

Stating and proving precise succinctness results for SML is in fact one more interesting open problem about sabotage modal logic.

For example, our earlier formula ♦ ∧ ♦ ∧ ⊥ in Section 2 was true in a model if and only if its underlying frame consists of one reflexive point.

If we remove the rules for sabotage we get a sound and complete tableau method for logic K that is somewhat non-standard and computationally demanding.

For instance, for link cutting such a PDL program definition would look as follows: (?ϕ; R; ?ϕ) ∪ (?¬ϕ; R; ?¬ϕ).

A different type of 'local' sabotage is studied in[START_REF] Areces | Moving arrows and four model checking results[END_REF][START_REF] Areces | Relation-changing modal operators[END_REF], whose modality refers to the model transformation that deletes an outgoing edge from the evaluation point and moves the evaluation point to the target of the deleted arrow.

This brute-force argument would fail in the presence of infinitely many successors.

From a hybrid logic point of view, we are now extending the hybrid logic known as H(E, ↓) with a local sabotage operator. Hybrid logics will return in Section 8.

In[START_REF] Seligman | Facebook and epistemic logic of friendship[END_REF] the authors assimilate this case to that of DEL-style deletions when the link to be deleted runs between two worlds having unique nominals as their names.

Cf.[START_REF] Van Benthem | Logic in Games[END_REF] on the background of these results in current logics of games.

Other non-trivial variations arise when Traveler is allowed to move first, or if more than one link is allowed between points (the original sabotage game was played over 'multi-graphs'), or if we allow multi-relational frames, as in[START_REF] Löding | Solving the sabotage game is PSPACE-hard[END_REF].

The standard clause is M, w |= µp.ϕ(p) iff w ∈ X ∈ 2 W | ||ϕ|| M[p:=X] ⊆ X ,where ||ϕ|| M[p:=X] is the truth-set of ϕ with V (p) set to be X.

One might think this reduces to a Travel Game over a 'supergraph' of ordinary graphs related by sabotage steps. But, given the complexity results we cited for sabotage modal logic, this translation necessarily blows up computational complexity.

In modal terms, p defines a semi-kernel of the underlying frame, if and only if the formula Ep ∧ U (p → ( (¬p ∧ p)) holds in the model, with E the global existential modality, and U the universal modality.

For some results on basic modal logics of poisoning, see also[START_REF] Mierzewski | The modal logic(s) of poison games[END_REF].

In the literature on abstract argumentation edges are interpreted in the opposite direction: aRb represents that argument a attacks argument b.

It may be instructive to compare Formulas[START_REF] Gabbay | When are two arguments the same? equivalence in abstract argumentation[END_REF] and[START_REF] Gierasimczuk | Learning and teaching as a game: a sabotage approach[END_REF]. From an argumentationtheoretic point of view, the second imposes a more stringent winning requirement on Traveler, forcing the Demon to get stuck, while the first allows Traveler to simply 'keep going'.

Work in these areas also shows that gamification is not unique. For instance, the µ-calculus formulas that we have used to describe games themselves have standard evaluation games, and the connection between games, describing formulas, and evaluation games for the latter is often an intriguing one.

Acknowledgments Davide Grossi was supported in part by NWO (VENI grant 639.021.816), and in part by EPSRC (grant EP/M015815/1). Guillaume Aucher was supported in part by AFR (grant TR-PDR BFR08-056). Johan van Benthem was supported in part by the Changjiang Scholars Program of the Chinese Ministry of Education. The authors wish to thank Valentin Goranko for insightful discussions on the topic of this paper, Sebastian Enqvist for improvements to one of our proofs, and the reviewers of this special issue for their various helpful comments.