Stéphane Demri

Morgan Deters

final-jancl15 Separation Logics and Modalities: A Survey

Keywords: Separation logic, decidability, computational complexity, expressive power, temporal logic, modal logic, first-order logic, second-order logic

Like modal logic, temporal logic, or description logic, separation logic has become a popular class of logical formalisms in computer science, conceived as assertion languages for Hoarestyle proof systems with the goal to perform automatic program analysis. In a broad sense, separation logic is often understood as a programming language, an assertion language and a family of rules involving Hoare triples. In this survey, we present similarities between separation logic as an assertion language and modal and temporal logics. Moreover, we propose a selection of landmark results about decidability, complexity and expressive power.

Introduction

1.0.0.1 When separation logic joins the club. Introducing new logics is always an uncertain enterprise since there must be sufficient interest to use new formalisms. In spite of this hurdle, we know several recent success stories. For instance, even though a pioneering work on symbolic modal logic by Lewis appeared in 1918 [START_REF] Lewis | A survey of symbolic logic[END_REF], the first monographs on symbolic modal logic appear about fifty years later, see e.g. [START_REF] Hughes | An introduction to modal logic[END_REF]. Nowadays, modal logic is divided into many distinct branches and remains one of the most active research fields in logic and computer science, see e.g. [START_REF]Handbook of modal logic[END_REF]. Additionally, the introduction of temporal logic to computer science, due to Pnueli [START_REF] Pnueli | The temporal logic of programs[END_REF], has been a major step in the development of model-checking techniques, see e.g. [CGP00, BBF + 01]. This is now a well-established approach for the formal verification of computer systems: one models the system to be verified by a mathematical structure (typically a directed graph) and expresses behavioral properties in a logical formalism (typically a temporal logic). Verification by modelchecking [START_REF] Clarke | Model checking[END_REF] consists of developing algorithms whose goal is to verify whether the logical properties are satisfied by the abstract model. The development of tools is done in parallel with the design of techniques to optimize the verification process. Apart from the development of model-checkers such as Cadence SMV, SPIN, or Uppaal, the transfer towards industrial applications is also present in research and development units. The development of description logics for knowledge representation has also followed a successful path, thanks to a permanent interaction between theoretical works, pushing ever further the high complexity and undecidability borders, and more applied works dedicated to the design of new tools and the production of more and more applications, especially in the realm of ontology languages. The wealth of research on description logic is best illustrated by [BCM + 03], in which can be found many chapters on theory, implementations, and applications. By contrast, Chapter 1 of [BCM + 03] provides a gentle introduction to description logics and recalls that its roots can be traced back a few decades. It is well-known that modal logic, temporal logic, and description logic have many similarities even though each family has its own research agenda. For instance, models can be (finite or infinite) graphs, the classes of models range from concrete ones to more abstract ones, and any above-mentioned class includes a wide range of logics and fragments. In this paper, we deal with another class of logics, separation logic, that has been introduced quite recently (see e.g. [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF][START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF]) and is the subject of tremendous interest, leading to many works on theory, tools and applications (mainly for the automatic program analysis). Any resemblance to modal, temporal, or description logic is certainly not purely coincidental-but separation logic also has its own assets.

In the possible-world semantics for modal logic, the modal operator 2 [resp. 3] corresponds to universal [resp. existential] quantification on successor worlds, and these are essential properties to be stated, partly explaining the impact of Kripke's discovery [START_REF] Kripke | A completeness theorem in modal logic[END_REF][START_REF] Copeland | The genesis of possible worlds semantics[END_REF]. Similarly, the ability to divide a model in two disjoint parts happens to be a very natural property and this might explain the success of separation logic in which disjoint memory states can be considered, providing an elegant means to perform local reasoning. Separation is a key concept that has been already introduced in interval temporal logic ITL [START_REF] Moszkowski | Reasoning about digital circuits[END_REF] with the chop operator, and in many other logical formalisms such as in graph logics [START_REF] Dawar | Expressiveness and complexity of graph logic[END_REF] or in extensions of PDL (see e.g. [START_REF] Benevides | Propositional dynamic logic with storing, recovering and parallel composition[END_REF][START_REF] Ph | Decidability and computability in PRSPDL[END_REF]). Moreover, dependence logic has also a built-in notion of separation, see e.g. [START_REF] Abramsky | From IF to BI: a tale of dependence and separation[END_REF][START_REF] Kontinen | Modal independence logic[END_REF][START_REF] Hella | The expressive power of modal dependence logic[END_REF]. Therefore, the development of separation logic can be partly explained by the relevance of the separation concept. Its impressive development can be also justified by the fact that separation logic extends Hoare logic for reasoning about programs with dynamic data structures, meeting also industrial needs as witnessed by the recent acquisition of Monoidics Ltd by Facebook.

1.0.0.2 Separation and composition. Separation logic has been introduced as an extension of Hoare logic [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] to verify programs with mutable data structures [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF][START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF]. A major feature is to be able to reason locally in a modular way, which can be performed thanks to the separating conjunction * that allows one to state properties in disjoint parts of the memory. Moreover, the adjunct implication - * asserts that whenever a fresh heap satisfies a property, its composition with the current heap satisfies another property. This is particularly useful when a piece of code mutates memory locally, and we want to state some property of the entire memory (such as the preservation of data structure invariants). In a sense, if modal logic is made for reasoning about necessity and possibility, separation logic is made for reasoning about separation and composition. No doubt that this type of statement is an oversimplification (apart from the fact that it may appear a bit old-fashioned to most modal logicians) but this may help to get a first picture. As a taste of separation logic, it is worth observing that models can be finite graphs and the classes of models range from concrete ones (with heaps for instance) to very abstract ones (see e.g. cancellative partial commutative monoids in Section 2.4).

Smallfoot was the first implementation to use separation logic, its goal to verify the extent to which proofs and specifications made by hand could be treated automatically [START_REF] Berdine | Smallfoot: Modular automatic assertion checking with separation logic[END_REF]. The automatic part is related to the assertion checking, but the user has to provide preconditions, postconditions, and loop invariants. A major step has been then to show that the method is indeed scalable [YLB + 08]. In a sense, the legitimate question about the practical utility of separation logic was quickly answered, leading to a new generation of tools such as Slayer developed by Microsoft Research, Space Invader [DOY06, YLB + 08], and Infer [START_REF] Calcagno | Infer: An automatic program verifier for memory safety of C programs[END_REF] (see also [START_REF] Sighireanu | Report on SL-COMP[END_REF] for another list of solvers). Actually, nowadays, many tools support separation logic as an assertion language and, more importantly, in order to produce interactive proofs with separation logic, several proof assistants encode the logic, see e.g. [START_REF] Th | A separation logic fragment for HOL[END_REF].

From the very beginning, the theory of separation logic has been an important research thread even if not always related to automatic verification. This is not very surprising since separation logic can be understood as a concretization of the logic BI of bunched implications which is a general logic of resource with a nice proof theory [START_REF] O'hearn | The logic of bunched implications[END_REF]. More precisely, the logic BI exists in different flavours: its intuitionistic version has additive and multiplicative connectives that behave intuitionistically whereas its Boolean version admits Boolean additive connectives with intuitionistic multiplicative connectives ( * and - * ), see more details in [START_REF] Larchey-Wendling | Nondeterministic phase semantics and the undecidability of boolean BI[END_REF]. So, separation logic is rather a concretization of Boolean BI.

Besides, as for modal and temporal logics, the relationships between separation logic, and first-order or second-order logics have been the source of many characterizations and works. This is particularly true since the separating connectives are secondorder in nature, see e.g. [START_REF] Lozes | Expressivité des Logiques Spatiales[END_REF][START_REF] Kuncak | On spatial conjunction as second-order logic[END_REF][START_REF] Calcagno | From separation logic to firstorder logic[END_REF][START_REF] Brochenin | On the almighty wand[END_REF]. For instance, separation logic is equivalent to a Boolean propositional logic [START_REF] Lozes | Separation logic preserves the expressive power of classical logic[END_REF][START_REF] Lozes | Expressivité des Logiques Spatiales[END_REF] if first-order quantifiers are disabled. Similarly, the complexity of satisfiability and model-checking problems for separation logic fragments have been quite studied [COY01, Rey02, CHO + 11, AGH + 14, BFGN14]. In [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF], the model-checking and satisfiability problems for propositional separation logic are shown PSPACE-complete; this is done by proving a small model property.

1.0.0.3 Content of the paper. The goal of this paper is twofold. First, we would like to emphasize the similarities between separation logic and modal and temporal logics. Our intention is to pinpoint the common features in terms of models, proof techniques, motivations, and so forth. Second, we wish to present landmark results about decidability, complexity, and expressive power, providing a survey on the theoretical side of separation logic. These are standard themes for studying logics in computer science and we deliberately focus on the logical aspects for separation logic, providing a wealth of bibliographical references for untouched subjects in the paper, such as the design of verification algorithms for tools using separation logic as an assertion language or the presentation of applications. Because of time and space limitations, we had to focus on core separation logic and for the presentation of the main results we adopt a puristic point of view. Namely, most of the logics • are without data values (by contrast, see e.g. [BDES09, BBL09, MPQ11]),

• use concrete models (by contrast to abstract models considered in [COY07, BK10, LWG10, BV14]), • are not multi-dimensional extensions of non-classical logics (by contrast, see e.g. [YRSW03, BDL09, CG13]), • do not provide general inductive predicates (lists, trees, etc.) (by contrast, see e.g. [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF][START_REF] Brotherston | A decision procedure for satisfiability in separation logic with inductive predicates[END_REF]).

However, these extensions shall be introduced and briefly discussed but we shall refer to original articles or surveys for in-depth developments. In Section 2.2, we introduce the plain version for separation logic and then in the rest of Section 2, we present a few variants with abstract memory models or with data values. Even though these logical formalisms provide a partial view on separation logics, we stick to them in the rest of the paper to present all the results, from decidability to expressive power. First-order separation logic 1SL with one record field plays the role of basic separation logic as modal logic K could play the role of basic modal logic [START_REF] Blackburn | Modal Logic[END_REF]. Section 3 shows connections between separation logics and classical logic augmented with second-order features, weak second-order logic, interval temporal logic ITL [START_REF] Moszkowski | Reasoning about digital circuits[END_REF], modal logic and multi-dimensional modal logics. The concept of separation, made completely explicit in separation logic, happens to be very natural and already present in many logical formalisms such as in interval temporal logics with the chop operator or more recently in separation logic for knowledge representa-tion [START_REF] Herzig | A simple separation logic[END_REF]. Moreover, Section 3 recalls why 1SL and variants can be easily viewed as fragments of weak dyadic second-order logic. Relationships with temporal logics with freeze on data words (see e.g. [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]) are also presented in Section 4.1.4 whereas some analogy with Presburger arithmetic can be found in Section 5.1 (see also in Section 5.2 the relationships between 1SL and first-order theory of natural numbers with addition and multiplication).

Section 4 is dedicated to decidability and complexity results. We present the standard proof techniques for several undecidability results and provide the justification for several decidability ones. Finally, we state several complexity results for tractable fragments but also for fragments with non-recursive elementary complexity. Section 5 presents results about the expressive power for propositional separation logics (such as 1SL0) and for first-order separation logics such as 1SL, known to be as expressive as weak-second-order logic [START_REF] Brochenin | On the almighty wand[END_REF]. Section 6 concludes the technical part of the paper by providing several pointers about proof systems for separation logics, from sequentstyle calculi to decision procedures built on SMT solvers.

Even though our intention is to produce a self-contained document as far as the definitions and results are concerned, we invite the reader to consult surveys on formal verification and separation logic, see e.g., the primer on separation logic in [O'H12], the lecture notes about Hoare logic and separation logic in [START_REF] Gordon | Hoare Logic. Lecture notes[END_REF] or [Jen13a, Chapter 7] and [START_REF] Jensen | Techniques for model construction in separation logic[END_REF].

Separation Logics

Basics on separation logic and formal verification

In this section, we provide a brief introduction to separation logic by showing how it is related to formal verification. Nevertheless, later sections give a precise definition and focus on the logical language rather than on the verification process. This means that we adopt a restrictive use of the term 'separation logic' which is understood as an assertion logic, rather than an understanding combining in some way the assertion logic, the programming language and/or the specification logic.

Hoare logic

Hoare logic, proposed in 1969 by Tony Hoare [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] and inspired by the earlier work of Floyd [START_REF] Floyd | Assigning meanings to programs[END_REF], is a formal system used to show the correctness of programs. Its hallmark, the Hoare triple, is composed of assertions φ and ψ and command C:

{φ} C {ψ}
Simply put, such a triple means that given a program state where the precondition φ holds, the execution of C yields a state in which the postcondition ψ holds. Two commands can be composed:

{φ} C 1 {ψ} {ψ} C 2 {ϕ} {φ} C 1 ; C 2 {ϕ} composition
Preconditions can be strengthened and postconditions can be weakened in a natural fashion (this is used later in Section 4.3.1):

φ ⇒ φ {φ } C {ψ} ψ ⇒ ψ {φ} C {ψ } strengthen/weaken
The expression φ ⇒ φ can be read as φ entails φ , which amounts to state the logical validity of the formula φ ⇒ φ , when defined in a first-order dialect. An assignment axiom schema is stated simply: {φ[x/e]} x := e {φ} assignment

However, this has a severe limitation when pointers are involved. Consider the following triple, an instance of the above schema:

{y = 1} x := 2 {y = 1}
This essentially states that an assignment of 2 to x does not affect the value of y (if it is 1). With many popular imperative programming languages, this is not the case, as x and y may in fact be aliased, i.e., they may refer to the same or a partially-overlapping region of computer memory. Naturally, this was understood early on as a limitation, and aliasing has continued to plague program analysis in the decades since. However, the simplicity and composability of Hoare's proposal was appreciated, and various ways of overcoming this limitation within Hoare's formalism have been sought. Many of these approaches have used some form of separation, by which distinct parts of memory can be reasoned about distinctly.

Birth of separation logic

Burstall introduced distinct nonrepeating tree systems in 1972 [START_REF] Burstall | Some techniques for proving correctness of programs which alter data structures[END_REF], implicitly appealing to a notion of separation to be later enshrined in separation logic. There were, however, limitations of Burstall's approach (see [START_REF] Reynolds | Intuitionistic reasoning about shared mutable data structure[END_REF] for a full treatment). Fragments of data structures could be asserted as separate, and this invention was important; however, they were not permitted to have internal sharing. This has the effect that the assertion language is limited in its ability to distinguish structures with (unbounded) sharing. Further, the notion of composition was directional, so that mutually-referential data posed a problem.

Recognizing these limitations, Reynolds introduced the notion of an "independent conjunction" to Hoare logic, capable of speaking of disjoint structures and thus maintaining some control in the face of the aliasing problem. Its first incarnation, interpreted classically, was flawed, as it assumed monotonicity of interpretations of assertions in extensions of memory states but included an unsound proof rule. This was quickly repaired by coopting an intuitionistic semantics [START_REF] Reynolds | Intuitionistic reasoning about shared mutable data structure[END_REF].

This intuitionistic version was discovered independently by Ishtiaq and O'Hearn [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF]. In fact, their efforts (together with Pym) on bunched implication (BI) logics [START_REF] O'hearn | The logic of bunched implications[END_REF][START_REF] Pym | The Semantics and Proof Theory of the Logic of Bunched Implications[END_REF] gave them a somewhat more general perspective, and they recognized Reynolds' assertion language as being an instance of bunched implication that reasons about pointers. Independently, working from Reynolds' earlier classical variant, they developed a version of BI that used Reynolds' independent conjunction, and gave it intuitionistic semantics. Afterward, they considered a classical version, but ended up presenting these in reverse, the intuitionistic as a variant of the classical; this as a result of the fact that the intuitionistic can be translated into the classical version, and the classical version was useful in reasoning about pointer disposal.

Their paper made two further important contributions. First, they introduced separating implication (the "magic wand") to the logic (this quite naturally came from BI's multiplicative implication). This addition of the magic wand was not merely an afterthought or side effect of the instantiation of bunched implication in this "pointer February 9, 2015 Journal of Applied Non-Classical Logics final-jancl15 logic" setting; indeed its addition was justified in its own right when first introduced [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF]. Despite this, many verification applications have made use of the separating conjunction only and do not employ the magic wand. However, nowadays its use in verification is more recognized; see [LP14, Section 1] and [HCGT14, Section 8] for recent discussions on this topic (see also [START_REF] Thakur | Satisfiability modulo abstraction for separation logic with linked lists[END_REF]).

Second, they introduced the frame rule, important for local reasoning [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF]. Given a Hoare triple {φ} C {ψ} and reasoning about partial computer memories satisfying φ and ψ, one can make conclusions about (disjoint) extensions of those partial memories and, in particular, about how these extensions are unaltered by C. This is at the core of the scalability of separation logic and its ability to handle aliasing. It will be made precise later, after suitable formal definitions have been made.

In all these early versions of separation logic, memory locations were distinct from the integers. Reynolds later offered an extension that takes memory locations to be a (countably infinite) subset of the integers, and made fields of larger units independently addressable. His goal was to adequately model the low-level operation of code and, particularly, address arithmetic. In this paper, we adopt such a convention: memory locations are integers. We also adopt modern syntax; before 2002, Reynolds used '&' for separating conjunction. The modern syntax is ' * ' for separating conjunction and '- * ' for the separating implication, both taken from bunched implication logic.

Separation logic on concrete models

Let us start by defining separation logics on concrete models, namely on heaps. Let PVAR = {x 1 , x 2 , . . .} be a countably infinite set of program variables and FVAR = {u 1 , u 2 , . . .} be a countably infinite set of quantified variables. A memory state is a pair (s, h) such that • s is a variable valuation of the form s : PVAR → N (the store),

• A heap with k ≥ 1 record fields is a partial function h : N N k with finite domain. We write dom(h) to denote its domain and ran(h) to denote its range.

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]. Herein, sometime, there is no need for program variables (with a store) because we establish hardness results without the help of such program variables. Moreover, for the sake of simplicity, we do not make a distinction between the set of locations (domain of h) and the set of values (set of elements from the range of h).

Two heaps h 1 and h 2 are said to be disjoint, noted h 1 ⊥h 2 , if their domains are disjoint; when this holds, we write h 1 h 2 to denote the heap corresponding to the disjoint union of the graphs of h 1 and h 2 , hence dom(h 1 h 2 ) = dom(h 1 ) dom(h 2 ). When the domains of h 1 and h 2 are not disjoint, the composition h 1 h 2 is not defined even if h 1 and h 2 have the same values on dom(h 1 ) ∩ dom(h 2 ). Moreover, we can also define the disjoint union of the memory states (s 1 , h 1 ) and (s 2 , h 2 ) when s 1 = s 2 and h 1 ⊥h 2 so that (s

1 , h 1 ) (s 2 , h 2 ) def = (s 1 , h 1 h 2 ).
In Figure 1, we illustrate how disjoint memory states are built when there is a unique record field while recalling a standard graphical representation. Each node represents a distinct natural number (the value is not specified in Figure 1) and each edge l → l encodes the fact that h(l) = l , assuming that h is the heap graphically represented. A variable x i just above a node means that its value by the store s is precisely that node. In Figure 1, the heap on the left of the equality sign (say h) is equal to the disjoint union of the two heaps on the right of the equality sign (say h 1 , h 2 from left to right). For example, the self-loop on the node labelled by x 3 encodes that (s, h) |= x 3 → x 3 . Similarly, (s,

h 1 ) |= x 3 → x 3 but not (s, h 2 ) |= x 3 → x 3 . x 1 x 2 x 3 x 4 = x 1 x 2 x 3 x 4 x 1 x 2 x 3 x 4
= π | φ ∧ ψ | ¬φ | φ * ψ | φ - * ψ | ∃ u φ
where u ∈ FVAR. The connective * is separating conjunction and - * is separating implication, usually called the magic wand. We make use of standard notations for derived connectives for this and all logics defined in this paper. As in classical first-order logic, an assignment is a map f : FVAR → N. The satisfaction relation |= is parameterized by assignments (obvious clauses for Boolean connectives are omitted):

• (s, h) |= f emp iff dom(h) = ∅. • (s, h) |= f e = e iff
• (s, h) |= f φ 1 * φ 2 iff h = h 1 h 2 , (s, h 1 ) |= f φ 1 , (s, h 2 ) |= f φ 2 for some h 1 , h 2 . • (s, h) |= f φ 1 - * φ 2 iff for all h , if h ⊥ h and (s, h ) |= f φ 1 then (s, h h ) |= f φ 2 . • (s, h) |= f ∃ u φ iff there is l ∈ N such that (s, h) |= f[u →l] φ where f[u → l]
is the assignment equal to f except that u takes the value l.

When φ has no program variables, we also write h |= f φ to mean that φ is satisfied on the heap h under the assignment f.

It is worth noting that separating conjunction * has an existential flavour whereas separating implication - * has a universal flavour. Nonetheless, - * universally quantifies over an infinite set, namely the set of disjoint heaps. In the literature, an alternative syntax is used where e → e 1 , . . . , e k is represented by the conjunction below:

e 1 → e 1 ∧ • • • ∧ e k → e k
When pointer arithmetic is allowed, e → e 1 , . . . , e k can be also understood as the conjunction below which requires some semantical adjustment. Nevertheless, in this paper, we stick to e → e 1 , . . . , e k , as defined above.

(e → e 1 ) ∧ (e + 1 → e 2 ) ∧ • • • (e + (k -1) → e k ),
Note also that it is possible to get rid of program variables by viewing them as free quantified variables with rigid interpretation. However, it is sometime useful to distinguish syntactically program variables from quantified variables.

For k ≥ 0, we write kSLk to denote the fragment of kSL with at most k quantified variables. So, we write kSL1 to denote the fragment of kSL restricted to a single quantified variable, say u. Moreover, kSLk (- * ) [resp. kSLk ( * )] denotes the fragment of kSLk without separating conjunction [resp. wihout separating implication]. Note also that kSL can be understood as a syntactic fragment of (k + 1)SL by simply encoding e → e 1 , . . . , e k by e → e 1 , e 1 , . . . , e k everywhere (the first expression is repeated twice).

As noted earlier, we do not make a distinction between the (countably infinite) set of locations and the set of values that includes the locations since only the set N is used to define the stores and heaps.

Let L be a logic of the form kSLk or one of its fragments or extensions. As usual, the satisfiability problem for L takes as input a formula φ from L and asks whether there is a memory state (s, h) and an assignment f such that (s, h) |= f φ. The validity problem is also defined as usual. The model-checking problem for L takes as input a formula φ from L, a memory state (s, h) and a finite assignment f for free variables from φ and asks whether (s, h) |= f φ (s is finitely encoded and it is restricted to the program variables occurring in φ). Note that the model-checking problem for first-order logic over finite structures is known to be PSPACE-complete (see e.g. [START_REF] Vardi | The complexity of relational query languages[END_REF]) but we cannot conclude a similar statement for fragments of separation logic (even though s, h and f can be finitely encoded) because separating implication quantifies over an infinite set of disjoint heaps.

When k = 1, observe also that heaps are understood as Kripke frames of the form (N, R) where R is a finite and functional binary relation. Indeed, R = {(l, h(l)) : l ∈ dom(h)} for some heap h. Furthermore, 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.

Finally, it is well-known that there exists a formal relationship between * and - * since - * is the adjunct of * . This means that (φ * ψ) ⇒ ϕ is valid iff φ ⇒ (ψ - * ϕ) is valid. Note that this does not imply that the formula ((φ * ψ) ⇒ ϕ) ⇔ (φ ⇒ (ψ - * ϕ)) is valid (otherwise * and - * would be inter-definable). However, sometimes, we are able to show that we can get rid of one of the separating connectives, see e.g. Section 5.2, without sacrificing the expressive power.

We also introduce so-called septraction operator ¬ - * : φ ¬ - * ψ is defined as the formula ¬(φ - * ¬ψ). As far as we know, its first appearance was in [START_REF] Vafeiadis | A Marriage of Rely/Guarantee and Separation Logic[END_REF]. So, (s, h) |= f φ ¬ - * ψ iff there is a heap h disjoint from h such that (s, h ) |= f φ and (s, h h ) |= f ψ. The septraction operator states the existence of a disjoint heap satisfying a formula and for which its addition to the original heap satisfies another formula.

A bunch of properties stated in 1SL

The logic 1SL allows one to express different types of properties on memory states. The examples below indeed illustrate the expressivity of 1SL.

• The domain of the heap has at least α elements: ¬emp * • • • * ¬emp (α times).

• The variable x is allocated in the heap: alloc(x) def = (x → x) - * ⊥.

• The variable x points to a location that is a self-loop:

∃ u (x → u) ∧ (u → u)
In the following, let u and u be the variables u 1 and u 2 , in either order. Note that any formula φ(u) with free variable u can be turned into an equivalent formula with free variable u by permuting 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)
It is easy to see that one can also define in 1SL that the heap domain has at least k ≥ 0 elements (written size ≥ k).

• u has a successor: alloc(u)

def = ∃ u u → u • u has at least α predecessors: u ≥ α def = α times (∃ u (u → u)) * • • • * (∃ u (u → u)) • u has at most α predecessors: u ≤ α def = ¬ ( u ≥ α + 1) • u has exactly α predecessors: u = α def = ( u ≥ α) ∧ ¬( u ≥ α + 1)
• There is a non-empty path from u to u and nothing else except loops that exclude u:

reach (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: reach(u, u)

def = u = u ∨ * reach (u, u) One can show that h |= f reach(u, u) iff there is i ∈ N such that h i (f(u)) = f(u).
The proof for this property can be found in [BDL12, 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 a (possibly empty) path from u to u and nothing else can be defined as follows:

sreach(u, u) def = reach(u, u) ∧ ¬(¬emp * reach(u, u))
sreach(u, u) can be understood as the 'strict' reachability predicate and it is usually written as the segment predicate ls(u, u). • There is at most a single connected component (and nothing else):

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

2comps def = 1comp * 1comp
It is also worth noting that the separation logic 1SL is not necessarily minimal, see obvious reasons below. A similar reasoning applies to any separation logic kSL. For instance, in 1SL, the atomic formula emp is logically equivalent to the following formula using only two quantified variables:

∀ u ¬(∃ u (u → u ))
Alternatively, it is equivalent to the following, which uses only one:

∀ u ¬((u → u) - * ⊥)
Note that (u → u) - * ⊥ is the way to express alloc(u) in 1SL1 (as shown at the top of this section).

More interestingly, the atomic formula of the form e = e for some expressions e, e is logically equivalent to the following formula by using a new quantified variable u that does not occur in e = e :

∀ u ((u → e) - * (u → e ))
The formula simply states that adding to the heap a memory cell pointing to the location interpreted by e amounts to adding a memory cell pointing to the location interpreted by e .

Abstract separation logics

Concrete models for separation logic are memory states or heaps as defined earlier, but alternative models exist, for instance heaps with permissions, see e.g. [START_REF] Bornat | Permission accounting in separation logic[END_REF][START_REF] Brotherston | Undecidability of propositional separation logic and its neighbours[END_REF]. It is also possible to introduce more abstract models with a partial operator for gluing together models that are separate in some sense. This is the approach introduced in [START_REF] Calcagno | Local action and abstract separation logic[END_REF] and investigated in great length in subsequent papers * , see e.g. [BK10, LWG10, BV14, HCGT14]. After all, such an abstraction should not come as a surprise since separation logic is understood as an assertion language in a Hoarestyle framework that interprets BI in concrete heaps. Moreover, sometimes, problems can be easily solved on abstract models because more freedom is allowed (see e.g. [START_REF] Brotherston | Parametric completeness for separation theories[END_REF][START_REF] Hou | Proof search for propositional abstract separation logics via labelled sequents[END_REF] or Theorem 4.2).

Let (HS k , , U k ) be the triple such that HS k is the set of memory states with k ≥ 1 record fields and U k is the set of memory states of the form (s, ∅) where ∅ is the unique heap with empty domain. The structure (HS k , , U k ) satisfies the following properties

(MON ms ) is a partial binary operation : HS k × HS k → HS k and U k ⊆ HS k , (AC ms ) is associative and commutative, (CAN ms ) is cancellative, i.e. if (s, h) (s , h ) is defined and (s, h) (s , h ) = (s, h) (s , h ), then (s , h ) = (s , h ), (U ms ) for all (s, h) ∈ HS k , we have {(s, h)} = {(s, h) (s , h ) : (s , h ) ∈ U k , (s, h) (s , h ) is defined}.
A separation model defined below satisfies the above properties for (HS k , , U k ) by abstracting the essential features and can be viewed as a Kripke frame for a multi-February 9, 2015 Journal of Applied Non-Classical Logics final-jancl15 dimensional modal logic with binary modalities, see e.g. [START_REF] Marx | Multi-Dimensional Modal Logic[END_REF][START_REF] Hou | Proof search for propositional abstract separation logics via labelled sequents[END_REF]. A separation model is a cancellative partial commutative monoid (M, •, U ), i.e.

(MON) M is a non-empty set, • is a partial binary operation • : M × M → M and U ⊆ M , (AC) • is associative and commutative, (CAN) • is cancellative, i.e. if m • m is defined and m • m = m • m , then m = m , (U) For all m ∈ M , we have m • U = {m}.
Obviously (HS k , , U k ) is a separation model but other memory models can be found in the literature, see e.g. [START_REF] Brotherston | Undecidability of propositional separation logic and its neighbours[END_REF] for many more examples. For instance, the RAM-domain model (P fin (N), , {∅}) is a separation model where P fin (N) is the set of finite subsets of N and X 1 X 2 is defined only if X 1 ∩X 2 = ∅ and then X 1 X 2 def = X 1 ∪X 2 (disjoint union). This corresponds to the separation model (HS k , , U k ) with k equal to zero.

Given a countably infinite set PROP = {p 1 , p 2 , . . .} of propositional variables, a valuation V is a map V : PROP → P(M ). Semantical structures of the separation model (M, •, U ) are understood as the separation model itself augmented by a valuation. Hence, the separation logic defined from the separation model (M, •, U ) has models that can be understood as Kripke models with underlying ternary relation induced by the operation • and interpretation of propositional variables done via V. The set of formulae is then defined as follows (note that it is a propositional language):

φ, ψ ::= emp | p | φ ∧ ψ | ¬φ | φ * ψ | φ - * ψ
Let m ∈ M and V : PROP → P(M ) be a valuation, the satisfaction relation |= is defined as follows (we omit the obvious clauses for Boolean connectives):

• m |= V emp iff m ∈ U (we keep the constant emp in the abstract setting but elements of U should be understood as units).

• m |= V p iff m ∈ V(p). • m |= V φ 1 * φ 2 iff for some m 1 , m 2 ∈ M , we have m = m 1 • m 2 , m 1 |= V φ 1 and m 2 |= V φ 2 . • m |= V φ 1 - * φ 2 iff for all m ∈ M such that m • m is defined, if m |= V φ 1 then m • m |= V φ 2 .
In the above definition for the satisfaction relation, the model (M, •, U ) is implicit but we also sometimes use the notation (M, •, U ), m |= V φ to emphasize the separation model in use.

A formula φ is valid in the separation model (M, •, U )

def ⇔ for all m ∈ M and for all valuations V, we have m |= V φ. Similarly, a formula φ is satisfiable in the separation model (M, •, U ) def ⇔ there exist m ∈ M and a valuation V such that m |= V φ. We write SL(M, •, U ) to denote the propositional separation logic defined from the separation model (M, •, U ) with propositional variables. When C is a class of separation models, we can also define the propositional separation logic SL(C) by admitting a family of separation models instead of a single model. Satisfiability and validity problems are defined accordingly. For instance, φ is satisfiable for SL(C) iff there exist

(M, •, U ) in C, m ∈ M and a valuation V such that (M, •, U ), m |= V φ.
The satisfiability problem for kSL0 (i.e. kSL without any first-order quantification) can be reformulated as the satisfiability problem in the separation model (HS k , , U k ) in which propositional variables are of the form x i → x j or x i = x j and the valuations V are constrained in such a way that (s, h)

∈ V(x i → x j ) iff h(s(x i )) = s(x j ). Similarly, we require that (s, h) ∈ V(x i = x j ) iff s(x i ) = s(x j ).
Of course, this reformulation as-sumes that atomic formulae have some structure and it also requires restricting the set of valuations. Note that the set of valuations can be restricted in many other ways, for instance by imposing that a propositional variable holds true only for a finite number of elements of M (see such restrictions in [START_REF] Brotherston | Undecidability of propositional separation logic and its neighbours[END_REF]).

Separation logic with data

In memory states defined in Section 2.2, heaps are of the form N N k when k record fields are involved. No record field is really distinguished and the logic kSL mainly allows to reason about the shape properties of the heap (and not so much on functional correctness). However, it is often important to be able to reason about data values, a typical example would be to consider programs that produce sorted lists. In that case, we would like to specify that the values occurring in a list are linearly ordered. Pointer arithmetic is another means to reason about data values when the set of locations (herein, represented by the set N) is equipped with relations other than equality. Even though it is well-known that adding data domains easily leads to undecidable logics, see e.g. [DD07, BMS + 06], there exist several successful examples of logics able to reason about heap structures and data values, while having decidable reasoning tasks, see e.g. [START_REF] Bansal | Beyond shapes: Lists with ordered data[END_REF][START_REF] Bouajjani | A logic-based framework for reasoning about composite data structures[END_REF][START_REF] Madhusudan | Decidable logics combining heap structures and data[END_REF]. Reasoning about data values mainly means to be able to distinguish at least one record field dedicated to data values and to express data constraints in the formulae. That is why, in full generality, data domains need to be introduced in the semantics.

A data domain is a pair (D, (R i ) i∈I ) where D is a non-empty set, I is an index set and each R i is a relation of arity a(i) on D, that is, it is a subset of D a(i) . A typical example of data domain is (Z, <, =). The index set I is not necessarily finite and below, we assume that D is infinite and the family (R i ) i∈I contains the diagonal relation on D so that equality tests between data values can be expressed in the logic. Indeed, this makes the data domain all the more interesting and non-trivial. A memory state with data (with respect to the data domain (D, (R i ) i∈I )) is a triple (s, h, d) such that (s, h) is a memory state and d is a partial function N D. Below, we also assume that dom(h) = dom(d) in order to have correspondences between partial functions of the form N D × N k (the first record field is therefore dedicated to data values) and pairs of the form (h, d) when h is a heap with k record fields. This is analogous to what is defined in [START_REF] Bansal | Beyond shapes: Lists with ordered data[END_REF], a pioneering work for separation logic with data values but other options would be possible, even though not investigated below.

The logic kSL[D, (R i ) i∈I ] is defined as kSL except that atomic formulae of the form R i (e 1 , . . . , e a(i) ) are added for each i ∈ I and the models are memory states with data with respect to (D, (R i ) i∈I ). In order to avoid confusion with equality between locations (by contrast to equality between their data values, if any), we write e ∼ e to denote the equality formula between two data values, following a similar convention from [BMS + 06]. For instance, linear ordered data domains have been considered in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Segoufin | Automata based verification over linearly ordered data domains[END_REF] with LTL-like logics or in [START_REF] Bansal | Beyond shapes: Lists with ordered data[END_REF] with separation logic where 1SL[Z, ≤, =] has been investigated. The satisfaction relation is extended in order to cope with the new atomic formulae:

• (s, h, d) |= f R i (e 1 , . . . , e a(i) ) def ⇔ d([e 1 ]), . . . , d([e a(i) ]) are defined and R i (d([e 1 ]), . . . , d([e a(i) )]). Note that in kSL[D, (R i ) i∈I ],
there is no quantification on data values but this would be possible by defining a multi-sorted separation logic to distinguish locations from data values, as done in [START_REF] Bansal | Beyond shapes: Lists with ordered data[END_REF]. Similarly, the logics of the form kSL (see e.g., Section 2.2) happen to be quite expressive (see forthcoming developments) and adding the ability to reason about data can only increase the computational complexity of the reasoning tasks. That is why, most of the variants of separation logic with data considered in [START_REF] Bansal | Beyond shapes: Lists with ordered data[END_REF] banish the magic wand operator and provide even further restrictions. Let 1SL sdc < be the fragment of 1SL( * )[Z, ≤, =] (without magic wand) such that the atomic formulae can only occur in subformulae of the form either e → e ∧ (e ≤ e ) or e → e ∧ (e ≤ e). As noted in [START_REF] Bansal | Beyond shapes: Lists with ordered data[END_REF], only short-distance comparisons are possible in 1SL sdc < and this may allow to specify sorted lists. For example, the formula below specifies that the list between x 1 and x 2 (assuming that reach(x 1 , x 2 ) ∧ alloc(x 1 ) ∧ alloc(x 2 ) holds true) is sorted:

∀u, u ((reach(x 1 , u) ∧ reach(u, u ) ∧ reach(u , x 2 )) ⇒ u ≤ u )
where ≤ is "less than or equal relation" definable in the data domain (Z, <, =).

Other types of logics with data have been considered in the literature. One of the most prominent ones is the logic STRAND introduced [START_REF] Madhusudan | Decidable logics combining heap structures and data[END_REF] that can state constraints on the heap structures but also on the data. Recursive structures are defined thanks to monadic second-order logic whereas the use of data constraints is significantly limited. The very combination of the two types of properties allow to reason with heap-manipulation programs using deductive verification and SMT solvers, such as Z3 [START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF]. Another related logic is the one introduced in [START_REF] Bouajjani | A logic-based framework for reasoning about composite data structures[END_REF] for which a quite general framework is proposed to reason about heap structures and data values.

Separation Logics and Friends

In this section, we present several logics that are closely related to some fragments of kSL. For instance, 1SL( * ) can be also viewed as the spatial logic for graphs but restricted to the graphs obtained from heaps with one record field [START_REF] Dawar | Expressiveness and complexity of graph logic[END_REF][START_REF] Lozes | Expressivité des Logiques Spatiales[END_REF] (see also context logic in [START_REF] Calcagno | Context logic as modal logic: Completeness and parametric inexpressivity[END_REF][START_REF] Ph | An Introduction to Context Logic[END_REF] or ambient logic [START_REF] Cardelli | Anytime, Anywhere: Modal Logics for Mobile Ambients[END_REF]). More relationships shall be established below.

First-order logic with second-order features

In this section, let us focus on 1SL without program variables. Models for 1SL can be viewed as first-order structures of the form (N, R) where R is a finite and deterministic binary relation. We have seen in Section 2.2 that there is a formula reach(u, u) in 1SL2( * ) such that h |= f reach(u, u) iff f(u)R f(u), where R is the reflexive and transitive closure of R with

R def = {(l, l ) : l ∈ dom(h), h(l) = l }
Anyway, 1SL without the separation connectives is clearly a fragment of first-order logic on structures of the form (N, R) where R is a finite and deterministic binary relation. Adding the separating conjunction provides a little bit of second-order logic, for instance by encoding the reachability relation. Given a binary relation R, we write DTC(R) to denote the deterministic transitive closure of R defined as the transitive closure of the relation

R det = {(l, l ) ∈ R : there is no l = l such that (l, l ) ∈ R} So, when (N, R) is an 1SL model, DTC(R) can be defined in 1SL2( * ) itself.
In fragments of classical logic, the presence of the deterministic transitive closure operator can lead to undecidability where the operator on the binary relation R amounts to consider the transitive closure of the deterministic restriction R det . In [START_REF] Grädel | Undecidability results on two-variable logics[END_REF], it is shown that FO2 (i.e. first-order logic restricted to two quantified variables) augmented with the deterministic transitive closure operator has an undecidable finitary satisfiability problem. By contrast, FO2 has the finite model property and the satisfiability problem is NEXPTIME-complete, see e.g. [START_REF] Grädel | On the decision problem for twovariable first-order logic[END_REF]. Recently, FO2 augmented with the deterministic transitive closure of a single binary relation is shown to have a decidable and EXPSPACE-complete satisfiability problem [START_REF] Charatonik | Decidability of Weak Logics with Deterministic Transitive Closure[END_REF]. The works [START_REF] Grädel | Undecidability results on two-variable logics[END_REF] and [START_REF] Charatonik | Decidability of Weak Logics with Deterministic Transitive Closure[END_REF] contain numerous undecidability results related to the deterministic transitive closure operator but this involves more than one binary relation, whereas the models for 1SL have a unique deterministic binary relation. However, several results presented in [START_REF] Charatonik | Decidability of Weak Logics with Deterministic Transitive Closure[END_REF] are quite optimal with respect to the syntactic resources.

Meanwhile, Yorsh et al.

[YRS + 06] study a decidable version of first-order logic with reachability; they get decidability by making severe syntactic restrictions on the placement of quantifiers and on the reachability constraints, although the resulting logic is capable of describing useful linked data structures.

Weak second-order logic

Next we define weak second-order logic kWSOL, for k ≥ 1. The sets PVAR and FVAR are defined as for kSL as well as the expressions e. We also consider a family SVAR = (SVAR i ) i≥1 of second-order variables, denoted by P, Q, R, . . . that are interpreted as finite relations over N. Each variable in SVAR i is interpreted as an i-ary relation.

As for kSL, models are memory states with k ≥ 1 record fields. A second-order assignment f is an interpretation of the second-order variables such that for every P ∈ SVAR i , f(P) is a finite subset of N i .

Atomic formulae take the form where P ∈ SVAR n for some n ≥ 1. We write kMSOL (monadic second-order logic) to denote the restriction of kWSOL to second-order variables in SVAR 1 and kDSOL (dyadic second-order logic) to denote its restriction to SVAR 2 . Like kSL, models for kWSOL are memory states and quantifications are done over all the possible locations. The satisfaction relation |= is defined as follows (f is a hybrid valuation providing interpretation for first-order and second-order variables):

• (s, h) |= f ∃ P φ iff there is a finite relation R ⊆ N n such that (s, h) |= f[P →R] φ where P ∈ SVAR n . • (s, h) |= f P(e 1 , . . . , e n ) iff ([e 1 ], . . . , [e n ]) ∈ f(P).
The satisfiability problem for kWSOL takes as input a sentence φ in kWSOL and asks whether there is a memory state (s, h) such that (s, h) |= φ. By Trakhtenbrot's Theorem [START_REF] Trakhtenbrot | Impossibility of an algorithm for the decision problem in finite classes[END_REF][START_REF] Örger | The Classical Decision Problem[END_REF], the satisfiability problem for kDSOL (and therefore for kWSOL) is undecidable since finite satisfiability for first-order logic with a unique binary relation symbol is undecidable. Note that a monadic second-order variable can be simulated by a binary second-order variable from SVAR 2 , and this can be used to relativize a formula from DSOL in order to check finite satisfiability.

Theorem 3.1. [START_REF] Brochenin | On the almighty wand[END_REF] kWSOL and kDSOL have the same expressive power.

It has been recently shown in [START_REF] Demri | Expressive completeness of separation logic with two variables and no separating conjunction[END_REF] that 1SL2(- * ) is as expressive as 1WSOL. The proof hinges on the fact that that every sentence from 1DSOL has an equivalent sentence in 1SL2(- * ), as discussed in Section 5.2.

Translation in the other direction concerns us in this section. Separation logic 1SL can easily be translated into 1DSOL. The presentation given here is by a simple internalization.

First, some formula definitions useful for the translation.

• init(P)

def = ∀ u v (P(u, v) ⇔ u → v), • heap(P) def = ∀ u v w ((P(u, v) ∧ P(u, w)) ⇒ v = w) (functionality), • P = Q R def = ∀ u v ((P(u, v) ⇔ (Q(u, v) ∨ R(u, v)) ∧ ¬(Q(u, v) ∧ R(u, v))).
The formula init initializes a binary relation P to be precisely the heap graph; this is a notational convenience for the top level of the translation. heap requires that a relation P is functional and is used to ensure that subheaps (as interpreted by second-order variables) are in fact heaps. Finally, P = Q R composes two relations representing subheaps (Q and R) into one-or alternatively, it can be seen as decomposing P into two disjoint pieces; it is used in both "directions" in the translation.

Let the top-level translation t(φ) def = ∃ P (init(P) ∧ t P (φ)), where t P is the translation with respect to P as the "current" heap for interpretation. It is homomorphic for Boolean connectives, and otherwise has this definition:

t P (u → v) def = P(u, v) t P (φ * ψ) def = ∃ Q Q P = Q Q ∧ t Q (φ) ∧ t Q (ψ) t P (φ - * ψ) def = ∀ Q ((∃ Q heap(Q ) ∧ Q = Q P) ∧ heap(Q) ∧ t Q (φ)) ⇒ (∃ Q heap(Q ) ∧ Q = Q P ∧ t Q (ψ))
Theorem 3.2. (see e.g. [START_REF] Brochenin | On the almighty wand[END_REF]) There exists a translation t such that for any 1SL sentence φ and for any memory state (s, h), we have

(s, h) |= φ in 1SL iff (s, h) |= t(φ) in 1DSOL.
Note that of course there must then also exist a translation from the smaller fragment 1SL2(- * ) into 1DSOL. This result (along with Theorem 3.1 above) will be useful later in showing expressive power results of separation logic.

3.2.0.1 General inductive predicates. Using general inductive predicates provides another means to define second-order properties on heaps and this is a very useful feature to describe the shape of data structures, such as linked lists for instance. Semantics for general inductive predicates using least fixpoint operators can be naturally encoded in second-order logic, see e.g. [START_REF] Qiu | Natural proofs for structure, data, and separation[END_REF]. Until very recently, such predicates are hard-coded but new results on the satisfiability and entailment problems for general inductive predicates have been obtained, see e.g. [IRS13, AGH + 14, BFGN14]. Whereas, it is shown in [START_REF] Brotherston | A decision procedure for satisfiability in separation logic with inductive predicates[END_REF] that the satisfiability problem for many standard fragments of separation logic augmented with general inductive predicates is decidable and complexity is characterized (see also [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF] for bounded tree-width structures), other fragments have been shown to admit decidable entailment problem [IRS13, AGH + 14]. These are general results that are very promising for automatic verification of programs, despite the generality of the defined predicates.

Interval temporal logics

Temporal logics are dedicated to temporal reasoning, see e.g. [START_REF] Manna | The Temporal Logic of Reactive and Concurrent Systems[END_REF] and it is common for such logics to reason about propositions that vary at different points in time, but it is useful as well to consider intervals; an early and classical study for reasoning about intervals can be found in [START_REF] Allen | Maintaining knowledge about temporal intervals[END_REF]. Interval-based temporal logics admit time intervals as first-class objects. One of the most prominent interval-based logics is Propositional Interval Temporal Logic (PITL), introduced 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. Naturally, this is rather reminiscent of the separating conjunction, and indeed the correspondence has recently been made precise in [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF]. Below, we consider PITL in which propositional variables are interpreted under the locality condition (the truth of a propositional variable on an interval depends only on the first letter of the interval) and for which decidability is guaranteed but computational complexity is very high. This will allow us to derive similar bounds for 1SL2( * ).

It is typical in interval temporal logic to not cleave the model into two disjoint pieces, but rather to permit overlap at one point. This gives nonempty models, and is one of the two main issues in showing correspondence between 1SL( * ) and PITL, though it is still possible. The other difficulty is in showing how to use 1SL( * ) to properly cut an interval so that the data encoding is not split in an improper way.

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 w ∈ Σ + . 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 ∈ Σ.
Roughly speaking, a holds true at a 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 define a ternary relation chops on words:

chops def = (w 1 , w 2 , w 3 ) ∈ (Σ + ) 3 | ∃ a, w , w s.t. w 1 = w aw , w 2 = w a, w 3 = aw
Then, let us define the satisfaction relation |= for PITL Σ between a word w ∈ Σ + and a formula φ:

• w |= a def ⇔ the first letter of w is a. • w |= pt def ⇔ the length of w is 1. • w |= ¬φ def ⇔ w |= φ. • w |= φ ∧ ψ def ⇔ w |= φ and w |= ψ. • w |= φ C ψ def ⇔ there exist w 1 , w 2 such that chops (w, w 1 , w 2 ), w 1 |= φ and w 2 |= ψ.
We then have the following results.

Lemma 3.3. Given α ≥ 1 and Σ = [1, α], there is a logarithmic-space translation t(•) of PITL formulae to 1SL2( * ) formulae such that a PITL Σ formula φ is satisfiable if and only if the 1SL2( * ) formula t(φ) is satisfiable.

There are two chief insights that permit this result. First, words may be represented by memory states which can be described by 1SL2( * ) formulae. Briefly, these memory states, called fishbone heaps in [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF] and defined formally herein (see Section 4.1.4), encode a word of length n over a finite alphabet of size m by an acyclic path of length n where each successive memory location has a number of predecessors that precisely encodes the element of the alphabet corresponding to its position within the word. Care must be taken during the translation so as not to divide these fishbones improperly, else the result may be interpreted as a different word. Second, there is a striking correspondence between PITL's chop and the separating conjunction. As PITL's chop conventionally separates an interval into two, duplicating the point of separation, the translation must take care to translate with respect to the duplicated point.

This result leads directly to Theorem 4.14, shown later.

Modal logics

Separation logic is related to modal logics in many ways, and actually the full paper is dedicated to put forward existing bridges. Nevertheless, below, we present several modal readings for separation logic. At first, the separating connectives * and - * force the interpretation of subformulae in alternative heaps, which is reminiscent to the destructive aspect of van Benthem's sabotage modal logic [vB05]. Indeed, sabotage modal logic (SML) defined in [vB05] has the ability to remove states in a transition system. A variant of SML is introduced in [START_REF] Rohde | Model checking and satisfiability for sabotage modal logic[END_REF] with the possibility to withdraw transitions, a feature also shared with logics from [PW04, Dem05, G öl07], see also logics of public announcements [START_REF] Lutz | Complexity and succinctness of public announcement logic[END_REF]. The satisfiability problem for that variant is shown undecidable in [START_REF] Rohde | Model checking and satisfiability for sabotage modal logic[END_REF] (another variant is shown undecidable in [START_REF] Ph | Moving in a crumbling network: The balanced case[END_REF] in which deletion of the transitions is done locally to the current state). Other modal logics updating the model while evaluating formulae have been considered in a systematic way in [START_REF] Aucher | Global and local graph modifiers[END_REF].

Secondly, several logical formalisms have included modalities from modal or temporal logics with separating connectives. Whereas a modal BI logic is introduced in [START_REF] Courtault | A modal BI logic for dynamic resource properties[END_REF] for expressing dynamic resource properties, temporal reasoning about memory states has been performed in several ways, for instance in Navigation Temporal Logic in [START_REF] Distefano | Who is pointing when to whom? On the automated verification of linked list structures[END_REF], in Evolution logic [START_REF] Yahav | Verifying temporal heap properties specified via evolution logic[END_REF] or in some LTL extension with formulae from separation logic at the atomic level [START_REF] Brochenin | Reasoning about sequences of memory states[END_REF][START_REF] Brochenin | Separation Logic: Expressiveness, Complexity, Temporal Extension[END_REF].

A taste of multi-dimensional modal logics

Versions of separation logics with the connectives * and - * can be also understood as multi-dimensional modal logics, see e.g. [MV97, GKWZ03, HCGT14]. Multidimensional modal logics are known as modal logics with n-ary modalities, n ≥ 1 and models are of the form M = (W, R, V ) with non-empty set W , R ⊆ W n+1 , for some n ≥ 1 and V : PROP → W . For each i ∈ [1, n + 1], we can define the n-ary modality 3 i such that M, w |= 3 i (φ 1 , . . . , φ i-1 , φ i+1 , . . . , φ n+1 ) iff there is (w 1 , . . . , w n+1 ) ∈ R with w i = w such that for all j ∈ [1, n + 1] \ {i}, we have M, w j |= φ j . Note that when n = 1, 3 1 corresponds to the standard modality 3 and 3 2 corresponds to the standard backward modality 3 -1 . So, it is not difficult to observe that 1SL0 can be understood as a multi-dimensional modal logic in the above sense with a unique Kripke model and n = 2. Such a unique model M = (W, R, V ) is defined as follows:

• W def = {(s, h) : s : PVAR → N, h : N fin N} (i.e., W def = HS 1 ). • ((s 1 , h 1 ), (s 2 , h 2 ), (s 3 , h 3 )) ∈ R def ⇔ s 1 = s 2 = s 3 and h 1 = h 2 h 3 . • V (x i → x j ) def = {(s, h) : h(s(x i )) = s(x j )}. • V (x i = x j ) def = {(s, h) : s(x i ) = s(x j )}. • V (emp) def = {(s, h) : dom(h) = ∅}.
With such a model, φ * ψ corresponds to 3 1 (φ, ψ), φ ¬ - * ψ corresponds to 3 2 (ψ, φ) or to 3 3 (ψ, φ) ( is commutative). Finally, φ - * ψ corresponds to ¬3 2 (¬ψ, φ). We invite the reader to consult [START_REF] Hou | Proof search for propositional abstract separation logics via labelled sequents[END_REF] for an explicit presentation of Kripke relational frames for abstract separation logics.

A modal logic for heaps

In order to conclude this section mainly dedicated to modal logics, we present a new modal logic with such frames [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF]. 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 φ | = φ | φ | φ * ψ | φ - * ψ
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. 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):

• 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 |= φ, • 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 .
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. [dR92]) 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. However, it is possible to design a relational translation t from MLH formulae into 1SL2 formulae by recycling variables. 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][START_REF] Van Benthem | Correspondence Theory[END_REF][START_REF] Blackburn | Modal Logic[END_REF]. Indeed, models for MLH are heap graphs. 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. Note that because MLH has models with a deterministic relation, its restriction without separating connectives is strongly related to Deterministic PDL [START_REF] Ben-Ari | Deterministic propositional dy-namic logic: finite models, complexity, and completeness[END_REF] and to Description Logic with functional roles, see e.g. [START_REF] Calvanese | Expressive description logics[END_REF].

Decidability and Computational Complexity

In this section, we present several results about the decidability status of separation logics and their fragments. Most of the undecidability results are obtained by quite simple reductions (only main ideas are presented below) whereas decidability is ob- tained by translation into a richer logical formalism, for example among decidable monadic second-order logics. We state a few results about complexity also; these shall be completed by a thorough discussion of expressive power in Section 5.

Undecidability results

We start by addressing the understanding, common to computer scientists, that "separation logic is undecidable"-although upon inspection, the proof does not in fact involve any appeal to separation logic. After, we consider various undecidable restrictions which get more to the heart of what makes separation logic undecidable.

Undecidability of 2SL

A remarkable result about the decidability status of (first-order) separation logic is stated below and is due to [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF] (see also [START_REF] Yang | Local Reasoning for Stateful Programs[END_REF]Section 8.1]).

Theorem 4.1. [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF] The satisfiability problem for 2SL is undecidable.

The proof is based on the fact that finitary satisfiability for classical predicate logic restricted to a single binary predicate symbol is undecidable [START_REF] Trakhtenbrot | Impossibility of an algorithm for the decision problem in finite classes[END_REF], see also [START_REF] Örger | The Classical Decision Problem[END_REF]. This means that given a first-order sentence φ built over the binary predicate symbol R, checking whether there is a finite structure (D, R) (a finite directed graph) such that (D, R) |= φ (in the first-order sense) is undecidable. Indeed, any such a structure can be encoded (modulo isomorphism) by some heap h and some distinguished location l 0 such that: where t(•) is defined below:

• l 0 ∈ dom(h), • D = {l ∈ N : h(l) = (l 0 , l 0 )}, • R = {(l, l ) ∈ D 2 : there is l such that h(l ) = (l, l )}.
• t is homomorphic for Boolean connectives. • t(u i = u j ) def = (u i = u j ) ∧ (u i → nil, nil) ∧ (u j → nil, nil), • t(R(u i , u j )) def = (u i → nil, nil) ∧ (u j → nil, nil) ∧ (∃u (u → u i , u j )), • t(∃ u ψ) def = ∃u (u → nil, nil) ∧ t(ψ), • t(∀ u ψ) def = ∀ u (u → nil, nil) ⇒ t(ψ).
Observe that nil is understood as a distinguished variable whose interpretation is not in the heap domain. It is also worth noting that T (φ) makes no use of program variables, separating conjunction, or separating implication. In a sense, the undecidability of 2SL, as explained above, is not very much related to separating connectives, but rather to the fact that heaps with two record fields can encode finite binary relations.

Theorem 4.2. [COY01]

The set of valid formulae for 2SL is not recursively enumerable.

As a consequence, 2SL is not finitely axiomatizable. Indeed, φ is finitely valid iff ∀u, nil ((u → nil, nil) ∧ (¬∃u , u nil → u , u )) ⇒ t(φ) is 2SL valid. Since this is a logarithmic-space reduction and since the set of finitely valid formulae is not recursively enumerable, this leads to Theorem 4.2. It seems that this fact is not so well-known (this is of course mentioned in [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF], and in a few other places such as in [Web04, Section 5] or in [Qiu13, Chapter 2]) but it has unpleasant consequences for defining proof systems for separation logics with concrete heaps (see e.g., [START_REF] Galmiche | Tableaux and resource graphs for separation logic[END_REF][START_REF] Lee | A proof system for separation logic with magic wand[END_REF][START_REF] Hou | Proof search for propositional abstract separation logics via labelled sequents[END_REF]). Note also that the result applies to any kSL since 2SL can be viewed then as a syntactic fragment of kSL as soon as k ≥ 2. Moreover, it is worth mentioning that the authors of the proof system in [START_REF] Lee | A proof system for separation logic with magic wand[END_REF] have acknowledged in their POPL'14 presentation that their system is actually unsound for Reynolds' semantics -we believe it might be worth mentioning such a fact to avoid a similar situation in the future.

In Section 5.2, we are able to show a similar result with 1SL by using directly firstorder theory of natural numbers with addition and multiplication.

Undecidability of 1SL

We have seen that the satisfiability problem for 2SL is undecidable [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF] with a proof that does not require separating connectives and uses [START_REF] Trakhtenbrot | Impossibility of an algorithm for the decision problem in finite classes[END_REF] in an essential way; a stronger statement is made in [START_REF] Brochenin | On the almighty wand[END_REF] by showing that the satisfiability problem for 1SL is undecidable as well. This is a consequence of the expressive equivalence between 1SL and weak second-order logic 1WSOL on memory states with a single record field.

Theorem 4.3. [BDL12] The satisfiability problem for 1SL is undecidable.

More recently, 1SL restricted to two variables (1SL2) has also been shown undecidable [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF] (via a reduction from the halting problem for Minsky machines, briefly recalled below) but without touching the central question of expressive completeness, which is the purpose of [START_REF] Demri | Expressive completeness of separation logic with two variables and no separating conjunction[END_REF]. By way of comparison with [GOR99, IRR + 04] and as discussed in Section 3.1, undecidability of 1SL2 cannot be derived from [GOR99, IRR + 04] since in 1SL models, we deal with a single functional binary relation, namely the finite heap. By contrast, FO2 is known to admit a decidable and NEXPTIMEcomplete satisfiability problem, see e.g. [START_REF] Grädel | On the decision problem for twovariable first-order logic[END_REF].

Propositional separation logics

Whereas the satisfiability problem for any propositional fragment kSL0 is decidable and indeed PSPACE-complete (see Section 4.3.2), propositional versions of abstract separation logic with propositional variables are easily shown undecidable.

Theorem 4.4. [BK10, LWG10] The satisfiability problems for SL(P fin (N), , {∅}) and for SL(HS k , , U k ) -k ≥ 1-are undecidable.

Actually, results in [BK10, LWG10] are much more general. Herein, we limit ourselves to two separation models that are obviously related to concrete heaps. Below, by way of example, we provide the undecidability proof for SL(P fin (N), , {∅}) by simple semantical arguments (and without using any proof-theoretical arguments, unlike what is done in [START_REF] Brotherston | Undecidability of propositional separation logic and its neighbours[END_REF][START_REF] Larchey-Wendling | The undecidability of Boolean BI through phase semantics[END_REF]). As far as we know, such a slightly alternative proof has not been published elsewhere.

Before presenting the undecidability proof, let us mention the equivalence of the statements below:

(1) φ is valid in SL(P fin (N), , {∅}).

(2) ¬φ is not satisfiable in SL(P fin (N), , {∅}).

(3) ¬φ is not satisfiable in SL(HS k , , U k ) (for any k ≥ 1). (4) φ is valid in SL(HS k , , U k ) (for any k ≥ 1).

Whereas the equivalences between instances for validity and satisfiability are standard, the equivalences related to distinct separation models are simply due to the fact, in such logics, composition of heaps only requires that the domain are disjoint, independently of the range of the heaps. Note also that SL(P fin (N), , {∅}) can be understood as the logic SL(HS k , , U k ) with k equal to zero.

Let M be a Minsky machine with α ≥ 1 instructions, 1 is the initial instruction and α is the halting instruction [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF]. Machine M has two counters c 1 and c 2 and the instructions are of the following types (j

∈ [1, 2], I ∈ [1, α -1], J, J 1 , J 2 ∈ [1, α]):
(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. 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]. We build a formula φ M such that M halts iff φ M is valid in SL(P fin (N), , {∅}), which entails the undecidability of the satisfiability problem for SL(P fin (N), , {∅}). The formula φ M is built over the propositional variables q, q , p 1 and p 2 . Given a valuation V, a configuration (I, c 1 , c 2 ) of M is encoded by some set X ∈ P fin (N) such that

• X ∈ V(q ) (meaning X encodes a configuration), • X = X 0 X 1 X 2 (X
can be decomposed so that there are disjoint parts about instruction counter, first counter and second counter),

• card(X 0 ) = I, card(X 1 ) = c 1 and card(X 2 ) = c 2 , • for all ∅ = Y ⊆ X 0 , Y ∈ V(q) \ (V(p 1 ) ∪ V(p 2 )), • for all ∅ = Y ⊆ X 1 , Y ∈ V(p 1 ) \ (V(p 2 ) ∪ V(q)), • for all ∅ = Y ⊆ X 2 , Y ∈ V(p 2 ) \ (V(p 1 ) ∪ V(q)).
In that case, we write X ≈ V (I, c 1 , c 2 ). The formula φ M has the following form:

((emp ∧ p 1 ∧ p 2 ∧ ¬q ∧ ¬q ) ∧ closure) ⇒ ( ¬ - * (q ∧ (p 1 * p 2 * (size = α ∧ q))))
The formula closure guarantees that for any configuration (I, c 1 , c 2 ) reachable from the initial configuration (1, 0, 0), there is some X ∈ P fin (N) such that X ≈ V (I, c 1 , c 2 ) (in that case, note that card(X) = I + c 1 + c 2 ).

The formula ¬ - * (q ∧ (p 1 * p 2 * (size = α ∧ q))) states that there is X ∈ P fin (N) such that X = X 0 X 1 X 2 , card(X 0 ) = α, X 1 encodes the first counter and X 2 encodes the second counter.

Let U ψ be an abbreviation for ¬ - * ψ and [U] ψ be an abbreviation for - * ψ, following an obvious analogy with the universal modality in Kripke models, see e.g. [START_REF] Goranko | Using the universal modality: gains and questions[END_REF][START_REF] Hemaspaandra | The price of universality[END_REF]. The formula closure is defined as the conjunction of the following formulae:

• U (size = 1 ∧ q ∧ q ). There is X encoding the configuration (1, 0, 0).

• [U](p 1 ⇒ (¬((¬p 1 ∧ ¬emp) * ) ∧ (¬emp ⇒ ¬p 2 ) ∧ ¬q ∧ ¬q ). • [U](p 2 ⇒ (¬((¬p 2 ∧ ¬emp) * ) ∧ (¬emp ⇒ ¬p 1 ) ∧ ¬q ∧ ¬q ), • [U](q ⇒ (¬((¬q ∧ ¬emp) * ) ∧ ¬p 1 ∧ ¬p 2 ).
In the sequel, the modalities U and [U] are used at the outermost level only and therefore they are evaluated only on the empty set. More generally, the universal modality

[U] can be defined as follows:

[U]φ def = (emp ∧ ( - * φ)) *
Consequently, whenever X |= V (q ∧ size = I) * p 1 * p 2 for some I ∈ [1, α], there is no I = I such that X |= V (q ∧ size = I ) * p 1 * p 2 . Moreover, there are unique X 0 , X 1 and X 2 such that X = X 0 X 1 X 2 , X 0 |= V (q ∧ size = I), X 1 |= V p 1 and X 2 |= V p 2 . We add to closure the following formulae:

• For all instructions of the form I: c 1 := c 1 + 1; goto J, we consider

[U]((((q ∧ size = I) * p 1 * p 2 ) ∧ q ) ⇒ (q ∧ size = I) * (((q ∧ size = J) * (size = 1 ∧ p 1 )) ¬ - * (((q ∧ size = J) * p 1 * p 2 ) ∧ q )))
• Formulae for instructions of the form I: c 2 := c 2 + 1; goto J are defined similarly.

• For all instructions of the form I: if c 1 = 0 then goto J 1 else (c 1 := c 1 -1; goto J 2 ), we consider

[U]((((q ∧ size = I) * p 2 ) ∧ q ) ⇒ ((q ∧ size = I) * ((q ∧ size = J 1 ) ¬ - * q )))∧ [U]((((q ∧ size = I) * (p 1 ∧ ¬emp) * p 2 ) ∧ q ) ⇒ (((q ∧ size = I) * (p 1 ∧ size = 1)) * ((q ∧ size = J 2 ) ¬ - * q )))
• Formulae for instructions of the form I: if c 2 = 0 then goto J 1 else (c 2 := c 2 -1; goto J 2 ), are defined similarly.

The correctness proof works as follows. Suppose that the machine M halts. This means that for any valuation V, if ∅ |= V (emp ∧ p 1 ∧ p 2 ∧ ¬q ∧ ¬q ) ∧ closure, then there is some X ∈ P fin (N) such that X ≈ V (α, c 1 , c 2 ) for some c 1 , c 2 ∈ N, i.e. there is some X ∈ P fin (N) such that X |= V (p 1 * p 2 * (size = α ∧ q)) ∧ q , which is equivalent to ∅ |= V ( ¬ - * ((p 1 * p 2 * (size = α ∧ q))) ∧ q ). Now suppose that the machine M does not halt, this means that there is no configuration of the form (α, c 1 , c 2 ) reachable from the initial configuration (1, 0, 0). Let us define the following valuation V 0 :

• V 0 (q) def = P fin ([1, α -1]) \ {∅}, • V 0 (p 1 ) def = P fin ({α + 2k + 1 : k ∈ N}), V 0 (p 2 ) def = P fin ({α + 2k : k ∈ N}), • V 0 (q ) is
equal to the set below: One can check that (1) for every configuration (I, c 1 , c 2 ), we have

{X ∈ P fin (N) : (I, c 1 , c 2 ) reachable from (1, 0, 0), X = X 0 X 1 X 2 , card(X 0 ) = I, X 0 ∈ P fin ([1, α -1]), card(X 1 ) = c 1 , X 1 ∈ P fin ({α + 2k + 1 : k ∈ N}), card(X 2 ) = c 2 , X 2 ∈ P fin ({α + 2k : k ∈ N})}
(I, c 1 , c 2 ) is reachable from (1, 0, 0) iff there is X such that X ≈ V0 (I, c 1 , c 2 ), (2) ∅ |= V0 (emp ∧ p 1 ∧ p 2 ∧ ¬q ∧ ¬q ) ∧ closure, (3) there is no X ∈ P fin (N) such that X |= V0 (p 1 * p 2 * (size = α ∧ q)) ∧ q .
Consequently, φ M is not valid in SL(P fin (N), , {∅}). This concludes the proof of Theorem 4.4. It is worth noting that this undecidability proof uses only semantical arguments.

Undecidability for separation logic with data

The logic 1SL( * ) happens to be decidable by reduction into 1MSOL (see forthcoming Section 4.2). Below, we show that 1SL3( * )[Z, =], i.e. 1SL3( * ) augmented with data values in which only equality tests are possible is undecidable. Definition of 1SL( * )[Z, =] can be found in Section 2.5. We provide a reduction from the satisfiability problem for some temporal logic with the freeze operator, see e.g. [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF][START_REF] Figueira | Future-looking logics on data words and trees[END_REF] whereas the original proof in [START_REF] Bansal | Beyond shapes: Lists with ordered data[END_REF] uses a first-order logic on data words. This shift does not provide any substantial new insights but this is more coherent with our intention to compare separation logics with modal or temporal logics, in most occasions. Nevertheless, this alternative proof remains an original feature of this document.

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. Formally, 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]. A wealth of specification formalisms for data words (and slight variants) has been introduced stemming from automata (see e.g. [KF94, NSV04, BL10]) to adequate logical languages such as first-order logic [BDM + 11, Dav09, SZ12] and temporal logics [START_REF] Figueira | Reasoning on words and trees with data[END_REF]. In [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF], a reduction is designed 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 and in particular this shows how data words can be encoded by heaps within 1SL2 (see below).

First, we need to explain how to encode data words by heaps and data maps, which is quite easy. Let dw = (a

1 , v 1 ) • • • (a L , v L ) be a data word in ([1, α] × N) + . The data word dw is encoded by the heap h dw containing a path l 0 → l 1 → • • • → l L → l L+1 where
• l 0 has no predecessor, l L+1 ∈ dom(h dw ) and l L+1 has a unique predecessor, • for every i ∈ [1, L], l i has a i predecessors and a i -1 of them have themselves no predecessors (the remaining predecessor is l i-1 ), • every location in dom(h dw ) is either on that path or points to a location on that path.

In order to encode the data values, we introduce some partial function

d dw : N Z such that for every i ∈ [1, L], d dw (l i ) = v i .
Such a path from l 1 to l L is called the main path. Other simple encodings are possible but the current one is well-suited for the forthcoming developments. Note also that h dw and d dw are not uniquely specified, and in particular we understand them modulo isomorphism.

The heap h dw looks like a fishbone. Let us make this precise. A heap h is a fishbone def ⇔ (fb1) card(dom(h)) ≥ 2, (fb2) there is a location reachable from all the locations of dom(h) that is not in dom(h), it has exactly one predecessor 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 and in the heap domain. The existence of such a main path is guaranteed by (fb3). As shown in [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF], there is a formula φ fb in 1SL2( * ) such that h |= φ fb iff h is a fishbone. Let us refine the notion of fishbone heap so that it takes into account constraints on numbers of predecessors. An α-fishbone is a fishbone heap such that every location on the main path has a number of predecessors in [1, α] Again, there is a formula φ α fb such that (s, h) |= φ α fb iff h is an α-fishbone heap. There is also a formula mp(u) in 1SL2( * ) such that for any α-fishbone heap h, (s, h) |= f mp(u) iff f(u) is on the main path (i.e., f(u) ∈ {l 1 , . . . , l L }).

Now, let us show that the satisfiability problem for 1SL3( * )[Z, =] is undecidable by designing a reduction from an undecidable logic whose models are data words. We have already explained how 1SL3( * )[Z, =] can encode data words. As mentioned earlier, there exist many formalisms to specify properties about data words; among them can be found temporal logics with the freeze operator [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF][START_REF] Figueira | Future-looking logics on data words and trees[END_REF]. Let LTL α ↓ (F,F -1 ) be the set of formulae defined as follows:

φ ::= a | ↑ | ↓ φ | ¬φ | φ ∧ φ | Fφ | F -1 φ with a ∈ [1, α].
The operators F and F -1 are the standard (non-strict) temporal operators stating the existence of some future [resp. past] position satisfying a given property. The atomic formula ↑ and the freeze operator ↓ are interpreted as in hybrid logics [START_REF] Areces | Hybrid logics: characterization, interpolation and complexity[END_REF] except that instead of storing a node address, a data value is stored. Formulae in LTL α ↓ (F,F -1 ) are interpreted over data words dw = (a

1 , v 1 ) • • • (a L , v L ) in ([1, α]×N) + via the satisfaction relation |= v (Boolean clauses are omitted and i ∈ [1, L]): • dw, i |= v a def ⇔ a i = a, • dw, i |= v ↑ def ⇔ v i = v, • dw, i |= v ↓ φ def ⇔ dw, i |= v i φ, • dw, i |= v Fφ def ⇔ there is i ∈ [i, L] such that dw, i |= v i φ, • dw, i |= v F -1 φ def ⇔ there is i ∈ [1, i] such that dw, i |= v i φ.
A sentence is satisfiable def ⇔ there is a data word dw in ([1, α] × N) + such that dw, 1 |= φ (no need to specify a data value since φ is closed). The satisfiability problem for LTL α ↓ (F,F -1 ) is known to be undecidable [FS09, Theorem 4]. Let us define T (φ) as follows:

T (φ) def = φ α fb ∧ t(u 0 , φ) ∧ mp(u 0 ) ∧ ¬∃ u 1 (u 1 → u 0 ∧ mp(u 1 ))
We aim at satisfying that φ is satisfiable iff T (φ) is satisfiable in 1SL3( * )[Z, =]. The map t takes two arguments: a quantified variable among {u 0 , u 1 } (variables are indeed recycled, see e.g. [START_REF] Gabbay | Expressive functional completeness in tense logic[END_REF]) and a formula. A third variable u 2 is used but its purpose is to store a data value because of the presence of the freeze operator. We define the logarithmic-space translation t as follows (i ∈ {0, 1}). • t is homomorphic for Boolean connectives,

• t(u i , ↑) def = (u 2 ∼ u i ) and t(u i , a) def = ( u i = a), • t(u i , ↓ ψ) def = ∃ u 2 ((u 2 ∼ u i ) ∧ t(u i , ψ)), • t(u i , Fψ) def = ∃ u 1-i (t(u 1-i , ψ) ∧ mp(u 1-i ) ∧ reach(u i , u 1-i )), • t(u i , F -1 ψ) def = ∃ u 1-i (t(u 1-i , ψ) ∧ mp(u 1-i ) ∧ reach(u 1-i , u i )).
We recall that u 2 ∼ u i holds true when u 2 and u i are allocated and have the same data value.

We have already seen how to define the formulae u i = a, reach(u i , u 1-i ), mp(u 1-i ) and φ α fb . It is easy to check that φ is satisfiable iff T (φ) is satisfiable in 1SL3( * )[Z, =] since the map t only internalizes the semantics of LTL α ↓ (F,F -1 ) in 1SL3( * )[Z, =].

Theorem 4.5. [BBL09, Theorem 3] The satisfiability problem for 1SL3( * )[Z, =] is undecidable.

Other undecidability results about separation logics with data values can be found in [START_REF] Bansal | Beyond shapes: Lists with ordered data[END_REF].

Decidability results

Having seen various undecidable fragments of separation logic, we now turn our attention to fragments that admit a decidable satisfiability problem. As one may conjecture from the results above, the magic wand is quite powerful; its removal results in a decidable logic. Alternatively, the magic wand can be retained at the cost of one additional variable. These and other decidability results are discussed below.

Removing the wand

First we show that 1SL( * ) is decidable with non-elementary recursive complexity. Actually, the complexity lower bound holds already when only two quantified variables are used whereas the problem for the full fragment 1SL2 happens to be undecidable too [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF]. First, note that 1MSOL on memory states with one record field is decidable by taking advantage of [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF][START_REF] Örger | The Classical Decision Problem[END_REF]. Indeed, the weak monadic secondorder theory of unary functions is the theory over structures of the form (D, f, =) where D is a countable domain, f is a unary function, and = is equality. This theory is decidable, see e.g. [BGG97, Corollary 7.2.11]. Since it is possible to express that D is infinite and to simulate that f is a partial function with finite domain, one can specify that (D, f, =) augmented with a first-order valuation is isomorphic to a heap. It is then possible to define a simple translation t P (.), computable in logarithmic space, such that a 1MSOL sentence φ is satisfiable iff infinity (¬∃ P ∀u P(u)) ∧∃ P t P (φ) is satisfiable in the weak monadic second-order theory of one unary function. See details in [START_REF] Brochenin | On the almighty wand[END_REF]. Using a similar technique, it is possible to translate 1SL( * ) into 1MSOL. Any formula φ in 1SL( * ) is satisfiable iff

∃ P (∀u P(u) ⇔ (∃u u → u )) ∧ t P (φ)
is satisfiable where t P (•) is defined with the following clauses:

• t P (u → u ) def = P(u) ∧ u → u , • t P (u = u ) def = u = u , • t P (φ * ψ) def = ∃ Q, Q (P = Q Q ) ∧ t Q (φ) ∧ t Q (ψ) where P = Q Q is an abbreviation for ∀u (P(u) ⇔ (Q(u) ∨ Q (u))) ∧ ¬(Q(u) ∧ Q (u)).
We leave out the Boolean connectives and first-order quantification, for which t P is homomorphic.

Theorem 4.6. [BDL12, Corollary 3.3] The satisfiability problem for 1SL( * ) is decidable.

As conjectured in [START_REF] Brochenin | On the almighty wand[END_REF], recently it has been shown that 1MSOL is strictly more expressive than 1SL( * ) [AD09, Corollary 5.3]. 1SL( * ) is an important fragment to consider-and an important one to show decidable-as some verification applications do not require the use of the separating implication.

Removing a variable

On the other hand, the wand can be retained if one is willing to give up a variable. A recent result [START_REF] Demri | Separation logic with one quantified variable[END_REF] establishes this and, coupled with the results of [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF][START_REF] Demri | Expressive completeness of separation logic with two variables and no separating conjunction[END_REF], we now have a complete understanding of the decidability boundary in fragments of separation logic that restrict the number of variables (see also Figure 4 in Section 7).

Theorem 4.7. [DGLWM14] Satisfiability for 1SL1 is decidable.

Other fragments

By taking advantage of the decidability of 1MSOL over memory states with one record field, we can deduce the following results. Non-elementary complexity of MLH( * ) is also established in [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF]. So, solving the satisfiability problem for MLH( * ) requires time bounded below by towers of exponentials of height that depend on the formula size, see e.g. [START_REF] Schmitz | Complexity hierarchies beyond elementary[END_REF].

In Section 2.5, we introduce an extension of 1SL( * ) in which data interpreted in Z are added and can be compared only locally. The translation from 1SL( * ) to 1MSOL can be extended to 1SL sdc < , which provides a quite strong new decidability result.

Theorem 4.9. [BBL09, Corollary 1] The satisfiability problem for 1SL sdc < is decidable.

It remains partly open to characterize a significant class of data domains for which the extension of 1SL( * ) with data from those data domains would lead to decidability too. Other decidability results about 1SL( * ) extended with data values can be found in [BBL09, Section 5.2].

Computational complexity

In this section, we consider the computational complexity of decision problems for separation logics (mainly satisfiability, validity and entailment) and we provide a few characterizations ranging from problems that can be solved in polynomial time to problems that are decidable with a non-elementary complexity. In order to guarantee a reasonably fair variety of fragments we consider propositional fragments as well as logics in which quantification is permitted, although such quantification is often quite restricted.

A well-known fragment in polynomial time

Even though performing reasoning in propositional logic kSL0 (with k ≥ 1) can be computationally expensive, see below the PSPACE-completeness results for validity and satisfiability, fragments have been designed that are useful for automatic program analysis and hopefully less demanding computationally.

The fragment presented below, has been introduced in [BCO04] and shown decidable by providing a complete proof system. More importantly, the tool Smallfoot has been designed from it, see e.g. [START_REF] Berdine | Smallfoot: Modular automatic assertion checking with separation logic[END_REF], and decides the entailment problem for such a fragment, which allows to verify automatically numerous properties. Strangely enough, the precise computational complexity of the entailment problem for such a fragment is not considered in [START_REF] Berdine | A decidable fragment of separation logic[END_REF] and it is only in [CHO + 11, HIOP13] that this problem has been successfully solved.

Let SF ('Smallfoot fragment') be the fragment of 1SL2 defined by the formula φ below, where φ p defines pure formulae and φ s defines spatial formulae:

φ p ::=⊥ | | (x i = x j ) | ¬(x i = x j ) | φ p ∧ φ p φ s ::= emp | | x i → x j | sreach(x i , x j ) | φ s * φ s φ ::= φ p ∧ φ s
where x i , x j are program variables from PVAR. As usually, the formulae are interpreted on memory states with one record field. Obviously, x i → x j is interpreted as the exact points-to relation ((s, h)

|= x i → x j iff dom(h) = s(x i ) and h(s(x i )) = s(x j ))
whereas (s, h) |= sreach(x i , x j ) holds true iff the heap contains exactly a path from s(x i ) to s(x j ). As shown earlier, sreach(x i , x j ) (and reach(x i , x j ) too) can be specified in 1SL2.

The entailment problem for SF is defined as follows:

input: two formulae φ, ψ in SF. question: is it the case that for all memory states (s, h), we have (s, h) |= φ implies (s, h) |= ψ?

Obviously the validity problem is more general than the entailment problem and such a problem makes sense because formulae in SF are not closed under negation. Nevertheless, it is clear that the entailment can be defined for many other versions of separation logic. Note also that the rule for strengthening precedent (SP)

φ ⇒ ψ {ψ } C {ψ} {φ} C {ψ}
involves entailment checking. This is a building block of the verification process and in particular, proof checking requires that entailment problem is decidable, if not tractable at all. Whereas a coNP algorithm is provided in [START_REF] Berdine | A decidable fragment of separation logic[END_REF], the optimal complexity is established in [CHO + 11] by using an original approach: to represent formulae as graphs and to search for homomorphisms on these special graphs.

Theorem 4.10. [CHO + 11, Theorems 16 & 24] The entailment and satisfiability problems for SF can be solved in polynomial time. Indeed, it is quite surprising that the entailment problem is computationally tractable. A slight extension may easily lead to untractability. For instance considering the variant clause φ ::= φ p ∧ φ s ∧ φ s (i.e., allowing a bit of conjunction) already leads to coNP-hardness [CHO + 11]. The algorithm presented in [CHO + 11] has been implemented and used for automatic verification, see [START_REF] Haase | SeLoger: A tool for graph-based reasoning in separation logic[END_REF].

In [START_REF] Piskac | Automating separation logic using SMT[END_REF], an extension of SF is considered, called 1SLLB, in which formulae are Boolean combinations of pure formulae and spatial formulae.

Corollary 4.11. The satisfiability problem for 1SLLB is NP-complete. NP-hardness is an obvious consequence that 1SLLB contains equality constraints and it is closed under Boolean connectives. The NP upper bound follows from the linear-time reduction from 1SLLB to the logic of graph reachability and stratified sets (GRASS) [START_REF] Piskac | Automating separation logic using SMT[END_REF].

Fragments in polynomial space

Most probably, NP-completeness already implies non-tractability but actually, propositional separation logic of the form kSL0 with k ≥ 1 can be potentially of even worse complexity, see e.g. [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF][START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF].

Theorem 4.12. [COY01] For every k ≥ 1, the satisfiability problem for (propositional) kSL0 is PSPACE-complete.

The proof for the PSPACE upper bound is sketched in Section 5.1 in which other results about the expressive power of kSL0 are discussed. Meanwhile, below, we show that 1SL0 is PSPACE-hard by reduction from QBF, following developments from [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF].

Let Q 1 p 1 • • • Q n p n φ be a QBF formula with {Q 1 , . . . , Q n } ⊆ {∃, ∀}
and φ is a propositional formula built over the proposition variables in {p 1 , . . . , p n }. In the translation process, we consider n program variables, say x 1 , . . . , x n so that the truth of p i is encoded by the satisfaction of alloc(x i ). In order to encode independence between the different variables, we enforce that all the program variables have distinct values in the original heap (see also below). Moreover, existential quantification over p i amounts to restrict the current heap either by the empty heap (in that case alloc(x i ) holds in the other heap) or by a unique memory cell so that alloc(x i ) holds, which allows to simulate quantification. However, it is necessary to enforce in the initial heap that alloc(x i ) holds for any program variable x i . Let us define the map t as follows:

• t(p i ) def = alloc(x i ). • t is homomorphic for Boolean connectives. • t(∃ p i ψ) def = (emp ∨ (alloc(x i ) ∧ ¬(¬emp * ¬emp))))) * t(ψ). • t(∀ p i ψ) def = ¬((emp ∨ (alloc(x i ) ∧ ¬(¬emp * ¬emp))))) * ¬t(ψ)). One can check that Q 1 p 1 • • • Q n p n φ is QBF satisfiable iff ( i =j x i = x j ) ∧ ( i alloc(x i )) ∧ t(Q 1 p 1 • • • Q n p n φ) is 1SL0 satisfiable.
The above reduction implies that the satisfiability problem for kSL0( * ) is PSPACEhard too and other fragments have been considered in [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF] by restricting further the use of Boolean or separating connectives. For instance, the satisfiability problem for kSL0(- * ) is PSPACE-hard too. PSPACE upper bound can be pushed a bit further by allowing a unique quantified variable. reachability predicates can lead to decidable extensions (which would capture some version of separation logic considered in [START_REF] Thakur | Satisfiability modulo abstraction for separation logic with linked lists[END_REF]).

Non-elementary fragments

Reduction from PITL satisfiability to 1SL2( * ) satisfiability leads to the following lower bound since PITL satisfiability problem is known to have non-elementary complexity (see definition of PITL in Section 3.3).

Theorem 4.14. [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF] The satisfiability problem for 1SL2( * ) is decidable with nonelementary complexity.

Again, solving the satisfiability problem for 1SL2( * ) requires time bounded below by towers of exponentials of height that depend on the formula size, see e.g. [START_REF] Schmitz | Complexity hierarchies beyond elementary[END_REF].

We have seen that 1SL( * ) is decidable whereas satisfiability for full 1SL is undecidable. However, 1SL( * ) is certainly not the largest decidable fragment of 1SL. Below, we investigate another decidable extension of 1SL( * ) introduced in [BDL12, Section 4] thanks to a restricted use of the magic wand; quantification over disjoint heaps is done only for heaps whose domain has cardinality smaller than some fixed n. - * states the existence of a disjoint heap for which the cardinality of the domain is bounded by n. More formally, we require that (s, h)

|= f φ 1 n ¬ - * φ 2 iff there is h ⊥ h such that card(dom(h )) ≤ n, (s, h ) |= f φ 1 and (s, h h ) |= f φ 2 . 1SL( * + n ¬
- * ) allows to encode the restricted use of the magic wand in the Hoare-like proof systems as in the backward-reasoning form rule (MUBR) recalled below (see e.g. [START_REF] Reynolds | An Overview of Separation Logic[END_REF]).

Expressive Power

In this section, we take care of the expressive power for propositional separation logics but also for first-order separation logics (with different types of characterization). It is worth recalling a few well-known results about expressive power of modal or temporal logics. For instance, linear-time temporal logic LTL is known to be as expressive as first-order logic by Kamp's Theorem [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF] (see also [START_REF] Hodkinson | Separation -past, present, and future[END_REF][START_REF] Rabinovich | A Proof of Kamp's theorem[END_REF]). Monadic second-order logic (MSO) is another yardstick logic and, for instance, it is well-known that ω-regular languages (those definable by B üchi automata) are exactly those definable in MSO, see e.g. [START_REF] Straubing | Finite Automata, Formal Logic, and Circuit Complexity[END_REF]. Similarly, extended temporal logic ETL, defined in [START_REF] Wolper | Temporal logic can be more expressive[END_REF] and extending LTL, is also known to be equally expressive with MSO. On non-linear structures, bisimulation invariant fragment of MSO and modal µcalculus have been shown equivalent [START_REF] Janin | On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic[END_REF]. For sets of nodes, XPath has been established equally expressive as first-order logic with two quantified variables, see e.g. an overview in [START_REF] Marx | Semantic characterizations of navigational XPath[END_REF]. In the realm of interval temporal logics, we also know expressive completeness of metric propositional neighborhood logic with respect to the two-variable fragment of first-order logic for linear orders with successor function, interpreted over natural numbers [BDG + 10].

Boolean formulae for propositional separation logics

In this section, we provide a characterization of the expressive power of propositional separation logic 1SL0, and a similar analysis can be done for any kSL0 with k > 1.

Theorem 5.1. [Loz04a, Chapter 5] Any formula φ in 1SL0 built over the program variables in {x 1 , . . . , x q } is logically equivalent to a Boolean combination of atomic formulae among size ≥ k, alloc(x i ), x i → x j and x i = x j (k ∈ N, i, j ∈ {1, . . . , q}).

The formulae of the form size ≥ k and alloc(x i ) are introduced in Section 2.2 and we recall that alloc(x i ) holds when s(x i ) belongs to the heap domain and size ≥ k holds when the cardinal of the heap domain is at least k. By way of example (¬emp * (x 1 → x 2 - * ⊥)) is equivalent to size ≥ 2 ∧ alloc(x 1 ). Furthermore, the cardinal of the heap domain without the interpretation of x 1 and x 2 (in the case it belongs to the domain) is at least k ≥ 0, can be expressed as follows:

(alloc(x 1 ) ∧ alloc(x 2 ) ∧ size ≥ k + 2)∨ (((alloc(x 1 ) ∧ ¬alloc(x 2 )) ∨ (¬alloc(x 1 ) ∧ alloc(x 2 ))) ∧ size ≥ k + 1)∨ (¬alloc(x 1 ) ∧ ¬alloc(x 2 ) ∧ size ≥ k)
It is clear that such a formula can be generalized to any finite set of program variables. We write size q ≥ k to denote the atomic formula such that (s, h) |= size q ≥ k iff card(dom(h) \ {s(x i ) : i ∈ [1, q]}) ≥ k. Note that size ≥ k can be expressed as follows:

(x 1 = x 2 ∧ alloc(x 1 ) ∧ alloc(x 2 ) ∧ size 2 ≥ k -2)∨ (x 1 = x 2 ∧ alloc(x 1 ) ∧ size 2 ≥ k -1)∨ (((alloc(x 1 ) ∧ ¬alloc(x 2 )) ∨ (¬alloc(x 1 ) ∧ alloc(x 2 ))) ∧ size 2 ≥ k -1)∨ (¬alloc(x 1 ) ∧ ¬alloc(x 2 ) ∧ size 2 ≥ k)
It is clear that such a formula can be generalized to any q ≥ 1. So using atomic formulae of the form size ≥ k or size q ≥ k does not make a difference in terms of expressive power.

Theorem 5.1 can be viewed as a means to eliminate separating connectives * and - * and this is analogous to quantifier elimination in Presburger arithmetic for which periodicity constraints need to be introduced in order to eliminate the quantifiers (see e.g. [START_REF] Cooper | Theorem proving in arithmetic without multiplication[END_REF]). Similarly, the atomic formulae size ≥ k and alloc(x i ) would require the use of the separating connectives to be properly defined in 1SL0 but in the Boolean combinations, these formulae are understood as primitive.

Even though Theorem 5.1 provides a nice characterization of the expressive power for 1SL0, several features limit its application. First, Theorem 5.1 only deals with the propositional case but we know that this is close to the best we can hope for. Indeed, a similar result is established in [START_REF] Demri | Separation logic with one quantified variable[END_REF] for 1SL1 by enriching the set of atomic formulae and by polishing and extending material from [START_REF] Lozes | Expressivité des Logiques Spatiales[END_REF][START_REF] Brochenin | Reasoning about sequences of memory states[END_REF] but the extension to 1SL2 is not possible (see developments below). Moreover, neither Theorem 5.1 states how to compute the equivalent formula nor it provides a precise information about the maximal bound k in atomic formulae size ≥ k that are used to build a Boolean combination equivalent to φ in 1SL0. Actually, one can restrict k to be at most polynomial in the size of φ, assuming that formulae are encoded as finite trees (as opposed to a DAG encoding that would imply an exponential blow-up). This entails a small model property in which the cardinal of the heap domain is bounded, see e.g. [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF][START_REF] Calcagno | From separation logic to firstorder logic[END_REF]. This feature is at the core of the translation into first-order logic (with empty signature) designed in [START_REF] Calcagno | From separation logic to firstorder logic[END_REF] and it regains the PSPACE upper bound for the satisfiability problem for 1SL0 (and for 2SL0 too), see e.g. [CGH05, Section 3.4].

Below, let us be a bit more precise about the way to prove Theorem 5.1 and to explain the main steps to show the PSPACE upper bound, which is reminiscent to many proofs showing PSPACE upper bound for modal logics by using Ladner-like algorithms, see e.g. [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF][START_REF] Spaan | The complexity of propositional tense logics[END_REF]. More details can be found in [START_REF] Demri | Separation logic with one quantified variable[END_REF]. Let q, α ≥ 1. We write Test q,α to denote the following set of atomic formulae:

{x i = x j , x i → x j , alloc(x i ) : i, j ∈ [1, q]} ∪ {size q ≥ k : k ∈ [0, α]}
We define an equivalence relation ≈ q,α on the class of memory states, so that two models are in the same equivalence class whenever they cannot be distinguished by any formula in Test q,α : (s, h) ≈ q,α (s , h ) iff for all ψ ∈ Test q,α , we have (s, h) |= ψ iff (s , h ) |= ψ.

One can show that for any formula φ in 1SL0 with q ≥ 1 program variables and with size |φ| (for some reasonably succinct encoding), for any α ≥ |φ|, if (s, h) ≈ q,α (s , h ), then (s, h) |= φ iff (s , h ) |= φ. This result or some of its variants established in [START_REF] Lozes | Expressivité des Logiques Spatiales[END_REF][START_REF] Brochenin | Reasoning about sequences of memory states[END_REF][START_REF] Demri | Separation logic with one quantified variable[END_REF] entails that for checking the satisfaction of φ in some memory state, what matters is really the satisfaction of atomic formulae in Test q,|φ| . Theorem 5.1 is then a direct consequence of this property.

Corollary 5.2. Let φ be a satisfiable formula in 1SL0 with q program variables. Then there is memory state (s, h) such that (s, h) |= φ and ran(s

) ∪ dom(h) ∪ ran(h) ⊆ [0, q + |φ| + 1].
Satisfaction of φ depends only on the satisfaction of formulae from Test q,|φ| . So, to check satisfiability status of φ, only the truth value of formulae in Test q,|φ| matters. That is why, instead of operating on memory states to check satisfiability, it is sufficient to operate on its abstractions (with respect to the basic properties induced by Test q,|φ| ), whence the introduction of symbolic memory states. A symbolic memory state S over (q, α) is a structure ((V, E), n) such that:

(1) There is a partition P of {x 1 , . . . , x q } such that P ⊆ V . This encodes the store.

(2) (V, E) is a functional directed graph and a node v in (V, E) is at distance at most one of some set of variables X in P .

February 9, 2015 Journal of Applied Non-Classical Logics final-jancl15 1: if ψ is atomic then return AMC(S, ψ); 2: if ψ = ¬ψ 1 then return not MC(S, ψ 1 ); 3: if ψ = ψ 1 ∧ ψ 2 then return (MC(S, ψ 1 ) and MC(S, ψ 2 )); 4: if ψ = ψ 1 * ψ 2 then return iff there are S 1 and S 2 such that * a (S, S 1 , S 2 )

and MC(S 1 , ψ 1 ) = MC(S 2 , ψ 2 ) = ; 5: if ψ = ψ 1 - * ψ 2 then return ⊥ iff for some S and S such that * a (S , S , S), MC(S , ψ 1 ) = and MC(S , ψ 2 ) = ⊥; 1: if ψ is emp then return iff E = ∅ and n = 0; 2: if ψ is x i = x j then return iff x i , x j ∈ X, for some X ∈ P ; 3: if ψ is x i → x j then return iff (X, X ) ∈ E where x i ∈ X ∈ P and x j ∈ X ∈ P ; (3) n ∈ [0, α] and this corresponds to the number of locations in the heap domain that are not equal to the interpretation of some program variables in {x 1 , . . . , x q }.

Given q, α ≥ 1, the number of symbolic memory states over (q, α) is exponential in q + α. Given a memory state (s, h), we define its abstraction Symb[s, h] over (q, α) as the symbolic memory state ((V, E), n) such that

• n = min(α, card(dom(h) \ {s(x i ) : i ∈ [1, q]})).
• P is a partition of {x 1 , . . . , x q } so that for all x, x , we have s(x) = s(x ) iff x and x belong to the same set in P . • V is made of elements from P as well as of locations from the set below:

{h(s(x i )) : s(x i ) ∈ dom(h), i ∈ [1, q]} \ {s(x i ) : i ∈ [1, q]}
• The graph (V, E) is defined as follows:

(1) (X, X ) ∈ E if X, X ∈ P and h(s(x)) = s(x ) for some x ∈ X, x ∈ X .

(2) (X, l) ∈ E if X ∈ P and h(s(x)) = l for some variable x in X and l ∈ {s(x i ) : i ∈ [1, q]}.

We define symbolic memory states to be isomorphic if (1) the partition P is identical, (2) the finite digraphs agrees on the atomic formulae of the form either x i → x j or alloc(x i ), and (3) the numerical values are identical. Note that given a symbolic memory state S over (q, α), there exists a memory state (s, h) such that Symb[s, h] and S are isomorphic. Not only every symbolic memory state has always a concretization but also symbolic memory states are the right way to abstract memory states when the language 1SL0 is involved, which can be formally stated as follows: (s, h) ≈ q,α (s , h ) iff Symb[s, h] and Symb[s , h ] are isomorphic symbolic memory states. Definition 5.1. Given symbolic memory states S, S 1 and S 2 , we write * a (S, S 1 , S 2 ) if there exist a store s and disjoint heaps h 1 and h

2 such that Symb[s, h 1 h 2 ] = S, Symb[s, h 1 ] = S 1 and Symb[s, h 2 ] = S 2 . ∇
Given q, α ≥ 1, the ternary relation * a can be decided in polynomial time in q+log(α) for all the symbolic memory states built over (q, α).

Figure 2 presents a procedure MC(S, ψ) returning a Boolean value in {⊥, } and taking as arguments, a symbolic memory state over (q, α) and a formula ψ with |ψ| ≤ α. All the quantifications over symbolic memory states are done over (q, α). A case analysis is provided depending on the outermost connective of the input formula. Its struc- ture is standard and mimicks faithfully the semantics for 1SL0 except that we deal with symbolic memory states. The auxiliary function AMC(S, ψ) also returns a Boolean value in {⊥, }, makes no recursive calls and is dedicated to atomic formulae (see Figure 3). The design of MC is similar to nondeterministic polynomial-space procedures, see e.g. [Lad77, Spa93, COY01].

Lemma 5.3. Let q, α ≥ 1, S be a symbolic memory state over (q, α) and φ be in 1SL0 built over x 1 , . . . , x q such that |φ| ≤ α. We have MC(S, φ) returns iff there exists (s, h) such that Symb[s, h] = S and (s, h) |= φ.

Consequently, we get the following complexity characterization Theorem 5.4. Model-checking and satisfiability problems for 1SL0 are PSPACE-complete.

PSPACE-hardness is due of [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF] and it is briefly explained in Section 4.3.2. PSPACE upper bound is a consequence of Lemma 5.3 by recalling that φ is satisfiable iff there is a memory state (s, h) such that (s, h) φ iff there is an symbolic memory state S over (q, |φ|) such that MC(S, φ) = . It is sufficient to guess S and then check whether MC(S, φ) returns . All of this can be done in nondeterministic polynomialspace and by Savitch's Theorem [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF], we get the PSPACE upper bound.

Corollary 5.5. Given a formula φ in 1SL0, computing a Boolean combination of atomic formulae from Test q,|φ| logically equivalent to φ can be done in polynomial space.

Results for first-order separation logics

Recent results have provided some insight into the power of separation logic's secondorder features. [START_REF] Brochenin | On the almighty wand[END_REF] demonstrated expressive equivalence of 1DSOL and 1WSOL, and showed a translation of 1WSOL into 1SL(- * ). Recently, [START_REF] Demri | Expressive completeness of separation logic with two variables and no separating conjunction[END_REF] sharpens this result by showing that a translation from 1DSOL into the two-variable restriction 1SL2(- * ) is possible. The proofs in both of these works are constructive.

Theorem 5.6. [DD14, BDL12] There is a translation T from 1DSOL to 1SL2(- * ) such that for every sentence φ in 1DSOL and for every memory state (s, h), we have (s, h) |= φ in 1DSOL iff (s, h) |= T (φ) in 1SL2(- * ).

These translations can accommodate both program variables and additional record fields (see discussion in [DD14, Section 5.5]). Note that the reverse is also true, as shown earlier by Theorem 3.2. Since there exist translations in both directions between 1DSOL and 1SL, we have the following result.

Theorem 5.7. [DD14, BDL12] 1SL, 1SL2(- * ), 1DSOL, and 1WSOL have the same expressive power. Such a comparison of equivalence of expressive power is commonly sought with two-variable logics. There are a number of results comparing the expressive power of FO2 to other logics. Some examples include equivalence between unary LTL and FO2, see e.g. [START_REF] Etessami | First-order logic with two variables and unary temporal logics[END_REF][START_REF] Ph | Expressiveness and Succinctness of First-Order Logic on Finite Words[END_REF]. Boolean modal logic with converse and identity is as expressive as FO2 [START_REF] Lutz | Modal logic and the two-variable fragment[END_REF] (see also [START_REF] Hella | One-dimensional fragment of first-order logic[END_REF]).

Note also that, as shown in [START_REF] Lozes | Separation Logic: Expressiveness and Copyless Message-Passing[END_REF], Theorem 5.7 is a key argument to show that separation logic is complete for sequential mono-procedural programs, when separation logic is understood as a programming language, an assertion language and a set of rules involving Hoare triples. Completeness means that every valid Hoare triple (see Section 2.1.1) is derivable in a given proof system dealing with Hoare triples. Ob- viously, completeness depends on the programming language, on the assertion logic and on the set of inference rules. More details can be found in [START_REF] Lozes | Separation Logic: Expressiveness and Copyless Message-Passing[END_REF], see also related results in [START_REF] Calcagno | Local action and abstract separation logic[END_REF][START_REF] Tatsuta | Completeness of pointer program verification by separation logic[END_REF] or in [START_REF] Tatsuta | Completeness of Separation Logic with Inductive Definitions for Program Verification[END_REF].

Corollary 5.8. 1SL3(- * ) without the equality predicate is as expressive as 1SL2(- * ). This is a consequence of the material presented at the end of Section 2.2 where u = u can be shown equivalent to the formula below (u is a new quantified variable):

∀ u ((u → u) - * (u → u))
Note also that the satisfiability problem for 1SL2 without program variables is shown undecidable in [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF]. This can be refined even further by banishing the equality predicate in that fragment. Indeed, u = u can be shown equivalent to the formula below:

- * ¬(((∃ u (u → u)) ∧ ¬(∃ u (u → u))) * )
This follows a similar idea developed in [Loz04a, Section 5.1.1]. By contrast, the decidability status of 1SL2(- * ) without program variables and without equality is open. Similarly, the decidability status of 1SL(- * ) where → is replaced by → (exact points-to relation) is also open.

Using similar ideas, one can show that any formula in 1SL1 can be transformed into an equivalent formula in 1SL1 but without the equality predicate. Indeed, x i = x j is logically equivalent to ∀ u ((u → x i ) - * (u → x j )) and x i = u (in 1SL1, one quantified variable is allowed) can be eliminated by making a case analysis when first-order quantification is performed on u.

Since 1SL2(- * ) and 1WSOL have the same expressive power, this implies the following impossibility result.

Theorem 5.9. The set of valid formulae for 1SL is not recursively enumerable.

As a consequence, 1SL is not finitely axiomatizable and this refines Theorem 5.9. A quick argument for proving Theorem 5.9 consists in noting that second-order logic is not finitely axiomatizable and 1SL is equivalent to it, but this would be too sloppy since there are so many variants of second-order logic, and some of them are indeed finitely axiomatizable. In order to be more precise and to show Theorem 5.9, it is nevertheless sufficient to combine the following arguments.

• First-order theory of natural numbers with addition and multiplication is not recursively enumerable by G ödel's first incompleteness theorem. • There is a logarithmic-space reduction t 1 such that for any formula φ from firstorder arithmetic, φ is valid iff t 1 (φ) is valid in 1WSOL. To show this, it is sufficient to represent natural numbers by the cardinals of finite sets and to deal with addition and multiplication by performing equality tests between finite set cardinalities. This can be done by using dyadic or ternary predicate symbols, for instance to state the existence of some bijection between two finite sets. By way of example, the atomic formula u 1 × u 2 = u 3 amounts to check whether the product set made of the interpretation of the monadic second-order variables P 1 and P 2 has the same cardinality as the interpretation of the monadic second-order variable P 3 . Obviously, this assumes that each variable u i has a unique corresponding monadic second-order variable P i . So the formula u 1 × u 2 = u 3 can be encoded by:

∃ P PRODUCT(P, P 1 × P 2 ) ∧ EQCARD(P, P 3 )

where PRODUCT(P, P 1 × P 2 ) def = ∀ u, u P(u, u ) ⇔ P 1 (u) ∧ P 2 (u ). The formula EQCARD(P, P 3 ) stating that the interpretation of the binary second-order variable has the same cardinality as the interpretation of the unary second-order variable can be defined similarly, but this requires to introduce a ternary secondorder variable specified as a bijection between the two sets.

• As shown in [START_REF] Demri | Expressive completeness of separation logic with two variables and no separating conjunction[END_REF], there is a logarithmic-space reduction t 2 such that for any formula φ from 1WSOL, φ is valid iff t 2 (φ) is valid in 1SL2(- * ). Actually, it is sufficient to show the result for 1DSOL and then this can be extended to 1WSOL by encoding n-ary finite relations with n finite binary relations. For example, P(e 1 , . . . , e n ) can be encoded by the conjunction ∃ v n i=1 P i (e i , v) where P 1 , . . . , P n are new binary second-order variables attached uniquely to the n-ary secondorder variable P, see e.g. [BDL12, Proposition 2.6].

5.2.0.1 Allowing infinite domains. Let kSL ∞ be the variant of kSL in which the heap domain can be either finite or infinite (in kSL, the heap domain is necessarily finite). It is easy to show that the set of valid formulae for kSL ∞ without separating connectives is recursively enumerable, which contrasts with Theorem 4.2. Indeed, the heap can be encoded by a (k + 1)-ary relation that is functional on its first argument (no more cardinality constraint). By contrast, 1SL ∞ (with separating connectives) does not admit a recursively enumerable set of valid formulae (and this holds for any kSL ∞ with k ≥ 1) since finiteness of the heap domain can be expressed in 1SL ∞ itself. A heap h is segmented whenever dom(h) ∩ ran(h) = ∅ and no location has strictly more than one predecessor. There is a simple formula seg in 1SL2 that characterizes segmented heaps, see e.g. [START_REF] Demri | Expressive completeness of separation logic with two variables and no separating conjunction[END_REF]. Now, it is easy to show that infinite heaps can be characterized by the formula seg ¬ - * ∀ u alloc(u).

1SL( * ) versus 1MSOL

A standard tool to show non-expressibility in first-order logic or in second-order logic is to use Ehrenfeucht-Fraïssé games, see e.g. [START_REF] Libkin | Elements of Finite Model Theory[END_REF] (called EF-games in the sequel). These games have been adapted for some versions of separation logic, see e.g. [START_REF] Antonopoulos | Separating graph logic from MSO[END_REF][START_REF]Expressive Power of Query Languages[END_REF] based on similar games on spatial logics [DGG04, Mar06, DGG07].

Theorem 5.10. [AD09, Ant10] 1SL( * ) is strictly less expressive than 1MSOL.

In [AD09, Ant10], using EF-games, it is shown that there is no formula in 1SL( * ) that characterizes the forests of binary trees such that there is one binary tree whose number of leaves is a multiple of 3. Even though the principle of the method with EFgames is standard, the proof is quite complex and tedious, since it requires designing two families of heaps, to define an adequate strategy for the Duplicator player and to show that the strategy does the job, see e.g. [START_REF]Expressive Power of Query Languages[END_REF] for most of the details as well as for additional bibliographical references. In particular, Duplicator has a winning strategy for a game on (h 1 , h 2 ) with rank r iff h 1 and h 2 agree on all formulae of 1SL( * ) of rank r. See [START_REF]Expressive Power of Query Languages[END_REF] for more details about the notion of game and rank, for instance.

By way of example, we explain below why the above-mentioned property can be expressed in 1MSOL. First, let us express in 1SL( * ) that the heap is a forest of binary trees, which entails that this can be stated in 1MSOL too, see e.g. Section 4.2. It is models and does not deal with concrete heaps as in kSL. Still, it is possible to design complete proof systems for propositional logics, such as the tableaux-style calculus for 2SL0 in [START_REF] Galmiche | Tableaux and resource graphs for separation logic[END_REF] but completeness for full 2SL is not possible (see Theorem 4.2). The literature contains also a few attempts to design complete proof systems for some kSL. Graph-based decision procedures can be found in [START_REF] Haase | SeLoger: A tool for graph-based reasoning in separation logic[END_REF], which goes beyond 1SL0 (see also an NP-complete fragment of separation logic that can be decided using a model-theoretical decision procedure [START_REF] Enea | Compositional invariant checking for overlaid and nested linked lists[END_REF]). It is also possible to design Ladnerlike algorithm for kSL0 as witnessed by the works in [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF][START_REF] Demri | Separation logic with one quantified variable[END_REF], see also Section 5.1.

Satisfiability Modulo

Theories for separation logics 6.2.0.2 Direct approach versus translation for modal logics. In order to mechanize modal logics, there exist at least two main approaches with well-identified motivations. The direct approach consists in building specialized proof systems for the logics and requires building new theorem provers but, it has the advantage to design fine-tuned tools and to propose plenty of optimizations. The development of tableaux-based provers for modal logics following the seminal work [START_REF] Fitting | Proof methods for modal and intuitionistic logics[END_REF] perfectly illustrates this trend. By contrast, the translation approach consists in reducing decision problems for the original logics to similar problems for logics that have already well-established theorem provers. Its main advantage is to use existing tools and therefore to focus only on the translations, that are usually much simpler to implement. For example, translation of modal logics into first-order logic, with the explicit goal to mechanize such logics is an approach that has been introduced in [START_REF] Ch | Methods for automated theorem proving in non classical logics[END_REF] (see also [START_REF] Fine | Some connections between elementary and modal logic[END_REF][START_REF] Van Benthem | Correspondence Theory[END_REF][START_REF] Moore | Reasoning about knowledge and action[END_REF]) and it has been intensively developed over the years, see e.g. [START_REF] Ohlbach | Encoding two-valued non-classical logics in classical logic[END_REF] for an overview. 6.2.0.3 Translation versus specialized algorithms for separation logic. Despite its young age, one can observe that the mechanization of separation logic follows a similar dichotomy. This is all the more obvious nowadays since there are a lot of activities to develop verification methods with decision procedures for fragments of practical use, see e.g. [CHO + 11]. Many decision procedures have been designed for fragments of separation logics or abstract variants, from analytic methods [START_REF] Galmiche | Tableaux and resource graphs for separation logic[END_REF][START_REF] Hou | Proof search for propositional abstract separation logics via labelled sequents[END_REF] to translation to theories handled by SMT solvers [START_REF] Piskac | Automating separation logic using SMT[END_REF], passing via graphbased algorithms [START_REF] Haase | SeLoger: A tool for graph-based reasoning in separation logic[END_REF]. The translation approach has been already advocated in [START_REF] Calcagno | From separation logic to firstorder logic[END_REF] in which propositional kSL0 is translated into a fragment of classical logic that can be decided in polynomial space. However, the framework of satisfiability modulo theories (SMT) remains probably the most promising one to develop decision procedures dedicated to reasoning tasks for separation logics, see e.g [BPS09, RBHC07, PWZ13, DGLWM14]. It is worth noting that verification of programs that manipulate linked-list structures can be also done with a SAT solver, when the assertions are written in some restricted logical formalism, see a remarkable example in [IBI + 13].

6.2.0.4 SMT solvers, program verification, and separation logic. Deciding logical formulae within a given logical theory is ubiquitous in computer science and the works around Satisfiability Modulo Theories (SMT) are dedicated to solve this problem by providing methods, proof systems and solvers in order to be able to decide as much theories as possible, as well as their combination (see e.g. [START_REF] Barrett | Satisfiability Modulo Theories[END_REF]). Nowadays, SMT solvers are essential for most tools that formally verify programs, from bounded model-checking to abstraction-based model-checking (actually the number of appli-February 9, 2015 Journal of Applied Non-Classical Logics final-jancl15 cations seems unbounded). A nice feature of such solvers is their ability to combine distinct theories allowing to express richer statements. As advocated in [START_REF] Piskac | Automating separation logic using SMT[END_REF], being able to integrate decidable fragments of separation logic in some SMT solver not only allows to decide satisfiability or entailment problems by taking advantage of the technology behind SMT solvers but also it provides an efficient way to combine separation logics with other theories, such as linear arithmetic LIA. Actually, the seminal paper [START_REF] Piskac | Automating separation logic using SMT[END_REF] provides a translation of 1SLLB (see also Section 4.3.1) into a decidable fragment of first-order logic and a decision procedure has been implemented in an SMT solver. This provides an important step to integrate reasoning about tion logic into SMT solvers. Some strongly related work can be also found in [START_REF] Navarro Pérez | Separation Logic Modulo Theories[END_REF]. Besides, the first competition of solvers for several fragments of separation logic was held recently, see e.g. [START_REF] Sighireanu | Report on SL-COMP[END_REF], witnessing how promising appears this research direction. In the article [START_REF] Sighireanu | Report on SL-COMP[END_REF] reporting the competition SL-COMP 2014, more can be found about the list of solvers that competed as well as the fragments of separation logic that have been considered (roughly, symbolic heaps with recursive definitions, see also Sections 4.3.1 and 3.2).

Conclusion

In this paper, we have presented a wide range of results about separation logic as far as decidability, complexity (see e.g., Section 4), and expressive power are concerned while pinpointing several relationships with modal or temporal logics (see Section 3). Figure 4 summarizes some of these results. Like the most popular classes of non-classical logics in computer science such as description logic (see e.g. [BCM + 03]) or temporal logic (see e.g. [START_REF] Gabbay | Temporal Logic: Mathematical Foundations and Computational Aspects[END_REF]), separation logic encompasses a large set of different logical formalisms. More importantly, the early works on separation logic or on BI, see e.g. [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF][START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF][START_REF] Pym | Possible worlds and resources: the semantics of BI[END_REF], have been the source of many theoretical works and it led to the development of many tools, see e.g. [START_REF] Berdine | Smallfoot: Modular automatic assertion checking with separation logic[END_REF][START_REF] Calcagno | Compositional shape analysis by means of bi-abduction[END_REF][START_REF] Calcagno | Infer: An automatic program verifier for memory safety of C programs[END_REF][START_REF] Sighireanu | Report on SL-COMP[END_REF]. This is a remarkable example of logical formalism that has been developed so quickly in both directions, in a so short amount of time. Even though it is not reasonable to expect to present all the research directions about separation logic within a single paper (or even only its main theoretical results), the research has been essentially driven towards the improvement of automatic program analysis, extending significantly Hoare logic [START_REF] Hoare | An axiomatic basis for computer programming[END_REF]. That is why promising research directions include, for instance, a more extensive use of fine-tuned SMT solvers (see e.g. [START_REF] Piskac | Automating separation logic using SMT[END_REF]), the development of methods for general inductive predicates (see e.g. [AGH + 14]) or the design of generic proof systems (see e.g. [START_REF] Brotherston | Parametric completeness for separation theories[END_REF]). In some other respect, building new bridges between separation logics and, modal and temporal logics can certainly be beneficial to transfer known results or proof techniques from modal logic (see e.g. [START_REF] Brotherston | Parametric completeness for separation theories[END_REF]). 7.0.0.5 Acknowledgments. This survey has greatly benefited from discussions and exchanges with many colleagues that help us to clarify numerous questions while writing this paper. We would like to thank Timos Antonopoulos (Oxford University), Kshitij Bansal (New York University), Anuj Dawar (Cambridge University), Didier Galmiche (LORIA, Nancy), Rajeev Goré (Australian National University), Christoph Haase (LSV, Cachan), Lauri Hella (University of Tampere), Zhe Hou (Australian National University), Dominique Larchey-Wendling (LORIA, Nancy), Etienne Lozes (LSV, Cachan), Daniel Mery (LORIA, Nancy), Ben Moszkowski (De Montfort University), Alwen Tiu (Nanyang Technological University), Heribert Vollmer (Leibniz Universität, Hannover), Thomas Wies (New York University), Zhilin Wu (LIAFA, Paris).

We would like also to thank two anonymous reviewers for their suggestions and remarks that help us to improve the quality of the manuscript.

Figure 1 .

 1 Figure 1. Disjoint memory states with one record fieldEach edge in the graphical representation of the heap h corresponds to a unique edge in the graphical representation of either h 1 or h 2 .For every k ≥ 1, formulae of kSL are built from expressions of the form e ::= x | u where x ∈ PVAR and u ∈ FVAR, and atomic formulae of the form

  [e] = [e ], with [x] def = s(x) and [u] def = f(u). • (s, h) |= f e → e 1 , . . . , e k iff [e] ∈ dom(h) and h([e]) = ([e 1 ], . . . , [e k ]).

February

π

  ::= e = e | e → e 1 , . . . , e k | P(e 1 , . . . , e n ) | emp | ⊥ Formulae of kWSOL are defined by the grammar φ, ψ ::= π | φ ∧ ψ | ¬φ | ∃ u φ | ∃ P φ

February

February

  Roughly speaking, a pair in R is encoded by a memory cell in h. Let us define the translation T such that φ has a finite model (D, R) iff T (φ) is satisfiable in 2SL with T (φ) def = ∃u, nil "non-empty domain" (u → nil, nil) ∧ "nil not in domain" (¬∃u , u nil → u , u ) ∧t(φ)

February

February

  Corollary 4.8.[START_REF] Demri | Two-variable separation logic and its inner circle[END_REF] The satisfiability problem for MLH( * ) is decidable.

Theorem 4. 13 .

 13 [START_REF] Demri | Separation logic with one quantified variable[END_REF] The satisfiability problem for 1SL1 is PSPACE-complete. PSPACE-hardness is inherited from the PSPACE-hardness of 1SL0 whereas the PSPACE upper bound requires an adequate abstraction. It is open whether 1SL1 extended with February 9, 2015 Journal of Applied Non-Classical Logics final-jancl15

  Let us define 1SL( * + n ¬ - * ) as an extension of 1SL( * ) by adding the binary operators n ¬ - * for every n ∈ N. Unlike - * , a formula with outermost connective n ¬

{

  (∃z x → z) * ((x → y) - * φ)} [x] := y {φ} Note that (x → y) - * φ is logically equivalent to ¬((x → y) 1 ¬ - * ¬φ). Theorem 4.15. [BDL12, Theorem 4.9] (I) There is a polynomial-time reduction from the 1SL( * + n ¬ - * ) satisfiability problem to the 1SL( * ) satisfiability problem. (II) 1SL( * + n ¬ - * ) satisfiability problem is decidable.

February

February

Figure 2 .

 2 Figure 2. Function MC(S, ψ)

Figure 3 .

 3 Figure 3. Function AMC(S, ψ)

February

February

1SL≡

  1DSOL ≡ 1WSOL ≡ 1SL(- * ), undec. [BDL12] dec., non-elem. [BDL12] 1SL2(- * ) ≡ 1DSOL, undec. [DD14] 1SL2( * ) dec., non-elem. [DD15] 1SL1 PSPACE-C. [DGLWM14] kSL0 PSPACE-C. [COY01] MLH( * ) dec., non-elem. [DD15] 1SLLB NP-C. [PWZ13] SF in P [CHO + 11] 1SL3( * )[Z, =] undec. [BBL09]1SL sdc < dec.[START_REF] Bansal | Beyond shapes: Lists with ordered data[END_REF]

Figure 4 .

 4 Figure 4. A few results about decidability and complexity

* Work partially supported by the EU Seventh Framework Programme under grant agreement No. PIOF-GA-2011-301166 (DATAVERIF). This survey paper follows an invited talk given at AIML'14, Groningen, August 2014.

† Work partially supported by the Air Force Office of Scientific Research under award FA9550-09-1-0596, and the National Science Foundation under grant 0644299. * See also the ANR project DYNRES at http://anr-dynres.loria.fr/ partly dedicated to abstract separation logics to reason about resources.

sufficient to state that every location has at most two predecessors and every location l can reach a non-allocated location (the root of the tree to which l belongs too if l is in the domain of the heap):

Note that the quantification above is fine even when u is not in the heap domain (take the value for u to witness the satisfaction of ∃ u (reach(u, u) ∧ ¬alloc(u))). In order to express in 1MSOL that there is a binary tree whose number of leaves is a multiple of 3, we first identify the locations of the tree (via the second-order variable P), we label each location of the tree by either P 0 , P 1 and P 2 (depending on the number of leaves (modulo 3) below the location) and we state consistency constraints (obviously simulating the behavior of some bottom-up three-state tree automaton) and finally we require that the root of the tree is labelled by P 0 . The formula defined below assumes that the heap is already known as a forest of binary trees.

∃ u (¬alloc(u) ∧ u ≥ 1) ∧ ∃ P, P 0 , P 1 , P 2 ((∀ u P(u) ⇔ reach(u, u)) ∧ (P = P 0 P 1 P 2 ) ∧ P 0 (u) ∧

Note that we used a shortcut formula (P = P 0 P 1 P 2 ) to state that the interpretation of P is the disjoint union of the interpretation of P 0 , P 1 and P 2 , details are omitted.

A Discussion about Decision Procedures and Calculi

In this section, mainly, we provide pointers about proof systems for separation logics, from sequent-style calculi to decision procedures built on SMT solvers.

Analytic proof systems

In the previous sections, we have seen that for any k ≥ 1, the set of valid formulae for kSL is not recursively enumerable and therefore there is no hope to design finite axiomatization for kSL and to design nice sequent-style proof systems. Nevertheless, calculi exist for abstract separation logics, mostly because first-order conditions are involved in separation models, see e.g. the conditions in [START_REF] Hou | Proof search for propositional abstract separation logics via labelled sequents[END_REF]. Similarly, display calculi for bunched logics can be found in [START_REF] Brotherston | Bunched logics displayed[END_REF]. Hilbert-style axiomatizations can be also found in [START_REF] Brotherston | Parametric completeness for separation theories[END_REF] by using nominals but again this involves mainly abstract separation