Relation-changing modal operators

C. Areces, R. Fervari, and G. Hoffmann. Relation-changing modal operators. Logic Journal of the IGPL, 23(4):601–627, 2015.

Download

[pdf] 

Abstract

We study dynamic modal operators that can change the accessibility relation of a model during the evaluation of a formula. In particular, we extend the basic modal language with modalities that are able to delete, add or swap an edge between pairs of elements of the domain. We define a generic framework to characterize this kind of operations. First, we investigate relation-changing modal logics as fragments of classical logics. Then, we use the new framework to get a suitable notion of bisimulation for the logics introduced, and we investigate their expressive power. Finally, we show that the complexity of the model checking problem for the particular operators introduced is PSpace-complete, and we study two subproblems of model checking: formula complexity and program complexity.

BibTeX

@Article{Areces2015b,
  author =       "C. Areces and R. Fervari and G. Hoffmann",
  journal =      "Logic Journal of the {IGPL}",
  title =        "Relation-changing modal operators",
  year =         "2015",
  number =       "4",
  pages =        "601--627",
  volume =       "23",
  abstract =     "We study dynamic modal operators that can change the
                 accessibility relation of a model during the evaluation
                 of a formula. In particular, we extend the basic modal
                 language with modalities that are able to delete, add
                 or swap an edge between pairs of elements of the
                 domain. We define a generic framework to characterize
                 this kind of operations. First, we investigate
                 relation-changing modal logics as fragments of
                 classical logics. Then, we use the new framework to get
                 a suitable notion of bisimulation for the logics
                 introduced, and we investigate their expressive power.
                 Finally, we show that the complexity of the model
                 checking problem for the particular operators
                 introduced is PSpace-complete, and we study two
                 subproblems of model checking: formula complexity and
                 program complexity.",
  doi =          "10.1093/jigpal/jzv020",
  owner =        "areces",
  timestamp =    "Tue, 28 Jul 2015 12:19:23 +0200",
  URL =          "http://dx.doi.org/10.1093/jigpal/jzv020",
}