Satisfiability for relation-changing logics

C. Areces, R. Fervari, G. Hoffmann, and M. Martel. Satisfiability for relation-changing logics. Journal of Logic and Computation, 28(7):1443–1470, 2018.

Download

[pdf] 

Abstract

Relation-changing modal logics are extensions of the basic modal logic with dynamic operators that modify the accessibility relation of a model during the evaluation of a formula. These languages are equipped with dynamic modalities that are able, for example, to delete, add, and swap edges in the model, both locally and globally. We study the satisfiability problem for some of these logics. We first show that they can be translated into hybrid logic. As a result, we can transfer some results from hybrid logics to elation-changing modal logics. We discuss in particular, decidability for some fragments. We then show that satisfiability is, in general, undecidable for all the languages introduced, via translations from memory logics.

BibTeX

@Article{Areces2018a,
  author =       "C. Areces and R. Fervari and G. Hoffmann and M.
                 Martel",
  journal =      "Journal of Logic and Computation",
  title =        "Satisfiability for relation-changing logics",
  year =         "2018",
  number =       "7",
  pages =        "1443--1470",
  volume =       "28",
  abstract =     "Relation-changing modal logics are extensions of the
                 basic modal logic with dynamic operators that modify
                 the accessibility relation of a model during the
                 evaluation of a formula. These languages are equipped
                 with dynamic modalities that are able, for example, to
                 delete, add, and swap edges in the model, both locally
                 and globally. We study the satisfiability problem for
                 some of these logics. We first show that they can be
                 translated into hybrid logic. As a result, we can
                 transfer some results from hybrid logics to
                 elation-changing modal logics. We discuss in
                 particular, decidability for some fragments. We then
                 show that satisfiability is, in general, undecidable
                 for all the languages introduced, via translations from
                 memory logics.",
  bibsource =    "dblp computer science bibliography, https://dblp.org",
  biburl =       "https://dblp.org/rec/journals/logcom/ArecesFHM18.bib",
  doi =          "10.1093/logcom/exy022",
  timestamp =    "Mon, 12 Nov 2018 14:55:40 +0100",
  URL =          "https://doi.org/10.1093/logcom/exy022",
}