Andreas Herzig

A simple separation logic

The kinds of models that are usually considered in separation logic are structures such as words, trees, and more generally pointer structures (heaps). In this paper we introduce the separation logic of much simpler structures, viz. sets. The models of our set separation logic are nothing but valuations of classical propositional logic. Separating a valuation V consists in splitting it up into two partial valuations v 1 and v 2 . Truth of a formula ϕ 1 * ϕ 2 in a valuation V can then be defined in two different ways: first, as truth of ϕ 1 in all total extensions of v 1 and truth of ϕ 2 in all total extensions of v 2 ; and second, as truth of ϕ 1 in some total extension of v 1 and truth of ϕ 2 in some total extension of v 2 . The first is an operator of separation of resources: the update of ϕ 1 * ϕ 2 by ψ is the conjunction of the update of ϕ 1 by ψ and the update of ϕ 2 by ψ; in other words, ϕ 1 * ϕ 2 can be updated independently. The second is an operator of separation of processes: updates by ψ 1 * ψ 2 can be performed independently. We show that the satisfiability problem of our logic is decidable in polynomial space (PSPACE). We do so by embedding it into dynamic logic of propositional assignments (which is PSPACE complete). We moreover investigate its applicability to belief update and belief revision, where the separation operators allow to formulate natural requirements on independent pieces of information.

Introduction

Separation logics [START_REF] Samin | BI as an assertion language for mutable data structures[END_REF][START_REF] O'hearn | Local reasoning about programs that alter data structures[END_REF][START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]] have a modal operator * which allows to talk about the separation of resources. Basically, the formula ϕ 1 * ϕ 2 is true in the model M if M can be split into two parts M 1 and M 2 such that ϕ 1 is true in M 1 and ϕ 2 is true in M 2 . The kinds of models that are usually considered in separation logic are structures such as words, trees, and more generally pointer structures (heaps). The separation logics of such structures are often undecidable. In this paper we investigate the separation logic of much simpler structures, viz. sets. We call our logic set separation logic, abbreviated SSL. The models of SSL are nothing but valuations of classical propositional logic. Separating a valuation V consists in splitting it up into two partial valuations v 1 and v 2 . Then separability of ϕ 1 and ϕ 2 in a valuation V can be defined in two different ways: first, as truth of ϕ 1 in all total extensions of v 1 and truth of ϕ 2 in all total extensions of v 2 ; and second, as truth of ϕ 1 in some total extension of v 1 and truth of ϕ 2 in some total extension of v 2 . We respectively denote these two separation operators by ∧ and ˙ . We chose the symbol ∧ due to its analogy with the symbol of disjoint union ∪, and we chose the symbol ˙ because denotes parallel execution.

We show that the satisfiability problem of set separation logic is decidable in polynomial space (PSPACE). We do so by embedding SSL into dynamic logic of propositional assignments DL-PA [START_REF] Balbiani | Dynamic logic of propositional assignments: a well-behaved variant of PDL[END_REF], whose star-free fragment is PSPACE complete. This contrasts with separation logics having the implicational connective - * , which are often undecidable even in the proopositional language [START_REF] Brotherston | Undecidability of propositional separation logic and its neighbours[END_REF][START_REF] Larchey | The undecidability of boolean bi through phase semantics[END_REF].

Our initial motivation to investigate separation operators was that they can be given an interesting interpretation in the context of the revision and update of propositional belief bases: we consider that when ϕ 1 and ϕ 2 are separable then they are independent pieces of information. This naturally leads to the following requirements.

• We suppose that ∧ expresses independence of resources: the update of ϕ 1 ∧ ϕ 2 by ψ is the conjunction of the update of ϕ 1 by ψ and the update of ϕ 2 by ψ; in other words, ϕ 1 ∧ ϕ 2 can be updated independently.

• We suppose that ˙ expresses independence of processes: the update of ϕ by ψ 1 ˙ ψ 2 is the parallel update of ϕ by ψ 1 and by ψ 2 ; in other worlds, updates by ψ 1 ˙ ψ 2 can be performed independently.

This extends previous approaches by Parikh, Makinson and others that are based on splitting languages [START_REF] Bienvenu | Prime implicate-based belief revision operators[END_REF][START_REF] Kourousias | Parallel interpolation, splitting, and relevance in belief change[END_REF][START_REF] Parikh | Beliefs, belief revision, and splitting languages[END_REF]. We investigate the compatibility of existing belief change operations with the above two requirements. The paper is organised as follows. In Section 2 we introduce set separation logic SSL. In Section 3 we provide a PSPACE upper bound for both its model checking and its satisfiability problem. In Section 4 we discuss the relation between SSL and language splitting-based belief change. Section 5 concludes.

Set separation logic SSL

Throughout the paper we use the following conventions. P = {p, q, . . .} is a countable set of propositional variables. The set {P 1 , P 2 } is a partition of P iff P 1 ∪ P 2 = P and P 1 ∩ P 2 = ∅.

A valuation is a total function from P to {0, 1}. We use V, V 1 , . . . for valuations. Two valuations V and V ′ agree on the set of variables P ⊆ P, if both give the same truth value to each of the variables in P:

V ∼ P V ′ iff V(p) = V ′ (p) for every p ∈ P.
A partial valuation is a partial function from P to {0, 1}. For a valuation V : P -→ {0, 1} and a set of propositional variables P ⊆ P, the restriction of V to P is the partial function whose domain is P, noted V| P . We use v, v 1 , . . . for partial valuations. The total valuation V is an extension of the partial valuation

v if V(p) = v(p) for every p ∈ dom(v). 1
The language of SSL is defined by the following grammar:

ϕ p | ¬ϕ | ϕ ∧ ϕ | ϕ ∧ ϕ | ϕ ˙ ϕ
where p ranges over the set of propositional variables P. The formula ϕ ∧ ψ may be read "ϕ and ψ are statically separable" and ϕ ˙ ψ may be read "ϕ and ψ are dynamically separable". Our intuition is the following: when ϕ ∧ ψ is true then the conjunction of ϕ and ψ can be updated separately; and when ϕ ˙ ψ is true then updating by the conjunction of ϕ and ψ can be performed in parallel.

We abbreviate the logical connectives ∧, → and ↔ in the usual way.

The truth conditions are as follows:

V | = p iff V(p) = 1; V | = ¬ϕ iff V | = ϕ; V | = ϕ 1 ∧ ϕ 2 iff V | = ϕ 1 and V | = ϕ 2 ; V | = ϕ 1 ∧ ϕ 2 iff there is a partition {P 1 , P 2 } of P such that V 1 | = ϕ 1 for every valuation V 1 agreeing with V on P 1 and
V 2 | = ϕ 2 for every valuation V 2 agreeing with V on P 2 ;

V | = ϕ 1 ˙ ϕ 2 iff there is a partition {P 1 , P 2 } of P such that V 1 | = ϕ 1 for some valuation V 1 agreeing with V on P 1 and V 2 | = ϕ 2 for some valuation V 2 agreeing with V on P 2 .
The conditions for the two separation operators can be reformulated in terms of partial valuations as follows:

V | = ϕ 1 ∧ ϕ 2 iff there is a partition {P 1 , P 2 } of P such that V 1 | = ϕ 1 for every extension V 1 of V| P 1 and
V 2 | = ϕ 2 for every extension V 2 of V| P 2 ;

V | = ϕ 1 ˙ ϕ 2 iff there is a partition {P 1 , P 2 } of P such that V 1 | = ϕ 1 for some extension V 1 of V| P 1 and V 2 | = ϕ 2 for some extension V 2 of V| P 2 .
Some observations:

• In the truth condition for ∧ , the exhaustiveness condition P 1 ∪ P 2 = P can be dropped. If we dropped the disjointness condition P 1 ∩ P 2 = ∅ then ϕ ∧ ψ trivialises to the conjunction ϕ ∧ ψ.

• In the truth condition for ˙ , if we drop the exhaustiveness condition P 1 ∪ P 2 = P then ϕ ˙ ψ trivialises to the consistency of both ϕ and ψ.

Here are some examples. Let V pq be a valuation such that V pq (p) = V pq (q) = 1 and let V p q be a valuation such that V p q( p) = 1 and V p q(q) = 0. Then we have:

V pq | = p ∧ q V pq | = p ˙ q V pq | = (¬p) ˙ (¬q) V pq | = p ∧ (p ∨ q) V pq | = p ˙ (¬p ∧ ¬q) V pq | = ¬p ˙ (¬p ∧ ¬q) V p q | = p ∧ (p ∨ q) V p q | = p ˙ (p ∨ q) V p q | = ¬p ˙ (p ∨ q) V p q | = p ∧ (p ∨ ¬q) V p q | = p ˙ (p ∨ ¬q) V p q | = ¬p ˙ ¬(p ∨ q)
Satisfiability and validity are defined as usual. The following formula schemas are valid:

ϕ 1 ∧ ϕ 2 ↔ ϕ 2 ∧ ϕ 1 ϕ 1 ˙ ϕ 2 ↔ ϕ 2 ˙ ϕ 1 ϕ 1 ∧ ϕ 2 → ϕ 2 ∧ ϕ 1 ϕ 1 ∧ ϕ 2 → ϕ 2 ˙ ϕ 1 ⊤ ∧ ϕ ↔ ϕ ⊤ ˙ ϕ ↔        ⊤ if ϕ is satisfiable ⊥ otherwise
As the last line shows, consistency of a formula ϕ can be expressed in the language of SSL by the formula ⊤ ˙ ϕ. Here are two inference rules preserving validity:

ϕ → ψ (ϕ ∧ χ) → (ψ ∧ χ) ϕ → ψ (ϕ ˙ χ) → (ψ ˙ χ)
The following equivalences are valid, where the propositional variables p and q are supposed to be different:

p ∧ p ↔ ⊥ p ˙ p ↔ p p ∧ ¬p ↔ ⊥ p ˙ ¬p ↔ ⊤ p ∧ q ↔ p ∧ q p ˙ q ↔ ⊤ p ∧ (p ∨ q) ↔ p ∧ q p ˙ (p ∨ q) ↔ ⊤ (p ∨ q) ∧ (p ∨ q) ↔ p ∧ q (p ∨ q) ˙ (p ∨ q) ↔ ⊤

Complexity

In this section we establish an upper bound for the complexity of both model checking and satisfiability checking of set separation logic. We prove this by showing that both ϕ 1 ∧ ϕ 2 and ϕ 1 ˙ ϕ 2 can be expressed in dynamic logic of propositional assignments DL-PA (that we have recently proposed with Philippe Balbiani and Nicolas Troquard in [START_REF] Balbiani | Dynamic logic of propositional assignments: a well-behaved variant of PDL[END_REF]) by equivalent formulas whose length is polynomial in the length of ϕ 1 ∧ ϕ 2 and ϕ 1 ˙ ϕ 2 , respectively.

DL-PA: dynamic logic of propositional assignments

The language of DL-PA is defined by the following grammar:

π p←⊤ | p←⊥ | ϕ? | π; π | π ∪ π | π * ϕ p | ⊤ | ⊥ | ¬ϕ | ϕ ∨ ϕ | π ϕ ||p←⊤|| = (V, V ′ ) : V ′ (p) = 1 and V ′ agrees with V on P \ {p} ||p←⊥|| = (V, V ′ ) : V ′ (p) = 0 and V ′ agrees with V on P \ {p} ||π; π ′ || = ||π|| • ||π ′ || ||π ∪ π ′ || = ||π|| ∪ ||π ′ || ||π * || = k∈N 0 (||π||) k ||ϕ?|| = {(V, V) : V ∈ ||ϕ||} ||p|| = {V : V(p) = 1} ||⊤|| = 2 P ||⊥|| = ∅ ||¬ϕ|| = 2 P \ ||ϕ|| ||ϕ ∨ ψ|| = ||ϕ|| ∪ ||ψ|| || π ϕ|| = {V : there is V ′ s.t. (V, V ′ ) ∈ ||π|| and V ′ ∈ ||ϕ||}
Table 1: Interpretation of the DL-PA connectives where p ranges over P. So an atomic program of the language of DL-PA is a program of the form p←ϕ. The operators of sequential composition (";"), nondeterministic composition ("∪"), unbounded iteration (" * ", the Kleene star), and test ("?") are familiar from PDL.

We define P ϕ to be the set of variables from P occurring in formula ϕ, and we define P π to be the set of variables from P occurring in program π. For example, P p←q∪p←¬q = {p, q} = P p←⊥ q .

We abbreviate the logical connectives ∧, → and ↔ in the usual way. Moreover, [π]ϕ abbreviates ¬ π ¬ϕ. The program skip abbreviates ⊤? ("nothing happens") and the program p←q abbreviates (q?; p←⊤) ∪ (¬q?; p←⊥) ("p gets the truth value of q").

DL-PA programs are interpreted by means of a (unique) relation between valuations: atomic programs p←⊤ and p←⊥ update valuations in the obvious way, and complex programs are interpreted just as in PDL by mutual recursion. Table 1 gives the interpretation of the DL-PA connectives.

A formula ϕ is DL-PA valid if ||ϕ|| = 2 P , and ϕ is DL-PA satisfiable if ||ϕ|| ∅. For example, the formulas p←⊤ ⊤ and p←⊤ ϕ ↔ ¬ p←⊤ ¬ϕ are DL-PA valid. Other examples of DL-PA validities are p←⊤ p and p←⊥ ¬p. Observe that if p does not occur in ϕ then both ϕ → p←⊤ ϕ and ϕ → p←⊥ ϕ are valid. This is due to the following semantical property. For the star-free fragment, both the DL-PA satisfiability problem and the DL-PA model checking problem are PSPACE complete.

Embedding set separation logic into DL-PA

We now give a polynomial transformation mapping set separation logic formulas ϕ 0 into DL-PA formulas.

Let P ′ be the set of variables p ′ such that p is in P and p ′ is fresh: p ′ does not occur in the formula ϕ 0 under consideration. The following abbreviations will be useful:

±p = p←⊤ ∪ p←⊥ changeSome({p 1 , • • • , p n }) = ± p 1 ; • • • ; ±p n store({p 1 , • • • , p n }) = p ′ 1 ←p 1 ; • • • ; p ′ n ←p n retrieve({p 1 , • • • , p n }) = p 1 ←p ′ 1 ; • • • ; p n ←p ′ n changeSomeMarked({p 1 , • • • , p n }) = ¬(p 1 ↔ p ′ 1 )? ∪ (p 1 ↔ p ′ 1 ?; ±p 1 ); • • • ¬(p n ↔ p ′ n )? ∪ (p n ↔ p ′ n ?; ±p n ) changeSomeUnmarked({p 1 , • • • , p n }) = p 1 ↔ p ′ 1 ? ∪ (¬(p 1 ↔ p ′ 1 )?; ±p 1 ); • • • p n ↔ p ′ n ? ∪ (¬(p n ↔ p ′ n )?; ±p n ) changeRestAndRestore({p 1 , • • • , p n }) = ((p 1 ↔ p ′ 1 ?; ±p 1 ) ∪ (¬(p 1 ↔ p ′ 1 )?; p 1 ←p ′ 1 )); • • • ((p n ↔ p ′ n ?; ±p n ) ∪ (¬(p n ↔ p ′ n )?; p n ←p ′ n ))
The program changeSome(P) nondeterministically changes the truth value of some variables in P. The program store(P) stores the truth value of each variable p by means of a fresh variable p ′ , and retrieve(P) reestablishes that 'old' value. When p and p ′ have different truth values then we say that p is marked; else we say that p is unmarked. The program changeSomeMarked(P) arbitrarily changes only the unmarked variables. The other way round, the program changeSomeUnmarked(P) leaves every unmarked p ∈ P unchanged and arbitrarily changes the marked p's.

Observe that each of the above programs has length linear in the cardinality n of the set of propositional variables {p 1 , . . . , p n }.

The next two propositions provide an embedding of set separation logic into DL-PA.

Proposition 2. Let ϕ 1 and ϕ 2 be two propositional formulas. Let P = P ϕ 1 ∩ P ϕ 2 . Let P ′ be the set of variables p ′ such that p is in P and p ′ is fresh: p ′ does not occur in the formula under consideration. Then the formula ϕ 1 ˙ ϕ 2 is equivalent to the DL-PA formula store(P); changeSome(P) Intuitively, after the program store(P) has stored the value of each of the elements of P, the program changeSome(P ′ ) allows to (nondeterministically) identify a subset of P: those p whose value differs from its copy p ′ . We consider that these 'marked' variables are those of the partial valuation for ϕ 1 , while the complementary, unmarked variables make up the partial valuation for ϕ 2 .

This can be turned more formally into a transformation from the language of set separation logic into the language of DL-PA. The transformation is clearly linear in the size of the original formula ϕ 0 .

The codomain of the transformation is the star-free fragment of DL-PA. As both model checking and satisfiability checking in DL-PA are PSPACE complete, it follows that model checking and satisfiability checking in set separation logic are in PSPACE. It remains to investigate the lower bounds.

Separability in the context of belief change operations

As we have mentioned in the introduction, one can use the SSL operators to formulate new postulates for belief change operations such as AGM belief revision operators [START_REF] Alchourrón | On the logic of theory change: Partial meet contraction and revision functions[END_REF][START_REF] Gärdenfors | Knowledge in Flux: Modeling the Dynamics of Epistemic States[END_REF] and KM update operators [START_REF] Katsuno | Propositional knowledge base revision and minimal change[END_REF][START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF]. We investigate this now in more depth.

The basic belief change postulates

Let • be a belief change operator and let β and ψ be boolean formulas. (We use β for the base and ψ for the input.) β • ψ is the result of incorporating the input ψ into the base β. Both revision and update operations were mainly studied from a semantical perspective: β • ψ is viewed as a set of valuations. Katsuno and Mendelzon promoted the distinction between belief update and belief revision [START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF]. Their idea is that update keeps track of changes in the world while revision corrects errors about an unchanged world. This can be illustrated by the revised and updated edition of a dictionary: we say that it has been revised because past errors have been corrected, and we say that it has been updated because new usages of existing words have been added to it and outdated usages have been dropped. Traditionally, β ⋄ ψ denotes the update of the base β by the input ψ and β * ψ denotes the revision of the base β by the input ψ.

Alchourrón, Gärdenfors and Makinson designed a set of postulates for belief revision operations (the so-called AGM postulates), and Katsuno and Mendelzon designed a set of postulates for belief update operations (the so-called KM-postulates). The following postulates are common to both kinds of operations:

(RE) if ||β 1 || = ||β 2 || and ||ψ 1 || = ||ψ 2 || then β 1 • ψ 1 = β 2 • ψ 2 (SUCCESS) β • ψ ⊆ ||ψ|| (PRES w ) if ||β|| ⊆ ||ψ|| then β • ψ = ||β||
where ||ϕ|| is the set of valuations where ϕ is true (just as in Section 3.1). We call the above the basic belief change postulates. RE is a postulate of insensitivity to syntax. SUCCESS says that belief change is successful: the input has priority. PRES w is a weak preservation postulate: if the input is already in the base then the base should not change. AGM revision operations moreover satisfy a strengthening of PRES w :

(PRES) if ||β|| ∩ ||ψ|| ∅ then β • ψ = ||β ∧ ψ||

Belief change operations and language splitting

It has been observed by many that the drastic update operation defined as

β • ψ =        ||β|| if ||β|| ⊆ ||ψ|| ||ψ|| otherwise
satisfies the KM postulates. Similarly, the following drastic revision operation

β • ψ =        ||β ∧ ψ|| if ||β|| ∩ ||ψ|| ∅ ||ψ|| otherwise
satisfies the AGM postulates. In order to exclude such operations, Parikh, Makinson and others argued for a further postulate of relevance [START_REF] Bienvenu | Prime implicate-based belief revision operators[END_REF][START_REF] Kourousias | Parallel interpolation, splitting, and relevance in belief change[END_REF][START_REF] Parikh | Beliefs, belief revision, and splitting languages[END_REF]. Its formulation refers to the syntax of the base and the input.

(REL) (β 1 ∧ β 2 ) • ψ = (β 1 • ψ) ∩ (β 2 • ψ) if P β 1 ∩ P β 2 = ∅
Just as in Section 2, P ϕ denotes the set of propositional variables occurring in the boolean formula ϕ. Therefore P β 1 ∩ P β 2 = ∅ means that the signatures of β 1 and β 2 are disjoint: the languages of β 1 and β 2 can be split. Each of the above drastic operations violates the postulate REL.

Separation-based belief change operations

In the same spirit and as already stated informally in the introduction, the SSL operators enable us to go beyond such syntax-based postulates and strengthen the above relevance postulate REL. The strengthening comes in a static version and in a dynamic version:

(REL s ) (β 1 ∧ β 2 ) • ψ = (β 1 • ψ) ∩ (β 2 • ψ) (REL d ) β • (ψ 1 ˙ ψ 2 ) = (β • ψ 1 ) • ψ 2 = (β • ψ 2 ) • ψ 1
where • is any belief change operation, be it update or revision. 2 The static relevance postulate REL s says that when the bases β 1 and β 2 are statically separable then they can be updated separately. Its dynamic counterpart REL d says that when the inputs ψ 1 and ψ 2 are dynamically separable then the update can be performed in parallel (or rather, in an interleaving fashion). It turns out that both postulates are violated by any AGM revision operation and and any KM update operation. Proof. Suppose • satisfies the basic belief change postulates and REL s . Consider the base β = (p ∨ q) ∧ (p ∨ q) and the input ψ = p ∨ q. We have seen above that β is equivalent to p ∧ q, and we therefore have:

β • ψ = (p ∨ q) ∧ (p ∨ q) • p ∨ q = p ∧ q • p ∨ q (by RE) = ||p ∧ q|| (by PRES w )
This is incompatible with what postulate REL s gives us: Proof. Suppose • satisfies the KM postulates and REL d . Consider the base β = ¬p and the input ψ = ¬p ˙ p. We have seen above that ψ is equivalent to ⊤, and we therefore have:

β • ψ = (p ∨ q) ∧ (p ∨ q) • p ∨ q = p ∨ q • p ∨ q ∩ p ∨ q • p ∨ q (by REL s ) = ||p ∨ q|| ∩ ||p ∨ q|| (by PRES w ) = ||p ∨ q||
β • ψ = ¬p • ¬p ˙ p = ¬p • ⊤ (by RE) = ||¬p|| (by PRES w ) This is incompatible with what postulate REL d gives us: 3 β • ψ = ¬p • ¬p ˙ p = (¬p • ¬p) ⋄ p (by REL d ) = ¬p • p (by PRES w ) ⊆ ||p|| (by SUCCESS)
Incompatibility is the case because the set of valuations where ¬p is true is non empty.

We have introduced a simple version of separation logic working on sets (alias propositional valuations) that we have called set separation logic, SSL. Our logic has two separation operators: ∧ allows to separate resources, and ˙ allows to separate updates.

We have shown that in our logic, both model checking and satisfiability checking can be done in polynomial space. We conjecture that the PSPACE upper bound that we have established coincides with the lower bound, but this remains to be proved. We would also like to provide an axiomatisation.

In the last part of the paper we have investigated the relation between SSL and belief change operations. We have formulated two postulates that appear to be natural and have shown that they are nevertheless incompatible with both AGM belief revision operations and KM belief update operations.

The problem of belief change respecting separation that we have studied in the last section is related to the frame problem in artificial intelligence [START_REF] Mccarthy | Some philosophical problems from the standpoint of artificial intelligence[END_REF]. Reiter's solution to that problem [START_REF] Reiter | The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression[END_REF][START_REF] Reiter | Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems[END_REF] is by now widely accepted for actions without ramifications, i.e., without side effects. In joint work with Hans van Ditmarsch and Tiago de Lima [START_REF] Hans Van Ditmarsch | From Situation Calculus to Dynamic Logic[END_REF] we have recently shown that Reiter's solution can be mapped to dynamic logics with propositional assignments DL-PA. Given that set separation logic can be embedded into DL-PA, it is immediate to extend it by propositional assignments.

It would be interesting to add the implicational connective - * of separation logic to SSL (which should lead to undecidability given the results of [START_REF] Brotherston | Undecidability of propositional separation logic and its neighbours[END_REF][START_REF] Larchey | The undecidability of boolean bi through phase semantics[END_REF]). it is however not clear how the semantics of - * can be defined in the framework of valuations.

Proposition 1 .

 1 Suppose p P ϕ , i.e., p does not occur in ϕ. Then ϕ ∈ ||V ∪ {p}|| iff ϕ ∈ ||V \ {p}||.Theorem 1 ( [2]). For the full language, both the DL-PA satisfiability problem and the DL-PA model checking problem are EXPTIME complete.

Proposition 4 .

 4 There is no operation • satisfying both the basic belief change postulates and REL s .

Proposition 5 .

 5 There is no operation • satisfying both the basic belief change postulates and REL d .

  Proposition 3. Let ϕ 1 and ϕ 2 be two propositional formulas. Let P = P ϕ 1 ∩ P ϕ 2 . Let P ′ be the set of variables p ′ such that p is in P and p ′ is fresh: p ′ does not occur in the formula under consideration. Then the formula ϕ 1 ∧ ϕ 2 is equivalent to the following DL-PA formula:

	store(P); changeSome(P ′ ) [changeSomeMarked(P)]ϕ 1 ∧
	[changeSomeUnmarked(P)]ϕ 2
	changeRestAndRestore(P) changeSome(P ϕ 2 \ P) ϕ 2

changeSome(P ϕ 1 \ P) ϕ 1 ∧

We might as well define valuations to be sets of propositional variables. However, it would have been less elegant to account for partial valuations under such a presentation.

Strictly speaking, REL d requires to build a formula representing the updates β • ψ 1 and β • ψ 2 , as usually done in the KM framework.

We recall that the second line of the proof is formulated sloppily: instead of the set of valuations ¬p•¬p there should be a formula representing that valuation.

Acknowledgements

The work in this paper was done in the framework of the ANR project DynRes (Dynamic Resources and Separation and Update Logics, project no. ANR-11-BS02-011). I would like to thank the members of the project for their comments of a (very preliminary) presentation of the ideas that are worked out in more detail here. Thanks are also due to the reviewers of WoLLIC 2013 whose comments I took into account as far as I could.


Tony Flores Pulgar

Jean-Luc Scharbarg

Katia Jaffrès-Runser

Extending CAN over the air: an interconnection study with IEEE802.11

The flexibility of wireless connectivity is appealing in the context of industrial networks. This paper discusses the use of a wireless protocol to interconnect remotely located fieldbuses. The focus of this paper is to analyze the feasibility and design issues related to this type of hybrid network architecture. Therefore, we concentrate on deriving appropriate bridging strategies for a network topology composed of remotely located CAN buses interconnected through a wireless local area network following the IEEE802.11g protocol. Using this very simple and costeffective architecture, we show in this study that by intelligently leveraging the features of CAN and IEEE802.11g in the interconnection policies employed, the missed deadlines can be limited for the CAN frames carried by the wireless network.

Introduction

Industrial fieldbus technologies are widely rolled out to offer real-time communication capabilities on the factory floor. A large set of protocols offer deterministic and timely bounded transmissions using tailored medium access schemes and architectures (e.g. PROFIBUS, PROFINET, TTEthernet, etc.). Controller Area Network [START_REF] Bosch | CAN Specification version 2.0[END_REF] is one of the mainstream standards for embedded communications. Despite the fact that it has been originally developed for automotive communications, CAN has found its place in factory automation applications to handle sensor-actuator communications because of its ease of use and the low cost of its controllers.

Recent developments for industrial communications consider introducing wireless transmissions into the global network architecture [START_REF] Pellegrini | On the use of wireless networks at low level of factory automation systems[END_REF][10] [START_REF] Willig | Wireless technology in industrial networks[END_REF]. First studies have assessed the capabilities of mainstream wireless technologies such as WiFi (IEEE802.11 [START_REF]IEEE Standard for Information technology-Telecommunications and information exchange between systems Local and metropolitan area networks Specific requirements Part 11: Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) Specifications[END_REF]), Bluetooth or Zig-Bee (IEEE802.15.4) [START_REF] Willig | Wireless technology in industrial networks[END_REF] for real-time communications. In parallel, new real-time wireless protocols have been designed [START_REF] Costa | Comparing rt-wifi and hcca approaches to handle real-time traffic in open communication environments[END_REF] [6] [START_REF] Ng | Performance evaluation of wireless controller area network (wcan) using token frame scheme[END_REF] [START_REF] Pereira | Widom: A dominance protocol for wireless medium access[END_REF] [9] [START_REF] Song | Wirelesshart: Applying wireless technology in real-time industrial process control[END_REF]. Recently, a TDMA-oriented solution called WirelessHART has been commercialized for factory automation applications [START_REF] Song | Wirelesshart: Applying wireless technology in real-time industrial process control[END_REF]. The main pit-fall of wireless communications is of course the increased unreliability the medium suffers from due to interference and pathloss compared to shielded wires.

There are several main motivations for developing a wireless fieldbus technology. First, wireless networks are much easier to deploy than wired networks. Second, mobile entities such as robots can communicate seamlessly. The works on wireless real time protocol design clearly aim at leveraging these two features. Another interesting benefit of wireless transmissions is to provide a costeffective network to interconnect distant heterogeneous or homogeneous legacy fieldbuses. The focus of this paper is to discuss this last use case of wireless communications.

A wireless interconnection will benefit architectures where several fieldbuses, located far from each other, need a backhaul network to exchange data. Either legacy wireless technologies such as WiFi or dedicated wireless protocols such as WirelessHART may be chosen, depending on the nature of the traffic exchanged between the remote buses. For hard real-time data, a dedicated reliable wireless solution has to be picked [START_REF] Costa | Comparing rt-wifi and hcca approaches to handle real-time traffic in open communication environments[END_REF] [START_REF] Guedes | A new {MAC} scheme specifically suited for real-time industrial communication based on {IEEE} 802[END_REF], while for soft realtime data, a cheaper and probably less reliable wireless technology can be chosen. But for both cases, we argue that the key point to achieve a timely behaviour of the endto-end flows in the network is to carefully define the bridging strategies of the wireless gateways interconnecting the fieldbuses with the wireless network.

This statement is illustrated in this paper with the interconnection of CAN buses through a standard IEEE802.11g wireless network using CSMA/CA (Carrier Sense Multiple Access with Collision Avoidance) medium access control in ad hoc mode. In this study case, soft real-time data is exchanged between the remote CAN networks using low-cost wireless Access Points. The paper proposes and discusses different bridging strategies that account for the specifics of CAN and CSMA/CA. The aim of this study is to highlight their impact on end-toend communication delays in a network where periodic flows are to be received in a timely manner. Of course, CSMA/CA being far from deterministic, the end-to-end (E2E) communication delay is not bounded anymore. But we show through simulations that intelligent encapsulation strategies of CAN frames into WiFi frames signifi-cantly improve the communication delay on the wireless network. Moreover we clearly show that this architecture is a good candidate for soft real-time traffic.

In our previous work [START_REF] Scharbarg | CAN-Ethernet architectures for real-time applications[END_REF], interconnection of CAN buses via legacy Ethernet has been studied. The motivation of studying interconnection through CSMA/CA for WiFi relies on the following facts:

First, a collision on Ethernet is far less time-consuming than on CSMA/CA since it is very quickly detected by emitters. Second, throughput on both technologies is different (e.g. 100 Mbps vs. up to 54 Mbps), at least doubling the transmission duration of a frame. Third, the overhead of collision avoidance and acknowledgement procedure triggers an additional timing overhead for CSMA/CA compared to CSMA/CD. This paper is organised as follows. Section 2 describes the architecture of interest. Section 3 proposes different bridging strategies. The performance of these strategies is analysed in Section 4. Section 5 concludes the paper and gives directions for future work. An example of the hybrid architecture targeted in this paper is described in Figure 1. Remote embedded networks follow the widely available CAN standard [START_REF] Bosch | CAN Specification version 2.0[END_REF]. The wireless local area network interconnecting the remote embedded buses follows the mainstream IEEE802.11g standard [START_REF]IEEE Standard for Information technology-Telecommunications and information exchange between systems Local and metropolitan area networks Specific requirements Part 11: Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) Specifications[END_REF]. A gateway is implemented between each CAN bus and the IEEE802.11 network. The example in Figure 1 includes three CAN buses and three pure wireless nodes N W 1 . . . N W 3 . Four nodes including one gateway are connected to each CAN bus (e.g.

Case study architecture

N C 4 , N C 5 , N C 6 , Gw 2 for CAN bus 2).
All wireless transmitters (GW 1 , N W 1 , . . .) are interconnected in ad hoc mode (no access point architecture).

Definition of the flows

Three kinds of flows are transmitted over this architecture:

• pure CAN flows are transmitted between stations connected on the same CAN bus: they do not transit on IEEE802.11,

• pure IEEE802.11 flows are transmitted between wireless stations: they do not transit on CAN,

• hybrid flows are transmitted between stations connected on different CAN buses: they transit on both technologies, via the gateways.

A pure CAN flow f C i is defined by the following elements:

• an identifier IdC i between 0 and 2047,

• a source node srcC i and a set of destination nodes destC i which all belong to the same CAN bus as the source node srcC i ,

• a period P C i which is the duration between the generation of two consecutive frames of the flow,

• a critical delay DC i which is the maximum allowed duration between the generation of a frame and its reception by its destination nodes,

• the size SC i in bytes of the payload of each frame of the flow.

A hybrid flow f H j is defined by the same elements as a pure CAN flow: an identifier IdH j , a source node srcH j , a set of destination nodes destH j , a period P H j , a critical delay DH j and the size SC j in bytes of the payload of each frame of the flow. The only difference is that destination and source nodes belong to different CAN bus. A pure IEEE802.11 flow f W k is defined by the following elements:

• a source node srcW k and a set of destination nodes destW k which are all connected to IEEE802.11,

• an average inter-frame duration P W k , following an exponential distribution (Poisson traffic),

• the size SW k in bytes of the payload of each frame of the flow. This configuration will be used as an illustrative example in the rest of the paper.

CAN protocol

The Controller Area Network (CAN, [START_REF] Bosch | CAN Specification version 2.0[END_REF]) is a serial communication protocol suited for networking sensors, actuators and other nodes in real-time systems. The CAN specification defines several versions of the protocols for the physical and the data link layer. In this paper, we focus on CAN 2.0 A.

Figure 2. CAN frame (sizes in bits)

The frame format is depicted in figure 2. Only the three following fields are relevant to the remainder of the paper:

• the identifier field, as mentioned earlier, identifies the data carried by the frame,

• the DLC field gives the length (in bytes) of the data field,

• the data field carries the payload of the frame.

Bit-stuffing is used to avoid the transmission of long sequences of bits with identical value. The computation of the frame length has to take into account these additional bits. In this paper, we use the upper bound given in [START_REF] Davis | Controller Area Network (CAN schedulability analysis: refuted, revisited and revised[END_REF].

The length C of a frame carrying S bytes of data is:

C = (55 + 10 × S) (1)
The medium access control (MAC) is CSMA/CR: the start of frame transmissions on the bus are synchronous. When two or more stations start a transmission simultaneously, the one with the smallest frame identifier wins and the others stop their transmission. This mechanism guarantees strict priority order on identifiers. It implies limitations on the bandwidth and the maximal length of the bus (e.g. 1 Mbps for 40 meters).

IEEE 802.11 MAC protocol

IEEE 802.11-2012 [START_REF]IEEE Standard for Information technology-Telecommunications and information exchange between systems Local and metropolitan area networks Specific requirements Part 11: Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) Specifications[END_REF] defines several standards to offer a wireless connectivity at transmission rates ranging from 11Mbps (e.g. legacy versions such as IEEE 802.11b) up to 600Mbps (IEEE 802.11n).

The fundamental medium access in IEEE 802.11 is a Distributed Coordination Function (DCF) which is based on Carrier Sense Multiple Access with Collision Avoidance (CSMA/CA). Additional protocols are defined to meet specific requirements but all use the service provided by DCF. In this work, we firstly concentrate on the basic DCF medium access to characterize the wireless medium access. In future work, it will be interesting of course to analyze how real time applications can leverage the QoS capabilities of enhanced protocols (e.g. EDCA, HCCA).

In DCF mode, a station performs carrier sensing to detect ongoing communications. If the channel is free for a period of time called Distributed InterFrame Space (DIF S), it transmits its frame immediately. If the channel is sensed busy, it defers its transmission until the end of the current transmission. Then, the station selects a random backoff b following an exponential backoff scheme. If the medium is idle for a DIF S period of time, the backoff is decremented every aSlotTime duration. The backoff interval time is decremented as long as the channel is idle and is frozen as the node detects a transmission. At the end of this transmission, when the channel remains idle during DIF S, decrementation resumes. As b reaches zero, the transmission is attempted immediately by the station.

After a successful transmission, the receiver sends an ACK after a duration called Short Inter Frame Space (SIF S). As SIF S is shorter than DIF S (DIF S = SIF S + 2 × aSlotT ime), there is no station that sees the channel idle until the end of the ACK transmission. If no ACK is received by the transmitter after an Extended Interframe Space (EIF S = SIF S + DIF S + ACKT xT ime 1 ), the transmission is attempted again.

A new backoff b is then uniformly chosen in the range [0, w-1] where w is the contention window. This window depends on the number of failed attempts experienced by the current transmission. At the first attempt w is equal to the minimum contention window CW min . Each unsuccessful transmission involves the multiplication of w by 2 until a maximum value of CW max is reached.

This Basic Access mechanism can be extended by the RTS/CTS message exchange to avoid the hidden terminal problem. In our architecture, all wireless transmitters are fixed and positioned in such a way that the hidden terminal problem doesn't occur. Thus, there is no motivation for implementing RTS/CTS mechanism in our case study.

In this paper, all wireless nodes (gateways, pure wireless emitters) function in ad hoc mode using DCF medium access protocol following the specification of the OFDM-PHY layer of 802.11g (20 MHz channel spacing). Table 2 gives the main timing parameters of the protocol. Since WiFi access points are static, we can consider that they are located at a distance where they can operate at the highest rate of 54 Mbps. We assume proper channel assignment has been performed so as to mitigate inter-node interference. In this ideal case study, transmissions are error-free and the transmission duration (in µ s) at 54 Mbps of a 1 with ACKT xT ime the transmission time of an ACK at the lowest mandatory transmission rate MPDU of x octets is derived according to [START_REF]IEEE Standard for Information technology-Telecommunications and information exchange between systems Local and metropolitan area networks Specific requirements Part 11: Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) Specifications[END_REF]:

d(x) = 20

The bridging strategy

The interconnection between each CAN bus and the IEEE802.11 network is implemented by a gateway (see Figure 1). Each gateway has to take into account the address mode of both CAN and IEEE802.11 technologies: CAN frame is addressing data while IEEE802.11 technology is addressing the source destination pairs. In order to cope with the address mode issue, an encapsulation strategy is considered. A frame f 1 of an hybrid flow f CW j is received by the gateway which is connected to its source CAN bus. This frame is encapsulated into an IEEE802.11 frame f 2 and transmitted on the wireless medium to the remote gateway connected to the destination CAN bus of f 1 . This gateway de-encapsulates f 1 which is then transmitted on its destination CAN bus.

Here, the two encapsulating gateways work in a symmetric way to enable a CAN to CAN remote communication. The bridging strategy is a generalization of an IEEE802.1d transparent bridge mechanism for the interconnection of two homogeneous networks through a different one.

The following paragraph presents the basic encapsulation strategy. Then, enhancements of this strategy are proposed in order to better use the available resources while keeping the end-to-end delay of hybrid flows in an acceptable margin.

Basic encapsulation strategy

In this basic encapsulation strategy, the source gateway encapsulates the CAN frame f 1 of f H j in the payload field of the IEEE802.11 frame f 2 . As soon as f 2 arrives at the destination gateway, f 1 is de-encapsulated.

The following derivations are illustrated using the example in Figure 1.

A possible scenario is depicted in Figure 3. A subset of the system is shown, i.e. CAN buses 1 and 2 and the wireless network. Rising arrows indicate the instant when frames are ready for transmission on the corresponding medium.

Let's focus on the hybrid flows f H A straightforward solution which limits this overhead consists in encapsulating more than one CAN frame in one IEEE802.11 frame. We denote N l,m , the exact number of CAN frames which are encapsulated in an IEEE802.11 frame at a given gateway Gw l when its destination is gateway Gw m .

Let's come back to the example in Figure 1. Let's assume that Gw 1 encapsulates three CAN frames in each IEEE802.11 frame with destination Gw 2 (N 1,2 = 3, while all the other N l,m are equal to 1). We recall that f H 4 is sent to Gw 3 . Thus, only frames from f H 3 , f H 2 and f H 1 can be grouped together. The impact of this strategy on the example is shown in Figure 4 4). This frame is transmitted on the wireless medium after a DIFS, since the medium is idle and there are no other pending frames. Gw 2 receives the frame and it decapsulates the three CAN frames. Finally, these frames are transmitted on CAN bus 2 in their order of priority. On this very simple example, the grouped strategy reduces the number of wireless frames (from 7 to 5) and there are no more collisions (there are never two pending frames at the same time).

Timers to decrease the delay of hybrid flows

The drawback of the grouped strategy is that it can delay some frames of hybrid flows that are combined together at their source gateway. In the example in Figure 4, the f H 3 frame has to wait until the arrival of the f H 1 frame. This delay can be very large. Considering the same example, let's assume that Gw 1 encapsulates two CAN frames instead of three in each IEEE802.11 frame with destination Gw 2 . A possible scenario is depicted in Figure 5. Only the events on CAN bus 1 and gateway Gw 1 are shown. The two first frames from hybrid flows (f H 3 and f H 2 ) are received and encapsulated by Gw 1 at time t + 0.6 ms. The third frame (from hybrid flow f H 1 ) has to wait in Gw 1 for the arrival of another frame from an hybrid flow. On this example, the time elapsed between the generation of the frame from f H 1 and its encapsulation in an IEEE802.11 frame is 7.8 ms. Since the critical delay of f H 1 is 8 ms, this frame has no chance to respect its deadline. One solution to overcome this problem is to upper bound the waiting time of a CAN frame in a gateway. It can be implemented by associating to each hybrid flow f H j a maximum waiting time W max j in its source gateway Gw l . When a frame from f H j arrives at its source gateway Gw l , two situations may occur:

CAN bus 1

Gw1

1. There are already N l,m -1 pending CAN frames in Gw l with the same destination CAN bus as the frame from f H j : these N l,m CAN frames are immediately encapsulated in an IEEE802.11 frame which is then ready for transmission.

2. there are less than N l,m -1 pending CAN frames in Gw l with the same destination CAN bus as the frame from f H j : a timer with duration W max j is started.

If the frame from f H j is still waiting when the timer expires, the frame is immediately encapsulated in an IEEE802.11 frame with all the other pending CAN frames having the same CAN destination bus.

Figure 6 shows the impact of these timers on the scenario in Figure 5. In this example, the maximum waiting time of a frame in gateway Gw 1 is 2 ms for flows going to Gw 2 , and N 1,2 = 2. f HG 1 is generated because there are two pending frames with CAN bus 2 as destination. f HG 2 is generated because the timer which is associated with the frame of flow f H 1 has expired. Thus f HG 1 encapsulates two CAN frames, while f HG 2 encapsulates only one. This strategy obviously favours a timely transmission of the f H 1 frame.

CAN bus 1

Gw1

Summary of the proposed strategies

All previously introduced strategies (basic, grouped, timed) can be characterized by the following parameters:

• The maximum number N l,m of CAN frames which can be encapsulated by each gateway Gw l in one IEEE802.11 frame,

• The maximum waiting time W max j of a frame of each hybrid flow f H j in its source gateway.

Thus, we have:

• When N l,m = 1 for all the gateways pairs or W max j = 0 for all hybrid flows, the basic strategy is applied,

• when at least one N l,m is greater than one and each W max j is larger than the critical deadline of its corresponding flow, the grouped strategy is applied,

• otherwise, the timed strategy is applied.

Bridging performance analysis

A quantitative analysis of the proposed bridging strategies has been conducted. This analysis is based on simulations. Therefore, a home-made simulation tool has been developed using QNAP2 [START_REF] Simulog | [END_REF].

In the following paragraphs, we consider two network configurations:

• the illustrative configuration of Figure 1 • a more complex configuration introduced in Section 4.2.

Illustrative configuration (CS1)

The first configuration is depicted in Figure 1 and the features of the flows are summarised in Table 1. All proposed encapsulation strategies (basic, grouped timed) are evaluated as presented in Table 3.

B basic G1 grouped N 1,2 = 2 N l,m = 1 ∀ (l, m) = (1, 2) G2 grouped N 1,2 = 3 N l,m = 1 ∀ (l, m) = (1, 2) T1 timed W max j = 1 ms ∀j T2 timed W max j = 2 ms ∀j T3 timed
W max j = 3 ms ∀j T4 timed W max j = 4 ms ∀j Table 3

. CS1: simulated strategies

We first look at the percentage of pure CAN and hybrid frames that miss their deadline. Whatever strategy is chosen, pure CAN frames never miss their deadline. Similarly, with the basic and timed strategies, hybrid frames never miss their deadline. Conversely, with the grouped strategies, some hybrid frames miss their deadline (0.2 % with G1, 0.5 % with G2). These results are not surprising. Indeed the overall configuration is lightly loaded. Thus a missed deadline is impossible for pure CAN flows and it can arise for hybrid flows only when the delay between the two CAN buses is high. This delay includes the waiting time at the source gateway, the IEEE802.11 delay (very unlikely to be high since the wireless medium is lightly loaded) and the waiting time at the destination gateway (short de-encapsulation time). Then a missed deadline will occur only when the waiting time in the source gateway is high. This can be the case with the grouped strategies, as shown in section 3.2. This result confirms the flaws introduced by the grouped strategies. These strategies are not further considered.

B T1 T2 T3 T4

f Hj f W1 1 0.88 0.77 0.7 0.53

Table 4. CS1: load of hybrid wireless frames

A second result concerns the frames which are transmitted on the wireless medium. Given the Poisson traffic distribution of pure wireless flows, their average number of frames is steady. Conversely, the number of wireless frames from hybrid flows depends on the encapsulation strategy which is used. Table 4 compares the number of wireless frames of hybrid flows to the number of frames of one of the pure wireless flows (e.g. f W 1 ). For the basic strategy, these two number of frames happen to be the same because of the period allocation of hybrid flow. Without surprise, this ratio decreases with the increase of the maximum delay at the gateway.

Table 5 shows the percentage of collisions for each strategy. This percentage is very low (never more than 0.4 %). This is a consequence of the light load of the wireless medium. Moreover, this percentage decreases when the value of the maximum delay in the gateway increases (the overall number of wireless frames decreases). B T1 T2 T3 T4 Col. (%) 0.375 0.358 0.343 0.335 0.328 Table 5. CS1: wireless collisions Table 6 shows the average delay of pure wireless flows. This delay decreases when the value of the maximum delay in the gateway increases. This is also a consequence of the reduction of the overall number of wireless frames.

Table 6. CS1: average delay of pure wireless flows

The results confirm the qualitative analysis of section 3. However, the small illustrative configuration considered in this section is too lightly loaded for a significant quantitative analysis of the different strategies. Such an analysis is conducted in the next section. It includes four CAN buses. Each CAN bus 1, 2 and 3 is the source of 8 hybrid flows. Bus 4 is the destination of all these hybrid flows. Table 7 summarizes the parameters of these hybrid flows. For the sake of simplicity, only the source and destination buses of these flows are given (the nodes are omitted). 8 summarises the parameters of these pure CAN flows. For clarity purposes, the bus ID these pure CAN flows belong to are only given.

IdCi Bus P Ci DCi SCi f C1 1 4 2 2 8 f C2 2 4 2 2 6 f C3 3 4 2 2 4 f C4 4 4 2 2 2 f C5 21 1 1 1 8 f C6 22 1 1 1 6 f C7 23 1 1 1 4 f C8 24 1 1 1 2 f C9 41 2 1 1 8 f C10 42 2 1 1 6 f C11 43 2 1 1 4 f C12 44 2 1 1 2 f C13 61 3 1 1 8 f C14 62 3 1 1 6 f C15 63 3 1 1 4 f C16 64 3 1 1 2

Table 8. CS2: pure CAN flows

The study is conducted with different numbers of identical pure IEEE802.11 flows (between 1 and 7) with P W i = 2 and SW i = 200.

We have conducted three sets of experiments:

• in the first one, we consider the basic encapsulation strategy,

• in the second one, we consider a timed encapsulation strategy where all hybrid flows are allocated the same maximum waiting delay,

• in the last one, we consider another timed encapsulation strategy where each hybrid flow is allocated a dedicated maximum waiting delay following W max j = (4.1 -(j × 0.1)) ms.

Table 9 summarises the simulated strategies.

results

Table 10 also shows the percentage of collisions and the average delays of pure wireless flows for each strategy and each simulated scenario (i.e. number of pure wireless flows). Empty values means that the wireless network is overloaded and transmission delays diverge. It can be noticed that these percentages of collisions (% Col) and delays (AvgD) are deeply linked to the number of contending IEEE802.11 frames.

Thus higher values of timers give smaller delays on the wireless network. However, they also increase the waiting time of hybrid frames in gateways. It means that a trade-off has to be found between the waiting delays in the gateways and the delays on the wireless network.

In order to better capture this trade-off, Table 11 presents the rates of hybrid frames which miss their deadlines. More precisely, each value in Table 11 is the average number of hybrid frames that miss their deadlines when 10 6 of such frames are generated and transmitted. Such missed deadline rates are compatible with soft real-time data transmissions.

We can conclude that the timed strategies outperform the basic one. Indeed, the basic strategy cannot cope with more than 4 pure IEEE802. The value of the timer also has an impact on the number of missed deadlines. In the configuration studied in this paragraph, the best value is 3 ms for all the hybrid flows (less than half of their period). It should be noticed that strategy T 5 gives slightly larger numbers of missed deadlines. The idea behind this strategy was to limit the waiting time in gateways for the hybrid flows with the lowest priorities, since they can experiment larger delays on CAN buses. The results for this strategy are not convincing.

In the general case, the choice of this timers has to take into account the distribution of the delays on the wireless network as well as the distribution of the delays on the CAN buses. Then these distributions have to be combined so that the distribution of the overall delay of the flows, excluding the waiting time at the gateways, can be obtained. A maximum waiting time at the gateway could be deduced from this distribution. To the best of our knowledge, the computation of such a distribution is still an open problem.

Conclusion and future works

This paper studies the extension of CAN over the air for the exchange of soft real-time data. CAN buses are interconnected through a standard IEEE802.11g wireless network using CSMA/CA medium access control in ad hoc mode. The interconnection between CAN and the wireless network is done by gateways. The bridging strategy implemented in these gateways is a key issue in such an architecture. We show on a case study that the best strategy consists in encapsulating a group of CAN frames in each IEEE802.11 frame while bounding the waiting time of each CAN frame at the ingress gateway. With such a strategy, the number of missed deadlines can be kept very small, provided that the wireless channel is reliable (we assume no transmission errors except collisions).

In future work, we will investigate the impact of a lossy wireless link where wireless nodes transmit at different rates. Another improvement is to derive analytically the timers of the hybrid flows. Lastly, in order to cope with hard real-time data, we will investigate more deterministic wireless protocols (HCCA, WirelessHART, . . .).

Figure 1 .

 1 Figure 1. Architecture example

Figure 5 .

 5 Figure 5. Flaw of the grouped strategy

Figure 6 .

 6 Figure 6. The timed strategy

Figure 7 . CS2 architecture overview 4 . 2 .

 742 Figure 7. CS2 architecture overview

B

  11 flows: the system doesn't deadline every 10 6 frames Table 11. CS2: Missed deadlines for hybrid flows converge. Conversely the timed ones are still working with 6 or 7 pure IEEE802.11 flows. These results are compatible with soft real-time data transmissions.

Table 1

 1

	presents the set of flows which are transmitted on
	the network architecture in Figure 1. Hybrid flows are
	depicted with dotted lines while other ones with full black
	lines. There are three pure CAN flows (one per CAN bus),
	four hybrid flows and three pure IEEE802.11 flows. The
	four hybrid flows are generated by stations from CAN bus
	1. Three of them (f H 1 , f H 2 and f H 3 ) have their desti-
	nation nodes on CAN bus 2, while the last one (f H 4 ), has
	its destination node on CAN bus 3.

Table 1 . Characteristics of the flows The

 1 CAN addressing system is based on message identifiers: a frame neither has a destination nor a source address. Frames are broadcasted on the bus. Stations get the frames they are interested in by filtering out the identifiers.

							Pure CAN flows
			IdCi		srcCi	destCi	P Ci	DCi	SCi
	f C1	10		N C1	N C2		4	4	8
	f C2	11		N C5	N C6		4	4	8
	f C3	12		N C7	N C9		4	4	8
							Hybrid flows
			IdHi		srcHi	destHi	P Hi	DHi	SHi
	f H1	1			N C1	N C4, N C6	8	8	8
	f H2	2			N C2	N C5, N C6	8	8	8
	f H3	3			N C3	N C4		8	8	8
	f H4	4			N C3	N C7, N C8	8	8	8
							Pure IEEE802.11 flows
		srcWi		destWi	P Wi	SWi
	f W1	N W1		N W3	2		200
	f W2	N W2		N W3	2		200
	f W3	N W3		N W1	2		200
	1	11		1 1 1	4	0..64	16	2	7	3
	SOF	Identifier	RTR	IDE	r0	DLC	Data	CRC	ACK	EOF	IFS

Table 2 . DCF parameters for OFDM-PHY Future

 2 works will concentrate on the impact of channel errors which are handled by the IEEE802.11 DCF protocol. Additional transit time due to retransmissions will arise in this case.

	+ 4	22 + 8(34 + x) 216	(2)
	SIFS DIFS EIFS CW min CW max
	16 µs 34 µs 78 µs	15	1023

  1 , f H 2 , f H 3 , f H 4 . All of them have their source node on CAN bus 1. One frame from hybrid flow f H 3 becomes ready for transmission on CAN bus 1 while one frame of flow f C 1 is being transmitted. At time t+0.135 ms, CAN bus 1 becomes idle. The frame from f H 3 is transmitted since it is the only pending frame. It is fully received by Gw 1 at time t+0.270 ms. It is then encapsulated by Gw 1 in an IEEE802.11 frame which becomes ready during the transmission of a frame from f W 2 . After this transmission, frames from f H 3 and f W 3 compete for the medium. They select the same random backoff. Consequently, they collide. At the end of this collision the frame from f H 3 gets access to the medium thanks to a random backoff which is smaller than the one of f W 3 . Then, the frame from f H 3 is received by Gw 2 , de-encapsulated and transmitted on CAN bus 2 which is idle. This transmission is achieved at time t + 0.8 ms.

	fC1	fH3			fH4 fH2		fH1
	CAN bus 1	fC1	fH3		fH4	fH2	fH1
		fW2 fW3	fH3	fW1	fH4	fH2	fH1
	IEEE802.11		fW2		fH3	fW1	fH4	fW3	fH2	fH1
						fH3			fH2	fH1
	CAN bus 2						fH3		fH2	fH1
	t	t+0.135 t+0.270			t+0.8		t+1.2	t+1.335	time
	Figure 3. Scenario with a basic strategy
	• 3.2. Grouping for a better use of the wireless medium
	This basic strategy is very simple but it doesn't use ef-
	ficiently the wireless medium. Indeed, encapsulating one
	single CAN frame (let's say 10 bytes) in an IEEE802.11
	frame (up to 2312 bytes of payload) generates a signifi-
	cant overhead: typically, assuming no collision and a null
	backoff, the overall time needed for one frame with a 10
	bytes payload (DIFS + transmission of the frame + SIFS
	+ transmission of ACK) is obtained from formula (2):
	34 + 20 + 4	22 + 8(34 + x) 216	+ 16 + 24 = 102 µs

• Similarly, frames from f H 4 , f H 2 and f H 1 are generated in this order. With respect to their priorities, they are transmitted in the same order on CAN bus 1. Each of them is then encapsulated in a separate IEEE802.11 frame. These frames have to share the wireless medium with frames from pure IEEE802.11 flows f W 1 and f W 3 . In this scenario, the selected random backoffs do not lead to any collision. Frames from f H 2 and f H 1 are transmitted last. Finally, they are de-encapsulated by Gw 2 and transmitted on CAN bus 2. They are received by their destination nodes at times t + 1.2 ms and t + 1.335 ms.

Given a payload of 50 bytes, the same sequence needs 110 µs.

  . Gw 1 receives

	fC1	fH3		fH4 fH2	fH1
	CAN bus 1	fC1	fH3	fH4	fH2	fH1
		fW2 fW3	fW1	fH4		fHG1
	IEEE802.11		fW2	fW3	fW1	fH4	fHG1
							fH1, fH2, fH3
	CAN bus 2						fH1	fH2	fH3
	t		t+0.270		t+0.735 t+0.870	time

Figure 4. Scenario with a grouped strategy frames from f H 3 , f H 2 and f H 1 at times t + 0.270, t + 0.735 and t + 0.870, respectively. Then, it encapsulates the three CAN frames in one IEEE802.11 frame (called f HG 1 in Figure

Table 7 . CS2: hybrid flows

 7 Four pure CAN flows are transmitted on each CAN bus 1, 2, 3 and 4. Table

		IdHi	Buses	P Hi	DHi	SHi
	f H1	11	1 → 4	10	10	8
	f H2	12	1 → 4	10	10	6
	f H3	13	1 → 4	10	10	4
	f H4	14	1 → 4	10	10	2
	f H5	15	1 → 4	10	10	8
	f H6	16	1 → 4	10	10	6
	f H7	17	1 → 4	10	10	4
	f H8	18	1 → 4	10	10	2
	f H9	31	2 → 4	10	10	8
	f H10	32	2 → 4	10	10	6
	f H11	33	2 → 4	10	10	4
	f H12	34	2 → 4	10	10	2
	f H13	35	2 → 4	10	10	8
	f H14	36	2 → 4	10	10	6
	f H15	37	2 → 4	10	10	4
	f H16	38	2 → 4	10	10	2
	f H17	51	3 → 4	10	10	8
	f H18	52	3 → 4	10	10	6
	f H19	53	3 → 4	10	10	4
	f H20	54	3 → 4	10	10	2
	f H21	55	3 → 4	10	10	8
	f H22	56	3 → 4	10	10	6
	f H23	57	3 → 4	10	10	4
	f H24	58	3 → 4	10	10	2

Table 9 . CS2: simulated strategies

 9 Table 10 shows results concerning the utilisation of the wireless medium. The first line of the table shows the relative number of IEEE802.11 frames generated by hybrid flows. Of course, the highest value is encounteredB basic T1 timed W max j = 1 ms ∀j T2 timed W max j = 2 ms ∀j T3 timed W max j = 3 ms ∀j T4 timed W max j = 4 ms ∀j T5 timed W max j = (4.1 -(j × 0.1)) ms

	by the basic strategy. Then, the number of IEEE802.11
	frames decreases when the value of the timer increases.
	Indeed, the average number of hybrid frames encapsu-
	lated in an IEEE802.11 frame increases when the timer in-
	creases. Strategy T 5 has variable values of timers (slightly
	less than 3 ms on average).
			B	T1	T2	T3	T4	T5
		f Hj f W1	4.8 2.8 1.9 1.4 1.2 1.6
	1	% Col	0.5 0.2 0.1 0.1 0.1 0.1
	f W AvgD 148 122 114 111 109 112
	2	% Col	0.9 0.4 0.3 0.3 0.2 0.3
	f W AvgD 172 138 129 124 122 125
	3	% Col	1.4 0.6 0.5 0.5 0.4 0.5
	f W AvgD 204 158 147 141 138 142
	4	% Col	2.2 1.0 0.8 0.8 0.7 0.8
	f W AvgD 250 185 169 162 158 163
	5	% Col		1.6 1.3 1.2 1.1 1.2
	f W AvgD		221 199 189 184 192
	6	% Col		2.5 2.0 1.8 1.6 1.8
	f W AvgD		279 242 227 220 231
	7	% Col				2.7 2.5 2.8
	f W AvgD				287 274 294

Table 10 . CS2: IEEE802.

 10


R Leonarduzzi
email: rleonarduzzi@bioingenieria.edu.ar

H Wendt

S Jaffard
email: jaffard@u-pec.fr

S G Roux

M E Torres

P Abry

EXTENDING MULTIFRACTAL ANALYSIS TO NEGATIVE REGULARITY: P-EXPONENTS AND P-LEADERS

Keywords: scale invariance, multifractal analysis, negative local regularity exponent, wavelet Leaders, estimation performance

Scale invariance is a widely used concept to analyze real-world data from many different applications and multifractal analysis has become the standard corresponding signal processing tool. It characterizes data by describing globally and geometrically the fluctuations of local regularity, usually measured by means of the Hölder exponent. A major limitation of the current procedure is that it applies only to locally bounded functions or signals, i.e., to signals with positive regularity. The present contribution proposes to characterize local regularity with a new quantity, the p-exponent, that permits negative regularity in data, a widely observed property in real-world data. Relations to Hölder exponents are detailed and a corresponding p-leader multifractal formalism is devised and shown at work on synthetic multifractal processes, representative of a class of models often used in applications. We formulate a conjecture regarding the equivalence between Hölder and p-exponents for a subclass of processes. Even when Hölder and p-exponents coincide, the p-leader formalism is shown to achieve better estimation performance.

CONTEXT, GOALS AND CONTRIBUTIONS

Scale invariance and Multifractal Analysis. Multifractal analysis [START_REF] Jaffard | Wavelet techniques in multifractal analysis[END_REF][START_REF] Riedi | Theory and applications of long range dependence[END_REF] has recently matured to a standard signal processing tool that provides a fine characterization of the scaling properties of time series (cf. e.g., [START_REF] Jaffard | Wavelet techniques in multifractal analysis[END_REF][START_REF] Riedi | Theory and applications of long range dependence[END_REF][START_REF] Wendt | Bootstrap for empirical multifractal analysis[END_REF]). In essence, multifractal analysis relies on the notion of local regularity, theoretically grounded in the definition of the Hölder exponent h(t) [START_REF] Jaffard | Wavelet techniques in multifractal analysis[END_REF][START_REF] Riedi | Theory and applications of long range dependence[END_REF]: The closer h(t) is to 0, the more irregular a signal X is at time position t; conversely, the larger h(t), the more regular X at t. Multifractal analysis does, however, not aim at characterizing X via the fluctuations of its local regularity along time, i.e., via the function h(t). Instead, it provides practitioners with a characterization of X via the multifractal spectrum D(h), consisting of a global geometrical description of the fluctuations of h(t). The practical estimation of D(h) is achieved through a procedure referred to as a multifractal formalism. It relies on the use of multiresolution quantities TX (a, t), i.e., of quantities that measure the behavior of X around t at scale a, such as wavelet coefficients. The asymptotic behavior of the time average of the moments of order q of TX (a, t) in the limit of fine scales theoretically defines the scaling function ζ(q) = lima→0 log(1/na k |TX (a, k)| q )/ log a, whose Legendre transform provides an estimate of D(h) in form of an upper bound (cf. Section 2 and [START_REF] Jaffard | Wavelet techniques in multifractal analysis[END_REF][START_REF] Riedi | Theory and applications of long range dependence[END_REF]).

The definition of ζ(q) above in essence amounts to assuming a scaling behavior with respect to the analysis scale a,

1/na k |TX (a, k)| q ≃ cqa ζ(q) , a → 0, (1)
connecting multifractal analysis as an analysis tool and scale invariance as a modeling paradigm. In practice, the asymptotic power law above is assumed to hold over a finite yet large range of scales am ≤ a ≤ aM , with aM /am ≫ 1, thus enabling the estimation of the scaling exponents ζ(q) and further of D(h).

Multifractal analysis has been successfully used as a tool to analyze, describe, model and classify temporal dynamics of signals in numerous real-world applications of very different types, including hydrodynamic turbulence [START_REF] Mandelbrot | Intermittent turbulence in self-similar cascades: divergence of high moments and dimension of the carrier[END_REF], biomedical data and body rhythms [START_REF] Ivanov | Multifractality in human heartbeat dynamics[END_REF][START_REF] Kotani | Multifractal heart rate dynamics in human cardiovascular model[END_REF], geophysical data [START_REF] Schertzer | Physically based rain and cloud modeling by anisotropic, multiplicative turbulent cascades[END_REF][START_REF] Ba Toledo | Wavelet-based multifractal analysis of nonlinear time series: The earthquake-driven tsunami of 27 february 2010 in chile[END_REF], fMRI [START_REF] Shimizu | Wavelet-based multifractal analysis of fMRI time series[END_REF][START_REF] Ciuciu | Scale-free and multifractal dynamic properties of fMRI signals during rest and task[END_REF], finance [START_REF] Calvet | Multifractal volatility: Theory, forecasting and pricing[END_REF] and image textures [START_REF] Wendt | Wavelet leaders and bootstrap for multifractal analysis of images[END_REF]. For reviews and examples, see e.g., [START_REF] Abry | Multiscale network traffic analysis, modeling, and inference using wavelets, multifractals, and cascades[END_REF][START_REF] Lopes | Fractal and multifractal analysis: A review[END_REF].

Related works: recent developments and open issues.

Multifractal analysis has received significant research efforts at both the theoretical and application levels. Most of the recent developments aiming at improving multifractal analysis, either in theoretical foundations or in applied schemes, focus on exploring the benefits of varying the multiresolution quantities TX (a, t) serving as the basic analysis unit. Increments, oscillations, wavelet coefficients, continuous wavelet transform modulus maxima [START_REF] Arneodo | A wavelet-based method for multifractal image analysis. I. Methodology and test applications on isotropic and anisotropic random rough surfaces[END_REF][START_REF] Muzy | The multifractal formalism revisited with wavelets[END_REF] and more recently wavelet leaders [START_REF] Wendt | Bootstrap for empirical multifractal analysis[END_REF] were used in the vast majority of cases. These developments were mainly concerned with parameter estimation performance and robustness (cf. [START_REF] Wendt | Bootstrap for empirical multifractal analysis[END_REF][START_REF] Soares | Towards the detection of microcalcifications on mammograms through multifractal detrended fluctuation analysis[END_REF] and references therein), or, more recently, with analysis refinement (e.g., detection of oscillating singular behaviors in data [START_REF] Abry | Detecting oscillating singularities in multifractal analysis : Application to hydrodynamic turbulence[END_REF].) Along another line, procedures avoiding the Legendre transform based formalism (which yields the convex hull of D(h) only) have been investigated. Notably, large deviation principle based approaches were studied, aiming at the estimation of non convex multifractal spectra (cf. e.g., [START_REF] Riedi | Theory and applications of long range dependence[END_REF][START_REF] Barral | On the estimation of the large deviations spectrum[END_REF]).

However, none of these developments reflected two fundamental facts. First, by definition, the Hölder exponent is positive, h(t) ≥ 0. Consequently, its use as a measure of local regularity induces a major a limitation for the application of multifractal analysis to real-world data: It permits the analysis of the fluctuations of local regularity for locally bounded functions only. Second, the choice of a particular multiresolution quantity TX (a, t) is tied to the way local regularity is measured and can therefore imply a change in the definition of the exponent used to measure local regularity. Often, in applications, real-world data are well modeled by stochastic processes whose sample paths do not constitute locally bounded functions, this is the case e.g., for fractional Gaussian noise or multifractal random walks [START_REF] Bacry | Multifractal random walk[END_REF], frequently used to model Heart Rate Variability [START_REF] Kotani | Multifractal heart rate dynamics in human cardiovascular model[END_REF], fMRI fluctuations [START_REF] Shimizu | Wavelet-based multifractal analysis of fMRI time series[END_REF][START_REF] Ciuciu | Scale-free and multifractal dynamic properties of fMRI signals during rest and task[END_REF] or Mandelbrot's multiplicative cascades, used to model, e.g., dissipation in hydrodynamic turbulence [START_REF] Mandelbrot | Intermittent turbulence in self-similar cascades: divergence of high moments and dimension of the carrier[END_REF], rainfalls [START_REF] Schertzer | Physically based rain and cloud modeling by anisotropic, multiplicative turbulent cascades[END_REF], cloud textures [START_REF] Arneodo | A wavelet-based method for multifractal image analysis. I. Methodology and test applications on isotropic and anisotropic random rough surfaces[END_REF], to list but a few examples. In these situations, the Hölder exponent is of limited practical use, and so are the associated multiresolution quantities.

Recently, an alternative measure of regularity, the p-exponent hp(t), has been introduced theoretically in the context of multifractal analysis [START_REF] Jaffard | Wavelet analysis of fractal boundaries[END_REF]. One of its potential advantages is that it enables to weaken the positive regularity and boundedness requirement and admits a certain range of negative exponents. It has, to the best of our knowledge, not been used in applications and remains poorly studied in terms of practical applicability and estimation performance. Goals, contributions and outline.

In this context, the goals of the present contribution are three-fold: First, it aims at defining the p-exponent, reviewing the key differences with the Hölder exponent, and devising the corresponding multiresolution quantities and multifractal formalism (cf. Section 2). Second, the principles and limitations of the p-exponent based multifractal formalism are illustrated on sample paths of a stochastic process chosen as a representative model for scale invariance in applications (cf. Section 3). Third, equality between Hölder and p-exponents is conjectured for a class of model processes. In the case of coinciding exponents, it is shown numerically that the p-leader formalism achieves better estimation performance than the wavelet leader formalism, now considered as a benchmark for practical multifractal analysis (cf. Section 4).

LOCAL REGULARITY, MULTIFRACTAL ANALYSIS

Hölder regularity

Wavelet coefficients.

Let {X(t)} t∈R denote the signal to be analyzed. Let ψ denote the mother wavelet, characterized by its uniform regularity index and number of vanishing moments N ψ , a strictly positive integer defined as:

ψ ∈ C N ψ -1 and ∀n = 0, . . . , N ψ -1, R t k ψ(t)dt ≡ 0 and R t N ψ ψ(t)dt = 0. Let {ψ j,k (t) = 2 -j/2 ψ(2 -j t -k)} (j,k)∈N 2 denote
the collection of dilated and translated templates of ψ that form an orthonormal basis of L 2 (R). The (L 1 -normalized) discrete wavelet transform coefficients dX (j, k) of X are defined as dX (j, k) = 2 -j/2 ψ j,k |X . For a detailed introduction to wavelet transforms, readers are referred to, e.g., [START_REF] Mallat | A Wavelet Tour of Signal Processing[END_REF] . Early formulations of multifractal analysis were based on the structure functions of wavelet coefficients, of order q ≥ 0,

η(q) = 1/nj k |dX (j, k)| q , (2)
but have been shown to suffer from poor practical performance (cf. e.g., [START_REF] Muzy | The multifractal formalism revisited with wavelets[END_REF][START_REF] Jaffard | Multifractal formalism for functions part ii: Selfsimilar functions[END_REF][START_REF] Jaffard | Wavelet techniques in multifractal analysis[END_REF][START_REF] Wendt | Bootstrap for empirical multifractal analysis[END_REF]), this is thus not further discussed here. Hölder exponent. Assume that {X(t)} t∈R consists of a locally bounded function (or sample path of a stochastic process), i.e., belongs to L ∞ (R). Then X is said to belong to Cα(t) at time position t ∈ R, with α ≥ 0, if there exist a constant C > 0 and a polynomial Pt satisfying Deg(Pt) < α such that, in a neighborhood of t:

|X(t + a) -Pt(t + a)| ≤ C|a| α , |a| → 0. (3)
The Hölder exponent of X at t is defined as:

h(t) = sup{α : X ∈ C α (t)} ≥ 0. (4)
It characterizes the local regularity of X at t in the sense that the larger (smaller) h(t), the smoother (rougher) X around t. The simplest example of a singularity at datum t0 whose Hölder exponent is h (when h is not a even integer) is supplied by the cusp-type function X(t) = X(t0) + B|t -t0| h . Multifractal spectrum and wavelet leaders. Though deeply rooted in the notions of local regularity and Hölder exponents, multifractal analysis does not aim at characterizing X through regularity as a function of time h(t). Instead, it provides practitioners with a global and geometrical description of the fluctuations along time of the Hölder exponent h, in terms of the multifractal spectrum D(h). Technically, D(h) is given by the Hausdorff dimensions of the sets of points where the Hölder exponent takes the value h (for details, the interested reader is referred to [START_REF] Jaffard | Multifractal formalism for functions part ii: Selfsimilar functions[END_REF][START_REF] Riedi | Theory and applications of long range dependence[END_REF][START_REF] Jaffard | Wavelet techniques in multifractal analysis[END_REF].)

The practical measurement of D(h) relies on a procedure referred to as the multifractal formalism: It requires the definition of multiresolution quantities, the wavelet leaders LX (j, k), defined as the local supremum of wavelet coefficients taken within a neighborhood over all finer scales [START_REF] Jaffard | Wavelet techniques in multifractal analysis[END_REF][START_REF] Wendt | Bootstrap for empirical multifractal analysis[END_REF]:

LX (j, k) = sup λ ′ ⊂3λ j,k |dX (λ ′ )|, where (5)
λ j,k = [k2 j , (k + 1)2 j ) and 3λ j,k = m{-1,0,1} λ j,k+m .

The LX (j, k) match the Hölder exponent in the sense that for t = 2 j k, LX (j, k) ∼ C2 jh(t) as 2 j → 0. This implies that 1 n j n j k=1 LX (j, k) q ∼ cq2 jζ(q) as 2 j → 0 as in [START_REF] Jaffard | Wavelet techniques in multifractal analysis[END_REF] and that the Legendre transform of ζ(q) yields an (upper-bound) estimate of the multifractal spectrum, L(h

) = minq (1 + qh -ζ(q)) ≥ D(h).
Limitation. The key limitation in the practical use of the Hölder based multifractal formalism resides in its applicability to locally bounded functions only. This requirement implies the equivalent condition that the minimum regularity hm = inft h(t) of the data is non-negative, which can be practically checked prior to application of the multifractal formalism by using the wavelet coefficient based estimate hm = lim

2 j →0 log 2 sup k |dX (j, k)|/ log 2 2 j . (6)
2.2. p-exponent regularity p-exponents. We extend local regularity measures to negative values by replacing the bounded function requirement by the condition that X(t) locally belongs to L p (R) for p ≥ 1: X is said to belong to T p α (t) with α > -1/p at time t if there exist C, R > 0 and a polynomial Pt (of degree N less than or equal to α) such that ∀a ≤ R

T (p) X (a, t) = 1 a t+a/2 t-a/2 |X(u) -Pt,N (u -t)| p du 1/p ≤ Ca α . (7)
The p-exponent hp(t) of X at t is defined as [START_REF] Jaffard | Wavelet analysis of fractal boundaries[END_REF]:

hp(t) = sup{α : X ∈ T p α (t)} (8)
and constitutes a natural substitute for the Hölder exponent when dealing with functions which are not bounded but locally belong to L p and admits negative local regularity exponents hp > -1/p. Obviously, the Hölder exponent coincides with the p-exponent for p = +∞: h(t) ≡ h∞(t); furthermore, h p ′ ≤ hp if p ′ ≥ p [START_REF] Jaffard | Wavelet analysis of fractal boundaries[END_REF][START_REF] Leonarduzzi | p-exponent and p-leaders for multifractal analysis[END_REF]. p-multifractal spectrum and p-leaders.

Mimicking the definition of D(h), mutatis mutandis, the p-multifractal spectrum D (p) (hp) is defined as the Hausdorff dimensions of the sets of points where the p-exponent takes the value hp.

The practical measurement of D (p) (h) requires the definition of new multiresolution quantities, the p-leaders [START_REF] Jaffard | Wavelet techniques for pointwise regularity[END_REF][START_REF] Jaffard | Function spaces vs. scaling functions: tools for image classification[END_REF][START_REF] Jaffard | Wavelet analysis of fractal boundaries[END_REF]:

L (p) (j, k) = 2 j λ ′ ⊂3λ j |d λ ′ | p 2 -j ′ 1/p , (9)
that match p-exponent local regularity in the sense that

for t = 2 j k, L (p) (j, k) ∼ C2 jhp(t) , 2 j → 0. (10)
The p-scaling function is defined similarly as in (1):

S(p, q, j) = 1/nj n j k=1 L (p) (j, k) q ∼ C (p)
q 2 jζp(q) , 2 j → 0; [START_REF] Calvet | Multifractal volatility: Theory, forecasting and pricing[END_REF] and the Legendre transform of ζp(q) yields an (upper-bound) estimate of D (p) (hp),

L (p) (hp) = min q (1 + qhp -ζp(q)) ≥ D (p) (hp). (12)
The demonstration of that results follows from the proof given in [START_REF] Jaffard | The contribution of wavelets in multifractal analysis[END_REF], which is generic for any well-behaved multiresolution quantity. In practice, X ∈ L p (R) must be verified prior to application of the p-leader multifractal formalism, by checking that η(p) ≥ 0 [START_REF] Jaffard | Wavelet analysis of fractal boundaries[END_REF][START_REF] Jaffard | Wavelet techniques for pointwise regularity[END_REF][START_REF] Jaffard | Function spaces vs. scaling functions: tools for image classification[END_REF], or equivalently that its Legendre transform L(h) satisfies

L(h) ≤ 1 + ph. (13)
Cumulants and estimation.

Following the original intuition in [START_REF] Castaing | Log-similarity for turbulent flows[END_REF], a polynomial expansion ζp(q) = m≥1 c

(p) m q m /m! enables a simplified analysis of ζp(q) through the expansion coefficients {c Reproducing the calculations in [START_REF] Castaing | Log-similarity for turbulent flows[END_REF] for pleaders immediately yields that these coefficients are directly related to the dependence with respect to scales 2 j of the cumulants of order m, denoted by C (p) m (j), of the logarithm of the p-leaders:

C (p) m (j) = Cumm ln L (p) (j, k) = c (0,p) m + c (p) m ln 2 j . ( 14
)
This scaling behavior is used for the practical estimation of the coefficients c m (j) against ln 2 j , for j ∈ [j1, j2]. In view of [START_REF] Calvet | Multifractal volatility: Theory, forecasting and pricing[END_REF], the ζp(q) are also estimated by linear regressions of log 2 S(p, q, j) versus log 2 2 j = j. These estimation procedures, implemented by ourselves, are used to obtain the results produced in Sections 3 and 4. Hölder versus p-exponents. In general, p-exponents do not coincide for different ps nor with Hölder exponent (see [START_REF] Leonarduzzi | p-exponent and p-leaders for multifractal analysis[END_REF] for a theoretical discussion); thus the associated spectrum yields a novel and versatile collection of characterizations of local regularity fluctuations, further illustrated and studied in Sections 3 and 4.

NEGATIVE REGULARITY

Multifractal random walk. The differences and potential benefits in using p-exponents and p-leaders for the characterization of local regularity fluctuations are now illustrated on pedagogical examples, containing negative p-exponents. They are based on fractionally differentiated realizations of multifractal random walk (MRW) [START_REF] Bacry | Multifractal random walk[END_REF][START_REF] Bacry | Multifractal stationary random measures and multifractal random walks with log-infinitely divisible scaling laws[END_REF], a popular and representative member of the class of multiplicative cascade based multifractal processes. This class constitutes one of the most prominently used class of multifractal models for applications. MRW is a non Gaussian process with stationary increments and its multifractal properties mimic those of the celebrated multiplicative log-normal cascades of Mandelbrot. It is defined as k) , where GH (k) are the increments of fractional Brownian motion with parameter H, and ω is a Gaussian random process, independent of GH and with non trivial autocovariance Cov[ω(k1), ω(k2)] = c2 ln

X(k) = n k=1 GH (k)e ω(
L |k 1 -k 2 |+1
when |k1 -k2| < L and 0 otherwise. MRW has scaling properties as in [START_REF] Jaffard | Wavelet techniques in multifractal analysis[END_REF] for q ∈ -2/c2, 2/c2 , with ζ(q) = (H + c2)q -c2q 2 /2 and its multifractal spectrum is given by D

(∞) (h) = 1+(h-c1) 2 /(2c2) (with c1 = H + c2 and hm = c1 - √ -2c2
). Hölder versus p-exponents. Regarding p-exponent analysis, we form the following conjecture, strongly backed up by the numerical simulations reported below, that will be proven in [START_REF] Leonarduzzi | p-exponent and p-leaders for multifractal analysis[END_REF]: Conjecture 1 The p-exponents of multiplicative cascade based multifractal processes X ∈ L p 0 coincide for all p ∈ [1, p0], hence

D (p) (h) = D (p 0 ) (h) for all p ∈ [1, p0].
Notably, this conjecture implies that when hm ≥ 0, the Hölder and the p-exponents coincide ∀p ≥ 1 and thus that the Hölder and the p-exponent based multifractal spectra coincide for MRW, and ∀p ≥ 1 :

D (p) (h) = D (∞) (h) = D(h).

Numerical experiments.

We fix c1 = 0.8 and c2 = -0.08 and use fractional differentiation of order γ to control the minimal regularity and function class embedding of the sample paths,

X (γ) = F -1 (ıω) γ F[X]
, where F stands for the discrete Fourier transform [START_REF] Tseng | Computation of fractional derivatives using Fourier transform and digital FIR differentiator[END_REF]. We set γ = {0, 0.4, 0.5, 0.6, 0.7}, yielding h

(γ) m = hm -γ = {0.4, 0, -0.1, -0.2, -0.3}, c (γ) 1 = c1 -γ, c (γ)
m = cm for m ≥ 2 and p0 = {+∞, +∞, 10, 5, 2.5}, where p0 denotes the value for p such that X (γ) ∈ L p 0 and ∀ε > 0 : X (γ) / ∈ L p 0 +ε . We fix N = 2 19 . Examples of sample paths are plotted in Fig. 1 (left column) and illustrate the potential of processes with negative p-exponents as models for applications, offering a continuum of moderately to strongly irregular sample paths. The corresponding multifractal spectra and estimates (as detailed in Section 2) for p = {2, 4, 8, ∞} (mean over 50 realizations) are plotted in Fig. 1 (right column), together with the theoretical limits D (p) (hp) ≤ 1 + php for the multifractal p-spectra of L p functions. Quality of estimation. First, we observe that in consistency with Conjecture 1, the results obtained with the wavelet leader and pleader formalisms coincide one with another for any of the values of p considered as long as h (γ) m ≥ 0 (p0 = +∞), and the formalisms, for any p, provide excellent estimates of the multifractal spectrum D(h) (Fig. 1, row 1-2). Second, as soon as h (γ) m < 0 (p0 < ∞), the wavelet leader based formalism fails to correctly estimate the spectrum D (p 0 ) (h) since the theoretical (bounded function) prerequisite for its application is violated, while the p-leaders estimates L (p) (h) correctly recover the multifractal spectrum D (p 0 ) (h) for values of p such that p ≤ p0 (Fig. 1, row 3-5). Once this condition for the function to be in L p is violated, the p-leader formalism provides biased estimates L (p) (h) which are bound to be at best tangent to 1 + ph (Fig. 1, row 3-5). For example, in row 4, h (γ) m = -0.2 and estimations L (p) are found to correctly estimate the theoretical spectrum D only for p = 2, 4 < p0 = 5, estimates for p = {8, ∞} ≥ p0 are found to differ significantly from the expected spectrum. In row 5, h (γ) m = -0.4 and L (p) estimates are correct for p = 2 < p0 = 2.5 only, while L (p) obtained with p = {4, 8, ∞} > p0 are clearly biased and constrained by the 1 + ph limits. These results are consistent with the theory outlined in Section 2 and demonstrate the practical effectiveness of the p-leader multifractal formalism in measuring negative values in local regularity.

ESTIMATION PERFORMANCE

The performance of the wavelet leader and p-leader multifractal formalisms for estimating the log-cumulants cm, m = 1, . . . , 4 are compared for 500 realizations from Monte Carlo simulations performed on MRW with process parameters as in Section 3 and γ = 0, hence with hm > 0 and Hölder and p-exponents and the corresponding spectra coinciding ∀p ≥ 1. A Daubechies' wavelet with N ψ = 2 is used, linear regressions are performed over the range (j1, j2) = [START_REF] Wendt | Bootstrap for empirical multifractal analysis[END_REF][START_REF] Abry | Detecting oscillating singularities in multifractal analysis : Application to hydrodynamic turbulence[END_REF]. In Fig. 2 It is observed that, for cm, m ≥ 2, variances systematically decrease when p decreases and also that biases decrease or remain constant when p decreases, thus rmse is systematically decreased when p decreases towards 1. For c1, variances appear to decrease only slightly with p while biases tend to re-increase when p → 1, thus yielding a minimum with an optimal trade-off p around 2. In overall, it is thus observed that, systematically, when p is decreased, the p-leader based estimation outperforms the wavelet leader based one, currently considered to achieve benchmark performance. Also, it provides practitioners with the possibility of tuning the parameter p to data and applications.

CONCLUSIONS

The present contribution has shown that p-exponent and p-leader based multifractal analysis extends the classical Hölder and leader based formulation in two ways: Local regularity analysis is extended to possibly negative values, commonly observed in real world data. For processes where Hölder and p-exponents coincide, estimation performance for multifractal attributes are significantly improved compared to the reference wavelet leader formalism when tuning p to small values, close to 1. Connections between Multifractal Detrended Fluctuation Analysis, another popular tool for multifractal analysis [START_REF] Soares | Towards the detection of microcalcifications on mammograms through multifractal detrended fluctuation analysis[END_REF] and p-leader multifractal analysis can be established and yield theoretical insights in the former tool. Also, while written explicitly for 1D signals, p-leader multifractal analysis can be extended to R d random fields, notably for image texture analysis. These developments are under current investigations, cf. [START_REF] Leonarduzzi | p-exponent and p-leaders for multifractal analysis[END_REF].

m

  by linear regressions of the estimates of C (p)

Fig. 1 .

 1 Fig. 1. Left column: A single realization of fractionally differentiated MRW with h (γ) m = {0.4, 0, -0.1, -0.2, -0.3} (from top to bottom, respectively). Right column: The theoretical multifractal spectra (black solid) and Legendre spectra (mean over 50 realizations, N = 2 19 , N ψ = 2, j1 = 10) corresponding with the functions in the left column for p = {2, 4, 8, ∞} (solid lines; red circle, green diamond, blue cross and magenta square); the dashed line segments indicate the theoretical bound 1 + hp for the spectrum of any L p function (in respective colors for the different p).

  , estimation performance are summarized as a function of p in terms of bias b( θ) = Ê[ θ] -θ (blue dashed lines with circles), standard deviations s( θ) = Ê[ θ2 ] -Ê[ θ] 2 (red dashed lines with crosses) and root mean squared errors (rmse) r( θ) = b( θ) 2 + s( θ) 2 (black solid lines with squares).

4 Fig. 2 .

 42 Fig. 2. Bias (blue dashed circle), standard deviation (red dashed cross) and root mean squared errors (black solid square) for the estimation of the expansion coefficients c (p) m as functions of p.

Work supported by ANR BLANC 2011 AMATIS BS0101102 and CNRS-CONICET grant 2010 112432