Moving Arrows and Four Model Checking Results

C. Areces, R. Fervari, and G. Hoffmann. Moving Arrows and Four Model Checking Results. In L. Ong and R. de Queiroz, editors, Proceedings of the 19th International Workshop on Logic, Language, Information and Computation (WoLLIC 2012), Lecture Notes in Computer Science, pp. 142–153, Springer, Buenos Aires, Argentina, 2012.

Download

[pdf] 

Abstract

We study dynamic modal operators that can change themodel during the evaluation of a formula. In particular, we extend thebasic modal language with diamond modalities that are able to swap, delete or add pairs of related elements of the domain, while traversing an edge of the accessibility relation. We study these languages together with the sabotage modal logic, which can arbitrarily delete edges of the model. We define a suitable notion of bisimulation for the basic modal logic extended with each of the new dynamic operators and investigate their expressive power, showing that they are all uncomparable. We also show that the complexity of their model checking problems is PSpace- complete.

BibTeX

@InCollection{Areces2012,
  author =       "C. Areces and R. Fervari and G. Hoffmann",
  booktitle =    "Proceedings of the 19th International Workshop on
                 Logic, Language, Information and Computation (WoLLIC
                 2012)",
  publisher =    "Springer",
  title =        "Moving Arrows and Four Model Checking Results",
  year =         "2012",
  address =      "Buenos Aires, Argentina",
  editor =       "L. Ong and R. de Queiroz",
  ISBN =         "978-3-642-32620-2",
  pages =        "142--153",
  series =       "Lecture Notes in Computer Science",
  volume =       "7456",
  abstract =     "We study dynamic modal operators that can change
                 themodel during the evaluation of a formula. In
                 particular, we extend thebasic modal language with
                 diamond modalities that are able to swap, delete or add
                 pairs of related elements of the domain, while
                 traversing an edge of the accessibility relation. We
                 study these languages together with the sabotage modal
                 logic, which can arbitrarily delete edges of the model.
                 We define a suitable notion of bisimulation for the
                 basic modal logic extended with each of the new dynamic
                 operators and investigate their expressive power,
                 showing that they are all uncomparable. We also show
                 that the complexity of their model checking problems is
                 PSpace- complete.",
}