On games and logics over dynamically changing structures

In the classical framework of graph algorithms, program logics, and corresponding model checking games, one considers changes of system states and movements of agents within a system, but the underlying graph or structure is assumed to be static. This limitation motivates a more general approach where dynamic changes of structures are relevant.In this thesis, we take up a proposal of van Benthem from 2002 and consider games and modal logics over dynamically changing structures, where we focus on the deletion of edges of a graph, resp., transitions of a Kripke structure. We investigate two-player games where one player tries to reach a designated vertex of a graph while the opponent sabotages this by deleting edges. It is shown that adding the 'saboteur' makes these games algorithmically much harder to solve. Further, we analyze corresponding modal logics which are augmented with cross-model modalities referring to submodels from which a transition has been removed. On the one hand, it turns out that these 'sabotage modalities' already strengthen standard modal logic in such a way that many nice algorithmic and model-theoretic properties get lost. On the other hand, the model checking problem remains decidable.The main limitation of modal logic is the lack of a mechanism for unbounded iteration or recursion. To overcome this, we augment the 'sabotage modal logics' of the first part of the thesis with constructors for forming least and greatest monadic fixed-points. The resulting logic extends the well-known mu-calculus and is capable of expressing iterative properties like reachability or recurrence as well as basic changes of the underlying Kripke structure, namely, the deletion of transitions. Finally, we introduce extended parity games where in addition, both players are able to delete edges of the arena and to store, resp., restore the current appearance of the arena by use of a fixed number of registers. We show that these games serve as model checking games for the aforementioned 'sabotage mu-calculus'.

Grantor dc:publisher

Publikationsserver der RWTH Aachen University

Year dc:date

2005

Author dc:creator

• Rohde, Philipp

Contributors dc:contributor

• Thomas, Wolfgang

• info:eu-repo/classification/ddc/510
• Mathematik
• Erfüllbarkeitsproblem
• Dynamische Logik
• Modallogik
• Model checking
• My-Kalkül
• Sabotage-Spiel
• Paritätsspiel
• Dynamic Logic
• Modal Logic
• Mu-Calculus
• Parity Game

Statement dc:rights

• info:eu-repo/semantics/openAccess

Language dc:language

eng

Identifier

https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-122417%22

OAI identifier oai:identifier

oai:publications.rwth-aachen.de:60724