Swap logic
| Title | Swap logic |
| Publication Type | Journal Article |
| Year of Publication | 2014 |
| Authors | Areces, C, Fervari, R, Hoffmann, G |
| Journal | Logic Journal of IGPL |
| Volume | 22 |
| Issue | 2 |
| Pagination | 309-332 |
| Keywords | complexity, dynamic logics, expressivity, Modal logic |
| Abstract | We 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. |
| DOI | 10.1093/jigpal/jzt030 |
PDF (Full text):
Work Package:
WP2
