Model checking and satisfiability for sabotage modal logic

Abstract

We consider the sabotage modal logic SML which was suggested by van Benthem. SML is the modal logic equipped with a 'transition-deleting' modality and hence a modal logic over changing models. It was shown that the problem of uniform model checking for this logic is PSPACE-complete. In this paper we show that, on the other hand, the formula complexity and the program complexity are linear, resp., polynomial time. Further we show that SML lacks nice model-theoretic properties such as bisimulation invariance, the tree model property, and the finite model property. Finally we show that the satisfiability problem for SML is undecidable. Therefore SML seems to be more related to FO than to usual modal logic. © Springer-Verlag Berlin Heidelberg 2003.