@article {95,
	title = {Swap logic},
	journal = {Logic Journal of IGPL},
	volume = {22},
	year = {2014},
	pages = {309-332},
	abstract = {We investigate dynamic modal operators that can change
the model during evaluation. We dene the logic SL by extending the basic modal language with the <sw> modality, which is a diamond operator that in addition has the ability to invert pairs of related elements in the domain while traversing an edge of the accessibility relation.
SL is very expressive: it fails to have the finite and the tree model property. We show that SL is equivalent to a fragment of rst-order logic by providing a satisability preserving translation. In addition, we provide an equivalence preserving translation from SL to the hybrid logic H(:;\down).
We also dene a suitable notion of bisimulation for SL and investigate its expressive power, showing that it lies strictly between the basic modal logic and H(:;\down). We finally show that its model checking problem is PSpace-complete and its satisability problem is undecidable.},
	keywords = {complexity, dynamic logics, expressivity, Modal logic},
	doi = {10.1093/jigpal/jzt030},
	author = {Carlos Areces and Fervari, Raul and Hoffmann, G.}
}