Rémi Brochenin

Stephane Demri

Stéphane Demri

Etienne Lozes

Reasoning about sequences of memory states 6

Keywords: separation logic, temporal logic, Büchi automaton, computational complexity

  L'archive ouverte pluridisciplinaire

Introduction

Verification of programs with pointers. Model-checking of infinite-state systems is a very active area of formal verification [START_REF] Burkart | Verification of infinite structures[END_REF] even though in full generality, simple reachability questions are undecidable. Nevertheless, many classes of infinite-state systems can be analyzed, such as Petri nets, timed automata, etc. Programs with pointer variables suffer the same drawback since reachability problems are also undecidable, see e.g. [START_REF] Bardin | Toward symbolic verification of programs handling pointers[END_REF][START_REF] Bouajjani | Programs with lists are counter automata[END_REF]. It is worth noting that specific properties need to be verified for such programs, such as the existence of memory leaks, memory violation, or shape analysis. Prominent logics for analyzing such programs are Separation Logic [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF], pointer assertion logic PAL [START_REF] Jensen | Automatic verification of pointer programs using monadic secondorder logic[END_REF], TVLA [START_REF] Lev-Ami | TVLA: A system for implementing static analyses[END_REF] and alias logic [START_REF] Bozga | On logics of aliasing[END_REF], to quote a few examples.

Towards a temporal separation logic. Since [START_REF] Pnueli | The temporal logic of programs[END_REF], temporal logics are used as languages for formal specification of programs. General and powerful automata-based techniques for verification have been developed, (see for example the works [START_REF] Vardi | Reasoning about infinite computations[END_REF][START_REF] Kupferman | An automata-theoretic approach to branching-time model checking[END_REF]). On the other hand, Separation Logic is a static logic for program annotation [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF], and more recently for symbolic computation [START_REF] Berdine | Symbolic execution with separation logic[END_REF]. Extending the scope of application of Separation Logic to standard temporal logic-based verification techniques has many potential interests. First, it provides a rich underlying assertion language where properties more complex than accessibility can be stated. Second, this may open a new direction of investigation for the purely static Separation Logic extended with general recursion, in the same spirit as [START_REF] Berdine | Shape analysis for composite data structures[END_REF]. For instance, if we write Xx to denote the next value of x (also sometimes written x ′ ), the formula (x ֒→ Xx)U(x ֒→ null), understood on a model with constant heap, characterises the existence of a simple flat list, which is usually written µL(x). x ֒→ null ∨ ∃x ′ .x ֒→ x ′ ∧ L(x ′ ). Third, temporal logics allow to work in the very convenient framework of "programs-as-formulae" and decision procedures for logical problems can be directly used for program verification. For instance, the previous formula can be seen as a program traversing a list and, more generally, programs without destructive updates can be expressed as formulae. Some programs with destructive updates that perform a simple pass on the heap, have an input-output relation that may be described by a formula. For instance, the formula (x ֒→ 0 Xx ∧Xx ֒→ 1 x)Ux ֒→ 0 null roughly expresses that the list in the initial heap h 0 is reversed in the final heap h 1 . Fourth, pointer arithmetic has been poorly studied until now, whereas arithmetical constraints in temporal logics are known to easily lead to undecidability, see e.g. [START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Demri | The effects of bounding syntactic resources on Presburger LTL[END_REF]. Actually, there is a growing interest in understanding the interplay of pointer arithmetic, temporal reasoning, and non aliasing properties.

Our contribution. We introduce a linear-time temporal logic LTL mem to specify sequences of memory states with underlying assertion language based on quantifier-free Separation Logic [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF]. From a logical perspective, the logic LTL mem can be viewed as a many-dimensional logic [START_REF] Gabbay | Many-dimensional modal logics: theory and applications[END_REF] since LTL mem contains a temporal dimension and the spatial dimension for memory states. Other many-dimensional logics can be found in [START_REF] Bennett | Multi-dimensional modal logic as a framework for spatio-temporal reasoning[END_REF][START_REF] Balbiani | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF][START_REF] Gabbay | Many-dimensional modal logics: theory and applications[END_REF][START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF]. Our logic addresses a very general notion of models, including the aspects of pointer arithmetic and recursive structures with records. We distinguish the satisfiability problems from the model-checking problems, as well as distinct subclasses of interesting programs, like for instance the programs without destructive update. The most promising result for future implementation is the pspacecompleteness of the satisfiability problems SAT(CL) and SAT(RF) where CL is the classical fragment without separation connectives and RF is the record fragment with no pointer arithmetic but with separation connectives. This result is very tight, as both propositional LTL and static Separation Logic are already pspace-complete [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF][START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF]. These results are obtained by reduction to the nonemptiness problem for Büchi automata on an alphabet made of symbolic memory states obtained by an abstraction that we show sound and complete, see e.g. [START_REF] Lozes | Expressivité des logiques spatiales[END_REF][START_REF] Calcagno | From separation logic to first-order logic[END_REF]. Such abstractions are similar to resource graphs from [START_REF] Galmiche | Characterizing provability in BI's pointer logic through resource graphs[END_REF][START_REF] Galmiche | Tableaux and resource graphs for separation logic[END_REF]. This is a variant of the automata-based approach introduced in [START_REF] Vardi | Reasoning about infinite computations[END_REF] for plain LTL and further developed with concrete domains of interpretation in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF]. Surprisingly, the abstraction method used to establish these results does not scale to the whole logic, due to a subtle interplay between separation connectives and pointer arithmetic. Moreover, we provide new undecidability results for several problems, for instance SAT ct (LF) (satisfiability with constant heap on the list fragment).

Related work. Previous temporal logics designed for pointer verification include Evolution Temporal Logic [START_REF] Yahav | Verifying temporal heap properties specified via evolution logic[END_REF], based on the three-valued logic abstraction method that made the success of TVLA [START_REF] Lev-Ami | TVLA: A system for implementing static analyses[END_REF], and Navigation temporal logic [START_REF] Distefano | Who is pointing when to whom? on the automated verification of linked list structures[END_REF], based on a tableau method quite similar to our automaton-based reduction. In these works, the assertion language for states is quite rich, as it includes, for instance, list predicate, quantification over adresses, and a freshness predicate. Because of this high expressive power, only incomplete abstractions are proposed, whereas we stick to exact methods. More importantly, our work addresses models with constant heaps and pointer arithmetic, which has not been done so far, and leads to a quite different perspective.

Structure of the paper. We define our logic LTL mem and several fragments and problems in Section 2. Section 3 introduces the symbolic memory states (also useful in Section 4) and presents the pspace-completeness of the satisfiability and model-checking problems for SL with pointer arithmetic. Section 4 is dedicated to the decidability proof of satisfiability for various fragments and its consequences for other problems. In Section 5, we mention several seemingly optimal undecidability results by encoding computations of Minsky machines. Section 6 contains concluding remarks.

This paper is an extended version of [START_REF] Brochenin | Reasoning about sequences of memory states[END_REF].

Memory Model and Specification Language

In this section, we introduce a separation logic dealing with pointer arithmetic and record values, and a temporal logic LTL mem . Unlike BI's pointer logic from [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF], we allow pointer arithmetic. For simplicity, we assume that Val = N ⊎ {nil}. In order to model field selectors, we consider an infinite set Lab of labels. We will usually range over values with u, v, over naturals with i, j, over labels with l, r, next, prev, and over variables with x, y. In the remainder, we will assume a fixed injection (x, i) ∈ Var × N → x, i ∈ Var.

+ i)(l) = s(e) (s, h) |= SL emp iff dom(h) = ∅ (s, h) |= SL A 1 * A 2 iff ∃ h 1 , h 2 s.t. h = h 1 * h 2 , (s, h 1 ) |= SL A 1 and (s, h 2 ) |= SL A 2 (s, h) |= SL A 1 - * A 2 iff for all h ′ , if h ⊥ h ′ and (s, h ′ ) |= SL A 1 then (s, h * h ′ ) |= SL A 2 (s, h) |= SL A 1 ∧ A 2 iff (s, h) |= SL A 1 and (s, h) |= SL A 2 (s, h) |= SL A 1 → A 2 iff (s, h) |= SL A 1 implies (s, h) |= SL A 2 (s, h) |= SL ⊥ never
We use the notation E ⇀ f in F for the set of partial functions from E to F of finite domain, and ⇀ f in+ the set of the ones of non-empty domain. The sets S of stores and H of heaps are then defined as follows:

S def ≡ Var → Val H def ≡ N ⇀ f in (Lab ⇀ f in+ Val).
We will range over a store with s, s ′ and over a heap with h, h ′ , h 1 , h 2 . We call memory state a couple (s, h) ∈ S × H. Hence, a heap can be equivalently understood as a finite subset of N × Lab × Val.

We will refer to the domain of a heap h by dom(h) ⊂ N. Intuitively, in our memory model, each index is thought as an entry point on some record cell containing several fields. Cells are either not allocated, or allocated with some record stored in. In a memory state (s, h), the memory cell at index i is allocated if i ∈ dom(h); in this case the stored record is h

(i) = {l 1 → v 1 , .., l n → v n }.
Note that the size of the information held in a memory cell is neither fixed, nor bounded. Our models could be more concrete considering labels as offsets and relying on pointer arithmetic. However, for our classification of several problems, it will be useful to consider pointer arithmetic independently.

The size of the store s with respect to a finite set of variables X ⊆ Var, written size X (s), is defined as card(X) × max(1 + log(1 + s(x)) : s(x) ∈ N, x ∈ X). Similarly, the size of the heap h with respect to a finite set of labels Y ⊆ Lab, written size Y (h), is defined as card(dom(h

)) × card(Y ) × max(1 + log(1 + h(i)(l)) : i ∈ dom(h), h(i)(l) is defined and h(i)(l) ∈ N).
The size of the memory state (s, h) with respect to X and Y , written size X,Y ((s, h)), is size X (s) + size Y (h).

Separation Logic. We now introduce the separation logic (SL) on top of which we will define our temporal logic. The syntax of the logic is given in Table 1.

In short, Separation logic is about reasoning on disjoint heaps, and we need to define what we mean by "disjoint heaps" in our model. Our level of granularity implies that a record cell cannot be decomposed in disjoint parts. Let h 1 and h 2 be two heaps; we say that h 1 and h 2 are disjoint, noted h 1 ⊥h 2 , if dom(h 1 ) ∩ dom(h 2 ) = ∅. The operation h 1 * h 2 is defined for disjoint heaps as the disjoint union of the two partial functions. Semantics of formulae is defined by the satisfaction relation |= SL (see Table 1). Formulae π are atomic formulae. The formula x + i l ֒→ e states that the value of the field l of the record stored at the address pointed by x with offset i is equal to the value of the expression e. The formula e = e ′ states the equality between the values of the two expressions, and emp means that the current heap has no memory cell allocated. In Table 1 (as well as in the rest of the paper), we assume that a store s is also defined for null with s(null) = nil. In some places, "null" is understood as a distinguished variable whose interpretation is fixed to the value nil ∈ Val \ N.

Formulae A of SL are called state formulae. A formula A * B with the separating conjunction states that A holds on some portion of the memory heap and B holds on a disjoint portion. A formula A- * B states that the current heap, when extended with any disjoint heap verifying A, will verify B. Boolean operators are understood as usual. Derivable connectives A ∨ B and ¬A are defined as usual. In the remainder, we focus on several specific fragments of this separation logic. We say that a formula is in the record fragment (RF) if all its subformulae of the form x + i l ֒→ e use i = 0. In that case, we write x l ֒→ e. We say that a formula is in the classical fragment (CL) if it does not contain any of the connectives * and - * . Finally, we say that a formula is in the list fragment (LF) if it is in the classical fragment and all subformulae x + i l ֒→ e use i = 0 and l = next, and we may simply write x ֒→ e. Clearly, the classical and record fragments are incomparable, while the list fragment is included in both of them.

Let ֒→ null)- * ⊥ is satisfied by (s 0 , h 0 ) whenever there is no heap h 1 with h 1 ⊥h 0 that allocates the variable x to nil on l field. In other words, the variable x is already allocated in the heap h 0 .

As usual, A is valid iff for every memory state (s, h), we have (s, h) |= SL A (written |= SL A). Satisfiability is defined dually: A is satisfiable iff there is a memory state (s, h), such that (s, h) |= SL A.

The size of the state formula A, written |A|, is the length of the string A for some reasonably succinct encoding of variables and integers with a binary representation. We will use the map | • | for other syntactic objects such as LTL mem formulae.

Temporal extension

Memory states sequences. Models of the logic LTL mem are ω-sequences of memory states, which means there are elements in (S × H) ω and they are understood as infinite computations of programs with pointer variables. We range over ρ for a given model, and its i th state ρ(i) will be noted (s i , h i ). In order to analyze computations from programs without destructive update, we shall also consider models with constant heap, that is elements in S ω × H.

The logic LTL mem . Formulae of LTL mem are defined in Table 2. Atomic formulae of LTL mem are state formulae from SL except that variables can be prefixed by the symbol "X". For instance, Xx is interpreted by the value of x at the next memory state. We use the notation X i x for i times X . . . X x (but keep in mind that encoding X i x requires memory space in O(i)). The temporal operators are the standard next-time operator X and until operator U present in LTL, see e.g. [START_REF] Gabbay | On the temporal analysis of fairness[END_REF][START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]. The satisfaction relation ρ, t |= φ, where ρ is a model of LTL mem , t ∈ N and φ is a formula, is also defined in Table 2. We use standard abbreviations such as Fφ for ⊤Uφ or Gφ for ¬F(¬φ). We freely use propositional variables p, q, having in mind that the propositional variable p should be understood as x p = x ⊤ for some fixed extra variables x p , x q , . . . , x ⊤ . In the sequel, given an atomic formula A, we write A[X u x ← x, u ] to denote the SL state formula in which every occurrence of a term of the form X u x is replaced by the variable x, u . Similarly, given a state formula A, we write A[x ← x, 0 ] to denote the state formula in which every occurrence of a variable x is replaced by x, 0 .

Enriched expressions η

::= x | Xη ξ ::= η | null Atomic formulae π ::= ξ = ξ ′ | η + i l ֒→ ξ State formulae A ::= π | emp | A * B | A- * B | A ∧ B | A → B | ⊥ Temporal formulae φ ::= A | Xφ | φUψ | φ ∧ ψ | ¬φ Semantics ρ, t |= Xφ iff ρ, t + 1 |= φ. ρ, t

Programs with pointer variables

In this section, we define the model-checking problems for programs with pointer variables over LTL mem specifications. The set I of instructions used in the programs is defined by the grammar below:

instr ::= x := y | skip | x := y → l | x → l := y | x := cons(l 1 : x 1 , .., l k : x k ) | free x | x := y[i] | x[i] := y | x := malloc(i) | free x, i
The denotational semantics of an instruction instr is defined as a binary relation (S × H) × (S × H) ⊆ instr in order to deal with the nondeterministic allocation of new memory cells. We list in Table 3 the formal denotational semantics of our instruction set. Observe that the instructions x := y[i], x := malloc(i) and x[i] := y deal with the specific label next. Boolean combinations of equalities between expressions are called guards and its set is denoted by G. A program is defined as a triple (Q, δ, q I ) such that Q is a finite set of control states, q I is the initial state and δ is the transition relation, a subset of Q × G × I × Q. We use q g,instr ---→ q ′ to denote a transition. We say that a program is without destructive update if transitions are labeled only with instructions of the form x := y, x := y → l, and x := y[i]. We write P to denote the set of programs and P ct to denote the set of programs without destructive update.

A program is a finite object whose interpretation can be viewed as an infinite-state system. More precisely, given a program p = (Q, δ, q I ), the transition system S p = (S, →) is defined as follows: S = Q × (S × H) (set of configurations) and (q, (s, h)) → (q ′ , (s ′ , h ′ )) iff there is a transition q g,instr ---→ q ′ ∈ δ such that (s, h) |= g and (s ′ , h ′ ) ∈ instr (s, h). Note that S p is not necessarily linear. A computation (or execution) of p is defined as an infinite path in S p starting with control state q I .

Computations of p can be viewed as LTL mem models, using propositional variables to encode the extra information about the control states (details are omitted herein).

Model-checking aims at checking properties expressible in LTL mem along computations of programs. To a logical fragment (SL, CL, RF, or LF), we associate a set of programs : all programs for SL and CL, programs with instructions having i = 0 for RF, and moreover with only the label next for LF. Given one Basic results. Using extended variables Xx, we may express some programs as formulae. This actually holds only for programs without destructive update, for the semantics with constant heap. Intuitively, we express the control of the program with propositional variables, and define a formula that encodes the transitions. As a consequence, the following result can be derived. Lemma 1. Let Frag be a fragment among SL, CL, RF, or LF. There is a logspace reduction from MC ct (Frag) to SAT ct (Frag) (resp. from MC ct init (Frag) to SAT ct init (Frag)).

x := y (s, h) ∋ (s[x → s(y)], h). x := y → l (s, h * {i → {l → v, . . . }}) ∋ (s[x → v], h * {i → {l → v, . . . }}) with s(y) = i x → l := y (s, h * {i → {l → v, . . . }}) ∋ (s, h * {i → {l → s(y), . . . }}) with s(x) = i x := cons(l 1 : x 1 , . . . , l k : x k ) (s, h) ∋ s[x → i], h * {i → {l 1 → s(x 1 ), . . . , l k → s(x k )}} with i ∈ dom(h) free x (s, h * {i → {. . . }}) ∋ (s, h) with s(x) = i skip (s, h) ∋ (s, h) x := y[i] (s, h * {i + i ′ → {next → v}}) ∋ (s[x → v], h * {i + i ′ → {next → v}})) with s(y) = i ′ x[i] := y (s, h * {i ′ + i → {next → v}}) ∋ (s, h * {i ′ + i → {next → s(y)}}) with s(x) = i ′ x := malloc(i) (s, h) ∋ s[x → i ′ ], h * {i ′ → {next → nil}, . . . , i ′ + (i -1) → {next → nil}} with i ′ , . . . , i ′ + (i -1) ∈ dom(h) free x, i (s, h * {i ′ + i → f }) ∋ (s, h) with s(x) = i ′
Proof. We adapt the proof in [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF] for reducing LTL model-checking to LTL satisfiability. To a program p = (Q, δ, q I ), we associate the formula φ p below built over the propositional variables in Q:

q I ∧ G q∈Q (q ⇒ ( q ′ ∈Q\{q} ¬q ′ ∧ τ ∈δ + q φ τ ))
where φ τ expresses that transition τ is fired between the current state and the next state and, δ + q is the set of transitions starting at the state q. In order to define φ τ , we need to translate instructions and guards into the logic (remember that there are limitations on the instructions). We translate instructions of the form

• x := y into Xx = y, • x := y → l into y l ֒→ Xx, • x := y[i] into y + i next ֒→ Xx.
Guards are translated accordingly. It is then standard to show that p |= φ iff φ ∧ φ p is satisfiable.

All the model-checking and satisfiability problems defined in this paper belong to Σ 1 1 in the analytical hierarchy. Indeed, the models and computations of programs can be viewed as functions f : N → N by encoding memory states and configurations by natural numbers (details are tedious). Then, the satisfaction relation between models and LTL mem formulae and the transition relations obtained from programs can be encoded by a first-order formula. This guarantees that these problems are in Σ 1 1 . Additionally, all the problems can easily be shown pspace-hard since they all generalize LTL satisfiability and model-checking [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF].

Discussion

Let us discuss few issues about the expressive power of this logical formalism. First, the interest of modelchecking programs with heap updates stems from early works on automata-based verification. Decision procedures are obtained at the cost of limitations: to define approximations as done in [START_REF] Yahav | Verifying temporal heap properties specified via evolution logic[END_REF][START_REF] Distefano | Who is pointing when to whom? on the automated verification of linked list structures[END_REF] or to restrict the programming language, see e.g. [START_REF] Bardin | From pointer systems to counter systems using shape analysis[END_REF]. However, with this approach, compositionality principles are lost, which is a pity since they made the success of separation logic, as the frame rule and the composition rule.

Second, assuming that the heap is constant is subject to promising developments. Indeed, it is then possible to define spatial operators at the same syntactic level as temporal operators, and write formulae as e.g. [((x ֒→ Xx)U(x ֒→ null))] * (y → null). Observe that this formula does not belong to LTL mem . This might be a way to model modularity in model-checking programs without destructive updates, but there are other points of interest we will try to advocate now.

Recursion with local parameters

The constant heap semantics provides an original viewpoint for recursion with local parameters and local quantification. The design of decision procedures in the presence of general recursive predicates was introduced in [START_REF] Berdine | Shape analysis for composite data structures[END_REF], as well as incomplete methods of inference even though they are apparently good in practice. Complete methods have been proposed for some standard recursive structures like trees, lists, or doubly-linked lists [START_REF] Berdine | Smallfoot: Modular automatic assertion checking with separation logic[END_REF]. But we are not aware of complete methods for a general form of recursive data structures defined on top of Separation Logic, and we believed that our logic could give an alternative way of specifying recursion, although we did not manage to characterize an interesting decidable fragment.

In order to be a bit more precise, let us consider the fragment of recursive separation logic where all recursive formulae are of the form:

(1) µX(x 1 , .., x k ). A(x 1 , .., x k ) ∨ ∃x ′ 1 ..x ′ k . B(x 1 , .., x k , x ′ 1 , .., x ′ k ) ∧ X(x ′ 1 , .., x ′ k )
This fragment is rich enough to express single lists, cyclic lists, and doubly-linked lists. However, we conjecture that it is not expressive enough for trees and DAGs. We conjecture that deciding satisfiability in the fragment of recursive separation logic mentioned above reduces to SAT ct (SL), and the model-checking problem reduces to SAT ct init , considering that (1) can be rewritten as:

B(x 1 , .., x k , Xx 1 , .., Xx k ) U A(x 1 , .., x k ).
In this perspective, our results could arise interesting decidability results for model-checking some of the recursive separation logic with local quantifiers. For satisfiability, we expect to define decidable fragments for SAT ct (SL), for instance considering the techniques for checking temporal properties of so-called flat programs without destructive updates introduced in [START_REF] Finkel | Towards model-checking programs with lists[END_REF]. Another interesting fragment of recursive separation logic is probably the one where recursion is guarded by the separation operator * , but we do not currently see how to treat it in the temporal logic perspective.

Programs as formulae

Let us speculate a bit more. We may take advantage of expressing programs as formulae in order to reduce model-checking to satisfiability, a known approach since [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]. For programs without destructive update, we take advantage of Lemma 1. Moreover, we believe we can extend this result to programs with updates, but with a slightly different perspective. The constant heap semantics can be helpful to define the input-output relation of programs, even with destructive updates, provided some conditions on the way the program read and write over the memory are satisfied. To do so, we consider the extension of LTL mem with two predicates ֒→ 0 and ֒→ 1 instead of the single ֒→, and models are couples of state sequences with constant heap, that is tuples (s i ) i≥0 , h 0 , h 1 . Let us define the input-output relation IO p of a program p as : for all (s 0 , h 0 ), (s 1 , h 1 ), (s 0 , h 0 )IO p (s 1 , h 1 ) if there is a run of p that starts with (s 0 , h 0 ) and ends with (s 1 , h 1 ). Then we conjecture that for an interesting class of programs, this relation is definable in LTL mem extended with ֒→ 0 and ֒→ 1 . Basically, the encoding of the control of the program will be the same as for programs without destructive updates, but the encoding of the instructions will be different. For instance,

x → l := y would be encoded by (Xx) l ֒→ 1 y whereas x := y → l would be encoded as y l ֒→ 0 Xx.

Separation Logic: Complexity and Abstraction

After defining an abstraction for the fragment RF of SL, which will be proved sound, we will be able to decide the complexity of model checking and satisfiability problems for SL.

Syntactic measures

The main approach to get decision procedures to verify infinite-state systems consists of introducing a symbolic representation for infinite sets of configurations. The symbolic representation defined below is motivated by a similar goal and it has similarities with symbolic heaps for Separation Logic in Smallfoot [START_REF] Berdine | Symbolic execution with separation logic[END_REF]. Let us start by some useful definitions. Following [START_REF] Lozes | Expressivité des logiques spatiales[END_REF], we introduce the set of test formulae that are SL formulae of the forms below: • x + i l ֒→ e, e = e ′ (see Table 1 for notations).

• alloc(x + i) def ≡ (x + i next → null)- * ⊥ (x + i is allocated).
Given a formula φ of LTL mem , we define its measure µ φ , understood as pieces of information about the syntactic resources involved in φ. Indeed, forthcoming symbolic states are finite objects parameterized by such syntactic measures. For a state formula A of LTL mem , the size of memory potentially examined by A, written w A , is inductively defined as follows: w A is 1 for atomic formulae, max(w A1 , w A2 ) for A 1 ∧ A 2 or A 1 → A 2 or A 1 - * A 2 , and w A1 + w A2 for A 1 * A 2 . Observe that w A ≤ |A|. Other simple sets about the syntactic resources of A need to be defined: Lab A (∈ P f (Lab)) is the set of labels from Lab occurring in A, Var A (∈ P f (Var)) is the set of variables from Var occurring in A, offsets A (∈ P f (N)) is the set of natural numbers i such that X u x + i l ֒→ e occurs in A, where P f (X) denotes the set of finite subsets of some set X.

Definition 2. A measure µ is defined as a tuple (offsets µ , w µ , Lab µ , Var µ ) ∈ P f (N) × N × P f (Lab) × P f (Var).
The set of measures has a natural lattice structure for the pointwise order, noted below µ ≤ µ ′ . We also write µ[w ← 0] to denote the measure µ except that the second component w is 0. The measure for A, written µ A , is the tuple (offsets A , w A , Lab A , Var A ). The measure of some formula φ of LTL mem , written µ φ , is sup{µ A[X u x← x,u ] : A occurs in φ}. We write size(µ) to denote the size of the measure µ in some reasonable succinct encoding. Definition 3. Given a measure µ = (offsets, w, Lab µ , Var µ ), we write T µ to denote the finite set of test formulae ψ defined as follows:

e ::= x | null f ::= x + i ψ ::= f l ֒→ e | alloc(f ) | e = e ′ | size ≥ k with i ∈ offsets, l ∈ Lab µ , k ∈ [0, w[ and x ∈ Var µ .
Observe that the cardinal of T µ φ is polynomial in |φ|. The variable x, u will be used in subsequent developments to deal with the interpretation of the term X u x in the formulae of the temporal logic. Given a measure µ = (offsets, w, Lab µ , Var µ ) and a memory state (s, h), we write Abs µ (s, h) = {A ∈ T µ : (s, h) |= SL A} to denote the abstraction of (s, h) with respect to µ. Given a measure µ and two memory states (s, h) and (s ′ , h ′ ), we write (s, h)

≃ µ (s ′ , h ′ ) iff Abs µ (s, h) = Abs µ (s ′ , h ′ ), that is, formulae in T µ cannot distinguish the two memory states.
The proof of Lemma 7 below is based on three technical lemmas. Before stating them and proving them, in Lemmas 4-6, we assume that the measure has offsets = {0} since we are dealing with RF. Moreover, we introduce the following definition: (offsets, w, Lab 0 , Var 0 ) + (offsets, w ′ , Lab 0 , Var 0 ) = (offsets, w + w ′ , Lab 0 , Var 0 ). Lemma 4 (Distributivity). Let µ, µ 1 and µ 2 be measures with all sets of offsets equal to {0} and µ = µ 1 + µ 2 . Let (s, h) and (s ′ , h ′ ) be memory states such that (s, h) ≃ µ (s ′ , h ′ ) and, h 1 , h 2 be heaps such that

h = h 1 * h 2 . Then, there exist heaps h ′ 1 and h ′ 2 with h ′ = h ′ 1 * h ′ 2 , (s, h 1 ) ≃ µ1 (s ′ , h ′ 1 ) and (s, h 2 ) ≃ µ2 (s ′ , h ′ 2 ).
Proof. Let (s, h), (s ′ , h ′ ), h 1 , h 2 and µ = (offsets, w, Lab 0 , Var 0 ), µ 1 = (offsets, w 1 , Lab 0 , Var 0 ) and µ 2 = (offsets, w 2 , Lab 0 , Var 0 ) satisfying the hypotheses of the lemma.

We shall define the disjoint heaps h ′ 1 and h ′ 2 by distinguishing the four disjoint sets of values S 1 , S 2 , A 1 and A 2 corresponding to the following sets:

• S 1 = dom(h ′ 1 ) ∩ Im(s ′ ), S 2 = dom(h ′ 2 ) ∩ Im(s ′ ), • A 1 = dom(h ′ 1 ) \ Im(s ′ ), A 2 = dom(h ′ 2 ) \ Im(s ′ ).
Let us first separate dom(h ′ ) ∩ Im(s ′ ) into two parts S 1 and S 2 . We define S i = s ′ (s -1 (dom(h i )) ∩ Var µ ), and we need to show that S 1 , S 2 are disjoint. Let us assume by contradiction that they are not, thus there are some variables x, y ∈ Var µ such that s ′ (x) = s ′ (y) ∈ S 1 ∩ S 2 , and s(x) ∈ dom(h 1 ) whereas s(y) ∈ dom(h 2 ). Since h 1 ⊥h 2 , s(x) = s(y), so s, h |= SL x = y, but s ′ , h ′ |= SL x = y, hence the contradiction. Now, we shall separate the set dom(h ′ )\Im(s ′ ) into two parts A 1 and A 2 . Let B = dom(h)\Im(s), B 1 = dom(h 1 )\Im(s) and B 2 = dom(h 2 )\Im(s). We have card(B 1 )+card(S 1 ) = card(dom(h 1 )) and card(B 2 )+ card(S 2 ) = card(dom(h 2 )). The sets A 1 and A 2 shall contain respectively card(A 1 ) and card(A 2 ) random elements of dom(h ′ ) \ Im(s ′ ) so that card

(A i ) = card(dom(h i )) -card(S i ) if card(dom(h)) < w; otherwise card(A i ) = min(w i , card(dom(h i ))) -card(S i ).
In order to select the elements of A 1 and A 2 , we distinguish different cases depending on card(dom(h 1 )) and card(dom(h 2 )).

Case 1: card(dom(h)) < w. Since (s, h) ≃ µ (s ′ , h ′ ), we have card(dom(h ′ )) = card(dom(h)). Hence, dom(h ′ ) \ Im(s ′ ) can be divided into two parts A 1 , A 2 such that A 1 ⊎ A 2 = dom(h ′ ) \ Im(s ′ ), card(A 1 ) = card(dom(h 1 )) -card(S 1 ) and card(A 2 ) = card(dom(h 2 )) -card(S 2 ). Case 2: card(dom(h)) ≥ w. Consequently card(dom(h ′ )) ≥ w. Case 2.1: card(dom(h 1 )) ≥ w 1 and card(dom(h 2 )) ≥ w 2 . There exist A 1 , A 2 such that A 1 ⊎ A 2 = dom(h ′ ) \ Im(s ′ ), card(A 1 ) = card(dom(h 1 )) -card(S 1 ) ≥ w 1 -card(S 1 ) and card(A 2 ) = card(dom(h 2 )) -card(S 2 ) ≥ w 2 -card(S 2 ).
Case 2.2: For some i ∈ {1, 2}, card(dom(h i )) < w i and card(dom(h

3-i )) ≥ w 3-i . There exist A 1 , A 2 such that A 1 ⊎ A 2 = dom(h ′ ) \ Im(s ′ ), card(A i ) = card(dom(h i )) -card(S i ). Then card(A 3-i ) = card(dom(h 3-i )) -card(S 3-i ) ≥ w 3-i -card(S 3-i ).
The heap h ′ 1 is defined as h ′ |A1∪S1 and the heap h ′ 2 is defined as h ′ |A2∪S2 . Since A 1 , A 2 , S 1 and S 2 are disjoint sets, we have that

A 1 ∪ S 1 and A 2 ∪ S 2 are disjoint. Moreover, A 1 ∪ A 2 ∪ S 1 ∪ S 2 = dom(h ′ ). So h ′ = h ′ 1 * h ′ 2 .
Observe that for i ∈ {1, 2}, we have card(dom

(h i )) ≥ w i iff card(dom(h ′ i )) ≥ w i and, card(dom(h i )) < w i implies card(dom(h i )) = card(dom(h ′ i )). It remains to show that (s, h 1 ) ≃ µ1 (s ′ , h ′ 1 ) and (s, h 2 ) ≃ µ2 (s ′ , h ′ 2 )
. The above considerations about cardinality entail that for all i ∈ {1, 2} and k < w i , we have size

≥ k ∈ Abs µi (s, h i ) iff size ≥ k ∈ Abs µi (s ′ , h ′ i ).
It is also easy to check that for all e = e ′ , alloc(x) ∈ T µi , e = e ′ ∈ Abs µi (s, h i ) iff e = e ′ ∈ Abs µi (s ′ , h ′ i ) and alloc(x) ∈ Abs µi (s, h i ) iff alloc(x) ∈ Abs µi (s ′ , h ′ i ). It remains to consider test formulae of the form x l ֒→ e. The following statements are equivalent:

• x l ֒→ e ∈ Abs µi (s, h i ), • s(x) ∈ N and h i (s(x))(l) = s(e), • s(x) ∈ N ∩ dom(h i ) and h(s(x))(l) = s(e), • s(x) ∈ dom(h i ) ∩ Im(s) and x l ֒→ e ∈ Abs µ (s, h), • s ′ (x) ∈ dom(h ′ i ) ∩ Im(s ′ ) and x l ֒→ e ∈ Abs µ (s ′ , h ′ ), • x l ֒→ e ∈ Abs µi (s ′ , h ′ i ).
In the proof of Lemma 7, we need Lemma 5 below, which is indeed an instance of Lemma 9.

Lemma 5. Let µ be a measure such that offsets µ = {0}. If (s, h) ≃ µ (s ′ , h ′ ), then for all h 0 ⊥h, there is

h ′ 0 ⊥h ′ such that (s, h 0 ) ≃ µ (s ′ , h ′ 0 ).
Lemma 6 (Congruence). Let (s, h 0 ), (s ′ , h ′ 0 ), (s, h 1 ), (s ′ , h ′ 1 ) be memory states such that h 0 ⊥h 1 , h ′ 0 ⊥h ′ 1 . Let µ be a measure such that offsets µ = {0}, and assume that (s, h 0 ) ≃ µ (s ′ , h ′ 0 ) and (s, h 1 ) ≃ µ (s ′ , h ′ 1 ). Then, (s,

h 0 * h 1 ) ≃ µ (s ′ , h ′ 0 * h ′ 1 ).
Proof. Let µ be the measure (offsets, w, Lab µ , Var µ ). We shall show that (s,

h 0 * h 1 ) ≃ µ (s ′ , h ′ 0 * h ′ 1 )
. By symmetry of ≃ µ , it is sufficient to prove that Abs µ (s,

h 0 * h 1 ) ⊆ Abs µ (s ′ , h ′ 0 * h ′ 1 ). Let A ∈ Abs µ (s, h 0 * h 1 )
. We make a case analysis according to A.

• If A = size ≥ k for some k < w, then k ≤ card(dom(h 0 * h 1 )). We want to show that k ≤ card(dom(h ′ 0 * h ′ 1 )) which implies that A ∈ Abs µ (s, h ′ 0 * h ′ 1 ). -If card(dom(h 1 )) ≥ w or card(dom(h 0 )) ≥ w, then card(dom(h ′ 1 )) ≥ w or card(dom(h ′ 0 )) ≥ w, respectively. So card(dom(h ′ 0 * h ′ 1 )) ≥ w and card(dom(h ′ 0 * h ′ 1 )) ≥ k as k < w. -If card(dom(h 1 )) < w and card(dom(h 0 )) < w, then card(dom(h 0 * h 1 )) = card(dom(h 1 )) + card(dom(h 0 )) = card(dom(h ′ 1 )) + card(dom(h ′ 0 )) = card(dom(h ′ 0 * h ′ 1 )). So k ≤ card(dom(h ′ 0 * h ′ 1 )). • If A is e = e ′ , then s(e) = s(e ′ ). Moreover, A ∈ Abs µ (s, h 1 ) iff A ∈ Abs µ (s ′ , h ′ 1 ). Therefore s ′ (e) = s ′ (e ′ ) and A ∈ Abs µ (s ′ , h ′ 0 * h ′ 1 )
.

• If A = x l ֒→ e then (h 0 * h 1 )(s(x))(l) = s(e). Hence, there is i ∈ {0, 1} such that h i (s(x))(l) = s(e). Since (s, h i ) ≃ µ (s ′ , h ′ i ), h ′ i (s ′ (x))(l) = s ′ (e) and (h ′ 0 * h ′ 1 )(s ′ (x))(l) = s ′ (e). So A ∈ Abs µ (s, h ′ 1 * h ′ 0 ). • If A = alloc(x) then s(x) ∈ dom(h 0 * h 1 ). Hence, there is i ∈ {0, 1} such that s(x) ∈ dom(h i ). Since (s, h i ) ≃ µ (s ′ , h ′ i ), s ′ (x) ∈ dom(h ′ i ) and s ′ (x) ∈ dom(h ′ 0 * h ′ 1 ), which entails A ∈ Abs µ (s, h ′ 0 * h ′ 1 )
. 10 Lemma 7 below states that our abstraction is correct for the fragments CL and RF.

Lemma 7 (Soundness of abstraction for SL). Let µ be a measure, (s, h) and (s ′ , h ′ ) be two memory states such that (s, h)

≃ µ (s ′ , h ′ ) [resp. (s, h) ≃ µ[w←0] (s ′ , h ′ )]. For any SL formula A such that µ A µ and A belongs to RF [resp. CL], we have (s, h) |= SL A iff (s ′ , h ′ ) |= SL A.
Proof. The proof of Lemma 7 for the classical fragment is rather straightforward. Indeed, any CL formula is a Boolean combination of test formulae. In order to deal with the record fragment, more efforts are needed. Suppose that (s, h) ≃ µ (s ′ , h ′ ) and A ∈ RF with µ A ≤ µ. By structural induction, we show that (s, h) |= SL A iff (s ′ , h ′ ) |= SL A. The base case when A has one of the forms e = e ′ , f l ֒→ e and emp is by an easy verification. Similarly, in the induction step, the cases when the outermost connective is Boolean are straightforward.

• Assume that (s, h) |= SL A with A = B 1 * B 2 .
verifying h ′ = h ′ 1 * h ′ 2 , (s, h 1 ) ≃ µ1 (s ′ , h ′ 1 ) and (s, h 2 ) ≃ µ2 (s ′ , h ′ 2 )
. By the induction hypothesis, we get

(s ′ , h ′ 1 ) |= SL B 1 and (s ′ , h ′ 2 ) |= SL B 2 . Consequently, (s ′ , h ′ ) |= SL A since h ′ = h ′ 1 * h ′ 2 and A = B 1 * B 2 . • Finally, assume A = B 1 - * B 2 . Let h ′ 1 ⊥h ′ be such that (s ′ , h ′ 1 ) |= SL B 1 . By Lemma 5, there is a heap h 1 such that (s, h 1 ) ≃ µ (s ′ , h ′ 1 )
, h ′ * h ′ 1 ) |= SL B 2 . Hence (s ′ , h ′ ) |= SL B 1 - * B 2 .
Note that we can extend this result to the whole SL by considering test formulae of the form x+i = x ′ +i ′ .

Complexity of reasoning tasks for SL

In this section, we show that model-checking, satisfiability, and validity, for SL, are pspace-complete. We use the abbreviations mc(SL), sat(SL) and val(SL) for the respective problems. These abbreviations are extended to any fragment of separation logic, for instance sat(RF) denotes the satisfiability problem for the record fragment.

pspace-hardness of mc(LF) and sat(LF) is a consequence of [21, Sect. 5.2]. As SL strictly contains LF, this entails the pspace-hardness of mc(SL) and sat(SL). Since SL is closed under negation, pspacecompleteness of val(SL) will follow from pspace-completeness of sat(SL).

In order to show that mc(SL) and sat(SL) are in pspace, we establish the lemmas below. Lemma 8 establishes a reduction from mc(SL) to mc(RF), so that we only need to consider RF in order to find the complexity of model-checking. Then, in Lemma 9, we will provide a small model property for RF, leading to the pspace-easiness of mc(RF) (see Lemma 10). Finally, we characterize the computational complexity of the satisfiability problem thanks to Lemma 12, which entails a reduction from sat(SL) to mc(SL). Lemma 8. There is a logspace reduction from mc(SL) to mc(RF).

Proof. Let t(A) be the formula obtained from A in SL by replacing each occurrence of x + i l ֒→ e by x, i l ֒→ e. The formula t(A) belong to RF. Given a store s, we write t(s) to denote the store such that t(s)( x, i ) = s(x) + i. One can show that for every heap h, we have (s, h) |= SL A iff (t(s), h) |= SL t(A). The proof is by structural induction on A.

We need to establish a quite technical lemma. Given a heap h, let Im 2 (h) be the set of natural numbers i such that there are i ′ and l for which h(i ′ )(l) = i. Lemma 9. Let µ = ({0}, w, Lab µ , Var µ ) be a measure, and l 0 be a label that does not belong to the finite set of labels Lab µ . If (s, h) ≃ µ (s ′ , h ′ ) and h 0 ⊥h is a heap, then there is a heap h ′ 0 such that

• h ′ 0 ⊥ h ′ , • (s, h 0 ) ≃ µ (s ′ , h ′ 0 ), • card(dom(h ′ 0 )) ≤ max(w, card(Var µ )), • max(dom(h ′ 0 ) ∪ Im 2 (h ′ 0 )) ≤ max((s ′ (Var µ ) ∩ N) ∪ dom(h ′ )) + w, • for all n ∈ dom(h ′ 0 ), {l : h ′ 0 (n)(l) is defined} ⊆ Lab µ ⊎ {l 0 }.
The heap h ′ 0 is said to be a small disjoint heap with respect to µ and (s ′ , h ′ ) and it can be represented in polynomial space in size(µ) + size Lab µ (h 0 ) + size Lab µ bis,Labµ ((s ′ , h ′ )).

Proof. Assume that (s, h) ≃ µ (s ′ , h ′ ) and h 0 ⊥h. We introduce two disjoint heaps h 01 and h 02 such that dom(h 01 ) = Im(s) ∩ dom(h 0 ), dom(h 02 ) = dom(h 0 )\Im(s) and h 0 = h 01 * h 02 . We define the heap h ′ 0 as the disjoint union h ′ 01 * h ′ 02 where h ′ 01 and h ′ 02 are defined so as to satisfy dom(h ′ 01 ) = Im(s ′ ) ∩ dom(h ′ 0 ) and dom(h ′ 02 ) = dom(h ′ 0 )\Im(s ′ ). In the sequel, the constant null will be viewed as a distinguished variable always interpreted by nil. We write V to denote the set of "variables" Var µ ∪ {null}.

• In order to define h ′ 01 , let V 1 , . . . , V a be the equivalence classes over the set V for the relation ∼ s defined by x ∼ s y if s(x) = s(y). Since (s, h) ≃ µ (s ′ , h ′ ), the relation ∼ s ′ defines the same set of equivalence classes. For each class V k , let i k be the image of the variables of V through s, and i ′ k through s ′ . Then, for each k ∈ [1, a] and l ∈ dom(h 01 (i k )), the heap h ′ 01 is defined as follows: As announced, we define h ′ 0 as the heap h ′ 01 * h ′ 02 . Let us show that the heap h ′ 0 has all the desired properties.

-if l / ∈ Lab µ , then h ′ 01 (i ′ k )(l 0 ) = nil and h ′ 01 (i ′ k )(l) is undefined, -if l ∈ Lab µ and h 01 (i k )(l) = i n for some n, then h ′ 01 (i ′ k )(l) = i ′ n , -if l ∈ Lab µ and h 01 (i k )(l) = i n for all n, then h ′ 01 (i ′ k )(l) = nil (in that case, nil ∈ {i ′ 1 , . . . , i ′ a }). The domain of h ′ 01 is included in Im(s ′ ), since Im(s ′ |V ) = {i ′ 1 , . . . , i ′ a }. • In order to define h ′ 02 , let b = max(0, min{card(dom(h 02 )), w -card(dom(h 01 ))}) and j ′ 1 , . . . , j ′ b be the b smallest natural numbers disjoint from {i ′ 1 , . . . , i ′ a } ∪ dom(h ′ ).
• Let us check that h ′ ⊥h ′ 0 . First, h ′ ⊥h ′ 01 since h⊥h 01 . Second, h ′ ⊥h ′ 02 by construction. • Let us check that (s, h 0 ) ≃ µ (s ′ , h ′ 0 ). We proceed by a case analysis on the form of the test formulae.

(e = e ′ ) Since (s, h) ≃ µ (s ′ , h ′ ), s(e) = s(e ′ ) iff s ′ (e) = s ′ (e ′ ).

(alloc(x)) We have equivalences between the propositions below:

-alloc(x) ∈ Abs µ (s, h 0 ), -s(x) ∈ dom(h 0 ), -there is k such that x ∈ V k and i k ∈ dom(h 0 ), -there is k such that x ∈ V k and i ′ k ∈ dom(h ′ 01 ), -alloc(x) ∈ Abs µ (s ′ , h ′ 0 ). (size ≥ k) First, observe that card(dom(h 01 )) = card(dom(h ′ 01 )). Moreover, by construction, if card(dom(h 0 )) < w, then card(dom(h 0 )) = card(dom(h ′ 0 )). When card(dom(h 0 )) ≥ w, the con- struction of h ′ 0 guarantees that card(dom(h ′ 0 )) ≥ w. So, for all formulae size ≥ k with k < w, size ≥ k ∈ Abs µ (s, h 0 ) iff size ≥ k ∈ Abs µ (s ′ , h ′ 0 ). (x l ֒→ e)
We have the following implications:

-x l ֒→ e ∈ Abs µ (s, h 0 ), -there is k such that x ∈ V k and h 0 (i k )(l) = s(e), -there are k, k ′ such that h 0 (i k )(l) = i k ′ , function MC((s, h), A, µ) (base-cases) If A is atomic, then return (s, h) |= SL A; (Boolean-cases) If A = A 1 ∧ A 2 ,
-there are k, k ′ such that x ∈ V k and h ′ 01 (i ′ k )(l) = i ′ k ′ , -x l ֒→ e ∈ Abs µ (s ′ , h ′ 0 ).

Now suppose that not x

l ֒→ e ∈ Abs µ (s, h 0 ). We distinguish 3 cases.

1. s(x) ∈ dom(h 0 ).

From the above case with alloc(x), s ′ (x) ∈ dom(h ′ 0 ) and therefore

x l ֒→ e ∈ Abs µ (s ′ , h ′ 0 ). 2. s(x) ∈ dom(h 0 ) (with i k = s(x)), l ∈ dom(h 0 (i k )) and h 0 (i k )(l) = s(e). If h 0 (i k )(l) = i k ′ for some k ′ ∈ [1, a], then s ′ (e) = i ′ k ′ . If for all k ′ ∈ [1, a], i k ′ = h 0 (i k )(l) (in particular h 0 (i k )(l) = nil), then by construction, h ′ 01 (i ′ k )(l) ∈ {i ′ 1 , . . . , i ′ a }. In both cases, x l ֒→ e ∈ Abs µ (s ′ , h ′ 0 ). 3. s(x) ∈ dom(h 0 ) (with i k = s(x)) and l ∈ dom(h 0 (i k )). Consequently, l ∈ dom(h ′ 0 (i ′ k )) and therefore x l ֒→ e ∈ Abs µ (s ′ , h ′ 0 ).
Therefore (s, h 0 ) and (s ′ , h ′ 0 ) have the same abstraction. • Let us check that card(dom(h ′ 0 )) ≤ max(w, card(Var µ )). We already know that a ≤ card(Var µ ). If card(dom(h ′ 01 )) ≥ w, then h ′ 02 is the empty heap and therefore card(dom(h ′ 0 )) ≤ a. Otherwise, by construction card(dom(h ′ 01 )) + card(dom(h ′ 02 )) ≤ w. Consequently, card(dom(h ′ 0 )) ≤ max(w, card(Var µ )). • Let us check that max(dom(h ′ 0 ) ∪ Im 2 (h ′ 0 )) ≤ max({s ′ (x) : x ∈ Var µ , s ′ (x) ∈ N} ∪ dom(h ′ )) + w. We have chosen the domain and image of h ′ 01 to be included in the image of s ′ plus nil, and therefore dom(h ′ 01 ) satisfies the above condition. The image of h ′ 02 is {nil}. The domain of h ′ 02 is composed of the smallest natural numbers which neither belong to s ′ (Var µ ), nor to dom(h ′ ). As dom(h ′ 02 ) has less than w elements, it is bounded by the w th such natural number, which is bounded by w + max((s ′ (Var µ ) ∩ N) ∪ dom(h ′ )).

• Let us check that for every n ∈ dom(h ′ 0 ), {l :

h ′ 0 (n)(l) is defined} ⊆ Lab µ ⊎ {l 0 }.
This condition is satisfied by construction of h ′ 01 and h ′ 02 .

Lemma 10. mc(RF) is in pspace.

Proof. The algorithm is described in Figure 1. First of all, the algorithm can be implemented in polynomial space since the quantifications are over sets of exponential size in |A| + size Varµ,Labµ ((s, h)) where µ A = (. . . , Lab µ , Var µ ), and the recursion depth is linear in |A|. Hence, all the heaps considered in the algorithm are of polynomial-size in |A| + size Var µ ,Labµ ((s, h)). It remains to be shown that the algorithm is correct: given A with µ A ≤ µ and (s, h) |= SL A iff MC((s, h), A, µ) returns ⊤. The only point to check in the proof by structural induction is the case when the outermost connective is the operator - * . Whenever (s, h) |= SL A 1 - * A 2 , there is a heap h 0 ⊥ h such that (s, h 0 ) |= SL A 1 and (s, h * h 0 ) |= SL A 2 . By Lemma 9 with (s ′ , h ′ ) = (s, h), there is a small disjoint heap h ′ 0 with respect to µ and (s, h) such that (s, h ′ 0 ) ≃ µ (s, h 0 ). Since the measure of A 1 is less than µ, Lemma 7 entails (s,

h ′ 0 ) |= SL A 1 . Moreover, by Lemma 6, (s, h * h ′ 0 ) |= SL A 2 . Consequently, (s, h) |= SL A 1 - * A 2 iff there is a small heap h ′ 0 such that (s, h ′ 0 ) |= SL A 1 and (s, h * h ′ 0 ) |= SL A 2 .
The rest of the section is dedicated to the characterization of the complexity of decision problems for SL. To do so, we need another technical lemma. Given a permutation σ : Val → Val with σ(nil) = nil and a heap h, we write σ • h to denote the partial function which maps i to the partial function σ • (h(i)). When viewing heaps as finite subsets of N × Lab × Val, σ • h is equal to {(i, l, σ(j)) : (i, l, j) ∈ h}. We write σ • h to denote the heap σ • (h • σ -1 ), which corresponds to {(σ(i), l, σ(j)) : (i, l, j) ∈ h}. For instance, given a label l and an address i, we have (σ

• h)(i)(l) = σ(h(σ -1 (i))(l))
. This operation allows us to rename all the addresses according to the permutation: the memory graph keeps the same shape, but vertices are placed on different addresses. We shall use the properties below that can be easily checked:

• For all permutations σ and disjoint heaps h 1 and h

2 , σ • (h 1 * h 2 ) = (σ • h 1 ) * (σ • h 2 ).
• For all permutations σ and heaps h, we have σ

-1 • (σ • h) = h.
Lemma 11. Let A be a state formula of SL with measure µ = (0, offsets, w, Lab µ , Var µ ) and (s, h) be a memory state. For all permutations σ : Val → Val with σ(nil) = nil such that for all x ∈ Var µ and i ∈ offsets, σ(s(x)

+ i) = σ(s(x)) + i, we have (s, h) |= SL A iff (σ • s, σ • h) |= SL A.
Proof. Let A be an SL formula, µ be a measure greater than µ A , s be a store and h be a heap. It is sufficient to show one direction of the equivalence since the other direction is obtained by application of the first one with the store σ • s and the well-defined inverse bijection σ -1 . Indeed, for all x ∈ Var µ ,

σ -1 ((σ • s)(x) + u) = σ -1 ((σ • s)(x)) + u. Assume that (s, h) |= SL A. We show that (σ • s, σ • h) |= SL A.
We are going to prove this by induction on A. The cases with boolean operators are trivial and are omitted herein. If A is an atomic formula, then we proceed by a case analysis.

e = e ′ s(e) = s(e ′ ) iff σ(s(e)) = σ(s(e ′ )) since σ is a bijection on Val.

A is x + i l ֒→ e: h(s(x)+i)(l) = s(e), and σ

•h(σ•s(x)+i)(l) = σ•h(σ -1 (σ(s(x))+i))(l) = σ•h(σ -1 (σ(s(x)+ i)))(l) = σ • h(s(x) + i)(l) = σ(h(s(x) + i)(l)) = σ(s(y)) = σ • s(e), A is emp: dom(σ • h) is empty iff dom(h) is empty. If A = A 1 * A 2 , then there are h 1 and h 2 such that h = h 1 * h 2 and (s, h 1 ) |= SL A 1 and (s, h 2 ) |= SL A 2 .
For each measure µ Ai , we have µ Ai µ A µ. Then, by induction, (σ

• s, σ • h i ) |= SL A i . Since σ • h = σ • (h 1 * h 2 ) = (σ • h 1 ) * (σ • h 2 ), we can conclude that (σ • s, σ • h) |= SL A. If A = A 1 - * A 2 , then let h 0 be a heap which is orthogonal to σ • h. Assume that (σ • s, h 0 ) |= SL A 1 . Then by induction, (σ -1 • (σ • s), σ -1 • h 0 ) |= SL A 1 , that is (s, σ -1 • h 0 ) |= SL A 1 . So (s, h * (σ -1 • h 0 )) |= SL A 2 , and by induction (σ • s, σ • (h * (σ -1 • h 0 ))) |= SL A 2 , that is (σ • s, (σ • h) * (σ • (σ -1 • h 0 ))) |= SL A 2 , and finally (σ • s, (σ • h) * h 0 ) |= SL A 2 . So, (σ • s, σ • h) |= SL A.
We state below a small memory state property that happens to be central to establish the results about the forthcoming pspace upper bounds.

Lemma 12 (Small memory state property). A state formula A in SL is satisfiable iff there is a store s such that (s, ∅) |= SL ¬(A- * ⊥) and for each variable x ∈ Var A , s(x) ≤ (card(Var A ) + 1) × (1 + max(offsets A )), where ∅ stands for the heap with empty domain, Var A is the set of variables occuring in A, and offsets A is the set of indices i such that x + i occurs in A for some variable x. If offsets A is empty, we can replace max(offsets A ) by 0.

Proof. First, it is straightforward to show that A in SL is satisfiable iff there is a store s such that (s, ∅) |= SL ¬(A- * ⊥), where ∅ is the heap with empty domain. So, we only have to prove that given an SL state formula A and a store s such that (s, ∅) |= SL A, there is a store s ′ such that (s ′ , ∅) |= SL A and for each x ∈ Var A , s ′ (x) ≤ (card(Var A ) + 1) × (1 + max(offsets A )) (the interpretation of other variables is irrelevant). In order to obtain this small store, we are going to decrease the value of the variables in several steps. Each step consists of applying a permutation to the memory graph.

Assume that (s, ∅) |= SL A and let MAX = 1 + max(offsets A ). Let x 0 be a dummy variable such that s(x 0 ) = 0, and x 1 , . . . x n be an ordering of the variables occuring in A such that for j ∈ [0, n -1], s(x j ) ≤ s(x j+1 ). If there is no k such that s(x k+1 ) ≥ s(x k ) + MAX, then for all x ∈ Var A , s(x) ≤ (n + 1) × (1 + MAX).

Otherwise, let k be the smallest index such that s(x k+1 ) ≥ s(x k ) + MAX. Let α = s(x k+1 ) -(s(x k ) + MAX). Let us define the permutation σ based on α:

• If j ≤ s(x k ) + MAX then σ(j) = j; • If s(x k+1 ) ≤ j ≤ s(x n ) + MAX, then σ(j) = j -α; • If j ≥ s(x n ) + MAX then σ(j) = j; • If s(x k ) + MAX < j < s(x k+1
) then we have to complete this function so as to obtain a bijection,

σ(j) = j -(s(x k ) + MAX) + (s(x n ) + MAX -α).
Observe that for all x ∈ Var A and i ∈ offsets A , σ(s(x) + i) = σ(s(x)) + i. This permutation satisfies the hypotheses of Lemma 11, and thus may be applied to (s, ∅), which then still satisfies A. We apply this type of permutation until there is no k such that s(x k+1 ) ≥ s(x k ) + MAX. So, by simple multiplication, for all x ∈ Var A , s(x) ≤ (n + 1) × MAX.

Proposition 13. The model-checking, satisfiability, and validity problems for SL are pspace-complete.

Proof. pspace-hardness results are consequences of [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF]Sect. 5.2]. The pspace upper bound for mc(SL) is a consequence of Lemmas 8 and 10. The pspace upper bound for sat(SL) is obtained by enumerating the small memory states of ¬(A- * ⊥) with empty heap (see Lemma 12) and then using Lemma 10.

Decidable fragments of first-order SL can be found in [START_REF] Galmiche | Tableaux and resource graphs for separation logic[END_REF][START_REF] Brochenin | On the almighty wand[END_REF][START_REF] Bansal | Beyond shapes: Lists with ordered data[END_REF].

Decidable Satisfiability Problems by Abstracting Computations

In this section, we establish the pspace-completeness of the problems SAT(CL) and SAT(RF). To do so, we abstract memory states whose size is a priori unbounded by finite symbolic memory states. As usual with linear temporal logic, temporal infinity in models is handled by Büchi automata recognizing ω-sequences. We propose below an abstraction that is correct for CL (allowing pointer arithmetic) and for RF (allowing all operators from Separation Logic) taken separately but that is not exact for the full language SL.

Symbolic models

Definitions. An important aspect of the method consists in defining a symbolic satisfiability relation. Here are the details. Given a measure µ, we write Σ µ to denote the powerset of T µ ; Σ µ is thought of as an alphabet, and elements a ∈ Σ µ are called letters. A symbolic model with respect to µ is defined as an infinite sequence σ ∈ Σ ω µ . Symbolic models are abstractions of models from LTL mem : given a model ρ : N → S × H and a measure µ, we write Abs µ (ρ) : N → Σ µ to denote the symbolic model with respect to µ such that for every

t ∈ N, Abs µ (ρ)(t) def = {A ∈ T µ : ρ, t |= A[ x, u ← X u x]}.
To a letter a, we associate the formula T F [a] = A∈a A ∧ A∈(Tµ\a) ¬A. For all symbolic models σ and formulae φ such that µ φ ≤ µ, we define the symbolic satisfaction relation σ, t |= µ φ as the satisfaction relation for models except for the clause about atomic subformulae is updated as follows:

σ, t |= µ A iff |= SL T F [σ(t)] ⇒ A[X u x ← x, u ].
We write L µ (φ) to denote the set of symbolic models σ with respect to µ such that σ, 0 |= µ φ. As a corollary of Lemma 7, we get a soundness result for our abstraction: Proposition 14. Let φ be a formula of LTL mem (RF) [resp. of LTL mem (CL)] and µ φ ≤ µ. For any model ρ, we have

ρ |= φ iff Abs µ (ρ) |= µ φ [resp. Abs µ[w←0] (ρ) |= µ φ].
Proof. We treat the case φ ∈ LTL mem (RF) (for the case φ ∈ LTL mem (CL), replace below µ by µ[w ← 0]). The induction step for the cases with Boolean and temporal operators is by an easy verification. Let us check the base case, for a state formula. Suppose that ρ, t |= B for an atomic formula B of LTL mem . By definition,

Abs µ (ρ)(t) def = {A ∈ T µ : ρ, t |= A[ x, u ← X u x]}. Let us show that |= SL T F [Abs µ (ρ)(t)] ⇒ B[X u x ← x, u ]. If for some memory state (s, h) |= SL T F [Abs µ (ρ)(t)], then by Lemma 7, (s, h) |= SL B[X u x ← x, u ]. Suppose now that Abs µ (ρ), t |= µ B. Hence, |= SL T F [Abs µ (ρ)(t)] ⇒ B[X u x ← x, u ]. Since ρ, t |= SL T F [Abs µ (ρ)(t)][ x, u ← X u x], we have ρ, t |= (B[X u x ← x, u ])[ x, u ← X u x]. This entails that ρ, t |= B.
Note that Abs µ is not surjective; we note L µ sat the set of symbolic models with respect to µ that are abstractions of some model for LTL mem . Consequently,

φ in LTL mem (RF) is satisfiable iff L µ φ (φ) ∩ L µ φ sat is nonempty.

ω-regularity and pspace upper bound

In order to show that SAT(RF) and SAT(CL) are in pspace we shall explain why testing the nonemptiness of L µ φ (φ) ∩ L µ φ sat can be done in pspace. Below we always treat the case for RF. For CL, replace every occurrence of µ φ by µ φ [w ← 0] and every occurrence of µ by µ[w ← 0]. To do so, we show that each language can be recognized by an exponential-size Büchi automaton satisfying the good properties to establish the pspace upper bound. If A is a Büchi automaton, we note L(A) the language recognized by A. Following [START_REF] Vardi | Reasoning about infinite computations[END_REF][START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF], let A be the generalized Büchi automaton defined by the structure (Σ, Q, δ, I, F ) such that (µ ≥ µ φ ):

• Q is the set of so-called atoms of φ, that are sets of temporal formulae included in the so-called closure set cl(φ) (see [START_REF] Vardi | Reasoning about infinite computations[END_REF]). Let us briefly recall that the closure set cl(φ) is the smallest set containing φ, closed under subformulae, negations (double negations are eliminated) and such that if

ψUψ ′ ∈ cl(φ), then X(ψUψ ′ ) ∈ cl(φ). A set X ⊆ cl (φ)
is an atom whenever it satisfies the usual conditions for subformulae whose outermost connective is Boolean and, we have ψUψ ′ ∈ X iff (ψ ′ ∈ X or (ψ, (ψUψ ′ ) ∈ X)) whenever ψUψ ′ ∈ cl(φ).

• I = {X ∈ Q : φ ∈ X}. • Σ = Σ µ . • X a -→ Y iff 1. for every atomic formula A of X, |= SL T F [a] ⇒ A[X u x ← x, u ]. 2. for every Xφ ′ ∈ cl (φ), Xφ ′ ∈ X iff φ ′ ∈ Y .
• Let {φ 1 Uφ ′ 1 , . . . , φ n Uφ ′ n } be the set of until formulae in cl (φ). Let F be equal to {F 1 , . . . , F n } where

F i = {X ∈ Q : φ i Uφ ′ i ∈ X or φ ′ i ∈ X} for i ∈ {1, . . . , n}. Let A µ
φ be the Büchi automaton equivalent to the generalized Büchi automaton A. It is easy to observe that A µ φ φ has an exponential amount of states in the size of φ and its transition relation can be checked in polynomial space in the size of φ. Moreover,

Lemma 15. Let φ in LTL mem (RF) [resp. LTL mem (CL)] and µ ≥ µ φ [resp. µ[w ← 0] ≥ µ φ [w ← 0]]. Then, L(A µ φ ) = L µ (φ) [resp. L(A µ[w←0] φ ) = L µ[w←0] (φ)].
We can also build a Büchi automaton

A µ sat such that L(A µ sat ) = L µ sat . A µ sat is defined as (Σ, Q, δ, I, F ), where Σ = Σ µ , Q = Σ µ , F = I = Q and a a ′ -→ a ′′ iff: 1. T F [a], T F [a ′′ ] are satisfiable, and a = a ′ , 2. for every formula x, u = x ′ , u ′ ∈ T µ with u, u ′ ≥ 1, x, u = x ′ , u ′ ∈ a iff x, u-1 = x ′ , u ′ -1 ∈ a ′′ , 3. for every formula x, u = null ∈ T µ with u ≥ 1, x, u = null ∈ a iff x, u -1 = null ∈ a ′′ , If µ = µ φ , then A µ
sat is of exponential-size in the size of φ and the transition relation can be checked in polynomial space in the size of φ. More importantly, this automaton recognizes satisfiable symbolic models.

Lemma 16. Let φ in LTL mem (RF) [resp. LTL mem (CL)] and µ = µ φ [resp. µ = µ φ [w ← 0]]. Then, L(A µ sat ) = L µ sat .
Proof. It is immediate that the abstraction of any model with respect to µ belongs to L(A µ sat ). Therefore, the set of abstractions of memory states with respect to µ is included in L(A µ sat ). The other inclusion is shown by induction. Let µ = (offsets, w, Lab 0 , Var 0 ) be the measure µ φ , m be max{u : there is x ∈ Var such that X u x occurs in φ} and MAXI be max(offsets) + 1. Let (a i ) i∈N be an ω-sequence of symbolic memory states in L(A µ sat ). We shall build a sequence (

s i , h i ) i∈N such that Abs µ ((s i , h i ) i∈N ) = (a i ) i∈N . So, for t ∈ N, a t = {A ∈ T µ : ρ, t |= A[ x, u ← X u x]}.
The construction is by induction on the position t ∈ N.

Let us study the base case of the induction that will provide a value for s 0 , . . . , s m , h 0 . Since (

a i ) i∈N ∈ L(A µ sat ), T F [a 0 ] is satisfiable. There are s ′ 0 and h ′ 0 satisfying (s ′ 0 , h ′ 0 ) |= SL T F [a 0 ]
. When dealing with the record fragment (offsets = {0}), the objects are appropriate for the initialization: h 0 = h ′ 0 and for u ∈ [0, m] and x ∈ Var 0 , we set s u (x) = s ′ 0 ( x, u ). When offsets = {0} (w = 0 and we are dealing with the fragment CL), there is no constraint on the size of the heap. We apply a permutation σ which maps all the images of variables to multiples of MAXI. For u ∈ [0, m], we consider the store s u such that for

x ∈ Var 0 , s u (x) = σ(s ′ 0 ( x, u )).
The heap h 0 is defined by enumerating the test formulae x, u +j

l ֒→ x ′ , u ′ ,
x, u + j l ֒→ null and alloc( x, u + j) of a 0 , and by defining the heap accordingly. When x, u + j

l ֒→ x ′ , u ′ ∈ a 0 , h 0 (s u (x) + j)(l) = s u ′ (x ′ ); when x, u + j l ֒→ null ∈ a 0 , h 0 (s u (x) + j)(l)
= nil; when alloc( x, u + j) ∈ a 0 , we define h 0 (s u (x) + j)(l 0 ) = nil, for some l 0 / ∈ Lab 0 . Thanks to the distance MAXI imposed between the values of variables, test formulae about the heap which are not in a 0 are not satisfied. Equalities e = e ′ are preserved since the store has only been modified by a permutation.

For the inductive step, suppose that we have already defined the stores s 0 , . . . , s k+m and heaps h 0 , . . . , h k for some position k ≥ 0 satisfying the conditions below: for every t ≤ k,

• for all A ∈ T µ , (s ⋆ t , h t ) |= SL A iff A ∈ a t , where s ⋆ t : x, u → s t+u (x);

• Im(s ⋆ t ) ⊆ MAXIN ∪ {nil}.
Let us build the store s k+m+1 and the heap h k+1 . Since (a i ) i∈N ∈ L(A µ sat ), T F [a k+1 ] is satisfiable. There exist a memory state (s ′ , h ′ ) satisfying (s ′ , h ′ ) |= SL T F [a k+1 ] and for all x ∈ Var and u ∈ [0, m -1], s ′ ( x, u ) = s k+1+u (x). By definition of A µ sat , ( x, u

+ 1 = x ′ , u ′ + 1 ∈ a k iff x, u = x ′ , u ′ ∈ a k+1 ) and ( x, u + 1 = null ∈ a k iff x, u = null ∈ a k+1 ) for all u, u ′ ∈ [0, m -1]. Consequently, for all u, u ′ ∈ [0, m -1], s k+1+u (x) = s k+1+u ′ (x ′ ) iff s ′ ( x, u ) = s ′ ( x ′ , u ′ ).
So, there is a permutation σ identical for the variables x, u with u ∈ [0, m -1] such that Im(σ • s ′ ) ⊆ MAXIN ∪ {nil}. By construction, for x, u ∈ V µ , σ(s ′ ( x, u )) ∈ MAXIN ∪ {nil}. For x ∈ Var 0 , we set s k+1+m (x) = σ(s ′ ( x, m )).

If we consider RF, this permutation satisfies the prerequisites of Lemma 11, since offsets = {0}. We can define h k+1 = σ • h ′ . Thanks to Lemma 11, we know that both of these models satisfy the same test formulae, which are exactly those in a k+1 .

If we are dealing with CL, then the definition of s k+m+1 ensures that the equalities satisfied are exactly those of a k+1 . This time the prerequisites of Lemma 11 are not satisfied unless offsets = {0}. We know that w = 0, which means that the only test formula about size in a k+1 is size ≥ 0; therefore there is no constraint on the size of the heap. The heap is defined by enumerating the test formulae of the form x, u + j l ֒→ x ′ , u ′ of a k+1 , and defining for each of them h k+1 (s k+1+u (x) + j)(l) = s k+1+u ′ (x ′ ) (idem when x, u + j l ֒→ null ∈ a k+1 , h k+1 (s k+1+u (x) + j)(l) = nil); and then for each of the test formulae of the form alloc( x, u + j) of a k+1 , we define h k+1 (s k+1+u (x) + j)(l 0 ) = nil, for some l 0 / ∈ Lab 0 . Thanks to the distance MAXI between variables, the test formulae about the heap which are not in a k+1 are not satisfied. Equalities e = e ′ are preserved since the store has only been modified by a permutation. This lemma is essential and it is not possible to extend it to the whole logic LTL mem even by allowing test formulae of the form x + i = y + j : we would then need automata with counters. Now, we can state our main complexity result.

Theorem 17. SAT(RF) and SAT(CL) are pspace-complete.

Proof. The lower bound is from LTL [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]. Let φ be an instance formula of SAT(RF) (for SAT(CL) replace below µ φ by µ φ [w ← 0]). As seen earlier, φ is satisfiable iff L

µ φ (φ) ∩ L µ φ sat is nonempty. Hence, φ is satisfiable iff L(A µ φ φ ) ∩ L(A µ φ sat ) = ∅.
The intersection automaton is of exponential size in the size of φ and can be checked nonempty by a nondeterministic on-the-fly algorithm. Since this algorithm, for the nonemptiness problem of Büchi automata, is in nlogspace and the transition relation in the intersection automaton can be checked in polynomial space in the size of φ, we obtain a nondeterministic polynomial space algorithm for testing satisfiability of φ. As usual, by Savitch's theorem, we get the pspace upper bound.

Other problems in pspace

Let Frag be either the classical fragment or the record fragment. Lemma 1 provides a reduction from MC ct init (Frag) to SAT ct init (Frag) based on a program-as-formula encoding. As we will see now, we may also reduce SAT ct init (Frag) to SAT(Frag) internalizing an approximation of the initial memory state which the logical language cannot distinguish from the initial memory state. As a consequence, the pspace upper bound for SAT(Frag) entails the pspace upper bound for both SAT ct init (Frag) and MC ct init (Frag). Proposition 18. Each of the problems SAT ct init (RF), MC ct init (RF), SAT ct init (CL) and MC ct init (CL) is pspacecomplete.

Proof. We begin with the fragment RF. By Lemma 1 and since SAT ct init (RF) is known to be pspace-hard, it remains to establish the pspace upper bound for SAT ct init (RF). Given a formula φ and an initial memory state (s, h), we shall build in polynomial-time a formula φ ct s,h in SAT(RF) such that φ is satisfiable in a model with initial memory state (s, h) and constant heap iff φ ct s,h is satisfiable by a general model. Since we have shown that SAT(RF) is in pspace, this guarantees that SAT ct init (RF) is in pspace. The idea of the proof is to internalize the initial memory state and the fact that the heap is constant in the logic SAT(RF). Actually, we will not exactly express that the heap is constant but the approximation we use will be sufficient for our purpose.

Apart from the variables of φ, the formula φ ct s,h is built over additional variables in V = {x i : i ∈ dom(h) ∪ Im(s)} ∪ {x i,l : i ∈ dom(h), l ∈ dom(h(i))}. The formula φ ct s,h is of the form G(ψ 1 ∧ ψ 2 ∧ ψ 3 ) ∧ ψ s ∧ ψ ′ , where the subformulae are defined as follows.

• ψ 1 states that the heap is almost equal to h since we cannot forbid additional labels in the logical language (dom(h) = {i 1 , . . . , i k }):

ψ 1 def = ( l∈dom(h(i1)) x i1 l → x i1,l ) * . . . * ( l∈dom(h(i k )) x i k l → x i k ,l ).
• ψ 2 states which variables are equal and which ones are not, depending on the initial memory state.

It is a conjunction of simple formulae. As an example, for i = j ∈ dom(h), a simple formula of ψ 2 is x i = x j . Similarly, if h(i)(l) = j and j ∈ dom(h), then x i,l = x j is a simple formula of ψ 2 . Details are omitted.

• ψ 3 states that the additional variables remain constant: x∈V x = Xx.

• The formula ψ ′ is obtained from φ by replacing each occurrence of x l ֒→ e by x l ֒→ e ∧ i∈dom(h),l ∈dom(h(i))

x = x i .

The additional conjunction is useful because our logical language cannot state that a label is not in the domain of some allocated address.

• ψ s states constraints about the initial store s: ψ

s def = x∈φ x = x s(x) .
It is then easy to check that φ is satisfiable by a model with initial memory state (s, h) and constant heap iff φ ct s,h is satisfiable by a general model. As far as the results for the classical fragment are concerned, by Lemma 1, there is a logspace reduction from MC ct init (CL) to SAT ct init (CL) and as done above, one can reduce SAT ct init (CL) to SAT(CL).

Proposition 19. MC ct init (SL) is pspace-complete.

Proof. As MC ct init (RF) is a subproblem of MC ct init (SL), Proposition 18 entails the pspace-hardness. It remains to prove the pspace upper bound. The proof goes by designing a polynomial space reduction to the model-checking problem for propositional LTL. Let (p, s 0 , h 0 , φ) be an instance of MC ct init (RF), where p = (Q, δ, q init ) is a program without destructive updates, (s 0 , h 0 ) is an initial memory state, and φ is a temporal formula in LTL mem (SL). Let Σ be the finite set of stores {s : Im(s) ⊆ Im(s 0 ) ∪ Im(h 0 )} restricted to variables occurring in p and φ. Its cardinality is bounded by (card(Im(s 0 ) ∪ Im(h 0 ))) |φ|+|p| . All the memory states in the transition system S p restricted to the configurations reachable from the initial memory state (s 0 , h 0 ) are in Σ × {h 0 }, since p is without destructive updates.

Let wdw be one plus the maximal natural number j such that X j x appears in φ (size of the window made of consecutive states that need to be considered simultaneously). We define the transition graph

G = (Q G , →, Q init ) such that: Q G = Q × Σ wdw , Q init is
the set of tuples (q init , s 1 , s 2 , .., s wdw ) such that (s 1 , h 0 ), .., (s wdw , h 0 ) is a prefix of a run of p with initial memory state (s 0 , h 0 ), and the transition relation → is defined as follows:

(q, s 1 , .., s wdw ) → (q ′ , s ′ 1 , .., s ′ wdw ) iff s k+1 = s ′ k , k = 1, .., wdw -1, and ∃q g,instr ---→ q ′ ∈ δ such that (s 1 , h 0 ) |= g and (s 2 , h 0 ) ∈ instr (s 1 , h 0 ).
We now define the propositional LTL model by associating to each vertex of the transition graph a set of propositional variables that are true. We define P rop to be the set of atomic formulae occurring in φ, so that φ can be seen as a propositional LTL formula over P rop. Then the LTL model is the vertex-labeled transition graph M = (G, λ), with λ : Q G → P(P rop), (q, s 1 , .., s wdw ) → {A ∈ P rop : s 1 , .., s wdw , h 0 |= SL A}.

By construction, M, (q init , s 1 , s 2 , .., s wdw ) |= φ in LTL for some (q init , s 1 , s 2 , .., s wdw ) ∈ Q init (existential version) if and only if p, (s 0 , h 0 ) |= φ. The model M can be computed in polynomial space in the size of (p, s 0 , h 0 , φ) in the sense that the (nondeterministic) transition function and the labelling function are computable in polynomial space. M has an exponential size in the size of (p, s 0 , h 0 , φ), but let us explain now why the existence of (q init , s 1 , s 2 , .., s wdw ) ∈ Q init such that M, (q init , s 1 , s 2 , .., s wdw ) |= φ can be checked in polynomial space. Let A φ be the automaton recognizing the models of φ over the set P rop of propositions: it has an exponential size in the size of (p, s 0 , h 0 , φ), and so is the product with M . Now the existence of (q init , s 1 , s 2 , .., s wdw ) ∈ Q init such that M, (q init , s 1 , s 2 , .., s wdw ) |= φ reduces to check the non-emptiness of A φ ∩ M , which is decidable in space O(log(|A φ |) + log(|M |)) by a nondeterministic on-the-fly algorithm. The problem can therefore be solved in polynomial space in the size of (p, s 0 , h 0 , φ) by a non-deterministic algorithm, and by Savitch's theorem this can be turned into a deterministic polynomial space algorithm.

Proposition 20. SAT ct init (SL \ {- * }) is pspace-complete.
Proof. pspace-hardness is a consequence of the pspace-hardness of SAT ct init (CL) since CL is a fragment of SL \ {- * }. In order to get the pspace upper bound, we are going to reduce the problem SAT ct init (SL\{- * }) to SAT ct init (RF). Let (s 0 , h), φ be an instance of SAT ct init (SL\{- * }). We shall build an instance (s ′ 0 , h), φ ′ of SAT ct init (RF). Let E = dom(h) ∪ {ki ∈ N : k ∈ dom(h) and X u x + i occurs in φ}. We modify the set Var by adding a new variable var(k) for each k ∈ E, and a variable var(x, i) for all x and i occuring in φ in an expression of the form X u x + i (possibly u or i is equal to zero). These variables do not occur in φ.

i := C i + 1 ; goto l ′ l: if C i = 0 then goto l ′ else C i := C i -1; goto l ′′ .
In a nondeterministic machine, after an incrementation or a decrementation, a nondeterministic choice of the form "goto l 1 or goto l 2 " is performed. The configurations of M are triples (l, c 1 , c 2 ), where l ∈ [1, n] and c 1 , c 2 ≥ 0 are the current values of the location counter and the two counters C 1 and C 2 , respectively. The consecution relation on configurations is defined in the obvious way. A computation of M is a sequence of related configurations, starting with the initial configuration (1, 0, 0). Different encodings of counters are used here as for instance the one in [START_REF] Bardin | From pointer systems to counter systems using shape analysis[END_REF] for which a counter C with value l is represented by a list of length l pointed to by an x dedicated to C. The same idea is used in the proof of Proposition 21 below. In order to show undecidability of SAT(SL), we alternatively encode counters by relying on pointer arithmetic and properties of heaps. Programs without destructive updates can simulate finite computations of Minsky machines on counters bounded by the size of some parts of the heap (the length of a list). In problems with an existential quantification on the initial heap, the maximal value of the counters can be guessed as shown to prove the results below.

Proposition 21. SAT ct (LF) and MC ct (LF) are Σ 0 1 -complete.

Proof. By Proposition 18, SAT ct init (LF) is decidable in polynomial space using a finite abstraction argument. Hence, SAT ct (LF) is in Σ 0 1 by adding an existential quantification over the initial memory state. Similarly, by Proposition 18, MC ct init (LF) is decidable in polynomial space. Hence, MC ct (LF) is also in Σ 0 1 . By Lemma 1, we only need to show that MC ct (LF) is Σ 0 1 -hard. We reduce the Σ 0 1 -complete halting problem for Minsky machines to it. The halting problem consists of determining whether M can reach a configuration with location counter n.

Let us build a formula φ and a program p in P ct such that the existence of some memory state (s 0 , h 0 ) for which p, (s 0 , h 0 ) |= φ is equivalent to the fact that the machine M reaches a configuration with location counter n. In order to encode the values of counters, we consider a variable z pointing to a list (as shown below) in the initial memory state (s 0 , h 0 ):

z next --→ next --→ • • • next --→ next --→ nil
The variable z remains constant along any execution of p and the length of the list is greater than the maximal value of the counters in some finite computation (hopefully ending at the instruction corresponding to location n). We consider also the variables x 1 and x 2 and along any execution of p, each variable x i points to a cell of the above sequence: the length of the list starting at x i encodes the value of the counter C i . Hence, in p, each x i is initialized to null.

The program p is made of the following stages:

1. Check that z points to a list;

2. Initialize the variables;

3. Simulate M .

Figure 2 shows how to perform stage 1 with a simple "while" loop. Observe that checking whether a counter is equal to zero corresponds in p to an equality test with null. In order to simulate M , its structure can be embedded in the control graph of p. For instance, a decrementation instruction is encoded in p by 21 l l ′ l ′′ (x i = null, x i := x i → next) (x i == null, skip) the transitions shown in Figure 3. An incrementation instruction requires a bit more care and its encoding in p is presented in Figure 4. Indeed, auxiliary variables y and y ′ initialized to z visits the list until it meets x i .

In the above encoding, every instruction l in M corresponds to a control state of p. Hence, the formula φ is simply Fn (remember that we may encode propositional variable n by additional variables dedicated only for this purpose, as stated earlier).

It is then easy to show that there is an initial memory state (s 0 , h 0 ) such that p reaches the control n starting with (s 0 , h 0 ) iff the machine M reaches the location counter n. Observe that both p and M are deterministic.

By constrast, programs with destructive update can work with unbounded heaps, and by using the representation of counters as above, they can faithfully simulate a Minsky machine, even if the initial heap is an empty heap, without any bound on the counters. Then, as LTL can express repeated accessibility, Σ 1 1 -hardness can be obtained. Proposition 22. The problems MC(LF) and MC init (LF) are Σ 1 1 -complete. Proof. It is possible to reduce the recurring problem for nondeterministic Minsky machines to MC(LF) and to MC init (LF). This problem is Σ 1 1 -hard [START_REF] Alur | A really temporal logic[END_REF]. The question is whether the machine has a computation with the location counter n repeated infinitely often; and this can be expressed by GFn in LTL mem .

The proof is quite similar to the proof of Proposition 21 except that there is no maximal value of the counters, the initial heap is empty (which can be expressed in LTL mem ), and the behavior of counters is encoded by updating the memory states. For instance, incrementing C i amounts to execute x i := cons(next : x i ) (the length of the list pointed by x i is incremented), decrementing C i amounts to execute x i := x i → next. Zero tests are encoded by null tests and the initial values of the variables is null. Details are omitted since there are no technical difficulties. Now, let us explain how to encode incrementation and decrementation with separating connectives and pointer arithmetic. Observe that expressions of the form x = y + 1 are not allowed in the logical language. We repair this "defect" in two different ways: using non-aliasing expressed by the separating conjunction, and using the precise pointing assertion x next → η stating that the heap contains only one cell, in conjunction with the - * operator. The formulae based on the separating conjunction correctly express incrementation and decrementation when the cells at indices x + 1 and Xx are allocated, whereas formulae based on the operator - * work when the heap is empty. Let SAT ? ? (SL) be any satisfiability problem among the four variants.

Proposition 23. SAT ? ? (SL) is Σ 1 1 -complete.

Proof. We reduce the recurrence problem for nondeterministic Minsky machines [START_REF] Alur | A really temporal logic[END_REF] to SAT ? ? (SL). Let φ 0 be the formula G(emp ∧ 2 i=1 (x i = null)). Incrementation and decrementation are performed thanks to the formulae φ - * x++ and φ - * x--, respectively. For any model ρ such that ρ, 0 |= φ 0 , and for any t, we have ρ, t |= φ - * xi++ iff s t (x i ) + 1 = s t+1 (x i ). Hence, we have a means to encode incrementation. Similarly, ρ, t |= φ - * xi--and s t (x i ) > 0 iff s t (x i ) -1 = s t+1 (x i ). The fact that a counter does not change is encoded by x i = Xx i . Given that φ 1 = G(x zero = Xx zero ∧ x zero = null) holds, zero tests are encoded by x i = x zero .

Given a nondeterministic Minsky machine M , we write ψ l to denote the formula encoding instruction l. For intance for the instruction "l: if C 1 = 0 then goto l ′ else C 1 := C 1 -1; goto l ′ 1 or goto l ′ 2 ," ψ l is equal to the formula below:

G((l ∧ x 1 = x zero ) ⇒ (x 2 = Xx 2 ∧ (Xl ′ 1 ∨ Xl ′ 2 ) ∧ φ - * x1--))∧ G((l ∧ x 1 = x zero ) ⇒ (x 1 = Xx 1 ∧ x 2 = Xx 2 ∧ Xl ′ )).
Finally, let φ 2 be a formula stating that each position corresponds to a unique configuration and the first instruction is 1:

φ 2 = G( l ( l ′ =l (l → ¬l ′ ))) ∧ 1.
Hence, (x 1 = x 2 = x zero ) ∧ φ 0 ∧ φ 1 ∧ ∧ l ψ l ∧ GFn is satisfiable iff M has a computation with instruction n repeated infinitely often.

Proposition 24. The problem SAT(SL \ {- * }) is Σ 1 1 -complete.

The proof of Proposition 24 is similar to the proof of Theorem 23 except that incrementation and decrementation are performed with the formulae φ * x++ and φ * x--respectively, and the heap is not always empty: at each increment or decrement, it has size precisely 1.

Conclusion

In the paper, we have introduced a temporal logic LTL mem for which assertion language is quantifier-free separation logic. Figure 5 shows the reductions between problems. Curved lines represent reductions for proving hardness in a class. Straight lines represent reductions for showing that a problem belongs to its class. Figure 6 contains a summary of the complexity results about fragments of LTL mem .

Finally, extending LTL mem with a special propositional variable heap = stating that the current heap is equal to the next one, can lead to undecidability (look at the problems of the form SAT ct ? (Frag)). However, it is open whether satisfiability becomes decidable if we restrict the interplay between the "until" operator U and heap = , for instance to forbid subformulae of the form G heap = with positive polarity.

  Expressions e ::= x | null Atomic formulae π ::= e = e ′ | x + i l ֒→ e State Formulae A ::= π | A * B | A- * B | emp (spatial fragment) | A ∧ B | A → B | ⊥ (classical fragment) Satisfaction (s, h) |= SL e = e ′ iff s(e) = s(e ′ ) (s, h) |= SL x + i l ֒→ e iff s(x) = nil and h(s(x)

  us illustrate the expressive power on simple examples. The formula ¬emp * ¬emp means that at least two memory cells are allocated. The formula x l → e, defined as ¬(¬emp * ¬emp) ∧ x l ֒→ e, is the local version of x l ֒→ e: (s, h) |= SL x l → e iff dom(h) = {s(x)} and h(s(x))(l) = s(e). The formula (x l

•

  size ≥ k def ≡ k times ¬emp * . . . * ¬emp (at least k indices are allocated).

  Hence, when card(dom(h 01 )) ≥ w, b = 0 and therefore there are no such natural numbers. Otherwise, dom(h ′ 02 ) = {j ′ 1 , . . . , j ′ b } and for each k ∈ [1, b], we define h ′ 02 (j ′ k )(l 0 ) = nil (which is an arbitrary value).

Figure 1 :

 1 Figure 1: Model-checking algorithm

  y := z) (y = null, y := y → next) (y == null, skip)

Figure 2 :

 2 Figure 2: Checking that z points to a list

Figure 3 :Figure 4 :

 34 Figure 3: Simulating a decrementation l l ′ (⊤, y := z) (⊤, y ′ := z) (y ′ = x i , y := y ′ ) (⊤, y ′ := y → next)

  x++ = emp ∧ (Xx next → null)- * x + 1 next → null φ - * x--= emp ∧ (x next → null)- * Xx + 1 next → null

Table 1 :

 1 The syntax and semantics of SL with pointer arithmetic and records

2.1. A separation logic with pointer arithmetic

Memory states. Let us introduce our model of memory. It captures features of programs with pointer variables that use pointer arithmetic and records. We assume a countably infinite set Var of variables (as usual, for a fixed formula we need only a finite amount), and an infinite set Val of values containing the set N of naturals, thought as address indexes, and a special value nil.

  |= φUψ iff there is t 1 ≥ t s.t. ρ, t 1 |= ψ and ρ, t ′ |= φ for all t ′ ∈ [t, t 1 [. ρ, t |= φ ∧ ψ iff ρ, t |= φ and ρ, t |= ψ. ρ, t |= φ → ψ iff ρ, t |= φ implies ρ, t |= ψ.

	ρ, t |= A	iff s ′ t , h t |= SL A[X k x ← x, k ] where ρ = (s t , h t ) t≥0 and
		s ′ t is defined by s ′ t ( x, k ) = s t+k (x).

Table 2 :

 2 The syntax and semantics of LTL mem Given a fragment Frag of SL, such as RF or LF, LTL mem (Frag) is the restriction of LTL mem to formulae in which occur only state formulae built over Frag (with extended variables X u x), and we write SAT(Frag) to denote the satisfiability problem for LTL mem (Frag): given a temporal formula φ in LTL mem (Frag), is there a model ρ such that ρ, 0 |= φ? The variant problem in which we require that the model has a constant heap [resp. that the initial memory state is fixed] is denoted by SAT ct (Frag) [resp. SAT init (Frag)]. The problem SAT ct init (Frag) is defined analogously.

Table 3 :

 3 Semantics for instructionsof these fragments Frag of SL, we write MC(Frag) to denote the model-checking problem for Frag: given a temporal formula φ in LTL mem with state formulae built over Frag and a program p of the associated set of programs, is there an infinite computation ρ of p such that ρ, 0 |= φ (which we write p |= φ)?

	This is the

  There are heaps h 1 and h 2 such that h = h 1 * h 2 , (s 1 , h 1 ) |= SL B 1 and (s 2 , h 2 ) |= SL B 2 . As µ µ A and µ A µ B1 + µ B2 , there are µ 1 and µ 2 such that µ 1 µ B1 , µ 2 µ B2 and µ 1 + µ 2 = µ. By application of Lemma 4, there are heaps h ′ 1 and h ′

	2

  and h 1 ⊥h, and so (s, h 1 ) |= SL B 1 by the induction hypothesis. Then (s, h * h 1 ) |= SL B 2 , and by Lemma 6, (s ′

  then return (MC((s, h), A 1 , µ) and MC((s, h), A 2 , µ)); Other Boolean operators are treated analogously.( * case) IfA = A 1 * A 2 , then return ⊥ if there are no h 1 , h 2 such that h = h 1 * h 2 and MC((s, h 1 ), A 1 , µ)and MC((s, h 2 ), A 2 , µ));(- * case) If A = A 1 - * A 2 , then return ⊥ if for some small disjoint heap h ′ with respect to µ and (s, h) verifying MC((s, h ′ ), A 1 , µ), we have not MC((s, h * h ′ ), A 2 , µ);

	Return ⊤;

Work partially supported by the RNTL project "AVERILES". The first author is supported by a fellowship from CNRS/DGA.

The initial store s ′ 0 is the extension of s 0 which maps var(k) to k, and var(x, i) to s 0 (x) + i. Finally:

s ′ 0 and φ ′ have a polynomial size in the size of the instance (s 0 , h), φ. Assume that (s 0 , h), φ is accepted by SAT ct init (SL\{- * }). Then there is (s i ) i∈N such that (s i , h) i∈N |= φ. Let s ′ i be s i extended so as to map var(k) to k and var(x, j) to s i (x) + j.

) since the value of a variable var(k) is constantly equal to k, and that (s

since for all positions, the value of var(k + i) is that of var(k) plus i and the value of var(x, i) is that of x plus i. So (s ′ i , h) i∈N |= φ ′ , and therefore (s ′ 0 , h), φ ′ is accepted by SAT ct init (RF). Now, assume that (s ′ 0 , h), φ ′ is accepted by SAT ct init (RF). Then there is a sequence (

, and so, at each time state t, we have

We write h ′ ≤ h when there is another heap h ′′ for which h = h ′ * h ′′ . Let us prove by induction on subformulae φ 0 of φ that for all t ∈ N and h ′ ≤ h, we have (

, from which we will conclude that (s 0 , h), φ is also accepted. Indeed, if V 0 is the set of variables occurring in φ, the restriction s ′ 0|V 0 is s 0|V 0 . Here is the proof by induction:

֒→ null is analogous and omitted below).

-Suppose that k / ∈ dom(h). We are going to prove that neither (s

Second, assume there is k ′ ∈ dom(h) such that k ′ = s ′ t+u (x) + i. Thanks to the property (I), from s ′ t+u (x) = k ′i, we get s ′ t+u (var(x, i)) = k ′ , and so k = k ′ ∈ dom(h), which leads to a contradiction. So there is no such k ′ , and not (s

and the same equivalence is true for h ′ 2 . From the two equivalences for h ′ 1 and h ′ 2 , we can conclude the same equivalence for

If we allow the operator - * in the above proposition, the current proof may not be adapted, since we would have to deal with heaps which are not sub-heaps of h in the induction step.

Undecidability Results

In this section, we show several undecidability results by using reduction from problems for Minsky machines. So, first we recall that a Minsky machine M consists of two counters C 1 and C 2 , and a sequence of n ≥ 1 instructions of one of the forms below:

Prop. 21

Theo. 17

pspace-complete problems Σ 0 1 -complete problems