Swap Logic

C. Areces, R. Fervari, and G. Hoffmann. 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

@Article{Areces2014d,
  author =       "C. Areces and R. Fervari and G. Hoffmann",
  journal =      "Logic Journal of the {IGPL}",
  title =        "Swap Logic",
  year =         "2014",
  number =       "2",
  pages =        "309--332",
  volume =       "22",
  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",
}