Sabotage modal logic \(\textsf{SML}\) offers a format for analyzing games that modify graphs on which they are played. We study some model-theoretic and proof-theoretic aspects of this system. On the one hand, our first result is a characterization theorem w.r.t. a fragment of first-order logic which is invariant for a natural notion of ‘sabotage bisimulation’. On the other hand, we offer a sound and complete tableau method and its associated labeled sequent calculus for analyzing valid reasoning. In the last part of the paper, we explain key features of \(\textsf{SML}\) and other modal logics that analyze model changes using a general logical framework based on ‘atomic logics’. Thanks to this generalized perspective, we can state a generalized characterization theorem as well as generic results about the definability of classes of models for model-changing modal logics. Finally, we offer some further directions and open problems, including fixed-point logics for network games.