Moving Arrows and Four Model Checking Results

Areces, C., Fervari, R., and Hoffmann, G.. Moving Arrows and Four Model Checking Results. In Ong, L. and de Queiroz, R., 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, September 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: (download)

@INCOLLECTION{arec:movi12,
  author = {Areces, C. and Fervari, R. and Hoffmann, G.},
  title = {Moving Arrows and Four Model Checking Results},
  booktitle = {Proceedings of the 19th International Workshop on Logic, Language,
	Information and Computation (WoLLIC 2012)},
  publisher = {Springer},
  year = {2012},
  editor = {Ong, L. and de Queiroz, R.},
  volume = {7456},
  series = {Lecture Notes in Computer Science},
  pages = {142-153},
  address = {Buenos Aires, Argentina},
  month = {September},
  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.},
  isbn = {978-3-642-32620-2}
}

Generated by bib2html.pl (written by Patrick Riley) on Sun Oct 02, 2016 17:05:49