Ruggero Lanotte

Massimo Merro

A Semantic Theory of the Internet of Things (extended abstract)

We propose a process calculus for modelling and reasoning on systems in the Internet of Things paradigm. Our systems interact both with the physical environment, via sensors and actuators, and with smart devices, via short-range and Internet channels. The calculus is equipped with a standard notion of labelled bisimilarity which represents a fully abstract characterisation of a well-known contextual equivalence. We use our semantic proof-methods to prove run-time properties of a non-trivial case study as well as system equalities.

Introduction

In the Internet of Things (IoT) paradigm, smart devices, such as smartphones, automatically collect information from shared resources (e.g. Internet access or physical devices) and aggregate them to provide new services to end users [START_REF] Gubbi | Internet of things (IoT): A vision, architectural elements, and future directions[END_REF].

The "things" commonly deployed in IoT systems are: RFID tags, for unique identification, sensors, to detect physical changes in the environment, and actuators, to pass information to the environment.

The research on IoT is currently focusing on practical applications such as the development of enabling technologies, ad hoc architectures, semantic web technologies, and cloud computing [START_REF] Gubbi | Internet of things (IoT): A vision, architectural elements, and future directions[END_REF]. However, as pointed out by Lanese et al. [START_REF] Lanese | Internet of things: a process calculus approach[END_REF], there is a lack of research in formal methodologies to model the interactions among system components, and to verify the correctness of the network deployment before its implementation.

The main goal of this paper is to propose a process calculus with a clearlydefined semantic theory, for specifying and reasoning on IoT applications. Designing a calculus for modelling a new paradigm requires understanding and distilling, in a clean algebraic setting, the main features of the paradigm. Let us try to figure out what the main ingredients of IoT are, by means of an example.

Suppose a simple smart home (see Fig. 1) in which the user can use her smartphone to remotely control the heating boiler of her house, and automatically turn on lights when entering a room. The house consists of an entrance and a lounge, separated by a patio. Entrance and lounge have their own lights (actuators) which are governed by different light manager processes, LightM ng. The boiler is in the patio and is governed by a boiler manager process, BoilerM ng. This process senses the local temperature (via a sensor) and decides whether to turn on/off the boiler, setting a proper actuator to signal the state of the boiler. The smartphone executes two concurrent processes: BoilerCtrl and LightCtr. The first one reads user's commands, submitted via the phone touchscreen (a sensor), and forward them to the process BoilerM ng, via an Internet channel. Whereas, the process LightCtrl interacts with the processes LightM ng, via short-range wireless channels (e.g. Bluetooth), to automatically turn on lights when the smartphone physically enters either the entrance or the lounge.

The whole system is given by the parallel composition of the smartphone (a mobile device) and the smart home (a stationary entity).

On this kind of systems one may wish to prove interesting run-time properties. Think of a fairness property saying that the boiler will be eventually turned on/off whenever specific conditions are satisfied. Or consistency properties, saying the smartphone will never be in two rooms at the same time. Even more, one may be interested in understanding whether our system has the same observable behaviour of another system. Let us consider a variant of our smart home, where lights functionality depends on GPS coordinates of the smartphone (localisation is a common feature of today smartphones). Intuitively, the smartphone sends its GPS position to a centralised light manager, CLightM ng (possibly placed in the patio), via an Internet channel. The process CLightM ng will then interact with the two processes LightM ng, via short-range channels, to switch on/off lights, depending on the position of the smartphone. Here comes an interesting question: Can these two implementations of the smart home, based on different light management mechanisms, be actually distinguished by an end user?

In the paper at hand we develop a fully abstract semantic theory for a process calculus of IoT systems, called CaIT. We provide a formal notion of when two systems in CaIT are indistinguishable, in all possible contexts, from the point of view of the end user. Formally, we adopt the approach of [START_REF] Honda | On reduction-based process semantics[END_REF][START_REF] Sangiorgi | The Pi-Calculus a theory of mobile processes[END_REF], often called reduction (closed) barbed congruence, which relies on two crucial concepts: a reduction semantics to describe system computations, and the basic observables to represent what the environment can directly observe of a system. In CaIT, there are at least two possible observables: the ability to transmit along channels, logical observation, and the capability to diffuse messages via actuators, physical observation. We have adopted the second form as our contextual equality remains invariant when adding logical observation. However, the right definition of physical observation is far from obvious as it involves some technical challenges in the definition of the reduction semantics (see the discussion in Sec. 2.3).

Our calculus is equipped with two labelled transition semantics (LTS) in the SOS style of Plotkin: an intensional semantics and an extensional semantics. The adjective intensional is used to stress the fact that the actions here correspond to activities which can be performed by a system in isolation, without any interaction with the external environment. While, the extensional semantics focuses on those activities which require a contribution of the environment. We prove that the reduction semantics coincides with the intensional semantics (Harmony Theorem), and that they satisfy some desirable time properties such as time determinism, patience, maximal progress and well-timedness [START_REF] Hennessy | A process algebra for timed systems[END_REF].

However, the main result of the paper is that weak bisimilarity in the extensional LTS is sound and complete with respect to our contextual equivalence, reduction barbed congruence. This required a non-standard proof of the congruence theorem (Thm. 2). Finally, in order to show the effectiveness of our bisimulation proof method, we prove a number of non-trivial system equalities.

In this extended abstract proofs are omitted; full details can be found in [START_REF] Castiglioni | A Semantic Theory of the Internet of Things[END_REF].

Outline Sec. 2 contains the calculus together with the reduction semantics, the contextual equivalence, and a discussion on design choices. Sec. 3 gives the details of our smart home example, and proves desirable run-time properties for it. Sec. 4 defines both the intensional and the extensional LTS. In Sec. 5 we define bisimilarity for IoT-systems, and prove the full abstraction result together with a number of non-trivial system equalities. Sec. 6 discusses related work.

The calculus

The syntax of our Calculus of the Internet of Things, shortly CaIT, is given in a two-level structure: a lower one for processes and an upper one for networks of smart devices.

M, N

::= 0 n[I P ] µ l M | N (νc)M P, Q ::= nil ρ.P P | Q π.P Q [b]P ; Q X fix X.P
We use letters n, m to denote nodes/devices, c, g for channels, l, h, k for (physical) locations, s, s for sensors, a, a for actuators and x, y, z for variables. Our values, ranged over by v and w, are constituted by basic values, such as booleans and integers, sensor and actuator values, and coordinates of physical locations.

A network M is a pool of distinct nodes running in parallel and living in physical locations. We assume a discrete notion of distance between two locations h and k, i.e. d(h, k) ∈ N. We write 0 to denote the empty network, while M | N represents the parallel composition of two networks M and N . In (νc)M channel c is private to the nodes of M . Each node is a term of the form n[I P ] µ l , where n is the device ID; I is the physical interface of n, represented as a partial mapping from sensor and actuator names to physical values; P is the process modelling the logics of n; l is the physical location of the device; µ ∈ {s, m} is a tag to distinguish between stationary and mobile nodes.

For security reasons, sensors in I can be read only by its controller process P . Similarly, actuators in I can be modified only by P . No other devices can access the physical interface of n. P is a timed concurrent processes which manages both the interaction with the physical interface I and channel communication. The communication paradigm is point-to-point via channels that may have different transmission ranges. We assume a global function rng() from channel names to N ∪ {-1, ∞}. A channel c can be used for: i) intra-node communications, if rng(c) = -1; ii) short-range inter-node communications (such as Bluetooth, infrared, etc

) if 0 ≤ rng(c) < ∞; iii) Internet communications, if rng(c) = ∞.
Technically, our processes build on CCS with discrete time [START_REF] Hennessy | A process algebra for timed systems[END_REF]. We write ρ.P , with ρ ∈ {σ, @(x), s?(x), a!v}, to denote intra-node actions. The process σ.P sleeps for one time unit. The process @(x).P gets the current location of the enclosing node. Process s?(x).P reads a value v from sensor s. Process a!v.P writes the value v on the actuator a. We write π.P Q, with π ∈ {c v , c(x)}, to denote channel communication with timeout. This process can communicate in the current time interval and then continues as P ; otherwise, after one time unit, it evolves into Q. We write [b]P ; Q for conditional (here guard b is always decidable). In processes of the form σ.Q and π.P Q the occurrence of Q is said to be time-guarded. The process fix X.P denotes time-guarded recursion, as all occurrences of the process variable X may only occur time-guarded in P . In processes c(x).P Q, s?(x).P and @(x).P the variable x is said to be bound. Similarly, in process fix X.P the process variable X is bound. In the term (νc)M the channel c is bound. This gives rise to the standard notions of free/bound (process) variables, free/bound channels, and α-conversion. A term is said to be closed if it does not contain free (process) variables, although it may contain free channels. We always work with closed networks: the absence of free variables is preserved at run-time. We write T { v / x } for the substitution of the variable x with the value v in any expression T of our language. Similarly, T { P / X } is the substitution of the process variable X with the process P in T .

Actuator names are metavariables for actuators like display@n or alarm@n. As node names are unique so are actuator names: different nodes have different actuators. The sensors embedded in a node can be of two kinds: location-dependent and node-dependent. The first ones sense data at the current location of the node, whereas the second ones sense data within the node, independently on the node's location. Thus, node-dependent sensor names are metavariables for sensors like touchscreen@n or button@n; whereas a sensor temp@h, for temperature, is a typical example of location-dependent sensor. Node-dependent sensor names are unique. This is not the case of location-dependent sensor names which may appear in different nodes. For simplicity, we use the same metavariables for both kind of sensors. When necessary we will specify the type of sensor in use.

We rule out ill-formed networks by means of the following definition. Last condition says that location-dependent sensors may be used only in stationary nodes (see discussion in Sec. 2.3). Hereafter, we will always work with well-formed networks. It is easy to show that well-formedness is preserved at runtime.

We adopt the following notational conventions. i∈I M i denotes the parallel composition of all M i , for i∈I. i∈I M i = 0 and i∈I P i = nil, for I = ∅. We write i M i when I is not relevant. We write π.P instead of fix X. π.P X. We use (νc)M as an abbreviation for (νc 1 ) . . . (νc k )M , with c = c 1 , . . . , c k .

Table 1 Reduction semantics (pos)

-

n[I @(x).P ] µ h τ n[I P { h /x}] µ h (sensread) I(s) = v n[I s?(x).P ] µ h τ n[I P { v /x}] µ h (actunchg) I(a) = v n[I a!v.P ] µ h τ n[I P ] µ h (actchg) I(a) = v I := I[a → v] n[I a!v.P ] µ h a n[I P ] µ h (loccom) rng(c) = -1 n[I c v .P R | c(x).Q S] µ h τ n[I P | Q{ v /x}] µ h (timestat) n[I Q i πi.Pi Qi | Q j σ.Rj] s h τ n[I Q i πi.Pi Qi | Q j σ.Rj] s h σ n[I Q i Qi | Q j Rj] s h (timemob) n[I Q i πi.Pi Qi | Q j σ.Rj] m h τ d(h, k) ≤ δ n[I Q i πi.Pi Qi | Q j σ.Rj] m h σ n[I Q i Qi | Q j Rj] m k (glbcom) d(h, k) ≤ rng(c) n[I c v .P R] µ 1 h | m[I c(x).Q S] µ 2 k τ n[I P ] µ 1 h | m[I Q{ v /x}] µ 2 k (parp) Q i ni[Ii Pi] µ i h i ω Q i ni[I i P i ] µ i h i ω∈{τ, a} Q i ni[Ii Pi | Qi] µ i h i ω Q i ni[I i P i | Qi] µ i h i (parn) M ω M ω∈{τ, a} M | N ω M | N (timepar) M σ M N σ N M | N τ M | N σ M | N (timezero) - 0 σ 0 (res) M ω N ω ∈ {τ, a, σ} (νc)M ω (νc)N (struct) M ≡ N N ω N ω ∈ {τ, a, σ} N ≡ M M ω M

Reduction semantics

The dynamics of the calculus is specified in terms of reduction relations over networks (see Tab. 1). As usual in process calculi, a reduction semantics [START_REF] Milner | The polyadic π-calculus: a tutorial[END_REF] relies on an auxiliary standard relation, ≡, called structural congruence, which brings the participants of a potential interaction into contiguous positions. For lack of space, we omit the formal definition of ≡, as it is quite standard.

As CaIT is a timed calculus, with a discrete notion of time, it will be necessary to distinguish between instantaneous reductions, M i N , and timed reductions, M σ N . Relation i denotes activities which take place within one time interval, whereas σ represents the passage of one time unit. Instantaneous reductions are of two kinds: those which involve the change of the values associated to some actuator a, written a , and the others, written τ . Intuitively, reductions of the form M a N denote watchpoints which cannot be ignored by the physical environment (in Ex. 2, and more extensively at the end of Sec. 2.3, we explain why this is important). Thus, we define the instantaneous reduction relation i = τ ∪ a , for any actuator a. We also define the reduction = τ ∪ σ . The first seven rules in Tab. 1 model intra-node activities. Rule (pos) serves to compute the current position of a node. Rule (sensread) represents the reading of the current data detected at some sensor s. Rules (actunchg) and (actchg) implement the writing of some data v on an actuator a, distinguishing whether the value of the actuator changes or not. Rule (loccom) models intra-node communications on a local channel c (rng(c) = -1). Rule (timestat) models the passage of time within a stationary node. Notice that all untimed intra-node actions are considered urgent actions as they must occur before the next timed action. Rule (timemob) models the passage of time for mobile nodes. This rule also serves to model node mobility. Mobile nodes can nondeterministically move from one physical location h to a (possibly different) location k, at the end of a time interval. Node mobility respects the following time discipline: in one time unit a node can move from h to k provided that d(h, k) ≤ δ, for some fixed δ ∈ N (if h = k then d(h, k) = 0). For the sake of simplicity, we fix the same constant δ for all nodes of our systems. Rule (glbcom) models inter-node communication along a global channel c (rng(c) ≥ 0). Intuitively, two nodes can communicate via a channel c only if they are within the transmission range of c. Rules (parp) and (parn) serve to propagate instantaneous reductions through parallel processes, and parallel networks, respectively. Rule (timepar) is for inter-node time synchronisation. The remaining rules are standard.

We write k i to denote k consecutive reductions i ; * i is the reflexive and transitive closure of i . We use the same notation for the reduction relation .

Below we report a few standard time properties which hold in our calculus: time determinism, maximal progress, patience and well-timedness.

Proposition 1 (Time properties).

-

If M σ M and M σ M , then M ≡ i∈I n i [I i P i ] µi hi and M ≡ i∈I n i [I i P i ] µi ki , with d(h i , k i ) ≤ 2δ, for all i ∈ I. -If M i M , then there is no M such that M σ M . -If M i M for no M , then there is N such that M σ N . -For any M there is a z ∈ N such that if M u i N then u ≤ z.
In its standard formulation, time determinism says that a system reaches at most one new state by executing a reduction step σ . However, by an application of Rule (timemob), our mobile nodes may change location when executing a reduction σ . Well-timedness ensures the absence of infinite instantaneous traces which would prevent the passage of time.

Behavioural equivalence

Our contextual equivalence is reduction barbed congruence [START_REF] Honda | On reduction-based process semantics[END_REF][START_REF] Sangiorgi | The Pi-Calculus a theory of mobile processes[END_REF], a standard contextually defined process equivalence that crucially relies on the definition of basic observables to represent what the environment can directly observe of a system3 . As already said in the Introduction, we choose to observe the capability to publish messages via actuators (physical observation).

Definition 2 (Barbs). We write

M ↓ a@h!v if M ≡ (ν g) n[I P ] µ h | M , with I(a) = v. We write M ⇓ a@h!v if M * M ↓ a@h!v .
The reader may wonder why our barb reports the location and not the node of the actuator. We also recall that actuator names are unique, so they somehow codify the name of their node. The location is then necessary because the environment is potentially aware of its position when observing an actuator: if every day at 6.00AM your smartphone rings to wake you up, then you may react differently depending whether you are at home or on holidays in the Bahamas!

Definition 3. A binary relation R over networks is barb preserving if M RN and M ↓ a@h!v implies N ⇓ a@h!v .
Definition 4. A binary relation R over networks is reduction closed if whenever M R N the following conditions are satisfied:

-M M implies N * N and M R N -M a M implies N * a * N and M R N .
Here, we require reduction closure of both and a , for any a. This is a crucial design decision in CaIT (see Ex. 2 and Sec. 2.3 for details).

In order to model sensor updates made by the physical environment on a sensor s, in a given location h, we define the operator [s@h → v] on networks. Definition 5. Given a location h, a sensor s, and a value v, we define:

n[I P ] µ h [s@h → v] def = n[I[s → v] P ] µ h , if I(s) defined n[I P ] µ k [s@h → v] def = n[I P ] µ k , if I(s) undef. or h = k (M | N )[s@h → v] def = M [s@h → v] | N [s@h → v] (νc)M [s@h → v] def = (νc) M [s@h → v] 0[s@h → v] def = 0.
Notice that when updating a sensor we use its location, also for node-dependent sensors. This is because when changing a node-dependent sensor (e.g. touching a touchscreen of a smartphone) the environment is in general aware of its position.

Definition 6. A binary relation R is contextual if M R N implies that -for all networks O, M | O R N | O -for all channels c, (νc)M R (νc)N -for all s, h, and v in the domain of s, M [s@h → v] R N [s@h → v].
The first two clauses requires closure under logical contexts (parallel systems), while the last clause involves physical contexts, which can nondeterministically update sensor values.

Finally, everything is in place to define our touchstone behavioural equality.

Definition 7. Reduction barbed congruence, ∼ =, is the largest symmetric relation over networks which is reduction closed, barb preserving and contextual.

Remark 1. Obviously, if M ∼ = N then M and N will be still equivalent in any setting where sensor updates are governed by specific physical laws.

We recall that the reduction relation ignores the passage of time, and therefore the reader might suspect that our reduction barbed congruence is impervious to the precise timing of activities. We show that this is not the case. Behind this example there is the general principle that reduction barbed congruence is sensitive to the passage of time. Had we merged a with τ then we would have M ∼ = N because the capability to observe messages on actuators, given by the barb, would not be enough to observe changes on actuators within one time interval.

Design choices

CaIT is a value-passing process calculus, à la CCS, which can be easily adapted to deal with the transmission of channel names, à la π-calculus [START_REF] Sangiorgi | The Pi-Calculus a theory of mobile processes[END_REF].

The time model we adopt is known as the fictitious clock approach (see [START_REF] Hennessy | A process algebra for timed systems[END_REF]): a global clock is supposed to be updated whenever all nodes agree on this, by globally synchronising on a special timing action σ. Thus, time synchronisation relies on some clock synchronisation protocol for mobile wireless systems [START_REF] Sundararaman | Clock synchronization for wireless sensor networks: a survey[END_REF].

In cyber-physical systems [START_REF] Schaft | An introduction to hybrid dynamical systems[END_REF], sensor changes are usually modelled either using continuous models (differential equations) or through discrete models (difference equations) 4 . However, in this paper we aim at providing a behavioural semantics for IoT applications from the point of the view of the end user. And the end user cannot directly observe changes on the sensors of an IoT application: she can only observe the effects of those changes via actuators and communication channels. Thus, in CaIT we do not represent sensor changes via specific models, but we rather abstract on them by supporting nondeterministic sensor updates (see Def. 5 and 6). Actually, as said in Rem. 1, behavioural equalities derived in our setting remains valid when adopting any specific model for sensor updates.

In CaIT the value associated to sensors and actuators can change more than once within the same time interval. At first sight this choice may appear weird as certain actuators may require some time to turn on. On the other hand, other actuators may have a very quick reaction. A similar argument applies to sensors. In this respect CaIT does not enforce a synchronisation of physical events as it happens for logical signals in synchronous languages [START_REF] Boussinot | The SL synchronous language[END_REF]. In fact, actuator changes are under nodes' control: if an actuator is a slow device then it is under the responsibility of its controller to update the actuator with a proper delay. Similarly, a sensor should be read only when its value makes sense.

Unlike mobile computations [START_REF] Cardelli | Mobile ambients[END_REF], smart devices do not decide where to move to: an external agent moves them. Furthermore, Def. 1 imposes that locationdependent sensors can only occur in stationary nodes. This allows us a local, rather than a global, representation of those sensors. The representation of mobile location-dependent sensors would have the same technical challenges of mobile wireless sensor networks [START_REF] Sundararaman | Clock synchronization for wireless sensor networks: a survey[END_REF].

Finally, we would like to explain our choice of barb. As said in the Introduction there are other possible definitions. For instance, one could observe the capability to transmit along a channel c, by defining ), with J (a) = 0, then it is easy to show that M ↓ c@h if and only if S a S ↓ a@h!1 . Thus, the barb on channels can always be reformulated in terms of our barb. The vice versa is not possible. The reader may also wonder whether it is possible to turn the reduction a into τ by introducing some special barb which would be capable to observe actuators changes. For instance, something like

M ↓ c@h if M ≡ (ν g) n[I c v .P Q | R]
M ↓ a@h!v.w if M ≡ (ν g) n[I a!w.P | Q] µ h | M , with I(a) = v and v = w.
It should be easy to see that this extra barb would not help in distinguishing the terms proposed in Ex. 2. Actually, here there is something deeper that needs to be spelled out. In process calculi, the term β of a barb ↓ β is a concise encoding of a context C β expressible in the calculus and capable to observe the barb ↓ β . However, our barb ↓ a@h!v does not have such a corresponding physical context in our language. Said with an example, in CaIT we do not represent the "eyes of a person" looking at the values appearing to some display. Technically speaking, in our calculus we don't have terms of the form a?(x).P to read values on the actuator a, simply because such terms would not be part of an IoT system. The lack of this physical

= nP [IP BoilerCtrl | LightCtrl] m out Home def = LM1 ˛BM ˛LM2 LM1 def = n1[I1 LightM ng1] s loc 1 LM2 def = n2[I2 LightM ng2] s loc 4 BM def = nB[IB BoilerM ng] s loc 2 BoilerCtrl def = fix X.mode?(z). b z .σ.X X LightCtrl def = Q 2 j=1 fix X. cj .σ.X X LightM ngj def = fix X. cj().lightj!on.σ.X lightj!off.X for j ∈ {1, 2} BoilerM ng def = fix X. b(x).[x = man] boiler!on.σ.M anual; T empCtrl T empCtrl M anual def = fix Y.b(y).[y = auto]X; σ.Y T empCtrl def = temp?(t).[t < Θ] boiler!on.σ.X; boiler!off.σ.X
context, together with the persistent nature of actuators' state, explains why our barb ↓ a@h!v must work together with the reduction relation a to provide the desired distinguishing power of ∼ =. Further discussions can be found in [START_REF] Castiglioni | A Semantic Theory of the Internet of Things[END_REF].

Case study: a smart home

In Tab. 2, we model the smart home discussed in the Introduction, and represented in Fig. 1. Our house spans over 4 contiguous physical locations loc i , for i = [1..4], such that d(loc i , loc j ) =| i -j |. The entrance is in loc 1 , the patio spans from loc 2 to loc 3 and the lounge is at loc 4 . The house can only be accessed via its entrance.

Our system Sys consists of the parallel composition of the smartphone, P hone, and the smart home, Home. The smartphone is represented as a mobile node, with δ = 1, initially placed outside the house: out = loc j , for j ∈ [1..4]. As the phone can only access the house from its entrance, and δ = 1, we have d(l, loc i ) ≥ i, for any l ∈ {loc 1 , loc 2 , loc 3 , loc 4 } and i ∈ [1..4]. Its interface I P contains only one sensor, called mode, representing the touchscreen to control the boiler. This is a node-dependent sensor. The process BoilerCtrl reads sensor mode and forwards its value to the boiler manager in the patio, BoilerM ng, via the Internet channel b (rng(b) = ∞). The domain of mode is {man, auto}, where man stands for manual and auto for automatic; initially, I P (mode) = auto.

In P hone there is a second process, called LightCtrl, which allows the smartphone to switch on lights only when getting in touch with the light managers installed in the rooms. Here, channels c 1 and c 2 serve to control the lights of entrance and lounge, respectively; these are short-range channels: rng(c 1 ) = rng(c 2 ) = 0.

The smart home Home consists of three stationary nodes: LM 1 , BM , and LM 2 . The light managers processes LightM ng 1 , LightM ng 2 , are placed in LM 1 and LM 2 , respectively. They manage the corresponding lights via the actuators light j , for j ∈ {1, 2}. The domain of these actuators is {on, off}; initially, I j (light j ) = off, for j ∈ {1, 2}.

= nP [IP BoilerCtrl | LightCtrl] m out Home def = Home ˛CLM CLM def = nC [∅ CLightM ng] s loc 3 LightCtrl def = fix X.@(x). g x .σ.X X CLightM ng def = fix X. g(y).[y = loc1] c1 .σ.X X; [y = loc4] c2 .σ.X X; σ.X X
The boiler manager process BoilerM ng is placed in BM (node n B ). Here, the physical interface I B contains a sensor named temp and an actuator called boiler; temp is a location-dependent temperature sensor, whose domain is N, and boiler is an actuator to display boiler functionality, whose domain is {on, off}. The boiler manager can work either in automatic or in manual mode. In automatic mode, sensor temp is periodically checked: if the temperature is under a threshold Θ then the boiler will be switched on, otherwise it will be switched off. Conversely, in manual mode, the boiler is always switched on. Initially, the boiler is in automatic mode, I B (temp) = Θ, and I B (boiler) = off.

Our system Sys enjoys a number of desirable run-time properties. For instance, if the boiler is in manual mode or its temperature is under the threshold Θ then the boiler will get switched on, within one time unit. Conversely, if the boiler is in automatic mode and its temperature is higher than or equal to the threshold Θ, then the boiler will get switched off within one time unit. These three fairness properties can be easily proved because our calculus is well-timed. In general, similar properties cannot be expressed in untimed calculi. Finally, our last property states the phone cannot act on the lights of the two rooms at the same time, manifesting a kind of "ubiquity". For the sake of simplicity, in the following proposition we omit location names both in barbs and in sensor updates, writing ↓ a!v instead of ↓ a@h!v , and [s → v] instead of [s@h → v]. The system Sys denotes an arbitrary (stable) derivative of Sys. Finally, we propose a variant of our system, where lights functionality depends on the position of the smartphone. Intuitively, the smartphone detects is current GPS position, via the process @(x).P , and then sends it to a centralised light manager process, CLightM ng, via an Internet channel g. This process will interact with the local light managers to switch on/off lights, depending on the position of the smartphone. In Table 3, new components have been overlined. Channels c 1 and c 2 have different range now, as they serve to communicate with the centralised light manager: rng(c 1 ) = 2 and rng(c 2 ) = 1.

Prop. 3 holds for Sys as well. Actually, the two systems are closely related.

Table 4 Intensional semantics for processes

(SndP) - c v .P Q cv ---→ P (RcvP) - c(x).P Q cv ---→ P { v /x} (PosP) - @(x).P @h ---→ P { h /x} (Com) P cv ---→ P Q cv ---→ Q rng(c) = -1 P | Q τ --→ P | Q (Sensor) - s?(x).P s?v ---→ P { v /x} (Actuator) - a!v.P a!v ---→ P (ParP) P λ --→ P λ = σ P | Q λ --→ P | Q (Fix) P { fix X.P /X } λ --→ Q fix X.P λ --→ Q (TimeNil) - nil σ --→ nil (Delay) - σ.P σ --→ P (Timeout) - π.P Q σ --→ Q (TimeParP) P σ --→ P Q σ --→ Q P | Q τ --→ P | Q σ --→ P | Q Proposition 4. For δ = 1, (νc)Sys ∼ = (νc)(νg)Sys.
The bisimulation proof technique developed in the remainder of the paper will be very useful to prove equalities between systems of such size.

We end this section with a comment. While reading this case study the reader should have noticed that our reduction semantics does not model sensor updates. This is because sensor changes depend on the physical environment, and a reduction semantics models the evolution of a system in isolation. Interactions with the external environment will be treated in our extensional semantics.

Labelled transition semantics

In this section we provide two labelled semantic models in the SOS style of Plotkin: the intensional semantics and the extensional semantics.

Intensional semantics Since our syntax distinguishes between networks and processes, we have two different kinds of transitions:

-P λ --→ Q, with λ ∈ {σ, τ, cv, cv, @h, s?v, a!v}, for process transitions -M ν --→ N , with ν ∈ {σ, τ, a, cv@h, cv@h}, for network transitions.

In Tab. 4 we report transition rules for processes, very much in the style of [START_REF] Hennessy | A process algebra for timed systems[END_REF]. As in CCS, we assume

@h ---→ P n[I P ] µ h τ --→ n[I P ] µ h (SensRead) I(s) = v P s?v ---→ P n[I P ] µ h τ --→ n[I P ] µ h (ActUnChg) I(a) = v P a!v ---→ P n[I P ] µ h τ --→ n[I P ] µ h (LocCom) P τ --→ P n[I P ] µ h τ --→ n[I P ] µ h (ActChg) I(a) = v P a!v ---→ P I := I[a → v] n[I P ] µ h a --→ n[I P ] µ h (TimeStat) P σ --→ P n[I P ] s h τ --→ n[I P ] s h σ --→ n[I P ] s h (TimeMob) P σ --→ P n[I P ] m h τ --→ d(h,k)≤δ n[I P ] m h σ --→ n[I P ] m k (Snd) P cv ---→ P rng(c) ≥ 0 n[I P ] µ h cv@h -----→ n[I P ] µ h (Rcv) P cv ---→ P rng(c) ≥ 0 n[I P ] µ h cv@h -----→ n[I P ] µ h (GlbCom) M cv@k -----→ M N cv@h -----→ N d(h, k) ≤ rng(c) M | N τ --→ M | N (ParN) M ν --→ M ν = σ M | N ν --→ M | N (TimePar) M σ --→ M N σ --→ N M | N τ --→ M | N σ --→ M | N (TimeZero) - 0 σ --→ 0 (Res) M ν --→ N ν ∈ {cv@h, cv@h} (νc)M ν --→ (νc)N
models timeouts when channel communications are not possible in the current time interval. Rule (TimeParP) is for time synchronisation of parallel processes.

The symmetric counterparts of Rules (ParP) and (Com) are omitted.

In Tab. 5 we report the rules for networks. Rule (Pos) extracts the position of a node. Rule (SensRead) models the reading of a sensor of the enclosing node. Rules (ActUnChg) and (ActChg) describes the writing of a value v on an actuator a of the node, distinguishing whether the value of the actuator is changed or not. Rule (LocCom) models intra-node communications. Rule (TimeStat) models the passage of time for a stationary node. Rule (TimeMob) models both time passing and node mobility at the end of a time interval. Rules (Snd) and (Rcv) model transmission and reception along an global channel. Rule (GlbCom) models internode communications. The remaining rules are straightforward. The symmetric counterparts of Rules (ParN) and (GlobCom) are omitted.

The reduction semantics and the labelled intensional semantics coincide.

Theorem 1 (Harmony theorem). Let ω ∈ {τ, a, σ}:

-M ω --→ M implies M ω M -M ω M implies M ω --→ M , for some M such that M ≡ M .
Extensional semantics Here we redesign our LTS to focus on the interactions of our systems with the external environment. As the environment has a logical makes communication simpler than ours; on the other hand it does not allow to enforce that a smart device cannot be in two places at the same time. In CaIT, both sensors and actuators are under the control of a single entity, i.e. the process of the node where they were deployed. This was a security issue. CaIT has a finer control of inter-node communication: takes into account both distance among nodes and transmission range of channels. Node mobility in CaIT is timed constrained: in one time unit at most a fixed distance δ may be covered.

Finally, Lanese et al. equip the IoT-calculus with an end-user bisimilarity which shares the same motivations of our bisimilarity. In the IoT-calculus, end users provide values to sensors and check actuators. Unlike us, they can also observe node mobility but they cannot observe channel communication. Enduser bisimilarity is not preserved by parallel composition. Compositionality is recovered by strengthening its discriminating power.

Our calculus takes inspiration from algebraic models for wireless systems [START_REF] Lanese | An Operational Semantics for a Calculus for Wireless Systems[END_REF][START_REF] Nanz | A Framework for Security Analysis of Mobile Wireless Networks[END_REF][START_REF] Merro | An Observational Theory for Mobile Ad Hoc Networks (full version)[END_REF][START_REF] Godskesen | A Calculus for Mobile Ad Hoc Networks[END_REF][START_REF] Benetti | Model checking ad hoc network routing protocols: Aran vs. endairA[END_REF][START_REF] Lanotte | Semantic analysis of gossip protocols for wireless sensor networks[END_REF][START_REF] Merro | A timed calculus for wireless systems[END_REF][START_REF] Ghassemi | Verification of Mobile Ad Hoc Networks: an Algebraic Approach[END_REF][START_REF] Singh | A process calculus for Mobile Ad Hoc Networks[END_REF][START_REF] Fehnker | A process algebra for wireless mesh networks[END_REF][START_REF] Merro | A calculus of trustworthy ad hoc networks[END_REF][START_REF] Cerone | Modelling mac-layer communications in wireless systems[END_REF][START_REF] Borgström | Broadcast psi-calculi with an application to wireless protocols[END_REF]. Most of these models adopt broadcast communication, while we consider point-to-point communication, as in [START_REF] Lanese | Internet of things: a process calculus approach[END_REF][START_REF] Fehnker | A process algebra for wireless mesh networks[END_REF][START_REF] Merro | A calculus of trustworthy ad hoc networks[END_REF]. We model network topology as in [START_REF] Lanese | An Operational Semantics for a Calculus for Wireless Systems[END_REF][START_REF] Merro | An Observational Theory for Mobile Ad Hoc Networks (full version)[END_REF]. Prop. 2 was inspired by [START_REF] Cerone | Modelling mac-layer communications in wireless systems[END_REF]. Fully abstract observational theories for calculi of wireless systems appear in [START_REF] Godskesen | A Calculus for Mobile Ad Hoc Networks[END_REF][START_REF] Merro | An Observational Theory for Mobile Ad Hoc Networks (full version)[END_REF][START_REF] Cerone | Modelling mac-layer communications in wireless systems[END_REF].

Vigo et al. [START_REF] Vigo | Broadcast, denial-of-service, and secure communication[END_REF] proposed a calculus for wireless-based cyber-physical systems endowed with a theory to model and reasoning on cryptographic primitives, together with explicit notions of communication failure and unwanted communication. However, as pointed out in [START_REF] Wu | A calculus for wireless sensor networks from quality perspective[END_REF], the calculus does not provide a notion of network topology, local broadcast and behavioural equivalence. It also lacks a clear distinction between physical components (sensor and actuators) and logical ones (processes). Compared to [START_REF] Vigo | Broadcast, denial-of-service, and secure communication[END_REF], paper [START_REF] Wu | A calculus for wireless sensor networks from quality perspective[END_REF] introduces a static network topology and enrich the theory with an harmony theorem.

CaIT shares some similarities with the synchronous languages of the Esterel family [START_REF] Boussinot | The SL synchronous language[END_REF]. In synchronous languages, computations proceed in phases called instants, which have some similarity with our time intervals. For instance, our timed reduction semantics has some points in common with that of CRL [START_REF] Attar | Fine-Grained and Coarse-Grained Reactive Noninterference[END_REF].

Finally, CaIT is somehow reminiscent of the SCEL language [9]. A framework to model behaviour, knowledge, and data aggregation of Autonomic Systems.

Fig. 1 A

 1 Fig. 1 A simple smart home

Definition 1 .

 1 A network M is said to be well-formed if: (i) it does not contain two nodes with the same name; (ii) different nodes have different actuators and different node-dependent sensors; (iii) for each n[I P ] µ h in M , with a prefix s?(x) (resp. a!v) in P , I(s) (resp. I(a)) is defined; (iv) for each n[I P ] µ h in M with I(s) defined for some location-dependent sensor s, it holds that µ = s.

Example 1 .

 1 Let M = n[∅ σ. c nil] s h and N = n[∅ c nil] s h , with rng(c) = ∞. Then, M σ N . As does not distinguish instantaneous from timed reductions, one may suspect that M ∼ = N , and that a prompt transmission along channel c is equivalent to the same transmission delayed of one time unit. However, the test T = test[J σ.a!1. c().a!0 nil] s l , with J (a) = 0, for some actuator a, can distinguish the two networks. In fact, if M | T a O = n[∅ c nil] s h | test[J c().a!0 nil] s l , with J (a) = 1, then there is no O such that N | T * a * O with O ∼ = O . This is because O can perform a reduction sequence a that cannot be matched by any O .

Proposition 2 .

 2 If M ∼ = N and M σ M then there is N such that N * τ σ * τ N and M ∼ = N . Now, we provide some insights into the design decision of having two different instantaneous reductions τ and a . Example 2. Let M =n[I a!1 | a!0.a!1] µ h and N =n[I a!1.a!0.a!1] µ h , with I(a)=0 and undefined otherwise. Then, within one time unit, M may display on the actuator a either the sequence of values 01 or the sequence 0101, while N can only display the sequence 0101. As a consequence, for a physical observer, the behaviours of M and N are clearly different. Now, if M τ a M = n[J a!1] µ h , with J (a) = 1, the only possible reply of N respecting reduction closure is N * a N = n[J a!0.a!1] µ h . However, it is evident that M ∼ = N because N can turn the actuator a to 0 while M cannot. Thus, M ∼ = N .

µk|

  N with c ∈ g and d(h, k) ≤ rng(c). However, if you consider the system S = (νc)(M | m[J c(x).a!1 nil] µ h

  [b]P ; Q = P if b = true, and [b]P ; Q = Q if b = false. Rules (SndP), (RcvP) and (Com) model communications along a channel c. Rule (PosP) is for extracting the physical position of the embedding node. Rules (Sensor) and (Actuator) serve to read sensors, and to write on actuators, respectively. Rules (ParP) and (Fix) are straightforward. The remaining rules allow us the derive the timed action σ. In Rule (Delay) a timed prefix is consumed. Rule (Timeout)

Table 2

 2 A smart home in CaIT

	Sys	def = P hone ˛Home
	P hone	def

Table 3

 3 Smart home: a position based light management

	Sys	def = P hone ˛Home
	P hone	def

  Proposition 3 (Run-time properties). Let Sys ( * i σ ) * Sys . -If Sys [mode →man] * i Sys σ then Sys ↓ boiler!on -If Sys [temp → t] * i Sys σ , with t < Θ, then Sys ↓ boiler!on -If Sys [temp → t] * i Sys σ , with t ≥ Θ, then Sys ↓ boiler!off -If Sys * i Sys ↓ light1!on then Sys ↓ light2!off , and vice versa.

Table 5

 5 Intensional semantics for networks

	(Pos)	P

See[START_REF] Sangiorgi | The Pi-Calculus a theory of mobile processes[END_REF] for a comparison between this approach and the original barbed congruence.

Difference equations relate to differential equations as discrete math relate to continuous math.

Acknowledgements We thank Ilaria Castellani and Matthew Hennessy for their precious comments, and Valentina Castiglioni for an early proof of the harmony theorem. The anonymous referees provided useful comments.

part (the parallel nodes) and a physical part (the physical world) our extensional semantics distinguishes two different kinds of transitions:

-M α --→ N , logical transitions, for α ∈ {τ, σ, a, cv k, cv k}, to denote the interaction with the logical environment; here, actuator changes, τ -and σ-actions are inherited from the intensional semantics, so we don't provide inference rules for -M α --→ N , physical transitions, for α ∈ {s@h?v, a@h!v}, to denote the interaction with the physical world .

In Tab. 6 the extensional actions deriving from rules (SndObs) and (RcvObs) mention the location k of the logical environment which can observe the communication occurring at channel c. Rules (SensEnv) and (ActEnv) model the interaction of a system M with the physical environment. The environment can nondeterministically update the current value of (location-dependent or node-dependent) sensors, and can read the information exposed on actuators.

Note that our LTSs are image finite. They are also finitely branching, and hence mechanisable, under the obvious assumption of finiteness of all domains of admissible values, and the set of physical locations.

Full abstraction

Based on our extensional semantics, we are ready to define a notion of bisimilarity. We adopt a standard notation for weak transitions. We denote with =⇒ the reflexive and transitive closure of τ -actions, namely ( Later on, we will take into account the number of τ -actions performed by a process. The expansion relation [START_REF] Arun-Kumar | An efficiency preorder for processes[END_REF], written , is a well-known asymmetric variant of ≈ such that P Q holds if P ≈ Q and Q has at least as many τ -moves as P .

A main result is that our bisimilarity is a congruence.

Theorem 2 (Congruence theorem). The relation ≈ is contextual.

The proof that ≈ is preserved by the sensor update operator [s@h → v] is non-standard and technically challenging. It required a well-founded induction. Thm. 2 is crucial to prove that our bisimilarity is sound with respect to reduction barbed congruence. Actually, our bisimilarity is both sound and complete.

Soundness follows from Thm. Thm. 2, and the capability of extensional actions to capture barbs. As to completeness, for any extensional action α we exhibit an observing context C α .

Remark 2. A consequence of Thm. 3 and Rem. 1 is that our bisimulation prooftechnique remains sound in a setting with more restricted contexts, where nondeterministic sensor updates are replaced by some specific model for sensors.

As testbed for our notion of bisimilarity, we prove a number of algebraic laws on well-formed networks.

Theorem 4 (Some algebraic laws). Laws 1-4 are a sort of tau-laws. Laws 5 and 6 models garbage collection of processes and nodes, respectively. Law 7 gives a sufficient condition for node anonymity as well as for non-observable node mobility.

Finally, we show that our labelled bisimilarity can be used to deal with more complicated systems. Let us prove that the two variants of the smart home mentioned in Prop. 4 are actually bisimilar. Due to the size of the systems involved, the proof of the proposition above is quite challenging. In this respect, the first four laws of Thm. 4 are fundamentals to apply non-trivial up-to expansion proof-techniques [START_REF] Sangiorgi | The Pi-Calculus a theory of mobile processes[END_REF].

Related work

To our knowledge, the IoT-calculus [START_REF] Lanese | Internet of things: a process calculus approach[END_REF] is the first (and only) process calculus for IoT systems. We report here the main differences between CaIT and the IoT-calculus. In CaIT, we can express desirable time and runtime properties (see Prop. 1 and Prop. 3). The nondeterministic link entailment of the IoT-calculus


Lazhar Dhaouadi
email: lazhardhaouadi@yahoo.fr

Applications of the q-Fourier Analysis to the Symmetric Moment Problem

Sufficient condition for the symmetric moment problem to be determinate is given using standards methods of q-Fourier analysis. This condition it cannot be a particular case of Carleman's criterion.

Introduction

For a positive measure µ on R, the nth moment is defined as

s n = x n dµ(x),
provided the integral exists. Let M * (R) be the set of positive measures on R with moment of any order and with infinite support. Given µ ∈ M * (R), then we consider V µ the set of all ν ∈ M * (R) such that s n = x n dµ(x) = x n dν(x) for n ≥ 0.

We say that µ is determinate if V µ = {µ}, otherwise µ is indeterminate. For more detail to this subject, the reader can consult the references [START_REF] Berg | Moment problems and polynomial approximation, Annales de la facultè des sciences de Toulouse 6 e série, tome spécial ≪ 100 ans après Th[END_REF] and [START_REF] Berg | Density questions in the classical theory of moments[END_REF], and the references theine. We recall that a moment problem is said to be symmetric if all moments of odd order are 0. It is desirable to be able to tell whether the moment problem is determinate or indeterminate just by looking at the moment sequence (s n ) n≥0 . We have the following classical sufficient condition for determinacy:

The Perron's criterion lim sup n→∞ s 2n (2n)! 1/2n < ∞ (1)
The Riesz's criterion

lim inf n→∞ s n n! 1/n < ∞ (2)
The Carleman's criterion

∞ n=1 1 2n √ s 2n = ∞ (3)
It follows easily that we have

(1) ⇒ (2) ⇒ (3).
So by Carlemans theorem (see [START_REF] Carleman | Sur les Problèmes des moments[END_REF]), if µ satisfy (3) then µ is determinate. In the end we have the following equivalent form of the Perron condition ∞ 0 e α|x| dµ(x) < ∞, for some α > 0.

For µ ∈ M * (R) let (P n ) be the corresponding orthonormal polynomials determined by

P n (x) = k n x n + ...., k n > 0; P n (x)P m (x)dµ(x) = δ nm .
For an indeterminate µ ∈ M * (R), it is known that the series

|P n (z)| 2 and
|Q n (z)| 2 converge uniformly on compact subsets of C, where (Q n ) the polynomials of the second kind

Q n (x) = P n (x) -P n (y) x -y dµ(y), x ∈ C.
Therefore, the series

A(z) = z ∞ n=0 Q n (0)Q n (z) B(z) = -1 + z ∞ n=0 Q n (0)P n (z) C(z) = 1 + z ∞ n=0 P n (0)Q n (z) D(z) = z ∞ n=0
P n (0)P n (z) determine entire functions. For t ∈ R∪{∞}, we introduce the special discrete measures so called N-extremal of the form

ν t = λ∈Λt m λ δ λ , Λ t = {z ∈ C B(z)t -D(z) = 0}, m λ = A(λ)t -C(λ) B ′ (λ)t -D ′ (λ) = ∞ n=0 P 2 n (λ) -1 , for λ ∈ Λ t , with Λ ∞ = {z ∈ C B(z) = 0}.
We recall the following result of M. Riesz [START_REF] Riesz | Sur le problème des moments et le théorème de Parseval correspondant[END_REF]:

Let µ ∈ M * (R) 1. If µ is indeterminate and ν ∈ V µ then (P n ) form an orthonormal basis of L 2 (ν) if and only if ν is N-extremal.
2. If µ is determinate then (P n ) form an orthonormal basis of L 2 (µ).

Main Results

We consider 0 < q < 1 and we design by µ the positive measure defined by

dµ(x) = ω(x) 2 dσ(x) = ω(x) 2 |x| 2v+1 d q x, v > -1,
where d q x a discrete measure defined by

d q x = (1 -q) n∈Z q n δ q n .
and ω an even real function satisfies ω(q n ) = 0 for all n ∈ Z.

Let (P n ) be the corresponding orthonormal polynomials for µ, and we consider R + q the support of µ

R + q = {q n , n ∈ Z}.
Theorem 1 The sequence (P n ) form an orthonormal basis of L 2 (µ) if and only if µ is determinate.

Proof. If the sequence (P n ) form an orthonormal basis of L 2 (µ) then µ is determinate or N-extremal. Suppose that µ is N-extremal, then there exist

t ∈ R ∪ {∞} such that µ = ν t = λ∈Λt m λ δ λ .
This implies Λ t = R + q . In the other hand Λ t is the set of zero of entire function and {0} is an accumulation point of Λ t , then Λ t = C, which is absurd.

Proposition 1

The sequence (P n ) form an orthonormal basis of L 2 (µ) if and only if

ψ n (x) = ω(x)P n (x),
form an orthonormal basis of L 2 (σ).

Proof. It is clear that

P n (x)P m (x)dµ(x) = δ nm ⇔ ψ n (x)ψ m (x)dσ(x) = δ nm .
Now, let f be a function belongs to L 2 (σ) and put g(x) = f (x) ω(x) , then g ∈ L 2 (µ) and we have g(x)P n (x)dµ(x) = 0 ⇔ f (x)ψ n (x)dσ(x) = 0, which lead to the result. Theorem 2 Let s n be the nth moment of σ. If

lim n→∞ q n/4 2n √ s 2n = 0, ( 4
)
then µ is determinate.

Proof. Using theorem 2, it suffice to prove that (P n ) form an orthonormal basis of L 2 (µ) and by the proposition 1, this is equivalent to prove that (ψ n ) form an orthonormal basis of L 2 (σ). Let f be a function belongs to L 2 (σ) such that f (x)ψ n (x)dσ(x) = 0, ∀n ∈ N.

We can write f = f + + f -, where f + is even and f -is odd. This implies

f + (x)x 2n ω(x)dσ(x) = f -(x)x 2n+1 ω(x)dσ(x) = 0, ∀n ∈ N. Then f + (x)ω(x)j v (λx, q 2 )dσ(x) = xf -(x)ω(x)j v (λx, q 2 )dσ(x) = 0, ∀λ ∈ R + q ,
where j v (x, q 2 ) is the the normalized q-Bessel function of third kind defined by

j v (x, q 2 ) = ∞ n=0
(-1) n q n(n+1) (q 2 , q 2 ) n (q 2v+2 , q 2 ) n x 2n .

We can exchange integral and sum because

∞ n=0 q n(n+1) (q 2 , q 2 ) n (q 2v+2 , q 2 ) n λ 2n |f + (x)|x 2n ω(x)dσ(x) ≤ f + 2 ∞ n=0 q n(n+1) (q 2 , q 2 ) n (q 2v+2 , q 2 ) n λ 2n x 4n ω 2 (x)dσ(x) 1/2 ≤ f + 2 ∞ n=0 q n(n+1) (q 2 , q 2 ) n (q 2v+2 , q 2 ) n √ s 4n λ 2n < ∞. and ∞ n=0 q n(n+1) (q 2 , q 2 ) n (q 2v+2 , q 2 ) n λ 2n |xf -(x)|x 2n ω(x)dσ(x) ≤ f - 2 ∞ n=0
q n(n+1) (q 2 , q 2 ) n (q 2v+2 , q 2 ) n λ 2n

x 2(2n+1) ω 2 (x)dσ(x)

1/2 ≤ f - 2 ∞ n=0 q n(n+1) (q 2 , q 2 ) n (q 2v+2 , q 2 ) n √ s 2(2n+1) λ 2n < ∞.
The convergence of the above series is a simple consequence of the Cauchy root test (4).

In [START_REF] Dhaouadi | Inequalities in q-Fourier Analysis[END_REF] the authors introduce the q-Bessel Fourier transform as follows

F q,v f (λ) = c q,v ∞ 0 f (x)j v (λx, q 2 )x 2v+1 d q x, ∀λ ∈ R q ,
where f is an even function belongs to L 1 (σ) and he have proved that if F q,v f = 0 then f = 0. Using the Cauchy-Schwartz inequality we prove that f + ω and xf -ω belongs to L 1 (σ), which implies that f + = f -= 0.

Application

In [START_REF] Ismail | A simple proof of Ramanujan's 1 ψ 1 sum[END_REF], the Ramanujan identity was proved k∈Z z k (bq k , q) ∞ = (bz, q/bz, q, q) ∞ (b, z, q/b, q) ∞ , where

(x, q) ∞ = ∞ i=0 (1 -q i x).
Let α > 0 and replace in the above sum b → -1, z → q α z, we obtain k∈Z q αk z k (-q k , q) ∞ = (-q α z, -q -α q/z, q, q) ∞ (-1, q α z, -q, q) ∞ = (-q α z, q, q) ∞ (-1, q α z, -q, q) ∞ (-q -α q/z, q) ∞ .

On the other hand (-q -α q/z, q) ∞ = ∞ i=0

(1 + q i-α q/z) =

[α] i=0

(1 + q i-α q/z)

∞ i=[α]+1
(1 + q i-α q/z)

= q z α [α] i=0 q i-α [α] i=0 (1 + q α-i z/q) ∞ i=[α]+1 (1 + q i-α z/q) = q z α [α] i=0 (1 + q i q α-[α] z/q) ∞ i=[α]+1 (1 + q i-α z/q)q ( [α] 2 -α)([α]+1) .
This gives

k∈Z q αk z k (-q k , q) ∞ =   (-q α z, q, q) ∞ (-1, q α z, -q, q) ∞ [α] i=0 (1 + q i q α-[α] z/q) ∞ i=[α]+1 (1 + q i-α z/q)   q z α q ( [α] 2 -α)([α]+1) . Put C(α, q, z) =   (-q α z, q, q) ∞ (-1, q α z, -q, q) ∞ [α] i=0 (1 + q i q α-[α] z/q) ∞ i=0 (1 + q i+[α]-α z)   q z α , and
σ(α) = [α] 2 -α ([α] + 1)
Now, let p > 0 and replace

α → n p , q → q 2p , z → q 2v+2 , we get (1 -q) k∈Z q 2nk q 2k(v+1) (-q 2pk , q 2p ) ∞ = (1 -q)C n p , q 2p , q 2v+2 q 2pσ( n p ) ,
We recall the definition of the q-exponential function

e(x, q) = 1 (x, q) ∞ = ∞ i=0 1 1 -q i x ,
and we can write

s 2n = ∞ 0
x 2n e(-x 2p , q 2p )x 2v+1 d q x = (1 -q)C n p , q 2p , q 2v+2 q 2pσ( n p ) , and then 2n √ s 2n = (1 -q)C n p , q 2p , q 2v+1 1 2n q p n σ( n p ) .

It is easy to prove that lim n→∞ (1 -q)C n p , q 2p , q 2v+2 1 2n

= 1.

For the particular case p = 3, we have lim In the end, if we denote by dµ(x) = e(-x 6 , q 6 )x 2v+1 d q x, then by the Theorem 2 we see that µ is determinate, but not satisfying the Carleman's criterion.

  4 2n √ s 2n = 0 and there exist n 0 > 0 such that for all n > n 0


Bruno Sauvalle
email: bruno.sauvalle@mines-paristech.fr

A criterion for the differential flatness of a nonlinear control system

Let's consider a control system described by the implicit equation F (x, ẋ) = 0. If this system is differentially flat, then the following criterion is satisfied : For some integer r, there exists a function ϕ(y0, y1, .., yr) satisfying the following conditions: (1) The map (y0, .., yr+1) → (ϕ(y0, y1, .., yr), ∂ϕ ∂y 0 y1 + ∂ϕ ∂y 1 y2 + .. + ∂ϕ ∂yr yr+1) is a submersion on the variety F (x, p) = 0. (2) The map y0 → x0 = ϕ(y0, 0, .., 0) is a diffeomorphism on the equilibrium variety F (x, 0) = 0.

Inversely, if a control system satifies this flatness criterion, then it is locally controllable at equilibrium points.

Introduction

The purpose of this note is to propose a new approach to the study of the differential flatness of a control system. For an overview of flatness theory, see for example [START_REF] Levine | Analysis and Control of Nonlinear Systems : A Flatness based approach[END_REF]. For an overview of existing differential flatness criteria, see [START_REF] Ph | Flat systems[END_REF], section 3.1.2, and [START_REF] Levine | On necessary and sufficient conditions for differential flatness[END_REF].

We consider a control system defined by the implicit equation F (x, ẋ) = 0, where F (x, p) is a smooth function defined on R n × R n , with rank ∂F ∂p = nm (m > 0). We assume that for each x there exists at least one p satisfying the equation, and more generally that the manifold F (x, p) can be parameterized using a smooth function u → f (x, u) satisfying F (x, f (x, u)) = 0. This condition is trivially satisfied if the system F (x, ẋ) = 0 is derived from some explicit description of the control system such as ẋ = f (x, u) .

Finding parameter functions

We say that a function ϕ(y 0 , ..y r ) defined on (R m ) r+1 with values in R n is a parameter function for the system F if we have for all smooth functions y(t) defined on R with values in R m , and writing x(t) = ϕ(y(t), ẏ(t), .., y (r) (t)), the equality F (x(t), d dt x(t)) = 0. We can also write this condition as :

F (ϕ(y(t), ẏ(t)..y (r) (t)), ∂ϕ ∂y 0 ẏ(t) + .. + ∂ϕ ∂y r y (r+1) (t)) = 0 (1)
Considering that for t fixed, the function y can be chosen so that y(t), ẏ(t), .., y (r+1) (t) take any independent values, we see that we have for any vectors y 0 , .., y r+1 in R m the equality F (ϕ(y 0 , y 1 , .., y r ), ∂ϕ ∂y 0

y 1 + ∂ϕ ∂y 1 y 2 .. + ∂ϕ ∂y r y r+1 ) = 0 (2)
Inversely, it is clear that if a function ϕ satisfies this partial differential equation, then equation ( 1) is satisfied for all smooth functions y.

The question of the existence and computation of parameter functions is then equivalent to the question of existence and computation of solutions to this implicit first order partial differential equation. A wide variety of techniques are available to study this question : Cartan Kähler theory, method of characteristics and Charpit equations if F is scalar, etc ..

The main difficulty here is that ϕ has to be a function of y 0 , ..y r only and must not depend of y r+1 , which appears as a free parameter in the equation. This requires that the ruled manifold criterion described in [START_REF] Rouchon | Necessary Condition and Genericity of Dynamic Feedback Linearization[END_REF] be satisfied.

Differentially flat systems

Let's recall (cf [START_REF] Levine | Analysis and Control of Nonlinear Systems : A Flatness based approach[END_REF]) that a system F (x, ẋ) is called differentially flat if there exists a parameter function ϕ satisfying equation (1) and another function ψ(x 0 , .., x s ) so that a solution x(t) of the system can be written as x(t) = ϕ(y, ẏ...y (r) ) if and only if y(t) = ψ(x, ẋ, ..x (s) ). This requirement is stronger than the existence of a parameter function. Let's note L τ for the derivation operator L τ ϕ(y) = r i=0 ∂ϕ ∂yi y i+1 . If ϕ is associated to a flat system, we have : Proposition 3.1 The smooth map Φ : (y 0 , .., y r+1 ) → (ϕ(y 0 ..y r ), L τ ϕ(y 0 ..y r+1 )) is a submersion on the manifold F (x, p) = 0.

Remark : this implies that dϕ is surjective. Proof : We have to prove that Φ and dΦ are surjective.

Let's consider an element (x 0 , p 0 ) of the manifold and the associated parameter u 0 so that p 0 = f (x 0 , u 0 ). Let's now choose the constant function u(t) defined by the formula u(t) = u 0 . Then the unique solution of the firts order ODE ẋ = f (x, u) with ẋ(0) = p 0 , x(0) = x 0 satisfies F (x, ẋ) = 0 for all values of t and is a smooth function of x 0 and p 0 . Using the function ψ, we get some function y(t) which is also a smooth function of x 0 and p 0 so that x(t) = ϕ(y, ẏ, ..y (r) ). Writing y(0) = y 0 , .., y (r+1) (0) = y r+1 can then write that (x 0 , p 0 ) = (ϕ(y 0 , .., y r ), L τ ϕ(y 0 ..y r+1 ) = Φ(y 0 , ..y r+1 )

This shows that Φ is surjective. Taking the differential of this equation with respect to (x 0 , p 0 ), we get

Id = dΦ • (..)
which shows that dΦ is surjective Proposition 3.2 The restriction of Φ to the elements of the form (y 0 , 0..0) is a diffeomorphism on the equilibrium manifold F (x 0 , 0) = 0

Proof : It is well known that Lie-Bäcklund equivalence preserves equilibrium points ( cf [START_REF] Levine | Analysis and Control of Nonlinear Systems : A Flatness based approach[END_REF], Th 5.2)

Controllability at equilibrium points

We now consider in this section a control system described by an equation F (x, ẋ) = 0 such that the equation (2) has a solution ϕ satisfying propositions 3.1 and 3.2.

Proposition 4.1 The system is locally controllable at equilibrium points.

Proof : We consider some equilibrium point x 0 , so that F (x 0 , 0) = 0. Using 3.1, we see that (x 0 , 0) is in the image of Φ and that dϕ is surjective at this point.

We now show that Kalman criterion is satisfied. Let's note A = ∂f ∂x and B = Im ∂f ∂u Let's take the derivative of the equation

F (x, f (x, u)) = 0 We get ∂F ∂x + ∂F ∂p A = 0
and, considering that for x fixed, the map u → f (x, u) is assumed to be a diffeomorphism on the manifold F (x, p) = 0,

B = Ker ∂F ∂p
We can write the equation (2) as

F (ϕ, L τ ϕ) = 0
Taking differentials with respect to y 0 ..y r+1 , we get the equalities : = 0

∂F ∂x ∂ϕ ∂y i + ∂F ∂p ∂ ∂y i L τ ϕ = 0 using the commutation relation [ ∂ ∂yi , L τ ] = ∂ ∂yi-1 for 1 ≤ i ≤ r + 1
• Differential with respect to y r+1 ( considering that ϕ is a function of y 0 ..y r only) :

∂F ∂p ∂ϕ ∂y r = 0

Considering that (x 0 , 0) is an equilibrium point of the system, we now use 3.2 to get y 1 = y 2 = .. = y r = y r+1 = 0. The equations become :

•••

  Differential with respect to y 0 : Differential with respect to y i for i ∈ 1..r : Differential with respect to y r+1 : A r B + A r-1 B + .. + B and we see that A r B + A r-1 B + .. + B has to contain the range of all the matrices ∂ϕ ∂yi , which generate R n


T D Tran Ngoc

Azita Ahmadi

Henri Bertin

What can be learnt about dispersivity from transport experiments in unsaturated double-porosity soils?

Dispersivity is assumed to be an intrinsic property which characterizes the heterogeneity scale of porous media. When the medium is unsaturated by two fluid phases (water and air), dispersivity depends strongly on the saturation. "Doubleporosity" medium concept can be attributed to a class of heterogeneous soils and rocks in which a strong contrast in local pore size characteristics is observed. In this work, we revisited the intrinsicity of the dispersivity of a double-porosity soil with different saturations, by performing a series of one-dimensional experiments of chloride tracer dispersion under different boundary conditions. The physical double-porosity model was composed of solidified clayey balls, distributed periodically in a more permeable sandy matrix. The dependence of the dispersivity on the saturation in the doubleporosity soil was established and compared with the trends obtained for the single-porosity soils in previous studies. RÉSUMÉ Il est généralement admis que la dispersivité est une propriété intrinsèque qui caractérise l'échelle d'hétérogénéité des milieux poreux. Lorsque le milieu est saturé par deux phases fluides (eau et air), elle dépend fortement de la saturation. Le concept du milieu à « double-porosité » peut être attribué à une classe de sols et de roches hétérogènes dans lesquels on observe un fort contraste de tailles caractéristiques locales de pores. Dans ce travail, nous avons revisité la nature intrinsèque de dispersivité d'un sol à double porosité avec des saturations différentes, en effectuant une série d'expériences unidimensionnelles de la dispersion d'un traceur, pour différentes conditions aux limites. Le modèle physique à double porosité a été composé de sphères argileuses solidifiées, réparties périodiquement dans une matrice de sable plus perméable. La dépendance de la dispersivité de la saturation dans le sol à double porosité a été établie et comparée avec les tendances obtenues pour les sols à simple-porosité dans des études antérieures. 1

INTRODUCTION

To treat a contaminated site, knowledge of the contaminant transport processes in the subsurface is required. One of the key processes is the dispersive transport that can be characterized by a parameter, called dispersivity [START_REF] Bear | Dynamics of fluid in porous media[END_REF]). This parameter is generally defined as the ratio between the dispersion coefficient and the flow velocity [START_REF] Bear | Dynamics of fluid in porous media[END_REF]. It is usually determined from concentration measurements (evolution with time and space) during laboratory and field tracer tests by using conventional/advanced models of convectiondispersion or spatial moments analysis [START_REF] Aris | On the dispersion of a solute in a fluid flowing through a tube[END_REF][START_REF] Fried | Groundwater Pollution[END_REF][START_REF] Gaudet | Solute transfer with exchange between mobile and stagnant water through unsaturated sand[END_REF][START_REF] Khan | A laboratory study of the dispersion scale effect in column outflow experiments[END_REF][START_REF] Vanderborght | Review of dispersivities for transport modeling in soils[END_REF][START_REF] Ngoc | Two-scale modeling of solute dispersion in unsaturated double-porosity media: Homogenization and experimental validation[END_REF]. Although it is largely admitted that the dispersivity is an intrinsic soil property [START_REF] Batu | Applied flow and solute transport modeling in aquifers: Fundamental principles and analytical and numerical methods[END_REF], there is not much information about intrinsic values of this property available for porous media in the literature [START_REF] Scheven | Intrinsic dispersivity of randomly packed monodisperse spheres[END_REF].

In practice, the dispersivity value used to numerically simulate a transport problem is usually estimated based on the length of the contaminant plume, or measuring the distance between the source and specific measurement points [START_REF] Aziz | BIOCHLOR, Natural Attenuation Decision Support System, User's Manual, Version 1.0[END_REF][START_REF] Dogan | Predicting flow and transport in highly heterogeneous alluvial aquifers[END_REF]. This practice comes from a general consensus about the scaledependent dispersivity reported by many over the last few decades (Gelhar et al. 1992;Pachepsky et al. 2003;Huang et al. 2006, among others). In the meanwhile, there has been no general conclusion concerning the saturation-dependent dispersivity for unsaturated media (by water and air). The correlation between the increase of dispersivity with decreasing saturation (Figure 1) has been stated according to the investigation of tracer dispersion experiments in sand columns therefore in single-porosity media [START_REF] Yule | Longitudinal and transverse dispersion coefficients in unsaturated plainfield sand[END_REF][START_REF] De Smedt | Study of tracer movement through unsaturated sand[END_REF]Haga et al. 1990;[START_REF] Padilla | The effect of water content on solute transport in unsaturated porous media[END_REF]Nutzmann et al. 2002;[START_REF] Latrille | Effect of water content on dispersion of transferred solute in unsaturated porous media[END_REF]. However, the experimental results of other authors [START_REF] Maraqa | Effects of degree of water saturation on dispersivity and immobile water in sandy soil columns[END_REF][START_REF] Toride | Hydrodynamic dispersion in an unsaturated dune sand[END_REF][START_REF] Sato | Solute dispersion in a variably saturated sand[END_REF] showed a nonmonotonic variation of the dispersivity as a function of the saturation (Figure 1). They observed for intermediate values of the water saturation, an increase of the dispersivity is observed as the saturation decreases, while the contrary is reported for small saturations [START_REF] Raoof | Saturationdependent solute dispersivity in porous media: Porescale processes[END_REF]Karadimitriou et al. 2016).

A class of heterogeneous soils and rocks can be studied by the concept of "double-porosity" media [START_REF] Barenblatt | Basic concepts in the theory of seepage of homogeneous liquids in the fissured rocks[END_REF] in which a strong contrast in local macro-micro pore size characteristics is observed such as in aggregated soils or fractured porous rocks. Solute dispersion phenomena in the macro-pores with interactions/exchanges with micro-pores are commonly observed [START_REF] Gerke | A dualporosity model for simulating the preferential movement of water and solutes in structured porous media[END_REF][START_REF] Schwartz | Estimating parameters for a dual porosity model to describe non-equilibrium, reactive transport in a finetextured soil[END_REF]. The relation between the dispersivity and water saturation for transport in such media is not still well understood. For this study, we observe the dispersivity of a double-porosity soil with different saturations by performing a series of one-dimensional experiments using a passive tracer (NaCl) under different boundary conditions. Second, we calculate the dispersivity numerically as a function of saturation, using theoretical results obtained from the homogenization method (Tran Ngoc 2008). The main objective is to investigate the dependence of the dispersivity on the saturation in the double-porosity soil and compare to the trends obtained with those observed for the single-porosity media in previous studies. This paper also presents the main results which were obtained with an emphasis put on experimental difficulties related to unsaturated conditions and the presence of heterogeneities.

Figure 1. The saturation-dependent dispersivities obtained from transport experiments in single-porosity soil columns available in the literature. For all experiments reported here, the dispersivity value was determined by the ratio of the dispersion coefficient and pore water velocity. d is mean grain diameter. (Refer to the digital version of this paper to distinguish dispersivity color code of each experiment).

EXPERIMENTS AND METHODOLOGY 2.1 1D physical model of double-porosity soil

The physical model of double-porosity soil constructed from the fine sand HN38 and sintered clay balls was initiated by [START_REF] Lewandowska | Milieux poreux hétérogènes: Modélisation des transferts de masse par homogénéisation[END_REF]. These two geomaterials come from the aquifers of Hostun (Southeastern France) and La Bisbal (Northeastern Spain) respectively. The grain density (g), dry bulk density (d) and average grain diameter (d50, Figure 2) of the HN38 sand were of 2.65 g/cm 3 , 1.59 g/cm 3 and 162 m respectively (Lewandowska et al. 2005), whereas the pore size was estimated in the range of 10 -500 m [START_REF] Vitorge | Size-and concentration-dependent deposition of fluorescent silica colloids in saturated sand columns: transport experiments and modeling[END_REF]. The properties of the clay balls are g= 3.01 g/cm 3 , d = 1.88 g/cm 3 and pore size range of 0.1 -1 m (Figure 2). The balls have an average diameter of 6.4 mm. The saturated permeability of the HN38 sand and sintered clay were respectively 2.87  10 -3 cm/s and 1.96  10 -6 cm/s, while the porosities were about 0.4 and 0.343 respectively [START_REF] Ngoc | Two-scale modeling of solute dispersion in unsaturated double-porosity media: Homogenization and experimental validation[END_REF]). The water retention curves for the sand and clay for imbibition and drainage stages were studied in Lewandowska et al. (2005;2008). Figure 3 presents an image by scanning electron microscope (SEM) for the HN38 sand and sintered clay ball.

The formation of the double-porosity physical soil follows the same principle as that presented in previous studies (Lewandowska et al. 2005;2008;[START_REF] Szymkiewicz | Two-scale modeling of unsaturated water flow in a double-porosity medium under axisymmetric conditions[END_REF]Tran Ngoc 2008;[START_REF] Lewandowska | Experiments and micromechanical modelling of elastic parameters of a composite geomaterial[END_REF]. The HN38 sand and sintered clay balls play the role of the macro-pores (between the sand grains) and micro-pores (inside the balls) in the double-porosity soil respectively. They were interlayered in a manner keeping a volumetric fraction of about 50% for each porous material, to reach a height of 45 -50 cm in a Plexiglas circular column of 6 cm inner diameter. In this way, a 1D periodic double-porosity soil with 3D periodic microstructure of 6.4  6.4  13 mm (see Figure 4) is constructed. This periodic cell is the representative elementary volume (REV) of the medium. Table 1 presents the key hydro-mechanical properties of the double-porosity physical soil. Table 1. Hydro-mechanical properties of the doubleporosity soil with the volume fraction of 50% for each porous material (sand porosity of 0.4 and clay porosity of balls of 0.343). (L = Height of the medium; Sw = water saturation; q = Darcy velocity; Ci = initial concentration in the medium; CL = inlet concentration; "-" unavailable; and "*" pulse duration of 4620 s.) porosity soil. In this model, the flow occurs only in the macro-pores (sandy matrix -domain 1 denoted 1) and is stagnant in the micro-pores (clay balls -domain 2 denoted 2) that resulted from modelling water flow in unsaturated double-porosity soil [START_REF] Lewandowska | Infiltration in a double-porosity medium: experiments and comparison with a theoretical model[END_REF]). The model consists of equations as follows [START_REF] Ngoc | Two-scale modeling of solute dispersion in unsaturated double-porosity media: Homogenization and experimental validation[END_REF]:

Hydrogeology parameter

      t C C C t C w 2 2 1 1 disp 1 1 1 ∂ ∂ ∇ ∇ ∇ ∂ ∂        q D , (1) with:
(1)

         d t C 1 t C 2 2 2 2 2 ∂ ∂ ∂ ∂ . (2)   2 2 2 2 C t ) C ( ∇ ∇ ∂ ∂ D    in the domain 2, 2, (3) 2 1
C C  on the interface  between the two domains, (4) where the indices "1" and "2" stand for the domains 1 (1) and 2 (1) respectively ( = 1 + 1); C [ML -3 ] is the concentration;  [-] is the water content (Sw = 100%  /n, with n porosity); w [-] is the volumetric fraction; q [LT -1 ] is the Darcy velocity vector; t [T] is the time variable; D2 [L 2 T -1 ] is the effective diffusion tensor in the domain 2; and Ddisp [L 2 T -1 ] is the dispersion tensor of the double-porosity medium defined by:

           d 1 1 1 1 disp χ q I χ D D ∇ (5)
where the χ function is the solution of the following local boundary value problem on a periodic microstructure of the double-porosity medium:

    1 1 1 1 1 w 1 q q χ q I χ D          . (6)     0 1    N I χ D ∇ on  , (7) 0 d 1 1       χ χ . ( 8
)
In this study the dispersivity of the double-porosity soil is defined by [START_REF] Bear | Dynamics of fluid in porous media[END_REF]

): q ) S ( D ) S ( w disp w  l . (9)
The dispersion coefficients Ddisp of the tests at different water saturation were determined by fitting with the numerical solution of the above model obtained by using the Comsol Multiphysics® code. The initial value Ddisp came from fitting the dispersion test in the domain 1 (pure sand, not presented here) with the CXTFIT [START_REF] Toride | The CXTFIT code for estimating transport parameters from laboratory or field tracer experiments[END_REF].

Note that the Equation 3 was re-written in the spherical coordinate system for the situation of the physical doubleporosity soil considered here.

Numerical study for the double-porosity dispersivity

We carried out a numerical investigation on the saturation-dependent dispersivity in an imagined doubleporosity medium (Figure 5), in order to try examining a trend of this relationship. For that, we implemented Equations 5 -8 by using also the Comsol Multiphysics® code. Note that the dispersivity value of the numerical study here is not comparable with the one of the physical double-porosity soil used in the dispersion experiments (Figure 4), because the period microstructure of the two media is totally different. We calculated the dispersivity of a double-porosity medium with simple cubic microstructures (Figure 5) at different saturation degrees. The domain 1 of this doubleporosity medium is the same sand material as in the dispersion experiments of [START_REF] Sato | Solute dispersion in a variably saturated sand[END_REF], from which a trend of the saturation-dependent dispersivity was established. The dispersivity is assumed to be the slope of the linear relationship between the dispersion coefficient and the velocity. The unsaturated flow conditions in [START_REF] Sato | Solute dispersion in a variably saturated sand[END_REF] were used in this numerical experiment. It means that the dispersivities of the double-porosity medium were determined at Sw = 50% and 82% for the flow range of 8.84  10 -4 -3.54  10 -3 cm/s. We solved the local boundary value problem (Equations 6 and 7) for the simple cubic period with D1(Sw = 50%) = 4.43  10 -7 cm 2 /s and D1(Sw = 82%) = 2.23  10 -6 cm 2 /s (D1 is the local diffusion tensor in the porous domain 1 which is assumed isotropic. Thus, we have a scalar D1) to calculate dispersion coefficients and then dispersivities. The geometry and soil inputs of the period were reported in the caption of Figure 5.

RESULTS AND DISCUSSION

Water saturation distribution

The precise water content distribution was already difficult to determine in homogeneous media of the previous experimental works (Paddila et al. 1999;Nutzmann et al. 2002;[START_REF] Latrille | Effect of water content on dispersion of transferred solute in unsaturated porous media[END_REF]. Figure 6 presents the water content () distribution of the double-porosity soils within the dispersion experiments under both saturated (Test 1) and unsaturated (Test 2) conditions. It is observed that the water content profiles have a non-uniform distribution.

Double-porosity dispersivity estimation

We fitted the dispersion coefficients Ddisp of the doubleporosity soil by reproducing the numerical BTCs for the experimental BTCs, with the double-porosity model (Figure 7), while keeping the same diffusion coefficient in the clay balls (D2 = 7.345  10 -7 cm 2 /s). The fitting quality is ensured by statistical criterions (see Tran Ngoc 2008). The Ddisp in the saturated (Test 1) and unsaturated (Test 2) experiments were of 2.713  10 -4 and 2.374  10 -4 cm 2 /s, respectively. Equation 9 can be applied for estimating the dispersivity of the physical double-porosity soil, regarding the Peclet number of the order of 1, calculated using the period size and the velocity and the dispersion coefficient in sand. (Pe = 2.8 and 1.8 for Test 1 and Test 2, respectively). We found the dispersivity l of 0.46 and 0.69 cm for the saturated (Test 1) and unsaturated (Test 2) double-porosity soil, respectively. Given that the unsaturated flow condition was the in Test 2 as in Test 3 and 4, the same dispersivity l = 0.69 cm used in the numerical simulations reproduced very well the experimental BTC of Test 3 and 4 (Figure 7). It is very interesting that this obtained dispersivity can be called intrinsic, because it does not depend on different boundary conditions (step-like and pulse-like transport) and macroscopic medium scales (different heights of the double-porosity soil, see Table 2) [START_REF] Zhou | Solute transport in porous media: Scale effects[END_REF]. To the best of our knowledge, for the first time, the intrinsic dispersivity parameter was found for an unsaturated physical double-porosity soil (of this study) at a given saturation degree, by a rigorous methodology.

The dispersivities of the physical double-porosity soil, of the numerical double-porosity soil, as well as of the simple-porosity soil (sand in the experiment of [START_REF] Sato | Solute dispersion in a variably saturated sand[END_REF] at the intermediary values and close to the saturation, are reported in Figure 8. The dispersivity in both physical and numerical double-porosity soils is larger than the one in simple-porosity soil (sand), because of the non-uniform saturation distribution that leads to a greater variation of pore velocity (Figure 6). Note that the dispersivity of 0.4 cm for the saturated Hostun sand could be estimated using a correlation with its d50 and Cu [START_REF] Xu | Statistical analysis of the relationships between dispersivity and other physical properties of porous media[END_REF]. This value is at the same order of magnitude of the fitted value from the BTC of the dispersion test in the Hostun sand (not presented here) (Tran Ngoc 2008). We observed that for the doubleporosity soils, the dispersivity increases with the decrease of the saturation degrees. This trend is in agreement with the findings of the previous works in the literature. We observed also, for the saturation degree values close to the saturated condition, the dispersivity is the same order of magnitude of the heterogeneity size in the doubleporosity soil (diameter of the clay inclusion), whereas the same order of magnitude of the grain size in the simpleporosity soil [START_REF] Ujfaludi | Determination of dispersion coefficients in soils using their pore size distribution[END_REF]Haga et al. 1999;[START_REF] Illangasekare | Dispersion and mass transfer coefficients in groundwater of near-surface geologic formations, Handbook of Chemical Mass Transport in the Environment[END_REF].

Figure 8. Dispersivity as a function of the water saturation degrees in the sand dispersion experiment of [START_REF] Sato | Solute dispersion in a variably saturated sand[END_REF]; in the double-porosity numerical dispersion experiment; and in the double-porosity physical dispersion experiment.

CONCLUSIONS

We estimated the dispersivity parameter of the doubleporosity soil, fitting the BTCs of the 1D dispersion experiments by the application of an appropriate doubleporosity model. These experiments were carried out under saturated and unsaturated conditions with the control of the local water content measured by a nondestructive gamma-ray technique. The experimental results allowed to affirm the existence of the intrinsic dispersivity of the physical unsaturated double-porosity soil. For the high saturation values, the obtained relationship between the dispersivity and the saturation in the double-porosity soil is the same as in the simpleporosity soils presented in the literature. More experiments of dispersion for small values of doubleporosity soil saturation will be needed in order to compare with the non-monotonic function of the dispersivity versus saturation obtained in the simple-porosity soils. Finally, we believe that this study contributes to the understanding of the behavior of the dispersivity in terms of saturation and scale in heterogeneous soils.

Figure 2 .Figure 3 .

 23 Figure 2. Pore size distribution obtained by mercury injection and grain size distribution of the Hostun HN38 sand measured by laser granulometry, classifying the soil as SP (poorly graded sand) according to the USCS classification. (Cu and Cc are the coefficients of uniformity and curvature.)

Figure 4 .

 4 Figure 4. Periodic microstructure of the double-porosity soil used for the dispersion experiments of this study.

  Kunsat are the permeability at saturation Sw = 100% and 82%; lsat and lunsat are the dispersivity at saturation Sw = 100% and 87%, "*" value filled by this study; E and  are the Young modulus and Poisson ratio, calculated with an axial strain range of 0.0120 -0.0242; B is the bulk modulus calculated with a pressure range of 50 -400 kPa.[START_REF] Jougnot | Hydraulic conductivity of unsaturated double porosity geomaterials[END_REF][START_REF] Ngoc | Two-scale modeling of solute dispersion in unsaturated double-porosity media: Homogenization and experimental validation[END_REF][START_REF] Lewandowska | Experiments and micromechanical modelling of elastic parameters of a composite geomaterial[END_REF] 2.2 Dispersion testsThe main apparatus used for the different stages of the dispersion experiments in the double-porosity soil are briefly presented(Tran Ngoc 2008). The first stage concerns the establishment of saturated/unsaturated steady-state flow using a peristaltic pump (Amersham Biosciences Pump P-500) for inflow rate control and a balance linked to a data logger (Campbell Scientific Ltd CR 10X) for outflow rate control. The double-porosity soil column was placed in the gamma ray mobile platform (installed in Bordeaux Mechanics and Engineering Institute) to locally measure the water content inside the column (from which the saturation degree is deduced). The NaCl tracer dispersion was launched in the final stage by switching water to tracer solution or vice-versa, according to selected boundary condition (pulse-like or stepwise-like) and initial condition (water displaced or displacing tracer solution). The evolution of tracer concentration with time (breakthrough curves -BTC) was monitored by measuring the density of the effluent by a densitometer (Anton Paar, mP 200).A series of dispersion tests were carried out in the double-porosity soil. The NaCl concentration of the tracer solution and the injection flux (therefore the Darcy velocity) were higher in the test under the saturated condition than in the tests under the unsaturated condition. For the pulse-like test, the salt tracer solution with a volume of about 1/10 total pore volume (482 cm3 ) was introduced in the medium during 4620 s. The main characteristics of the 4 dispersion tests are reported in Table2. Tests 2, 3 and 4 presented in[START_REF] Ngoc | Two-scale modeling of solute dispersion in unsaturated double-porosity media: Homogenization and experimental validation[END_REF] for validating a theoretical transport model are again used in this study for investigating a relation between the dispersivity and saturation.2.3 Dispersivity determination of the double-porosity soilWe use the dispersionconvection model obtained by applying asymptotic homogenization technique[START_REF] Auriault | Heterogeneous medium. Is an equivalent macroscopic description possible?[END_REF] to reproduce the dispersion tests in the double-

Figure 5 .

 5 Figure 5. Double-porosity simple cubic period of the numerical study with length l = 2 cm and diameter d = 1 cm of clayey inclusion. Considering that the domain 1 is the sand matrix with n1 = 0.413 and w1 = 0.804 and the domain 2 is the clay with n2 = 0.350 and w2 = 0.196.This comes obviously from the presence of heterogeneities (i.e. clay balls). However, it is very hard to figure out the water re-distribution induced by the heterogeneities, in spite of using the gamma ray attenuation technique. The water content distribution can be assumed macroscopically uniform by calculating the average water content in Test 1 (water content at saturation, S  n) and Test 2 of 0.355 and 0.313 (measured values  3% of precision), respectively.

Figure 6 .

 6 Figure 6. Volumetric water content profiles measured inside the double-porosity soil column for the dispersion tests by gamma ray attenuation technique (Data of Test 1 and 2 were published in Tran Ngoc et al. 2015 and 2011, respectively).

Figure 7 .

 7 Figure 7. Experimental breakthrough curves in the double-porosity soils under different boundary conditions versus the simulated ones. The dispersivities were fitted by using the double-porosity model. (The experiment and simulation curve data of Test 2, 3 and 4 were published in Tran Ngoc et al. 2011).

Table 2 .

 2 Experimental conditions of the dispersion tests in the double-porosity soil.

	Test	L [cm]	Sw [%]	q [cm/s]	Ci [g/l]	CL [g/l]
	1	50.3	100	5.90e-4	20	0
	2	51.0	88	3.44e-4	0	5
	3	46.9	-	3.44e-4	0	5
	4	46.9	-	3.44e-4	0	5*

ACKNOWLEDGMENTS

The experiments presented here were previously conducted in the framework of Tran Ngoc TD's PhD thesis, supervised by Prof. Jolanta Lewandowska. This research is funded by Vietnam National Foundation for Science and Technology Development (NAFOSTED) under grant number 107. 01-2015.25.