Relation-Changing Modal Operators

Abstract. We study dynamic modal operators that can change the ac-cessibility relation of a model during the evaluation of a formula. In par-ticular, we extend the basic modal language with modalities that are able to delete, add or swap an edge between pairs of elements of the domain. We define a generic framework to characterize this kind of operations. First, we investigate relation-changing modal logics as fragments of clas-sical logics. Then, we use the new framework to get a suitable notion of bisimulation for the logics introduced, and we investigate their expres-sive power. Finally, we show that the complexity of the model checking problem for the particular operators introduced is PSpace-complete, and we study two subproblems of model checking: formula complexity and program complexity