Swap logic

TitleSwap logic
Publication TypeJournal Article
Year of Publication2014
AuthorsAreces, C, Fervari, R, Hoffmann, G
JournalLogic Journal of IGPL
Volume22
Issue2
Pagination309-332
Keywordscomplexity, dynamic logics, expressivity, Modal logic
AbstractWe investigate dynamic modal operators that can change the model during evaluation. We dene 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 satisability preserving translation. In addition, we provide an equivalence preserving translation from SL to the hybrid logic H(:;\down). We also dene 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 satisability problem is undecidable.
DOI10.1093/jigpal/jzt030
PDF (Full text): 
Work Package: 
WP2