Carlos Areces

Diego Figueira

Santiago Figueira

Sergio Mera

The expressive power of Memory Logics

come   L'archive ouverte pluridisciplinaire

Modal Logics and Memory Logics

Nowadays, the term modal logics loosely refers to an extremely wide variety of languages, which are used in many different applications (see, e.g., (Blackburn et al., 2006)). Actually, the fact that the number of members in this family keeps constantly increasing is one of the defining characteristic of the field. While most modal logics have certain general aspects in common (e.g., they are usually interpreted in terms of relational structures and they are computationally well behaved), there usually are as many modal logics satisfying any of these "characterizing properties" as there are modal logics not honoring them. As a result, it is very hard indeed to come up with a proper definition of what a modal logic is. Perhaps one of the few general traits of the field is the desire to investigate languages specially tailored for specific tasks.

In this article we investigate the expressive power of a family of modal logics called memory logics, which extend both the semantics and the syntax of the classical modal logic. Many logical properties of memory logics have been investigated in recent articles. The original idea was introduced in [START_REF] Areces | Hybrid logics: The old and the new[END_REF]. [START_REF] Areces | Tableaux and model checking for memory logics[END_REF] investigate tableau algorithms and model checking for memory logics, while Areces, Figueira, & Mera (2009) discuss axiomatic completeness results. In this article we extend results originally presented in [START_REF] Areces | Expressive power and decidability for memory logics[END_REF] and provide full proofs.

We will introduce and motivate memory logics now. We need first some basic definitions. Let S be a first-order relational signature (i.e., a first order signature without function and constant symbols), and let M = D, I be a relational structure interpreting S (i.e., D is a non empty set and I is an interpretation function that assigns to all relational symbols in S a relation of the correct arity). It is well known that the basic modal language K can be interpreted on M (see [START_REF] Blackburn | Modal Logic[END_REF] for details). When interpreting modal formulas on relational structures, elements in the domain are sometimes called states, and the interpretations of relational symbols are called accessibility relations.

It is often said that modal languages provide an internal perspective of the structures over which they are evaluated. As [START_REF] Blackburn | Modal Logic[END_REF] put it, "a modal formula [can be seen as] a little automaton standing at some state in a relational structure, and only permitted to explore the structure by making journeys to neighboring states."

It is natural to think of a modal formula as exploring the structure, but what about changing it? Suppose we want to grant our little automaton the additional power to modify the structure during its exploratory trips. This question is not new, and it has resulted in different proposals of what are called dynamic logics.

Consider, for example, the task of assigning semantics to a programming language. Clearly, the different instructions of the language change the computational state. It is then natural to define their semantics by specifying which changes each atomic operation of the language introduces. This idea is at the core of formalisms like Hoare-Floyd logics [START_REF] Floyd | Assigning meanings to programs[END_REF][START_REF] Hoare | An axiomatic basis for computer programming[END_REF]) which include, for example, special operators to indicate the state of variables before and after a given instruction.

As a second example, consider the area of linguistics called dynamic semantics. One of its fundamental claims is that the standard truth-conditional view of sentence meaning -which is the result of using classical logic as representation languages-does not do sufficient justice to the fact that uttering a sentence changes the context it was uttered in. Deriving inspiration, in part, from work on the semantics of programming languages, dynamic semantic theories have developed several variations on the idea that the meaning of a sentence should be equated with the changes it makes to a context. Different dynamic logics like those introduced by Groenendijk & Stokhof in (1991a;1991b) try to capture these ideas. As yet a third example with an ample literature, we can mention dynamic epistemic logics [START_REF] Plaza | Logics of public communications[END_REF][START_REF] Gerbrandy | Bisimulations on Planet Kripke[END_REF][START_REF] Van Benthem | Logics for information update[END_REF][START_REF] Van Benthem | An essay on sabotage and obstruction[END_REF][START_REF] Van Benthem | Logics of communication and change[END_REF][START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF]. These logics model the evolution of the knowledge of epistemic agents via updates to the model representing their epistemic state. For example, some of these languages represent the act of an agent updating its epistemic state with the information that ϕ is true by eliminating all alternative epistemic states where ¬ϕ holds.

Our last family of examples come from the area of temporal logics for verification. In this area, it is many times necessary to model time-critical systems that depend on quantitative rather than qualitative properties. Many temporal logics introduced for this task use explicit global clocks which are accessed and controlled through logical operators.

Examples of such logics are XCTL [START_REF] Harel | Explicit clock temporal logic[END_REF], half-order logics [START_REF] Alur | A really temporal logic[END_REF][START_REF] Henzinger | Half-order modal logic: How to prove real-time properties[END_REF], and timed and metric temporal logics [START_REF] Alur | Model-checking in dense real-time[END_REF][START_REF] Alur | The benefits of relaxing punctuality[END_REF][START_REF] Koymans | Specifying real-time properties with metric temporal logic[END_REF][START_REF] Ouaknine | On the decidability of metric temporal logic[END_REF].

By contrast, other logics which are also called dynamic are not dynamic in the sense mentioned above, the main example being Propositional Dynamic Logic PDL, [START_REF] Harel | Dynamic logic[END_REF]. In PDL formulas are evaluated in a model but they cannot modify it (even though the language does include special operators to verify that certain property holds in a given state and continue evaluation accordingly, which provide extended expressivity [START_REF] Berman | Propositional dynamic logic is weaker without tests[END_REF]).

Memory logics can be seen as an attempt to investigate some of the common characteristics of all these logics, in the simplest possible set up. Going back to our little automaton, suppose we extend our definition of a model to a triple M = D, I, M , where M is an arbitrary subset of D. We can think of M as a memory where the automaton can store states that are considered particularly interesting. Defining the semantics of this operator is straightforward. Let us write D, I, M , w |= ϕ for w ∈ D and ϕ a formula to indicate that ϕ is true at w in the relational structure D, I extended with the memory M . Let us use r ('remember') to represent the memorize operator. We can then define

D, I, M , w |= r ϕ iff D, I, M ∪ {w} , w |= ϕ.
In other words, r is an instruction to modify the memory of the model, and ϕ is evaluated in the modified structure. The operation r by itself is totally useless. If we cannot access the information stored in M , r ϕ is equivalent to ϕ. Let us add then an operator k ('known') that checks whether the current state has been previously remembered:

D, I, M , w |= k iff w ∈ M.
This simple language gives us already new tautologies. For example, it is easy to see that the formula r k is always true. It is also not difficult to see (using well known results from modal logic) that the memory logic operator gives us additional expressivity. Let us remind the semantics of the standard (unary) modal operator diamond r of the basic modal language1 . Assuming that I(r) is a binary relation, we define:

D, I, M , w |= r ϕ iff for some w ∈ D s.t. (w, w ) ∈ I(r) D, I, M , w |= ϕ.
That is, the formula r ϕ is true in a state w if the formula ϕ is true in an r-successor. Now, the memory logic formula r r k is true in a state when evaluated on a model with an empty memory if and only if it is self reachable via the accessibility relation I(r). I.e., D, I, ∅ , w |= r r k iff (w, w) ∈ I(r).

As formulas of the basic modal language have the tree model property (i.e., a formula is satisfiable if and only if it is satisfiable in model which is a tree, and hence it does not contain reflexive loops [START_REF] Blackburn | Modal Logic[END_REF]), this property cannot be expressed in the basic modal language.

In the same spirit of the operators r and k introduced above, we can naturally define operators that modify any element of a model (adding or deleting states or modifying the interpretation function). In this paper we will restrict ourselves to operators that can access and modify only the memory M (even though we will briefly discuss possible alternative structures for M ). In Section 2 we will formally introduce the syntax and semantics of the memory logics we will investigate. In Section 3 we will define suitable notions of model equivalence for each language, which we will use in Section 4 to investigate their expressive power. In Section 5 we will show that most of the languages obtained, even in this simple set up, are undecidable. We show one case where decidability is regained by imposing a very strict 'memorization policy'. Section 6 finishes the paper with our conclusions and ideas for future work.

We close this section with some additional details on how memory logics were originally conceived, and how they relate to binding and hybrid logics.

Memory Logics and Hybrid Logics, or how Memory Logics were Born

Memory logics where initially defined for purely theoretical reasons (related to questions concerning binding and decidability), but it soon became clear that they could provide an interesting perspective on the question of how a formula can modify the model in which it is being evaluated, as we discussed above.

Memory logics were originally inspired by hybrid logics containing binders like HL(↓) (see [START_REF] Areces | Hybrid logics[END_REF]). But while ↓ was introduced to investigate dynamic naming of elements in a model, memory logics include operators to store and retrieve information from some kind of information structure or memory. In any case, once we take the appropriate point of view HL(↓) can be considered the first memory logic.

Let us start by formally introducing HL(↓). Assume a signature S = prop, nom, rel , where prop, nom and rel are countably infinite, pairwise disjoint sets of propositional, nominal and relational symbols respectively. For simplicity, and as it is usually done with modal languages, we will only introduce unary modal operators2 . The syntax of HL(↓) is defined as follows

ϕ ::= | p | i | ¬ϕ | ϕ ∧ ϕ | r ϕ | ↓i.ϕ,
where p ∈ prop, i ∈ nom and r ∈ rel. We can see that the language of HL(↓) is the language of the basic modal logic K (see [START_REF] Blackburn | Modal Logic[END_REF] for details) extended with nominals and ↓i.

Semantically, HL(↓) is also very close to K. HL(↓)-formulas are interpreted on relational structures extended with an assignment function to interpret nominals. Formally, a model for HL(↓) is a tuple D, I, g where g : nom → D is an assignment function. I assigns a subset of D to elements in prop, and a binary relation on D to elements of rel. Given D, I, g , the semantic conditions for HL(↓) are defined as: One way of looking at the semantic condition for ↓i.ϕ is that it dynamically creates a name for the current state (by linking the nominal i to it), so that we can later refer to it during the evaluation of ϕ. An alternative perspective is to see ↓i as an instruction to modify the model (by storing the current point of evaluation into i), and continue the evaluation of ϕ in the modified model. The difference between the two perspectives is subtle, but important for this article. In the latter, we are considering the assignment g as a kind of memory in our model, while ↓i and i are the tools we use to access the memory for reading and writing. The question then presents itself naturally: are there other kinds of interesting memory structures and memory operators?

D, I, g , w |= iff always D, I, g , w |= p iff w ∈ I(p) D, I, g , w |= i iff g(i) = w D, I, g , w |= ¬ϕ iff D, I, g , w |= ϕ D, I, g , w |= ϕ ∧ ψ iff D, I,
The assignment g is a very sophisticated memory structure: it has unbounded size, it provides direct access to all its memory cells, and each stored element can be unequivocally retrieved. The memory M we discussed above, together with the operators r and k , provides a much simpler memory structure. Intuitively, these operators cannot discern between different states stored in M , while an assignment g keeps a complete mapping between states and nominals. But notice that r is a binder, and effectively binds instances of k appearing in its scope. In other words, as we can see ↓i and nominals as memory operators which store and retrieve information from a memory structure, we could see r as a binder that binds occurrences of k in its scope. As the memory structure used by r and k has less discerning power, we would expect that the logic containing the new operators is less expressive than HL(↓).

Syntax and Semantics for Memory Logics

In this section we will introduce the syntax and semantics of the different memory logics that we will discuss in the article, and fix some terminology.

All the languages we will introduce are obtained by extending (in some cases, also slightly modifying) the syntax and semantics of the basic modal logic. Furthermore, with the exception of one case in which we discuss using a stack as a memory container, all the logics we analyze have the operators r and k . Therefore, for notational convention, we will use ML (for memory logics) as a prefix indicating a language that uses a set as a container, and that includes r and k . Then we will list the additional operators included in the language. Since the usual semantics of the diamond operator is going to be slightly modified in some cases, we will also include the diamond explicitly in this list. For example, ML( r ) is basic modal logic (i.e., with the usual diamond operator) extended with r and k .

Definition 1 (Syntax). Let prop = {p 1 , p 2 , . . . } (the propositional symbols) and rel = {r 1 , r 2 , . . . } (the relational symbols) be disjoint, countable infinite sets. The set forms of formulas in the signature prop, rel is defined as:

forms ::= | p | ¬ϕ | ϕ 1 ∧ ϕ 2 | r ϕ | r ϕ | k | r ϕ
where p ∈ prop, r ∈ rel and ϕ, ϕ 1 , ϕ 2 ∈ forms. The other standard operators are introduced via definitions. In particular [r]ϕ := ¬ r ¬ϕ and [[r]]ϕ := ¬ r ¬ϕ.

Throughout this article we are going to use the usual notion of modal depth of a formula, that is, the deepest nesting of modal operators. Modal formulas without modal operators have a modal depth of zero.

Definition 2 (Semantics). Given a signature S = prop, rel , a model is a tuple M = D, I, M where D is a nonempty set, I is an interpretation function such that I(p) ⊆ D for p ∈ prop and I(r) ⊆ D × D for r ∈ rel. M ⊆ D will be called the memory of the model. For notational convenience, let us assume fixed for the rest of the article the models

M = D, I, M , M 1 = D 1 , I 1 , M 1 and M 2 = D 2 , I 2 , M 2 .
Given a model M and a list of states [w 1 , . . . , w n ], w i ∈ D, we define M[w 1 , . . . , w n ] = D, I, M ∪ {w 1 , . . . , w n } . Now, let M be a model and w ∈ D, then the semantics for the different operators is defined as:

M, w |= iff always M, w |= p iff w ∈ I(p) M, w |= ¬ϕ iff M, w |= ϕ M, w |= ϕ ∧ ψ iff M, w |= ϕ and M, w |= ψ M, w |= r ϕ iff there is w such that (w, w ) ∈ I(r) and M, w |= ϕ M, w |= r ϕ iff there is w such that (w, w ) ∈ I(r) and M[w], w |= ϕ M, w |= r ϕ iff M[w], w |= ϕ M, w |= k iff w ∈ M .
Given a model M and w ∈ D, the set of propositions that are true at a given state w is defined as props(w) = {p ∈ prop | w ∈ I(p)}. Given two models M 1 and M 2 , and states w 1 ∈ D 1 and w 2 ∈ D 2 , we say that they agree when props(w 1 ) = props(w 2 ) and

w 1 ∈ M 1 iff w 2 ∈ M 2 .
Given a model M and w in the domain of M, we call M, w a pointed model.

A particularly interesting class of models to investigate is the class C ∅ = {M | M = D, I, ∅ }, i.e., the class of models where the memory is empty. Since we are working with logics that deal with the notion of state, it is natural to consider starting to evaluate a formula in a model of C ∅ . It is over C ∅ that the operators k and r have the most natural interpretation, and as we will see in the next sections, the restriction to this class has important effects on expressivity and decidability. It is worth noting that in this case a formula is initially evaluated in a model of C ∅ , but during the evaluation the model can change to one with nonempty memory. We will put an empty set as a subscript on the prefix ML every time we work with C ∅ as the class of initial models. For example ML( r ) restricted to this class of initial models is ML ∅ ( r ).

We will not consider all possible combinations of operators, since it is not our intention to be completely exhaustive. We are only going to analyze some combinations that we consider interesting, and in each section we will indicate the fragments we will be using. In many cases, the results shown for some fragments can be easily transferred to other fragments, not explicitly analyzed.

Model Equivalence

In this section we will investigate the notion of model equivalence for some of the memory logics that we introduced. Our goal is to define tools that will help us investigate their expressive power. In particular, we will define a notion of model equivalence in terms of Ehrenfeucht-Fraïssé games [START_REF] Ebbinghaus | Mathematical Logic[END_REF] and then introduce an alternative, but equivalent, notion in terms of bisimulations.

Definition 3 (Ehrenfeucht-Fraïssé Games). Let M 1 and M 2 be two models and let w 1 ∈ D 1 and w 2 ∈ D 2 .

An Ehrenfeucht-Fraïssé game EF (M 1 , M 2 , w 1 , w 2 ) is defined as follows. There are two players called Spoiler and Duplicator. Duplicator immediately looses the game

EF (M 1 , M 2 , w 1 , w 2 )
if w 1 and w 2 do not agree (i.e., either props(w 1 ) = props(w 2 ) or one of the states is in the memory and the other is not). Otherwise, the game starts, with the players moving alternatively. Spoiler always starts a turn of the game choosing in which model he will make a move. Let us set s = 1 and d = 2 in case he chooses M 1 ; otherwise, let s = 2 and d = 1.

For the logics ML( r ) and ML ∅ ( r ), the possible moves are as follows:

1. Memorize: Spoiler extends M s to M s ∪ {w s }. The next turn then starts with

EF (M 1 [w 1 ], M 2 [w 2 ], w 1 , w 2 )
(Duplicator does nothing in this case).

(M 1 , M 2 , v 1 , v 2 ).
The moves for the logics ML( r ) and ML ∅ ( r ) are similar, except that during a chose successor step Spoiler always remembers the current world, i.e., the game continues with EF

(M 1 [w 1 ], M 2 [w 2 ], v 1 , v 2 ) after Duplicator response.
In the case of an infinite game, Duplicator wins. Note that with this definition, exactly one of Spoiler or Duplicator wins each game.

Given two pointed models M 1 , w 1 and M 2 , w 2 we write M 1 , w 1 ≡ EF M 2 , w 2 when Duplicator has a winning strategy for EF (M 1 , M 2 , w 1 , w 2 ) (the exact type of game involved will usually be clear from the context, and we will write ≡ EF L when we need to specify that the game corresponds to the language of the logic L).

Even thought in the rest of the article we will use the game notion of model equivalence, a structural notion can be given that is closer to the usual notion of bisimulation for modal logics. Both definitions are equivalent, but depending on the context, one can be more natural than the other (e.g., in [START_REF] Mera | Modal Memory Logics[END_REF] the structural notion is used to prove results related to Craig interpolation).

Definition 4 (Bisimulations). Let M 1 and M 2 be two models. Let ∼ be a binary relation between ℘(D 1 ) × D 1 and ℘(D 2 ) × D 2 .

For ML( r ) and ML ∅ ( r ) a bisimulation satisfies the following properties:

(nontriv ) ∼ is not empty.

(agree) If M, m ∼ N, n , then m and n agree.

(forth) If M, m ∼ N, n and (m, m ) ∈ I 1 (r), then there exists n ∈ D 2 such that (n, n ) ∈ I 2 (r) and M, m ∼ N, n . (back ) If M, m ∼ N, n and (n, n ) ∈ I 2 (r), then there exists m ∈ D 1 such that (m, m ) ∈ I 1 (r) and M, m ∼ N, n . (remember ) If M, m ∼ N, n , then M ∪ {m}, m ∼ N ∪ {n}, n .
For the logics ML( r ) and ML ∅ ( r ) the (back) and (forth) conditions are replaced by:

(mforth) If M, m ∼ N, n and (m, m ) ∈ I 1 (r), then there exists n ∈ D 2 such that (n, n ) ∈ I 2 (r) and M ∪ {m}, m ∼ N ∪ {n}, n . (mback ) If M, m ∼ N, n and (n, n ) ∈ I 2 (r), then there exists m ∈ D 1 such that (m, m ) ∈ I 1 (r) and M ∪ {m}, m ∼ N ∪ {n}, n .
Given two pointed models M 1 , w 1 and M 2 , w 2 we write M 1 , w 1 ↔ M 2 , w 2 if there is a bisimulation linking M 1 , w 1 and M 2 , w 2 . Again, the exact type of bisimulation involved will usually be clear from the context, and we will write ↔ L when we need to specify that the bisimulation corresponds to the logic L.

As we said before, the notions of Ehrenfeucht-Fraïssé games and bisimulations coincide, as indicated in the following theorem.

Theorem 5. Let L ∈ {ML( r ), ML ∅ ( r ), ML( r ), ML ∅ ( r )}. Given two pointed models M 1 , w 1 and M 2 , w 2 then M 1 , w 1 ≡ EF L M 2 , w 2 if and only if M 1 , w 1 ↔ L M 2 , w 2 .
Proof. We will discuss the case only for ML( r ) as the proof is similar for languages containing r .

For the right to left direction. Assume that M 1 , w 1 ↔ M 2 , w 2 and that ∼ is a bisimulation linking M 1 , w 1 and M 2 , w 2 . We will prove that there is a strategy for Duplicator in the game EF (M 1 , M 2 , w 1 , w 2 ). First note that the game EF (M 1 , M 2 , w 1 , w 2 ) is well defined, since by (agree), w 1 and w 2 are agreeing states. We show that there is a strategy for Duplicator by proving that (1) for any pair of tuples S, w and Q, v such that S, w ∼ Q, v , and for any move Spoiler makes in the game

EF (M 1 [S], M 2 [Q], w, v),
there is always an appropriate answer for Duplicator such that the next step of the game is EF (M 1 [S ], M 2 [Q ], w , v ) and S , w ∼ Q , v . Given the initial assumptions, the fact that Duplicator has a winning strategy on the game EF (M 1 , M 2 , w 1 , w 2 ) easily follows from (1). So let us suppose that S, w ∼ Q, v and consider the game w, v). Without loss of generality, we assume that Spoiler chooses M 1 to make his move. There are two kinds of moves Spoiler can do:

EF (M 1 [S], M 2 [Q],
• Spoiler make a memorize step, and the game continues with v). By the (remember) condition, we know that S ∪ {w}, w ∼ Q ∪ {v}, v .

EF (M 1 [S∪{w}], M 2 [Q∪ {v}], w,
• Spoiler chooses an r-successor w of w. By the (forth) condition (we use (back) here if Duplicator chooses M 2 for his move), there is an r-successor v of v such that S, w ∼ Q, v . Using (agree), we know that w and v agree, so v is a good choice for Duplicator. The game continues with

EF (M 1 [S], M 2 [Q], w , v ) and S, w ∼ Q, v .
For the other direction, suppose that Duplicator has a winning strategy S on the game EF (M 1 , M 2 , w 1 , w 2 ). We define ∼ in the following way:

S, w ∼ Q, v if and only if EF (M 1 [S], M 2 [Q], w, v) is a reachable state of EF (M 1 , M 2 , w 1 , w 2 )
when Duplicator follows strategy S. We have to prove that the relation ∼ is a bisimulation. Suppose that S, w ∼ Q, v .

• The condition (agree) is easy to check.

• To see that the (forth) condition holds, suppose that (m, m ) ∈ I 1 (r). One possible move for Spoiler in the game

EF (M 1 [S], M 2 [Q], w, v) is to choose m from M 1 , and
because Duplicator uses the winning strategy S, he can answer with a state v ∈ M 2 , a successor of v, such that w and v agree. Therefore, the next step of the game is

EF (M 1 [S], M 2 [Q], w , v
), and by definition, S, w ∼ Q, v . The (back) condition is equivalent.

• Finally, to verify the (remember) condition, note that in the game

EF (M 1 [S], M 2 [Q],
w, v) Spoiler can choose to make a memorize step, and therefore the next step of the game is

E(M 1 [S ∪ {w}], M 2 [Q ∪ {v}], w, v). By definition, that means that S ∪ {w}, w ∼ Q ∪ {v}, v .
Therefore, ∼ is actually a bisimulation. Because the state

EF (M 1 , M 2 , w 1 , w 2 ) is (triv- ially) reachable, M 1 , w 1 ∼ M 2 , w 2 as desired.
As one could expect, both notions of model equivalence preserve the truth value of formulas. Given two pointed models M 1 , w 1 and M 2 , w 2 , we write M 1 , w 1 ≡ L M 2 , w 2 if for any formula ϕ in the language of the logic L we have that

M 1 , w 1 |= ϕ if and only if M 2 , w 2 |= ϕ. Proving then that M 1 , w 1 ≡ EF L M 2 , w 2 (equivalently M 1 , w 1 ↔ L M 2 , w 2 ) implies M 1 , w 1 ≡ L M 2 ,
w 2 only requires a simple induction. Establishing that the notions ≡ EF L , ↔ L and ≡ L coincide on image finite models (i.e., models where each state has only a finite number of successors considering the union of the accessibility relations) is only slightly harder. Theorem 6. Let L ∈ {ML( r ), ML ∅ ( r ), ML( r ), ML ∅ ( r )}. Let M 1 , w 1 and M 2 , w 2 be two pointed models. Then

M 1 , w 1 ≡ EF L M 2 , w 2 (equivalently, M 1 , w 1 ↔ L M 2 , w 2 ) implies M 1 , w 1 ≡ L M 2 , w 2 . If M 1 and M 2 are image finite, then M 1 , w 1 ≡ L M 2 , w 2 implies both M 1 , w 1 ≡ EF L M 2 , w 2 and M 1 , w 1 ↔ L M 2 , w 2 .

Expressive Power

In this section we compare the expressive power of memory logics with respect to both modal and hybrid logics. To do this, we will have to find a natural mapping between models of each logic. Such a mapping is easy to define in the case of the ML ∅ logics, where we only consider models with an empty memory: each modal model D, I can be identified with the memory model D, I, ∅ . Similarly, for sentences of HL(↓) (i.e., formulas where each nominal i appears in the scope of ↓i) the memory model D, I, ∅ can be identified with the hybrid model D, I, g for g an arbitrary assignment. In other cases, the definition will involve a change in the signature. But for the moment, assume that we consider two logics L and L such that both can be evaluated over the same class of models (modulo representation issues).

Definition 7 (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(ϕ),
(here it should be understood that the model M is seen as a model of L on the left and as a model of L on the right, and that 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 equally expressive (notation

L = L ) if L ≤ L and L ≤ L.
To improve the presentation of this section, sometimes we are going to present theorems that are later subsumed by stronger results (e.g. Theorem 10 is subsumed by Theorem 13, and later by Corollary 21). The reasons for doing this are in some cases just for the sake of clarity. In others it is because we believe that the proofs of some results are interesting by themselves.

Logics with an initially empty memory

We will compare the logics ML ∅ with the basic modal logic K and the hybrid logic HL(↓). We are going to establish that K < ML ∅ ( r ) < ML ∅ ( r ) < HL(↓).

First we are going to show that the freedom to decide when to remember a state gives ML ∅ ( r ) more expressive power when compared to ML ∅ ( r ).

Theorem 8. ML ∅ ( r ) < ML ∅ ( r ).
Proof. [ML ∅ ( r ) ≤ ML ∅ ( r )]: It is easy to see that there is a translation Tr from ML ∅ ( r ) to ML ∅ ( r )-formulas which maps r ϕ to r r ϕ and verifies M |= ϕ if and only if M |= Tr(ϕ).

[ML ∅ ( r ) ≤ ML ∅ ( r )]: Let M 1 = {w, v, x}, I 1 , ∅ and M 2 = {w, v, x}, I 2 , ∅ such that I 1 (r) = {(w, v), (v, x), (x, w)}, I 2 (r) = {(w, v), (v, x), (x, v)}, and I 1 (p) = I 2 (p) = ∅ for p ∈ prop as shown below: w v x M 1 w v x M 2
We claim M 1 , w ≡ EF ML( r ) M 2 , w . As every state in both models has a unique successor, Duplicator has only one way of playing, which is actually a winning strategy. Hence M 1 , w ≡ ML( r ) M 2 , w . But M 1 , w |= r r r r k , while M 2 , w |= r r r r k .

We will now compare the expressive power of memory logics with the basic modal logic K. It is not difficult to see intuitively that r and k do bring additional expressive power into the language of K: with their help we can detect cycles in a given model, while formulas of K are invariant under unraveling.

Theorem 9. K < ML ∅ ( r ).

Proof. As K is a sub-language of ML ∅ ( r ), K ≤ ML ∅ ( r ) taking Tr to be the identity function. To see that ML ∅ ( r ) ≤ K, let M 1 = {w}, I 1 , ∅ with I 1 (r) = {(w, w)}, M 2 = {u, v}, I 2 , ∅ with I 2 = {(u, v), (v, u)}, and I 1 (p) = I 2 (p) = ∅ for p ∈ props be two models as shown below:

w M 1 u v M 2
The models are K bisimilar [START_REF] Blackburn | Modal Logic[END_REF]. However, they can be distinguished by the ML( r )-formula r k .

We will now compare the expressive power of memory logics with respect to hybrid logics. The most natural choice for the comparison is the hybrid logic HL(↓). We will prove that HL(↓) is strictly more expressive than ML ∅ ( r ). Intuitively, ↓ can easily simulate r , but k does not distinguish between different memorized states (while nominals bound by ↓ do).

Theorem 10. ML ∅ ( r ) < HL(↓).

Proof. We first prove that ML ∅ ( r ) ≤ HL(↓). We define the translation Tr, taking ML ∅ ( r )-formulas over the signature prop, rel to HL(↓) sentences over the signature prop, rel, nom . Tr is defined for any finite set N ⊆ nom as follows:

Tr N (p) = p p ∈ prop Tr N ( k ) = i∈N i Tr N (¬ϕ) = ¬Tr N (ϕ) Tr N (ϕ 1 ∧ ϕ 2 ) = Tr N (ϕ 1 ) ∧ Tr N (ϕ 2 ) Tr N ( r ϕ) = r Tr N (ϕ) Tr N ( r ϕ) = ↓i.Tr N ∪{i} (ϕ) where i / ∈ N .
Induction then shows that M, w |= ϕ iff M, g, w |= Tr ∅ (ϕ), for any g. Now we prove that HL(↓) is strictly more expressive than ML ∅ ( r ). Let

M 1 = {w 0 , w 1 , w 2 , . . . }, I 1 , ∅ M 2 = {w 0 , w 1 , w 2 , . . . }, I 2 , ∅ I 1 (r) = {(n, m) | n = m} ∪ {(w 0 , w 0 )} I 2 (r) = I 1 (r) ∪ {(w 1 , w 1 )} I 1 (p) = I 2 (p) = ∅ for p ∈ prop.
Graphically,

w 0 w 1 w 2 w 3 w 4 • • • w 0 w 2 w 3 w 4 w 5 • • • w 1 M 1 M 2
We prove that M 1 , w 0 ≡ EF ML ∅ ( r ) M 2 , w 0 showing a winning strategy for Duplicator. Intuitively, the strategy is as follows: whenever one player is in M 1 , w 0 the other will be in M 2 , w 0 or M 2 , w 1 , and conversely whenever a player is in M 1 , w n , n > 0, the other will be in M 2 , w m , m > 1. This is maintained until Spoiler (if ever) decides to remember a state. Once this is done, then any move leads to a win of Duplicator. Formally, the winning strategy will have two stages: On the other hand, let ϕ be the formula ↓i.

r (i ∧ r (¬i ∧ ↓i. r i)). It is easy to see that M 1 , w 0 |= ϕ but M 2 , w 0 |= ϕ.
We have shown that ML ∅ ( r ) < HL(↓) but the proof seems to intrinsically use infinite models, in contrast with the proofs for Theorems 8, 9 and 10 in which finite models are used. Actually, ML ∅ ( r ) < HL(↓) even on finite models. For this purpose we will first introduce a version of the Ehrenfeucht-Fraïssé game presented in Definition 3 where the number of turns is bounded.

Definition 11. The n-moves Ehrenfeucht-Fraïssé game for a given logic L, denoted

EF n L (M 1 , M 2 , w 1 , w 2 ),
is the game in which Spoiler can only make n moves in the game to beat Duplicator. If Duplicator has a strategy to remain undefeated for n moves, he wins the game and we write

M 1 , w 1 ≡ EF n L M 2 , w 2 .
We will state without a proof the following easy theorem.

Theorem 12. Let L ∈ {ML( r ), ML ∅ ( r ), ML( r ), ML ∅ ( r )}. For any pair of pointed models, M 1 , w 1 ≡ EF n L M 2 , w 2 if and only if for every formula ϕ of L with modal depth n, M 1 , w 1 |= ϕ iff M 2 , w 2 |= ϕ. Now we can prove the desired result for finite models:

Theorem 13. ML ∅ ( r ) < HL(↓) over the class of finite models.

Proof. We will prove that there is a property ϕ expressible in HL(↓) that cannot be expressed in ML ∅ ( r ) over finite models. To do this, for every n we will exhibit two finite models

M n 1 , M n 2 such that M n 1 , w 0 |= ϕ, M n 2 , w 0 |= ϕ but M n 1 , w 0 ≡ EF n ML ∅ ( r )
M n 2 , w 0 . This implies that there is no ML ∅ ( r )-formula ψ capable of expressing this property.

Let ϕ = ↓i. r (i ∧ r (¬i ∧ ↓i. r i)) as in the proof of Theorem 10, and let, for n ≥ 1,

M n 1 = D n , I n 1 , ∅ and M n 2 = D n , I n 2 , ∅ where D n = {w 0 , . . . , w n+1 }, I n 1 (r) = {(a, b) | a, b ∈ D n , a = b} ∪ {(w 0 , w 0 )}, I n 2 (r) = I n 1 (r) ∪ {(w 1 , w 1 )}, and I n 1 (p) = I n 2 (p) = ∅ for p ∈ prop As an example, M 2
1 and M 2 2 would be

w 0 w 1 w 2 w 3 M 1 2 w 0 w 1 w 2 w 3 M 2 2
Clearly, for every n ≥ 1, M n 1 , w 0 |= ϕ and M n 2 , w 0 |= ϕ. To prove that M n 1 , w 0 ≡ EF n ML ∅ ( r ) M n 2 , w 0 , we will describe Duplicator's winning strategy: 1. While Spoiler does not remember any reflexive state, Duplicator plays with the following strategy: whenever Spoiler is in

w k , 2 ≤ k ≤ n + 1 in one model, Duplicator is in an agreeing state w k , 2 ≤ k ≤ n + 1 in the other one. If one player is in w 0 in M n 1 then the other is in w 0 or w 1 in M n 2 . Finally, if Spoiler plays w 1 in M n 1 , Duplicator plays in an agreeing w k , 2 ≤ k ≤ n + 1 in M n 2 .
With this strategy, Spoiler chooses a reflexive state if and only if Duplicator answers with a reflexive one, and Duplicator is always able to choose an agreeing state.

2. If ever Spoiler decides to remember a reflexive state, then for every state w i chosen by Spoiler, Duplicator will always have an agreeing state w j in the other model. This happens because the models have n + 2 states, and therefore there is always at least two non-remembered states. At each round the number of unremembered states can only be decremented by one, and then up to round n both players will always see remembered and unremembered states from w i and well as from w j .

Because Duplicator wins the game for any n, any candidate ψ ∈ ML ∅ ( r ) expressing ϕ will fail for a sufficiently large n.

The HL(↓)-sentence we use in the proofs of Theorem 10 and 13 has only one nominal. Hence, we have actually proved that HL 1 (↓) ≤ ML ∅ ( r ), where HL 1 (↓) is HL(↓) restricted to only one nominal. But actually, it is also the case that ML ∅ ( r ) ≤ HL 1 (↓). More generally, for any fixed number k of nominals, the logics HL k (↓) and ML ∅ ( r ) are incomparable.

Theorem 14. For any fixed k, the logics HL k (↓) and ML ∅ ( r ) are incomparable in terms of expressive power.

Proof. We will show the proof for k = 1, the general case being similar. HL 1 (↓) ≤ ML ∅ ( r ) is a direct consequence of the proof of Theorem 10.

To prove

ML ∅ ( r ) ≤ HL 1 (↓), let M 1 = {w 1 , w 2 , w 3 }, I 1 , ∅ with I 1 (r) = {(w i , w j ) | 1 ≤ i, j ≤ 3} and I 1 (p) = ∅ for p ∈ prop, and M 2 = {w 1 , w 2 }, I 2 , ∅ with I 2 (r) = {(w i , w j ) | 1 ≤ i, j ≤ 2} I 2 (p) = ∅ for p ∈ prop. That is, M 1 is a clique of size 3 while M 2 is a clique of size 2. It is easy to check that M 1 , w 1 ≡ HL 1 (↓) M 2 ,
w 1 because they are HL 1 (↓)-bisimilar as defined in [START_REF] Areces | Hybrid logics[END_REF]. However, the formula

ϕ = r r (¬ k ∧ r r ¬ k ) distinguishes the models: M 1 , w 1 |= ϕ but M 2 , w 1 |= ϕ.
The proof for HL k (↓) is similar, taking cliques of the appropriate size.

Erase and forget

As it is natural to define operators that store states in the memory, we can also introduce operators that delete states from it. In this section we will investigate their behavior. We extend the memory logics we have been discussing with two new operators that remove states from the memory. We define both a global operator e that completely wipes out the memory, and a local version f , which deletes the current evaluation state. We extend the syntax of the memory languages to include e and f :

forms ::= | p | ¬ϕ | ϕ 1 ∧ ϕ 2 | r ϕ | r ϕ | k | r ϕ | e ϕ | f ϕ,
were ϕ ∈ forms (see Definition 1 for details). We also extend the semantics (Definition 2) with the following two conditions:

D, I, M , w |= e ϕ iff D, I, ∅ , w |= ϕ D, I, M , w |= f ϕ iff D, I, M \ {w} , w |= ϕ.
As we intuitively discussed above, the e operator replaces the current memory with the empty set, while f only removes the current state.

In this section we are only going to consider e and f for classes of models where the original memory is empty, and with the usual interpretation for the diamond operator. Hence, following our naming convention, we will refer to these logics adding the new operators to the prefix ML. For example, ML ∅ ( r , e , f ) is the memory logic augmented with both e and f operators.

Clearly, the notions of Ehrenfeucht-Fraïssé game and bisimulation need to be extended to include these new operators, given that we want model equivalence to preserve the truth value of formulas.

Definition 15. The definition of Ehrenfeucht-Fraïssé game for logics with e and f extends Definition 3 adding two new possible moves. Remember that the current move is EF (M 1 , M 2 , w 1 , w 2 ), that the turn starts by Spoiler choosing one of the two models, and that we set s = 1 and d = 2 in case Spoiler chooses M 1 , and that s = 2 and d = 1 otherwise.

1. Erase: Spoiler wipes out the memory, setting M s = M d = ∅. The next turn starts with EF ( D 1 , I 1 , ∅ , D 2 , I 2 , ∅ , w 1 , w 2 ).

Forget:

Spoiler deletes w s from M s setting M s = M s \ {w s }. The next turn starts with EF ( D 1 , I 1 , M 1 \ {w 1 } , D 2 , I 2 , M 2 \ {w 2 } , w 1 , w 2 ).
In a similar way we can extend the notion of bisimulation we introduced before.

Definition 16. The notion of bisimulation extend the one described in Definition 4 with the rules:

(erase) If M, m ∼ N, n , then ∅, m ∼ ∅, n . (forget) If M, m ∼ N, n , then M \ {m}, m ∼ N \ {n}, n .
Once more, the definitions are modular, each new type of move in the Ehrenfeucht-Fraïssé, and each new rule for the bisimulation definition corresponds, respectively to the e and f operators. If one of these operators is added to the language, the corresponding rule or type of move needs to be added to the corresponding definition of bisimulation or game in order to preserve the extended language.

Now we can establish the first result regarding these new operators: independently adding e and f does increase the expressive power.

Theorem 17. ML ∅ ( r ) < ML ∅ ( r , f ) and ML ∅ ( r ) < ML ∅ ( r , e ).
Proof. It is trivial to see that both ML ∅ ( r ) ≤ ML ∅ ( r , f ) and ML ∅ ( r ) ≤ ML ∅ ( r , e ) hold using the identity translation. To verify ML ∅ ( r ) = ML ∅ ( r , f ) and ML ∅ ( r ) = ML ∅ ( r , e ), let M 1 and M 2 be the models described in the proof of Theorem 10 Recall that M 1 , 0 is ML ∅ ( r )-bisimilar to M 2 , 0 .

To see that ML ∅ ( r ) = ML ∅ ( r , f ), we show that these two pointed models are distinguishable with a ML ∅ ( r , f )-formula. Let

ψ = [r] f ( r ( k ∧ r k )).
Intuitively, ψ states that no matter which accessible state we choose, we can move to it, eliminate it from the memory, and move to an already remembered state which is connected to some (possibly different) remembered state. Now let

ϕ = r r (¬ k ∧ r ψ).
It is clear that M 2 , 0 |= ϕ, since one can remember the state 0, then move to state 1 (which is not remembered), and remember it leaving the model in the state M 2 [0, 1] and the evaluation state in 1. Then it is easy to see that M 2 [0, 1], 1 |= ψ. However, one can verify that M 1 , 0 |= ϕ. Indeed, suppose that, after remembering the state 0, we move to state n > 0 and we remember it. By the definition of M 1 , the state n will not be reflexive. Now,

M 1 [0, n], n |= ψ because M 1 [0, n], 0 |= f ( r ( k ∧ r k )), i.e., M 1 [n], 0 |= r ( k ∧ r k ). Showing that ML ∅ ( r ) = ML ∅ ( r , e ) is easier. Let ϕ = r r (¬ k ∧ e r r k ). It is not difficult to see that M 2 , 0 |= ϕ but M 1 , 0 |= ϕ.
On the other hand, we are still below the expressive power of HL(↓):

Theorem 18. ML ∅ ( r , e , f ) ≤ HL(↓).

Proof. In line with the proof of Theorem 10, we define a truth-preserving translation from formulas of ML ∅ ( r , e , f ) into formulas of HL(↓). To define our translation we use a finite sequence S of nominals in nom, where each nominal i in the sequence is tagged with a superscript r (representing a remember) or with a superscript f (representing a forget). We use the operation S • i to denote the operation of inserting the element i at the end of the sequence S. λ stands for the empty sequence.

Tr S (p) = p p ∈ prop Tr S (¬ϕ) = ¬Tr S (ϕ) Tr S (ϕ 1 ∧ ϕ 2 ) = Tr S (ϕ 1 ) ∧ Tr S (ϕ 2 ) Tr S ( r ϕ) = r Tr S (ϕ) Tr S ( r ϕ) = ↓i.Tr S•{i r } (ϕ) where i / ∈ S. Tr S ( f ϕ) = ↓i.Tr S•{i f } (ϕ) where i / ∈ S. Tr S ( e ϕ) = Tr λ (ϕ) Tr S ( k ) = T (S),
where T is a translation from sequences of nominals to ML ∅ ( r , e , f )-formulas defined in the following way:

T (λ) = ⊥ T (S • i r ) = i ∨ T (S) T (S • i f ) = ¬i ∧ T (S).
A simple induction shows that M, w |= ϕ iff M, g, w |= Tr λ (ϕ), for any g.

Corollary 19. ML ∅ ( r , e ) ≤ HL(↓) and ML ∅ ( r , f ) ≤ HL(↓). Now we show that ML ∅ ( r , e ) is not more expressive than ML ∅ ( r , f ) using a game argument as we did for ML ∅ ( r ).

Theorem 20. ML ∅ ( r , f ) ≤ ML ∅ ( r , e ).

Proof. Let M = {s} ∪ ω 0 ∪ ω 1 ∪ . . . , I, ∅ , where each ω i is a different copy of ω, and (s,n) | for all n = s}, and I(p) = ∅ for p ∈ prop. Intuitively, the model is as follows

I(r) = {(n, m) | n ∈ ω i , m ∈ ω j , i ≤ j} ∪ {(n, s),
ω 0 ω 1 ω 2 ω 3 . . . s M
Each ω i is a total relation on the natural numbers and, in addition, all elements of w i are related to all elements of w j if i < j.

We prove that M, w 0 ≡ EF M, w 1 for ML ∅ ( r , e ), where w 0 ∈ ω 0 and w 1 ∈ ω 1 . Given a state w, we define the neighborhood of w as N (w) = {v | (w, v) ∈ I(r)}, and we say that the neighborhood of a state w is remembered when N (w) ∩ M = ∅, where M is the current memory. The strategy we are going to define observes the following invariant:

1. Every time Spoiler has moved to a state w, then Duplicator has answered with an agreeing state v such that N (w) was not remembered if and only if N (v) was not remembered.

2. Every time Spoiler has moved to a state w ∈ ω i , Duplicator has answered with a state v ∈ ω j . And every time Spoilers has moved to s, Duplicator has moved to s.

It is clear that this invariant holds at the beginning of the game. We will prove that each step of the strategy preserves the invariant. Remember that at any stage of the game, the number of remembered states is always finite. Assume that Spoiler is in a state w ∈ ω s and Duplicator in v ∈ ω d . The strategy for Duplicator is the following:

1. If Spoiler decides to remember w, then the game continues with both w and v remembered. So both N (w) and N (v) become remembered, and the invariant is preserved.

2. If Spoiler decides to forget all the states in the model, then both N (w) and N (v) become not remembered, and the game continues with the invariant preserved. If N (w) is not remembered, given the shape of the model, the only possibility is that w = s. Therefore v = s, and we have already seen that the neighborhoods match in this case. The remaining case is when N (w) is remembered. Given the invariant, we know that N (v) is remembered, so if Spoiler chooses w ∈ M , we know that there is a v ∈ M that Spoiler can move to. In this case it is trivial to see that N (v ) is not remembered. On the other hand, if Spoiler chooses w ∈ M , then a safe choice for Duplicator is a non remembered v ∈ ω d , that is, a state in the same cluster as v. Since each ω i is infinite, there is always such a v , and also this choice guarantees that N (v ) is not remembered.

If

On the other hand, let ϕ = r r r

(¬ k ∧ r k ∧ r r ( k ∧ f [r]¬ k )) be a formula of ML ∅ ( r , f ). It is easy to see that M, w 1 |= ϕ but M, w 0 |= ϕ.
Corollary 21. ML ∅ ( r , e ) < HL(↓) and ML ∅ ( r , e ) < ML ∅ ( r , e , f )

Proof. Trivial given Theorems 20 and 18

To end this subsection we want to observe that there are still some interesting questions that remain open. For example, the relation between HL(↓) and ML ∅ ( r , e , f ):

Question 1. HL(↓) = ML ∅ ( r , e , f )?
We conjecture that the answer is positive, but we have not found yet a pair of models (similarly to the proofs of Theorems 20 and 10) in which the difference can be shown. The other natural question is the relation between ML ∅ ( r , e ) and ML ∅ ( r , f ):

Question 2. ML ∅ ( r , e ) ≤ ML ∅ ( r , f )?
Again we conjecture that the answer is positive, and the proof should follow the style of the proof of Theorem 20

Memory Logics with a Stack

In this subsection we want to analyze other memory containers different than a set. A priori, any kind of data structure could be a suitable alternative, but it should be clear that certain choices immediately gives back the full expressive power of HL(↓). For example, suppose we use an unbounded array to store elements of the domain, and that we combine it with suitable operators that can store and retrieve elements to and from a given index. The results is nothing other than a different formulation of assignments and the combination of the ↓ operator and nominals.

In what follows we will discuss a more subtle case. Suppose that we use a stack instead. I.e., our memory structure will still be unbounded, but we are only allowed to store element at the top, and inspect and remove only the top element. We will show that, even though the access to the memory structure is restricted, we still have the full expressive power of HL(↓). But let us start by formally introducing this language. Its syntax is defined as follows:

forms

::= | p | ¬ϕ | ϕ 1 ∧ ϕ 2 | r ϕ | (push)ϕ | (pop)ϕ | (top)
where p ∈ prop, r ∈ rel and ϕ, ϕ 1 , ϕ 2 ∈ forms. The semantic rules for the new operators are as follows. Assume that S is a stack represented as a list. The symbol λ represent the empty stack, and if S is a stack and w an element S • w represent the stack obtained by adding w as top-most element.

D, I, S , w |= (push)ϕ iff D, I, S • w , w |= ϕ D, I, S • v , w |= (pop)ϕ iff D, I, S , w |= ϕ D, I, λ , w |= (pop)ϕ iff never D, I, S • v , w |= (top) iff v = w D, I, λ , w |= (top) iff never
Let us call ML st ∅ ( r ) the logic obtained by adding these operators to the basic modal logic, and when we restrict ourselves to the class where stacks are initially empty. We will show that ML st ∅ ( r ) and HL(↓) are equally expressive. Because we are restricting ourselves to the class of models where the stack is initially empty, models in ML st ∅ ( r ) can be seen as models of HL(↓) by ignoring the stack.

Theorem 22. ML st ∅ ( r ) = HL(↓).
Proof. To prove ML st ∅ ( r ) ≤ HL(↓), we define a translation mapping a formula in ML st ∅ ( r ) and a list of nominals N into a formula of HL(↓).

Tr N (p) = p p ∈ prop Tr N (¬ϕ) = ¬Tr N (ϕ) Tr N ( r ϕ) = r Tr N (ϕ) Tr N (ϕ 1 ∧ ϕ 2 ) = Tr N (ϕ 1 ) ∧ Tr N (ϕ 2 ) Tr N ((push)ϕ) = ↓i.Tr N •i (ϕ) where i / ∈ N Tr N •i ((pop)ϕ) = Tr N (ϕ) Tr λ ((pop)ϕ) = ⊥ Tr N •i ((top)) = i Tr λ ((top)) = ⊥
We can show by induction in ϕ that M, w |= ϕ iff M, g, w |= Tr λ (ϕ), for any g.

To prove HL(↓) ≤ ML st ∅ ( r ) we define a translation mapping an HL(↓)-formula and a list of nominals N into an ML st ∅ ( r )-formula. The translation coincides with the translation above for the propositional, negation, conjunction and modality cases. We translate ↓ and nominals as follows:

Tr N (↓i.ϕ) = (push)Tr N •i (ϕ) Tr N (i) = (pop) |N |-n (top) i ∈ nom, N [n] = i, ∀m > n : N [m] = i,
where |N | represents the length of N and N [n] represents the n-th element of N . It can be shown by induction in ϕ that if ϕ is an HL(↓)-sentence, M, g, w |= ϕ iff M, w |= Tr λ (ϕ) for any g.

Non empty memory classes

Comparing the expressive power between the logics that start evaluating formulas in C ∅ and the ones that use an arbitrary memory poses a complication because, strictly speaking, each of them uses a different class of models. In this case it is not as obvious how to define the mapping between each type of models. The most natural option seems to involve a shift in the signature of the language, in order to preserve the information stored in the models.

Consider, for example, an arbitrary model M = D, I, M for ML( r ). If we want to consider it as a model of ML ∅ ( r ) we need to 'make room' for the non empty memory M somehow. We will do that by considering M = D, I, M as a model over a signature with one additional propositional symbol which we will call known and that will be interpreted as M .

Theorem 23.

1. ML ∅ ( r ) over the signature prop ∪ {known}, rel is equivalent to ML( r ) over the signature prop, rel .

2. ML ∅ ( r ) over the signature prop∪{known}, rel is equivalent to ML( r ) over the signature prop, rel .

Proof. The argument for 2 is exactly the same as the one for 1. Hence, let us prove ML ∅ ( r ) = ML( r ) (over the appropriate signatures). We start by associating every model M = D, I, M of ML( r ) over the signature prop, rel with the model M = D, I , ∅ of ML ∅ ( r ) over the signature prop ∪ {known}, rel where I is identical to I over prop and rel and I (known) = M . [ML ∅ ( r ) ≤ ML( r )]: use the translation Tr that replaces occurrences of the propositional symbol known by k in any formula of ML ∅ ( r ). Clearly for any formula ϕ ∈ ML ∅ ( r ) we have that M , w |= ϕ iff M, w |= Tr(ϕ).

[ML( r ) ≤ ML ∅ ( r )]: use the translation Tr that replaces occurrences of k by ( k ∨ known) in any formula of ML( r ). Clearly for any formula ϕ ∈ ML( r ) we have that M, w |= ϕ iff M , w |= Tr(ϕ).

Intuitively, the only thing we need to do is to store I(known) in the starting memory and vice versa. In the presence of f and e the memory does not grow monotonically and hence we cannot simulate it using known ∨ k . Now, the same expressivity hierarchy we proved for logics with empty memory can be established for logics with arbitrary memory, that is K < ML( r ) < ML( r ) < HL(↓):

Theorem 24.

1. ML( r ) over the signature prop, rel is strictly more expressive than K over the signature prop ∪ {known}, rel .

2. ML( r ) < ML( r ).

3. HL(↓) over the signature prop ∪ {known}, rel, nom is strictly more expressive than ML( r ) over the signature prop, rel .

Proof. The proof for 1 is the same as the proof for Theorem 9 The proof for 2 is the same as the proof for Theorem 8 To prove 3 we adapt the translation Tr defined in the proof of Theorem 10 with the following clause for k :

Tr N ( k ) = i∈N i ∨ known.
HL(↓) ≤ ML( r ) can then be shown using the following models. Let M 1 = {w}, I 1 , {w} with I 1 (r) = {(w, w)} and I 1 (p) = ∅ for p ∈ prop; and M 2 = {u, v}, I 2 , {u, v} with I 2 (r) = {(u, v), (v, u)} I 2 (p) = ∅ for p ∈ prop.

Duplicator always wins on EF (M 1 , M 2 , w, u) and thus M 1 , w ≡ EF ML( r ) M 2 , u. On the other hand, M 1 , w |= ↓i. r i but M 2 , u |= ↓i. r i.

(Un)Decidability and the Finite Model Property

In the previous section we showed memory logics more expressive than K but less expressive than HL(↓) (the only exception is ML st ∅ ( r ), which has the same expressive power than HL(↓)). Given that K is decidable and HL(↓) undecidable [START_REF] Areces | Hybrid logics[END_REF], exploring where the decidability line lies is an intriguing question. The main goal of this section is to investigate this issue, together with the related question of whether the logic is sufficiently expressive to force infinite models.

We start by investigating ML( r ) and ML ∅ ( r ). We will show that even though they are equivalent in terms of expressive power when we allow a shift in the signature, the satisfiability problem for ML( r ) is decidable (actually pspace-complete) while ML ∅ ( r ) is already undecidable. As we will show in the proof of Theorem 27 the trick is to use a 'dirty' memory. In ML ∅ ( r ), we are restricted to the class of models where the memory is always initialized to ∅ and we can't play this trick anymore. Actually ML( r ) is really standing on the decidability line: adding a single nominal to ML( r ) pushes the satisfiability problem over to undecidability.

Theorem 26 (Tree model property). Let M, w be a ML( r )-model. Then there is a tree M such that M, w ≡ EF M , w .

Proof. We prove the result for the unimodal case, the generalization to the multimodal case is straightforward. Let M = D, I, M , define M = D , I , M as follows. Its domain D consists of all finite sequences ū = (u 0 , . . . , u n ) such that u 0 = w, n ≥ 0 and (u i , u i+1 ) ∈ I(r) for 0 ≤ i < n. Let ū = (u 0 , . . . , u n ) and v = (v 0 , . . . , v m ), then define I (r) as follows, (ū, v) ∈ I (r) if and only if m = n + 1, u i = v 1 for i = 0, . . . , n and (u n , v m ) ∈ I(r). I (p) is defined by setting (u 0 , . . . , u n ) ∈ I (p) iff u n ∈ I(p). Finally, (u 0 , . . . ,

u n-1 , u n ) ∈ M iff u n ∈ {u 0 , . . . , u n-1 } or u n ∈ M .
Let s i be the sequence (v 0 , . . . , v i ). We show that Duplicator has a winning strategy in the game EF (M, M , w, w). It is sufficient to see that in the game

EF (M[v 0 , . . . , v n ], M [s 0 , . . . , s n ], v n+1 , s n+1 ),
Duplicator can always answer successfully to Spoiler's moves.

• If Spoiler chooses M[v 0 , . . . , v n ] and some v n+1 , a successor of v n , Duplicator chooses the sequence s n+1 = s n v n+1 .

• If Spoiler chooses M [s 0 , . . . , s n ] and s n+1 = s n v n+1 (for some v n+1 ), a successor of s n , Duplicator chooses the state v n+1 .

By definition s n+1 and v n+1 agree. Observe that the memory of M[v 0 , . . . , v n ] is M ∪ {v 0 , . . . , v n } and the memory of M [s 0 , . . . , s n ] is M ∪ {s 0 , . . . , s n }. It is also clear that v n+1 ∈ M if and only if s n+1 ∈ M . Formally, v n+1 ∈ M ∪ {v 0 , . . . , v n } implies s n+1 ∈ M by definition. And s n+1 ∈ S ∪ {s 0 , . . . , s n }, then s n+1 ∈ S (since there are no cycles in M ) and by definition v n+1 ∈ M ∪ {v 0 , . . . , v n }.

Theorem 27. The satisfiability problem of ML( r ) is pspace-complete.

Proof. We first show decidability of the satisfiability problem of ML( r ) proving that any satisfiable formula of ML( r ) is satisfiable in a recursively bounded model. Let ϕ be a ML( r )-formula of modal depth k, and suppose M 1 , w |= ϕ. By Theorem 26, there is a tree M 2 such that M 2 , w |= ϕ. Using Theorem 25, we know that M 2 , w |= Tr(ϕ) (here, M 2 is taken as a K model over the appropriate signature). Now we can use the bounded tree model property for basic modal logic [START_REF] Blackburn | Modal Logic[END_REF], so there must be a recursively bounded tree M 3 = D 3 , I 3 and v ∈ D 3 such that M 3 , v |= Tr(ϕ). Finally, we can use Theorem 25 again, and conclude D 3 , I 3 , I 3 (known) , v |= ϕ, where I 3 is the restriction of I 3 to the signature that does not contain known.

The pspace-completeness follows from the fact that the translation Tr is linear, and that the satisfiability problem for the basic modal logic is pspace [START_REF] Blackburn | Modal Logic[END_REF]. Now we show that adding f to ML( r ) keeps the logic decidable. In fact, ML( r , f ) can be encoded into ML( r ) using a linear translation. In other words, ML( r , f ) ≤ ML( r ) and hence f does not add expressivity when added to ML( r ). At the end of this section we are going to see that this is not the case for e .

Theorem 28. The satisfiability problem for ML( r , f ) is pspace-complete.

Proof. We show that there is a linear translation from ML( r , f ) to ML( r ). Let Tr a be the following translation from ML( r , f ) formulas to ML( r ) formulas, where a ranges over {r, f }:

Tr a (p) = p p ∈ prop Tr r ( k ) = k Tr f ( k ) = ¬ Tr a (¬ϕ) = ¬Tr a (ϕ) Tr a (ϕ 1 ∧ ϕ 2 ) = Tr a (ϕ 1 ) ∧ Tr a (ϕ 2 ) Tr a ( r ϕ) = r Tr r (ϕ) Tr a ( r ϕ) = r Tr r (ϕ) Tr a ( f ϕ) = Tr f (ϕ).
Given a model M = D, I, M and a state w ∈ D, we define M[-w] = D, I, M \ {w} . We prove by mutual induction on ϕ these two properties:

(

1) M, w |= ϕ iff M, w |= Tr r (ϕ). (2) M[-w], w |= ϕ iff M, w |= Tr f (ϕ).
Notice that (1) in fact shows that ML( r , f ) ≤ ML( r ). The only interesting cases for both properties are r , r and f . For the property ( 1 Property (1) shows that we have defined a satisfiability preserving translation. Observe that the linearity of the translation is trivial, and given Theorem 27 we conclude the desired result.

We now turn to ML ∅ ( r ). The ideas are similar to the case of ML( r ) + i but this time we cannot use the nominal i to make the spy point. On the other hand, we know that the memory is empty when we start evaluating a formula.

Theorem 31. ML ∅ ( r ) lacks the finite model property.

Proof. Consider the following formulas:

(Back) p ∧ [[r]]¬p ∧ r ∧ [[r]] r ( k ∧ p) (Spy) [[r]][[r]](¬p → r ( k ∧ p ∧ r ( k ∧ ¬ r ( k ∧ ¬p)))) (Irr) ¬ r (¬p ∧ r (¬p ∧ k ))) (Succ) [[r]] r ¬p (No-3cyc) ¬ r r (¬ k ∧ r (¬ k ∧ r ( k ∧ ¬p))) (Tran) [[r]](¬p → r ( k ∧ p ∧ [[r]](¬p ∧ ¬ k → r ( k ∧ p∧ r ( k ∧ ¬p ∧ r ( k ∧ ¬p)))))).
Let Inf be Back ∧ Spy ∧ Irr ∧ Succ ∧ No-3cyc ∧ Tran, and let M = D, I, ∅ . The proof that M is infinite if M, w |= Inf is similar to the proof of Theorem 29 Instead of using i to identify the spy point we now use p and k . k is needed to distinguish the spy point from other points where p might hold.

Notice that Back, Spy, Succ, and No-3cyc are very similar to the ones in the proof of Theorem 29, Irr forces I(r) to be irreflexive and Tran says that every pair of successors u and v are related (either (u, v) ∈ I(r) or (v, u) ∈ I(r)), and this together with the other formulas, implies that I(r) is transitive.

In a similar way, we can encode the ω × ω tiling problem to show that satisfiability in ML ∅ ( r ) is undecidable.

Theorem 32. The satisfiability problem for ML ∅ ( r ) is undecidable.

Proof. The formula ϕ T needed for the encoding of a tiling problem T in this case is the conjunction of the following:

(Back) p ∧ [[s]]¬p ∧ s ∧ [[s]] s ( k ∧ p) ∧ [[s]][[s]]( k ∧ p) (Spy) [[s]][[ †]](¬p ∧ s ( k ∧ p ∧ s ( k ∧ ¬ † k ))) † ∈ {r, u} (Grid) [[s]] † † ∈ {r, u} (Func) [[s]][[ †]] s s ( k ∧ † k ∧ [[ †]] k ) † ∈ {r, u} (Conf) [[s]] u r s s ( k ∧ ¬ r k ∧ u k ∧ r u ( k ∧ ¬ r k )) (UR-no-Cycle) [[s]][[u]][[r]]¬ k ∧ [[s]][[r]][[u]]¬ k (URU-no-Cycle) [[s]][[u]][[r]][[u]]¬ k (Unique) [[s]] 1≤i≤n t i ∧ 1≤i<j≤n (t i → ¬t j ) (Vert) [[s]] 1≤i≤n t i → u 1≤j≤n,u(T i )=d(T j ) t j (Horiz) [[s]] 1≤i≤n t i → r 1≤j≤n,r(T i )=l(T j ) t j .
From the undecidability of ML ∅ ( r ), we can easily conclude the undecidability of ML( r ) and ML ∅ ( r ).

Theorem 33. ML ∅ ( r ) lacks the finite model property and it is undecidable.

Proof. Straightforward from Theorems 8, 31 and 32

To prove failure of the finite model property for the case ML( r ) we first notice that the following lemma is easy to establish (we only state it for the mono-modal case; a similar result is true in the multimodal case). Failure of the finite model property is then a direct consequence. Proof. Using the idea of Lemma 34 and the formula ϕ T in the proof of Theorem 32, we can obtain a formula ψ such that if M, w |= ψ then M is a tiling of ω × ω. For the converse, we can build exactly the same model as in the proof of Theorem 32 and check that it satisfies ψ. Now we want to briefly mention the case of erase with respect to decidability. Given that e can be seen as an operator that internalizes the notion of starting the evaluation of a formula with an empty memory, it is quite easy to establish the following result:

Theorem 37. The satisfiability problem for ML( r , e ) is undecidable. Furthermore, the logic lacks the finite model property.

Proof. Theorems 31 and 32 show that the logic ML ∅ ( r ) lacks the finite model property and that its satisfiability problem is undecidable. It is straightforward to see that just adding e in front of each encoding is enough to achieve the same results for ML( r , e ).

Conclusions and Further Work

In this article we investigated several memory logics. These logics were inspired by the hybrid logic HL(↓) considering the ↓ operator as a storage command and the assignment function as a storage structure. The aim of this article is to explore this idea, investigating different ways in which information can be stored and retrieved, and the logics that result. There are different dimensions in which the idea can be carried further, which we inspect in this article. We can, for example, vary the type of storage structure. An assignment function is a very sophisticated memory structure: it has unbounded size, it provides direct access to all its memory cells, and each stored element can be unequivocally retrieved. We discussed in detail the result of using a set (instead of a function) as the information container, and show that this change results in logics with strictly lower expressive power. We also show that if we replace the set with a richer structure that allows the unique identification of the elements stored (like is the case in a stack) we regain the full expressive power of HL(↓).

The second dimension we analyzed was the collection of memory operators included in the language. We show that operators to add, test membership and delete elements from the memory can be naturally defined, and we mapped out the expressive power of the resulting logics.

Finally, the third dimension we investigated was the effect of imposing conditions on the state of the initial memory of the model in which we evaluate a formula. Requiring the initial memory to be empty (a natural requirement when working with models with state) boost the expressive power of the logic.

In terms of expressive power, the memory logics we presented lie between the basic modal logic K and the hybrid logic HL(↓). Figure 1 summarizes the results established in this article. The solid unlabeled arrows represent the < relationship, i.e., L → L means that the logic L is strictly less expressive than the logic L . In some cases we specifically indicate other relations (like ≤ or ≤), and the dashed arrows show the suspected answers to the open questions 1 and 2 we formulated.

We also discussed in detail complexity results. In most cases the satisfiability problem of the languages we introduced is undecidable. We were able to pin down only two logics, ML( r ) and ML( r , f ), which still have the bounded tree model property, and established that their satisfiability problem is pspace-complete. In other words, to regain decidability we had to allow models with a potentially non empty memory and imposed (through the operator r ) a very restricted policy to memorize states. To obtain these results we defined in Section 5 different equivalence preserving translations which can be used to transfer known results, for example, from HL(↓) to ML( r ) and ML ∅ ( r ). For instance, both logics are compact and their formulas are preserved by generated sub-models (see [START_REF] Areces | Hybrid logics: characterization, interpolation and complexity[END_REF]).

The study we carried out in this paper draws a more detailed picture of the properties of of memory logics. We have investigated these logics in a number of recent papers [START_REF] Areces | Hybrid logics: The old and the new[END_REF]Areces, Figueira, & Mera, 2009;[START_REF] Areces | Tableaux and model checking for memory logics[END_REF][START_REF] Mera | Modal Memory Logics[END_REF] in which we present complete axiomatizations, tableaux calculi, complexity analisys for model checking, and preliminary results on the Beth and the interpolation properties for different fragments of this family. But there is still work to be done.

Even though we obtained logics less expressive than HL(↓), most of the logics we analyzed are undecidable. One of the motivations behind memory logics was to find decidable but yet useful logics to model scenarios with state. With this goal in mind several directions for future research suggest themselves. One possibility is to study memory logics as temporal logics, restricting the class of models to linear or tree structures which has shown to reduce complexity for hybrid logics (see [START_REF] Areces | The computational complexity of hybrid temporal logics[END_REF]). The complexity of hybrid logics over restricted frame classes was investigated in detail by [START_REF] Schneider | The Complexity of Hybrid Logics over Restricted Classes of Frames[END_REF], and a similar approach can be pursued for memory logics. In a related line, the freeze operator of [START_REF] Henzinger | Half-order modal logic: How to prove real-time properties[END_REF] (a binding operator weaker than ↓ that bind values associated to the states instead of the states themselves) can also be further weakened using the ideas presented in this article. Finally decidable memory logics could also be obtained by following the approach of [START_REF] Meier | The complexity of satisfiability for fragments of hybrid logic-Part I[END_REF] which instead of restricting the class of frames, imposed restrictions on the Boolean operators allowed in the language.

  g , w |= ϕ and D, I, g , w |= ψ D, I, g , w |= r ϕ iff there is w s.t. (w, w ) ∈ I(r) and D, I, g , w |= ϕ D, I, g , w |= ↓i.ϕ iff D, I, g , w |= ϕ where g (j) = g(j) for j = i and g (i) = w.

2.

  Chose Successor: Spoiler chooses r ∈ rel, and v s , an I s (r)-successor of w s . If w s has no I s (r)-successors, then Duplicator wins. Duplicator has to chose v d , an I d (r)successor of w d , such that v s and v d agree. If there is no such successor, Spoiler wins. Otherwise the game continues with EF

  ), let ϕ = r ψ. M, w |= r ψ iff (by definition) there is a w ∈ D, such that (w, w ) ∈ I(r) and M[w], w |= ψ iff (by inductive hypothesis on (i)) M[w], w |= Tr r (ψ) iff (by definition) M, w |= r Tr r (ψ) iff (by definition) M, w |= Tr r ( r ψ). The next case is ϕ = r ψ. M, w |= r ψ iff (by definition) M[w], w |= ψ iff (by inductive hypothesis on (1)) M[w], w |= Tr r (ψ) iff (by definition) M, w |= r Tr r (ψ) iff (by definition) M, w |= Tr r ( r ψ). Finally, let ϕ = f ψ. M, w |= f ψ iff (by definition) M[-w], w |= ψ iff (by inductive hypothesis on (2)) M, w |= Tr f (ψ) iff (by definition) M, w |= Tr r ( f ψ). For the property (2), let ϕ = r ψ. M[-w], w |= r ψ iff (by definition) there is a w ∈ D, such that (w, w ) ∈ I(r) and M[w], w |= ψ iff (by inductive hypothesis on (1)) M[w], w |= Tr r (ψ) iff (by definition) M, w |= r Tr r (ψ) iff (by definition) M, w |= Tr f ( r ψ). The next case is ϕ = r ψ. M[-w], w |= r ψ iff (by definition) M[w], w |= ψ (by inductive hypothesis on (1)) M[w], w |= Tr r (ψ) iff (by definition) M, w |= r Tr r (ψ) iff (by definition) M, w |= Tr f ( r ψ). The last case is ϕ = f ψ. M[-w], w |= f ψ iff (by definition) M[-w], w |= ψ (by inductive hypothesis on (2)) M, w |= Tr f (ψ) iff (by definition) M, w |= Tr f ( f ψ).

Lemma 34 .

 34 Let d be the modal depth of ϕ. If D, I, M , w |= d i=0 [r] i ¬ k ∧ ϕ then D, I, ∅ , w |= ϕ. Corollary 35. ML( r ) lacks the finite model property. Proof. Using Lemma 34 we can prove that the formula 4 i=0 [r] i ¬ k ∧ Inf , where Inf is the formula in the proof of Theorem 31, forces an infinite model. Corollary 36. The satisfiability problem for ML( r ) is undecidable.

KFigure 1 :

 1 Figure 1: Different expressive power of memory logics

  1. While Spoiler does not remember any reflexive state, Duplicator plays as follows:if Spoiler chooses w 0 in any model, Duplicator chooses w 0 in the other; if Spoiler chooses w

n , n > 0 in M 1 , Duplicator plays w n+1 in M 2 ; if Spoiler chooses w n , n > 0 in M 2 , Duplicator plays w n-1 in M 1 . Notice that with this strategy Spoiler chooses a reflexive state if and only if Duplicator answers with a reflexive one. This is clearly a winning strategy.

2. If ever Spoiler decides to remember a reflexive state, Duplicator starts using the following strategy: if Spoiler selects a state w n , Duplicator answers with an agreeing state w m of the opposite model. Notice that this is always possible since both w n and w m see infinitely many non remembered states and at least one remembered state.

  . If Spoiler plays in a state w ∈ ω s such that N (w ) is not remembered, then Duplicator chooses ω d and a state v ∈ ω d such that N (v ) is not remembered. Note that by definition of neighborhood and the fact that the accessibility relation is reflexive on ω i , w and v are not in the current memory M . Furthermore, this is always a valid move for Duplicator, given that there are infinitely many ω i connected with ω d and the fact that the number of remembered states is finite. So Duplicator can always choose a sufficiently large d and a state v ∈ ω d such that N (v ) is not remembered.5. If Spoiler plays in a state w ∈ ω s such that N (w ) is remembered, then Spoiler moves to an agreeing state v ∈ ω d . Let us see that there is always such v and that the invariant is preserved.

Spoiler moves to s in one model, Duplicator moves to s in the other model. Since every state of every ω i is connected to s, this is always a possible move for Duplicator. Given the invariant and the fact that s is connected with every other state in the model, it is easy to see that N (s) is not remembered in one model iff N (s) is not remembered in the other model. 4

Of course, the operator is usually defined on models without memory. We will define it so that it does not interact with the memory M .

Actually, we will restrict ourselves to unary modalities through the article.

Acknowledgements: S. Figueira is partially supported by CONICET (grant PIP 370).

The Decidability of ML( r )

We will first prove that K and ML( r ) are expressively equivalent over the class of tree models. We will then prove that ML( r ) has a tree model property. With those results at hand, decidability and pspace-completeness of ML( r ) easily follows.

Theorem 25. Restricted to the class of tree models, the logic K over the signature prop∪ {known}, rel is equivalent to ML( r ) over the signature prop, rel .

Proof. [K ≤ ML( r )]: This is a direct corollary of Theorem 9 [ML( r ) ≤ K]: We start by noticing that in ML( r ) we can eliminate k at modal depth 0 from a formula like r ϕ.

Claim: Let ϕ be the result of replacing all the occurrences of k that are in ϕ ∈ ML( r ) at modal depth zero by . Then M, w |= r ϕ if and only if M, w |= ϕ .

Proof of Claim. We proceed by induction on ϕ. The case for k , the propositional symbols and booleans are straightforward. We analyze the other cases: Define now the following translation taking ML( r )-formulas over the signature prop, rel to K-formulas over the signature prop ∪ {known}, rel :

Let ϕ ∈ ML( r ), and let M = D, I, M be an arbitrary tree model. Let M = D, I where I is identical to I except that I (known) = M . We can prove that M, w |= ϕ if and only if M , w |= Tr(ϕ).

We proceed by induction on ϕ. The propositional and boolean cases are trivial. The k case is also easy given the definitions. Let us consider ϕ = r ψ. Because M is a tree, the remember operator has no effect beyond modal operators, so M, w |= r ψ if and only if there exists v such that (w, We now prove that ML( r ) has the tree model property [START_REF] Blackburn | Modal Logic[END_REF], that is, every satisfiable formula in ML( r ) is satisfied in a tree model.

Undecidable Memory Logics

While ML( r ) is decidable, it seems to be standing at the border of undecidability. The logic ML ∅ ( r ), obtained from ML( r ) by restricting the class of models to those where S = ∅ is undecidable. Actually, the logic ML( r ) + i, obtained by adding a single nominal to ML( r ), is already undecidable. We first prove failure of the finite model property for ML( r ) + i.

Theorem 29. ML( r ) + i lacks the finite model property.

Proof. Consider the following formulas:

Because Back is satisfied, w ∈ B, B = ∅ and for all b ∈ B, (b, w) ∈ I(r). Note that Empty says that the one and two-step neighbors of w are not in M , and this also implies that every state in B is irreflexive. Because Spy is satisfied, if a = w and a is a successor of an element of B then a is also an element of B. As Succ is satisfied at w, every point in B has a successor distinct from w. No-3cyc disallow cycles of size 2 or 3 in B; and together with Tran they force I(r) to transitively order B.

It follows that B is an unbounded strict partial order as showed in the picture below, hence infinite, and so is D. i

• • •

We now show that ML( r ) + i is undecidable by encoding the ω × ω tiling problem (see [START_REF] Börger | The classical decision problem[END_REF]). Following ideas in [START_REF] Blackburn | Hybrid languages[END_REF], we will use three modalities s , u and r . We construct a spy point over the relation I(s) (i.e., the point of evaluation will have access in one I(s)-step to any reachable state in the model). The relations I(u) and I(r) represent moving up and to the right, respectively, from one tile to the other. We code each type of tile with a fixed propositional symbol t i . With this encoding we define for each tiling problem T , a formula ϕ T such that the set of tiles types T tiles ω × ω iff ϕ T has a model. Theorem 30. The satisfiability problem for ML( r ) + i is undecidable.

Proof. Let T = {T 1 , . . . , T n } be a set of tile types. Given a tile type T i , u(T i ), r(T i ), d(T i ), l(T i ) will represent the colors of the up, right, down and left edges of T i respectively. Define:

(

1≤j≤n,r(T i )=l(T j ) t j . Let the formula ϕ T be the conjunction of all the above formulas. We show that T tiles ω × ω if and only if ϕ T is satisfiable.

Suppose M, w |= ϕ T . Observe that Back and Spy, together with Empty make w a spy via I(s) (and also force I(u) and I(r) to be irreflexive and asymmetric). These I(s)accessible states will represent the tiles. We will have that [[s]]ψ holds at w iff ψ is true at every tile, and s s ψ holds at tile v iff ψ is true at some (perhaps the same) tile. Now, Grid states that from every tile there is another tile moving up (that is, following the I(u)-relation). The same holds for the right direction (following the I(r)-relation). Func (together with Back and Spy) forces I(u) and I(r) to be functional. Conf ensures that the tiles are arranged as a grid, once we force I(u)•I(r), the composition of I(u) and I(r), to be irreflexive (UR-No-Cycle), and we forbid the existence of cycles following successive steps in the I(u), I(r) and I(u) relations, in that order (URU-no-Cycle).

That completes the description of the grid. The last three formulas ensure that every tile has a unique type t i , and that the colors of the tiles match properly. From this, it easily follows that M is a tiling of ω × ω.

For the converse, suppose f : ω × ω → T is a tiling of ω × ω. We define the model M = ω × ω ∪ {w}, I, ∅ where I is The reader may verify that, by construction, M, w |= ϕ T .