Moving Arrows and Four Model Checking Results
| Title | Moving Arrows and Four Model Checking Results |
| Publication Type | Conference Paper |
| Year of Publication | 2012 |
| Authors | Areces, C, Fervari, R, Hoffmann, G |
| Conference Name | Proceedings of WoLLIC 2012 |
| Date Published | September |
| Conference Location | Buenos Aires, Argentina |
| 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. |
Work Package:
WP2
