Stephane Demri

A Two-Variable Separation Logic and Its Inner Circle

Keywords: F.3.1 [Specifying and Verifying and Reasoning about Programs]: Logics of Programs Theory, Verification Separation logic, two-variable logics, interval temporal logic, modal logic, data logic, decidability, complexity

Separation logic is a well-known assertion language for Hoare-style proof systems. We show that first-order separation logic with a unique record field restricted to two quantified variables and no program variables is undecidable. This is among the smallest fragments of separation logic known to be undecidable, and this contrasts with decidability of two-variable first-order logic. We also investigate its restriction by dropping the magic wand connective, known to be decidable with non-elementary complexity, and we show that the satisfiability problem with only two quantified variables is not yet elementary recursive. Furthermore, we establish insightful and concrete relationships between two-variable separation logic and propositional interval temporal logic (PITL), data logics, and modal logics, providing an inner circle of closely-related logics.

INTRODUCTION

Bounding the number of variables. The satisfiability problem for the two-variable fragment of first-order logic (FO2) is decidable [START_REF] Scott | A decision method for validity of sentences in two variables[END_REF][START_REF] Mortimer | On language with two variables[END_REF], and it is NEXPTIME-complete [START_REF] Lewis | Complexity Results for classes of quantificational formulas[END_REF]Grädel et al. 1997a], even though the extension with three variables is known to be undecidable [START_REF] Kahr | Entscheidungsproblem reduced to the ∀ ∃ ∀ case[END_REF]. Bounding the number of variables to find decidable fragments is usually motivated by identifying maximal fragments that are decidable or to determine a rough boundary between decidability and undecidability. It is often observed that the critical zone for the decidability border lies between two and three variables for first-order dialects; for instance, the two-variable fragment of first-order intuitionistic logic (with constant domain) has been shown undecidable in [START_REF] Gabbay | Undecidability of modal and intermediate first-order logics with two individual variables[END_REF], whereas FO2 extended with weak forms of recursion such as transitive closure operators is also undecidable [START_REF] Grädel | Undecidability Results on Two-Variable Logics[END_REF]. Similarly, monodic two-variable first-order linear-time temporal logic with equality is undecidable [START_REF] Degtyarev | Equality and monodic first-order temporal logic[END_REF]. By contrast, decidability results of FO2 interpreted over linear structures can be found in [START_REF] Otto | Two Variable First-Order Logic over Ordered Domains[END_REF]]; FO2 on data words is de-cidable, too, and somewhat equivalent to the reachability problem for Petri nets [START_REF] Boja Ńczyk | Two-variable logic on data words[END_REF]]. There are also other decidable extensions of FO2, see [START_REF] Pacholski | Complexity of Two-Variable logic with counting[END_REF]Grädel et al. 1997b;[START_REF] Kiero Ński | Two-Variable First-Order Logic with Equivalence Closure[END_REF][START_REF] Szwast | FOˆ2 with one transitive relation is decidable[END_REF][START_REF] Charatonik | Decidability of Weak Logics with Deterministic Transitive Closure[END_REF]. At the propositional level, bounding the number of propositional variables also makes sense, to restrict syntactic resources and to study its impact on the complexity of decision problems; see examples for modal and temporal logics in [START_REF] Halpern | The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic[END_REF][START_REF] Demri | The complexity of Propositional Linear Temporal Logics in Simple Cases[END_REF]. Herein, we follow a similar path, and we consider first-order separation logic [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF]].

Decidability and complexity issues for separation logics. Before going any further, let us recall briefly that the models (heaps) in separation logics can be understood as partial functions with profile h : N N k for some k ≥ 1 and with finite domain (k corresponds to the number of record fields). The set of natural numbers behaves here as an abstraction for the sets of locations and values, respectively. Separating connectives are those in the logical formalism that operate on models by possibly updating them by addition or removal of elements in the domain of the heap (this is done in a controlled way, of course). Program variables are understood as first-order variables with a rigid interpretation (in contrast to quantified variables).

First-order separation logic is used as an assertion language for Hoare-style proof systems about programs with pointers [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF]]. There is an ongoing quest to determine expressive fragments with relatively low complexity (see e.g. [START_REF] Cook | Tractable Reasoning in a Fragment of Separation Logic[END_REF]) and to extend known decidability results (see e.g. [START_REF] Iosif | The Tree Width of Separation Logic with Recursive Definitions[END_REF]Brotherston et al. 2014]). As far as decidability is concerned, first-order separation logic with two record fields (2SL) is shown undecidable in [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF]] (see also [Yang 2001, Section 8.1] or the undecidability results from [START_REF] Brotherston | Undecidability of Propositional Separation Logic and Its Neighbours[END_REF][START_REF] Larchey-Wendling | Nondeterministic Phase Semantics and the Undecidability of Boolean BI[END_REF], which are obtained in an alternative setting with propositional variables and no first-order quantification) and the proof does not require any use of separating connectives.

So, the result in [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF]] has been strengthened in [START_REF] Brochenin | On the Almighty Wand[END_REF] by showing that first-order separation logic with a unique record field (1SL) is also undecidable, which is obtained by showing that 1SL is equivalent to weak secondorder logic (weakness refers to quantifications over finite sets only). Recently, in [START_REF] Demri | Expressive completeness of separation logic with two variables and no separating conjunction[END_REF], 1SL restricted to two quantified variables has also been shown to be equivalent to weak second-order logic, providing another undecidability proof but one more complex than what is presented below, since one needs to go through an encoding of weak second-order logic. If separating implication (also known as the "magic wand" operator) is dropped, decidability is regained but with non-elementary complexity as a consequence of [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF][START_REF] Stockmeyer | The complexity of decision problems in automata theory and logic[END_REF]. A natural continuation of this undecidability result, quite surprising considering that there is a single record field, would be to see how the undecidability is sensitive to the number of quantified variables, following the trend of works related to two-variable fragments of first-order dialects. Whereas 1SL restricted to one variable and augmented with program variables admits a decidable satisfiability problem and is the subject of another paper [Demri et al. 2014], we study herein the two-variable first-order separation logic without program variables; the atomic formulae are made of the equality predicate symbol and the points-to predicate only (no other predicate symbols are allowed), which is a considerably downgraded version of the full logic. Separating connectives include separating conjunction and separating implication.

Our contribution. The paper presents two main results and provides interesting relationships between separation logic [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF]], interval temporal logic [START_REF] Moszkowski | A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time[END_REF]], data logics [START_REF] Boja Ńczyk | Two-variable logic on data words[END_REF]] and modal logics, see e.g. [START_REF] Blackburn | Modal Logic[END_REF]. In that way, we improve our understanding about the expressive power of separation logic fragments.

(1) We show that two-variable first-order separation logic with a unique record field (1SL2) has an undecidable satisfiability problem by reduction from the halting problem for Minsky machines (Section 4). It is certainly minimal in terms of the number of quantified variables, considering that the case with one variable is decidable [Demri et al. 2014]. This concludes the classification of fragments of 1SL with respect to the number of variables. For first-order separation logic, undecidability already strikes with two variables (by contrast to the NEXPTIMEcompleteness of FO2), which could be explained by the fact that the magic wand can be used to simulate quantification of locations (see the proof in Section 4). In our proof, all the difficulties are concentrated on the use of only two variables: of course, we can take advantage of the recycling of variables as done for modal logics [START_REF] Gabbay | Expressive Functional Completeness in Tense Logic[END_REF]], but this is not sufficient since we need to compare the neighborhood of locations that are not direct predecessors or successors. This is where the separating operators for separation logic are helpful, for instance to operate surgically on selections of the heap (see Section 4.4). Additionally, we provide evidence that an undecidable logic on data words from [START_REF] Boja Ńczyk | Two-variable logic on data words[END_REF]] can be reduced to two-variable first-order separation logic (Section 4.6). Logics on data words have already been used to get undecidability results for separation logic with data fields, see e.g. [START_REF] Bansal | Beyond Shapes: Lists with Ordered Data[END_REF]].

Herein, we use a simple version of first-order separation logic without program variables, without data fields, and apart from equality, there is only one binary relation, and it is functional and finite. This marks a substantial difference with existing work, and it highlights just how few our syntactic resources are while still getting undecidability and complexity lower bounds.

(2) Two-variable first-order separation logic with a unique record field and without the magic wand (1SL2( * )) is known to be decidable (as a consequence of [Brochenin et al. 2012, Corollary 3.3]), but we establish non-elementary complexity by a reduction from Moszkowski's Propositional Interval Temporal Logic PITL (see e.g. [START_REF] Moszkowski | A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time[END_REF]), despite the restriction on the number of variables. So, we are able to make an interesting bridge between interval temporal logics and separation logics (see Section 3). This is not completely surprising since there is a clear similarity between the "chop" operator in interval temporal logics and the separating conjunction in separation logic, but we are able to conclude an original result about a fragment of two-variable first-order separation logic. To our knowledge, this is the first time that the similarity has been turned into a concrete, interesting result. The possibility to relate separation logic and interval temporal logic has been already envisaged by Tony Hoare, see e.g. [START_REF] Zhou Chaochen | Logics of Specification Languages[END_REF].1 Finally, we refine this result by proposing a new simple modal logic MLH interpreted on heaps that can be translated into two-variable separation logic with a unique record field via a standard translation schema (see Section 2.4 and Section 3.4). For instance, we are able to show that MLH restricted to only the separating conjunction (i.e. without the magic wand operator) has non-elementary complexity. So, we are also happy to provide a modal logic closely related to twovariable separation logic, strengthening relationships between modal logics and two-variable fragments (see also [START_REF] Lutz | The complexity of reasoning with Boolean Modal Logics[END_REF] in a more classical setting).

Figure 1 diagrams the contributions of this paper and puts them in context with previously-known results. Logic definitions can be found in Sections 2, 3.1, and 4.6.

PITL non-elementary [START_REF] Moszkowski | A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time[END_REF] MLH( * )

non-elementary (Theorem 3.12)

1SL2( * )

non-elementary (Theorem 3.8) [START_REF] Etessami | First-Order Logic with Two variables and Unary Temporal logics[END_REF] 1SL( * )

α≥1 FO2 α,0 (<, +1, =) NEXPTIME-complete
decidable [START_REF] Brochenin | On the Almighty Wand[END_REF] MSO decidable [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF] Halting problem undecidable [START_REF] Minsky | Computation: finite and infinite machines[END_REF] MLH (introduced herein) Structure of the paper. Section 2 is primarily dedicated to the presentation of the separation logic 1SL, but it also explains how data words can be encoded in 1SL2( * ). This encoding will be useful many times in succeeding sections. Moreover, we introduce a new modal logic on heaps (MLH) that is a fragment of 1SL2( * ). Section 3 recalls the basics of propositional interval temporal logic PITL and we present an elementary satisfiability-preserving reduction from PITL to 1SL2( * ), leading to a non-elementary lower bound for 1SL2( * ). This result is strengthened by showing non-elementarity of MLH restricted to only the separating conjunction * . Section 4 contains a master reduction from the halting problem for Minsky machines into the satisfiability problem for 1SL2. To do so, several technical problems need to be solved and we dedicate one subsection to each of them. We also explain how undecidability results for first-order data logics can be used to obtain a similar result for 1SL2, which provides an alternative to the master reduction. Finally, Section 5 contains concluding remarks.

PRELIMINARIES

First-order separation logic with one record field (1SL)

A heap h is a partial function h : N N with finite domain. We write dom(h) to denote its domain and ran(h) to denote its range. Two heaps h 1 , h 2 are said to be disjoint, denoted h 1 ⊥ h 2 , if their domains are disjoint; when this holds, we write h 1 h 2 to denote the heap obtained from h 1 and h 2 by taking their disjoint union. We use l i , with i, l i ∈ N and i ≥ 0, to represent locations. We write

l 1 → l 2 → • • • → l m (or, equivalently, l m ← l m-1 ← • • • ← l 1 ) to mean that for every i ∈ [1, m -1], h(l i ) = l i+1 . In that case {l 1 , . . . , l m-1 } ⊆ dom(h).
We write l to denote the cardinal of the set {l : h(l ) = l} made of predecessors of l (heap h is implicit in the expression l). A location l is an ancestor of a location l iff there exists i ≥ 0 such that h i (l) = l where h i (l) is shorthand for h(h(. . . (h(l) . . .))) (i applications of h to l).

Usually in models for separation logic(s), memory states have a heap and a store for interpreting program variables, see e.g. [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF]]. Our work concentrates on hardness results, and we are able to obtain these results without using such program variables. For this reason, we do not introduce them. Observe also that heaps will be understood as first-order structures of the form (N, R) where R is a finite and functional binary relation. Indeed, R = {(l, h(l)) : l ∈ dom(h)} for a heap h. A new modal logic with such frames is presented in Section 2.4. The locations l and l are in the same connected component whenever (l, l ) ∈ (R ∪ R -1 ) * . Usually, connected components are understood as non-singleton components. A finite functional graph (N, R) can be made of several maximal connected subgraphs so that each connected subgraph is made of a cycle, possibly with trees attached to it. Figure 2 presents a heap, i.e. a finite functional graph on N with two maximal connected subgraphs. Let Var = {u 1 , u 2 , . . .} be a countably infinite set of quantified variables. Formulae of 1SL are defined by the abstract grammar below:

φ ::= u i = u j | u i → u j | emp | φ ∧ φ | ¬φ | φ * φ | φ - * φ | ∃ u i φ
The connective * is called the separating conjunction and the connective - * is called the separating implication (also known as the magic wand). We will make use of standard notations for the derived connectives.

An assignment is a map f of the form Var → N. The satisfaction relation |= is parameterized by assignments and defined as follows:

-h |= f emp def ⇔ dom(h) = ∅. -h |= f u i = u j def ⇔ f (u i ) = f (u j ). -h |= f u i → u j def ⇔ f (u i ) ∈ dom(h) and h(f (u i )) = f (u j ). -h |= f φ 1 ∧ φ 2 def ⇔ h |= f φ 1 and h |= f φ 2 . -h |= f ¬φ def ⇔ h |= f φ. -h |= f φ 1 * φ 2 def ⇔ there exist h 1 , h 2 such that h 1 ⊥ h 2 , h = h 1 h 2 , h 1 |= f φ 1 and h 2 |= f φ 2 . -h |= f φ 1 - * φ 2 def ⇔ for all h , if h ⊥ h and h |= f φ 1 then h h |= f φ 2 . -h |= f ∃ u i φ def ⇔ there is l ∈ N such that h |= f [ui →l] φ (f [u i → l] refers to a map equal to f except that u i takes the value l). Remark 2.1. Given a bijection σ : N → N, we write h = h • σ to denote the heap whose graph is {(σ(l), σ(h(l))) : l ∈ dom(h)}. Similarly, we write f = f • σ to denote the assignment such that f (u i ) = σ(f (u i )). Note that for all formulae φ, we have h |= f φ iff h |= f φ.
That is why heaps equipped with assignments are understood modulo bijections (i.e. concrete heaps are canonical elements of equivalence classes).

For a fixed i ≥ 0, we write 1SLi to denote the fragment of 1SL restricted to i quantified variables and 1SLi( * ) to denote its restriction when the magic wand operator is disallowed.

Let L be a logic among 1SL, 1SLi, 1SLi( * ). The satisfiability problem for L takes as input a sentence φ from L and asks whether there is a heap h such that h |= φ (regardless of assignment, as φ has no free variables). THEOREM 2.2. [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF][START_REF] Brochenin | On the Almighty Wand[END_REF] The satisfiability problem for 1SL is undecidable, and the satisfiability problem for 1SL( * ) is decidable with nonelementary complexity.

Decidability of 1SL( * ) is shown by (easy) reduction into weak monadic second-order logic of one unary (total) function with equality (referred to as MSO in Figure 1) that is shown decidable in [Börger et al. 1997, Corollary 7.2.11] by using [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF]].

Toolkit of formulae

In the following, let u and u be the variables u 1 and u 2 , in either order. Throughout this paper, we build formulae with the quantified variables u and u. Note that any formula φ(u) with free variable u can be turned into an equivalent formula with free variable u by switching the two variables.

Below, we define (standard) formulae and explain which properties they express.

-The domain dom(h) has exactly one location:

size = 1 def = ¬emp ∧ ¬(¬emp * ¬emp)
-The domain dom(h) has exactly two locations:

size = 2 def = (¬emp * ¬emp) ∧ ¬(¬emp * ¬emp * ¬emp)
u has a successor: alloc(u)

def = ∃ u u → u -u has at least k predecessors: u ≥ k def = k times (∃ u u → u) * • • • * (∃ u u → u) -u has at most k predecessors: u ≤ k def = ¬ ( u ≥ k + 1) -u has exactly k predecessors: u = k def = ( u ≥ k) ∧ ¬( u ≥ k + 1)
-For all ∼∈ {≤, ≥, =} and i ≥ 0, we define the following formulae:

u 0 ∼ k def = u ∼ k u i+1 ∼ k def = ∃ u u → u ∧ u i ∼ k u -i-1 ∼ k def = ∃ u u → u ∧ u -i ∼ k
For instance, u 6 ≥ 5 states that there is a (necessarily unique) location at distance 6 from u and its number of predecessors is greater than or equal to 5. The formula u -5 ≤ 2 states that there is a (not necessarily unique) location at distance -5 from u and its number of predecessors is not strictly greater than 2. For instance, u 1 ≥ 1 is logically equivalent to alloc(u).

-There is a non-empty path from u to u and nothing else except loops that exclude u:

ls (u, u) def = u = 0 ∧ alloc(u) ∧ ¬alloc(u) ∧ ∀ u ((alloc(u) ∧ u = 0) =⇒ u = u) ∧ ∀ u ( u = 0 ∧ u = u) =⇒ ( u = 1 ∧ alloc(u))
-There is a (possibly empty) path from u to u:

ls(u, u) def = u = u ∨ * ls (u, u) One can show that h |= f ls(u, u) iff there is i ∈ N such that h i (f (u)) = f (u).
The proof for this property can be found in [Brochenin et al. 2012, Lemma 2.4] (a similar property has been established for graph logics in [START_REF] Dawar | Expressiveness and complexity of graph logic[END_REF]). -There is at most a single connected component (and nothing else):

1comp def = ¬emp ∧ ∃ u ∀ u alloc(u) ⇒ ls(u, u)
-There are exactly two components:

2comps def = 1comp * 1comp
Remark 2.3. The heap is a finite tree with at least two nodes can be expressed by the formula below:

¬emp ∧ ∃ u ¬alloc(u) ∧ (∀ u alloc(u) ⇒ ls(u, u))
Complexity results about two-variable fragments of first-order logic over finite trees can be found in [START_REF] Benaim | Complexity of two-variable logic over finite trees[END_REF]] but we cannot really take advantage of them since we do not use predicate symbols apart from equality and the points-to relation. By contrast, we do admit separating connectives.

Remark 2.4. Observe that all formulae in our toolkit above are in the 1SL2( * ) fragment. This is not by accident; we will study this fragment extensively in Section 3 and will need to employ several of the above formulae.

Encoding data words with multiple attributes

In this section, we present a simple encoding of data words with multiple attributes into heaps that will be useful in the rest of the paper. Finite data words [START_REF] Bouyer | A Logical Characterization of Data Languages[END_REF]] are ubiquitous structures that include timed words, runs of Minsky machines, and runs of concurrent programs with an unbounded number of processes. These are finite words in which every position carries a label from a finite alphabet and a finite tuple of data values from some infinite alphabet. A wealth of specification formalisms for data words (and slight variants) has been introduced stemming from automata to adequate logical languages such as first-order logic [START_REF] Boja Ńczyk | Two-variable logic on data words[END_REF][START_REF] Th | Two-Variable Logic and Two Order Relations[END_REF] and temporal logics [START_REF] Figueira | Reasoning on words and trees with data[END_REF][START_REF] Decker | Ordered Navigation on Multi-attributed Data Words[END_REF].

A data word of dimension β is a finite non-empty sequence in ([1, α] × N β ) + for some α ≥ 1 and β ≥ 0. The set [1, α] is understood as a finite alphabet of cardinal α whereas N is the infinite data domain. Data words of dimension zero are simply finite words over a finite alphabet whereas data words of dimension one correspond to data words in the sense introduced in [START_REF] Bouyer | A Logical Characterization of Data Languages[END_REF]]. Finite runs of Minsky machines (with two counters) can be viewed as data words of dimension two over the alphabet [1, α] assuming that the Minsky machine has α distinct instructions (see also Section 4.1).

Let dw = (a 1 , d 1 1 , . . . ,

d 1 β ) • • • (a L , d L 1 , . . . , d L β ) be a data word in ([1, α] × N β ) + , i.e.
dw is of dimension β and its underlying alphabet has cardinal α ≥ 1. The data word dw shall be encoded by the heap h dw containing a path of the form below:

l 1 0 → l 1 1 → • • • → l 1 β → • • • → l L 0 → l L 1 → • • • → l L β
where -for every i ∈ [1, L], l i 0 has a i + 2 predecessors, -for all i ∈ [1, L] and all j ∈ [1, β], l i j has d i j + α + 3 predecessors, -every location in the domain of the heap is either on that path or points to a location on that path.

Such a path from l 1 0 to l L β is called the main path, and h

(β+1)L-1 dw (l 1 0 ) = l L β .
Other simple encodings are possible (for instance without shifting the values from the finite alphabet or from the infinite domain) but the current one is well-suited for all the developments made in this paper. In particular, the encoding allows us to know easily whether a location encodes a letter from the finite alphabet or an element from the infinite domain. Note also that h dw is not uniquely specified, and we understand it modulo isomorphism as discussed in Remark 2.1.

Figure 3 presents the encoding of the data word dw 0 = (2, 1)(1, 2)(2, 2) of dimension 1 with α = 2 with its representation of the heap h dw in which the predecessors of the locations on the main path are provided schematically. We use this type of schema in Section 4 to illustrate a few constructions. 3. The heap for data word dw 0 = (2, 1)(1, 2)(2, 2) of dimension 1 and with α = 2 (focus on the main path) with its schematic representation.

• • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • Fig.
The heap h dw looks like a fishbone. Let us make this precise. A heap h is a fishbone def ⇔ (fb1). dom(h) = ∅, (fb2). there is a location reachable from all the locations of dom(h) that is not in dom(h), and (fb3). there are no distinct locations l 1 , l 2 , l 3 , l 4 , l 5 such that l 1 → l 2 → l 3 ← l 4 ← l 5 in the heap h.

When h is a fishbone, it has a tree-like structure (when looking at the edges backward), equipped with a root (the unique location from (fb2)), but additionally, one can recognize the locations on the main path as those locations with at least one predecessor. The existence of such a main path is guaranteed by (fb3). The first location on the main path satisfies the formula

first(u) def = ( u ≥ 1) ∧ ¬( u -1 ≥ 1)
and the last location on the main path satisfies precisely the formula

last(u) def = ( u ≥ 1) ∧ ¬alloc(u)
Let φ fb be the formula below:

(fb1) ¬emp ∧ (fb2) (∃ u ¬alloc(u) ∧ (∀ u alloc(u) ⇒ ls(u, u))) ∧ (fb3) ¬(∃ u ( u -2 ≥ 0) * ( u -2 ≥ 0)) LEMMA 2.5. Let h be a heap. h |= φ fb iff h is a fishbone.
The proof for Lemma 2.5 is by an easy verification. Now, let us refine the notion of a fishbone heap so that it takes into account constraints on numbers of predecessors. An (α, β)-fishbone is a fishbone heap such that (C1). the first location on the main path has a number of predecessors in [3, α + 2], (C2). on the main path, a location with a number of predecessors in [3, α + 2], is followed by β locations with at least α + 3 predecessors, and (C3). the number of locations on the main path is a multiple of β + 1.

It is easy to check that the formulae φ C1 , φ C2 and φ C3 in 1SL2( * ) defined below are able to express the conditions (C1), (C2) and (C3), respectively. This assumes that the heap is already known to be a fishbone, which is equivalent to the satisfaction of φ fb (by Lemma 2.5).

φ (C1) def = ∃ u first(u) ∧ (3 ≤ u ≤ α + 2) φ (C2) def = ∀ u (3 ≤ u ≤ α + 2) ⇒ i∈[1,β] u +i ≥ α + 3 φ (C3) def = ∀ u (3 ≤ u ≤ α + 2) ⇒ ((¬ u +(β+1) ≥ 0) ∨ (3 ≤ u +(β+1) ≤ α + 2)) We write dw(α, β) to denote the formula φ fb ∧ φ (C1) ∧ φ (C2) ∧ φ (C3) . It specifies the shape of the encoding of data words in ([1, α] × N β ) + as stated below. LEMMA 2.6. Let h be a heap. We have h |= dw(α, β) iff h is an (α, β)-fishbone.
Again, the proof is by an easy verification by using Lemma 2.5 and the correspondence between condition (Ci) and the formula φ (Ci) .

Given a data word dw = (a

1 , d 1 1 , . . . , d 1 β ) • • • (a L , d L 1 , . . . , d L β )
, we can associate a (α, β)fishbone h dw with (1 + β) × L locations on the main path, say

l 1 0 → l 1 1 → • • • → l 1 β → • • • → l L 0 → l L 1 → • • • → l L β such that -for every i ∈ [1, L], l i 0 = a i + 2, -for all i ∈ [1, L] and all j ∈ [1, β], l i j = d i j + α + 3.
The heap h dw is unique modulo isomorphism. This natural encoding generalizes the encoding of finite words by heaps in [Brochenin et al. 2012, Section 3] (see also [START_REF] Bansal | Beyond Shapes: Lists with Ordered Data[END_REF]) while providing a much more concise representation. Note also that the encoding by itself is of no use since it is essential to be able to operate on it with the logical language at hand.

Conversely, given a (α, β)-fishbone h with (1 + β) × L locations on the main path, say

l 1 0 → l 1 1 → • • • → l 1 β → • • • → l L 0 → l L 1 → • • • → l L β we associate a (unique) data word dw h = (a 1 , d 1 1 , . . . , d 1 β ) • • • (a L , d L 1 , . . . , d L β ) such that for every i ∈ [1, L], a i def = l i 0 -2 and for all i ∈ [1, L] and all j ∈ [1, β], d i j def = l i j -α -3.
LEMMA 2.7. There is a one-to-one map between data words in

([1, α] × N β ) + and (α, β)-fishbone heaps (modulo isomorphism).
The proof is then by an easy verification. So, we have seen that finite words can be encoded in 1SL2( * ), which allows us to establish that 1SL2( * ) is NEXPTIME-hard since first-order logic restricted to two quantified variables on finite words (written FO2 α,0 (<, +1, =) herein) is NEXPTIMEcomplete [START_REF] Etessami | First-Order Logic with Two variables and Unary Temporal logics[END_REF]]. Indeed, consider a sentence φ in that fragment of first-order logic. Let us define t

(φ) such that φ is satisfiable iff dw(α, 0) ∧ t(φ) is satis- fiable in 1SL2( * ).
We define the logarithmic-space translation t as follows (i, j ∈ {1, 2}).

t is homomorphic for Boolean connectives, t(

u i = u j ) def = u i = u j , -t(a(u i )) def = ( u i = a + 2), -t(u i = 1 + (u j )) def = u j → u i , -t(u i < u j ) def = ls(u i , u j ) ∧ u i = u j , -t(∃ u i φ) def = ∃ u i ( u i ≥ 1) ∧ t(φ).
Note that FO2 α,0 (<, +1, =) and 1SL2( * ) share the same number of quantified variables and ls(u i , u j ) can be expressed in 1SL2( * ) (see Section 2.2). We do not provide the correctness proof herein since we can do much better than NEXPTIME-hardness by making a strong connection with Moszkowski's Interval Temporal Logic ITL (with the locality condition), see Section 3. However, we shall use a similar type of reduction in Section 4.6 with β > 0.

A modal logic for heaps

Let us conclude this section about logics for heaps, by introducing a new modal logic. We introduce a modal logic that is closely related to 1SL2. Modal Logic for Heaps (MLH) is a multimodal logic in which models are exactly heap graphs and it does not contain propositional variables (as 1SL does not contain unary predicate symbols). In a sense, it is similar to Hennessy-Milner logic HML [START_REF] Hennessy | On observing nondeterminism and concurrency[END_REF] in which the only atomic formulae are truth constants. However, the language contains modal operators and separating connectives, which is a feature shared with the logics defined in [START_REF] Courtault | A Modal BI Logic for Dynamic Resource Properties[END_REF]. We define below the formulae of the modal logic MLH.

φ ::= ⊥ | ¬ φ | φ ∧ φ | 3 φ | 3 -1 φ | = φ | φ | φ * φ | φ - * φ
Note that there are no quantified variables involved in formulae, which is a feature shared with most known propositional modal logics, see e.g. [START_REF] Blackburn | Modal Logic[END_REF]].

We write MLH( * ) to denote the fragment of MLH without the magic wand operator - * .

A model for MLH M is a pair (N, R) such that R is a binary relation on N that is finite and functional. Otherwise said, the models for MLH are heap graphs. Models for MLH could be defined as heaps but we prefer to stick to the most usual presentation for modal logics with frames. The satisfaction relation |= is defined below and it provides a standard semantics for the modal operators and separating connectives (we omit the clauses for Boolean connectives):

-never M, l |= ⊥, -M, l |= 3φ def ⇔ there is l such that (l, l ) ∈ R and M, l |= φ, -M, l |= 3 -1 φ def ⇔ there is l such that (l , l) ∈ R and M, l |= φ, -M, l |= φ def ⇔ there is l such that (l, l ) ∈ R * and M, l |= φ where R * is the reflexive and transitive closure of R, -M, l |= = φ def ⇔ there is l = l such that M, l |= φ, -M, l |= φ 1 * φ 2 def ⇔ (N, R 1 ), l |= φ 1 and (N, R 2 ), l |= φ 2 for some partition {R 1 , R 2 } of R, -M, l |= φ 1 - * φ 2 def ⇔ for all models M = (N, R ) such that R ∩ R = ∅ and R ∪ R is functional, M , l |= φ 1 implies (N, R ∪ R ), l |= φ 2 .
We use the following standard abbreviations:

-U φ def = φ ∨ = φ, [U ]φ def = ¬ U ¬φ, -[ =]φ def = ¬ = ¬φ, -3 -1 ≥k def = 3 -1 * • • • * 3 -1 (k ≥ 1 times), 3 -1 ≤k-1 def = ¬3 -1 ≥k , -3 -1 [k1,k2] def = 3 -1 ≥k1 ∧ 3 -1 ≤k2 , 3 -1 =k def = 3 -1 ≥k ∧ 3 -1 ≤k .
A formula φ is satisfiable whenever there is a model M and a location l such that M, l |= φ. The satisfiability problem for MLH is therefore defined as any such problem for modal logics. Note that MLH has forward and backward modalities as in Prior's tense logic (see e.g. [START_REF] Prior | Past, Present and Future[END_REF]), the inequality modal operator (see e.g. [START_REF] De Rijke | The modal logic of inequality[END_REF]) and the transitive closure operator as in PDL (see e.g. [START_REF] Harel | Dynamic Logic[END_REF]). The most non-standard feature of MLH is certainly the presence of the separating connectives. It is possible to design a relational translation from MLH formulae into 1SL2 formulae by recycling variables (only u 1 and u 2 are used, so i ∈ {1, 2}):

t is homomorphic for the connectives ¬, ∧, * and - * ,

-t(⊥, u i ) def = ⊥, -t(3 φ, u i ) def = ∃ u 3-i (u i → u 3-i ) ∧ t(φ, u 3-i ), -t(3 -1 φ, u i ) def = ∃ u 3-i (u 3-i → u i ) ∧ t(φ, u 3-i ), -t( = φ, u i ) def = ∃ u 3-i (u i = u 3-i ) ∧ t(φ, u 3-i ), -t( φ, u i ) def = ∃ u 3-i ls(u i , u 3-i ) ∧ t(φ, u 3-i ). PROPOSITION 2.8. A formula φ in MLH is satisfiable iff ∃ u 1 t(φ, u 1 ) is satisfiable in 1SL2. Moreover, if φ is in MLH( * ), then ∃ u 1 t(φ, u 1 ) is in 1SL2( * ).
PROOF. (sketch) The proof is obtained as an obvious adaptation of the proof for the relational translation from modal logic K into FO2, see e.g. [START_REF] Ch | Methods for automated theorem proving in non classical logics[END_REF]van Ben-them 1976;[START_REF] Blackburn | Modal Logic[END_REF]. Indeed, the models (N, R) for MLH are heap graphs and therefore formulae in 1SL2 can be equivalently interpreted on MLH models; for instance, we get

(N, R) |= f u 1 → u 2 iff (f (u 1 ), f (u 2 )) ∈ R. Similarly, (N, R) |= f φ 1 - * φ 2 iff for all MLH models (N, R ) such that (N, R∪R ) is an MLH model too and (N, R ) |= f φ 1 , we have (N, R ∪ R ) |= f φ 2 .
Note that u j is the only free variable in t(φ, u j ). The standard translation t is semantically faithful in the following sense: for all MLH models (N, R), l ∈ N and formulae φ in MLH, we have (N, R), l |= φ iff (N, R) |= [u1 →l] t(φ, u 1 ). This is sufficient to establish Proposition 2.8.

We show that for all i ∈ {1, 2}, for all formulae ψ in MLH, for all MLH models M = (N, R) and for l ∈ N, we have

M, l |= ψ iff M |= [ui →l] t(ψ, u i ).
The proof is by structural induction. The base case for ⊥ and the cases in the induction step for the Boolean connectives are straightforward. By way of example, let us provide the cases in the induction step for ψ = ψ and for ψ = ψ 1 * ψ 2 . The proof for the other cases is similar and quite standard. Case ψ = ψ . The following are equivalent:

-M, l |= ψ, -M, l |= ψ for some l ∈ R * (l) (by definition of |=), -M |= [u3-i →l ] t(ψ , x 3-i ) for some l ∈ N such that l ∈ R * (l) (by the induction hypothe- sis), -M |= [ui →l] ∃ u 3-i ls(u i , u 3-i ) ∧ t(ψ , x 3-i ) (by definition of |= in 1SL2 and by the fact that ls is the reachability predicate), -M |= [ui →l] t(ψ, u i ) (by definition of t). Case ψ = ψ 1 * ψ 2 . The following are equivalent: -M, l |= ψ, -(N, R 1 ), l |= ψ 1 and (N, R 2 ), l |= ψ 2 for some partition {R 1 , R 2 } of R, (by definition of |= in MLH), -(N, R 1 ) |= [ui →l] t(ψ 1 , u i ) and (N, R 2 ) |= [ui →l] t(ψ 2 , u i ) for some partition {R 1 , R 2 } of R, (by the induction hypothesis), -M |= [ui →l] t(ψ 1 , u i ) * t(ψ 2 , u i ) (by definition of the satisfaction relation in 1SL2) -M |= [ui →l] t(ψ, u i ) (by definition of t).
Modal logic MLH can be viewed as a fragment of 1SL2. Any formula ψ 1 * ψ 2 [resp. ψ 1 - * ψ 2 ] in t(φ, u 1 ) has at most one free variable. A similar restriction can be found in monodic fragments for first-order temporal logics, see e.g. [START_REF] Degtyarev | Equality and monodic first-order temporal logic[END_REF].

Since MLH( * ) can be translated into 1SL2( * ) and 1SL( * ) is decidable [Brochenin et al. 2012, Corollary 3.3], we get decidability of MLH( * ) as a corollary.

COROLLARY 2.9. The satisfiability problem for MLH( * ) is decidable.

Note that to be more uniform, we could have added to the modal language the converse operators = -1 and -1 . However, since the inequality relation is symmetric, = -1 φ is logically equivalent to = φ. The above translation can be obviously extended with the modal operator -1 and therefore decidability holds also for this extension. However, we have introduced MLH mainly to establish non-elementarity of MLH( * ) (shown below), refining the result for 1SL2( * ). We did not include -1 because the proof of non-elementarity result does not require it. By contrast, we do not know whether the satisfiability problem for MLH is decidable. As far as we know, the characterization of the computational complexity of MLH without separating connec-tives is open too. This corresponds to a fragment of deterministic PDL with (restricted) graded modalities and inequality modality.

WHEN INTERVAL TEMPORAL LOGIC MEETS SEPARATION LOGIC

Interval-based temporal logics admit time intervals as first-class objects (instead of time points), and an early and classical study for reasoning about intervals can be found in [START_REF] Allen | Maintaining knowledge about temporal intervals[END_REF]]. One of the most prominent interval-based logics is Propositional Interval Temporal Logic (PITL), introduced by Ben Moszkowski in [START_REF] Moszkowski | Reasoning about digital circuits[END_REF]] for the verification of hardware components. It contains the so-called 'chop' operation that consists of chopping an interval into two subintervals. This is of course reminiscent of separating conjunction in separation logic, and in this section we make a formal statement about this correspondence, in addition to deriving new complexity results. Before doing so, it is worth noting that even though most standard point-based temporal logics used in computer science are decidable (CTL, CTL , ECTL , etc.), undecidability is much more common in the realm of interval-based temporal logics. Below, we consider PITL in which propositional variables are interpreted under the locality condition and for which decidability is guaranteed but computational complexity is very high. This will allow us to derive similar bounds for 1SL2( * ).

Below, we recall the main definitions about PITL under the locality condition and we explain why formulae from PITL can be faithfully translated into formulae in 1SL2( * ), leading to insights about both formalisms and new complexity results. A similar analysis is presented for MLH( * ) making new bridges between modal logic, interval-based temporal logics and separation logic.

Logic PITL

Given α ≥ 1, we consider the finite alphabet Σ = [1, α] and we write PITL Σ to denote propositional interval temporal logic in which the models are non-empty finite words in Σ + . We write PITL instead of PITL Σ when the finite alphabet Σ is clear from the context. Formulae for PITL Σ are defined according to the following abstract grammar:

φ ::= a | pt | ¬φ | φ ∧ φ | φ C φ
with a ∈ Σ. Even though elements of Σ are natural numbers (for the sake of technical convenience), we write a to denote such an arbitrary element to emphasize that a is a letter from a finite alphabet. Roughly speaking, a holds true at word w when a is the first letter of w. Similarly, the atomic formula pt holds true at a word w when the word w is only a single letter. The connective C is the chop operator, which chops a word.

Formally, we have a nonempty word w ∈ Σ + , its length |w|, extractions of the ith letter w i where 1 ≤ i ≤ |w|, and extractions of nonempty subwords w i..j = w i w i+1 ..w j , where 1 ≤ i ≤ j ≤ |w|. We define a ternary relation chops on words:

chops def = {(w 1 , w 2 , w 3 ) | ∃ a, w , w such that w 1 = w aw , w 2 = w a, w 3 = aw }
Observe that when a word w 1 is chopped into two subwords w 2 and w 3 , there is an overlap between the last letter of w 2 and the first letter of w 3 . For instance, (abb, ab, bb) ∈ chops but (ab, a, b) ∈ chops.

Let us define the satisfaction relation |= for PITL Σ between a word w ∈ Σ + and a formula φ:

-w |= a def ⇔ w 1 = a (here, w 1 denotes the first letter of w). -w |= pt def ⇔ |w| = 1. -w |= ¬φ def ⇔ w |= φ. -w |= φ ∧ ψ def ⇔ w |= φ and w |= ψ. -w |= φ C ψ def ⇔ there exist words w 1 , w 2 such that chops (w, w 1 , w 2 ), w 1 |= φ and w 2 |= ψ.
The satisfiability problem for PITL Σ consists in checking whether a PITL Σ formula admits a model satisfying it. Note that the models are nonempty, finite words and the satisfaction of a letter on a word depends only on its first letter (the locality condition).

Two examples. Consider the alphabet Σ with two distinct letters a and b and the PITL Σ formula below:

(b C a) C ¬pt
This formula is satisfiable; many words satisfy this formula, for example the word "bab"-the top-level chop is satisfied since ba |= b C a and ab |= ¬pt. This gives insight on how to specify a lower-bound on word length, by applying sufficiently many chops and ¬pt to force a particular (minimum) length. Of course, b C a also enforces a minimum word length (of 2), but constrains also the word content.

Consider another example:

pt ∧ (a C b)
For this formula to be satisfiable, there must exist a word w for which both w |= pt and w |= a C b. This is impossible, as the first implies |w| = 1, and there is no way to chop a single-letter word into subwords that satisfy both a and b; the formula is unsatisfiable.

THEOREM 3.1. (see e.g. [START_REF] Moszkowski | Reasoning about digital circuits[END_REF][START_REF] Moszkowski | A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time[END_REF]) Given α ≥ 1 and Σ = [1, α], the satisfiability problem for PITL Σ is decidable, but with α ≥ 2 is not elementary recursive.

Correspondence between words and heaps

From now on, we use the data word representation of Section 2.3. From Lemma 2.7, we know there is a fishbone heap h w corresponding to each nonempty word w ∈ Σ + . Let us define a relation ∼ that establishes this correspondence between words and their fishbone representations, adding also a correspondence between the empty word and the empty heap:

∼ def = (w, h w ) | w ∈ Σ + ∪ {( , ∅)}
Here, observe that:

(1) ∼ is a bijection between the set of finite words in Σ * and the set of (equivalence classes of isomorphic) (α, 0)-fishbone heaps augmented with the empty heap; (2) so, every word w is in dom(∼);

(3) so, every (α, 0)-fishbone heap is in ran(∼); (4) so, if w ∼ h, h is either empty or an (α, 0)-fishbone heap; and (5) if w ∼ h, then w is empty iff dom(h) is empty.

In this section, we will only employ (α, 0)-fishbone heaps, with α = card(Σ).

The correspondence between finite words in Σ + and (α, 0)-fishbone heaps satisfies a nice property as far as splitting a word into two disjoint subwords is concerned (which is a slight variant of chopping). Before making a formal statement, let us introduce the following notion.

A clean cut of a (α, 0)-fishbone heap h is a pair of (α, 0)-fishbone heaps (h 1 , h 2 ) such that h = h 1 h 2 , and for some words w 1 ∼ h 1 and w 2 ∼ h 2 , we have w 1 w 2 ∼ h. That is, a clean cut is one that neatly cleaves a heap representation of a word into two subheaps in correspondence with two subwords. Figure 4 illustrates examples of a clean cut and a non-clean cut on a fishbone heap. Informally, a non-clean cut is one that either results in one subheap (or both) no longer satisfying the (α, 0)-fishbone conditions, or that results in subheaps that don't preserve predecessor counts and thus don't represent subwords of the original.

• • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • qrrrrrrrrrrrrrrr • • • • • • • • • • • • • • • • • • • • • • • • • • q r r
r r r r r r r r r r r r r r LEMMA 3.2. Let w ∼ h with w = w 1 w 2 ∈ Σ * . There exist heaps h 1 and h 2 such that h = h 1 h 2 , w 1 ∼ h 1 , and w 2 ∼ h 2 .

PROOF. Suppose that w ∼ h and w = w 1 w 2 ∈ Σ * . If w 1 = ε or w 2 = ε, then the proof is by an easy verification with h equal to h 1 or h 2 respectively. In particular, if w = ε, then h is the empty heap and therefore w 1 = w 2 = ε and h 1 = h 2 = ∅, which satisfies the statement.

Otherwise suppose that w

= a 1 • • • a K ∈ Σ + , w 1 = a 1 • • • a K ∈ Σ + , w 2 = a K +1 • • • a K ∈ Σ + (K > K ). Since w is nonempty and w ∼ h, h is a fishbone heap and the main path of h is of the form l 1 - → l 2 - → • • • - → l K and for every i ∈ [1, K], l i = a i + 2.
Let h 1 be the subheap of h whose domain is {l ∈ N : l is an ancestor of l K in h}, and let h 2 be the unique heap such that h = h 1 h 2 . It is easy to show that w 1 ∼ h 1 and w 2 ∼ h 2 . Moreover, it is not difficult to see that (h 1 , h 2 ) is a clean cut of h. Lemma 3.2 entails the following lemma, that will be useful to show the correctness of our reduction from PITL Σ into 1SL2( * ). It is tailored to the semantics of the chop operator in PITL Σ . LEMMA 3.3. For all letters a, b ∈ Σ, words w ∈ Σ + and w , w ∈ Σ * , and heaps h such that w ∼ h and chops (aw, aw b, bw ), there exist heaps h 1 , h 2 such that w b ∼ h 1 , w ∼ h 2 , and h = h 1 h 2 .

A reduction and its three ways to chop

In this section, we present a satisfiability-preserving translation of PITL Σ into 1SL2( * ). This translation hinges on the insight that the chop operation is very similar to the separating conjunction in separation logic. However, the correspondence is not an exact one: the connective C of PITL Σ does not cut into disjoint pieces, but rather preserves one letter on both sides, in a sense "duplicating" the letter upon which the chop operates. To handle this discrepancy, our translation uses the standard separating conjunction on heaps, but internally carries a "ghost letter" (a parameter to the translation) on one side to represent this "lost" letter. In the translation, we denote this ghost letter parameter a ∈ Σ. Figure 5 illustrates how a chop operation on words is translated into a separation on heaps. It is worth noting that we must always obtain a clean cut from the original heap.

Before presenting the formal definition of the translation, let us present a formula that allows us to perform a clean cut for which one of the subheaps contains all the ancestors of f (u). Such a formula will be used in the translation and this is the purpose of Lemma 3.4. LEMMA 3.4. Given a fishbone heap h and a word w such that w ∼ h, and an assignment f such that f (u) is a location on the main path of h with h |= f alloc(u), any pair of heaps

(h 1 , h 2 ) such that h = h 1 h 2 , h 1 |= f dw(α, 0) ∧ ¬alloc(u), and h 2 |= f dw(α, 0) ∧ u = 0, is a clean cut of h.
PROOF. Since h 1 |= f dw(α, 0) and h 2 |= f dw(α, 0), we know the heaps h 1 and h 2 are (α, 0)-fishbones. Fishbones are single components, so we know that h must be separated into exactly two connected components. It remains to analyze precisely how h can be separated into two fishbones, and to show that it must be a clean cut.

We know l = f (u) is on the main path of h, so that means h |= f u > 0. Since h 2 |= f u = 0, that means l must have the same number of predecessors in h as it does in h 1 . We know h 1 |= f ¬alloc(u), and we know l has at least one predecessor in h 1 . Therefore, l is on the main path of h 1 . We know h 2 |= f u = 0, so l is not on the main path of h 2 . However, it is allocated (since h |= f alloc(u) and h 1 |= f ¬alloc(u)), so its successor (call the location l ) is on the main path of h

2 . Let f = f [u → l ]. Now, note that h |= f u → u and h 1 |= f u → u,
and recall that that on a fishbone, no two predecessors of an element can both have predecessors (fb3). Therefore, l must have the same number of predecessors in h 2 as it did in h, and none of these predecessors can be on the main path.

Thus l is the final location on the main path of h 1 , and l is the first location on the main path of h 2 . Further, l has 0 predecessors in h 2 and the same number of predecessors in h and h 1 . l has 0 predecessors in h 1 and the same number of predecessors in h and h 2 .

Putting the above together, since l and l are positions on the main path of h such that h(l) = l , and since l ∈ dom(h 1 ), l ∈ dom(h 2 ), l ∈ ran(h 1 ), l ∈ ran(h 2 ), we must have a clean cut.

We reduce a PITL Σ formula φ to a 1SL2( * ) formula t(φ) with the help of the main translation t(•). We use the auxiliary translation map t a (•) parameterized by a ghost letter a. The three disjuncts in the translation of φ C ψ correspond to three types of chopping of w that leads to three ways of separating the heap h (assuming that w ∼ h):

(1) When (w, aw 1 b, bw 2 ) ∈ chops and the ghost letter is a, the heap h is separated into the heap h 1 with w 1 b ∼ h 1 (with ghost letter a) and into the heap h 2 with w 2 ∼ h 2 (with ghost letter b).

(2) When (w, w, b) ∈ chops and the ghost letter is a, the heap h is separated into itself (again with ghost letter a) and into the empty heap (with ghost letter b).

(3) When (w, a, w) ∈ chops and the ghost letter is a, the heap h is separated into the empty heap (with ghost letter a) and into itself (again with ghost letter a).

These are the three possible cases and the rest of the translation is quite straightforward.

t(φ) def = dw(α, 0) ∨ emp ∧ a∈Σ t a (φ) t a (b) def = if b = a ⊥ if b = a t a (pt) def = emp t a (¬φ) def = ¬t a (φ) t a (φ ∧ ψ) def = t a (φ) ∧ t a (ψ) t a (φ C ψ) def = chop1 a ∨ chop2 a ∨ chop3 a
(with the three formulae as defined below)

chop1 a def = b∈Σ ∃ u u = b + 2 ∧ dw(α, 0) ∧ ¬alloc(u) ∧ t a (φ) * dw(α, 0) ∧ u = 0 ∧ t b (ψ) chop2 a def = b∈Σ (∃ u last(u) ∧ u = b + 2) ∧ t a (φ) * emp ∧ t b (ψ) chop3 a def = emp ∧ t a (φ) * t a (ψ)
In full generality, t a (•) is also parameterized by the alphabet Σ (see the clause for formulae with outermost chop operator C) and the formulae chop1 a , chop2 a , and chop3 a are parameterized by φ C ψ. Clearly the translation t(•) can only produce 1SL2( * ) formulae, as the right-hand side of each translation step above is in 1SL2( * ). Note also that t a (φ) always produces a closed formula (i.e., without free occurrences of individual variables). The correctness of the translation is stated below, making completely explicit the role of the ghost letter in the translation process. LEMMA 3.5. Let a ∈ Σ, w ∈ Σ * , and h be a heap such that w ∼ h. For every PITL Σ formula φ, we have aw |= φ iff h |= t a (φ).

Remark 3.6. Note that since t a (φ) has no free occurrences of individual variables, in Lemma 3.5, there is no need to specify what the assignments are.

PROOF. The proof is by structural induction. The base cases are:

-t a (b). (⇒) If aw |= b, then a = b. Clearly h |= , so h |= t a (b). (⇐) h |= t a (b), so it must be that a = b (since h |= ⊥). Thus aw |= b. -t a (pt). (⇒) If aw |= pt, then w = . Thus h = ∅. Since t a (pt) = emp, we have h |= t a (pt).
(⇐) h |= t a (pt), and since t a (pt) = emp, we know h = ∅. Thus w = , so clearly aw |= pt.

The inductive cases are:

t a (¬φ Case 3. w = , w = (the chop occurs in the middle of the word). We know w 1 is nonempty and starts with a, so let w 1 be a word such that w 1 = aw 1 . From Lemma 3.3, we have heaps h 1 , h 2 such that h = h 1 * h 2 , w 1 ∼ h 1 , and w ∼ h 2 . Observe that, since they are in ran(∼), h 1 and h 2 are (α, 0)-fishbones. Since aw 1 |= φ and bw |= ψ, then by IH, we have h 1 |= t a (φ) and h 2 |= t b (ψ). Now, let l be the location of the chop, so that l is the last position on the main path of h 1 and a predecessor of the first position on the main path of h 2 . Let f be an assignment such that f (⇐) If we have that h |= t a (φ C ψ), then one of the disjuncts in the translation holds, depending on where the separation applies in the heap and the content at that position. We consider three cases based on which of the constraints (chop1 a , chop2 a , or chop3 a ) applies.

(u) = l. Since h 1 |= f dw(α, 0) ∧ ¬alloc(u) ∧ t a (φ) and h 2 |= f dw(α, 0) ∧ u = 0 ∧ t b (ψ), we have h |= f dw(α, 0) ∧ ¬alloc(u) ∧ t a (φ) * dw(α, 0) ∧ u = 0 ∧ t b (ψ) .
Case 1. The chop1 a constraint applies (neither subheap is empty). We know it holds for some b ∈ Σ, and that the existentially quantified formulae holds for some location; w.l.o.g., assume that the case b ∈ Σ holds, with location l. Let f be an assignment such that f (u) = l. We know that h |= f u = b + 2, and that h can be separated into two disjoint subheaps h 1 , h 2 such that h 1 |= f dw(α, 0) ∧ ¬alloc(u) ∧ t a (φ) and h 2 |= f dw(α, 0) ∧ u = 0 ∧ t b (ψ). This cut must be a clean cut by Lemma 3.4. By IH, then, we have words w 1 , w 2 such that w 1 ∼ h 1 , w 2 ∼ h 2 , aw 1 |= φ, and bw 2 |= ψ. We know w 1 ends with a letter b, since u is the last position on the main path of h 1 and has b + 2 predecessors. So then chops (aw 1 w 2 , aw 1 , bw 2 ) holds. Thus aw 1 w 2 |= φ C ψ.

Case 2. The chop2 a constraint applies (the right subheap is empty). We know it holds for some b ∈ Σ, and that the existentially quantified formula holds for some location; w.l.o.g., then, assume that the case b ∈ Σ holds, at some location l. We know that heap h can be separated into two disjoint subheaps h 1 , h 2 such that h 1 |= t a (φ), h 2 = ∅, and h 2 |= t b (ψ). Thus h = h 1 , and by IH we have aw |= φ and b |= ψ. Next, let f be an assignment such that f (u) = l. We know h |= f last(u) and that h |= f u = b + 2.

Since w ∼ h, the last letter of w is b. So chops (aw, aw, b), and therefore aw |= φ C ψ.

Case 3. The chop3 a constraint applies (the left subheap is empty). We then have h 1 = ∅, ∅ |= t a (φ), and h 2 |= t a (ψ). Since h = h 2 , by IH we have a |= φ and aw |= ψ. Then chops (aw, a, aw); thus aw |= φ C ψ.

Therefore, aw |= φ iff h |= t a (φ)
As a result, we obtain a reduction between the satisfiability problems, as stated below.

LEMMA 3.7. Given α ≥ 1 and Σ = [1, α], a PITL Σ formula φ is satisfiable if and only if the 1SL2( * ) formula t(φ) is satisfiable.

PROOF. (⇒) Suppose that φ is satisfiable. This means that there exists a nonempty word w such that w |= φ. The word w can be written in the form w = aw for some letter a. If w = , we have w ∼ ∅ and by Lemma 3.5, we have ∅ |= emp ∧ t a (φ). So ∅ |= t(φ) and therefore t(φ) is satisfiable. If w = , then there is a (α, 0)-fishbone heap h such that w ∼ h . By Lemma 3.5, we have h |= dw(α, 0) ∧ t a (φ). So h |= t(φ) and therefore t(φ) is satisfiable.

(⇐) If t(φ) is satisfiable, then there exists a heap h such that h |= (dw(α, 0) ∨ emp) ∧ a∈Σ t a (φ). If h |= emp ∧ t a (φ) for some letter a, then by Lemma 3.5, we have a |= φ. Otherwise, if h |= dw(α, 0) ∧ t a (φ), then h is an (α, 0)-fishbone heap by Lemma 2.6 and then there is a word w such that w ∼ h such that by Lemma 3.5, we have aw |= φ. In both cases, φ is a satisfiable formula in PITL Σ . THEOREM 3.8. The satisfiability problem for 1SL2( * ) is decidable but not elementary recursive.

PROOF. Satisfiability for PITL Σ is known to be decidable with non-elementary complexity when Σ has at least two elements, see e.g. [START_REF] Moszkowski | Reasoning about digital circuits[END_REF][START_REF] Moszkowski | A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time[END_REF], and 1SL( * ) is decidable [START_REF] Brochenin | On the Almighty Wand[END_REF]. From the correctness of our translation t(•) of PITL Σ to 1SL2( * ) (Lemma 3.7), we then conclude that 1SL2( * ) is decidable but not elementary recursive. Note that the map t(•) may require exponential time and space in the size of the input formula in the worst-case but this is still fine to establish that 1SL2( * ) is not elementary recursive, since this adds only a single exponential.

As mentioned earlier, Theorem 3.8 refines the non-elementarity result for 1SL( * ) established in [START_REF] Brochenin | On the Almighty Wand[END_REF]].

Remark 3.9. The reduction from PITL to 1SL2( * ) provided in this section allows us to underline the common features of both formalisms. However, non-elementarity of 1SL2( * ) can be established in a slightly different way as explained below. First, nonelementarity of PITL is due to Dexter Kozen (see e.g. [Moszkowski 2004, Appendix A.3])2 , and the proof is by reduction from the nonemptiness problem of regular expressions built over a binary alphabet with union, concatenation and complement [START_REF] Stockmeyer | The complexity of decision problems in automata theory and logic[END_REF]. Nonelementarity of 1SL2( * ) can be obtained by defining a similar reduction, but this is of course less insightful to understand the relationships between interval temporal logic and separation logic. Alternatively, it is also possible to consider the variant of PITL in which the chop operator does not share a letter, since this variant is of identical expressive power and complexity. In that way, we may avoid the introduction of the ghost letter but at the cost of introducing empty models (which may occur when chopping has no sharing) and of using a less standard interval temporal logic. So, the current reduction from PITL is quite an attractive option to relate the logics. Finally, as noted in [Moszkowski 2004, Appendix A], complexity results about PITL presented in [START_REF] Moszkowski | Reasoning about digital circuits[END_REF]] were obtained in collaboration with Joseph Halpern.

In Section 3.4 below, we establish an even stronger result (see Theorem 3.12). The proof uses the same principles as for the proof of Theorem 3.8 and we only need to express the properties in modal lingua.

A refinement with the modal fragment of 1SL2( * )

In this section, we show that the satisfiability problem for MLH( * ) is decidable but it is not elementary recursive. Decidability is due to the fact that the standard translation leads to formulae in 1SL2( * ), see Section 2.4. In order to establish the lower bound, we express in MLH( * ) all the properties that were useful to translate PITL Σ formulae into 1SL2( * ). For instance, note that the empty heap is the only heap validating the formula ([U ]¬3 ). Similarly, a location with at least one predecessor and with no successor (for instance, last location on the main path in a fishbone heap) satisfies the formula

(3 -1 ∧ ¬3 ).
More interestingly, the formula in 1SL2( * ) characterizing the (α, β)-fishbone heaps has a modal counterpart. Let us consider the following formulae.

-The formula φ 2 fb defined below is designed exactly as the formula φ fb (see Section 2.3).

( U 3 )∧ U ((3 -1 ∧ ¬3 ) ∧ [ =]¬(3 -1 ∧ ¬3 )) ∧ [U ](3 ⇒ (3 -1 ∧ ¬3 ))∧ (¬ U (3 -1 3 -1 * 3 -1 3 -1 ))
This is a faithful translation except that we use the specification language MLH( * ). -The formula φ 2 (C1) defined below is also designed exactly as the formula φ (C1) (see Section 2.3). C3) . It specifies the shape of the encoding of data words in ([1, α] × N β ) + as stated below. Note that since dw 2 (α, β) is a Boolean combination of formulae whose outermost connectives are [U ] or U , then dw 2 (α, β) holds true at some location iff dw 2 (α, β) holds true at any location. LEMMA 3.10. Let M = (N, R) be a model for MLH. M, l |= dw 2 (α, β) for some location l iff M is the graph of an (α, β)-fishbone heap.

U ((3 -1 ) ∧ (¬3 -1 3 -1 ) ∧ 3 -1 [3,α+3] ) -The formula φ 2 (C2) is equal to [U ](3 -1 [3,α+3] ⇒ i∈[1,β] i times 3 • • • 3 3 -1 ≥α+3 ) -The formula φ 2 (C3) is defined below: [U ](3 -1 [3,α+3] ⇒ (¬ β+1 times 3 • • • 3 ) ∨ β+1 times 3 • • • 3 (3 -1 [3,α+3] )) We write dw 2 (α, β) to denote the formula φ 2 fb ∧ φ 2 (C1) ∧ φ 2 (C2) ∧ φ 2 (
Again, the proof is by an easy verification by using Lemma 2.5 and the correspondence between condition (Ci) and the formula φ 2 (Ci) . In the rest of this section we are back to the case β = 0.

Given a formula φ in PITL Σ with Σ = [1, α], we define a modal formula t 2 (φ) such that φ is satisfiable iff t 2 (φ) is satisfiable. Actually, the modal formula t 2 (φ) will express exactly the same properties as in the translation into 1SL2( * ). For instance, t 2 (φ) is precisely the formula below:

(dw 2 (α, 0) ∨ ([U ]¬3 )) ∧ ( a∈Σ t 2 a (φ))
The formula t 2 a (φ) is defined inductively as follows.

t 2 a (a)

def = and t 2 a (b) def =⊥ for every letter b ∈ Σ \ {a}. -t 2 a (•) is homomorphic for Boolean connectives. -t 2 a (pt) def = ([U ]¬3 ). -The formula t 2 a (φ C ψ) is defined as chop1 2 a ∨ chop2 2 a ∨ chop3 2 a where: -chop1 2 a def = b∈Σ U ((3 -1 =b+2 ∧ dw 2 (α, 0) ∧ ¬3 ∧ t 2 a (φ)) * (dw 2 (α, 0) ∧ ¬3 -1 ∧ t 2 b (ψ))), -chop2 2 a def = ( b∈Σ U ((3 -1 ∧ ¬3 ) ∧ 3 -1 =b+2 ) ∧ (t 2 a (φ) * (t 2 b (ψ) ∧ ([U ]¬3 )))), -chop3 2 a def = ((t 2 a (φ) ∧ ([U ]¬3 )) * t 2 a (ψ)). LEMMA 3.11. Let α ≥ 1, Σ = [1, α]
, φ be a PITL Σ formula and t 2 (φ) be its translation in MLH. We have φ is satisfiable iff t 2 (φ) is satisfiable.

The proof goes as in the case for the direct translation into 1SL2( * ) since the modal subformulae express exactly the same properties. Therefore, we can refine Theorem 3.8 as follows.

THEOREM 3.12. The satisfiability problem for MLH( * ) is decidable but not elementary recursive.

Interestingly, we do not know the decidability status for full MLH (i.e., with the magic wand operator).

HOW TWO VARIABLES WITH THE MAGIC WAND ENCODE RUNS

In this section, we consider the logic 1SL2 (i.e., equipped with both the separating conjunction and the separating implication), and we prove its undecidability. In order to show that the 1SL2 satisfiability problem is undecidable, we reduce the halting problem for Minsky machines [START_REF] Minsky | Computation: finite and infinite machines[END_REF]].

Minsky machines in a nutshell

Let M be a Minsky machine with α ≥ 1 instructions, where 1 is the initial instruction and α is the halting instruction. Machine M has two counters C 1 and C 2 and the instructions are of the following types:

(a) I:

C j := C j + 1; goto J. (b) I: if C j = 0 then goto J 1 else (C j := C j -1; goto J 2 ). (c) α: halt. (j ∈ [1, 2], I ∈ [1, α -1], J, J 1 , J 2 ∈ [1, α])
Machine M halts if there is a run of the form

(I 0 , c 1 0 , c 2 0 ), (I 1 , c 1 1 , c 2 1 ), . . . , (I L , c 1 L , c 2 L ) such that (I i , c 1 i , c 2 i ) ∈ [1, α]×N 2 (i ∈ [1, L]
), the succession of configurations respects the instructions (in the obvious way), I 0 = 1, I L = α, and c 1 0 = c 2 0 = 0. The halting problem consists in checking whether a machine halts and it is known to be undecidable, see e.g. [START_REF] Minsky | Computation: finite and infinite machines[END_REF]]. Clearly, a halting run is a data word dw of dimension 2 such that the first letter is 1 and the last letter is α.

When a Minsky machine M has α ≥ 1 instructions, any run starting from the initial instruction 1 and ending by the halting instruction α (there is a single such run since M is deterministic) is a data word of dimension two over the finite alphabet [1, α]. The main and obvious idea to get undecidability is to show how 1SL2 can characterize heaps encoding data words of dimension two corresponding to halting runs of M .

Roadmap

Let us start by explaining how the rest of the section is structured. The next paragraph describes how initial and final conditions on the run are encoded in 1SL2; typically the run starts by instruction 1 and possibly ends by the halting instruction α. Then, the next two paragraphs deal with the description of two problems that we need to tackle. (Section 4.3 and Section 4.4 contain the technical developments.) In a nutshell, the first problem consists of being able to compare the numbers of predecessors of two locations (which corresponds to comparison of two counter values in Minsky machines), whereas the second problem is related to the fact that these two locations may be separated by distance three along the main path. Both issues stem from the fact that we have only two individual variables at hand. (It is already known how to solve these problems with an unbounded number of variables [START_REF] Brochenin | On the Almighty Wand[END_REF]].) Section 4.5 provides the final definition of the reduction from the halting problem for Minsky machines to the satisfiability problem for 1SL2 whereas Section 4.6 presents the idea of an alternative undecidability proof by reduction from a first-order logic on data words (see Section 2.3). These proofs share essential building blocks, for instance the constructions allowing to compare numbers of predecessors. However, this provides different points of view as well.

Limit conditions. We have seen that (α, 2)-fishbone heaps can be characterized thanks to the formula dw(α, 2). Obviously, more constraints need to be expressed, typically those related to the first instruction and those related to the halting instruction. Let us start by specifying the limit conditions thanks to the formulae φ first and φ last below.

-The first three locations on the main path have 3, α + 3, and α + 3 predecessors respectively:

φ first def = ∃ u first(u) ∧ ( u = 3) ∧ ( u +1 = α + 3) ∧ ( u +2 = α + 3)
-The main path encoding the run ends by a configuration with the halting instruction:

φ last def = ∃ u (( u = α + 2) ∧ ( u +2 ≥ 0) ∧ ¬( u +3 ≥ 0))
Let us call φ the conjunction of dw(α, 2) ∧ φ first ∧ φ last . It specifies the shape of the encoding of the run without taking care of the constraints about counter values and instruction counter. LEMMA 4.1. Let h be a heap. h |= φ iff h encodes a data word andd 1 1 = d 1 2 = 0. We have provided formulae for basic properties about the encoding of the runs, but this is insufficient. Indeed, three consecutive locations on the main path encode a configuration of the Minsky machine M . In order to check that two consecutive configurations correspond to a step that is valid for M , we need to compare numbers of predecessors for locations on the main path at distance three from each other. For instance, considering locations l and l on the main path such that l = h 3 (l), we plan to build formulae to express constraints between l and l . There are two problems there.

dw = (a 1 , d 1 1 , d 1 2 ) • • • (a L , d L 1 , d L 2 ) such that a 1 = 1, a L = α,
Distance three. Firstly, with two variables, one can explore the heap but is obliged to "forget" previously visited locations (in fact, it is possible to store only a finite amount of information). Since [START_REF] Gabbay | Expressive Functional Completeness in Tense Logic[END_REF]], it is known how to visit a graph with only two quantified variables. In the current encoding of runs, we will need to compare the numbers of predecessors of locations at distance three on the main path. Let us consider the formula below:

∃ u [∀ u (u → u) ⇒ ( u = 3 ∨ u = 7)] ∧ [∃ u (u → u) ∧ ∃ u ((u → u) ∧ u = 11)]
This formula states that there are two locations in the model for which there is a path of length 2 between them, the second location has exactly 11 predecessors and for the first one, every predecessor has either 3 or 7 predecessors.

In MLH (without the use of * or - * ), this property can be written as follows:

U (2 -1 (3 -1 =3 ∨ 3 -1 =7 ) ∧ 333 -1 =11 )
So, it is possible to state properties between locations that are not direct successors, but note that we can only enforce properties while we are visiting the nodes: once we move forward or backward we have no more access to previously visited locations. This becomes a problem when we need to compare number of predecessors for locations at distance three. Observe that if we had proposed another encoding of the runs, at some stage we would have to deal with locations that are not direct successors and for which we need to compare some potentially unbounded amount of information (since we need anyhow to encode counter values that are potentially unbounded). Section 4.4 provides a solution to this problem by presenting a selective chopping of the heap that preserves the numbers of predecessors we wish to compare while being able to access easily those locations for which the number of predecessors are compared.

It is worth observing that for locations on the main path related to counter instructions, we are not in big trouble because it is possible with two quantified variables to visit two successive locations related to counter instructions and to check that they respect the instructions of the Minsky machine (because only a finite amount of information needs to be encoded). While moving along the model, we may "forget" where we start, but this is fine since we can remember the value of the counter instruction in the formula. By contrast, when comparing two locations corresponding to two successive values of the same counter, this does not work anymore.

Arithmetical constraints. Secondly, we have also to be able to compare numbers of predecessors between locations. For instance, given two locations l and l , we wish to be able to check whether l = l or l = l + 1. Such a need should not come as a surprise, since in our encoding of data words, data values are represented by numbers of predecessors. Such arithmetical constraints can be expressed in 1SL (i.e. without limiting the number of quantified variables), and this has been a key step to establish 1SL's equivalence to weak second-order logic on heaps [START_REF] Brochenin | On the Almighty Wand[END_REF]]. In Section 4.3, we provide a fine-tuned adaptation with only two quantified variables (instead of an unbounded number of variables) and with substantial simplifications. The developments in Section 4.3 are not consequences of developments from [Brochenin et al. 2012, Section 5.2] but rather refinements using similar principles. Actually, we can take advantage of the fact that we do not work on an arbitrary heap but rather on an (α, 2)-fishbone heap. Moreover, we do not seek expressive completeness but rather we aim at expressing a sufficient set of arithmetical constraints to allow us to characterize (α, 2)-fishbone heaps that encode halting runs of M .

Expressing arithmetical constraints

Below, we show how to express in 1SL2 the constraints u = u, u = u + 1 and u = u + 1, which is not at all obvious. We explain why this can be done in 1SL2 by a careful recycling of variables; along the way, we also take advantage of the properties of heaps satisfying φ .

We shall use the fact that N ≤ N iff for every n ≥ 0, we have N ≤ n implies N ≤ n. Quantification over the set of natural numbers will be simulated by quantification over disjoint heaps in which n is related to the cardinal of their domains. Such quantification is performed thanks to the magic wand operator.

A fork in h is a sequence of distinct locations l, l 0 , l 1 , l 2 such that h(l 0 ) = l, l 0 = 2, h(l 1 ) = l 0 , h(l 2 ) = l 0 and l 1 = l 2 = 0. The endpoint of the fork is l. Similarly, a knife in h is a sequence of distinct locations l, l 0 , l 1 such that h(l 0 ) = l, l 0 = 1, h(l 1 ) = l 0 and l 1 = 0. The endpoint of the knife is l. By way of example, the heap of Figure 6 contains three knives, two forks and four endpoints (identified by ' '). 6. A heap with three knives, two forks and four endpoints.

• • • • • • • • • • • • • • • • • Fig.
LEMMA 4.2. Let h be a (α, β)-fishbone heap with α ≥ 1 and β ≥ 0. Then, h has no knife and no fork.

Indeed, in such heaps, any allocated location has no predecessor or at least three predecessors.

A heap h is a collection of knives def ⇔ there is no location in dom(h) that does not belong to a knife and no distinct knives share the same endpoint. A heap h is segmented whenever dom(h) ∩ ran(h) = ∅ and no location has strictly more than one predecessor. LEMMA 4.3. Let h be a (α, β)-fishbone heap with α ≥ 1, β ≥ 0 and h be a segmented heap disjoint from h. Then, h h has no fork.

Being segmented can be naturally expressed in 1SL2:

seg def = ∀ u u (u → u ⇒ (( u = 1) ∧ ( u = 0) ∧ ¬alloc(u)))
The statement below is counterpart to [Brochenin et al. 2012, Lemma 5.2] with simplified properties and with simpler formulae but using only two quantified variables. LEMMA 4.4. There are formulae forky(u), KS and KS1F in 1SL2 such that for every heap h, (I) h |= f forky(u) iff all the predecessors of f (u) are endpoints of forks, (II) h |= KS iff h is a collection of knives, (III) h |= KS1F iff there are h 1 , h 2 such that h = h 1 h 2 , h 1 is a collection of knives and h 2 is made of a unique fork such that its unique endpoint is not in the range of h 1 .

PROOF. forky(u) is equal to:

∀ u (u → u) ⇒ (∃ u (u → u) ∧ ( u = 2) ∧ ¬( u -1 ≥ 1))
A knife is made of two consecutive memory cells that can be respectively called part 1 and part 2 as shown in

l part 1 ---→ l part 2 ---→ l . KS def = ∀ u alloc(u) ⇒ (φ part1 (u) ∨ φ part2 (u))
where

φ part1 (u) def = ( u = 0) ∧ ( u +1 = 1) ∧ ( u +2 = 1) ∧ ¬( u +3 ≥ 0) φ part2 (u) def = ( u = 1) ∧ ( u -1 = 0) ∧ ( u +1 = 1) ∧ ¬( u +2 ≥ 0) KS1F def = unique fork [∃ u ( u = 2) ∧ ( u +1 = 1) ∧ ¬( u +2 ≥ 0) ∧ ¬( u -1 ≥ 1) ∧ ¬(∃ u (u = u) ∧ ( u = 2))] ∧ [∀ u alloc(u) ⇒ (φ part1 (u) ∨ φ part2 (u) part with knifes ∨ (( u = 0) ∧ ( u +1 = 2)) ∨ ( u = 2)) part with one fork ]
In our proof, we use the idea of augmenting the heap with a segmented heap, then augmenting it further with knives to form forks whose endpoints are predecessors of u; this is borrowed from [START_REF] Brochenin | On the Almighty Wand[END_REF]]. As it is, this would not be sufficient to express arithmetical constraints on fishbone heaps since only two quantified variables are allowed. This restriction is not considered in [START_REF] Brochenin | On the Almighty Wand[END_REF]]-the formulae there use strictly more than two quantified variables. This is why we had to provide specific developments that are well-tailored to fishbone heaps while taking into account our limited amount of syntactic resources. Simplifications have also been made in order to focus on undecidability rather than on questions of expressive power. LEMMA 4.5. Let h be a heap with h = h 1 h 2 and f be an assignment such that h 1 |= f φ , f (u) is on the main path of the (α, 2)-fishbone heap h, h 2 |= f seg ∧ u = 0, n = card(ran(h 2 ) \ dom(h 1 )) and m is the number of predecessors of f (u) in h 1 . We have the following properties:

(a) h |= f ¬(KS - * ¬forky(u)) iff n ≥ m. (b) h |= f ¬(KS1F - * ¬forky(u)) iff n ≥ m -1.
In Figure 7, we present three heaps obtained by combining a segmented heap h 2 with collections of knives (corresponding to h 3 in the proof of Lemma 4.5). Edges labelled by '1' are part of a fishbone heap h 1 (partially represented) whereas edges labelled by '2' are part of a segmented heap h 2 so that no edge points to f (u) or to f (u). The heap on the left (corresponding to h 1 * h 2 in Lemma 4.5) is obtained by adding a segmented heap h 2 whereas the heap in the middle (say h 1 * h 2 * h 3 ) is obtained then by adding a collection of knives h 3 so that every predecessor of f (u) is the endpoint of a fork. Note that not all edges of the segmented heap are used to build forks. Similarly, the heap on the right (say h 1 * h 2 * h 3 ) is obtained then by adding a collection of knives h 3 to the heap h 1 * h 2 on the very left so that every predecessor of f (u) is the endpoint of a fork.

• f (u) • f (u) • • • • • • • • • • • • • • • 1 1 1 1 1 1 2 2 2 2 2 • f (u) • f (u) • • • 3 3 • • • • • • • • • • • • • • • • • • • • 3 3 1 1 1 1 1 1 2 2 2 2 2 3 3 3 3 3 3 • f (u) • f (u) • • • 3 3 • • • • • • • • • • • • • • • • • • 1 1 1 1 1 1 2 2 2
PROOF. Let us provide the proof for (a). (The proof for (b), being analogous, is omitted.) So, let h be a heap with h = h 1 h 2 such that h 1 |= f φ and h 2 |= f seg ∧ u = 0. Moreover, f (u) is on the main path, which entails that h(f

(u)) = f (u) (if h(f (u)
) is defined at all) and f (u) has at least one predecessor.

One can make the following (obvious) observations.

(O1). The heap h 1 has no knives and, h 1 and h 1 h 2 have no forks. (see Lemma 4.2 and Lemma 4.3). (O2). h 1 h 2 may not satisfy φ but this is fine since we only need to focus on the number of predecessors of f (u) (i.e., on the value m). Indeed, h 1 h 2 may contain knives (see the left heap in Figure 7). A knife l 1 → l 2 → l 3 in h 1 h 2 is made of l 1 ∈ dom(h 2 ) and of l 2 ∈ dom(h 1 ). This observation is not really used below but, hopefully, it could be helpful to better grasp how the heaps h 1 and h 2 are combined. (O3). f (u) has the same number of predecessors in h 1 and in h 1 h 2 . This is due to the fact that h 2 |= f u = 0. (O4). For every n ≥ 0, there is a disjoint heap h 2 such that h = h 1 h 2 , h 2 |= f seg ∧ u = 0 and card(ran(h 2 ) \ dom(h 1 )) = n. See the left heap in Figure 7 with card(dom(h 2 )) = 5 and card(ran(h 2 ) \ dom(h 1 )) = 4 (look at edges labelled by '2'). Once more, this observation is not used below but it will be in the proof of Proposition 4.6.

First, let us suppose that h |= f ¬(KS - * ¬forky(u)), i.e., ( †) there is a heap h 3 , disjoint from h 1 h 2 , such that (h 1 h 2 ) h 3 |= f forky(u) and h 3 |= f KS. Let us make additional observations.

-The only forks in h 1 h 2 h 3 whose endpoints are predecessors of f (u) are those obtained with l 1 → l 2 such that l 1 ∈ dom(h 2 ) (so h 2 (l 1 ) = l 2 ), l 2 ∈ dom(h 1 ), and l 1 → l 2 → l 3 is a knife from h 3 . This is due to (O1) and to the fact that all the predecessors of f (u) in h have no predecessors since f (u) is on the main path of h.

-The number of forks in h 1 h 2 h 3 whose endpoints are predecessors of f (u) is therefore less of equal to card(ran(h 2 ) \ dom(h 1 )). -The number of predecessors of f (u) in h 1 h 2 h 3 is greater or equal to the number of its predecessors in h 1 (by using (O3)). So, if h 1 h 2 h 3 |= f forky(u), then the number of predecessors of f (u) in h 1 is smaller or equal to card(ran(h 2 ) \ dom(h 1 )) = n, i.e. n ≥ m.

Now, let us establish the other direction and let us suppose that n ≥ m and the predecessors of f (u) are p 1 , . . . , p m . Let l 1 1 , l 2 1 , . . . , l 1 n , l 2 n be locations such that {l 1 1 , . . . , l 1 n } = ran(h 2 ) \ dom(h 1 ) and for every i ∈ [1, n], we have h 2 (l 2 i ) = l 1 i . Let us build h 3 so that it satisfies ( †), which is quite easy to realize. Let l new 1 , . . . , l new m be (new) locations that are not in dom(h 1 h 2 ) ∪ ran(h 1 h 2 ). We define h 3 so that it contains exactly m knives whose endpoints are exactly all the predecessors of f (u). For every

i ∈ [1, m], we define h 3 (l new i ) def = l 1 i and h 3 (l 1 i ) def = p i (well, that is possible because l 1 i ∈ dom(h 1 h 2 )). It is easy to check that h 3 satisfies ( †). Consequently, h |= f ¬(KS - * ¬forky(u)) iff n ≥ m.
Now, we are able to state the main proposition of this section that allows us to compare the numbers of predecessors for two locations on the main path of a fishbone heap. Let us introduce the following abbreviations:

ϕ 1 (u, u) def = seg ∧ u = 0 ∧ u = 0, ϕ 2 (u) def = ¬(KS - * ¬forky(u)) and ϕ 3 (u) def = ¬(KS1F - * ¬forky(u)).
PROPOSITION 4.6. Suppose h 1 |= f φ and, f (u) and f (u) are on the main path of h 1 . We have the following equivalences:

-

h 1 |= f ϕ 1 (u, u) - * (ϕ 2 (u) ⇒ ϕ 2 (u)) iff u ≤ u. -h 1 |= f ϕ 1 (u, u) - * (ϕ 2 (u) ⇒ ϕ 3 (u)) iff u ≤ u + 1. -h 1 |= f ϕ 1 (u, u) - * (ϕ 3 (u) ⇒ ϕ 2 (u)) iff u ≤ u -1.
PROOF. By way of example, let us show the second property. The other cases are proved in a similar fashion. Let h 1 be a heap satisfying φ . The statements below are equivalent.

(1) ) in the proof of Lemma 4.5). This is possible by using the fact that one can add a segmented heap so that the resulting heap has n isolated memory cells. Indeed, given the heap

h 1 |= f (ϕ 1 (u, u) - * (ϕ 2 (u) ⇒ ϕ 3 (u)))). (2) For every disjoint heap h 2 such that h 2 |= f ϕ 1 (u, u), if h 1 h 2 |= f ϕ 2 (u), then h 1 h 2 |= f |= ϕ 3 (u). (by definition of |= f ) (3) For every n ≥ 0, there is a disjoint heap h 2 with card(ran(h 2 ) \ dom(h 1 )) = n such that h 2 |= f ϕ 1 (u, u) and if h 1 h 2 |= f ϕ 2 (u), then h 1 h 2 |= f ϕ 3 (u) (see (O4
h 1 , let us build a disjoint heap h 2 such that h 2 |= f ϕ 1 (u, u) and dom(h 2 ) = n for any fixed n ≥ 0. Since X = dom(h 1 ) ∪ ran(h 2 ) ∪ {f (u), f (u)} is a finite subset of N, there are 2n distinct locations l 1 1 , l 2 1 , . . . , l 1 n , l 2 n in N \ X. We simply need to define h 2 such that dom(h 2 ) def = {l 1 1 , . . . , l 1 n }, ran(h 2 ) def = {l 2 1 , . . . , l 2 n } and for all i ∈ [1, n], we set h 2 (l 1 i ) def = l 2 i . (4) for every n ≥ 0, we have n ≥ u in h implies n ≥ u -1 in h. (by Lemma 4.5) (5) u ≤ u + 1.

Constraints between locations at distance three

The goal of this section is the following: given a formula ϕ(u, u) equal to either u = u or u = u + 1 (in particular, this means that ϕ(u, u) only deals with numbers of The formula 1comp was introduced in Section 2.2, and it states that the heap is made of a unique connected component. The way h has to be divided to satisfy the formula is illustrated by the two heaps in the middle of Figure 8. PROOF. Let h be heap such that h |= f dw(α, 2) ∧ ( u +4 ≥ 0) ∧ ( u ≥ α + 3). Let h be the almost u-3cut heap of h and h be the heap such that h = h h . By construction of h , it is easy to check that h

|= f 1comp∧( u +4 = 1)∧¬( u +5 ≥ 0). Similarly, h |= f 1comp. This implies that h |= f 1comp * (1comp ∧ ( u +4 = 1) ∧ ¬( u +5 ≥ 0)).
So, suppose that the almost u-3cut heap of h satisfies:

h |= f φ(u). This means that h |= f 1comp and h |= f (1comp ∧ ( u +4 = 1) ∧ ¬( u +5 ≥ 0) ∧ φ(u)). Hence, h |= f 1comp * (1comp ∧ ( u +4 = 1) ∧ ¬( u +5 ≥ 0) ∧ φ(u)). Now, suppose that h |= f 1comp * (1comp ∧ ( u +4 = 1) ∧ ¬( u +5 ≥ 0) ∧ φ(u)). There are heaps h 1 and h 2 such that h 2 |= 1comp and h 1 |= f (1comp∧( u +4 = 1)∧¬( u +5 ≥ 0)∧φ(u)). In particular, this means that h 1 |= f 1comp ∧ ( u +4 = 1) ∧ ¬( u +5 ≥ 0).
Let us show that there is a unique pair (h 1 , h 2 ) of heaps satisfying that property and

h 1 = h , which will entail that h |= f φ(u). First note that {f (u), h(f (u)), h 2 (f (u)), h 3 (f (u)), h 4 (f (u))} ⊆ dom(h 1 ) h 5 (f (u)) ∈ dom(h 1 )
Since h 1 |= f ( u +4 = 1), all the predecessors of h 4 (f (u)), apart from h 3 (f (u)), are in dom(h 2 ) and there are more than two such predecessors since h 4 (f (u)) is on the main path of h and therefore has at least three predecessors in h.

Hence, h 1 contains also all the ancestors of h 3 (f (u)), otherwise h 2 would have at least two distinct connected components. So, the u-3cut of h is also a subheap of h 1 . Now, it is easy to check that if any location in dom(h ) that is not a predecessor of h 4 (f (u)) were in dom(h 1 ), then h 1 would have more than two connected components. Hence, h 1 is the almost u-3cut heap of h and therefore h |= f φ(u).

Let us build on Lemma 4.8 so as to be able to specify properties on the u-3cut heap. LEMMA 4.9. Let h |= f dw(α, 2) ∧ ( u +4 ≥ 0) ∧ ( u ≥ α + 3)) and φ(u) be the formula

(size = 1) * (¬( u +4 ≥ 0) ∧ φ UC (u)). Then, h |= f 1comp * (1comp ∧ ( u +4 = 1) ∧ ¬( u +5 ≥ 0) ∧ φ(u)) iff the u-3cut of h, say h , satisfies: h |= f φ UC (u).
We write φ AUC (u) to denote the formula 1comp * (1comp∧( u +4 = 1)∧¬( u +5 ≥ 0)∧φ(u)) with φ(u) equal to (size = 1) * (¬( u +4 ≥ 0) ∧ φ UC (u)).

The proof for Lemma 4.9 is also by an easy verification by observing that an almost u-3cut heap is equal to the u-3cut plus one memory cell (see Figure 8).

By combining Lemma 4.7-4.9, we get the following proposition by performing a case analysis depending whether u +4 ≥ 0 holds true or not on the heap h. PROPOSITION 4.10. Let h be a heap and f be an assignment such that h

|= f dw(α, 2) ∧ ( u +3 ≥ 0) ∧ ( u ≥ α + 3)). We have h |= f [u →h 3 (f (u))] ϕ(u, u) iff h |= f ϕ +3 (u) with the formula ϕ +3 (u) defined below: ϕ +3 (u) def = (¬( u +4 ≥ 0) ∧ φ UC (u)) ∨ (( u +4 ≥ 0) ∧ φ AUC (u))
PROOF. We distinguish two cases depending whether h is itself its u-3cut or not.

Case 1: ¬( u +4 ≥ 0), i.e. h is its own u-3cut heap. By Lemma 4.7, if h |= f [u →h 3 (f (u))] ϕ(u, u), then h |= f φ UC (u) and therefore h |= f ϕ +3 (u). Conversely, if h |= f ϕ +3 (u), then h |= f φ UC (u) since ( u +4 ≥ 0) does not hold on h. Again, by Lemma 4.7, we get that h |= f [u →h 3 (f (u))] ϕ(u, u). Case 2: ( u +4 ≥ 0). By Lemma 4.7, if h |= f [u →h 3 (f (u))] ϕ(u, u), then h |= f φ UC (u)
where h is the u-3cut of h. By Lemma 4.9, this implies that h |= f φ AUC (u) and therefore h |= f (i.e., counter C j has non-zero value and we are really dealing with instruction I), then the number of predecessors of h 3 (l) is equal to the number of predecessors of l minus one, which corresponds to encode a decrement on counter C j . Subformulae ( 7) and ( 8) admit a similar reading.

It is now easy to show the following lemma since we have seen that all the constraints between consecutive configurations can be encoded in 1SL2, assuming that the heap encodes a data word in ([1, α] × N 2 ) + . LEMMA 4.11. M has a halting run iff

dw(α, 2) ∧ φ f irst ∧ φ last ∧ I∈[1,α] ϕ I is satisfiable in 1SL2.
Below, we conclude by the main result of the paper. THEOREM 4.12. 1SL2 satisfiability problem is undecidable.

We know that if the number of quantified variables is not restricted, 1SL(- * ) is undecidable too [START_REF] Brochenin | On the Almighty Wand[END_REF]] and recently the satisfiability problem for 1SL2(- * ) has been shown undecidable as well [START_REF] Demri | Expressive completeness of separation logic with two variables and no separating conjunction[END_REF], but this requires a far more complex proof passing via an equivalence to weak second-order logic.

4.6. Note on a variant proof using α≥1 FO2α,1(<, +1, =, ∼, ≺)

As mentioned earlier, there exist many formalisms to specify properties about data words; among them can be found first-order languages. Below, we recall a few standard definitions as well as the main results. Finally, we sketch the proof of a reduction from an undecidable variant of first-order logic on data words into 1SL2. These results show interesting relationships between first-order logics on data words and separation logics.

Let us present the first-order language FO2 α,β (<, +1, =, ∼, ≺) to interpret data words in ([1, α] × N β ) + following developments from [START_REF] Boja Ńczyk | Two-variable logic on data words[END_REF]. Most of the time, a fragment of the full language is needed, but it is helpful to provide the most general definition once and uniformly.

Let FO2 α,β (<, +1, =, ∼, ≺) be the set of formulae defined below:

φ ::= a(v) | v ∼ j v | v ≺ j v | v < v | v = 1 + (v) | v = v | ¬φ | φ ∧ φ | ∃ v φ
-dw |= f a(u i ) def ⇔ a f (ui) = a, -dw |= f u i ∼ j u i def ⇔ d f (ui) j = d f (u i ) j , -dw |= f u i ≺ j u i def ⇔ d f (ui) j < d f (u i ) j , -dw |= f u i = u i def ⇔ f (u i ) = f (u i ), -dw |= f u i = 1 + (u i ) def ⇔ f (u i ) = f (u i ) + 1, -dw |= f u i < u i def ⇔ f (u i ) < f (u i ), -dw |= f ∃ u i φ def ⇔ there is p ∈ [1, L] such that dw |= f [ui →p] φ.
A sentence φ in FO2 α,β (<, +1, =, ∼, ≺) is satisfiable def ⇔ there is a data word dw in ([1, α] × N β ) + such that dw |= φ (no need to specify a variable assignment since φ is closed).

Let us recall major results about FO2 on data words; FO2 α,0 (<, +1, =) was introduced in Section 2.3 and the others just above. Theorem 4.13(IV) shall be used in this section but decidability can be regained, as shown in [START_REF] Th | Two-Variable Logic and Two Order Relations[END_REF], where finite satisfiability of FO2 over data words with a linear order on the positions and a linear order and a corresponding successor relation on the data values shown in EXPSPACE [START_REF] Th | Two-Variable Logic and Two Order Relations[END_REF].

A slightly simpler undecidability proof can be also obtained from the undecidability of the satisfiability problem for α≥1 FO2 α,1 (<, +1, =, ∼, ≺) on data words [START_REF] Boja Ńczyk | Two-variable logic on data words[END_REF]] (see Theorem 4.13(IV)). In order to obtain a reduction from the halting problem for Minsky machines, we had to deal with encoding of instructions, which is a bit tedious in some places but the gain has been to obtain a master reduction. Master reductions are understood as reductions from decision problems involving, for instance, Turing machines, Minsky machines or any other standard class of computational models. These reductions are always preferred because no intermediate decision problems are involved and therefore this limits the sources of flaws for example. Nevertheless, the reduction from the satisfiability problem α≥1 FO2 α,1 (<, +1, =, ∼, ≺) is a bit simpler if undecidability has to be explained in the most concise way.

Let us briefly provide the main ingredients for such a proof. We define a logarithmicspace translation t as follows. A position u in the data word corresponds to a location on the main path of the fishbone encoding the same position but for the (unique) part related to the (unique) datum. In the translation process, we freely use macros defined earlier (i, j ∈ {1, 2}).

t is homomorphic for Boolean connectives, t(u i = u j ) def = u i = u j , t(u i < u j ) def = ls(u i , u j ) ∧ u i = u j , t(u j = 1 + (u i ))

def = * (ls (u i , u j ) ∧ ( u +3 i = 1) ∧ ¬( u +4 i ≥ 0)), -t(a(u i )) def = ∃ u 3-i (u 3-i → u i ) ∧ ( u 3-i = a + 2), -t(u i ∼ 1 u j ) def = u i = u j , -t(u i ≺ 1 u j ) def = u i + 1 ≤ u j , 34 -t(∃ u i φ) def = ∃ u i ( u i ≥ α + 3) ∧ t(φ).
LEMMA 4.14. Let φ be a formula in FO2 α,1 (<, +1, =, ∼, ≺).

(I) For every data word dw in ([1, α] × N) + , dw |= φ iff h dw |= dw(α, 1) ∧ t(φ). (II) Let h be a heap such that h |= dw(α, 1) ∧ t(φ), then there is a data word dw in ([1, α] × N) + such that h and h dw are isomorphic and dw |= φ.

As a corollary, 1SL2 is undecidable, since for any φ in FO2 α,1 (<, +1, =, ∼, ≺), φ is satisfiable iff dw(α, 1) ∧ t(φ) is satisfiable in 1SL2. Note that the gain with the proof sketched above is not that significant; however, we do not need the material from Section 4.4. (Still, though, we need to express arithmetical constraints between the numbers of predecessors.) Furthermore, we need to formally prove Lemma 4.14, which is of a complexity comparable to the material in Section 4.5. Observe also that Section 4.4 is interesting in its own right because it establishes a result about the expressive power of 1SL2 by performing surgical cuts.

CONCLUSION

In the paper, we have shown that two-variable first-order separation logic (1SL2) is undecidable by designing a simple master reduction from the halting problem for Minsky machines and, if we drop the magic wand operator (a fragment called 1SL2( * )), we get decidability but with non-elementary complexity. Our contribution is related to the hardness results when only two variables are used (no program variables, only two quantified variables, no unary predicate symbols). Heavy recycling of variables is done, following the classical result for modal logic [START_REF] Gabbay | Expressive Functional Completeness in Tense Logic[END_REF]]. In order to get these results, we have shown a simple encoding of data words with multiple attributes that is used both for the undecidability and for the non-elementarity result. This nice relationship with data logics [START_REF] Boja Ńczyk | Two-variable logic on data words[END_REF]] is also complemented by the fact that we have shown how to encode propositional interval temporal logic (PITL) [START_REF] Moszkowski | A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time[END_REF]] into 1SL2( * ). Hence, we believe we have established promising bridges between data logic(s), interval temporal logic(s), and separation logic(s), apart from providing additional evidence of the importance of intervals in logics for computer science. Moreover, we have introduced a separation modal logic MLH. While its decidability status remains open, we have proved that its restriction to separating conjunction is decidable with non-elementary complexity. This has been not only an opportunity to better understand the expressive power of separation logic fragments but also to significantly populate 1SL2's inner circle (see Figure 1 for an overview).

Fig. 4 .

 4 Fig.4. A visual depiction of clean and non-clean cuts. Clockwise from left: the original (α, 0)-fishbone heap; a clean cut of the original heap; a non-clean cut of the original heap. Note that clean cuts must result in two (α, 0)-fishbone heaps. A non-clean cut may or may not do so; the figure depicts a non-clean cut that does result in two (α, 0)-fishbone heaps.

Fig. 5 .

 5 Fig. 5. The correspondence between PITL's chop 'C' and separation logic's separating conjunction ' * ' (before and after).

  (⇒) If aw |= φ C ψ, then there are w 1 , w 2 such that chops (aw, w 1 , w 2 ), w 1 |= φ, and w 2 |= ψ. From the definition of chops, we have, further, that there are b, w , w such that aw = w bw , w 1 = w b, and w 2 = bw . Case 1. w = (the chop occurs at the first position). Then aw = bw and w 1 = b = a, so w = w . Since a |= φ and aw |= ψ, we have by IH that ∅ |= t a (φ) and h |= t a (ψ). Then h |= emp ∧ t a (φ) * t a (ψ), so h |= chop3 a , and h |= t a (φ C ψ). Case 2. w = , w = (the chop occurs at the last position). aw = w 1 , so aw |= φ. w 2 = b, so b |= ψ. By IH, we then have h |= t a (φ) and ∅ |= t b (ψ). Thus h |= t a (φ) * emp ∧ t b (ψ). Further, since the last letter of w is b and w ∼ h, the last location on the main path of h must have b + 2 predecessors. Therefore, h |= ∃ u last(u) ∧ u = b + 2. So h |= chop2 a , and thus we have h |= t a (φ C ψ).

  Further, since in h, location l encodes the letter b, it has b + 2 predecessors, so we have h |= f u = b + 2, so h |= chop1 a . Then h |= t a (φ C ψ).

Fig. 7 .

 7 Fig. 7. A segmented heap and collections of knives.

  with v ::= u 1 | u 2 , j ∈ [1, β] and a ∈[1, α]. When β = 0, this implies that there is no atomic formula using ∼ j or ≺ j . We write FO2 α,β (<, +1, =, ∼) to denote the restriction of FO2 α,β (<, +1, =, ∼, ≺) without ≺. Formulae in FO2 α,β (<, +1, =, ∼, ≺) are interpreted over data wordsdw = (a 1 , d 1 1 , . . . , d 1 β ) • • • (a L , d L 1 , . . . , d L β ) in ([1, α] × N β ) + via the satisfaction relation |= f parameterized by f : {u 1 , u 2 } → [1, L](Boolean clauses are omitted, and i, i ∈ {1, 2}):

  The satisfiability problem for α≥1 FO2 α,0 (<, +1, =) is NEXPTIME-complete[START_REF] Etessami | First-Order Logic with Two variables and Unary Temporal logics[END_REF]] (see also [Weis 2011, Corollary 2.2.4]). (II) The satisfiability problem for α≥1 FO2 α,1 (<, +1, =, ∼) is decidable and closely related to the reachability problem for Petri nets [Boja ńczyk et al. 2011; David 2009, Theorem 3]. (III) The satisfiability problem for α≥1 FO2 α,2 (<, +1, =, ∼) is undecidable [Boja ńczyk et al. 2011; David 2009, Proposition 27]. (IV) The satisfiability problem for α≥1 FO2 α,1 (<, +1, =, ∼, ≺) is undecidable [Boja ńczyk et al. 2011; David 2009].

  ). (⇒) aw |= ¬φ, so aw |= φ. By IH, h |= t a (φ), so h |= ¬t a (φ) and precisely ¬t a (φ) = t a (¬φ). (⇐) h |= ¬t a (φ), so h |= t a (φ). By IH, aw |= φ, so aw |= ¬φ. t a (φ ∧ ψ). (⇒) aw |= φ ∧ ψ, so aw |= φ and aw |= ψ. By IH, h |= t a (φ) and h |= t a (ψ), so then h |= t a (φ) ∧ t a (ψ). We have h |= t a (φ ∧ ψ). (⇐) h |= t a (φ ∧ ψ), so h |= t a (φ) ∧ t a (ψ). Then h |= t a (φ) and h |= t a (ψ). By IH, aw |= φ and aw |= ψ, so aw |= φ ∧ ψ. t a (φ C ψ).

We thank Ben Moszkowski for pointing us to this work.

We thank Ben Moszkowski for pointing us to this fact.

ACKNOWLEDGMENT

We would like to thank Emanuel Kiero ński, Ben Moszkowski, and Guido Sciavicco. for insightful exchanges about interval temporal logics and two-variable first-order logic(s). Furthermore, we are indebted to two anonymous referees for many helpful and insightful suggestions that helped us to improve the quality of this manuscript.

Work partially supported by the EU Seventh Framework Programme under grant agreement No. PIOF-GA-2011-301166 (DATAVERIF), the Air Force Office of Scientific Research (under award FA9550-09-1-0596), and the National Science Foundation (under grant 0644299). Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that

predecessors and Section 4.3 explains how to define these formulae in 1SL2), we show how to define a formula in 1SL2, say ϕ +3 (u), such that

assuming that h 3 (f (u)) is defined and h |= f dw(α, 2) ∧ ( u ≥ α + 3)). When ϕ(u, u) is equal to u = u [resp. u = u + 1], we write u = u +3 [resp. u = u +3 + 1] instead of ϕ +3 (u). Note that if we had three quantified variables, defining ϕ +3 (u) would not require much work since the formula below does the job:

Let us start our construction. To do so, let h be a heap and f be an assignment such that h |= f dw(α, 2) ∧ ( u +3 ≥ 0) ∧ ( u ≥ α + 3)). In the statements below, this property is always satisfied.

The u-3cut of h is the minimal subheap h 3cut of h (with respect to set inclusion of the domain) such that all the ancestors of l = h 3 (f (u)) in dom(h) are also ancestors of l in h 3cut . It looks like a clean cut from Section 3 but operated on h 3 (f (u)) and on an (α, 2)fishbone heap. As a consequence, f (u) and l have the same amount of predecessors in h and in the u-3cut heap. Moreover, if f (u) has more than α + 3 predecessors, then the u-3cut of h is also a (α, 2)-fishbone heap.

In Figure 8, the bottom left heap is the u-3cut of the heap at the top. When h |= f u +4 ≥ 0, the almost u-3cut of h is the minimal subheap of h containing the u-3cut heap and such that u +4 = 1 holds true. The almost u-3cut of h contains the edge from l which is the only predecessor of the interpretation of u +4 . In Figure 8, the middle left heap is the almost u-3cut of the heap at the top. Below, we explain how to obtain the u-3cut of some heap, possibly via the construction of the almost u-3cut, if it exists.

Lemma 4.7 below states that all we need to define ϕ +3 (u) is to be able to express a property in its u-3cut. In particular, the only location that is unallocated and on the main path is

PROOF. Let l = h 3 (f (u)) and l = f (u). Let h be the u-3cut heap of h. We have ( †) l in h is equal to l in h and l in h is equal to l in h . Indeed, the u-3cut heap h is a subheap of h such that all the ancestors of l in h are also ancestors of l in h and l is an ancestor of l in h. Note also that l is the unique location such that h

. Note that we use the fact that ϕ(u, u) specifies a property about the numbers of predecessors.

When h is equal to its u-3cut, i.e. when ( u +4 ≥ 0) does not hold, we have

Now, let us consider the case when h is not equal to its u-3cut (probably, the most common situation) and let us show how to separate the current heap so that we can isolate the u-3cut heap. ϕ +3 (u) (thanks to its second disjunction). Conversely, if h |= f ϕ +3 (u), then h |= f φ AUC (u) since ( u +4 ≥ 0) holds on h. Again, by Lemma 4.9, we get that h |= f [u →h 3 (f (u))] φ UC (u) and by Lemma 4.7, we conclude h |= f [u →h 3 (f (u))] ϕ(u, u).

Note that the reasoning performed in this section cannot be extended to an arbitrary formula ϕ(u, u) since taking a u-3cut or an almost u-3cut preserves the number of predecessors of f (u) and h 3 (f (u)) but may not preserve more general properties. Nevertheless, this is sufficient for our needs in Section 4.5.

Master reduction from halting problem for Minsky machines

We shall use formulae of the form ϕ +3 (u) when ϕ(u, u) expresses one of the following arithmetical constraints: u = u, u = u + 1 and u = u + 1 (see Section 4.4). For each instruction I ∈ [1, α -1], we build a formula φ I so that the Minsky machine M halts iff the formula φ ∧ I∈[1,α-1] ϕ I is satisfiable in 1SL2. It remains to define ϕ I for each instruction I.

If instruction I is of the form "I: C j := C j + 1; goto J" then we need to check the following properties:

(1) If a location l encodes the instruction I on the main path (i.e. l = I + 2) and h 3 (l) is defined, then the location h 3 (l) encodes the instruction J.

(2) If a location l encodes the value for the counter C j in a configuration with instruction I (i.e., l ≥ α + 3 and the jth ancestor of l has I + 2 predecessors) and h 3 (l) is defined, then l + 1 = h 3 (l).

(3) Similarly, if a location l encodes the value for the counter C 3-j (i.e., the counter C 3-J is not updated after instruction I) in a configuration with instruction I (i.e., l ≥ α + 3 and the jth ancestor of l has I + 2 predecessors) and h 3 (l) is defined, then

The properties can be expressed by the formula ϕ I below:

Each subformula decorated by a curly bracket with (i) expresses exactly the property (i) above. Note that u +3 = J + 2 states that the number of predecessors of h 3 (f (u)) is J + 2, which is quite easy to express in 1SL2 (see Section 2.2). By contrast, the formula u = u +3 -1 states that the number of predecessors of h 3 (f (u)) is equal to the number of predecessors of f (u) plus one, which requires the more sophisticated formulae introduced in Section 4.3 and in Section 4.4.

Similarly, let I be the instruction "I: if C j = 0 then goto J 1 else (C j := C j -1; goto J 2 )" then ϕ I is defined as follows:

The subformula decorated by a curly bracket with (4) states that a location l encodes the instruction I and h j (l) has α + 3 predecessors (i.e., counter C j has value zero), then the location h 3 (l) has J 1 +2 predecessors (i.e., the next instruction is J 1 ). Similarly, the subformula decorated by a curly bracket with (5) states that if a location l encodes the instruction I and h j (l) has strictly more than α+3 predecessors (i.e., counter C j has non-zero value), then the location h 3 (l) has J 2 + 2 predecessors (i.e., the next instruction is J 2 ). Moreover, the subformula decorated by a curly bracket with (6) states that if a location l has at least α + 3 predecessors and its jth ancestor has I + 2 predecessors