Relation-Changing Logics as Fragments of Hybrid Logics

C. Areces, R. Fervari, G. Hoffmann, and M. Martel. Relation-Changing Logics as Fragments of Hybrid Logics. Electronic Proceedings in Theoretical Computer Science, 226:16–29, Open Publishing Association, Catania, Italy, 2016. Proceedings of the 7th International Symposium on Games, Automata, Logics and Formal Verification

Download

[pdf] 

Abstract

Relation-changing modal logics are extensions of the basic modal logic that allow changes to the accessibility relation of a model during the evaluation of a formula. In particular, they are equipped with dynamic modalities that are able to delete, add, and swap edges in the model, both locally and globally. We provide translations from these logics to hybrid logic along with an implementation. In general, these logics are undecidable, but we use our translations to identify decidable fragments. We also compare the expressive power of relation-changing modal logics with hybrid logics.

BibTeX

@Article{Areces2016a,
  author =       "C. Areces and R. Fervari and G. Hoffmann and M.
                 Martel",
  note =         "Proceedings of the 7th International Symposium on
                 Games, Automata, Logics and Formal Verification",
  title =        "Relation-Changing Logics as Fragments of Hybrid
                 Logics",
  year =         "2016",
  address =      "Catania, Italy",
  editor =       "D. Cantone and G. Delzanno",
  pages =        "16--29",
  publisher =    "Open Publishing Association",
  journal =      "Electronic Proceedings in Theoretical Computer
                 Science",
  volume =       "226",
  ISSN =         "2075-2180",
  abstract =     "Relation-changing modal logics are extensions of the
                 basic modal logic that allow changes to the
                 accessibility relation of a model during the evaluation
                 of a formula. In particular, they are equipped with
                 dynamic modalities that are able to delete, add, and
                 swap edges in the model, both locally and globally. We
                 provide translations from these logics to hybrid logic
                 along with an implementation. In general, these logics
                 are undecidable, but we use our translations to
                 identify decidable fragments. We also compare the
                 expressive power of relation-changing modal logics with
                 hybrid logics.",
  doi =          "10.4204/EPTCS.226.2",
  owner =        "areces",
  timestamp =    "2016.09.30",
}