Moving Arrows and Four Model Checking Results

TitleMoving Arrows and Four Model Checking Results
Publication TypeConference Paper
Year of Publication2012
AuthorsAreces, C, Fervari, R, Hoffmann, G
Conference NameProceedings of WoLLIC 2012
Date PublishedSeptember
Conference LocationBuenos Aires, Argentina
AbstractWe 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: