Stéphane Demri

Raul Fervari

On the Complexity of Modal Separation Logics

Keywords: separation logics, relation-changing logics, satisfiability, model-checking, complexity, expressive power

We introduce a modal separation logic MSL whose models are memory states from separation logic and the logical connectives include modal operators as well as separating conjunction and implication from separation logic. With such a combination of operators, some fragments of MSL can be seen as genuine modal logics whereas some others capture standard separation logics, leading to an original language to speak about memory states. We analyse the decidability status and the computational complexity of several fragments of MSL, leading to surprising results, obtained by designing proof methods that take into account the modal and separation features of MSL. For example, the satisfiability problem for the fragment of MSL with 3, the inequality modality = and separating conjunction * is shown Tower-complete whereas the restriction either to 3 and * or to = and * is only NP-complete.

Introduction

Combining modalities and separating connectives. Separation logic is known as an assertion language to perform verification, by extending Hoare-Floyd logic in order 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]. Local reasoning is a key feature of separation logic and the separating conjunction * allows us to state properties in disjoint parts of the memory. Moreover, the separating implication - * asserts that whenever a fresh heap satisfies a property, its composition with the current heap satisfies another property. Hence, the separating connectives * and - * allow us to evaluate formulae in alternative models, which is a feature shared with many modal logics such as sabotage logics [START_REF] Van Benthem | An Essay on Sabotage and Obstruction, in: Mechanizing Mathematical Reasoning[END_REF][START_REF] Löding | Model checking and satisfiability for sabotage modal logic[END_REF], logics of public announcements (see e.g., [START_REF] Lutz | Complexity and succinctness of public announcement logic[END_REF]), interval temporal logics [START_REF] Hodkinson | Non-finite axiomatizability and undecidability of interval temporal logics with C, D, and T[END_REF] or relation-changing logics [START_REF] Aucher | Global and local graph modifiers[END_REF][START_REF] Areces | Relation-Changing Modal Operators[END_REF].

Many other examples of such logics can be found in the literature (see also [START_REF] Dawar | Expressiveness and complexity of graph logic[END_REF]) but the modalities involved in such logics can be of a different nature. For instance, combinations of epistemic logics and abstract separation logics (such as variants of BI) can be found in [START_REF] Courtault | A modal BI logic for dynamic resource properties[END_REF][START_REF] Galmiche | A substructural epistemic resource logic[END_REF]. Sometimes, the concept of separation is different and perform at a different level, for instance a simple separation logic is introduced in [START_REF] Herzig | A simple separation logic[END_REF] in which separation is performed on valuations instead of being performed on heaps. A slightly different approach including description logics [START_REF] Baader | An Introduction to Description Logic[END_REF] was investigated in [START_REF] Georgieva | Description logics for shape analysis[END_REF][START_REF] Calvanese | Shape and content -A database-theoretic perspective on the analysis of data structures[END_REF]. An interesting attempt to get a logic (namely CT 2 ) that captures both a very expressive description logic and a separation logic (the symbolic heap fragment) can be found in [START_REF] Calvanese | Shape and content -A database-theoretic perspective on the analysis of data structures[END_REF].

Our motivations. Most existing logics combining (epistemic, temporal, etc.) modalities and separating connectives are multi-dimensional logics and the modal dimension is often orthogonal with the separation dimension (see e.g. [START_REF] Brochenin | Reasoning about sequences of memory states[END_REF][START_REF] Courtault | A modal BI logic for dynamic resource properties[END_REF][START_REF] Galmiche | A substructural epistemic resource logic[END_REF]), which allows to get proof methods combining adequately the modal part and the separation part. Our intention in this work is to introduce a modal separation logic whose models are Kripke-style structures that can be also viewed as memory states from separation logic, without being multidimensional. As a gain, it is possible to study the computational effects of the interaction between modalities and separating connectives but within a uniform framework and to push further the expressive power of the underlying modal logics as well as the expressive power of the underlying separation logics. Adding modalities to separation logics happens to be an original means to work on fragments of first-order separation logics. So, the logic MSL introduced herein can be understood as a hybrid separation logic, by analogy to hybrid versions of modal logics [START_REF] Blackburn | Representation, reasoning, and relational structures: a hybrid logic manifesto[END_REF]. Note that a hybrid extension of Boolean BI is defined in [START_REF] Brotherston | Parametric completeness for separation theories[END_REF], in which nominals are interpreted by heaps whereas herein, the nominals are interpreted by locations.

Our contributions. We introduce the logic MSL whose models are Kripkestyle structures with domain N (understood as the set of locations) and the accessibility relation is finite and functional (understood as some heap h : N → f in N). In MSL, the modal connectives are Q and the inequality modality = [START_REF] De Rijke | The modal logic of inequality[END_REF] whereas the separating connectives are the separating conjunction * and separating implication - * (also known as the magic wand operator). These connectives allow to update dynamically the model under evaluation. Therefore, in MSL, Q provides a means to move within the model following the accessibility relation, = adds the possibility to jump to (almost) any location of the model, and the connectives * and - * , removes or adds edges in the model respectively. The closest logic to MSL is probably the modal logic of heaps MLH [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF] since they share the same class of frames. However, there are differences, notably MSL has propositional variables (unlike MLH whose atomic formulae are truth constants) and MSL does not contain the converse modality and the reflexive transitive closure modality. Moreover, MSL shares with some logics from [START_REF] Larchey-Wendling | Nondeterministic phase semantics and the undecidability of Boolean BI[END_REF][START_REF] Brotherston | Undecidability of propositional separation logic and its neighbours[END_REF] the feature of having propositional variables whose interpretation is unrestricted but in such logics, the propositional variables are interpreted as sets of memory states whereas in MSL, the variables are interpreted as sets of locations, as usual for modal logics.

• MSL restricted to Q and * , written MSL( * , Q), can be viewed as the min-imal modal separation logic as it witnesses a simple interaction between Q and, on the other side * and emp (formula stating that the heap domain is empty). By showing a small model property, we establish that the satisfiability problem for MSL( * , Q) is NP-complete. The same result is shown for MSL( * , = ) by adapting arguments for the logic of elsewhere [START_REF] Segerberg | A note on the logic of elsewhere[END_REF][START_REF] Demri | A simple tableau system for the logic of elsewhere[END_REF]. To obtain the NP upper bound, we need to show that underlying modelchecking problems are in P, which requires a refined analysis as the model checking problem for propositional separation logic (even restricted to * ) is already PSpace-complete [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF].

• As far as decidability is concerned, we show that the satisfiability problem for MSL( * , Q, = ) is decidable by translation into the weak monadic second-order theory of one unary function shown decidable in [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF]. This extends the decidability proof of 1SL( * ) from [START_REF] Brochenin | On the almighty wand[END_REF] as, now, propositional variables need to be taken into account. More surprisingly, even though both MSL( * , Q) and MSL( * , = ) are NP-complete, we establish that the satisfiability problem for MSL( * , Q, = ) is Tower-hard by reduction from the nonemptiness problem for star-free expressions [START_REF] Meyer | Word problems requiring exponential time[END_REF][START_REF] Stockmeyer | The complexity of decision problems in automata theory and logic[END_REF][START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF].

To do so, we show an essential property: the formula ∃ x, y ls(x, y) from separation logic (see e.g. [START_REF] Berdine | A decidable fragment of separation logic[END_REF][START_REF] Cook | Tractable reasoning in a fragment of separation logic[END_REF]) can be expressed in MSL( * , Q, = ), which allows us to encode finite words. The notion of Tower-completeness is borrowed from [START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF].

• Using the fact that ls(x, y) can be expressed in MSL( * , Q, = ) we also establish that MSL (i.e. MSL( * , Q, = ) augmented with the magic wand - * ) admits an undecidable satisfiability problem by using the recent result from [START_REF] Demri | The effects of adding reachability predicates in propositional separation logic[END_REF] about the undecidability of propositional separation logic (with * and - * ) augmented with the list segment predicate ls.

• Along the paper, we also investigate variants of MSL (or some of its fragments) by slightly modifying the semantics or by adding other modal connectives. For instance, we provide a reduction from the satisfiability problem for MSL( * , Q) when the models are arbitrary countable Kripke-style models into global sabotage logic over general models [START_REF] Areces | Undecidability of relation-changing modal logics[END_REF].

Preliminaries

In this section we introduce the modal separation logic MSL, as well as several fragments that we briefly compare with propositional separation logic.

Modal separation logic MSL

Let PROP = {p 1 , q 1 , p 2 , q 2 , . . .} be a countably infinite set of propositional variables. Formulae for the logic MSL are defined by the grammar below:

φ ::= p | emp | ¬φ | φ ∨ φ | Qφ | = φ | φ * φ | φ - * φ,
where p ∈ PROP. An MSL model is a tuple M = N, R, V such that R ⊆ N×N is finite and functional, and V : PROP → P(N). Since separation logics are interpreted on structures representing heaps, our formulas are interpreted on models where the accessibility relation is finite and functional. The models

M 1 = N, R 1 , V and M 2 = N, R 2 , V are disjoint if R 1 ∩ R 2 = ∅;
M, l |= p def ⇔ l ∈ V(p) M, l |= emp def ⇔ R = ∅ M, l |= Qφ def ⇔ M, l |= φ, for some l ∈ N such that (l, l ) ∈ R M, l |= = φ def ⇔ M, l |= φ, for some l ∈ N such that l = l M, l |= φ 1 * φ 2 def ⇔ N, R 1 , V , l |= φ 1 and N, R 2 , V , l |= φ 2 , for some partition {R 1 , R 2 } of R M, l |= φ 1 - * φ 2 def ⇔ for all M = N, R , V such that R∪R is finite and functional, and R ∩ R = ∅, we have M , l |= φ 1 implies N, R ∪ R , V , l |= φ 2 .
The semantics for the modal operators and the separating connectives is the standard one, see e.g. [START_REF] Blackburn | Modal Logic[END_REF][START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF]. Other standard connectives or formulae are used:

• [ =]φ def = ¬ = ¬φ and Pφ def = ¬Q¬φ, • U φ def = φ ∨ = φ and [U]φ def = ¬ U ¬φ, • ! φ def = U (φ ∧ [ =]
¬φ) (unicity of the satisfaction of φ),

• the atomic formula size = 1 is a shortcut for ¬emp ∧ ¬(¬emp * ¬emp).

The satisfiability problem for the logic MSL, takes as input a formula φ and asks whether there exist an MSL model M and a location l such that M, l |= φ. Not only our study includes MSL but above all, we also deal with fragments. For instance, the fragment with Boolean connectives and Q is the basic modal logic ML. Otherwise, as a convention, we always consider the Boolean part and the emptiness constant emp, and we put between parentheses the rest of (separating or modal) connectives we are considering. The main logics we consider are MSL( * , Q), MSL( * , = ) and MSL( * , Q, = ).

Nominals, program variables and separation logic in a nutshell

In all the fragments of MSL containing the inequality modality [START_REF] De Rijke | The modal logic of inequality[END_REF], it is known that nominals from hybrid logics [START_REF] Blackburn | Representation, reasoning, and relational structures: a hybrid logic manifesto[END_REF] can be used since stating that p holds true in a unique location can be expressed by ! p. So, we can freely use nominals. Syntactically, nominals are taken from PVAR = {x, y, . . .}, that is actually also used as the set of program variables in separation logic (see below). Indeed, nominals and program variables are both interpreted by locations, as noticed in [START_REF] Georgieva | Description logics for shape analysis[END_REF]. So, checking the satisfiability status of a formula φ containing x 1 , . . . , x n actually amounts to checking the satisfiability status of ( 1≤i≤n ! x i ) ∧ φ. A formula φ is said to be global iff its satisfaction does not depend on the location and we simply write M |= φ (instead of M, l |= φ). Below, we show why these formulae are important to compare MSL with separation logics. Indeed, MSL behaves as a standard modal logic since the satisfaction relation has three arguments (a model, a location and a formula) but it can be also presented as a separation logic so that the satisfaction relation takes only two arguments, a model and a global formula. Let us briefly explain why separation logic can be viewed as a fragment of MSL. A memory state is a pair (s, h) such that s : PVAR → N (the store) and h : N → fin N is a partial function with finite domain (the heap). Models of the separation logic SL( * , - * ) are memory states. When the respective domains of the heaps h 1 and h 2 are disjoint, we write h 1 h 2 to denote the heap corresponding to the disjoint union of h 1 and h 2 . Formulae of SL( * , - * ) are built from

φ ::= x = y | x → y | emp | ¬φ | φ ∧ φ | φ * φ | φ - * φ,
where x, y ∈ PVAR. The satisfaction relation |= is defined as follows:

(s, h) |= x = y def ⇔ s(x) = s(y) (s, h) |= emp def ⇔ dom(h) = ∅ (s, h) |= x → y def ⇔ s(x) ∈ dom(h) and h(s(x)) = s(y) (s, h) |= φ 1 * φ 2 def ⇔ there are h 1 and h 2 such that h 1 h 2 = h, (s, h 1 ) |= φ 1 and (s, h 2 ) |= φ 2 (s, h) |= φ 1 - * φ 2 def ⇔ for all h 1 , if (dom(h 1 ) ∩ dom(h) = ∅ and (s, h 1 ) |= φ 1 ), then (s, h h 1 ) |= φ 2 .
Any memory state (s, h) can be viewed as the MSL model M = N, R, V such that R = {(l, h(l)) | l ∈ dom(h)} and the restriction of V to PVAR is equal to s. Actually, any formula φ of SL( * , - * ) is satisfiable iff t(φ) is satisfiable in MSL where t is homomorphic for Boolean and separating connectives and,

t(x = y) def = U (x ∧ y) t(emp) def = emp t(x → y) def = U (x ∧ Qy).
It is worth noting that each formula t(φ) is a global formula of MSL.

Alternative semantics

A general model M = W, R, V is such that W is an arbitrary countable set, R ⊆ W × W and V : PROP → P(W). This corresponds to standard (countable) Kripke structures with no frame condition. A finite and functional model M = W, R, V is such that W is a finite set, R ⊆ W × W is functional and V is a valuation. Without loss of generality, we assume W ⊆ N. Each syntactic fragment L of MSL gives rise to the logic L f (resp. L g ) where the models for L f are finite and functional models (resp. are general models). When L includes - * , the definition of |= for L g is updated as follows:

M, l |= φ 1 - * φ 2 def ⇔ for all M = W, R , V such that R ∩ R = ∅ M , l |= φ 1 implies W, R ∪ R , V , l |= φ 2 .
Note that the formula ( - * ¬((¬emp) - * ⊥)) is valid for MSL but not for MSL f . The model-checking problem for MSL f is defined in the usual way. As MSL can be viewed as a fragment of second-order logic (the second-order feature is needed to internalise the semantics of separating connectives), the model-checking problem for MSL f is in PSpace. More surprisingly, we show that the restriction to either

MSL f ( * , = ) or MSL f ( * , Q) is in P, whereas the restriction to MSL f ( * , Q, = ) is already untractable. Lemma 2.1 The model-checking problem for MSL f ( * , Q, = ) is PSpace- hard. Proof 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 {p 1 , . . . , p n } and the Boolean connectives ∧, ∨ and ¬ (only in front of atomic propositions). Satisfiability problem for QBF formulae is known to be PSpace-complete [START_REF] Stockmeyer | The polynomial-time hierarchy[END_REF].

In the reduction of

ϕ = Q 1 p 1 • • • Q n p n φ, we introduce a finite and func- tional model M n = W, R, V with W = [0, 2n] such that Q 1 p 1 • • • Q n p n φ is satisfiable iff M n , 0 |= t(ϕ), where t(•) is recursively defined below. The truth of the propositional variable p i in QBF subformulae is encoded by the satisfaction of the formula = (p i ∧ p ∧ Q ) from MSL f ( * , Q, = ).
First, let us complete the definition of M n over the propositional variables {p , p 1 , . . . , p n }.

V(p i ) def = {i, n + i}, for all i = 1, . . . , n V(p ) def = [1, n] R def = {(i, 0) | i ∈ [1, 2n]}. 0 M n p 1 p p 1 . . . p n p p n
Let us define the map t as follows (homomorphic for Boolean connectives):

t(p i ) def = = (p i ∧ p ∧ Q ) t(∃ p i ψ) def = (size = 1 ∧ = (p i ∧ Q )) * t(ψ) t(∀ p i ψ) def = ¬((size = 1 ∧ = (p i ∧ Q )) * ¬t(ψ)).
For every j ∈ [1, n + 1], we write φ j to denote the formula

Q j p j • • • Q n p n φ.
By definition, we have

φ 1 = Q 1 p 1 • • • Q n p n φ and by convention φ n+1 = φ.
Given a model M ⊆ M n and a propositional valuation v, we write M ≈ j v to denote the fact that:

• For all i ∈ [1, j -1], exactly one location in {i, n + i} has an outgoing edge.

• For all i ∈ [j, n], all the locations in {i, n + i} have an outgoing edge.

• For all i ∈ [1, j -1], i has an outgoing edge iff v(p i ) = .

By induction on j, one can show that for all

j ∈ [1, n + 1], if M ≈ j v, then M, 0 |= t(φ j ) iff v |= φ j . Details are omitted. So, as M n ≈ 1 v for any v, we have v |= ϕ iff M n , 0 |= t(φ 1 ). As ϕ is a closed formula and φ 1 = ϕ, ϕ is satisfiable iff M n , 0 |= t(ϕ). P
MSL can be seen as a logic with the ability to add or remove edges from the accessibility relation, closely related to relation-changing modal logics [START_REF] Areces | Relation-Changing Modal Operators[END_REF]. Below, we discuss the connections between MSL and the global sabotage logic MSL g (Q, gsb ). Formulae of MSL g (Q, gsb ) extends those of ML by adding the operator gsb interpreted over general models M = W, R, V as:

M, l |= gsb φ def ⇔ for some (l , l ) ∈ R, M - l ,l , l |= φ, where M - l ,l = W, R \ {(l , l )}, V . MSL g (Q, gsb
) can be encoded into MSL g ( * , Q) by the translation t that is homomorphic for Boolean connectives and for Q and, t( gsb φ)

def = (size = 1) * t(φ). We have φ is satisfiable iff t(φ) is satisfiable for MSL g ( * , Q). Similarly, MSL(Q, gsb ) is the variant of MSL g (Q, gsb ) with MSL models.

Decision problems in Tower

Below, we establish that the satisfiability problem for MSL( * , Q, = ) is in Tower [START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF], the class of problems of time complexity bounded by a tower of exponentials, whose height is an elementary function of the input. To do so, we design a reduction to the satisfiability problem for MSL f ( * , Q, = ) and then we show that the satisfiability problem for MSL f ( * , Q, = ) is in Tower by translation into the weak MSO theory of one unary function. Notice that the difference between MSL( * , Q, = ) and MSL f ( * , Q, = ) is that models in MSL( * , Q, = ) have finite relations over an infinite set of locations, while the set of locations in MSL f ( * , Q, = ) models is finite. This proof is analogous to the decidability proof for 1SL( * ) in [START_REF] Brochenin | On the almighty wand[END_REF] but our main technical task is to solve the satisfiability problem for MSL( * , Q, = ) by using only propositional variables that hold true on a finite amount of locations. First, we show that locations satisfying the same propositional variables and with no successor satisfy the same formulae. Lemma 3.1 Let p 1 , . . . , p n be propositional variables, M = N, R, V be a model and l = l be locations such that R(l) = R(l ) = ∅ and, l and l agree on p 1 , . . . , p n . For all φ in MSL( * , Q, = ) built over p 1 , . . . , p n , M, l |= φ iff M, l |= φ.

Let φ in MSL( * , Q, = ) be built over p 1 , . . . , p n . Let us define T (φ) as

T (φ) def = φ ∧ X⊆{p1,...,pn} U (P ⊥ ∧ p∈X p ∧ p ∈X ¬p ∧ = (P ⊥ ∧ p∈X p ∧ p ∈X ¬p)).
When = is not present, the second conjunct can be removed (see Lemma 4.3, where we take T (φ) = φ). Such a conjunct states that there are two distinct locations with no successor that agree on propositional variables from X and it is needed since ! p ∧ [U]p is satisfiable for MSL f ( * , = ) but not for the logic MSL( * , = ).

Lemma 3.2 φ is satisfiable in MSL( * , Q, = ) iff T (φ) is satisfiable in MSL f ( * , Q, = ).
The complexity class Tower has been introduced in [START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF] and sits between the class of elementary problems and the class of primitive recursive problems. By Lemma 3.2, there is a reduction from the satisfiability problem for MSL( * , Q, = ) into the satisfiability problem for MSL f ( * , Q, = ) that works in exponential time. There is also a (logspace) reduction from the satisfiability problem for MSL f ( * , Q, = ) into the satisfiability problem for the weak MSO theory of one unary function whose structures are D, f, = where D is a countable domain, f is a unary function ('weakness' refers to the fact that the monadic predicates are interpreted by finite sets). This theory is decidable, see e.g. [9, Corollary 7.2.11] and it can be shown in Tower as it can be reduced to the satisfiability to the MSO theory of the infinite binary tree. In the proof of Theorem 3.3, the reduction from MSL f ( * , Q, = ) simply internalises its semantics by using the (weak) second-order feature of the target logic.

In order to conclude this section, we consider the standard converse modality Q -1 (not originally in MSL), when it interacts with separating connectives. More precisely, M, l

|= Q -1 φ def ⇔ M, l |= φ, for some l ∈ N such that (l , l) ∈ R.
Although replacing Q by Q -1 does not sound as leading to a major variant, we will show that Q -1 already brings new difficulties.

Theorem 3.4

The satisfiability problem for MSL( * , Q -1 ) is PSpace-hard as well as the model-checking problem for MSL f ( * , Q -1 ).

Note that MSL( * , Q -1 ) contains MSL(Q -1 ) that can be viewed as a slight variant of the modal logic K on finite trees, known to admit a PSpace-complete satisfiability problem. So, PSpace-hardness of the satisfiability problem for MSL( * , Q -1 ) is quite expected.

By using the proof technique from the proof of Theorem 3.3, we can establish the result below where Q -1 is part of the modal operators. As a conclusion, there is a huge gap for MSL( * , Q -1 ) between the PSpacehardness for the satisfiability problem and the Tower upper bound.

NP-complete fragments of MSL

In this section, we show that the satisfiability problems for MSL( * , Q) and for MSL( * , = ) are NP-complete. In order to establish the NP upper bound, we reduce the problems to their variants with finite and functional models, we show a linear-size model property and finally, we prove that the model-checking problems are in P, dealing in each case with particular technical difficulties.

The minimal modal separation logic MSL( * , Q)

To show that MSL( * , Q) has a linear-size model property (i.e., the cardinal of the relation can be bounded), we introduce an equivalence relation s,n ∼ (s ≥ 0 is a parameter about the number of edges and n ≥ 1 is a parameter about the propositional variables) such that s,n ∼ -equivalent models satisfy the same formulae with less than s syntactic resources (to be defined) and built over {p 1 , . . . , p n }. First, we need to explain how to decompose models with respect to the parameters s and n and, the relation to at most the s first steps from a given location as well as the total number of edges, counting up to s. Below, we show that this abstraction is correct with respect to the expressive power of MSL( * , Q), see e.g. Lemma 4.2. Let M = N, R, V be a model, l ∈ N and s ≥ 0, we define W l,s and R l,s as follows.

• W l,s

def = {(i, l i ) | i ∈ [0, s], ∃ l 0 , . . . , l i , l = l 0 Rl 1 • • • Rl i-1 Rl i }. We also write t l = max{i | (i, l i ) ∈ W l,s } (so t l ≤ s). • R l,s def = {(l i , l i+1 ) | i ∈ [0, t l -1]
and (i, l i ), (i + 1, l i+1 ) ∈ W l,s }. We also write s l def = card(R l,s ) and rem l = min(s -card(R l,s ), card(R \ R l,s )). So, s l ≤ t l ≤ s and s l + rem l ≤ s.

Let M, M be models, l, l ∈ N and s ≥ 0, n ≥ 1 such that W l,s and R l,s are defined as above and W l ,s and R l ,s are related to M , l and s. Let us define the relation

s,n ∼ : M, l s,n ∼ M , l def
⇔ the conditions below are satisfied:

• We have t l = t l ( def = t). Say, W l,s = {(0, l 0 ), . . . , (t, l t )} and W l ,s = {(0, l 0 ), . . . , (t, l t )}.

• For all i ∈ [0, t], l i in M and l i in M agree on {p 1 , . . . , p n } ⊂ PROP.

• For all i, j ∈ [0, t -1], we have

l i = l j iff l i = l j . Hence, s l = s l ( def = s ). • We have rem l = rem l ( def = rem ).

The binary relation s,n

∼ is an equivalence relation. In Figure 1, M, l 0 4,n ∼ M , l 0 (assuming that l i and l i agree on {p 1 , . . . , p n } for every i ∈ [0, 3], and, l 2 /l 2 and l 4 agree too). By contrast, M, l 0 5,n ∼ M , l 0 does not hold. Lemma 4.1 below is essential to justify that s,n ∼ behaves properly with disjoint unions of models. Its proof is tedious as numerous cases are needed.

Lemma 4.1 Let s, s 1 , s 2 ≥ 1 with s = s 1 + s 2 , M, l s,n ∼ M , l and M 1 , M 2 be models such that M = M 1 M 2 . There are models M 1 and M 2 such that M = M 1 M 2 , M 1 , l s1,n ∼ M 1 , l and M 2 , l s2,n ∼ M 2 , l .
Given a formula φ in MSL( * , Q), let us define its esize (written esize(φ)):

• esize(p) def = esize(emp) def = 1, esize(¬φ) def = esize(φ), esize(Qφ) def = 1 + esize(φ), • esize(φ ∧ ψ) def = max(esize(φ), esize(ψ)), esize(φ * ψ) def = esize(φ) + esize(ψ).
Note that esize(φ) is greater than the modal degree of φ, and approximatively, esize(φ) provides an upper bound on the number of edges that need to be considered in a model for φ (so it will play the role of the value s). For technical reasons, we have assumed that esize(p) = 1, so that esize(φ) ≥ 1 for any φ. Lemma 4.2 Let s, n ≥ 1. For all formulae φ in MSL( * , Q) with esize(φ) ≤ s and built over p 1 , . . . , p n , we have M, l

s,n ∼ M , l implies M, l |= φ iff M , l |= φ.
The following quantitative result is crucial to get the NP upper bound. Lemma 4.3 Let φ be a formula in MSL( * , Q). φ is satisfiable iff φ is satisfiable in a finite and functional model with card(R) ≤ esize(φ).

It remains to show that the model-checking problem for MSL f ( * , Q) is in P. The main difficulty rests on the fact that evaluating an * -formula may require to consider an exponential number of pairs of disjoint submodels. Fortunately, only a polynomial amount of disjoint unions are shown relevant. At the beginning of this section, we defined a decomposition of any MSL model based on the parameter s ≥ 0. Such a decomposition was useful to show Lemma 4.3. A similar decomposition can be done with finite and functional models. More precisely, let M = W, R, V be a finite and functional model and l ∈ W. One can easily define the set W l,s , the relation R l,s and the values t l , s l and rem l . Consequently, an equivalence relation

s,n
∼ can be also defined on finite and functional pointed models leading to a natural variant of Lemma 4.2 involving finite and functional models instead of MSL models.

In order to check whether M, l |= φ holds, we start by building a submodel M = W, R , V ⊆ M with card(R ) ≤ esize(φ) and check whether M , l |= φ holds. The submodel M can be built in polynomial time in the size of M and in s. In forthcoming Algorithm 1, instead of working with models, we operate with slightly more abstract structures. An abstract frame up to s is a pair F = ((l 0 , . . . , l t ), r) where r ≥ 0, (l 0 , . . . , l t ) ∈ N + (standing for locations linked by edges) and the conditions below hold:

(truncation) t * + r ≤ s and t ≤ s with t * = card({(l i , l i+1 ) | i ∈ [0, t -1]}).
(maximality) t < s implies there is no i < t such that l i = l t . (functionality) for all i < j < t, we have l i = l j implies t = s and l i+1 = l j+1 .

Given a finite and functional model M = W, R, V , l ∈ W, and s ≥ 0, we write abst(M, l, s) to denote the abstraction ((l 0 , . . . , l t ), r) with {(0, l 0 ), . . . , (t, l t )} = W l,s and r = rem l . An abstract frame is not explicitly equipped with a propositional valuation but in forthcoming Algorithm 1, we manipulate such structures as the associated propositional valuation will be systematically the one induced by the valuation of the input model. Let shrink(M, l, s) be the finite and functional model

M = W, R , V such that R def = {(l i , l i+1 ) | i ∈ [0, t -1]} ∪ {(n 1 , n 1
), . . . , (n r , n r )}, where {(n 1 , n 1 ), . . . , (n r , n r )} is a set of r egdes in R \ R l,s and the locations n 1 , . . . , n r are minimal. Lemma 4.4 below justifies the correctness of the abstraction. Let us define a notion of disjoint union between abstract frames to mimic the disjoint union of models. Let s = s 1 + s 2 , s, s 1 , s 2 ≥ 1, F = ((l 0 , . . . , l t ), r) be an abstract frame up to s, F i = ((l i 0 , . . . , l i ti ), r i ) be an abstract frame up to s i , with i ∈ {1, 2}. We write

F = F 1 F 2 def ⇔ (i)-(v) below hold (i ∈ {1, 2}): (i) max(t 1 , t 2 ) ≤ t, t 1 × t 2 = 0 and, if t > 0 then t 1 + t 2 > 0. (ii) (l i 0 , . . . , l i ti ) = (l 0 , . . . , l ti ). (iii) 0 < t i < min(s i , t) implies r 3-i > 0. (iv) 0 < t i implies r 1 + r 2 ≤ r + t * -t * i . (v) 0 < t i and r 1 + r 2 < r + t * -t * i imply r i = s i -t * i or r 3-i = s 3-i . Though (i)-(v)
sound reasonable at first glance, the best way to understand what is really needed, is by proving Lemma 4.5 and Lemma 4.6. Similarly, given abstract frames F 1 = ((l 1 0 , . . . , l 1 t1 ), r 1 ) up to s 1 and F 2 = ((l 2 0 , . . . , l 2 t2 ), r 2 ) up to s 2 with s 1 ≤ s 2 , we write F 1 ⊆ F 2 whenever (l 1 0 , . . . , l 1 t1 ) is a factor of (l 2 0 , . . . , l 2 t2 ) and, r 1 + t * 1 ≤ r 2 + t * 2 . Algorithm 1 below operates with abstract frames and its correctness is partly based on forthcoming Lemma 4.5 and Lemma 4.6. For instance, Lemma 4.5 can be understood as a correctness result: disjoint unions of models lead to the satisfaction of the conditions (i)-(v) at the level of abstract frames. Lemma 4.5 Let s = s 1 + s 2 with s, s 1 , s 2 ≥ 1. Let M, M 1 and M 2 be finite and functional models such that M = M 1 M 2 . For all l ∈ W, we have abst(M, l, s) = abst(M 1 , l, s 1 ) abst(M 2 , l, s 2 ).

By contrast, Lemma 4.6 below can be understood as a completeness result: the satisfaction of (i)-(v) can always be mimicked at the level of models. Lemma 4.6 Let s = s 1 + s 2 with s, s 1 , s 2 ≥ 1. Let M be finite and functional, F i be an abstract frame up to s i (i ∈ {1, 2}) such that abst(M, l, s) = F 1 F 2 . There are

M 1 and M 2 such that M = M 1 M 2 , F i = abst(M i , l, s i ) (i ∈ {1, 2}).
What is essential is the fact that the number of non-equivalent decompositions is polynomial and not exponential in the size of F, which is a serious guarantee to obtain a model checking algorithm running in polynomial time.

Lemma 4.7 Let s = s 1 + s 2 with s, s 1 , s 2 ≥ 1, F = ((l 0 , . . . , l t ), r) be an abstract frame up to s. We have card

({(F 1 , F 2 ) | F = F 1 F 2 , F i up to s i }) ≤ 2(s + 1)(s 1 + 1)(s 2 + 1).
Algorithm 1 below uses first principles of dynamic programming as well as the map shrink(F, s) defined as follows (abstract version of the shrink construction on models): shrink(((l 0 , . . . , l t ), r), s) def = ((l 0 , . . . , l t ), r ) with

• t = min(s, t),

• t * = card({l 1 , . . . , l t }) and,

• r = min(s -t * , r + (card({l 1 , . . . , l t }) -t * )).

One can show that shrink(((l 0 , . . . , l t ), r), s) ⊆ ((l 0 , . . . , l t ), r) and shrink(((l 0 , . . . , l t ), r), s) is an abstract frame up to s. Algorithm 1 only computes values for T (shrink(F, esize(ψ k )), k) as it would be time-consuming (and useless) to compute all the values T (F, k). This is enforced by the values in the for loops and by line 2. The map shrink(•, •) is also further needed for conjunctions as the measure esize(•) involves a maximum for conjunctions.

Algorithm 1 Model Checking MSL f ( * , Q) In: A finite and functional model M = W, R, V , a location l ∈ W, an MSL( * , 3) formula φ Out: Return 1 iff M, l |= φ. 1: function MC(M, l, φ) 2: ((l 0 , . . . , l L ), R) := abst(M, l, esize(φ)) card({l 1 , . . . , l L }) + R ≤ esize(φ) 3: ψ 1 , . . . , ψ M subformulae of φ in increasing size ψ M = φ 4: for k ← 1 to M do 5:
for j ← L downto 0 do 6:

for len ← 0 to max{len ∈ [0, L -j] | card({l j , . . . , l j+len }) ≤ esize(ψ k )} do 7: for r ← 0 to max{r ∈ [0, R] | card({l j , . . . , l j+len }) + r ≤ esize(ψ k )} do 8: F := ((l j , . . . , l j+len ), r) F = shrink(F , esize(ψ k )) 9:
case ψ k of 10:

emp: T (F , k) := 1 if (len = 0 and r = 0), otherwise 0.

11:

p: T (F , k) := 1 if l j ∈ V(p), otherwise 0. 12:

¬ψ k : T (F , k) := 1 -T (F , k ) k < k 13: ψ k 1 ∧ ψ k 2 : k 1 , k 2 < k 14:
T (F , k) := min(T (shrink(F , esize(ψ k 1 )), k 1 ), T (shrink(F , esize(ψ k 2 )), k 2 )) 15:

3ψ k : if (len > 0), F := shrink(((l j+1 , . . . , l j+len ), r), esize(ψ k )) k < k 16:

T (F , k) := 1 if (len > 0) and T (F , k ) = 1, otherwise 0. 17:

ψ k 1 * ψ k 2 : k 1 , k 2 < k 18: s 1 := esize(ψ k 1 ); s 2 := esize(ψ k 2 ) esize(ψ k ) = s 1 + s 2 19: T (F , k) := max{min(T (F 1 , k 1 ), T (F 2 , k 2 )) | F = F 1 F 2 , F i up to s i } 20:
end case 21: return T (((l 0 , . . . , l L ), R), M ) Due to the organisation of the for loops, each time the algorithm computes T (F, k), it requires values of the form T (F , k ), always with F ⊆ F and k < k, so the algorithm is properly defined. The algorithm runs in polynomial time thanks to Lemma 4.7. The following lemma establishes that the algorithm is correct and explains what is the intention behind computing the values T (F, k). From Section 2, we recall that MSL(Q, gsb ) is defined as a fragment of MSL( * , Q) with the translation t( gsb φ) def = (size = 1) * t(φ) (global sabotage modal operator). As a corollary of Theorem 4.9, we obtain the result below.

The fragment MSL( * , = )

We also establish that the satisfiability problem for MSL( * , = ) is NPcomplete and its model-checking problem is in P. To do so, we reduce the problems from MSL( * , = ) to MSL f ( * , = ) and we show a small model property. Given φ in MSL( * , = ), let us define its * -weight w * (φ) as follows: As a corollary, if φ in MSL( * , = ) is satisfiable, then it has a model with at most w * (φ) edges. Let us refine this. Let M = N, R, V be an MSL model with card(R) = β, l ∈ N and φ be in MSL( * , = ) such that M, l |= φ. Let ψ 1 , . . . , ψ N be the subformulae of φ such that = ψ 1 , . . . , = ψ N are the only subformulae of φ whose outermost connective is = . For all i ∈ [1, N ] and all β ∈ [0, β], we define at most two locations l i,β 1 and l i,β 2 as follows. Lemma 4.11, this definition makes sense as two models with the same valuation and with the same cardinal of the relation satisfy the same formulae.

• w * (p) def = 0, w * (emp) def = 1, w * (¬φ) def = w * ( = φ) def = w * (φ), • w * (φ ∧ ψ) def = max(w * (φ), w * (ψ)), w * (φ * ψ) def = w * (φ) + w * (ψ).
• Given R ⊆ R with card(R ) = β , we have N, R , V , l i,β 1 |= ψ i and N, R , V , l i,β 2 |= ψ i . By
• If possible we require that l i,β 1 and l i,β 2 are distinct, otherwise if there is only one location satisfying ψ i in N, R , V , we require l i,β

1 = l i,β 2 . • If no location satisfies ψ i in N, R , V , then by default l i,β 1 = l i,β 2 = l. Let W def = {l} ∪ {l i,β j | j ∈ {1, 2}, i ∈ [1, N ], β ∈ [0, β]}. Lemma 4.12 We have W, R, V , l |= φ.
So, MSL( * , = ) satisfies a small model property.

Corollary 4.13 Let φ be a formula in MSL( * , = ). φ is satisfiable iff φ is MSL f ( * , = ) satisfiable in a model with card(W) ≤ 1 + 2|φ| × w * (φ).
It remains to characterise the complexity of the model-checking problem for MSL f ( * , = ). Proof Let M = W, R, V be a finite and functional model, l ∈ W, and φ be a formula in MSL( * , = ). Let ψ 1 , . . . , ψ M be the subformulae of φ ordered in increasing size. We assume W = [0, K] for some K ≥ 0, l = 0 and card(R) = β. In order to determine whether M, l |= φ, we use a labelling algorithm and we complete a table

T (i, j, k) with i ∈ [0, K], j ∈ [0, β] and k ∈ [1, M ] that takes the value 1 iff W, R , V , i |= ψ k with card(R ) = j (dynamic
programming is used here as usual). The polynomial-time upper bound is mainly due to the fact (see Lemma 4.12) that what matters in a partition

{R 1 , R 2 } of R ⊆ R is the respective cardinalities of R 1 and R 2 .
Algorithm 2 Model Checking MSL f ( * , = )

In: A finite and functional model M = [0, K], R, V , K ≥ 0, an MSL( * , = ) formula φ Out: Return 1 iff M, 0 |= φ. 1: function MC(M, l, φ) 2: ψ 1 , . . . , ψ M subformulae of φ in increasing size ψ M = φ 3: β := card(R) 4: for j ← 0 to β do 5:
for k ← 1 to M do 6:

for i ← 0 to K do 7:

case ψ k of 8:

emp:

T (i, j, k) := 1 if (j = 0), otherwise 0 9: p: T (i, j, k) := 1 if i ∈ V(p), otherwise 0 10: ¬ψ k : T (i, j, k) := 1 -T (i, j, k ) k < k 11: ψ k 1 ∧ ψ k 2 : T (i, j, k) := min(T (i, j, k 1 ), T (i, j, k 2 )) k 1 , k 2 < k 12: = ψ k : k < k 13: T (i, j, k) := max(T (1, j, k ), . . . , T (i -1, j, k ), T (i + 1, j, k ), . . . , T (K, j, k )) 14: ψ k 1 * ψ k 2 : k 1 , k 2 < k 15: T (i, j, k) := max{min(T (i, I, k 1 ), T (i, J, k 2 )) | I + J = j and I, J ≥ 0} 16: end case 17: return T (0, β, M )
It is worth noting that computing T (i, j, k) always requires values T (i , j , k ) that have already got a value and the whole procedure requires polynomial-time in β + M + K. The correctness of T (i, j, k) = 1 iff W, R , V , i |= ψ k with card(R ) = j is then by an easy verification. The satisfaction of M, l |= φ is therefore stored in T (0, β, M ). P Again, we are able to establish an NP upper bound.

Theorem 4. [START_REF] Calvanese | Shape and content -A database-theoretic perspective on the analysis of data structures[END_REF] The satisfiability problem for MSL( * , = ) is NP-complete.

5 MSL( * , Q, = ): a Tower-complete fragment of MSL

In this section, we show that the satisfiability problem for MSL( * , Q, = ) is Tower-complete. The upper bound is from Section 3 whereas the proof for Tower-hardness consists of two parts. First, we show that there is a formula in MSL( * , Q, = ) that characterises the linear structures. Then, we reduce the nonemptiness problem for star-free expressions into the satisfiability problem.

Encoding linear structures

The goal of this section is to design a global formula in MSL( * , Q, = ), namely φ ∃ls , such that for all models M, we have M |= φ ∃ls iff either R is empty or R = {(l 0 , l 1 ), . . . , (l n-1 , l n )} for some n ≥ 1 such that for all i = j ∈ [0, n], we have l i = l j . In that case, we say that M is linear . Given a finite set X ⊆ PROP, the relation {(l 0 , l 1 ), . . . , (l n-1 , l n )} encodes the finite word b 1 • • • b n where each letter b j is equal to {p ∈ X | l j ∈ V(p)} (the labelling of the location l 0 is irrelevant for the encoding). When R is empty, the pair M, l encodes the empty string.

Note that φ ∃ls shall be free of propositional variables, which is not so surprising as it expresses a property about the structure of the model. This corresponds to the natural counterpart of the list segment predicate ls(x, y) in separation logic, defined as follows:

(s, h) |= ls(x, y)

def ⇔ either (dom(h) = ∅ and s(x) = s(y)) or h = {l 0 → l 1 , l 1 → l 2 , . . . , l n-1 → l n } with n ≥ 1, l 0 = s(x), l n = s(y) and for all i = j ∈ [0, n], l i = l j .
So, the formula φ ∃ls expresses a property that corresponds to ∃ x, y ls(x, y) from (first-order) separation logic. Given an MSL model M = N, R, V , let us introduce a few notions that are helpful to build the formula φ ∃ls . As MSL( * , Q, = ) does not include Q -1 and (unlike MLH [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF]), we need to characterise linear structures by combining intricate properties. By way of example, stating that each location has at most one predecessor can be easily expressed with [U](¬(Q -1 * Q -1 )), but, obviously, this formula does not belong to MSL( * , Q, = ).

A loop in M is a sequence of locations (l 0 , . . . , l n ) for some n ≥ 1 such that l 0 = l n and for all i ∈ [0, n-1], (l i , l i+1 ) ∈ R. M has at most one maximally connected component (MCC) whenever for all l, l such that R(l) and R(l ) are non-empty, there is l + such that (l, l + ) ∈ R + and (l , l + ) ∈ R + , where R + is the transitive closure of R. A location l is a leaf in M if R(l) = ∅ and R -1 (l) = ∅, and l is a pre-root if R(l) = {l } for some l and R(l ) = ∅. In Figure 2 we illustrate these concepts. This terminology making reference to trees is best understood if we think the definitions with respect to R -1 .

l 0 M l 1 l 2 l 0 M l 1 l 2 l 3 l 4 l 0 M l 1 . . . l n Figure 2.
M is a MCC and a loop, with no leaves and no pre-roots; M is a MCC with three leaves (l 0 , l 1 and l 3 ) and two pre-roots (l 2 and l 3 ); M is linear.

Obviously, if M is linear, then it is loop-free, it has at most one MCC and has a unique leaf in case M is non-empty. The result below states the converse, and below we explain how to express all these properties. Let us consider the formulae below (whose semantics is given in Lemma 5.3). The proof is rather tedious and is intrinsically related to the definition of the formulae. Let φ ∃ls be emp ∨ (UniqTreePRoot ∧ ! Leaf). By combination of the previous lemmas and using that if M is linear and non-empty, then M has at most one MCC and a unique pre-root, we get the result below. The formula ls(x, y) can be therefore encoded by the formula below:

PRoot

def = QP⊥; UniqTreePRoot def = ¬Loop ∧ ((¬(¬emp * ¬emp)) ∨ ! PRoot) Leaf def = (Q ∧ size = 1)∨ (Q ∧ ¬PRoot ∧ ((size = 1 ∧ Q ) * UniqTreePRoot)).
φ ls(x,y) def = φ ∃ls ∧ ((emp ∧ U (x ∧ y)) ∨ ( U (x ∧ Leaf) ∧ U (PRoot ∧ Qy))).

The reduction

In this section, we show that the satisfiability problem for MSL( * , Q, = ) is Tower-hard by reduction from the nonemptiness problem for star-free expressions [START_REF] Meyer | Word problems requiring exponential time[END_REF][START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF]. The proof takes advantage of Theorem 5.4 to encode finite words and separating conjunction will be helpful to encode concatenation, whereas complement and union operators in the star-free expressions are taken care by negation and disjunction, respectively. Our proof is reminiscent to developments from [21, Section 3] as it is essential to be able to encode finite words. Instead of reducing the satisfiability problem for Propositional Interval Temporal Logic [START_REF] Moszkowski | Reasoning about digital circuits[END_REF] as done in [21, Section 3], we define a reduction from the nonemptiness problem for star-free expressions. A star-free expression e over some alphabet Σ is defined by The nonemptiness problem consists in checking whether L(e) = ∅. The problem is shown decidable with a non elementary procedure in [START_REF] Meyer | Word problems requiring exponential time[END_REF][START_REF] Stockmeyer | The complexity of decision problems in automata theory and logic[END_REF] and refined to Tower-completeness in [START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF].

Given a finite alphabet Σ = {a 1 , . . . , a α }, we use the models encoding finite words thanks to the formula φ ∃ls and furthermore, we require that [U] i a i where a i def = p i ∧ j =i ¬p j . So, for every w ∈ Σ * , there is a pair M, l encoding w. We define a relation £ that establishes this correspondence: w £ M, l def ⇔ M is linear and

• If w = ε, then M has an empty accessibility relation and l is arbitrary.

• If w = a i1 • • • a in (n ≥ 1), then M has n edges and l is the unique leaf. With R = {(l 0 , l 1 ), . . . , (l n-1 , l n )}, for all k ∈ [1, α], V(p k ) = {l j | j ≥ 1, i j = k}.
The correspondence between finite words in Σ * and pairs M, l satisfies a nice property as far as splitting a word into two disjoint subwords is concerned. Each expression e is translated as

T (e) def = ([U] i a i ) ∧ φ ∃ls ∧ (emp ∧ t(e)) ∨ (¬emp ∧ Leaf ∧ t(e)),
where t(•) is recursively defined. The four disjuncts in t(e 1 e 2 ) below correspond to cases depending on the emptiness of subwords.

t(ε) def = emp t(a i ) def = (Qa i ) ∧ size = 1 t(∼ e) def = ¬t(e) t(e 1 ∪ e 2 ) def = t(e 1 ) ∨ t(e 2 ) t(e 1 e 2 ) def = ψ 1 ∨ ψ 2 ∨ ψ 3 ∨ ψ 4 ψ 1 def = emp ∧ t(e 1 ) ∧ t(e 2 ) ψ 2 def = (t(e 1 ) ∧ emp) * t(e 2 ) ψ 3 def = t(e 1 ) * (t(e 2 ) ∧ emp) ψ 4 def = (φ ∃ls ∧ ¬emp ∧ t(e 1 )) * (φ ∃ls ∧ ¬emp ∧ U (Leaf ∧ t(e 2 ))).
In ψ 4 , to evaluate t(e 2 ), we move to the unique leaf of the linear structure. Lemma 5.7 Let w ∈ Σ * , and M be a linear model such that w £ M, l. For every star-free expression e, we have w ∈ L(e) iff M, l |= t(e).

As a consequence, Lemma 5.8 Given α ≥ 1, Σ = {a 1 , . . . , a α } and a star-free expression e built on Σ, L(e) = ∅ iff the formula T (e) is MSL( * , Q, = ) satisfiable.

Finally, we get the Tower-completeness. Theorem 5.9 The satisfiability problem for MSL( * , Q, = ) is Towercomplete.

When the magic wand strikes back

In this short section, we show that the satisfiability problem for MSL is actually undecidable by taking advantage of previous results. All the previous complexity results, deal with fragments that are - * -free. It is well-known that adding the separating connective - * can dramatically augment the expressive power or the complexity, see e.g. [START_REF] Brochenin | On the almighty wand[END_REF]. Below, the expressive strength of - * is again illustrated, via a reduction from propositional separation logic augmented with the list segment predicate ls [START_REF] Demri | The effects of adding reachability predicates in propositional separation logic[END_REF]. By contrast, it is known that the modal logic for heaps MLH restricted to * is decidable [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF], but it is open whether the addition of - * leads to undecidability.

First, note that the interval temporal logic with the operators C, D and T over the class of finite strict orders (equivalently, one may consider only the finite intervals of N) is shown to admit an undecidable satisfiability problem in [START_REF] Hodkinson | Non-finite axiomatizability and undecidability of interval temporal logics with C, D, and T[END_REF] and to be non recursively enumerable. By contrast, the version of the logic in which the propositional valuation of an interval only depends on the first value of the interval (the locality condition) is decidable as satisfiability can be reduced to the satisfiability problem for first-order logic over N, ≤, +1 . As we have seen in the paper, the formula φ ∃ls can enforce a linear structure whose labelling depends on the first location (corresponding to the locality condition) but it is unclear how to reduce the undecidable version to MSL, even though there is a clear correspondence between the chop operator C and * , and between the operators D and T, and - * . Instead, our undecidability proof for (full) MSL is by reducing the satisfiability problem for SL( * , - * , ls), recently shown undecidable in [START_REF] Demri | The effects of adding reachability predicates in propositional separation logic[END_REF]. Notice that for the translation of SL( * , - * , ls) formulae, the most complex part is the encoding of the atomic formulae ls(x, y). However, all this work has already been done in Section 5 when we encode linear structures with MSL( * , Q, = ). Then, what gives us undecidability is essentially the inclusion of the - * operator.

Let us define the translation t(•) from SL( * , - * , ls) into MSL formulas, which is homomorphic for Boolean and separation connectives, and t(emp) As the satisfiability problem for SL( * , - * , ls) is recently shown undecidable [START_REF] Demri | The effects of adding reachability predicates in propositional separation logic[END_REF], we get the following result. Theorem 6.2 The satisfiability problem for MSL is undecidable.

Another consequence is the non-finite axiomatisability of MSL, which is inherited from SL( * , - * , ls). As a corollary, the modal logic for heaps MLH (including - * ) augmented with propositional variables is undecidable [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF] as MSL is one of its fragments.

Furthermore, the satisfiability problem of MSL g (Q, gsb ) is undecidable [START_REF] Areces | Satisfiability for relation-changing logics[END_REF]. Therefore, when considering general models, the minimal modal separation logic MSL g ( * , Q) is also undecidable (use a map t such that t( gsb φ) def = (size = 1) * t(φ)).

Conclusion

We have introduced the logic MSL and studied several of its fragments. For MSL( * , Q), we proved that the satisfiability problem is NP-complete whereas the model-checking problem is in P. A similar complexity characterisation is provided for MSL( * , = ). Surprisingly, we have shown that the satisfiability problem for MSL( * , Q, = ) is Tower-complete. A key element of our Tower-hardness proof is the ability to express the property ∃ x, y ls(x, y) from separation logic. Hence, we are able to show that MSL admits an undecidable satisfiability problem. Along the paper, we also investigated variants of MSL (or some of its fragments) by slightly modifying the semantics or by adding other modal connectives. For instance, we have proved that the satisfiability problem for MSL(Q, gsb ) is (only) NP-complete.

Most of the results are summarised in the table below. The decidability status of MSL f and MLH [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF] is also open. Finally, the design of proof systems for modal separation logics remains a challenging question.

  when this holds, M 1 M 2 denotes the model corresponding to the disjoint union of M 1 and M 2 , and M 1 ⊆ M 2 means that M 1 and M 2 have the same valuation and R 1 ⊆ R 2 . Given M = N, R, V and l ∈ N, the satisfaction relation |= is defined below (clauses for Boolean connectives are omitted):

Theorem 3 . 3

 33 The satisfiability problem for MSL( * , Q, = ) is in Tower.

Theorem 3 . 5

 35 The satisfiability problem for MSL( * , Q, Q -1 , = ) is in Tower.

∼with s = 5 s l0 = 4 t l0 = 5 rem l0 = 1 with s = 5 s l0 = t l0 = 4 rem l0 = 1 Figure 1 .

 54515411 Figure 1. Decomposition.

Lemma 4 . 4

 44 Let s ≥ 0, M = W, R, V be finite and functional and l ∈ W with M = shrink(M, l, s). Then M, l s,n ∼ M , l and abst(M, l, s) = abst(M , l, s).

Lemma 4 . 8

 48 For all k ∈ [1, M ], for all abstract frames F = ((l, . . .), R ) up to esize(ψ k ) with F ⊆ ((l 0 , . . . , l L ), R), when the model-checking algorithm ends, T (F, k) = 1 iff for all finite and functional submodels M ⊆ M such that abst(M , l, esize(ψ k )) = F, we have M , l |= ψ k .So the model checking problem for MSL f ( * , Q) is in P, and we can conclude.

Theorem 4 . 9

 49 The satisfiability problem for MSL( * , Q) is NP-complete.

Corollary 4 . 10

 410 The satisfiability problem of MSL(Q, gsb ) is NP-complete.

Lemma 4 . 11

 411 Let α ≥ 0 and M = N, R, V and M = N, R , V be MSL models such that min(card(R), α) = min(card(R ), α). Then, for all locations l and formulae φ in MSL( * , = ) such that w * (φ) ≤ α, we have M, l |= φ iff M , l |= φ.

Lemma 4 . 14

 414 The model-checking problem for MSL f ( * , = ) is in P.

Lemma 5 . 1

 51 Let M be an MSL model with a non-empty relation. M is linear iff M is loop-free and has a unique leaf.Let us introduce the global formula Loopdef = * (([U]PQ ) ∧ ¬emp). Lemma 5.2 Let M be an MSL model. M |= Loop iff M has at least one loop.

Lemma 5 . 3

 53 Let M = N, R, V be a model and l ∈ N. (I) M, l |= PRoot iff l is a pre-root. (II) M, l |= UniqTreePRoot iff M is loop-free and either R is empty or (M has at most one MCC and a unique pre-root). (III) Assuming that M |= UniqTreePRoot, we have M, l |= Leaf iff l is a leaf.

Theorem 5 . 4

 54 Let M = N, R, V be a model. M |= φ ∃ls iff M is linear.

e

  ::= a | ε | e ∪ e | ee | ∼ e, where a ∈ Σ and ε denotes the empty string. Star-free expressions e are interpreted by languages L(e) ⊆ Σ * as follows: • L(a) def = {a} for all a ∈ Σ; L(ε) def = {ε}; L(∼ e) def = Σ * \ L(e); • L(e ∪ e ) def = L(e) ∪ L(e ); L(ee ) def = {ww ∈ Σ * | w ∈ L(e), w ∈ L(e )}.

Lemma 5 . 5 7 . 5 . 6

 55756 Let w £ M, l with w = w 1 w 2 ∈ Σ * . There exist linear models M 1 and M 2 and l such thatM = M 1 M 2 , w 1 £ M 1 , l and w 2 £ M 2 , l .Another technical lemma is needed for the proof of Lemma 5.Lemma Let w £ M, l with M = M 1 M 2 and, M 1 and M 2 are linear. There are w 1 , w 2 ∈ Σ * and l ∈ N such that w = w 1 w 2 , w 1 £ M 1 , l and w 2 £ M 2 , l .

def=Lemma 6 . 1

 61 emp t(x = y) def = U (x ∧ y) t(x → y) def = U (x ∧ Qy) t(ls(x, y)) def = φ ∃ls ∧ ((emp ∧ U (x ∧ y)) ∨ ( U (x ∧ Leaf) ∧ U (PRoot ∧ Qy))),where x, y are nominals and φ ∃ls defined as in Section 5.1. We get the result below. Let φ be an SL( * , - * , ls) formula. φ is satisfiable iff t(φ) is satisfiable in MSL.

  models) MSL( * , 3), MSL( * , = ) P NP-complete MSL( * , 3, = ) PSpace-complete Tower-complete MSL PSpace-complete Undecidable MSL( * , 3 -1 ) PSpace-complete PSpace-hard, in Tower MSL(3, gsb ) P NP-complete Understanding the effects of the interactions between modal operators and separating connectives is still to be strengthened and many interesting problems are left open. By way of example, we have shown that the satisfiability problem for MSL( * , Q -1 ) is PSpace-hard and in Tower but a complexity characterisation is not yet known. Similarly, the satisfiability problem for MSL( * , Q, = ) is shown Tower-complete, what about its slight variant MSL( * , Q, U )?

Ackowledgements. We would like to thank Alessio Mansutti (LSV, France) for helpful suggestions and enlightning discussions. This work was partially supported by ANPCyT-PICTs-2016-0215, SeCyT-UNC, and the Laboratoire International Associé INFINIS.


Weike Feng

Jean-Michel Friedt
email: jean-michel.friedt@femto-st.fr

Grigory Cherniak

Motoyuki Sato

Passive bistatic radar using DVB-T receivers as general-purpose software-defined radio receivers

We investigate the use of low-cost digital video broadcast-terrestrial (DVB-T) receivers as general-purpose software-defined radio (SDR) receivers for passive bistatic radar (PBR) applications. Two DVB-T receivers are synchronized using a common clock to perform coherent measurements. By exploiting the direct-path signal in the surveillance channel, we use the cross-correlation process to estimate the time offset between the data streams of reference and surveillance channels caused by the USB communication. We demonstrate the detection of static and moving targets as well as short-range targets, including a landing airplane at 8 km, multiple ships with different velocities, and vehicles within 20 m from the receiver acquiring at a 2 MHz bandwidth, by using Japan's ISDB-T digital TV signal broadcast. We also propose to improve the range resolution of the designed PBR system by combining multiple SDR receivers tuned to different carrier frequencies. The designed system and proposed method can be used for various applications, such as airplane navigation, harbor protection, and traffic density monitoring.

I. INTRODUCTION

Active radar measurement is associated with high power and broadband emitters. The radar signals from the emitter decay as a function of the product of the square of the source-target distance and the square of the target-receiver distance. Therefore, stronger emission powers are required than that required for one-way communication applications.

Moreover, because the radar range resolution is inversely proportional to its bandwidth, broadband signals are required for a high radar range resolution. An alternative to using a dedicated radar emitter is to use some of the radiofrequency signal sources already deployed for various purposes [1][2][3][4][5][START_REF] Olivadese | EUSAR. 9th European Conference on[END_REF][START_REF] Zheng | [END_REF] : for example, frequency-modulated broadcast emitters, digital audio broadcasting emitters, and digital terrestrial television broadcasting (DTTB) emitters. Use of these sources is advantageous because there is no requirement for frequency allocation for specific applications.

Use of non-cooperative sources for a radar application establishes a passive radar system 8 , which is intrinsically bistatic because the transmitter and the receiver are at different locations. Passive bistatic radar (PBR) has been extensively studied for different applications by adopting different sources [START_REF] Baczyk | [END_REF][10][11][START_REF] Frölind | Radar Conference (RadarConf )[END_REF][START_REF] Hoyo | [END_REF][14] . Although PBR can work independently from the employed waveforms, its performance (measured in terms of parameters such as spatial resolution and ambiguity), coverage area, and available period are mainly determined by the adopted source 15 . Among the different sources, DTTB signals can provide a superior ambiguity function compared to that provided by conventional analog signals, cover an urban-wide area because of the high transmission power, and facilitate continuous measurement. Therefore, DTTB signals are extensively studied for detecting airplanes [START_REF] Baczyk | Radar Conference[END_REF] , ships [START_REF] Capria | IEEE Gold Remote Sensing Conference[END_REF] , and vehicles [START_REF] Capria | Geoscience and Remote Sensing Symposium (IGARSS)[END_REF] . In Japan, Integrated Services Digital Broadcasting Terrestrial (ISDB-T) has been used as the DTTB standard [START_REF] Takada | Proceedings of the IEEE[END_REF] . Some studies of PBR using the ISDB-T signal have been conducted in the last decade [START_REF] Honda | [END_REF][START_REF] Nakamura | Geoscience and Remote Sensing Symposium (IGARSS)[END_REF] .

Recently, conversion of processing steps from hardware to software has been an ongoing trend, which is driven not only by the flexibility and reconfigurability of software with respect to hardware but also by the lower cost of consumer electronics [START_REF] Mahnke | [END_REF][START_REF] Berizzi | Radar Conference[END_REF][START_REF] Marimuthu | [END_REF][25][26] . Communication modems had followed this trend in the 1990s, and now radiofrequency reception peripherals are following a similar trend. Porting the driver of a digital video broadcast-terrestrial (DVB-T) receiver to the Linux operating system led to the discovery that Realtek RTL2832U-based DVB-T receivers can serve as general-purpose software-defined radio (SDR) receivers, including for the development of high grade scientific instruments 27 . The flexibility of SDR receivers allows for the use of a single affordable hardware in a wide range of fields, including oscillator characterization 28 , communication, time transfer 29 , or electromagnetic wave propagation conditions. Their broad availability and low cost have made them popular among amateur SDR enthusiasts, including those using the open-source GNU Radio SDR framework [START_REF] Rondeau | Opportunistic Spectrum Sharing and White Space Access: The Practical Reality[END_REF] : the DVB-T receivers are supported as I/Q coefficient sources with sample rate up to 2.4 Msamples/s and 8-bit resolution, which are suitable for many analog and low-bandwidth digital communication modes, thus making them ideal for adapting to educational material. Since 2010, through the introduction of the now-defunct Elonics E4000 and with the latest versions that use the Rafael Micro R820T2, several radiofrequency frontends have been made available for signal amplification and down-conversion to baseband.

In this study, we use low-cost SDR receivers to illustrate PBR processing techniques to a wide audience. First, we review the fundamentals of passive radar signal processing.

Then, a PBR system is designed using DVB-T receivers. We then demonstrate the process of coherent measurements using two DVB-T receivers synchronized by a common clock.

Experimental results of mapping stationary and moving targets are presented. Finally, we present the improvement of the range resolution by combining multiple SDR receivers, each tuned to a different carrier frequency. The presented techniques are generally applicable whenever multiple SDR receivers are to be combined either for correlation measurement, bandwidth extension for improved timing resolution or phase measurement with respect to an unknown reference signal in general.

II. FUNDAMENTALS OF PASSIVE RADAR SIGNAL PROCESSING

The underlying requirement for passive radar application is to measure the signal emitted by a non-cooperative source, called the reference signal, and the signal reflected by targets, called the surveillance signal. A cross-correlation technique is required to identify delayed copies of the reference signal in the surveillance signal. As will be illustrated in section IV, in the static case, the cross-correlation technique used is simply the direct cross correlation of surveillance signal S(t) and reference signal R(t) and the output is therefore only dependent upon the time delay τ between these signals:

χ(τ ) = +∞ -∞ S(t) • R * (t -τ )dt (1)
Considering that the Fourier transform of the cross-correlation χ is the product of the Fourier transform of S(t) multiplied by the complex conjugate of the Fourier transform of R(t), Eq. 1 can be effectively calculated by implementing the fast Fourier transform (FFT). The non-cooperative source is not noise but has some structured information that may repeat in time or frequency. Therefore, we must analyse the spectral characteristics of the source to assess its suitability for passive radar application [START_REF] Harms | Radar Conference[END_REF] .

After demonstrating the static target mapping, we will consider the mapping of moving targets in section V. In the bistatic configuration, a target moving at a velocity v introduces a maximum Doppler shift of f D = 2f 0 v c on the reflected signal, where f 0 is the carrier frequency and c is the velocity of electromagnetic waves. Therefore, cross-correlation of the surveillance signal S(t) with the reference signal R(t), time-shifted by τ and frequency-shifted by f D , naturally yields the following cross-ambiguity function:

χ(τ, f D ) = +∞ -∞ S(t) • R * (t -τ )e -j2πf D t dt (2)
To reduce the computational complexity, we will use the batch algorithm to calculate Eq. 2 effectively 32 . First, the large dataset is parsed into small batches such that the Doppler shifts of targets within each batch are negligible. For each batch, cross-correlation is performed by implementing FFT. Then, because the direct-path interference and echoes from stationary targets for different batches show small changes, mean-value subtraction is performed to reduce their influences. Finally, the Fourier transform along the batch direction provides the long-term evolution of the Doppler frequencies of the targets.

Ideally, the associated cross-ambiguity function when applying copies of the reference signal as surveillance signals would be a Dirac function. However, in practical application, the sources may exhibit some undesirable properties in the time or frequency domain, which can be erroneously interpreted as detected targets. The ambiguity function of the source obtained by auto-correlating the reference signal with its time-shifted and Doppler-shifted copies provides information on such undesirable property, which can be used to prevent false target detection. The ambiguity functions of various sources have been documented 15 . In Sendai (Japan), three television towers emit 3-kW signals at a frequency range of 470-570

MHz, as shown in Fig. 1. We use the 509-MHz channel for the moving target detection process, and its ambiguity function is given in Fig. 2, in which the information at ±220 Hz offset should not be mistaken for targets. We note that other channels will give the similar results, which are not shown in this paper for concision. For short-range applications with a bandwidth of only 2 MHz, because it is unnecessary and impractical to perform range compression, only 1D Fourier transform is used to estimate the Doppler frequency of targets. Therefore, in this case, we apply τ = 0 in Eq. 2, giving:

χ(f D ) = +∞ -∞ S(t) • R * (t)e -j2πf D t dt (3)
This can be effectively calculated by FFT, as will be described in section V. Since we apply τ = 0, it is assumed that the target is limited within the first bistatic range cell, i.e.

the short range is defined as 150 m.

III. REQUIREMENT OF COHERENT MEASUREMENTS

Many studies have demonstrated the ability to perform coherent measurements using two DVB-T receivers synchronized by a common clock 33,34 . However, apart from the result description, these studies do not provide a formal and detailed description of the procedure that was followed to acquire the data. Time-delayed copies of the reference signal in the surveillance signal can be identified under the following three conditions: (1) the local oscillator of both radiofrequency receivers must be coherent over the duration of the analysis, (2) the data transferred by the two receivers must be synchronous, and (3) the direct wave reaching the surveillance receiver must not overwhelm the weak reflections from distant targets. These conditions can be achieved by using two consumer electronic DVB-T receivers, with the local oscillator of one receiver used as a clock for the other one, as shown in Fig. 3.

However, in the case of DVB-T receivers used in consumer electronics, to achieve the target carrier frequency, the quartz oscillator is set at a universal serial bus (USB) clock frequency and multiplied by a phase-locked loop (PLL) by the radiofrequency frontend.

In coherent measurements, because of the use of the PLL, although fine frequency steps can be achieved by dithering, some phase coherence loss will be introduced. Moreover, the PLL behavior's dependence on temperature introduces a phase difference between the two receivers. The frequency dithering, active as a default configuration of the librtlsdr library in the Debian distribution of Linux, as shown in Fig. 4, is deactivated by modifying the software 35 and compiling a custom version of the osmosdr GNU Radio source block linked against the updated library. Temperature drift is tackled by providing a thermal link between the two receiver frontends.

The data transmission synchronization is addressed at the post-processing level. DVB-T receivers communicate over a USB, so the latency between two measurement initialization sequences cannot be predicted. Indeed, the data stream start time is observed to randomly vary as GNU Radio triggers the measurements from both dongles asynchronously. However, once the data stream starts, the time offset is observed to be constant and no sample loss is observed for data rates below 2.048 Msamples/s. The time offset between the two data streams is observed to mostly range within ±500 µs, or ±1000 samples when sampling at 2

Msamples/s.Because a strong direct-path interference is always received by the surveillance channel, identifying the time delay by cross-correlating two signals is possible. However, we emphasize that this initial calibration only remains valid as long as the data stream remains uninterrupted.

IV. APPLICATION TO STATIC TARGET DETECTION

Having described the basic setup and processing sequence, we now demonstrate a measurement using the experimental setup described in the previous section. We used a fixed 18-element Yagi-Uda antenna that provides the reference signal and an 18-element surveillance Yagi-Uda antenna that scans over a 170 • angular range in azimuth direction incrementally with 5 • step. The nominal horizontal and vertical 3 dB beamwidth is 30 ± 5 • for such antenna models. For these static targets, the cross-correlation calculation was performed using Eq. 1. GNU Radio is used to achieve a real-time display of the cross-correlation result between two DVB-T receivers as the data are being acquired, which is a key feature with respect to post-processing to ensure that the collected data are usable in the field.

The real-time cross-correlation was achieved by converting the continuous data stream into vectors, followed by Fourier transform of each vector, computation of the product of one resulting vector and the complex conjugate of the other vector, and finally inverse Fourier transform of the product vector. All these steps are available as processing blocks in GNU Radio and can be readily implemented for real-time analysis.

V. APPLICATION TO MOVING TARGET DETECTION

A moving target has the Doppler frequency shift introduced by its motion, which can help to differentiate it from the static clutter. We demonstrate moving target detection on the range-Doppler plane of aircrafts and ships; the former exhibit large velocities even at their landing stage, and the latter exhibit smaller velocities but a larger radar cross-section (RCS).

A. Airplane detection

The experiment was conducted near the Sendai airport, shown in Fig. 1: despite the short range (0-10 km) demonstration, the objective of this experimental framework is to provide a controlled experimental environment with visual assessment of the plane presence, as well as matching the non-cooperative emitter radiation pattern 37 oriented towards the ground rather than the sky, as would be needed for monitoring cruising planes. In addition, the range-Doppler map of the airplane when a 125-ms-long integration time is selected, which provides an 8-Hz Doppler resolution, is shown in Fig. 7. By comparing Fig. 7 and Fig. 6, we note that by increasing the integration time to 0.5 s, although the computation time is increased, sidelobes are reduced and the signal-to-noise ratio is significantly improved. Near-range moving cars are well visible above the clutter and the airplane is identified easily at a far range.

- Various types of airplanes, including large commercial aircraft, smaller two-seater training aircrafts, and helicopters, have been detected in the same day using this system 38 . The measurement sequence durations are limited by the data bandwidth: with 2 Msamples/s, 4 bytes/sample, two channels, and I/Q coefficients, the data rate is 32 MB/s or 1.92 GB/min.

Therefore, because of storage limitations, all measurements were maximum 4-minute long.

For the identification of the range and velocity analysis during airplane landing, the range-Doppler maps are stacked to obtain a complete trajectory estimation of the airplane. The result for a 1.5 minute long record is illustrated in Fig. 8, where the landing route can be clearly observed, as indicated by the rectangle.

B. Ship detection

Ships entering and leaving the port of Sendai, shown in Fig. 9, were also observed using the designed passive radar. The parameters used here were different from those of the experiments with the airplanes. Since the ships move much more slowly than airplanes, 2-slong data segments are selected, which provides a 0.5-Hz Doppler frequency resolution and high signal-to-noise ratio. Fig. 9 and Fig. 10 show the detection and trajectory estimation results for three ships that are visible on the horizon. Two of the ships were moving in opposite directions with respect to the antennas, while the third one was static during the entire measurement duration.

Because ships move slower than airplanes, a strategy was devised to extend the acquisition duration of GNU Radio. Although GNU Radio processes floating point numbers, the DVB-T receivers only sample 8-bit data. Hence, the complex values provided to GNU Radio, ranging from -1 to +1, are scaled by 127 and stored as interleaved 8-bit integers. Therefore, the acquisition duration is increased by 4 times, which results in a record duration of 12 min.

C. Short-range moving vehicles

Finally, we applied PBR measurements using low-cost DVB-T receivers to near-range moving target detection. Since the 2-MHz bandwidth receivers allow for a bistatic range resolution of only 150 m, the range measurement of a low-RCS target at short range, such as cars or motorbikes, is not feasible. Therefore, we set τ = 0 at a fixed value to calculate the cross-ambiguity function Eq. 2, such that the short-range target detection problem becomes a simple Doppler identification through the Fourier transform, as given in Eq. 3.

Figure 11 shows the result of a 3-minute long dataset analysis, with a 0.5-s integration time. In this measurement case, various vehicles drove toward or away from the surveillance antenna, which induced positive or negative Doppler frequencies (Y-axis), respectively. Figure 12 shows results of the analysis of another dataset. While acquiring the data, a movie of the road was recorded, from which images were extracted at one frame per second.

The images were then manually selected by deleting those without any moving target. This

VI. RANGE RESOLUTION IMPROVEMENT BY EXTENDING THE NUMBER OF RECORDING CHANNELS

The bistatic range resolution is given by the inverse of the measurement bandwidth.

The television channels' bandwidth is as wide as 6 MHz, but each DVB-T receiver can only sample up to 2 Msamples/s or a range resolution of 150 m. The range resolution can be improved by expanding the measurement bandwidth, which is possible with SDRs, by multiplying the number of receivers, each tuned to a different carrier frequency. Within one given television channel broadcast, two adjacent frequencies allow for sampling up to 4 Msamples/s, thereby halving the range resolution. Furthermore, the flexibility of SDR allows for tuning to different television channels that are characterized by widely different carrier frequencies emitted from the same location, as shown in Fig. 13. In this case, the range resolution is significantly increased but at the cost of high-level sidelobes introduced by the frequency gap between the two sampled datasets [START_REF] Olivadese | IET International Conference on Radar[END_REF]40 .

FIG. 13. A passive radar setup with four receivers, with two receivers tuned to different carrier frequencies connected to the reference antenna, while the other two tuned to the same carrier frequency set connected to the surveillance antenna. A single master clock cannot be directly distributed to the three slaves by connecting the oscillator output to the three inputs: a hexinverted 7404 is used as a buffer between the output and two of the inputs. The MiniCircuits ZFSC-2-4 splitters are used between the antennas and the DVB-T receivers.

In a quad-receiver setup, for the coherent analysis of the signals recorded by two DVB-T pairs tuned to different carrier frequencies, the synchronization procedure for compensating for the delay introduced by the USB communication must be accurate such that the cells in the range-Doppler map are matched. Since the resulting range resolution is increased with respect to the single-channel analysis, interpolation is needed to accurately position the cells in the range direction: any delay between the data recorded by the surveillance and reference channels, caused by the USB communication, will be observed as a range error, and signals from two sets of reference and surveillance channels will not accumulate coherently to increase the range resolution. Indeed, since multiple channel signals are combined by summing complex spectra obtained after frequency transposition, accurate alignement of the datastreams collected from receivers is mandatory for phase coherence. A two step process is used: initially, samples collected by reference and surveillance channels tuned to the same band are aligned by correlation as described previously, and then digital communication delays between receivers are computed and compensated for with sub-sampling period accuracy using interpolation, assuming that the propagation delay is the same for all channels as expected from a non-dispersive medium as air. Thus improved range resolution is achieved thanks to the increased bandwidth by reaching higher timing resolution than the sampling period as needed to provide phase coherence throughout the spectrum range.

Thus, we analyze the fine synchronization by using the direct wave signals received by both reference and surveillance channels at two different frequencies. Using an oversampling approach, for example by zero-padding the Fourier transform and computing the low-pass filtered inverse Fourier transform, under the assumption that the direct wave is characterized by a single correlation peak, the cross-correlation peak position will provide a time delay with an accuracy better than the sampling rate. By using this time delay on both channel pairs, the targets are positioned in the same range cell, thereby resulting in the range resolution improvement. The acquisition and processing algorithm is summarized as follows:

1. collect data from four SDR receivers, two of which are connected to the reference antenna, while two are connected to the surveillance antenna. The first and third receivers are tuned to one frequency, the second and fourth are tuned to a frequency farther from the first one by more than the sampling bandwidth;

2. synchronize the first two and last two data streams by oversampling the data and selecting the maximum of their cross-correlations;

3. throughout the data analysis, assume the delays introduced by the USB communication latencies to be constant and the stream to be continuous, and shift the oversampled datasets by the delays identified from step 2;

4. combine the synchronized oversampled datasets from the two frequency ranges during the cross-correlation computation to increase the range resolution. The approach to combine two frequency ranges is given as follows:

(a) assuming that the synchronized oversampled datasets with two carrier frequencies f 1 and f 2 (t) are R 1 (t), R 2 (t), S 1 (t) and S 2 (t), based on Eq. 1, compute the crosscorrelation for each dataset by implementing FFT, giving

χ 1 (τ ) = +∞ -∞ S 1 (t) • R * 1 (t -τ )dt (4)
and

χ 2 (τ ) = +∞ -∞ S 2 (t) • R * 2 (t -τ )dt (5)
(b) combine the cross-correlation results by

χ(τ ) = χ 1 (τ )e j2πf 1 τ + χ 2 (τ )e j2πf 2 τ (6)
The need for interpolating data through oversampling during the delay matching search is illustrated in Fig. 14. If no oversampling is performed, the datasets collected at each frequency are aligned to within one sampling period, and the cross-correlation peaks of samples collected at both frequencies are not properly aligned to sharpen the correlation peak through destructive interference of the sidelobes. By contrast, upon oversampling, the broadband cross-correlation peak is observed to narrow to one-half of the narrowband width.

These measurements were collected by letting both measurement and surveillance channels connect to the reference antenna that points toward the non-cooperative emitter.

In the dataset used to obtain the results shown in Fig. shows that the Doppler resolution is not influenced by the combination of different channels because the total integration time is unchanged.

VII. CONCLUSION

In this study, we demonstrate the use of consumer-grade DVB-T receivers as generalpurpose SDR receivers in PBR detection. We present the processing steps required to

FIG. 1 .

 1 FIG. 1. Left: Three TV towers located 3.3 km from the CNEAS laboratory broadcast in the Sendai (Japan) area. Background map: Google Maps. Right: Spectrum of the six terrestrial digital television stations broadcasting in Sendai.

FIG. 2 .

 2 FIG. 2. Ambiguity function of the ISDB-T signal in Sendai, Japan.

FIG. 3 .

 3 FIG. 3. Experimental setup, where a thermal link made by a copper beam is put between the two radiofrequency frontends. The reference oscillator output from one receiver feeds the clock signal of the other receiver.

FIG. 4 .

 4 FIG.4. Impact of dithering (green active, red deactivated) on the phase difference between the outputs of two DVB-T receivers fed by the same oscillator.

Figure 5 (

 5 Figure 5 (top) illustrates the map obtained from the above-mentioned cross-correlation process: the returned signals are maximum in the azimuth of the nearest buildings. However, the poor range resolution associated with the low measurement bandwidth provides a low spatial resolution for such short-range measurements. If the DVB-T receivers are replaced with a radiofrequency-grade oscilloscope , such as an Agilent 54850 sampling at 10 Gsamples/s, and an external amplifier and a down-converter are used, then the resulting map of the signals reflected by the short-range and far-range buildings would be consistent and considerably sharper, as shown in Fig. 5 (bottom). The flexibility of GNU Radio and SDR has been validated by using a digital oscilloscope, as demonstrated by using the signal source we provide at 36 , instead of the low-bandwidth DVB-T receivers.

FIG. 5 . 1 FIG. 6 .

 516 FIG. 5. Cross-correlation result as a function of azimuth and range obtained by (top) DVB-T receivers and (bottom) a radiofrequency-grade oscilloscope.

Figure 6 (

 6 Figure 6 (left) shows the range-Doppler map of a landing airplane when the direct-path interference and echoes from stationary targets were not eliminated by subtracting the mean trace value.

FIG. 7 .

 7 FIG. 7. Range-Doppler map of a landing airplane with a 125-ms integration time.

FIG. 8 .

 8 FIG. 8. Trajectory of a landing airplane for a 1.5-minute record.

FIG. 9 .FIG. 10 .

 910 FIG. 9. Range-Doppler map of multiple ships (left), and experimental setup (right).

FIG. 11 .

 11 FIG. 11. Doppler evolution (Y-axis) of targets as a function of time (X-axis) for vehicle measurement 1.

FIG. 12 .

 12 FIG. 12. Top: Doppler evolution (Y-axis) of targets as a function of time (X-axis) for vehicle measurement 2. Bottom: selection of a few images from a movie recorded while acquiring radar data, indicating each time a vehicle is visible in front of the receiver.

FIG. 15 . 1 FIG. 16 .

 15116 FIG. 15. Cross-correlation results obtained by combining two discontinuous frequency bands (top) without interpolation and (bottom) with interpolation. Due to the frequency gap between the two used frequency bands, high-level sidelobes are produced.

  . Fig.17 (top) shows that the rangeresolution is improved by combining two frequency bands together, while Fig.17

  (bottom)

FIG. 17

 17 FIG. 17. (Top) Cross-sections along the range direction at a fixed Doppler shift -24.4 Hz, and (bottom) Doppler-frequency cross-sections at a fixed range of 2215 m.

ACKNOWLEDGMENTS

This work is supported by JSPS Grant-in-Aid for Scientific Research (A) 26249058. J.-MF is grateful to Tohoku University for granting a position as a three-month visiting scientist to the Center for Northeast Asian Studies (CNEAS). The DVB-T passive radar investigation is partly supported by the French Centre National de la Recherche Scientifique (CNRS) PEPS grant.