The Expressive Power of Swap Logic Raul Fervari FaMAF, Universidad Nacional de Córdoba, Argentina fervari@famaf.unc.edu.ar Abstract. Modal logics are appropriate to describe properties of graphs. But usually these are static properties. We investigate dynamic modal operators that can change the model during evaluation. We define the logic SL by extending the basic modal language with the ✸ modality, which is a diamond operator that has the ability to invert pairs of re- lated elements in the domain while traversing an edge of the accessibility relation. We will investigate the expressive power of SL, define a suitable notion of bisimulation and compare SL with other dynamic logics. Keywords: Modal logic, dynamic logics, hybrid logic, bisimulation, expressivity. 1 Introduction There are many notions in language and science that have a modal character, e.g. the classical notion of necessity and possibility. Modal logics [5, 6] are logics designed to deal with these notions. In general, they are adequate to describe certain patterns of behaviour of the real world. For this reason, modal logics are not just useful in mathematics or computer science; they are used in philosophy, linguistics, artificial intelligence and game theory, to name a few. Intuitively, modal logics extend the classical logical systems with operators that represent the modal character of some situation. In particular, the basic modal logic (BML) is an extension of propositional logic, with a new operator. We now define formally the syntax and semantics of BML. Definition 1 (Syntax). Let PROP be an infinite, countable set of propositional sym- bols. The set FORM of BML formulas over PROP is defined as: FORM ::= p | ¬ϕ | ϕ ∧ ψ | ✸ϕ, where p ∈ PROP and ϕ, ψ ∈ FORM. We use ✷ϕ as a shorthand for ¬✸¬ϕ, while ⊥, ⊤ and ϕ ∨ ψ are defined as usual. Definition 2 (Semantics). A model M is a triple M = hW, R, V i, where W is a non-empty set; R ⊆ W × W is the accessibility relation; and V : PROP → P(W ) is a valuation. Let w be a state in M, the pair (M, w) is called a pointed model; we will usually drop parenthesis and write M, w. Given a pointed model M, w and a formula ϕ we say that M, w satisfies ϕ (M, w |= ϕ) when M, w |= p iff w ∈ V (p) M, w |= ¬ϕ iff M, w 6|= ϕ M, w |= ϕ ∧ ψ iff M, w |= ϕ and M, w |= ψ M, w |= ✸ϕ iff for some v ∈ W s.t. (w, v) ∈ R, M, v |= ϕ. R.K. Rendsvig and S. Katrenko (Eds.): ESSLLI 2012 Student Session Proceedings, CEUR Work- shop Proceedings vol.: see http://ceur-ws.org/, 2012, pp. 23–31. 24 Raul Fervari ϕ is satisfiable if for some pointed model M, w we have M, w |= ϕ. As shown in Definition 2, modal logics describe characteristics of relational struc- tures. But these are static characteristics of the structure, i.e. properties never change after the application of certain operations. If we want to describe dynamic aspects of a given situation, e.g. how the relations between a set of elements evolve through time or through the application of certain operations, the use of modal logics (or actually, any logic with classical semantics) becomes less clear. We can always resort to modeling the whole space of possible evolutions of the system as a graph, but this soon becomes unwieldy. It would be more elegant to use truly dynamic modal logics with operators that can mimic the changes that structure will undergo. This is not a new idea, and a clear example of this kind of logics is the sabotage logic SML introduced by van Benthem in [4]. Consider the following sabotage game. It is played on a graph with two players, Runner and Blocker. Runner can move on the graph from node to accessible node, starting from a designated point, and with the goal of reaching a given final point. He should move one edge at a time. Blocker, on the other hand, can delete one edge from the graph, every time it is his turn. Of course, Runner wins if he manages to move from the origin to the final point in the graph, while Blocker wins otherwise. van Benthem proposes transforming the sabotage game into a modal logic; this idea has been studied in several other works [8, 11]. In particular, they defined the operator of sabotage as: M, w |= ✸ϕ – iff there is a pair (v, u) of M such that M{(v,u)} , w |= ϕ, where ME = hW, R \ E, V i, with E ⊆ R. It is clear that the ✸ – operator changes the model in which a formula is evalua- ted. As van Benthem puts it, ✸ – is an “external” modality that takes evaluation to another model, obtained from the current one by deleting some transition. It has been proved that solving the sabotage game is PSpace-hard [4], while the model checking problem of the associated modal logic is PSpace-complete and the satisfiability problem is undecidable [8, 9]. It has been investigated in these articles that the logic fails to have two nice model theoretical properties: the finite model property (if a formula is satisfiable, then it is satisfiable in a finite model) and the tree model property (every satisfiable formula is satisfied in the root of a tree-like model). Another family of model changing logics is memory logics [1, 3, 10]. The semantics ❖ of these languages is specified on models that come equipped with a set of states ❖ called the memory. The simplest memory logic includes a modality r that stores the current point of evaluation into memory, and a modality k that verifies whether ❖ the current state of evaluation has been memorized. The memory can be seen as a special proposition symbol whose extension grows whenever the r modality is used. In contrast with sabotage logics, the basic memory logic expands the model with an ever increasing set of memorized elements. The general properties of memory logics are similar to those of sabotage logics: a PSpace-complete model checking problem, an undecidable satisfiability problem, and failure of both the finite model and the tree model properties. In this article, we will investigate a model changing operator that in the general case doesn’t shrink nor expand the model. Instead, it has the ability to swap the direction of a traversed arrow. The ✸ operator is a ✸ operator — to be true at a state w it requires the existence of an accessible state v where evaluation will continue— but it changes the accessibility relation during evaluation —the pair (w, v) is deleted, and the pair (v, w) is added to the accessibility relation. The Expressive Power of Swap Logic 25 A picture will help understand the dynamics of ✸. The formula ✸✸⊤ is true in a model with two related states: ✸✸⊤ ✸⊤ w v w v As we can see in the picture, evaluation starts at state w with the arrow pointing from w to v, but after evaluating the ✸ operator, it continues at state v with the arrow now pointing from v to w. In this article, we will study the expressive power of SL and will compare it with BML and some dynamic logics. 2 Swap Logic Now we introduce syntax and semantics for SL. We will define first some notation that will help us describe models with swapped accessibility relations. Definition 3. Let R and S be two binary relations over a set W . We define the relation RS = (R \ S −1 ) ∪ S. When S is a singleton {(v, w)} we write Rvw instead of R{(v,w)} . Intuitively RS stands for R with some edges swapped around (S contains the edges in their final position). The following property is easy to verify: Proposition 1. Let R, S, S ′ ⊆ W 2 be binary relations over an arbitrary set W , then ′ S′ (RS )S = RS . We extend BML with a new operator ✸. For (v, w) ∈ R−1 , let Mvw = hW, Rvw , V i. Similarly, for S ⊆ R−1 , MS = hW, RS , V i. Then we define the semantics of the new operator as follows: M, w |= ✸ϕ iff for some v ∈ W s.t. (w, v) ∈ R, Mvw , v |= ϕ. The semantic condition for ✸ looks quite innocent but, as we will see in the following example, it is actually very expressive. Example 1. Define ✷0 ϕ as ϕ, ✷n+1 ϕ as ✷✷n ϕ, and let ✷(n) ϕ be a shorthand for V i (3) 1≤i≤n ✷ ϕ. The formula ϕ = p ∧ ✷ ¬p ∧ ✸✸✸p is true at a state w in a model, only if w has a reflexive successor. Notice that no equivalent formula exists in the basic modal language (satisfiable formulas in the basic modal language can always be satisfied at the root of a tree model). Let us analyse the formula in detail. Suppose we evaluate ϕ at some state w of an arbitrary model. The ‘static’ part of the formula p ∧ ✷(3) ¬p makes sure that p is true in w and that no p state is reachable within a three steps neighbourhood of w (in particular, the evaluation point cannot be reflexive). Now, the ‘dynamic’ part of the formula ✸✸✸p will do the rest. Because ✸✸✸p is true at w, there should be an R-successor v where ✸✸p holds once the accessibility relation has been updated to Rvw . Now, v has to reach a p-state in exactly two Rvw -steps to satisfy ✸✸p. But the only p state sufficiently close for this to happen is w which is reachable in one step. As w is not reflexive, v has to be reflexive so that we can linger at v for one loop and reach p in the correct number of states. Example 1 shows that the tree model property fails for SL. It should be a warning about the expressivity of SL, which is certainly above that of the BML. 26 Raul Fervari 3 Bisimulation and Expressive Power In most modal logics, bisimulations are binary relations linking elements of the domains that have the same atomic information, and preserving the relational structure of the model [6]. This will not suffice for SL where we also need to capture the dynamic be- haviour of the ✸ operator. The proper notion of SL-bisimulations links states together with the context of potentially swapped edges. Definition 4 (Swap Bisimulations). Given models M = hW, R, V i and M′ = hW ′ , R′ , V ′ i, together with points w ∈ W and w′ ∈ W ′ we say that they are bisimilar and write M, w - M′ , w′ if there is a relation Z ⊆ (W × P(W 2 )) × (W ′ × P(W ′2 )) such that (w, R)Z(w′ , R′ ) satisfying the following conditions. Whenever (w, S)Z(w′ , S ′ ) then (Atomic Harmony) for all p ∈ PROP, M, w |= p iff M′ , w′ |= p; (Zig) If wSv, there is v ′ ∈W ′ s.t. w′ S ′ v ′ and (v, S)Z(v ′ , S ′ ); (Zag) If w′ S ′ v ′ , there is v∈W s.t. wSv and (v, S)Z(v ′ , S ′ ); ′ ′ (S-Zig) If wSv, there is v ′ ∈W ′ s.t. w′ S ′ v ′ and (v, S vw )Z(v ′ , S ′v w ); ′ ′ (S-Zag) If w′ S ′ v ′ , there is v∈W s.t. wSv and (v, S vw )Z(v ′ , S ′v w ). Theorem 1 (Invariance for Swap Logic.). Let M = hW, R, V i and M′ = hW ′ , R′ , V ′ i two models, w ∈ W , w′ ∈ W ′ , S ⊆ R−1 and S ′ ⊆ R′−1 . If M, w - M′ , w′ then for any ′ formula ϕ ∈ SL, MS , w |= ϕ iff M′S , w′ |= ϕ. Proof. The proof is by structural induction on SL formulas. The base case holds by Atomic Harmony, and the ∧ and ¬ cases are trivial. [✸ϕ case:] Let M = hW, R, V i and M′ = hW ′ , R′ , V ′ i. Suppose M, w |= ✸ϕ. Then there is v in W s.t. wRv and M, v |= ϕ. Since Z is a bisimulation, by (zig) we have v ′ ∈ W ′ s.t. w′ R′ v ′ and (v, R)Z(v ′ , R′ ). By inductive hypothesis, M′ , v ′ |= ϕ and by definition M′ , w′ |= ✸ϕ. For the other direction use (zag). [✸ϕ case:] For the left to the right direction suppose M, w |= ✸ϕ. Then there is v ∈ W s.t. wRv and Mvw , v |= ϕ. Because Z is a bisimulation, by (S-zig) we have v ′ ∈ W ′ ′ ′ ′ ′ s.t. w′ R′ v ′ and (v, Rvw )Z(v ′ , R′v w ). By inductive hypothesis, M′v w , v ′ |= ϕ and by definition M′ , w′ |= ✸ϕ. For the other direction use (S-zag). ⊓ ⊔ Example 2. The two models in row A of Table 1 are SL-bisimilar. The simplest way Example 3. There is no SL-bisimulation between the models in row B of Table 1. to check this is to recast the notion of SL-bisimulation as an Ehrenfeucht-Fraı̈ssé game Indeed the used as the one formula ✸✸✷⊥but for BML, is where satisfied Spoiler , w′also in M2can andswap not in M1 , w. arrows Notice when thatfrom moving the models are BML-bisimilar. a node to an adjacent node. It is clear that Duplicator has a winning strategy. We are now ready to investigate the expressive power of SL. Definition 5 (L ≤ L′ ). We say that L′ is at least as expressive as L (notation L ≤ L′ ) if there is a function Tr between formulas of L and L′ such that for every model M and every formula ϕ of L we have that M |=L ϕ iff M |=L′ Tr(ϕ). M is seen as a model of L on the left and as a model of L′ on the right, and we use in each case the appropriate semantic relation |=L or |=L′ as required. We say that L′ is strictly more expressive than L (notation L < L′ ) if L ≤ L′ but not L′ ≤ L. And we say that L and L′ are uncomparable (notation L 6= L′ ) if L  L′ and L′  L. The Expressive Power of Swap Logic 27 A w w′ v′ M1 M2 B w w′ v′ M1 M2 ′ w v w v′ C ν µ′ ν′ M1 M2 D w w′ v′ M1 M2 Table 1. Table of comparison between models. The definition above requires that both logics evaluate their formulas over the same class of models. However, we can abuse of this detail when operators of some logic do not interact with the part of the model that is different of the other one. For example, memory logics operate over models that contains an aditional set to store visited states (a memory), and in our results we will evaluate formulas with an initial empty memory. When we evaluate SL-formulas over memory logics models with an empty memory, we can as well forget about that memory and treat them as standard Kripke models. The same occurs with hybrid models (where there are nominals and ↓ operator in the language). Our first result is fairly straightforward as it builds upon Example 3: BML is strictly less expressive than SL. Theorem 2. BML < SL. Proof. We have to provide a translation from BML formulas to SL. This is trivial as BML is a fragment of SL. To prove SL  BML consider the models in row B of Table 1. They are bisimilar for BML but, as we already mentioned, the SL formula ✸✸✷⊥ distinguishes them. ⊓ ⊔ Now we will compare SL with the hybrid logic H(:, ↓), whose operator ↓ is a dynamic operator. Definition 6 (Hybrid Logic H(:, ↓)). Let the signature hPROP, NOMi be given, with NOM ⊆ PROP. We extend BML with two new operators n:ϕ and ↓n.ϕ, where p ∈ PROP, n ∈ NOM and ϕ, ψ ∈ FORM. A hybrid model M is a triple hW, R, V i as usual, but V : PROP → P(W ) is such that V (p) is a singleton if p ∈ NOM. Let w be a state in M, the semantics of the new operators is defined as: hW, R, V i, w |= n:ϕ iff hW, R, V i, v |= ϕ where V (n) = {v} hW, R, V i, w |= ↓n.ϕ iff hW, R, Vnw i, w |= ϕ, where Vnw is defined by Vnw (n) = {w} and Vnw (m) = V (m) when m 6= n. 28 Raul Fervari Formulas like ↓n.ϕ, can be intuitively read as “after naming the current state n, ϕ holds”. For instance, ↓n.♦n means “the current state is reflexive”, and ↓n.♦n means “all accessible states are reflexive” Theorem 3. SL < H(:, ↓). Proof. We will define an adequate translation from SL to H(:, ↓). As models of H(:, ↓) have a fixed frame, we will encode the configuration of the model (i.e., the current state of swapped links) at the syntactic level. To do so, we will take advantage of the binder ↓ and nominals to name the pair of points of the model where a swap should occur. Let F be a non-empty set of pairs of nominals. Intuitively, this set will play a similar role than the set S of Definition 3. However, it contains purely syntactic information in the form of pair of nominals, as opposed to a direct description of swapped edge of the model. Moreover, it stores swapped links in the order of their former state. That is, F (as in “forbidden”) represents the set of links that cannot be taken any more. We use F to keep track of the configuration of the model in which a subformula must be satisfied. In fact, we will make heavy use of nominals to exactly determine if there are links that we should not take, when translating modal logic connectors. The complexity of the translation lies in the operators ✸ and ✸. The translation of ✸ϕ subformulas considers two cases: – either the diamond is satisfied using a successor by a link that either has not been swapped, or is a swapped reflexive link. To know which accessible worlds in the hybrid model should not be accessible in the swap model, we first have to determine where we are. That is, for every forbidden pair (x, y) ∈ F , decide if x is true or not at the current point. Then for all true x, we enforce that either ¬y is true at the destination point, or x is true (for the reflexive case). Of course, the translation of ϕ has to be true at that destination point. – or the diamond is satisfied by taking a swapped edge (y, x). In this case the current point of evaluation should be y and we should continue evaluation at x. The cases for ✸ subformulas are similar, but we should record that the used link is now swapped: – either ✸ is satisfied by traversing a new edge, in which case we name it (x, y) and we add it to the set F . – or ✸ is satisfied by taking an already swapped edge (x, y) ∈ F , in which case the current point of evaluation is y, we should continue at x and remove (x, y) from F. Formally then, the equivalence-preserving translation from SL to H(:, ↓) is defined as follows: Definition 7. Let F ⊆ NOM × NOM. Define ( )′F from formulas of SL to formulas of H(:, ↓) as Let F ⊆ NOM × NOM. Define ( )′F from formulas of SL to formulas of H(:, ↓) as (p)′F = p (¬ϕ)′F = ¬(ϕ)′F (ψ ∧ ϕ)′F = ′ V F ∧ (ϕ)V (ψ) ′ F V (♦ϕ)′F = ( ′ xy∈F (¬)xy6∈c x) → ♦(( xy∈c ¬y ∨ x) ∧ (ϕ)F ) W c∈P(F ) ∨ xy∈F y ∧ x:(ϕ)′F V V V (✸ϕ)′F = ( xy∈F (¬)xy6∈c x) → ↓i♦(↓j( xy∈c ¬y ∨ x) ∧ (ϕ)′F ∪ij ) Wc∈P(F ) ∨ xy∈F y ∧ x:(ϕ)′F \xy The Expressive Power of Swap Logic 29 where i and j are nominals that do not appear in F . We introduced two SL-bisimilar models in Example 2. Finally the formula ↓x.♦¬x distinguishes them, being true in M2 , w′ and false in M1 , w. ⊓ ⊔ Summing up, SL is strictly in between BML and H(:, ↓). Let us now compare SL with a family of dynamic modal logics called memory logics. Memory logics [1, 10] are modal logics with the ability to store the current state of evaluation into a set, and to consult whether the current state of evaluation belongs to this set. This set is also called the memory. ❖❖ ❖ Definition 8 (Memory Logics). The set FORM of formulas of ML( r , k ) over ❖ ❖ PROP is defined as in Definition 1 but adding a new zero-ary operator k and a new unary operator r ϕ. The same holds for ML(hhrii, k ), but adding hhriiϕ and deleting the classical ✸. A model M = hW, R, V, Si is an extension of an SL model with a memory S ⊆ W . Let w be a state in M, we define satisfiability as: ❖ ❖ hW, R, V, Si, w |= k iff w ∈ S ❖ hW, R, V, Si, w |= r ϕ iff hW, R, V, S ∪ {w}i, w |= ϕ hW, R, V, Si, w |= hhriiϕ iff hW, R, V, Si, w |= r ♦ϕ. ❖❖ ❖ A formula ϕ of ML( r , k ) or ML(hhrii, k ) is satisfiable if there exists a model hW, R, V, ∅i such that hW, R, V, ∅i, w |= ϕ. ❖ ❖ In the definition of satisfiability, the empty initial memory ensures that no point of ❖ the model satisfies the unary predicate k unless a formula r ϕ or hhriiϕ has previously ❖❖ been evaluated there. The memory logic ML(hhrii, k ) does not have the ♦ operator, ❖❖ ❖ and its expressive power is strictly weaker than ML( r , k ) [3, 10]. We now show that the expressive power of SL is uncomparable with both ML( r , k ) and ML(hhrii, k ). Theorem 4. SL 6≥ ML(hhrii, k ).❖ ❖ Proof. As we mentioned, no SL formula distinguishes the models in row A of Table 1, but hhrii¬ k is satisfiable in M2 , w′ but not in M1 , w. ⊓ ⊔ ❖❖ Theorem 5. ML( r , k ) 6≥ SL. ❖❖ ❖ Proof. The models in row C of Table 1 are bisimilar in ML( r , k ). Indeed they are BML bisimilar and acyclic, hence k is always false after taking an accessibility relation. The formula ✸✸✸✸✸✷⊥ is satisfiable in M2 , w′ but not in M1 , w. ⊓ ⊔ ❖❖ ❖ Corollary 1. The expressive powers of ML( r , k ) and SL are uncomparable. The same holds for ML(hhrii, k ) and SL. ❖ ❖❖ Proof. From Theorems 4 and 5, given that ML(hhrii, k ) < ML( r , k ) [3].⊓ ⊔ ❖❖ We now compare the expressive powers of ML( r , k ) and SL with the sabotage modal logic SML. Theorem 6. SL 6≥ SML. – Proof. Consider again models in Example 2, that are SL-bisimilar. The formula ✸✸⊤ distinguishes them (it is satisfiable in M2 , w′ but not in M1 , w). ⊓ ⊔ 30 Raul Fervari ❖❖ Theorem 7. ML( r , k ) 6≥ SML. ❖❖ Proof. Models in row D of Table 1 are bisimilar in ML( r , k ), but the formula ✸✸⊤ – is satisfiable in M2 , w′ but not in M1 , w. ⊓ ⊔ ❖❖ ❖ The following picture sums up the results of this section (relationships between ML( r , k ), ML(hhrii, k ) and H(:, ↓) have been extracted from [3]). SML 6≥ 6≥ ❖ ML(hhrii, k ) < ❖❖ ML( r , k ) < < 6≥ 6≥ BML 6≥ H(:, ↓) 6≥ 6≥ < < SL It remains an open question the other directions of the comparison between SML and the other logics, because no notion of bisimulation for SML has been provided yet. 4 Conclusions In this paper we have extended the basic modal language with the ✸ operator, which is a diamond operator that has the ability to invert pairs of related elements in the domain while traversing an edge of the accessibility relation. Other dynamic languages that can modify the model have been investigated in the literature (e.g., sabotage logics [4, 8], memory logics [3, 10], hybrid logics [2, 7]), and we have discussed the relation between these languages and SL. In particular, we have introduced an adequate notion of bisimulation for SL and used it to show that the expressive power of SL lies ❖❖ strictly in between the expressive powers of BML and the hybrid logic H(:, ↓), while ❖ it is uncomparable with the expressive powers of the memory logics ML( r , k ) and ML(hhrii, k ). Many theoretical aspects of SL remain to be investigated. For example, it would be interesting to obtain an axiomatic characterization which is sound and complete. The task is probably non trivial, as the logic fails to be closed under uniform substitution. A proper axiomatization will require an adequate definition of when a formula is free to substitute another formula in an axiom. More generally, it is a challenge to study the properties of other dynamic operators beside ✸. For example, two operators which would be closer to those investigated by sabotage logics would be one that access an arbitrary element in the model (similar to a global modality) and makes it a successor of the current point of evaluation, complemented with one that access a successor of the current point of evaluation and deletes the edge between the two. Investigating further examples of this kind of operator will let us have a clearer picture of the gains and losses of working with logics which can dynamically modify the model. Acknowledgments: This work was partially supported by grants ANPCyT-PICT-2008-306, ANPCyT-PIC- 2010-688, the FP7-PEOPLE-2011-IRSES Project “Mobility between Europe and Ar- gentina applying Logics to Systems” (MEALS) and the Laboratoire Internationale Associé “INFINIS”. The Expressive Power of Swap Logic 31 References 1. Areces, C.: Hybrid logics: The old and the new. In: Arrazola, X., Larrazabal, J. (eds.) Proc. of LogKCA-07. pp. 15–29. San Sebastian, Spain (2007) 2. Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logics, pp. 821–868. Elsevier (2006) 3. Areces, C., Figueira, D., Figueira, S., Mera, S.: The expressive power of memory logics. The Review of Symbolic Logic 4(2), 290–318 (2011) 4. van Benthem, J.: An essay on sabotage and obstruction. In: Mechanizing Mathe- matical Reasoning. pp. 268–276 (2005) 5. Blackburn, P., van Benthem, J.: Modal logic: A semantic perspective. In: Handbook of Modal Logic. Elsevier North-Holland (2006) 6. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic, Cambridge Tracts in The- oretical Comp. Scie., vol. 53. Cambridge University Press (2001) 7. Blackburn, P., Seligman, J.: Hybrid languages. Journal of Logic, Language and Information 4, 251–272 (1995) 8. Löding, C., Rohde, P.: Model checking and satisfiability for sabotage modal logic. In: Pandya, P., Radhakrishnan, J. (eds.) FSTTCS. LNCS, vol. 2914, pp. 302–313. Springer (2003) 9. Löding, C., Rohde, P.: Solving the sabotage game is PSPACE-hard. In: Mathemat- ical Foundations of Computer Science 2003, Lecture Notes in Computer Science, vol. 2747, pp. 531–540. Springer, Berlin (2003) 10. Mera, S.: Modal Memory Logics. Ph.D. thesis, Univ. de Buenos Aires and UFR STMIA - Ecole Doctorale IAEM Lorraine Dép. de Form. Doct. en Informat. (2009) 11. Rohde, P.: On games and logics over dynamically changing structures. Ph.D. thesis, RWTH Aachen (2006)