Davide Sangiorgi

Equations, contractions, and unique solutions

Keywords: F.3.1 [Logics and Meaning of Programs]: Specifying and Verifying and Reasoning about Programs-logics of programs, F.3.2 [Logics and Meaning of Programs]: Semantics of Programming Languages-operational semantics Bisimulation, Coinduction, Equations, Unique solution, Contraction

come

Equations, contractions, and unique solutions

Introduction

Bisimilarity is employed to define behavioural equivalences and reason about them. Originated in concurrency theory, bisimilarity is now widely used also in other areas, as well as outside Computer Science.

In this paper, behavioural equivalences, hence also bisimilarity, are meant to be weak because they abstract from internal moves of terms, as opposed to the strong ones, which make no distinctions between the internal moves and the external ones (i.e., the interactions with the environment). Weak equivalences are, practically, the most relevant ones: e.g., two equal programs may produce the same result with different numbers of evaluation steps.

[Copyright notice will appear here once 'preprint' option is removed.] In proofs of bisimilarity results, the bisimulation proof method has become predominant, particularly with the enhancements of the method provided by the so called 'up-to techniques' [START_REF] Pous | Enhancements of the bisimulation proof method[END_REF]. Among these, one of the most powerful ones is 'up-to expansion and context', whereby the derivatives of two terms can be rewritten using expansion and bisimilarity and then a common context can be erased. Forms of 'bisimulations up-to context' have been shown to be effective in various fields, including process calculi [START_REF] Piérard | Sound bisimulations for higherorder distributed process calculus[END_REF][START_REF] Pous | Enhancements of the bisimulation proof method[END_REF][START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF], λ-calculi [START_REF] Koutavas | Small bisimulations for reasoning about higher-order imperative programs[END_REF][START_REF] Lassen | Relational reasoning about contexts[END_REF][START_REF] Lassen | Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context[END_REF][START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF], and automata [START_REF] Bonchi | Checking nfa equivalence with bisimulations up to congruence[END_REF][START_REF] Rot | Coinductive proof techniques for language equivalence[END_REF].

The landmark document for bisimilarity is Milner's CCS book [START_REF] Milner | Communication and Concurrency[END_REF]. In the book, Milner carefully explains that the bisimulation proof method is not supposed to be the only method for reasoning about bisimilarity. Indeed, various interesting examples in the book are handled using other techniques, notably unique solution of equations, whereby two tuples of processes are componentwise bisimilar if they are solutions of the same system of equations. This method is important in verification techniques and tools based on algebraic reasoning [START_REF] Baeten | Process Algebra: Equational Theories of Communicating Processes[END_REF][START_REF] Roscoe | The theory and practice of concurrency[END_REF][START_REF] Roscoe | Understanding Concurrent Systems[END_REF]].

Milner's theorem that guarantees unique solutions [START_REF] Milner | Communication and Concurrency[END_REF] has however limitations: the equations must be 'guarded and sequential', that is, the variables of the equations may only be used underneath a visible prefix and preceded, in the syntax tree, only by the sum and prefix operators. This limits the expressiveness of the technique (since occurrences of other operators above the variables, such as parallel composition and restriction, in general cannot be removed), and its transport onto other languages (e.g., languages for distributed systems or higher-order languages, which usually do not include the sum operator).

In this paper we propose a refinement of Milner's technique in which equations are replaced by special inequations called contractions. Intuitively, for a behavioural equivalence , its contraction is a preorder in which P Q holds if P Q and, in addition, Q has the possibility of being as efficient as P . That is, Q is capable of simulating P by performing less internal work. It is sufficient that Q has one 'efficient' path; Q could also have other paths, that are slower than any path in P . Uniqueness of the solution of a system of contractions is defined as with systems of equations: any two solutions must be equivalent with respect to . The difference with equations is in the meaning of solution: in the case of contractions the solution is evaluated with respect to the preorder , rather than the equivalence .

If a system of equations has a unique solution, then the corresponding system of contractions, obtained by replacing the equation symbol with the contraction symbol, has a unique solution too. The converse however is false: it may be that only the system of contractions has a unique solution. More important, the condition that guarantees a unique solution in Milner's theorem about equations can be relaxed: 'sequentiality' is not required, and 'guardedness' can be replaced by 'weak guardedness', that is, the variables of the contractions can be underneath any prefix, including a prefix representing internal work. (This is the same constraint in Milner's 'unique solution of equations' theorem for strong bisimilarity; the constraint is unsound for equations on weak bisimilarity.)

We show that Milner's theorem is not complete for pure equations (equations in which recursion is only expressible through the variables of the equations, without using the recursion construct of the process language): there are bisimilar processes that cannot be solutions to the same system of guarded and sequential pure equations. In contrast, completeness holds for weakly-guarded pure contractions. The contraction technique is also computationally complete: any bisimulation R can be transformed into an equivalent system of weakly-guarded contractions that has the same size of R (where the size of a relation is the number of its pairs, and the size of a system of contractions is the number of its contractions). An analogous result also holds with respect to bisimulation enhancements such as 'bisimulation up-to expansion and context'. The contraction technique is in fact computationally equivalent to the 'bisimulation up-to contraction and context' technique -a refinement of 'bisimulation up-to expansion and context'.

The contraction technique can be generalised to languages whose syntax is the term algebra derived from some signature, and whose semantics is given as an LTS. In this generalisation the weak-guardedness condition for contractions becomes a requirement of autonomy, essentially saying that the processes that replace the variables of a contraction do not contribute to the initial action of the resulting expression. The technique can also be transported onto other equivalences, including contextually-defined equivalences such as barbed congruence, and non-coinductive equivalences such as contextual equivalence (i.e., may testing) and trace equivalence [START_REF] De Nicola | Testing equivalences for processes[END_REF][START_REF] Van Glabbeek | The linear time-branching time spectrum II[END_REF][START_REF] Morris | Lambda-Calculus Models of Programming Languages[END_REF]. For each equivalence, one defines its contraction preorder by controlling the amount of internal work performed.

Finally, we show that a contraction preorder can be injected into the bisimulation game. That is, given an equivalence and its contraction preorder , we can define the technique of 'bisimulation up-to and context' whereby, in the bisimulation game, the derivatives of the two processes can be manipulated with and (similarly to the manipulations that are possible in the standard 'bisimulation up-to expansion and context' using the expansion relation and bisimilarity) and a common context can then be erased. The resulting 'bisimulation up-to and context' is sound for . This technique allows us to derive results for using the (enhanced) bisimulation proof method.

The contraction technique cannot however be transported onto all (weak) behavioural equivalences. For instance, it does not work in the setting of infinitary trace equivalence (whereby two processes are equal if they have the same finite and infinite traces), and must testing [START_REF] De Nicola | Testing equivalences for processes[END_REF]. A discussion on this point is deferred to the concluding section.

We conclude the paper with an example of application of contractions to a higher-order language, which exploits the autonomy condition.

Structure of the paper All background material is reported in Section 2. Contractions and their properties are introduced in Section 3, for bisimilarity and the CCS language. The extension to languages defined from a generic signature is presented in Section 4. The transport of contractions onto other behavioural equivalences is discussed in Sections 5 (barbed congruence), 6 (contextual equivalence), 7 (trace equivalence), and 8 (non-applicability to certain equivalences). The injection of contractions into the bisimulation game is described in Section 9. The example with higher-order languages is reported in Section 10.

Background

CCS

We assume an infinite set of names a, b, . . . and a set of constant identifiers (or simply constants) for writing recursive processes. The special symbol τ does not occur in the names and in the constants. The class of the CCS processes is built from the operators of parallel composition, guarded sum, restriction, and constants, and the guard of a sum can be an input, an output, or a silent prefix:

P := P1 | P2 | Σi∈I µi. Pi | νa P | K µ := a | a | τ
where I is a countable indexing set. Sums are guarded so to ensure that behavioural equivalences and preorders are substitutive. We write 0 when I is empty, and P + Q for binary sums, with the understanding that, to fit the above grammar, P and Q should be sums of prefixed terms. Each constant K has a definition K = P . We sometimes omit trailing 0, e.g., writing a | b for a. 0 | b. 0 . We write µ n . P for P preceded by n µ-prefixes. In a few examples we write !µ. P as abbreviation for the constant Kµ.P = µ. (P | Kµ.P ). The operational semantics is given by means of an LTS, and is reported in Figure 1 (the symmetric version of the two rules for parallel composition has been omitted). The immediate derivatives of a process P are the elements of the set {P | P µ -→ P for some µ }. We use to range over visible actions (i.e., inputs or outputs, excluding τ ).

Some standard notations for transitions: =⇒ is the reflexive and transitive closure of Further notations Letters R, S range over relations. We use infix notation for relations, e.g., P R Q means that (P, Q) ∈ R. We use a tilde to denote a tuple, with countably many elements; thus the tuple may also be infinite. All notations are extended to tuples componentwise; e.g., P R Q means that Pi R Qi, for each component i of the tuples P and Q. And C[ P ] is the process obtained by replacing each hole [•]i of the context C with Pi. We write R c for the closure of a relation under contexts. Thus P R c Q means that there are a context C and tuples P , Q with

P = C[ P ], Q = C[ Q] and P R Q. We use symbol def = for abbreviations. For instance, P def = G,
where G is some expression, means that P stands for the expression G (in contrast, symbol = is used for the definition of constants, whereas = is used for syntactic equality and for equations). If ≤ is a preorder, then ≥ is its inverse (and conversely).

Bisimilarity and expansion

We focus on weak behavioural equivalences, which abstract from the number of internal steps performed.

DEFINITION 2.1 (bisimilarity).

A process relation R is a bisimulation if, whenever P R Q, we have:

1. P µ -→ P implies that there is Q such that Q µ = ⇒ Q and P R Q ; 2. the converse of (1) on the actions from Q. Σi∈I µi. Pi µ i --→ Pi P µ -→ P P | Q µ -→ P | Q P a -→ P Q a -→ Q P | Q τ -→ P | Q P µ -→ P νa P µ -→ νa P µ = a, a P µ -→ P K µ -→ P if K = P Figure 1. The LTS for CCS P and Q are bisimilar, written P ≈ Q, if P R Q for some bisimulation R. 2
We sometimes call bisimilarity weak bisimilarity, to distinguish it from strong bisimilarity, ∼, obtained by replacing in the above definition the weak answer

Q µ = ⇒ Q with the strong Q µ -→ Q .
The bisimulation proof method can be enhanced by means of up-to techniques. One of the most useful auxiliary relations in up-to techniques is the expansion relation e [START_REF] Sangiorgi | The problem of "Weak Bisimulation up to[END_REF]. This is an asymmetric version of ≈ where P e Q means that P ≈ Q, but also that Q achieves the same as P with no more work, i.e. with no more τ actions. Intuitively, if P e Q, we can think of Q as being at least as fast as P or, more generally, we can think that P uses at least as many resources as Q.

DEFINITION 2.2 (expansion).

A process relation R is an expansion if, whenever P R Q,

1. P µ -→ P implies that there is Q with Q µ -→ Q and P R Q ; 2. Q µ -→ Q implies that there is P with P µ = ⇒ P and P R Q . P expands Q, written P e Q, if P R Q, for some expansion R.
Relation e is studied -using a different terminology -by Arun-Kumar and Hennessy [START_REF] Arun-Kumar | An efficiency preorder for processes[END_REF]: they show that e is a mathematically tractable preorder and has a complete proof system for finite terms based on a modification of the standard τ laws for CCS. In CCS, strong and weak bisimilarity are congruence relations, and expansion is a precongruence. It holds that ∼ ⊆ e and e ⊆ ≈; moreover each inclusion is strict. The inclusions are obvious. For the strictness, we have that P ∼ τ . P , P e τ . P , and τ . P e P , τ . P ≈ P .

A powerful up-to technique is 'bisimulation up-to e and context'. It combines 'up-to expansion' (the possibility of rewriting the derivatives of two related processes using e and ≈), with 'up-to context' (the possibility of removing a common context from the derivatives). We recall that R c is the context closure of R.

DEFINITION 2.3 (bisimulation up-to e and context).

A process relation R is a bisimulation up-to e and context if, whenever P R Q, we have:

1. P µ -→ P implies that there is Q with Q µ = ⇒ Q and P e R c ≈ Q ; 2.
the converse of (1) on the actions from Q.

The occurrence of e on the left of R c cannot be replaced by ≈, as this would break the soundness of the technique [START_REF] Pous | Enhancements of the bisimulation proof method[END_REF]. The technique is sound [START_REF] Sangiorgi | Locality and True-concurrency in Calculi for Mobile Processes[END_REF]: LEMMA 2.4 (soundness of bisimulation up-to e and context). If R is a bisimulation up-to e and context, then R ⊆ ≈.

An example

In examples in the paper, we sometimes use a version of CCS with value passing; this could be translated into pure CCS [START_REF] Milner | Communication and Concurrency[END_REF], but having explicit value passing improves readability. In a value-passing calculus, a(x). P is an input at a in which x is the placeholder for the value received, whereas a n . P is an output at a of the value n; and A n is a parametrised constant. The following example illustrates 'bisimulation up-to e and context', and will then be used for comparison with other techniques.

We wish to implement a server that, when interrogated by clients at a channel c, starts a certain interaction protocol with the client, after consulting an auxiliary server A at a. Here the auxiliary server A is deterministic: at every cycle it outputs an integer value, which changes with the cycle (this change is represented by the successor function, for simplicity).

We consider two implementations of the server. The difference between them is that the first server, L, is lazy, and consults A only after a request from a client has been received. In contrast, the other server, E, consults A beforehand so to be then ready in answering a client:

L = c(z). a(x). (L | R c, x, z ) E = a(x). c(z). (E | R c, x, z ) A n = a n . A n + 1
Here R c, x, z represents the interaction protocol that is started with a client, and can be any process. It may use the values x and z (obtained from the client and the auxiliary server A); the interactions produced may actually depend on the values x and z. Process R c, x, z may also use channel c, and therefore trigger further interactions with the main server; in contrast, R c, x, z may not use a (i.e., it may not interrogate the auxiliary server). We use the 'bisimulation up-to expansion and context' technique to prove that the composition of the two servers with A yields bisimilar lazy and eager systems:

LS n def = νa (A n | L) ES n def = νa (A n | E) Relation R def = ∪n{(LS n , ES n )}
is a bisimulation up-to expansion and context. Consider a pair (LS n , ES n ). The two processes have one initial transition; the most interesting case is the challenge transition from ES n , and we only consider this one. We have

ES n τ -→ νa (A n + 1 | c(z). (E | R c, n, z )) def = E
Process LS n may not produce internal steps, hence its only possible answer is

LS n =⇒ LS n

We can now perform some algebraic manipulations of E : first, we employ CCS expansion law to pull out the prefix at c, then a structural law to resize the scope of the restriction at a in which we exploit the property that R c, n, z may not use a. (All these laws are valid for strong bisimilarity, hence also for expansion.) We thus obtain:

E e c(z). (νa (A n + 1 | E) | R c, n, z ) = c(z). (ES n + 1 | R c, n, z ) def = E
We can act similarly on LS n , and in addition also employing the law

νa (a(y). P | a v . Q) ≈ νa (P { v /y} | Q) (1)
This gives us:

LS n ≈ c(z). (νa (A n + 1 | L) | R c, n, z ) = c(z). (LS n + 1 | R c, n, z ) def = L
We have thus obtained two processes, E and L , in the context closure of R, and we are done.

In the proof, the 'up-to' techniques allow us to work with a relation that has exactly one pair for each integer. Specifically, 'upto context' avoids us considering processes in parallel with the lazy and eager systems, whereas 'up-to expansion' allows us to reason only on the 'normal forms' LS n and ES n for these systems.

Systems of equations

Uniqueness of solutions of equations [START_REF] Milner | Communication and Concurrency[END_REF] intuitively says that if a context C obeys certain conditions, then all processes P that satisfy the equation P ≈ C[P ] are bisimilar with each other.

We need variables to write equations. We use capital letters X, Y, Z for these variables and call them equation variables. The body of an equation is a CCS expression possibly containing equation variables. Thus such expressions, ranged over by E, live in a CCS grammar extended with equation variables. DEFINITION 2.5. Assume that, for each i of a countable indexing set I, we have variables Xi, and expressions Ei possibly containing such variables. Then {Xi = Ei}i∈I is a system of equations. (There is one equation for each variable Xi.)

We write E[ P ] for the expression resulting from E by replacing each variable Xi with the process Pi, assuming P and X have the same length. (This is syntactic replacement, akin to the substitution of the holes of a context with processes.) The components of P need not be different from each other, as it must be for the variables X. If the system has infinitely many equations, the tuples P and X are infinite too. DEFINITION 2.6. Suppose {Xi = Ei}i∈I is a system of equations:

• P is a solution of the system of equations for ≈ if for each i it holds that Pi ≈ Ei[ P ].

• the system has a unique solution for ≈ if whenever P and Q are both solutions for ≈, then P ≈ Q.

Examples of systems with a unique solution for ≈ are:

1. X = a. X 2. X1 = a. X2, X2 = b. X1
The unique solution of the system (1), modulo ≈, is the constant K = a. K: for any other solution P we have P ≈ K. The unique solution of (2), modulo ≈, are the constants K1, K2 with K1 = a. K2 and K2 = b. K1; again, for any other pair of solutions P1, P2 we have K1 ≈ P1 and K2 ≈ P2. Examples of systems that do not have unique solution are:

1. X = X 2. X = τ . X 3. X = a | X
All processes are solutions of ( 1) and ( 2); examples of solutions for

(3) are K and K | b, for K = a. K.

DEFINITION 2.7. A system of equations {Xi = Ei}i∈I is

• guarded if, in each Ei, each occurrence of an equation variable is underneath a visible prefix; • sequential if, in each Ei, each occurrence of an equation variable only appears underneath prefixes and sums.

In other words, if the system is sequential, then for every expression Ei, any subexpression of Ei in which Xj appears, apart from Xj itself, is a sum (of prefixed terms). For instance,

• X = τ . X + µ. 0 is sequential but not guarded, because the guarding prefix for the variable is not visible. • X = . X | P is guarded but not sequential.

• X = . X + τ . νa (a. b | a. 0), as well as X = τ . (a. X + τ . b. X + τ ) are both guarded and sequential.

THEOREM 2.8 (unique solution of equations, [START_REF] Milner | Communication and Concurrency[END_REF]). A system of guarded and sequential equations has a unique solution for ≈.

The proof exploits an invariance property on immediate transitions for guarded and sequential expressions, and then extracts a bisimulation (up-to bisimilarity) out of the solutions of the system.

To see the need of the sequentiality condition, consider the equation (from [START_REF] Milner | Communication and Concurrency[END_REF])

X = νa (a. X | a)
where X is guarded but not sequential. Any processes that does not use a is a solution.

Contractions

In Theorem 2.8 the constraints on guardedness and, especially, on sequentiality limit its applicability. Further, the same definitions and examples discussed for bisimilarity (and hence also the same limitations) apply to other behavioural equivalences; e.g., contextual equivalence and trace-based equivalences.

One may wonder if the conditions of Theorem 2.8 can be relaxed by simply requiring that each equation be sequentially guarded, that is, of the form X = Σj j . Ej (where j is a visible action). Unfortunately, uniqueness still fails; a counterexample is X = a. νa (a | X) .

Any process P with P ≈ a. P , and P unable to use a, is a solution. Examples are a. 0 and a. b. 0.

An equation X = a. E need not have a unique solution even if we confine ourselves to processes that may only perform a transitions. An example is the equation

X = a. νb (νa (a. !a. b | X) | !b. a) .
Here the body of the equation produces an a, cancels the first a from X and then reproduces all other a's. Any process P with P ≈ a. P for some P , is a solution; for instance, a. 0 or a. a. 0 or even !a. 0.

Contraction preorders

The constraints on the unique-solution Theorem 2.8 can be weakened if we move from equations to certain inequations that we call contractions.

Intuitively, for a behavioural equivalence , its contraction is a preorder in which P Q holds if P Q and, in addition, Q has the possibility of being at least as efficient as P . That is, if P can do some work (i.e., some interactions with its environment), then Q should be able to do the same work at least as quickly as P (i.e., performing no more τ -steps then those performed by P ). Process Q, however, may be nondeterministic and may have other ways of doing the same work, and these could be slow (i.e., involving more τ -steps than those performed by P ). We first explain the idea on the concrete case of bisimilarity.

DEFINITION 3.1 (bisimulation contraction).

A process relation R is a bisimulation contraction if, whenever P R Q,

1. P µ -→ P implies there is Q such that Q µ -→ Q and P R Q ; 2. Q µ -→ Q implies there is P such that P µ = ⇒ P and P ≈ Q .
Bisimilarity contraction, written bis , is the union of all bisimulation contractions.

In the first clause Q is required to match P 's challenge transition with at most one transition. This makes sure that Q is capable of mimicking P 's work at least as efficiently as P . In contrast, the second clause of Definition 3.1, on the challenges from Q, entirely ignores efficiency: it is the same clause of weak bisimulation -the final derivatives are even required to be related by ≈, rather than by R.

Bisimilarity contraction is coarser than the expansion relation e of Definition 2.2. Clause (1) is the same in the two definitions. But in clause (2) expansion uses P µ = ⇒ P , rather than P µ = ⇒ P ; moreover with contraction the final derivatives are simply required to be bisimilar. An expansion P e Q tells us that Q is always more efficient than P , whereas the contraction P bis Q just says that Q has the possibility of being more efficient than P . EXAMPLE 3.2. We have a bis τ . a. However, a + τ . a bis a, as well as its converse, a bis a + τ . a. Indeed, if P ≈ Q then P bis P + Q. The last two relations do not hold with e, which explains the strictness of the inclusion e ⊆ bis .

2

As bisimilarity contraction follows expansion in one direction and bisimilarity in the other, clearly separating the two, the precongruence and congruence for such relations can be combined into a precongruence proof for the contraction. THEOREM 3.3. bis is a precongruence in CCS.

Systems of contractions

A system of contractions is defined as a system of equations, except that the contraction symbol is used in the place of the equality symbol =. Thus a system of contractions is a set {Xi Ei}i∈I where I is an indexing set and expressions Ei may contain the contraction variables {Xi}i∈I . DEFINITION 3.4. Given a behavioural equivalence and its contraction , and a system of contractions {Xi Ei}i∈I , we say that:

• P is a solution for of the system of contractions if P E[ P ];

• the system has a unique solution for if whenever P and Q are both solutions for then P Q.

When we reason about bisimilarity, the contraction symbol is interpreted as the bisimilarity contraction bis , and the equivalence as the bisimilarity ≈. Thus P solution for bis of the system of contractions {Xi

Ei}i∈I means that P bis E[ P ]; and the system having a unique solution for ≈ means that whenever P and Q are both solutions for bis then P ≈ Q. LEMMA 3.5. If a system of equations {Xi = Ei}i∈I has a unique solution for ≈, then also the corresponding system of contractions {Xi Ei}i∈I has a unique solution for ≈.

The lemma holds because any system of equations has at least one solution for strong bisimilarity, obtained by interpreting the equations as recursive process definitions. A solution for strong bisimilarity is also a solution in the system of contractions. Moreover, any solution of the system of contractions is a solution of the system of equations. (The converse, in contrast, is false: as we shall see, systems of contractions more easily have a unique solution.) 3.3 Conditions for unique solution of contractions DEFINITION 3.6. A system of contractions {Xi Ei}i∈I is weakly guarded if, in each Ei, each occurrence of a contraction variable is underneath a prefix.

In proofs about weakly-guarded contractions we will often unfold the contractions, exploiting the substitutivity of the contraction preorder, with the objective of placing processes that are solutions of the contractions underneath a certain number of prefixes. Suppose P are solutions of a system of contractions {Xi LEMMA 3.7. Suppose P and Q are solutions for ≈ of a system of weakly-guarded contractions. For any context C, if

C[ P ] µ = ⇒ R, then there is a context C such that R bis C [ P ] and C[Q] µ = ⇒≈ C [ Q].
C such that C [ P ] µ = ⇒ C [ P ] bis R and C [ Q] µ = ⇒ C [ Q]. Finally, again applying the definition of bis on C[ Q] bis C [ Q], we derive C[ Q] µ = ⇒≈ C [ Q]. 2
THEOREM 3.8 (unique solution of contractions for ≈). A system of weakly-guarded contractions has a unique solution for ≈.

Proof [Sketch] One shows that if P and Q are solutions for ≈ of a system of weakly-guarded contractions, then the relation

R def = {(R, S) | R ≈ C[ P ], S ≈ C[ Q] for some context C} .
is a bisimulation, exploiting Lemma 3.7. 2

In comparison to Theorem 2.8 for equations, in Theorem 3.8 for contractions the 'guardedness' condition is weakened, allowing variables that are underneath τ prefixes; most important, the sequentiality condition is removed, allowing variables underneath any process constructs. EXAMPLE 3.9. The following contractions have a unique solution for ≈:

1. X τ . X 2. X a. νa (a | X)) 3. X a. νb (νa (a. !a. b | X) | !b. a)
We have seen in Section 2.4 and at the beginning of Section 3 that the corresponding equations do not have a unique solution. The solutions of the contraction (1) are all inactive processes, where a process is inactive if it cannot perform visible actions (i.e., if P is the process, then there is no P and visible action such that P =⇒ P -→). The contraction has a unique solution because all inactive processes are bisimilar. It is easy to see that an inactive process is solution. Conversely, suppose P is not inactive, and let n be the least n ≥ 0 such that P ( τ -→) n -→ for some ; then P is not a solution of P τ . P because τ . P needs at least n + 1 τsteps before exhibiting any visible action, and therefore can never be more efficient than P . Example of solutions for (2) and (3) are a. P and τ . a. P , where P is inactive. Any solution of ( 2) and ( 3) is bisimilar with a. 0. 2 REMARK 3.10. Results such as Lemma 3.7 and Theorem 3.8 also hold if the game played in clause (1) of Definition 3.1 of bisimulation contraction is that of strong simulation (i.e., "P µ -→ P implies there is Q such that Q µ -→ Q and P R Q "). However, the resulting relation would not be coarse enough to capture expansiona major goal for this paper is understanding existing 'bisimilarity up-to' techniques, where expansion is important. 2

Completeness

An interesting class of contractions are those in which the body E of each contraction X E does not contain constants. In these systems, all forms of infinity in the behaviour of processes are captured by recursive calls through the contraction variables. We call such systems pure. Similarly we call pure a system of equations without constants. In this section we discuss the expressiveness of pure systems of contractions and equations. (With constants the question is vacuous, as the behaviour of any process P is captured by the guarded and sequential equation X = P .) We show that the technique of weakly-guarded contractions given by Theorem 3.8 is complete, whereas that of guarded and sequential equations given by Theorem 2.8 is not.

If R is a relation then we can also view R as an ordered sequence of pairs (e.g., assuming some lexicographical ordering). Then Ri indicates the tuple obtained by projecting the pairs in R on the i-th component (i = 1, 2). THEOREM 3.11 (completeness). Suppose R is a bisimulation. Then there is a system of weakly-guarded pure contractions of which R1 and R2 are solutions for bis .

Proof [Sketch] Suppose R is a bisimulation. We define a system of contractions of which R1 and R2 are solutions. The variables of the contractions are of the form XP,Q for P R Q, and there is one contraction for each pair in R.

We show how the contraction for a pair P R Q is built. Consider an enumeration of all the transitions from P : The contractions in the proof of the theorem are sequential and weakly guarded, but not necessarily guarded. The assertion of Theorem 3.11 can actually be refined: the technique based on weakly-guarded contractions is also computationally complete with respect to the bisimulation proof method, in the sense that the size of the structures needed and the subsequent amount of checks are comparable. The size of a relation is the number of its pairs. The size of a system of contractions is the number of contractions. The proof of Theorem 3.11 shows that the system of contractions derived from a bisimulation R has the same size as R; moreover, the work needed to prove that R1 and R2 are solutions of the system of contractions is precisely the work needed to check the challenge/response diagrams of the bisimulation game for R.

In contrast, the method for equations resulting from Theorem 2.8 is not complete. For instance, there is no system of guarded and sequential pure equations in which one of the solutions is the process K so defined:

K = τ . (a | K) + τ . 0 .
To see this, it is useful to express the behaviour of K via the following constants:

H0 = τ . H1 + τ Hi = τ . Hi+1 + a. Hi-1 + τ . a i (i > 0)
We have a i | K ≈ Hi, for each i, as witnessed by the relation

R def = ∪ i≥0 {(a i | K, Hi)} ,
which is a bisimulation up-to strong bisimilarity. Now, for each n = m, we have Hn ≈ Hm (because, assuming n < m, Hm cannot match the transition Hn τ -→ a n ); moreover, for each n there is a transition Hn τ -→ Hn+1. As a consequence, the infinite sequence of transitions

H0 τ -→ H1 τ -→ • • • Hn τ -→ Hn+1 τ -→ • • • (2)
go through states that are pairwise non-bisimilar. An equation of which K is solution should be able to express the same behaviour. This is impossible, however, if the equation is sequential and guarded, because the equation variables must be underneath a visible prefix, and can only be reached by performing a visible action. Hence an infinite nesting of internal transitions as in (2) cannot be derived.

Relationship with up-to context

The completeness of the contraction technique given by Theorem 3.11, including the computational completeness discussed after the theorem, remains also with respect to powerful enhancements of the bisimulation proof method such as 'up-to context' techniques.

We show that the contraction technique is in fact computationally equivalent to the 'up-to bis and context' technique, a refinement of the 'up-to expansion and context' of Definition 2.3 (the former captures a larger set of relations because bisimilarity contraction is coarser than expansion). DEFINITION 3.12 (bisimulation up-to bis and context). A process relation R is a bisimulation up-to bis and context if, whenever P R Q, we have:

1. P µ -→ P implies there is Q such that Q µ = ⇒ Q and P bis R c ≈ Q 2.
the converse of (1) on the actions from Q. THEOREM 3.13. Suppose R is a bisimulation up-to bis and context. Then there is a system of weakly-guarded contractions, of the same size as R, of which R1 and R2 are solutions for bis .

Conversely, suppose P and Q are solutions for bis to the same system of weakly-guarded contractions. Then the relation {(Pi, Qi)}i is a bisimulation up-to bis and context.

The theorem is proved along the lines of Theorem 3.11. REMARK 3.14. The definition of contraction was derived by attempts at obtaining theorems such as 3.11 and 3.13. The constructions in the theorems do not work with expansion in place of bisimilarity contraction.

2

From Theorems 3.13 and 3.8 we derive: COROLLARY 3.15. (soundness of 'bisimulation up-to bis and context'). If R is a bisimulation up-to bis and context, then R ⊆ ≈.

Having shown that the techniques of weakly-guarded contractions and 'bisimulation up-to bis and context' are equivalent, we can derive the soundness of one from the soundness of the other (in Corollary 3.15 we took the contraction technique as primitive). The complexity of the soundness proofs of the two techniques is similar. The main difference is that the expressions in the body of the contractions are weakly guarded, whereas the contexts of the 'up-to context' bisimulation techniques are not. As a consequence, in the proofs for the 'up-to context' techniques one has to reason about all possible interactions between a context and the processes plugged into it, proceeding by transition induction and a case analysis on the last rule used to derive a transition. With contractions this is avoided, exploiting the weak-guardedness condition and the unfolding of the contractions.

Example: the lazy and eager servers

We show a proof of the bisimilarity between the lazy and the eager systems of Section 2.3 using the technique of unique solution of contractions. This serves both as an an illustration of the application of the technique, and as a comparison with the technique based on the bisimulation proof method employed in the proof of Section 2.3.

The proof consists in showing that {LS n }n and {ES n }n are solutions of the following system of contractions:

{Xn c(z). (Xn+1 | R c, n, z )}n (3)
We establish that {ES n }n is a solution using the algebraic laws in the proof in Section 2.3 (noticing that in (1) ≈ can be replaced by bis ):

ES n bis νa (A n + 1 | c(z). (E | R c, n, z )) ∼ c(z). (νa (A n + 1 | E) | R c, n, z ) = c(z). (ES n + 1 | R c, n, z ) .
We proceed similarly for LS n . The contraction (3) is not sequential, hence contractions and Theorem 3.8 cannot be replaced by equations and Theorem 2.8.

Language generalisation

We have shown the property of unique solution of weakly-guarded contractions in CCS. We generalise here the theorem to an arbitrary process language, using a more abstract condition. The generalisation serves both to better understand the validity of the theorem, and for applicability to languages that, unlike CCS, do not have an explicit prefixing construct.

For this generalisation we consider the case -standard in process algebra -in which the syntax of the processes is the term algebra generated by some signature, and the semantics is given as an LTS. We call process language any such language. We use L to denote a generic process language, and L(X ) for its extension with the contraction variables in X . We say that L is ≈-safe if, in L, ≈ is a congruence relation, and its corresponding contraction bis is a precongruence.

In Theorem 3.8, the 'weakly guarded' hypothesis makes sure that the body of a contraction alone determines the first interaction. The body is thus autonomous: the interaction occurs without contributions from the terms that replace the contraction variables. Whenever the bodies of the contractions are autonomous in this sense, the unique-solution property holds. DEFINITION 4.1 (autonomous contractions). An expression E of L(X ) is autonomous if for all processes P of L we have:

• if E[ P ] µ -→ R, then there is a context C such that R = C[ P ],
and for all Q, also E

[ Q] µ -→ C[ Q].

A system of contractions {Xi

Ei}i∈I is autonomous if each expression Ei is autonomous. THEOREM 4.2. In any ≈-safe process language L, a system of autonomous contractions has a unique solution for ≈.

The proof of the theorem is similar to that of Theorem 3.8. Checking the autonomy property is often straightforward. For instance, in the case of the GSOS format [START_REF] Bloom | Bisimulation can't be traced[END_REF], autonomy holds if, in the body E of a contraction, all variables are underneath an axiom operator, that is, an operator that, as CCS prefix, is defined by means of SOS rules in which the set of hypothesis is empty.

In some cases, autonomy may be better than the weaklyguarded hypothesis even if the calculus has a prefix operator: we shall see an example in Section 10, with the Higher-Order πcalculus, where autonomy allows us to capture occurrences of the contraction variables within output prefixes.

Barbed congruence

We (briefly) consider the application of the idea of contraction to barbed congruence [START_REF] Milner | Barbed bisimulation[END_REF], for various reasons. First, barbed congruence is a contextually-defined form of behavioural equivalence, and it paves the way to the treatment of other forms of contextual equivalence. Second, we want to show that -sometimes -the contraction techniques make it possible to work directly with barbed congruence, even though it is contextually defined (e.g., the example with higher-order processes in Section 10). Third, the definition of barbed congruence applies to any language with a reduction semantics (i.e., a reduction relation and a barb, or observation, predicate), as opposed to the LTS semantics of the languages in earlier sections.

Thus the definitions and results in this section hold for any algebraic calculus (the term algebra over a signature) equipped with a reduction semantics, that is, a reduction relation -→ and a barb predicate ↓. We use RL for referring to a generic such language, and RL(X ) for its extension with the contraction variables in X . (For CCS, -→ is τ -→ and P ↓ holds if P -→, for some visible action .) As usual, =⇒ is the reflexive and transitive closure of -→; and P ⇓ holds if there is P with P =⇒ P and P ↓.

DEFINITION 5.1 (barbed bisimulation and congruence).

A relation R on the processes of RL is a barbed bisimulation if whenever P R Q:

1. P -→ P implies there is Q such that Q =⇒ Q and P R Q ; 2. P ↓ implies Q ⇓;
3. the converse of ( 1) and ( 2), on challenges from Q.

Barbed bisimilarity, written ≈ bar , is the union of all barbed bisimulations. Two processes P and Q are barbed congruent, written

P ≈ c bar Q, if for each context C, it holds that C[P ] ≈ bar C[Q]. 2
REMARK 5.2. The definitions of barbed congruence in the literature often make use of a set of barb predicates; we use only one barb here for mere simplicity of presentation. A variant of barbed congruence is reduction-closed barbed congruence [START_REF] Honda | On reduction-based process semantics[END_REF], in which the closure under contexts is placed within the definition of bisimilarity. The difference between the two variants has no consequences on the results in the paper. 2

In the 'contraction version' of barbed bisimilarity we write

Q ∧ -→ Q if Q -→ Q or Q = Q . DEFINITION 5.

(barbed contraction, barbed congruence contraction).

A relation R on the processes of RL is a barbed contraction if, whenever P R Q:

1. P -→ P implies there is Q such that Q ∧ -→ Q and P R Q ; 2. Q -→ Q implies there is P such that P =⇒ P and P ≈ bar Q ; 3. P ↓ implies Q ↓; 4. Q ↓ implies P ⇓.
Barbed contraction, written bar , is the union of all barbed contractions. Barbed congruence contraction, written c bar , relates two processes P and Q if, for each context C, it holds that

C[P ] bar C[Q].
We transport the concept of autonomy to reduction-based semantics.

DEFINITION 5.4 (reduction-autonomous contractions

). An expression E of RL(X ) is reduction-autonomous if for all processes P and context C of RL:

• if C[E[ P ]] -→ R, then there is a context C such that R = C [ P ] and, for all Q, also C[E[ Q]] -→ C [ Q]; • if C[E[ P ]] ↓ then, for all Q, also C[E[ Q]] ↓.

A system of contractions {Xi

Ei}i∈I is reduction-autonomous is each expression Ei is reduction-autonomous.

Barbed congruence and its contraction are, by definition, fully substitutive. Hence the safety requirement of Theorem 4.2 is not needed. In the property of unique solution for barbed congruence, the symbols and of Definition 3.4 become ≈ c bar and c bar , respectively. THEOREM 5.5. In RL, any system of reduction-autonomous contractions has a unique solution for ≈ c bar .

Uniqueness of solution of contractions for non-coinductive equivalences

We consider now non-coinductive equivalences. We focus on contextual equivalence [START_REF] Morris | Lambda-Calculus Models of Programming Languages[END_REF] (i.e., may testing [START_REF] De Nicola | Testing equivalences for processes[END_REF]), because it is widely studied. As the barbed congruence of Section 5, so contextual equivalence is contextually defined. Thus the setting considered is the same: an algebraic process language equipped with a reduction semantics. We reuse notations and terminologies from Section 5. Intuitively, two terms are contextually equivalent when they are equally observable, in any context. DEFINITION 6.1 (contextual equivalence). P ≈ctx Q holds when

C[P ] ⇓ iff C[Q] ⇓, for all C.
The definition of the contextual equivalence contraction uses the predicate P ⇓ n , indicating that a barb is reached in at most n steps, i.e., P ( τ -→) m P ↓, for some P , with 0 ≤ m ≤ n. DEFINITION 6.2 (contextual equivalence contraction). P ctx Q if for all C:

1. C[P ] ⇓ n implies C[Q] ⇓ n , for any n; 2. C[Q] ⇓ implies C[P ] ⇓.
Thus, referring to contextual equivalence, the symbols and of Definition 3.4 become ≈ctx and ctx. THEOREM 6.3. A system of reduction-autonomous contractions has a unique solution for ≈ctx.

Proof [Sketch] Suppose P and Q are solutions for ctx, and consider a context C. One shows that

C[ P ] ⇓ implies C[ Q] ⇓. Suppose C[ P ] ⇓ n .
One proceeds by induction on n, exploiting the properties of the unfolding of contractions. 2 COROLLARY 6.4. In CCS, a system of weakly-guarded contractions has a unique solution for ≈ctx.

Example: the lazy and eager servers, revisited

Contextual equivalence does not have the congruence problems of bisimilarity for summation that motivated, in the presentation of CCS in Section 2, the use of guarded sums. We can therefore admit the full summation construct ΣiPi in the grammar for the CCS processes. Such a flexibility will be useful in this example. We revisit the lazy and eager servers in the example of Section 2.3. We modify the auxiliary server A, which was consulted by the main server before starting an interaction protocol with a client. In Section 2.3, the server was deterministic; now it is nondeterministic. Thus all definitions remain the same except that A always returns an arbitrary integer:

A = Σn∈N a n . A
The system with the lazy main server is now

LS def = νa (A | L),
and the system with the eager main server is

ES def = νa (A | E),
where L and E are as in Section 2.3. The timing difference between LS and ES in consulting A is observable under bisimilarity. The reason is that an interaction

ES -→ νa (A | c(z). (E | R c, n, z )) ,
in which n is received from A, is a commitment to using n in the interaction with the next client. In contrast, LS is unable to make such a commitment -its only initial transition is a visible one.

The difference is however not observable under contextual equivalence. We prove LS ≈ctx ES using the technique of unique solution of weakly-guarded contractions. The proof is similar to that with the deterministic auxiliary server and the bisimilarity contraction in Section 3.6, with a further simplification: a single contraction is sufficient, namely

X c(z). Σn(X | R c, n, z ) (4)
To show that both LS and ES are solutions for ctx of this contraction, we employ the same laws and algebraic reasoning of Section 3.6 (which are sound because bisimilarity implies contextual equivalence). An additional laws is required in the proof of ES:

Σiα. Ri ctx α. ΣiRi (α is any prefix) (5)
(the law is actually valid for strong contextual equivalence, where two equal processes are required to reach an observable in the same 8 2014/12/3 number of steps). This is one of the most distinguishing laws of contextual equivalence. Using the laws we have:

ES = νa (A | E) ctx Σnc(z). νa (A | E | R c, n, z ) ctx c(z). Σn(νa (A | E) | R c, n, z ) = c(z). Σn(ES | R c, n, z )
which shows that ES is a solution of the contraction (4). The proof that also LS is a solution is simpler. The above proof is similar to the proofs with the servers in Sections 2.3 and 3.6. All these proofs, explicitly or implicitly, employ 'up-to context' reasoning; above the common context is c(z).

Σn([•] | R c, n, z ).
A proof that follows the definition of contextual equivalence would be hard due to the quantification on all contexts. In CCS, contextual equivalence coincides with trace equivalence. The equality in the example cannot be proved purely algebraically, using standard axiom systems for trace equivalence, because the systems compared are not finite or finite state (axiomatisations are complete only on these systems). One could show that ES and LS have the same traces proceeding by induction on the length of the traces. The proof is tedious, for instance because R could be any process. REMARK 6.5. The proof of the equality between ES and LS reveals the essence of the technique based on unique solution of contractions. One employs some simple algebraic laws to prove that two tuples of terms are solutions of a certain system of contractions, from which the equality between the two tuples is derived from the unique-solution theorem. The algebraic laws may have been obtained in various ways (e.g., an axiomatisation of the equality for the finite terms). In our example we have used laws for bisimilarity, because it implies contextual equivalence, plus law [START_REF] Bloom | Bisimulation can't be traced[END_REF]. Law ( 5) is a well-known law in axiomatisations of trace equivalence; the law can also be easily proved directly in terms of contextual equivalence, reasoning by induction on the length on the number of τ -steps needed to reach an observable. 2

Trace equivalence

In this section we briefly consider trace equivalence. In CCS and most process algebras, trace equivalence is a direct characterisation of contextual equivalence, in the same way as bisimilarity is for barbed congruence. Aside from this, we look at trace equivalence because it is a behavioural equivalence non-contextual and inductive. We use s to range over traces, i.e., non-empty sequences of visible actions. We assume to be in a generic process language L with an LTS semantics, as in Section 4. We write P µ = ⇒n P if P µ = ⇒ P is derived using n strong transitions (i.e., we have P (

τ -→) m µ -→ ( τ -→) m P and n = m + m + 1. If s = 1, . . . , n, then we write P s = ⇒ if P 1 = = ⇒ P1 2 = = ⇒ P2 . . . Pn-1 n = = ⇒
= ⇒ iff Q s = ⇒.
Two processes P, Q are in the trace equivalence contraction, written P tr Q, if, for each trace s:

1. if P s = ⇒n then Q s = ⇒m for some m ≤ n; 2. if Q s = ⇒ then P s = ⇒.
A process language is ≈tr-safe if ≈tr is a congruence and tr a precongruence. THEOREM 7.2. In any ≈tr-safe process language L, a system of autonomous contractions has a unique solution for ≈tr.

Refined forms of trace equivalence exist. For instance, ready trace equivalence [START_REF] Jos | Readytrace semantics for concrete process algebra with the priority operator[END_REF][START_REF] Van Glabbeek | The linear time-branching time spectrum II[END_REF] combines traces with barbs. The idea of contraction and Theorem 7.2 can be adapted to ready traces by combining the treatment of traces in Definition 7.1 with the treatment of barbs in Definitions 5.3 and 6.2.

Non-applicability of the technique

The contraction technique may be applied to any equivalence whose observables are finitary, in the sense that if an observable holds then it can be reached in a finite number of transitions. Bisimilarity is in this class: the observables are the weak transitions There are behavioural equivalences, however, in which the observables are not finitary. For instance, an observable may be inherently coinductive, as for observables such as infinite traces and non-termination. We illustrate the possible failure of the contraction techniques in these cases using infinitary trace equivalence, whereby two processes are equated if they have the same traces, including the infinite ones. It is unclear how the contraction of infinitary trace equivalence should be defined. In any case, however, 'unique solution' would fail, even for guarded and sequential contractions. As an example, consider the processes P def = Σna n and Q def = P + a. !a. 0. These processes are not infinitary trace equivalent. However, in an 'infinitary trace' semantics they both are solutions to the (guarded and sequential) contraction X a + a. X

The definition of the the contraction for infinitary trace equivalence is irrelevant here, because the processes have no τ -transitions. Similar problems arise for must equivalence, where non-termination is observable -the same counterexample of infinitary trace equivalence applies.

Injecting contractions into the bisimulation game

An advantage of bisimilarity, with respect to other behavioural equivalences, is the locality of the required checks: related states only have to match each other's immediate transitions. We can inject some locality also in other equivalences by introducing the corresponding contraction into a 'bisimulation up-to' game. We illustrate this possibility with contextual equivalence, which is inductive and contextual and therefore faraway from bisimilarity and its local checks. Since we play the bisimulation game, we assume a process language L with an LTS semantics, on top of which contextual equivalence (and reduction semantics) is defined as in CCS.

DEFINITION 9.1 (bisimulation up-to ctx). A relation R on the process language L is a bisimulation up-to ctx if, whenever P R Q, we have:

1. P µ -→ P implies Q µ = ⇒ Q and P ctx R ≈ctx Q 2.
the converse of (1) on the actions from Q.

As in the case of ordinary bisimulation, so bisimulation up-to ctx may be enhanced by combination with further up-to techniques. For instance, in the bisimulation up-to ctx and context the requirement P ctx R ≈ctx Q on the derivatives of Definition 2.3 becomes P ctx R c ≈ctx Q It is sufficient to analyse the most powerful technique ('up-to ctx and context'), and the results will also hold for the weaker 'up-to ctx'. We derive soundness from that of the corresponding contraction technique. LEMMA 9.2. In L, suppose R is a bisimulation up-to ctx and context. Then there is a system of reduction-autonomous contractions, of the same size as R, of which R1 and R2 are solutions for ctx.

COROLLARY 9.3. (soundness of bisimulation up-to ctx and context). Suppose a relation R on the process language L is a bisimulation up-to ctx and context. Then R ⊆ ≈ctx.

We have seen that, in the case of bisimilarity, the techniques of 'unique solution of contractions for ≈' and of 'bisimulation up-to contraction and context' are equivalent. For contextual equivalence, however, the former technique is more powerful. The reason is that, in the 'bisimulations up-to ctx and context' game, laws and equalities for ≈ctx are applied only after the derivatives of the processes in the pairs have been chosen. For instance, the lazy and eager servers of Section 6.1, LS and ES, cannot be a pair of a bisimulation up-to ctx and context, for the same reason why they are not bisimilar: the challenge transition

ES τ -→ νa (A | c(z). (E | R c, n, z ))
cannot be matched by LS.

In some cases, however, the obstacle can be bypassed. We show this for the processes LS and ES of the server example. We relate LS to a contraction ES of ES, obtained by abstracting the initial private communication with the auxiliary server A:

ES ctx Σnνa (A | c(z). (E | R c, n, z )) def = ES (6)
Now, the singleton relation {(LS, ES )} is a bisimulation up-to ctx and context. The processes in the pair initially may only perform an input at c; if v is the value received in the input, then the transitions are

ES c v ---→ Σnνa (A | E | R c, n, v ) def = ES 1 and LS = νa (A | c(z). a(x). (L | R c, x, z )) c v ---→ νa (A | a(x). (L | R c, x, v )) def = LS1
Now we have, using algebraic reasoning similar to that in previous examples with the servers and (6):

ES 1 ∼ Σn(νa (A | E) | R c, n, v ) ctx Σn(ES | R c, n, v ) and LS1 ctx Σn(νa (A | L) | R c, x, v ) = Σn(LS | R c, x, v )
This is sufficient, up-to ctx and context. Finally, having proved ES ≈ctx ES and ES ≈ctx LS, we derive ES ≈ctx LS by transitivity.

Other behavioural equivalences and their contractions can be injected into the 'bisimulation up to' game, along the lines of what done here for contextual equivalence.

Higher-order languages

The contraction technique may also be used in higher-order languages such as the λ-calculus and the Higher-Order π-calculus [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF]. We refrain from attempting to produce a general theory of contractions for higher-order languages, comparable in power to the bisimulation proof method for these languages. We leave this for future work. Here we simply show that the transport to a higher-order setting of the most basic contraction techniques -those involving a reduction semantics and contextually-defined equivalences -can still be useful. We illustrate this on the Higher-Order π-calculus.

We consider the Higher-Order π-calculus in its simplest form, where only processes can be communicated. Below is the syntax; see Figure 2 for the reduction semantics.

P ::= a P . Q | a(x). P | x | νa P | P | Q | 0
We use a, b, c, . . . to range over names, and x, y, z, . . . to range over variables; we call them language variables (to distinguish them from the contraction or equation variables such as X, Y ). An input a(x). P binds the free occurrences of variable x in P ; similarly a restriction νa P binds the free occurrences of name a in P . A term is open or closed depending on whether it may, or may not, have free language variables (in any case, it may have free names).

Systems of contractions in the Higher-Order π-calculus In the definition of barbed congruence and its contraction, the only technicality of higher-order languages that has to be taken into account is the distinction between open and closed terms. This is dealt with in the expected manner. All running terms are supposed to be closed. Thus the definitions of equivalences and preorders in earlier sections (e.g., barbed congruence and its contraction) are meant to be on closed terms. The definitions are generalised to open expressions by requiring instantiation of the language variables with all closing substitutions, i.e., substitutions that make the terms closed (using, in contextual definitions, closing contexts rather than closing substitutions would yield the same relations).

An example

The example is about two ways of modeling the replication operator. We consider the equality (barbed congruence) between the terms c A and c B , where Terms c A and c B send on c processes (A and B) that can receive a process at b and then replicate this process. Indeed, if P is the process so received, assuming a does not occur free in P , in one case we obtain the term

AP def = νa (M { P /y} | a M { P /y} )
and in the other case

BP def = νa (N | a P | N ) ,
and then we have:

AP -→ P | AP -→ P | P | AP -→ • • • BP -→ P | BP -→ P | P | BP -→ • • •
The internal structure of AP and BP is however different.

A system of contractions that proves c A ≈ c bar c B is the following:

X c Y . 0 Y b(y). Z Z τ . (y | Z)
These contractions are reduction-autonomous, and therefore have a unique solution for barbed congruence. Note that, in the first contraction, a contraction variable occurs within the initial output prefix. Thus the contraction is not weakly guarded. Still, the contraction is reduction-autonomous because a process that replaces the Structural congruence the least congruence ≡ such that: The third process of each solution has y free, as its corresponding contraction. To prove that these are solutions, we need a few simple algebraic laws.

• P | Q ≡ Q | P , P | (Q | R) ≡ (P | Q) | R, P | 0 ≡ P ; νa 0 ≡ 0, νa νb P ≡ νb νa P ; (νa P ) | Q ≡ νa (P | Q), if a not free in Q The reduction relation P -→ Q is the least relation such that: a(x). R | a P . Q -→ R{ P /x} | Q P -→ P P | Q -→ P | Q P -→
Using the bisimulation proof method, the proof of the equality between c A and c B is more cumbersome; with the bisimulation techniques currently available, a proof requires an infinite relation. Even in the case of environmental bisimulation, where a form of 'up-to context' is available, the relation used in [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF] for the same example is infinite because, intuitively, the values emitted, A and B, have to be stored in an environment, and can then be played back at any time, possibly several times. What makes the difference is that contractions here allow us to extract a common context that incorporates the prefix for the initial action. In contrast, in 'upto context' techniques for bisimulation, contexts are only removed from the derivatives, after firing an initial prefix.

Further related work

Milner's theorem about unique solution of equations stems from an axiomatisation of bisimulation on finite-state processes [START_REF] Milner | A complete axiomatisation for observational congruence of finite-state behaviors[END_REF]. Indeed, in axiomatisations of behavioural equivalences [START_REF] Baeten | Process Algebra: Equational Theories of Communicating Processes[END_REF][START_REF] Milner | Communication and Concurrency[END_REF], the corresponding rule plays a key role and is called fixed-point rule, or recursive specification principle; see also [START_REF] Moshe | A complete axiomatisation for trace congruence of finite state behaviors[END_REF], for trace equivalence. The possible shapes of the solutions of systems of equations, in connection with conditions on the guardedness of the equations, is studied by Baeten and Luttik [START_REF] Jos | Unguardedness mostly means many solutions[END_REF].

Unique solution of equations has been considered in various settings, including languages, algebraic power series and pushdown automata (see the surveys [START_REF] Kunc | Simple language equations[END_REF][START_REF] Petre | Algebraic systems and pushdown automata[END_REF]), as well as in coalgebras (e.g., [START_REF] Milius | Abstract GSOS rules and a modular treatment of recursive definitions[END_REF]). These models, however, do not have the analogous of 'internal step', around which all the theory of contractions is built. In functional languages, unique solution of equations is sometimes called 'unique fixed-point induction principle'. See for instance [START_REF] Sands | Computing with Contexts: A simple approach[END_REF], in which the conditions resembles Milner's conditions of Theorem 2.8, and [START_REF] Hutton | Representing Contractive Functions on Streams[END_REF], which studies equations on streams advocating a condition based on the notion of 'contractive function' (the word 'contraction' here is unrelated to its use in our paper).

A tutorial on bisimulation enhancements is [START_REF] Pous | Enhancements of the bisimulation proof method[END_REF]. 'Up-to context' techniques have been formalised in a coalgebraic setting, and adapted to languages whose LTS semantics adheres to the GSOS format [START_REF] Bloom | Bisimulation can't be traced[END_REF]; see for instance [START_REF] Bonchi | Coinduction up to in a fibrational setting[END_REF], which uses lambda-bialgebras, a generalisation of GSOS to the categorical framework.

The techniques in Section 9, transporting the bisimulation proof method and some of its enhancements onto non-coinductive equivalences, remind us of techniques for reducing non-coinductive equivalences to bisimilarity. For instance, trace equivalence on nondeterministic processes can be reduced to bisimilarity on de-terministic processes, following the powerset construction for automata [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF]; a similar reduction can be made for testing equivalence [START_REF] Cleaveland | Testing equivalence as a bisimulation equivalence[END_REF]. These results rely on transformations of transitions systems, which modify the nondeterminism and the set of states, in such a way that a given equivalence on the original systems corresponds to bisimilarity on the altered systems. In contrast, in the techniques of Section 9 the transformation of processes is performed dynamically, alongside the bisimulation game: two processes are manipulated only when necessary, i.e., when their immediate transitions would break the bisimulation game. Some beautiful results have been obtained in CSP [START_REF] Roscoe | The theory and practice of concurrency[END_REF][START_REF] Roscoe | Understanding Concurrent Systems[END_REF] in which systems of equations have unique solutions provided their least fixed point (intuitively obtained by infinite unfolding of the equations) does not contain divergent states. In CSP the semantics has usually a denotational flavour and, most important, the reference behavioural equivalence, failure equivalence, is divergent sensitive. As mentioned in Section 8, currently we do not know how to handle divergence in the theory of contractions, as divergence is not a finitary observable. We note however that (at least in the equivalences considered in the paper) unique solution of contractions holds in cases where the infinite unfolding of the contractions would introduce divergence: e.g., the contractions of Example 3.9, as well as the contractions employed in the examples about the lazy and eager servers (where divergence may appear if, in the interaction protocol with a client, the main server is called back).

Conclusions and future work

In this paper we have presented operational techniques, based on the idea of contraction, for proving weak behavioural equivalences, that is, equivalences that abstract from internal moves. We have focused on concurrent languages but the techniques are not meant to be specific to concurrency. We have illustrated the techniques with bisimulation, the most natural ground of application, discussing also completeness. We have then shown that the technique of unique solution of contractions can be transported onto other equivalences, with finitary observables (e.g., contextual equivalence, barbed congruence, trace equivalence). We have also seen that the contraction preorders can be injected into the bisimulation game. In the case of bisimulation, this leads to a (minor) improvement of an existing technique, namely 'bisimulation up-to expansion and context'. The case of non-coinductive or contextual equivalences such as contextual equivalence is more interesting: we can use the bisimulation proof method (enhanced with up-to context) for reasoning on these equivalences, combined with algebraic laws for manipulating states whose immediate transitions would break the bisimulation game. Such techniques allow us, implicitly, to transfer 'up-to context' forms of reasoning, originally proposed for labeled bisimilarities and their proof method, onto equivalences that are contextual or non-coinductive.

As for the technique based on equations, so the technique based on contractions is meant to be used in combination with algebraic reasoning, on terms whose behaviour is not finite or finite-state: the recursion on the contraction variables captures the infinite be-haviour of terms, and the proof that certain processes are solutions is carried out with pure algebraic reasoning.

In comparison with equations, a drawback of unique solution of contractions for an equivalence is that the solutions are not -interchangeable: it may be that P is solution and Q is not, even though P Q. The proof of completeness of the 'unique solution of contractions' method with respect to the bisimulation proof method uses the sum operator to express the possible initial actions of a process. We would like to see how completeness can be recovered in languages in which the sum operator is missing. One may consider the introduction of an operator akin to sum, to be used only for writing contractions. Also, we did not tackle completeness in equivalences other than bisimilarity.

We have related the contraction technique to bisimulation enhancements such as 'up-to expansion and context'. While powerful, these are not the only possible enhancements. It would be interesting to see whether other enhancements can be captured using contractions or similar notions.

We would like to understand on which behavioural equivalences the technique of unique solution of contractions works. We mentioned in Section 8 that it seems to work if the observables of the equivalence are finitary. More experimentation is needed to clarify this point, and formalise appropriate conditions.

In the example with a higher-order language, we have applied the most basic contraction techniques -those for contextuallydefined equivalences. The use of other contraction techniques requires further investigation. Such study may shed light on the applicability of up-to context techniques to higher-order languages [START_REF] Koutavas | Small bisimulations for reasoning about higher-order imperative programs[END_REF][START_REF] Lassen | Relational reasoning about contexts[END_REF][START_REF] Lassen | Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context[END_REF][START_REF] Piérard | Sound bisimulations for higherorder distributed process calculus[END_REF][START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF].

Our original motivation for studying contractions was to better understand 'up-to context' enhancements of the bisimulation proof method and their soundness. More broadly, the goal of the line of work reported is to improve our understanding of bisimilarity and the proof techniques for it, including the possibility of exporting the techniques onto other equivalences.

=

  ⇒ is =⇒ µ -→=⇒ (the composition of the three relations). Moreover, P µ -→ P holds if P µ -→ P or (µ = τ and P = P ); similarly P µ = ⇒ P holds if P µ = ⇒ P or (µ = τ and P = P ). We write P ( µ -→) n P if P can become P after performing n µ-transitions. Finally, P µ -→ holds if there is P with P µ -→ P , and similarly for other forms of transitions.

  Ei}i∈I , and consider a context C[ P ]. Then the process obtained from C[ P ] by unfolding the contractions once is C[ E[ P ] ]; the process obtained by unfolding the contractions twice is C[ E[ E[ P ]] ]; and similarly for the n-unfolding.

  Proof [Sketch] Let n be the length of the transition C[ P ] µ = ⇒ R (the number of 'strong steps' of which it is composed), and let C [ P ] and C [ Q] be the processes obtained from C[ P ] and C[ Q] by unfolding the definitions of the contractions n times. Thus in C each hole is underneath at least n prefixes, and cannot contribute to an action in the first n transitions. We have C[ P ] bis C [ P ], and C[ Q] bis C [ Q], by the precongruence properties of bis . Moreover, since each hole of the context C is underneath at least n prefixes, applying the definition of bis on the transition C[ P ] µ = ⇒ R, we infer the existence of

  Prwhere r ranges over some countable set IP . Following the bisimulation game, for each r there is Qr s.t. Q µr = = ⇒ Qr and Pr R Qr. Proceeding similarly on the challenge transitions from Q, i.e. Q µs --→ Qs for s ∈ IQ, we find processes Ps with P µs = = ⇒ Ps and Ps R Qs. Then the contraction for the pair P, Q is: XP,Q Σrµr. XP r ,Qr + Σsµs. XP s,Qs2

DEFINITION 7 . 1 .

 71 Pn, for some processes P1, . . . , Pn. Similarly we write P s = ⇒m if there are P1, . . . , Pn with P 1 = = ⇒m 1 P1 2 = = ⇒m 2 P2 . . . Pn-1 n = = ⇒m n Pn, and m = Σimi. Two processes P, Q of L are trace equivalent, written P ≈tr Q, if for each trace s we have P s

=

  ⇒ is finitary because obtained by composing a finite number of strong transitions ( τ -→ and µ -→). Different uses of µ = ⇒ may have different lengths, but each length is finite. The same argument holds for ⇓, the observable of contextual equivalence. In all these cases, the contraction preorder precisely arises by playing with such finite measures.

  y). νa (M | a M ) for M def = a(x). (y | x | a x ) and B def = b(y). νa (N | a y | N ) for N def = a(x). (x | a x ).

Figure 2 .

 2 Figure 2. The reduction semantics for HOπ

2014/12/3

2014/12/3

2014/12/3

2014/12/3

2014/12/3

2014/12/3

2014/12/3

2014/12/3

2014/12/3

2014/12/3

Acknowledgments

I have benefited from discussions with Luca Aceto, Jos Baeten, Filippo Bonchi, Matthew Hennessy, Bill Roscoe, David Sands, and from the comments of the anonymous referees. This work has been partially supported by the ANR project 12IS02001 'PACE', and the MIUR-PRIN project 'CINA'.


Olesia Mokrenko

Suzanne Lesecq

Warody Lombardi

Diego Puschini

Carolina Albea

Olivier Debicki

Dynamic Power Management in a Wireless Sensor Network using Predictive Control

Technological advances have made wireless sensor nodes cheap and reliable enough to be brought into various application domains. These nodes are powered by battery, thus they have a limited lifespan which is a major drawback for their acceptance. This paper addresses a power consumption control problem of wireless nodes equipped with batteries. Dynamic power management is used to dynamically re-configure the set of sensor nodes in order to provide given service and performance levels with a minimum number of active nodes and/or a minimum load on such components. The power control formulation is based on model predictive control with constraints and binary optimization variables, leading to a mixed integer quadratic programming problem. Simulations are performed to demonstrate the efficiency of the proposed control method.

I. INTRODUCTION

Wireless sensor networks (WSN) are usually made of lowpower, low-cost, and energy-constrained sensor nodes (SNs) that are deployed to sense a physical phenomenon of interest. The data are collected by access points. From the collected data, an application is built to monitor and/or control the physical world. In both situations, the nodes can be dedicated to specific roles, namely, sensing, actuation and control, or to any combination of the three main roles. Whatever the assigned functionality is, the node embeds processing capability associated with memory capacity, both possibly limited.

In the literature, the SNs are typically split in four main subsystems (SSs) [START_REF] Ian F Akyildiz | Wireless sensor networks: a survey[END_REF] (see Fig. 1):

• the communication subsystem connects the sensor node (SN) to the global architecture in order to send/receive information; • the computing subsystem contains a processing element (for example, a micro-controller unit (MCU)) together with its associated memory; • the sensing subsystem senses physical variables. It can contains several sensors with their adapter (for example, a analog-to-digital converter (ADC)) (when mandatory); • the power supply subsystem that contains the battery used by all the subsystems described above. Most of the wireless SNs are powered by batteries. This is very convenient from a deployment point of view because no {FirstName.LastName}@cea.fr 2 C. Albea is with CNRS, LAAS, 7 avenue du Colonel Roche, F-31400 Toulouse, France and Univ. of Toulouse, UPS, LAAS, F-31400, Toulouse, France calbea@laas.fr Fig. 1: Functional subsystems of a wireless sensor node plug is needed by the node. However, the limited available energy makes the node lifespan a tremendous drawback of the wireless node technologies. Moreover, this limited energy may influence the robustness and/or reliability of the monitoring and/or control application built on top of the WSN. As a consequence, nodes have to be designed with stringent power/energy consumption constraints [START_REF] Ian F Akyildiz | Wireless sensor networks: a survey[END_REF] in order to increase the node lifespan. [START_REF] Anastasi | Energy conservation in wireless sensor networks: A survey[END_REF] proposes a survey of various approaches that can be implemented in order to increase the WSN lifespan. The authors consider the sensing and communication subsystems. They split the possible approaches in three families, namely: duty cycling, data driven and mobility, for the node energy conservation. The experiment is conducted using TelosB [3] nodes.

Even if each subsystem in the sensor node is designed with power efficiency objectives, their association does not necessarily lead to a low-power SN. Consequently, a power/energy management policy for the whole SN is mandatory.

The ability to enable and disable SNs as well as to adapt their performance to the workload, is key to achieve energy efficient functioning of the whole sensor network. Dynamic Power Management (DPM) is proposed here to dynamically re-configure a WSN in order to provide the requested services and performance levels with a minimum number of active SNs and/or a minimum load on the nodes. DPM is used in the System-on-Chip (SoC) area. It encompasses a set of techniques that achieve energyefficient computation by selectively turning off or reducing the performance of the system components when they are idle (or partially unexploited). The fundamental premise for the DPM applicability is that systems (and their components) experience non-uniform workloads during the operation time. This assumption is valid for most systems, both when considered in isolation (e.g. SoC platform) and when connected via a network (e.g. a set of SNs). A second assumption of DPM is that it is possible to predict, with a certain degree of confidence, the workload fluctuations. Note that when "energy-hungry" sensors [START_REF] Alippi | Energy management in wireless sensor networks with energyhungry sensors[END_REF] are embedded in the nodes, an efficient DPM must be implemented in order to have an optimal overall energy. This global power management policy is certainly a more complex problem than the one dedicated to a single node because, in essence, the WSN is spatially distributed, usually with a clock frequency in each node that is not (properly) synchronized with the other ones.

The present paper addresses DPM at the WSN level. The objective is to provide for the WSN a given service (hereafter named "mission") while the lifespan is extended, the power consumption within the network being minimized. The mission is expressed as a set of constraints on the different functioning modes of each SN.

Related work

Power management at the WSN level has already been addressed in the literature in order to increase the node lifespan, see for instance [START_REF] Chen | Utility-based asynchronous flow control algorithm for wireless sensor networks[END_REF], [START_REF] Ian F Akyildiz | Wireless sensor networks: a survey[END_REF]. This latter shows that tradeoff mechanisms that give the end-user the option of prolonging the network lifetime at the cost of lower throughput or higher transmission delay, can be implemented. The kinds of mechanisms are not discussed in the present paper, but they might be added to the proposed control. There, Model Predictive Control (MPC) seems an appropriate technique, as it is based on an optimal control policy applied by predicting the behavior of the system over a receding horizon [START_REF] María M Seron | Characterisation of receding horizon control for constrained linear systems[END_REF]. Due to its characteristics, MPC can handle constraints [START_REF] David Q Mayne | Constrained model predictive control: Stability and optimality[END_REF] during the design phase while being applied to linear Single-Input-Single-Output (SISO) and Multiple-Input-Multiple-Output (MIMO) systems [START_REF] Eduardo | Model predictive control[END_REF], [START_REF] Marian | Predictive control: with constraints[END_REF], nonlinear [START_REF] Allgöwer | Nonlinear model predictive control[END_REF], [START_REF] Allgöwer | Nonlinear predictive control and moving horizon estimation-an introductory overview[END_REF] and hybrid systems [START_REF] Bemporad | Predictive control of constrained hybrid systems[END_REF], [START_REF] Lazar | Model predictive control of hybrid systems: Stability and robustness[END_REF]. This last class of systems can describe continuous (and sampled) states (real-set variables), discrete and state-machine states (integer-set variables) and logic rules (binary-set variables) [START_REF] Bemporad | Control of systems integrating logic, dynamics, and constraints[END_REF]. It is solved as a mixed integer program (MIP).

A similar problem is considered in the literature using the Fault-Tolerant Control (FTC) paradigm [START_REF] Camacho | Fault-tolerant model predictive control[END_REF]. In this present paper, MPC can handle FTC schemes by changing the constraints or by considering different models in a switched framework. Fault Detection and Isolation (FDI) can be used in a receding horizon strategy, in order to identify parameters and thus determine if the data obtained is consistent with the established model. In this sense, FDI involves deciding if the system works as expected, i.e. if all the components (sensors, actuators, controllers) behave satisfactorily. This decision is generally taken by processing input/output data, and FDI strategies should be able to detect a fault and eventually isolate it. Once the fault is detected, a control reconfiguration can occur in order to guarantee stability and avoid performance degradation.

Power control in a WSN using multiple-description coding is addressed in [START_REF] Daniel E Quevedo | Power control and coding formulation for state estimation with wireless sensors[END_REF] whose main contribution is to investigate the role of dynamic power control and coding when state estimation is considered. The control objective is to counteract the channel variability (i.e. ensure Quality of Service (QoS)) Fig. 2: Single-hop heterogeneous sensor network architecture and achieve a compromise between the battery use and the estimation accuracy. The controller is located in a gateway. It decides upon the transmission power level and the coding scheme to be used by each node. However, satisfying the QoS does not guarantee that the "mission", as defined here, is satisfied.

The paper is organized as follows. Section II is first dedicated to the system modeling. Then the control objectives are provided. The control design is developed in section III. It is based on Constrained Predictive Control techniques, with bounded states, equality and inequality constraints and binary control values. Section IV implements the proposed control on a realistic benchmark. Conclusion and future work are provided in section V.

II. SYSTEM MODELING AND CONTROL OBJECTIVES

Consider a WSN that contains n ∈ N nodes S i , i = 1, . . . , n, powered by batteries. The nodes are supposed heterogeneous, i.e. their hardware can differ, some nodes possibly embedding more computational capabilities than other ones, leading to different roles in the network. Moreover, their battery characteristics can be different. The communication is supposed to be single-hop clustered [START_REF] Mhatre | Homogeneous vs heterogeneous clustered sensor networks: a comparative study[END_REF]: each SN sends its data to a specific node called "sink" which is responsible for the monitoring and control of the area connected by the SNs and/or for interconnecting to a Wide Area Network such as the Internet. This sink chooses the working mode of the nodes thanks to a strategy presented hereafter. The topology considered is depicted in Fig. 2.

Each SN can be placed in different functioning modes M j , j = 1, . . . , m, m ∈ N, which are related to the states (on, sleep, off, etc.) of each SN subsystem, characterized by a known average power consumption for a given period of time. Here, the nodes are supposed to provide redundant information. Therefore, in order to achieve a given service, only a subset of the SNs is absolutely mandatory. Thus, if one selects properly the mode of the nodes, power savings can be achieved. In other words, most of the devices can be placed in sleep mode, while the other ones are active (i.e. sending and/or transmitting information).

In order to control energy savings in the WSN, the remaining energy in the nodes is modeled with a discretetime linear time-invariant (LTI) state-space system:

x k+1 = Ax k + Bu k (1)
where x k ∈ R n,+ is the remaining energy in the battery of node S i , i = 1, . . . , n, at instant k. Bu k represents the averaged energy that will be used during the time interval

[T P W k, T P W (k +1)],
where T P W is the decision period (i.e. the time period when the power control is run). The battery has a bounded capacity. Thus, for node S i :

0 x i X i max (2)
The initial battery charge (i.e. at instant k = 0) for S i is denoted X i 0 . The state matrix A ∈ R n×n is equal to the identity matrix

I n while u k = [u T 1 , • • • , u T n ] T ∈ {0, 1} nm is the control with u i {j} ∈ {0, 1}. Each sub-vector u i represents the mode of S i .
The SN S i has a unique working mode at instant k. Therefore, for i = 1, . . . , n, a set of constraints has to be defined at each instant k: 1) is interpreted as the control matrix. Each component b ij represents the amount of energy averaged over T P W consumed by the SN S i , when it works in mode M j during the time interval [T P W k, T P W (k + 1)] (see Table I). Note that a change from one mode to another has an extra energy cost that is supposed to be integrated in b ij in this paper.

m j=1 u i {j} = 1 (3) Matrix B = diag [-B 1 , . . . , -B n ] ∈ R n×nm in Eq. (
In order to fulfill a "mission" while decreasing the power consumption, a subset of d j ∈ N SNs is assigned to a given mode M j . Thus an extra set of constraints is defined:

n i=1 u i {j} = d j (4)

Control objectives

A dynamic energy saving control policy has to be implemented at the WSN level in order to increase its lifespan while guaranteeing adequate performance levels expressed as a mission. The capability to fulfill a mission is related to the WSN QoS. However, it imposes extra functional constraints to the WSN. As indicated above, the control variable u k takes its values in {0, 1}. It fixes the functioning mode of each node under constraints (3) (meaning that each mode is in a unique mode) and (4) that are used to define the mission. For instance, in a network of n SNs that deliver strongly correlated information, the whole system power consumption can be decreased if the nodes are properly managed in order to provide just enough information for the application to be performed "properly". Broadly speaking, this means that the application requires N on < N nodes that communicate while N -N on nodes can be set in the Sleep mode that consumes less energy than the On mode.

III. CONTROL DESIGN

The power consumption minimization of (1) can be presented as a Quadratic Programming (QP) problem. Constrained Predictive Control implies the resolution of this problem via the minimization of a cost function using a finite number of finite-dimensional positive definite Quadratic Problems. The constrained QP does not feature the undesirable mismatch between the open-loop and closed-loop nominal system trajectories, which is presented in the other popular forms of MPC that can be implemented with a finite QP algorithm.

Recently, the interest in using MPC for controlling systems that involve a mix of real-valued dynamics and logical rules has arisen [START_REF] Bemporad | Predictive control of constrained hybrid systems[END_REF], [START_REF] Bemporad | Control of systems integrating logic, dynamics, and constraints[END_REF]. Unfortunately, when this problem is formulated as an optimization one, the resulting description is no longer a QP problem but a Mixed-Integer Quadratic Programming (MIQP) problem. This latter involves optimization variables that can be real values, but also integer values or even binary values, which makes the problem harder to solve than an ordinary QP problem.

It is assumed throughout the rest of the paper that the pair (A, B) of ( 1) is stabilizable. At each sampling time (i.e. decision time as defined above), the current state (assumed to be available) x k = x k|k can be used to find the optimal control sequence u * = u T k|k , . . . , u T k+Np-1|k

T by means of the following minimization problem:

u * = arg min u Np-1 i=0 x T k+i|k Qx k+i|k + Nu-1 i=0 u T k+i|k Ru k+i|k subject to:          x k+i+1|k = Ax k+i|k + Bu k+i|k , i = 1, . . . , Np -1 u k+i|k = 0, i = Nu, Nu + 1, . . . , Np -1 u k+i|k ∈ {0, 1} Xmin x k+i|k Xmax, i = 1, . . . , Np -1 (5)
where Q = Q T 0 and R = R T > 0 are weighting matrices, X min and X max are the lower and upper bounds on the state x k+i|k , and the pair (Q 1/2 , A) is detectable. The prediction horizon N p , the control horizon N u N p together with matrices Q and R are the degrees of freedom of the control design methodology.

By compacting the states involved in the optimization problem (5) as x = x T k+1|k , . . . , x T k+Np|k T and denoting x k|k = x, the cost function is rewritten in a matrix form as:

arg min u x T Qx + u T Ru subject to:      u ∈ {0, 1} Finx x Ḡinx Fequ u = Ḡequ (6) where Q = diag [Q, . . . , Q], R = diag [R, . . . , R].
The inequality and equality constraints are fully described by Finx ∈ R s×n , Ḡinx ∈ R s , Fequ ∈ R p×r and Ḡequ ∈ R p , p = (N p -N u )nm, r = N p nm, s = N p q that express the constraints (2), (3) and ( 4) on x k|k and u k|k ∀k, respectively. System (1) can now be extended in a compact matrix form:

x = Φx + Γu Φ =      A A 2 . . . A Np      , Γ =      B 0 • • • 0 AB B • • • 0 . . . . . . . . . . . . A Np-1 A Np-2 • • • A Np-Nu      (7)
Then ( 6) is given as a MIQP (see e.g. [START_REF] Marian | Predictive control: with constraints[END_REF]) arg min u u T Hu + 2u T F x subject to:

     u ∈ {0, 1} Finx Γu Ḡinx -Finx Φx Fequ u = Ḡequ (8)
where

H = Γ T QΓ + R, F = Γ QΦ (9)
It is worth mentioning that the the control designer has to choose of the weighting matrices Q and R and the prediction N p and control N u horizon.

IV. APPLICATION

To show the effectiveness of the proposed strategy, a benchmark with n = 6 SNs S i and one sink is considered in simulation 1 . At instant k, the SN S i , i = 1, . . . , 6, can be in a unique mode among 3 possible ones M j , j = 1, . . . , 3 (see Table II):

• M 1 is the standard On mode. In this mode, the node acquires measurements. It has transmission/reception capabilities. It can also process data and it monitors its battery. Fig. 3 shows the typical current consumption of a SN working in M 1 mode. The waveform corresponds to a wireless SN application cycle: the node awakes from the Sleep state. Then, it goes to Rx state, waiting for a beacon. It collects data and prepares the data packets to be transmitted. Then, the packet is sent to the sink. On the figure, one can see the dependence of the current consumption on the state of each node subsystem. Channels number one and two correspond to the transmission and reception current consumption of the Communication SS, respectively. The fourth channel representsthe MCU/Sensor(s) current consumption (Processing and Sensing SSs). The third channel corresponds to the total SN current consumption; • M 2 corresponds to a Sleep mode. In this mode, the SN uses the internal oscillator for lower power consumption (Real Time Clock). When the node awakes the clock is switched to a high frequency oscillator for faster operations but also with a higher power consumption; • M 3 corresponds to the SN in the total Switch off state.

In practice, this mode is equivalent to a faulty situation, e.g. the node battery is completely drained, the sink cannot reach the node, etc. Note that the node can exit M 3 for instance when it has enough energy to be placed in M 1 , or when the sink can access it again. In the present scenario, the mission is split in two phases corresponding respectively to daytime and night period of time. Therefore, the constraints that define the mission have to be dynamically changed, depending on the time schedule and two constraints (4) define the dynamic mission:

day (8am -6pm) : d 1 = 3 (3 nodes in M 1 ) night (6pm -8am) : d 1 = 1 (a unique node in M 1 ) (10)
The sampling period associated to the SNs is T s = 60s. Thus, data collected from sensors in M 1 are every minute. Note that the nodes in mode M 1 perform the reception, measurement, computing and transmission functionalities every minute. The SNs that are not in mode M 1 are placed in M 2 . All the SNs in mode M 2 have to wake up every hour. This latter corresponds to the period T mb = 1h associated with the monitoring of the battery remaining capacity. The remaining energy is sent to the sink. Note that this is in fact a measurement phase with y k = x k . M 3 corresponds to a faulty situation is imposed when

X i 0 X i max ≤ δ.
This corresponds to the situation when the node battery is nearly fully drained.

Assume at k 0 , the node batteries have enough energy so that any node S i can fulfill the mission (i.e. being in M 1 ). Therefore, during the day (resp. night) period, three (resp. one) nodes are placed in mode M 1 while the 3 (resp. 5) other nodes are placed in M 2 . As soon as the battery capacity of a SN, say sensor S f , is lower than δ, S f falls in mode M 3 . Then, the control law assigns a new mode to the remaining nodes in order to meet the dynamic mission while minimizing the energy consumption of the sensor network. Actually, the set of constraints is modified because u f (3) = 1. Hereafter, δ = 0.1 is chosen.

For the system (1), A = I 6 while the components of matrix B are calculated from the values given in Table III, multiplied by battery nominal voltage value of the corresponding SN (see Table IV where the battery characteristics associated to each node are provided). Note that the numerical values are derived from [START_REF] Fourty | An advanced study of energy consumption in an ieee 802.15. 4 based network: Everything but the truth[END_REF]. Table IV also provides the initial capacity of the batteries associated with each SN. These latter numerical values are obtained from [START_REF] Sudevalayam | Energy harvesting sensor nodes: Survey and implications[END_REF].

The weighting matrices Q and R that appear in the definitions of Q and R in [START_REF] Marian | Predictive control: with constraints[END_REF] are chosen equal to:

Q = 0 6×6 ; R = B T B ( 11
)
where 0 is the null matrix with appropriate dimension. The choice Q = 0 6×6 roots in the fact that the state dynamics should evolve as slowly as possible [START_REF] Robert L Williams | Linear state-space control systems[END_REF]. The choice of R implies that the nodes with bigger energy consumption are more penalized. From (2), the inequality constraints become:

I 6 -I 6 Fin x    x 1 . . . x 6    ≤ X 1 max • • • X 6 max 0 • • • 0 T Gin x (12)
while the equality constraints (3) and ( 4) are defined as:

   1 1 1 • • • 0 . . . . . . . . . 0 • • • 1 1 1    F 1 equ    u 1 {j} . . . u 6 {j}    =    1 . . . 1    G 1 equ (13)
  1 0 0 1 0 0 • • • 1 0 0 0 1 0 0 1 0 • • • 0 1 0 0 0 1 0 0 1 • • • 0 0 1   F 2 equ    u 1 {j} . . . u 6 {j}    =   a b c   G 2 equ ( 14
)
where a and b correspond to the number of nodes in modes M 1 and M 2 , respectively. During daytime a = 3 and at night a = 1 (see [START_REF] Allgöwer | Nonlinear model predictive control[END_REF]). c corresponds to the number of nodes fallen in mode M 3 with c = nab. The other matrices are defined as follows:

F equ = F 1 equ F 2 equ T ; G equ = G 1 equ G 2 equ T ; Fequ = diag [F equ , . . . , F equ ], Ḡequ = diag [G equ , . . . , G equ ], Finx = diag [F inx , . . . , F inx ], Ḡinx = diag [G inx , . . . , G inx ].
The prediction horizon is chosen N p = 5 and the control horizon is N u = 1. As the considered system presents slow dynamics, this horizon seems sufficient enough. The decision period (i.e. the time period when the power control is run) is T P W = T mb = 1h. Thus, the MIQP problem is solved on-line at each decision time T P W k.

The power control of the SNs at network level is simulated in the MATLAB environment. The MIQP problem is solved with Yalmip [START_REF] Löfberg | Yalmip : A toolbox for modeling and optimization in MATLAB[END_REF]. Fig. 4 provides simulation results. One can see the evolution of the number of SNs: it depends on the daytime/night condition and on the battery conditions.

The battery energy state of the SNs is shown when the control of the whole network is implemented in Fig. 5a. Fig. 5b shows the energy in the battery nodes in the usual situation, i.e. when all nodes are in the On state during the whole period of simulation. Note that in the first situation with "daytime/night" conditions, the mission can be extended up to 691 hours. This lifespan is highly extended more than 2x because un-useful nodes are in sleep mode. In the case the Dynamic Power Management at network level is not implemented, the network lifespan is equal to 302 hours. This means that, for this particular scenario, the proposed management method doubles the lifespan. Fig. 5c compares the total energy consumption in both situations (i.e. with and without DPM). In this paper, dynamic power management of SNs at network level via MPC has been proposed. The energy in the SN batteries is modeled using a state-space representation. The control is solved using a MIQP approach. The objectives for the dynamic power control are expressed as a mission that defines a minimum number of active SNs to attain performance levels. In this way, only the sensors that are mandatory to fulfill the mission are in On mode while the other ones are placed in Sleep mode. In this way, the lifespan of WSN is extended. Experiments in simulation for n = 6 SNs have been conducted. The results are promising and can be extended to a larger number of SNs depending the complexity of the MIQP problem to be solved. The DPM method is currently under implementation on a test-bench in order to evaluate in real-life conditions the capability of the proposed control method at network level.

Fig. 3 :

 3 Fig. 3: Excerpt of the waveforms of a typical cycle for a wireless sensor node working in mode M 1 (current consumption)

Fig. 4 :

 4 Fig. 4: Functioning modes of sensor nodes vs. time with DPM (simulation started at midnight)

Fig. 5 :

 5 Fig. 5: Results of the system simulation

TABLE I :

 I Average energy consumption for each SN S i in the different modes M j over the certain time period T P W

	Sensor node	Mode M1	Mode M2	. . .	Mode Mm
	S 1	b 11	b 12	. . .	b 1m	= B 1
	. . .	. . .	. . .	. . .	. . .	. . .
	Sn	b n1	b n2	. . .	bnm	= Bn

TABLE II :

 II Functioning modes for sensor node S i

	Modes	Processing SS	Communication SS	Sensing SS
	M 1	Active	Tx / Rx	On
	M 2	Sleep	Off	Off
	M 3	Off	Off	Off

TABLE III :

 III Average current consumption (mA • h) of sensor node S i in the functioning mode M j over the period T mb

	Sensor node	Mode M 1	Mode M 2	Mode M 3
	S 1	6.56	0.92	0
	S 2	8.72	1.11	0
	S 3	7.75	1.08	0
	S 4	9.43	1.26	0
	S 5	7.54	1.29	0
	S 6	7.20	1.03	0

TABLE IV :

 IV Sensor node battery characteristics (each sensor node embeds two AA batteries)

	Sensor node	Battery Type	Nominal Voltage [V]	Battery capacity X i max /2 [mA•h]	Initial battery X i 0 capacity X i max
	S 1	NiCd	1.2	1100	1
	S 2	NiCd	1.2	1100	0.8
	S 3	NiMH	1.2	2500	1
	S 4	NiMH	1.2	2500	0.7
	S 5	Li-ion	3.7	740	0.9
	S 6	Li-ion	3.7	740	1

O. Mokrenko, S. Lesecq, W. Lombardi, D. Puschini and O. Debicki are with Univ. Grenoble Alpes, F-38000 Grenoble, France and CEA, LETI, MINATEC Campus, F-38054 Grenoble, France

Note the control approach has been developed for n ∈ N nodes, see the previous section.

ACKNOWLEDGMENT

This work has been partly funded by the Artemis AR-ROWHEAD project under grant agreement nb. 332987 and by the FP7 SCUBA project under grant agreement nb. 288079.