Swap Logic

Areces, C., Fervari, R., and Hoffmann, G.. Swap Logic. Logic Journal of the IGPL, 22(2):309–332, 2014.

Download: [pdf] 

Abstract:

We investigate dynamic modal operators that can change the model during evaluation. We define the logic SL by extending the basic modal language with the $\swap$ 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 first-order logic by providing a satisfiability preserving translation. In addition, we provide an equivalence preserving translation from SL to the hybrid logic H(:, $\downarrow$). We also define a suitable notion of bisimulation for SL and investigate its expressive power, showing that it lies strictly between the basic modal logic and H(:, $\downarrow$). We finally show that its model checking problem is PSpace-complete and its satisfiability problem is undecidable.

BibTeX: (download)

@ARTICLE{arec:swap13,
  author = {Areces, C. and Fervari, R. and Hoffmann, G.},
  title = {Swap Logic},
  journal = {Logic Journal of the IGPL},
  year = {2014},
  volume = {22},
  pages = {309--332},
  number = {2},
  abstract = {We investigate dynamic modal operators that can change the model during
	evaluation. We define the logic SL by extending the basic modal language
	with the $\swap$ 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 first-order logic
	by providing a satisfiability preserving translation. In addition,
	we provide an equivalence preserving translation from SL to the hybrid
	logic H(:, $\downarrow$). We also define a suitable notion of bisimulation
	for SL and investigate its expressive power, showing that it lies
	strictly between the basic modal logic and H(:, $\downarrow$). We
	finally show that its model checking problem is PSpace-complete and
	its satisfiability problem is undecidable.},
  owner = {areces},
  timestamp = {2013.02.10}
}

Generated by bib2html.pl (written by Patrick Riley) on Sun Oct 02, 2016 17:05:49