=Paper=
{{Paper
|id=None
|storemode=property
|title=The Expressive Power of Swap Logic
|pdfUrl=https://ceur-ws.org/Vol-954/paper3.pdf
|volume=Vol-954
}}
==The Expressive Power of Swap Logic==
https://ceur-ws.org/Vol-954/paper3.pdf
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)