Sorin Stratulat
email: sorin.stratulat@univ-lorraine.fr

Validating Back-links of FOL ID Cyclic Pre-proofs

Cyclic pre-proofs can be represented as sets of finite tree derivations with back-links. In the frame of the first-order logic with inductive definitions (FOL ID ), the nodes of the tree derivations are labelled by sequents and the back-links connect particular terminal nodes, referred to as buds, to other nodes labelled by a same sequent. However, only some back-links can constitute sound pre-proofs. Previously, it has been shown that special ordering and derivability conditions, defined along the minimal cycles of the digraph representing a particular normal form of the cyclic pre-proof, are sufficient for validating the back-links. In that approach, a same constraint could be checked several times when processing different minimal cycles, hence one may require additional recording mechanisms to avoid redundant computation in order to downgrade the time complexity to polynomial.

We present a new approach that does not need to process minimal cycles. It based on a normal form that allows to define the validation conditions by taking into account only the root-bud paths from the non-singleton strongly connected components of its digraph.

Introduction

In [START_REF] Brotherston | Cyclic proofs for first-order logic with inductive definitions[END_REF][START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF][START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF], Brotherston and Simpson introduced the notion of cyclic (pre-)proof in the frame of firstorder logic with inductive definitions (for short FOL ID and detailed, e.g., in [START_REF] Aczel | An introduction to inductive definitions[END_REF]) and including equality. In this setting, the cyclic pre-proofs are sequent-based proof derivations usually presented in the form of finite trees. Some of their terminal nodes, called buds, are labelled by 'not-yet proved' sequents that already labelled other nodes, called companions. For each bud there is only one companion and the bud-companion relations are referred to as back-links.

Not all back-links may constitute sound pre-proofs. Indeed, a pre-proof can be constructed for any false sequent S by applying a stuttering inference step1 that creates a copy of S. This terminal node is a bud whose companion is the root of the pre-proof. [START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF][START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] also introduced the CLKID ω inference system for building cyclic pre-proofs and defined a sufficient criterion for checking their soundness in terms of a global trace condition. This condition is an ω-regular property that can be checked as an inclusion between two Büchi automata. The inclusion test includes an automata complementation procedure [START_REF] Kupferman | Weak alternating automata are not that weak[END_REF] whose time complexity is exponential in the number of states of the automaton to be complemented.

A more effective soundness criterion was given in [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF] for pre-proofs generated by CLKID ω N , a restricted version of CLKID ω . Inspired from a previous method [START_REF] Stratulat | A unified view of induction reasoning for first-order logic[END_REF][START_REF] Stratulat | Mechanically certifying formula-based Noetherian induction reasoning[END_REF] for checking the soundness of cyclic proofs built using the Noetherian induction principle for reasoning on conditional specifications, its time complexity can be downgraded to polynomial. To do this, a CLKID ω N pre-proof is normalised to some set of finite tree derivations which can be represented as a directed graph (for short, digraph) having some arrows labelled by substitutions. The soundness criterion asks that some derivability and ordering constraints hold along the paths leading root nodes to bud nodes in the minimal cycles of the digraph, i.e., cycles that do not include other cycles.

In general, the number of minimal cycles in a digraph with n nodes can be much greater than the number of its buds (which is always smaller than n). For complete digraphs, i.e., digraphs for which every pair of distinct nodes is connected by arrows in the two ways, one can define the number of minimal cycles built by k ∈ [2..n] nodes, as follows. We take one of the n nodes as the starting node in the cycle, then the next one from the remaining n -1 nodes, and so on for k -1 times. So there are n × (n -1) × . . . × (nk + 1) ways to do it. Since the cycle consisting of the k nodes can be built in k different times, depending which is the starting node among its nodes, this number is n! (n-k)!k . Hence, the total number of minimal cycles in a complete digraph with n nodes is

n ∑ k=2 n! (n -k)!k
Fortunately, the number of arrows in any digraph built with the approach from [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF] is smaller than that for the complete digraphs because each bud node has only one companion. However, a orderingderivability constraint can be checked several times as it may be defined w.r.t. different minimal cycles. In [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF], it was already suggested that their number can be reduced to the number of buds from the minimal cycles, hence smaller than n. This redundancy can be avoided, for example, by using recording mechanisms.

In this paper, we present an improved version of the soundness criterion for validating CLKID ω N preproofs. The advantage is that the computation of minimal cycles is not needed and there is no redundancy in the computation of the ordering-derivability constraints. In order to do this, we propose a new normal form of CLKID ω N pre-proofs and define ordering and derivability constraints for every root-bud path that occurs in a non-singleton strongly connected component (SCC) of the digraphs associated to the new normal forms. We show that the number of constraints is that of the buds from the non-singleton SCCs.

The rest of the paper is structured as follows. Section 2 gives a brief presentation of FOL ID and CLKID ω N . Section 3 introduces the soundness criterion for CLKID ω N pre-proofs by detailing the normalisation procedure, the digraph construction and the definition of the ordering and derivability conditions. A comparison is made with the soundness criterion from [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF]. The conclusions and future work are given in the last section.

Induction-based sequent calculus

Syntax. The logical setting is that presented in [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF], based on FOL ID with equality using a standard (countable) first-order language Σ. The predicate symbols are labelled either as ordinary or inductive, and we assume that there is an arbitrary but finite number of inductive predicate symbols. The terms are defined as usual. By t, we denote a vector of terms (t 1 , . . . ,t n ) of length n, the value of n being usually deduced from the context.

New terms and formulas are built by instantiating variables by terms via substitutions. A substitution is a mapping from variables to terms, of the form {x 1 → t 1 ; . . . ; x p → t p }, for some p > 0, which can be written in a more compact form as {x → t}, where x ≡ (x 1 , . . . , x p ), t ≡ (t 1 , . . . ,t p ), and ≡ is the syntactic equality. The composition of σ 1 with σ 2 is denoted by σ 1 σ 2 , for all substitutions σ 1 and σ 2 . A term t is an instance of t , or t matches t , if there is a substitution σ such that t ≡ t σ . Similarly, the notion of matching can be extended to vector of terms, atoms, and formulas. For any substitution σ applied to a formula F, we use the notation F[σ ] instead of Fσ .

Deductive sequent-based inference rules. The proof derivations are built from sequents [START_REF] Gentzen | Untersuchungen über das logische Schließen[END_REF] of the form Γ ∆, where Γ and ∆ are finite multisets of formulas called antecedents and succedents, respectively. FV (Γ ∆) denotes its set of free variables. An inference rule is represented by a horizontal line followed by the name of the rule. The line separates the lower sequent, called conclusion, from a (potentially empty) multiset of upper sequents, called premises. Most of the rules introduce an explicitly represented formula from the conclusion, called principal formula. In this case, the rules are annotated by L (resp., R) if the rule is introduced on the left (resp, right) of the symbol from the conclusion.

A specification is built from a finite inductive definition set of axioms Φ consisting of formulas of the form

h m=1 Q m (u m ) ∧ l m=1 P m (t m ) ⇒ P(t), (1)
where h, l are naturals, Q 1 , . . . , Q h are ordinary predicate symbols, P 1 , . . . , P l , P are inductive predicate symbols. 0 m=1 is a shortcut for the 'true' boolean constant and can be ignored. The deductive part of the sequent-based reasoning about FOL ID is performed using the Gentzen's LK rules [START_REF] Gentzen | Untersuchungen über das logische Schließen[END_REF] and an 'unfold' rule. The unfold rule (R.(rname)) replaces an atom P(t ) using the axiom (rname) defining P. E.g., (1) can be applied on Γ P(t ), ∆ if P(t ) ≡ P(t)[σ ] for some substitution σ , as:

seq Q inst seq P inst (R.(1)) , Γ P(t ), ∆ where seq Q inst (resp., seq P inst) is the multiset of sequents h m=1 {Γ Q m (u m )[σ ], ∆} (resp., l m=1 {Γ P m (t m )[σ ], ∆}).
Semantics. The standard interpretation of inductive predicates is built from prefixed points of a monotone operator issued from the set of axioms representing Φ [START_REF] Aczel | An introduction to inductive definitions[END_REF]. Its least prefixed point, approached by an iteratively built approximant sequence, helps defining a standard model for (Σ, Φ) (see, e.g., [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] for details).

Definition 1 (validity). Let M be a standard model for (Σ, Φ), Γ ∆ a sequent and ρ a valuation which interprets in M the variables from FV (Γ ∆). We write Γ |= M ρ ∆ if every G ∈ Γ holds in M there is some D ∈ ∆ that also holds in M. We say that Γ ∆ is M-true and write Γ |= M ∆ if Γ |= M ρ ∆, for any ρ. When M is implicit from the context, we use true instead of M-true. A rule is sound, or preserves the validity, if its conclusion is true whenever its premises are true. Hence, the conclusion of every 0-premise sound rule is true.

The CLKID ω

N cyclic inference system

CLKID ω [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] includes the LK rules, the rules from Figure 1 that process equalities, the 'unfold' rule and the (Case) rule which represents a left-introduction operation for inductive predicate symbols:

case distinctions (Case P(t )) Γ, P(t ) ∆

For each axiom of the form (1), is the case distinction for which each free variable y from (1) is fresh w.r.t. the free variables from the conclusion of the rule (y can be renamed to a fresh variable, otherwise). P 1 (t 1 ), . . . , P l (t l ) are case descendants of P(t ).

Γ,t = t, Q 1 (u 1 ), . . . , Q h (u h ), P 1 (t 1 ), . . . , P l (t l ) ∆ (2)
(= R) Γ t = t, ∆ Γ[{x → u; y → t}] ∆[{x → u; y → t}] (= L) Γ[{x → t; y → u}],t = u ∆[{x → t; y → u}]
The inference system CLKID ω N , introduced in [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF], is the restricted version of CLKID ω for which (= L) is replaced by the generalization rule (Gen) that substitutes a term by a variable:

Γ [{t → u}] ∆ [{t → u}] (Gen) Γ ,t = u ∆
where t is a free variable that does not occur in u.

(Gen) is the particular instance of (= L) from Figure 1 when y ∈ FV (Γ ∆) and t ∈ FV (Γ ∆) that also does not occur in u. By using the property that Φ[{y → u}] ≡ Φ, holding whenever y is a free variable not occurring in a formula Φ, the last condition can simplify (= L) to a form equivalent to (Gen):

Γ[{x → u}] ∆[{x → u}] (= L) Γ[{x → t}],t = u ∆[{x → t}] CLKID ω
N pre-proof trees. A derivation tree for a sequent S is built by successively applying inference rules starting from S. We consider only finite derivation trees whose terminal nodes can be either leaves or buds. The leaves are labelled by sequents that represent conclusions of 0-premise rule, e.g., the unfold rule using unconditional axioms. For each bud there is another node, called companion and having the same sequent labelling. The bud and its companion are annotated by the same sign, e.g., †. In addition, the buds having a same companion are labelled by the sign followed by a number that makes them unique, e.g., †1, †2,. . . . A back-link is a relation bud-companion.

Notation 1 (pre-proof tree, induction function for tree). The pair (D, R) denotes a pre-proof tree, where D is a finite derivation tree and R is a defined induction function assigning a companion to every bud in D.

Example 1. To highlight the changes w.r.t. [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF], we take the same running example (also presented in [START_REF] Brotherston | A generic cyclic theorem prover[END_REF]). Let N and R be two inductive predicates defined by:

⇒ N(0) (3) N(x) ⇒ N(sx) (4) ⇒ R(0, y) (5) R(x, 0) ⇒ R(sx, 0) (6) R(ssx, y) ⇒ R(sx, sy) (7)
where the parentheses around the argument of s are omitted. One can build the following pre-proof of N(x), N(y) R(x, y):

(R.( 5
)) Ny R(0, y) (R.(5)) R(0, 0) Nx R(x , 0) ( †1) (Subst) Nx R(x , 0) (R.(6)) Nx R(sx , 0) (Case N) Nx R(x , 0) ( †) (R.(6)) Nx R(sx , 0) Nx, Ny R(x, y) ( * 1) (Subst) Nssx , Ny R(ssx , y ) (Cut) Nx , Ny R(ssx , y ) (R.(7)) Nx , Ny R(sx , sy ) (Case N) Nx , Ny R(sx , y) (Case N) Nx, Ny R(x, y) ( * )
where the double line means that (Gen) was applied after (Case) and the principal formulas of the (Case) steps are underlined. (Cut) is applied as in [START_REF] Brotherston | A generic cyclic theorem prover[END_REF]. For lack of space, the parentheses around the argument of N are omitted.

We denote by S(N) the sequent labelling any node N. A path is a list [N 0 , N 1 , . . .] of nodes in a pre-proof tree such that, for all i ≥ 0, S(N i+1 ) is either one of the premises of the rule applied on

S(N i ) if N i is not a terminal node, or S(R(N i )) if N i is a bud.
Definition 2 (Trace, Progress point [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF]). Let (D, R) be a CLKID ω N pre-proof tree and let [N 0 , N 1 , . . .] be one of its infinite paths and denoted by l. A trace following l is a sequence (τ i ) i≥0 of inductive antecedent atoms (IAAs) such that, for all i, we have that N i is labelled by Γ i ∆ i and:

1. τ i is some P j i (t i ) ∈ Γ i ; 2. if Γ i ∆ i is the conclusion of (Subst) then τ i = τ i+1 [θ ],
where θ is the substitution used by the LK's (Subst) rule defined as:

Γ ∆ (Subst) Γ[θ ] ∆[θ ]
3. if Γ i ∆ i is the conclusion of (Gen) having t = u as principal formula, there is a formula F such that τ i = F and τ i+1 = F[{t → u}];

4. if Γ i ∆ i is the conclusion of a (Case) rule then either a) τ i+1 = τ i , if τ i is not the principal formula of the rule instance, or b) τ i is the principal formula and τ i+1 is a case descendant of τ i . In the latter case, i is said to be a progress point of the trace;

5. if Γ i ∆ i is the conclusion of any other rule then τ i+1 = τ i .

Remark 1. Non-equality relations between (instances of) τ i and τ i+1 in the above definition are possible only when i is a progress point.

Remark 2. Condition 3 is an abbreviated form of the case dealing with (= L) in Definition 5.4 from [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF], by applying the discussed restrictions to

(= L), i.e., if Γ i ∆ i is the conclusion of (= L), of the form Γ[{x → t; y → u}],t = u ∆[{x → t; y → u}]
and having t = u as principal formula, there is a formula F such that τ i = F [{x → t; y → u}] and τ i+1 = F [{x → u; y → t}] under the following conditions: y ∈ FV (Γ i \{t = u} ∆ i ), t is a free variable not occurring in u and t ∈ FV (Γ ∆).

An infinitely progressing trace is a trace with infinitely many progress points.

3 The criterion for validating the soundness of CLKID ω N pre-proofs

The proof that some cyclic pre-proof is sound is done by using a Descente Infinie argument. The general technique is to assume, by contradiction, that the root of a pre-proof is labelled by a false sequent. Then, we have to show that there is an infinite path of nodes in the pre-proof for which there is an infinite progressing trace following some tail of it. This means that all successive steps in the tail are decreasing and the steps corresponding to the progress points are strictly decreasing w.r.t. some semantic ordering over ordinals. We get a contradiction because it is not possible to built an infinite strictly decreasing sequence of ordinals.

Since the inference rules are sound, an infinite path of nodes labelled by false sequents should exist in the pre-proof whenever its root sequent is false. A sufficient criterion for validating the soundness of CLKID ω pre-proofs is the global trace condition [START_REF] Brotherston | Cyclic proofs for first-order logic with inductive definitions[END_REF][START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF][START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF]: for every infinite path, there is an infinitely progressing trace following some tail. A different sufficient criterion for validating the soundness of CLKID ω N pre-proofs was given in [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF]; it defines ordering and derivability conditions to be satisfied by the digraph representing some normal form of the pre-proof. The normalisation procedure transforms the pre-proof into a set of pre-proof trees, for short pre-proof tree-sets, such that the root of the pre-proof is among the roots of the trees from the normal form. If the sequent labelling the root of the pre-proof is false, one can build an infinite path in the digraph, whose nodes are labelled by false sequents and for which there is an infinite progressing trace following some tail of it.

In the following, we present an improved version of the criterion from [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF].

Normalising pre-proof trees

The normalisation process consists in the exhaustive application of the following three operations. The first operation applies on an internal node labelled by some premise of (Subst), of the form . . .

Γ ∆ (Subst) Γ[σ ] ∆[σ ] . . .
The result is displayed in Figure 2. The internal node is duplicated and the subtree derivation rooted by it is detached to become a new tree derivation. At the end, we get two distinct pre-proof trees. The two occurrences of the duplicated node establish a new bud-companion relation.

Γ ∆ ( * 1) (Subst) Γ[σ ] ∆[σ ] . . . . . . Γ ∆ ( * ) (new tree)
Figure 2: The result of the first operation.

The second operation applies on a non-root companion which is duplicated and the subtree derivation rooted by it becomes a new pre-proof tree. The result is displayed in Figure 3. The sequent labelling the copy of the companion ( * ) becomes the conclusion of a new (Subst) rule. The substitution used by the new (Subst) rule is chosen such that its premise labels a new bud node labelled by the same sequent as the conclusion, e.g., the empty substitution. The new bud node will have (*) assigned as companion.

The last operation applies on a bud node labelled by some sequent that is the premise of a rule r different from (Subst) such that

Γ ∆ ( * 1) (Subst) Γ ∆ . . . . . . Γ ∆ ( * ) (new tree)
Figure 3: The result of the second operation.

Γ ∆ ( * 1) r is transformed to Γ ∆ . . . Γ ∆ ( * 1) (Subst) Γ ∆ r Γ ∆ . . .
Let ( * ) denote the companion of the bud node. A new application of (Subst) with the empty substitution was performed on the bud sequent such that the node labelled by its premise becomes the new bud node whose companion is ( * ).

Compared with the normalisation procedure from [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF], the two procedures share only the first operation. The procedure from [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF] also includes an operation that applies on non-root companions but does not include the (Subst)-step from Figure 3. It does not have an equivalent transformation for the third operation.

The following properties, related to the normalisation process and the resulted normal form as given by Lemmas 1 and 2, are satisfied.

Lemma 1 (termination). The normalisation process terminates.

Proof. The number of nodes that can be processed by the three operations is finite, for every pre-proof tree. In addition, it decrements after applying each operation.

The induction function is extended to allow new bud-companion relations between nodes from different pre-proof trees.

Definition 3 (rb-path, IH-node). An rb-path is a path of the form [R, . . . , H, B] that leads the root R to a bud B in some pre-proof tree of a pre-proof tree-set such that B is the only bud in the path. We will call H an inductive hypothesis node (for short, IH-node).

A path in a pre-proof tree-set (M D, M R) is a list [N 0 , N 1 , . . .] of nodes in M D such that, for all i ≥ 0, S(N i+1 ) is one of the premises of the rule applied on S(N

i ) if N i is an internal node, or S(M R(N i )) if N i is a bud. Lemma 2.
The normalisation of any pre-proof (D, R) of a sequent S builds a pre-proof tree-set (M D, M R)

1. that has a pre-proof tree rooted by a node labelled by S, and 2. for which each of its rb-paths [R, . . . , B] has B as the only node that is labelled by the premise of a (Subst) rule. A node is a (Subst)-node if and only if it is an (IH)-node.

Proof. Claim 1) holds because the first operation duplicates only non-root nodes and the third operation expands bud nodes, so the root nodes do not change. If S labels the root node of a pre-proof tree t having a non-root companion n, t will be processed by the second operation applied on n but will still have its root labelled by S.

Claim 2) holds by the construction of the normal forms.

Example 2. The second operation can be applied on the non-root companion from Example 1, denoted by ( * ), to give the following normalised pre-proof tree-set:

(R.( 5
)) Ny R(0, y) Nx R(x , 0) ( †1) (Subst) Nx R(x , 0) (R.( 6
)) Nx R(sx , 0) Nx, Ny R(x, y) ( * ) (Subst) Nssx , Ny R(ssx , y ) (Cut) Nx , Ny R(ssx , y ) (R.(7)) Nx , Ny R(sx , sy ) (Case N) Nx , Ny R(sx , y) (Case N) Nx, Ny R(x, y) ( * ) (R.(5)) R(0, 0) Nx R(x , 0) ( †) (Subst) Nx R(x , 0) (R.( 6
)) Nx R(sx , 0) (Case N) Nx R(x , 0) ( †)

Building the digraph of a pre-proof tree-set

Any pre-proof tree-set can also be represented as a digraph of sequents built from the nodes of its treeset. The digraph associated to a pre-proof tree-set (M D, M R) is crucial in our setting to check whether (M D, M R) is a proof tree-set. Its edges are arrows built as follows:

• a forward arrow leads a node N 1 to a node N 2 if there is a rule that was applied on the sequent labelling N 1 and the sequent labelling N 2 is a premise of the rule;

• a back-link (or backward arrow) starts from a bud and ends to its companion. Some arrows will be annotated by substitutions. Each forward arrow, starting from a (Gen)-node whose principal formula is x = u, is annotated by the equality substitution {x → u}. The forward arrow starting from a node N that is different from (Gen)and (Subst)-nodes is annotated with the identity substitution for S(N), which maps the free variables from S(N) to themselves. Finally, the forward arrows starting from (Subst)-nodes and the back-links are not annotated. They help to build infinite paths but do not play any role when defining the soundness constraints.

By abuse of notation, a path in a digraph is a (potentially infinite) list of nodes built by following the arrows in the digraph. An rb-path is any path leading a root to some bud node and does not have other bud nodes. Unless otherwise stated, we will consider only rb-paths in the digraphs associated to normalised pre-proof tree-sets. Remark 3. According to Lemma 2, the bud node B of any such rb-path is the only node in the rb-path for which S(B) is the premise of a (Subst) rule.

Definition 4 (cumulative substitution

). An rb-path [N 1 , . . . , N n , B] (n > 0) can be annotated by the cumulative substitution σ all id σ 1 • • • σ n-1 , where σ i is the substitution annotating the forward arrow leading N i to N i+1 , for each i ∈ [1..n -1], and σ all id is the overall identity substitution

∪ N∈[N 1 ,...,N n-1 ] {x → x | x ∈ FV (S(N))}.
A list of sequents [S 1 , . . . , S n ] (n > 0) is admissible if either i) it is a singleton (n = 1), or ii) for every i ∈ [2..n], S i is the premise of some rule whose conclusion is S i-1 . By construction, the list of sequents labelling the nodes from every path from the digraph associated to a pre-proof tree-set is admissible. Lemma 3. Let [N 1 , . . . , N n-1 , N n , B] be an rb-path.

We define its cumulative list l c as

[S(N 1 )[θ c (1,n) ], . . . , S(N n-1 )[θ c (n-1,n) ], S(N n ), S(B)],
where θ c (i,n) is the cumulative substitution for [N i , . . . , N n-1 , N n ]. Then, the following properties hold:

1. l c is admissible, and 2. the rule applied on each S(N i ) is also applicable on S(N

i )[θ c (i,n) ], ∀i ∈ [1..n -1], if it is different from (Gen).
If the rule is (Gen), the (Gen)-step can be replaced by a (W k)-step, where the LK's (W k) rule is defined as

Γ ∆ (W k) if Γ ⊆ Γ, ∆ ⊆ ∆ Γ ∆
Proof. We will perform induction on n. If n = 1, then N n ≡ N 1 and [S(N 1 )] is a singleton, hence it is admissible.

If n > 1, let p denote the path [N 1 , . . . , N n-1 , N n , B]. By induction hypothesis, we assume that

[S(N 1 )[θ c (1,n-1) ], . . . , S(N n-2 )[θ c (n-2,n-1) ], S(N n-1 )] is admissible, where θ c (i,n-1) (i ∈ [1..n -2]
) is the cumulative substitution annotating [N i , . . . , N n-1 ] and the rules applied on S(N i )[θ c (i,n-1) ] and S(N i ) are the same. We denote by θ c (n-1,n-1) the identity substitution for S(N n-1 ). Let θ c (i,n) be the cumulative substitution annotating [N i , . . . , N n-1 , N n ], for all i ∈ [1..n -1]. Let also θ be the substitution annotating the forward arrow leading N n-1 to N n , which can be either an identity substitution, or an equality substitution. In the first case, for every

i ∈ [1..n -1], θ c (i,n) is i) θ c (i,n-1) ∪ {x → x | x ∈ x} if the rule applied on S(N n-1
) is the LK's rule (∀R) or (∃L), defined below:

Γ F, ∆ (∀R) if x ∩ FV (Γ ∪ ∆) = / 0 Γ ∀xF, ∆ Γ, F ∆ (∃L) if x ∩ FV (Γ ∪ ∆) = / 0 Γ, ∃xF ∆
and x is the vector of new free variables introduced by these rules, or ii) θ c (i,n-1) , otherwise. Since S(N i )[θ c (i,n-1) ] ≡ S(N i )[θ c (i,n) ] by induction hypothesis, we can apply the same rules on S(N i )[θ c (i,n) ] and S(N i ), hence the list

[S(N 1 )[θ c (1,n) ], . . . , S(N n-1 )[θ c (n-1,n) ], S(N n )] is admissible. [S(N 1 )[θ c (1,n) ], . . . , S(N n-1 )[θ c (n-1,n) ], S(N n ), S(B)
] is also admissible since S(B) is the premise of a (Subst) rule whose conclusion is S(N n ), by property 2) from Lemma 2.

For the second case, θ is an equality substitution. We have that θ c (i,n) equals θ c (i,n-1) θ , for all i ∈ [1..n -1]. Since the rule applied on a sequent can also be applied on every instance of it, we have that

[S(N 1 )[θ c (1,n) ], . . . , S(N n-1 )[θ c (n-1,n) ], S(N n )] is admissible; the rule applied on S(N i ) can also be applied on S(N i )[θ c (i,n) ], for all i ∈ [1..n -1].
Notice that the (Gen) rule has S(N n ) as premise when applied on

S(N n-1 )[θ c (n-1,n) θ ]. Let us assume that x = u is the principal formula of S(N n-1 )[θ c (n-1,n) ].
Then, θ is {x → u}. On the one hand, (Gen) cannot be applied on S(N n-1 )[θ c

(n-1,n) θ ], whose principal formula is u = u, when u is a non-variable term. On the other hand, the generalised form of (Gen) from CLKID ω , displayed in Figure 1, would replace u by u and delete u = u. If S(N n-1 )[θ c

(n-1,n) θ ] is of the form Γ, u = u ∆, the same result can be achieved with CLKID ω N by applying (W k) instead:

Γ ∆ (W k) Γ, u = u ∆ So, the list [S(N 1 )[θ c (1,n) ], . . . , S(N n-1 )[θ c (n-1,n) ], S(N n )] is admissible. [S(N 1 )[θ c (1,n) ], . . . , S(N n-1 )[θ c (n-1,n) ], S(N n ), S(B)
] is also admissible, as shown for the first case.

A path has cycles if some nodes are repeated in the path. The set of strongly connected components (SCCs) of a digraph P of some pre-proof tree-set (M D, M R) is a partition of P, where each SCC is a maximal sub-graph for which any two different nodes are linked in each direction by following only arrows from the sub-graph. Therefore, every non-singleton SCC has at least one cycle. Additionally, if P is acyclic, each of its nodes is a singleton SCC.

Example 3. The digraph of the normalised pre-proof tree-set from Example 2 is:

Nx, Ny 1 R(x, y) {x →0} z z {x →sx } 9 9 Ny 2 R(0, y) Nx , Ny 3 R(sx , y) {y →0} 8
8
{y →sy } Nx , Ny 5 R(sx , sy )

Nx 4 R(sx , 0) Nx 10 R(x , 0) {x →0} z z {x →sx } Nx , Ny 6 R(ssx , y ) π Nx 9 R(x , 0) G G 11 R(0, 0) Nx 12 R(sx , 0) π Nssx , Ny 7 R(ssx , y ) Nx 13 R(x , 0) Nx, Ny 8 R(x, y) p p Nx 14 R(x , 0) b b
The sequent labelling a node is annotated by the number of the node in the digraph. The digraph has two non-singleton SCCs: i) π:{N 10 , N 12 , N 13 , N 14 }, and ii) π : {N 1 , N 3 , N 5 , N 6 , N 7 , N 8 }.

Defining the ordering and derivability conditions

The premises for defining the new soundness criterion are similar to [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF]. Let π be a SCC from P and < a an ordering stable under substitutions defined over the set S of instances of the IAAs from the sequents labelling nodes inside π, i.e., if l < a l then l[σ ] < a l [σ ], for all l, l ∈ S and substitution σ . Given a path p in π, we say that an IAA τ j derives from an IAA τ i using the trace (τ k ) (k≥0) along p if i < j. Also, given two arbitrary substitutions γ and δ , we say that

τ j [γ] derives from τ i [δ ] using (τ k ) (k≥0) along p. < π is the multiset extension [2] of < a .
The ordering constraints from a multiset extension relation comparing two sequent instances can be combined with derivability constraints on IAAs to give the < π -derivability relation, referred to as ordering-derivability when the ordering is not known. For this, we assume that every sequent S has associated a measure value (weight), denoted by A S and represented by a multiset of IAAs of S. Definition 5 (< π -derivability). Let N i and N j be two nodes occurring in some path p from π, and θ , δ be two substitutions. We define A S(N i )[θ ] (resp., A S(N j )[δ ] ) as the multiset, resulting from A S(N i )[θ ] (resp., A S(N j )[δ ] ) after the pairwise deletion of all common IAAs from A S(N i )[θ ] and A S(N j ) [δ ] . In addition, we assume that for each l ∈ A S(N j )[δ ] \A S(N j )[δ ] , there is l ∈ A S(N i )[θ ] \A S(N i )[θ ] satisfying i) l ≡ l , and ii) l is the unique literal from A S(N j )[δ ] that derives from l using some trace following p.

Then, S(N j )[δ ] is < π -derivable from S(N i )[θ ] along p if for each l ∈ A S(N j )[δ ] there exists l ∈ A S(N i ) [θ ] such that l > a l and l derives from l using some trace following p.

By the definition of < π as a multiset extension of < a , the following results can be proved when considering some path in π. Lemma 4. If S is < π -derivable from S then A S < π A S .

Proof. By the definition of the ordering constraint in the < π -derivability relation.

Lemma 5. The '< π -derivability' relation is stable under substitutions and transitive.

Proof. Let S and S be two sequents such that S is < π -derivable from S along some path p in π. By Lemma 4, A S > π A S . Since < π is stable under substitutions, we have that A S [σ ] > π A S[σ ] , for every substitution σ . According to Definition 5, the derivability relations between their IAAs do not change by instantiation operations. Therefore, S[σ ] is < π -derivable from S [σ ] along p. We conclude that the '< π -derivability' relation is stable under substitutions.

To prove the transitivity property, let us assume three sequents S 1 , S 2 and S 3 labelling nodes in a path p built by the concatenation of two paths p 1 and p 2 such that S 3 is < π -derivable from S 2 along p 2 and S 2 is < π -derivable from S 1 along p 1 . We will try to prove that S 3 is < π -derivable from S 1 along p.

Since S 3 is < π -derivable from S 2 along p 2 , by Definition 5 we have that (i1) for each l 3 ∈ A S 3 there exists l 2 ∈ A S 2 such that l 2 > a l 3 and l 3 derives from l 2 using some trace following p 2 , and (ii1) for each l 3 ∈ A S 3 \A S 3 , there is some l 2 ∈ A S 2 \A S 2 such that l 3 ≡ l 2 and l 3 is the unique IAA that derives from l 2 using some trace following p 2 , where A S 3 (resp., A S 2 ) is the multiset resulting from A S 3 (resp., A S 2 ) after the pairwise deletion of all common IAAs from A S 3 and A S 2 . Also, since S 2 is < π -derivable from S 1 along p 1 , we have that (i2) for each l 2 ∈ A S 2 , there exists l 1 ∈ A S 1 such that l 1 > a l 2 and l 2 derives from l 1 using some trace following p 1 , and (ii2) for each l 2 ∈ A S 2 \A S 2 , there is some l 1 ∈ A S 1 \A S 1 such that l 2 ≡ l 1 and l 2 is the unique IAA that derives from l 1 using some trace following p 1 , where A S 2 (resp., A S 1 ) is the multiset resulting from A S 2 (resp., A S 1 ) after the pairwise deletion of all common IAAs from A S 2 and A S 1 . We have to check that for each l 3 ∈ A S 3 , there exists l 1 ∈ A S 1 such that l 1 > a l 3 and l 3 derives from l 1 using some trace following p, where A S 3 (resp., A S 1 ) is the multiset resulting from A S 3 (resp., A S 1 ) after the pairwise deletion of all common IAAs from A S 3 and A S 1 . Moreover, for each l 3 ∈ A S 3 \A S 3 , there is some l 1 ∈ A S 1 \A S 1 such that l 3 ≡ l 1 and l 3 is the unique IAA that derives from l 1 using some trace following p. We consider the following cases:

1. If l 3 ∈ A S 3 there exists l 2 ∈ A S 2 such that l 2 > a l 3 and l 3 derives from l 2 using some trace t 2 following p 2 .

(a) If l 2 ∈ A S 2 there exists l 1 ∈ A S 1 such that l 1 > a l 2 and l 2 derives from l 1 by using some trace t 1 following p 1 . Then l 1 > a l 3 by the transitivity of < a , so l 1 ∈ A S 1 , l 3 ∈ A S 3 and l 3 derives from l 1 using the concatenation of t 1 and t 2 following p. (b) If l 2 ∈ A S 2 \A S 2 , there is l 1 ∈ A S 1 \A S 1 such that l 2 ≡ l 1 and l 2 is the unique IAA that derives from l 1 by using some trace t 1 following p 1 . Since l 1 (≡ l 2 ) > a l 3 , we have that l 1 ∈ A S 1 , l 3 ∈ A S 3 and l 3 derives from l 1 using the concatenation of t 1 and t 2 following p.

2. If l 3 ∈ A S 3 \A S 3 there exists l 2 ∈ A S 2 such that l 3 ≡ l 2 and l 3 is the unique IAA that derives from l 2 using some trace t 2 following p 2 .

(a) If l 2 ∈ A S 2 there exists l 1 ∈ A S 1 such that l 1 > a l 2 and l 2 derives from l 1 by using some trace t 1 following p 1 . Then, l 1 > a (l 2 ≡)l 3 , so l 1 ∈ A S 1 , l 3 ∈ A S 3 and l 3 derives from l 1 using the concatenation of t 1 and t 2 following p.

(b) If l 2 ∈ A S 2 \A S 2 there exists l 1 ∈ A S 1 such that l 1 ≡ l 2 and l 2 is the unique IAA that derives from l 1 by using some trace t 1 following p 1 . This means that l 3 ∈ A S 3 \A S 3 , l 1 ∈ A S 1 \A S 1 with l 1 ≡ (l 2 ≡)l 3 and l 3 derives from l 1 using the concatenation of t 1 and t 2 following p. In addition, l 3 is the unique IAA in A S 3 that derives from l 1 .

The soundness criterion consists in checking if the sequents labelling (IH)-nodes from every nonsingleton SCC, referred to as induction hypotheses, satisfy some constraints.

Definition 6 (induction hypothesis (IH), IH discharged by a SCC). Let π be a non-singleton SCC and [R, . . . , H, B] an rb-path p in π. We say that the induction hypothesis (IH) S(H) is discharged by π if S(H) is < π -derivable from S(R)[θ c ] along p, where θ c is the cumulative substitution annotating p.

Theorem 1 (soundness). The sequents, labelling the roots from every normalised pre-proof tree-set whose non-singleton SCCs discharge their IHs, are true.

Proof. Let M be a standard model for (Σ, Φ) and assume a normalised pre-proof tree-set. Let also P denote its digraph whose non-singleton SCCs discharge their IHs. By contradiction, we assume that there exists a root node N such that S(N) is false. We define a partial (well-founded) ordering < R over the (finite number of) root nodes from P such that, for every two distinct root nodes N 1 and N 2 , we have N 1 < R N 2 if i) N 1 and N 2 are not in the same SCC, and ii) N 1 can be joined from N 2 in P.

By induction on < R , we consider the base case when N is a < R -minimal node. (The step case, when N is not a < R -minimal node, will not be detailed since it can be treated similarly by assuming that all < R -smaller root nodes are labelled by true sequents.) If N is included in a one-node SCC, N is also a leaf node. The only 0-premise rules are the LK's (Ax) rule as well as (R.) when unfolding with unconditional axioms. In both cases, S(N) is true which leads to a contradiction.

Let us now assume that N is a < R -minimal node from some non-singleton SCC π. We will analyse all possible scenarios and show that each of them leads to a contradiction. The tree t from P and rooted by N should have buds labelled by false sequents, otherwise S(N) would be true. Let B be such a bud such that N h is its companion and [N, . . . , H, B] is an rb-path in π. N h should be a root node from π because N is < R -minimal; it is labelled by the false sequent S(B). Since the CLKID ω N rules are sound, by Lemma 3, we conclude that the cumulative instance S(N)[θ c ] is false, where θ c is the cumulative substitution for [N, . . . , H, B]. π discharges its IHs, so we have that S(B)[δ h ](≡ S(H)) is < π -derivable from S(N)[θ c ], where δ h is the substitution used by the (Subst)-step whose conclusion is S(H). By Lemma 4, we have that A S(N h )[δ h ] < π A S(N)[θ c ] .

We perform a similar reasoning on N h as for N. There is an rb-path [N h , . . . , H , N f ] such that the companion of N f (in π) is N h and S(N h )[δ h ] shares false instances with S(N h )[θ c 1 ], where θ c 1 is the cumulative substitution annotating [N h , . . . , H , N f ]. By contradiction, we assume that no false instance of S(N h )[δ h ] is shared. Then, one can build a finite bud-free pre-proof tree of S(N h )[δ h ], by using only sound rules. Hence, S(N h )[δ h ] is true, so contradiction. Therefore, there are two substitutions ε and τ such that S(N h )[δ h ε] ≡ S(N h )[θ c We have defined a more efficient soundness criterion for a class of CLKID ω pre-proofs considered in [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF], by building a set of non-redundant ordering-derivability constraints. We have shown that these constraints can also be extracted from those that define the soundness criterion from [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF], by deleting the duplicated values. The new normal forms and their digraphs allow to uniformly represent rb-paths and can be built in linear time. We conclude that the two soundness checking criteria have the same polynomial-time complexity if the time complexity for comparing two IAAs is at most polynomial.

In the future, we plan to adapt our approach to make more effective other soundness criteria based on minimal cycles, e.g., those involving cyclic formula-based Noetherian induction reasoning [START_REF] Stratulat | A unified view of induction reasoning for first-order logic[END_REF][START_REF] Stratulat | Mechanically certifying formula-based Noetherian induction reasoning[END_REF], and other systems where the soundness can be checked by the global trace condition, as CLJID ω [START_REF] Berardi | Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs[END_REF].

Figure 1 :

 1 Figure 1: Sequent-based rules for equality reasoning.

  1 τ] and S(N h )[θ c 1 τ] is false. Let S(N h )[δ h ](≡ S(H )) be the instance of S(N h ) used as IH. Since it is discharged by π, we have that A S(N h )[θ c 1 ] > π A S(N h )[δ h ] . From A S(N)[θ c ] > π A S(N h )[δ h ]4 Conclusions and future work

for example, by applying the LK's (Subst) rule with an identity substitution (see the definition of (Subst) in Definition

2).

Acknowledgements

The author thanks the anonymous reviewers for their comments that helped to improve the quality of the paper.

and the previous ordering constraint, we get A S(N)[θ c ε] > π A S(N h )[δ h ε] and A S(N h )[θ c

1 τ] > π A S(N h )[δ h τ] , by the 'stability under substitutions' property of < π . Hence,

For similar reasons as given for S(N h )[δ h ], we can show that S(N h )[δ h τ] is false, hence it can be treated similarly as S(N h )[δ h ]. And so on, the process can be repeated to produce an infinite strictly < π -decreasing sequence s of measure values associated to instances of sequents labelling root nodes from π, of the form

. . We can associate to s the infinite admissible list l s of its sequents

. .] and define the path p underlying l s as the concatenation of the rb-paths from π that built s, i.e., [N, . . . , B, N h , . . . , N f , . . .]. By the construction of s, every successive (Subst)-, bud and root nodes in p are labelled by the same sequent instance in l s , so the (Subst)-steps are stuttering in l s . By Lemma 4, all (Gen)can be replaced by (W k)-steps. p is of the form [N ∞ . . . , N 1 , . . . , N 0 ] where N 0 , N 1 , . . . , N ∞ are an infinite number of all the occurrences of N in p.

We will show that there is a trace following p that has an infinite number of progress points. As explained in [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF], it means that there is an infinite strictly decreasing sequence of ordinals, hence contradiction. Since p is the concatenation of rb-paths in π and π discharges its IHs, for each such rb-path the bud sequent is < π -derivable from the cumulative instance, along the rp-path, of the root sequent. By Lemma 5, there is an instance S(N ∞ )[θ ∞ ] such that S(N 0 ) is < π -derivable from it along p, where θ ∞ is the composition of all cumulative substitutions of the rb-paths from l. For any two consecutive nodes N i and

where θ i (resp., θ i-1 ) are the compositions of all cumulative substitutions of the rb-paths along

Let us denote by S (resp, S ) the sequent

. By Definition 5 and the transitivity of the < π -derivability relation, for each IAA l from A S there is an IAA l from A S such that l derives from l . Therefore, there are n traces along the path p [N ∞ , . . . , N i ], where n is the number of IAAs from S.

We will show that the traces along p have an infinite number of progress points. By contradiction, we assume that this number is finite. Therefore, there is a subpath p of p whose traces have no progress points and there exists j ∈ [1..∞] such that N j and N j-1 belong to p . Let us denote by S j (resp, S j-1 ) the sequent S(N j )[θ j ] (resp., S(N j-1 )[θ j-1 ]). Since S j-1 is < π -derivable from S j , we have that A S j-1 < π A S j . By the definition of < π as a multiset extension of the ordering < a over the instances of IAAs from the root sequents in π, there should be an IAA l ∈ A S j-1 for which there is another IAA l ∈ A S j such that l < a l and l derives from l , i.e., l and l are from an infinite trace t following (a subpath of) p which has no progress points. According to the definition of a trace (see Definition 2) and the way l s was built, l < a l is possible only if the subtrace of t from l to l has at least one progress point, so contradiction. Otherwise, l ≡ l since i) l s is admissible, ii) the (Subst)-steps are stuttering, iii) the (Gen)-steps can be replaced by (W k)-steps, and iv) the instantiation steps that built s preserve the equality relations.

Example 4. For the sequents labelling the nodes from the digraph given in Example 2, we define the measure values A Nt R(t,0) = {Nt}, ∀t, and A Nt 1 ,Nt 2 R(t 1 ,t 2 ) = {Nt 2 }, ∀t 1 ,t 2 . The IH S(N 13 ) is < π -derivable from S(N 10 )[{x → sx }], hence discharged by the SCC π using the trace [Nx , Nx , Nx ], if {Nx } < π {Nsx }. Also, the IH S(N 7 ) is < π -derivable from S(N 1 )[{x → sx ; y → sy }] in the SCC π using the trace [Ny, Ny, Ny , Ny , Ny , Ny ] if {Ny } < π {Nsy }. The ordering constraints hold if < π and < π are the multiset extensions of a recursive path ordering [START_REF] Baader | Term Rewriting and All That[END_REF] < rpo for which z < rpo sz, for every variable z.

By Theorem 1, the root sequents in the pre-proof tree-set, S(N 1 ) and S(N 10 ), are true.

Comparison with the soundness checking criterion from [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF]. In [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF], the ordering-derivability constraints issued when analysing if a pre-proof tree-set is a proof are defined at the level of the minimal cycles of its digraph, referred to as n-cycles. A n-cycle is defined as a finite circular list [N 1 1 , . . . , N p 1 1 ], . . . , [N 1 n , . . . , N p n n ] of n (> 0) paths leading root nodes to buds such that

Let π be a non-singleton SCC and C an n-cycle [N 1 1 , . . . , N p 1 1 ], . . . , [N 1 n , . . . , N p n n ] from π. The induction hypotheses are defined at the n-cycle level. For all i ∈ [1..n], let θ c i be the cumulative substitution annotating

, otherwise. The sequents labelling the IH-nodes correspond exactly to the induction hypotheses used in the paper. We say that the IHs S(N f j )

In [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF], a proof is every pre-proof tree-set whose digraph has only n-cycles that discharge their IHs and it has been shown that its root sequents are true. Since several n-cycles may share the same root-bud path, some ordering-derivability constraints may be duplicated when checking that a pre-proof is a proof. For example, the path

] from the digraph given in Figure 4. Even if the number of n-cycles from a digraph can be large, as explained in the introduction, the number of distinct ordering-derivability constraints is always smaller or equal than the number of buds from the non-singleton SCCs. With the approach from [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF], the duplicates of the constraints do not need to be again processed if the already processed constraints are recorded. It has been shown that the time complexity of the soundness checking procedure is polynomial if the number of the orderingderivability constraints is that of the buds from the non-singleton SCCs. With our new approach, the number of operations for normalising a CLKID ω N pre-proof of n nodes is given by the sum of non-root companions, non-terminal (Subst)-nodes and nodes labelled by some sequent that is the premise of a rule r different from (Subst). So, it is smaller than 3n. Let c be the maximal cost of an operation, including the node duplication and the creation of a (Subst)-node or bud-companion relation. Their total cost is smaller than 4nc (the second operation duplicates it twice). The costs for annotating substitutions and for evaluating an ordering-derivability constraint are given in [START_REF] Stratulat | Cyclic proofs with ordering constraints[END_REF].


X Nicolas
email: xavier.nicolas@u-pem.fr

E Chénier

G Lauriat

Thermal boundary conditions for convective heat transfer of dilute gases in slip ow regime

Keywords: microuidics, micro-channel, slipping ow, shear stress power, shear work, convection heat transfer, thermal boundary condition

For gaseous ows in the slip ow regime, the power of the viscous stress at the wall is not zero. From the uid domain point of view, it is a sink term, or a lost heat ux, that must be taken into account. It must be added to the diusive heat ux in the uid to appropriately model the heat ux transmitted from the uid to the wall and the temperature eld. The present technical note aims at theoretically establishing the appropriate thermal conditions in a general context: both thick and thin walls are considered as well as for imposed temperature (H1), imposed heat ux (H2) and convective heat transfer (H3) at the wall. Recent validations of this model, resulting from experimental and numerical comparisons of the convective heat transfer at the walls, are briey discussed.

Introduction

In the last decades, the research activities about convective heat transfer in microdevices have rapidly been growing due to the considerable development of engineering applications. The Knudsen number, Kn = λ/L, dened as the ratio of the gas molecular mean-free-path, λ, to a characteristic length scale, L, such as the hydraulic diameter of a duct, allows a measure of the validity of the continuum approach and a classication of the gas ow regimes [START_REF] Gad-El Hak | Fluid mechanics of microdevices -The Freeman scholar lecture[END_REF][START_REF] Karniadakis | Microows and Nanoows -Fundamentals and Simulation[END_REF]. For 0.001 < Kn < 0.1, the ow regime is called the slip-ow regime: the continuum assumption is still valid in the ow core but slip conditions, i.e. velocity slip, temperature jump and thermal creep, must be considered at the solid boundaries of the ow domain, to model the presence of the Knudsen layer (the very thin layer in a thermodynamical non-equilibrium state close to the solid boundary).

The ow eld solution, described by a system of non-linear partial dierential equations (conservation equations resulting from the Newton law, the rst law of thermodynamics and the equation of state), depends on initial and boundary conditions. The expressions of the velocity-slip and thermal jump at solid walls for weakly rareed ows have been established for a long time, by Maxwell [START_REF] Maxwell | On stresses in raried gases arising from inequalities of temperature[END_REF] and Smoluchowski [START_REF] Smoluchowski | Ueber wärmeleitung in verdünnten gasen[END_REF] and discussed since then by many authors. These boundary conditions that allow computing the uid velocity and temperature accounting for the Knudsen layer are commonly used (at rst or second order in Kn) in convective heat transfer modeling [START_REF] Zhang | A review on slip models for gas microows[END_REF][START_REF] Kandlikar | Heat transfer in microchannels -2012 status and research needs[END_REF]. At this stage, there are not major controversies in the heat transfer literature.

However, when Kn > 0.001, in particular for gas ows in microdevices, some changes need to be brought to the expression of the heat ux transmitted through the wall: due to the slip velocity in the Knudsen layer, the power of the viscous stress is not zero at the wall and it must be taken into account in the thermal boundary condition to satisfy the heat ux consevation. This was rst introduced by Maslen [START_REF] Maslen | On heat transfer in slip ow[END_REF] and discussed by Sparrow and Lin [START_REF] Sparrow | Laminar heat transfer in tubes under slip-ow conditions[END_REF]. Since then, only a few authors have taken into account the power of the viscous stress at the wall in their analysis of heat transfer [START_REF] Shi | Chocked ow of low density gas in a narrow parallel-plate channel with adiabatic walls[END_REF][START_REF] Miyamoto | Chocked ow and heat transfer of low density gas in a narrow parallel-plate channel with uniformly heating walls[END_REF][START_REF] Hadjiconstantinou | Dissipation in small gaseous ows[END_REF][START_REF] Ramadan | Pressure work and viscous dissipation eects on heat transfer in a parallel-plate microchannel gas ow[END_REF]. So, as most of the authors neglected this contribution, it was eventually forgotten. Then Hong and Asako [START_REF] Hong | Some considerations on thermal boundary condition of slip ow[END_REF] reiterated its importance in 2010. However, it appears that the heat transfer community still goes on ignoring this boundary condition or uses it erroneously by considering that the imposed heat ux at the wall only balances the diusive ux transmitted to the uid. It can be thus underlined that most of the papers published in the archival literature on forced convective heat transfer in microdevices have provided erroneous values of the wall heat ux (or Nusselt number) or temperature eld due to ill prescribed thermal boundary conditions.

The present technical note specically focuses on the appropriate thermal boundary conditions for ows in microdevices in the slip regime and for rst order slip models. After the work by [START_REF] Maslen | On heat transfer in slip ow[END_REF] [START_REF] Maslen | On heat transfer in slip ow[END_REF] and [START_REF] Sparrow | Laminar heat transfer in tubes under slip-ow conditions[END_REF] [START_REF] Sparrow | Laminar heat transfer in tubes under slip-ow conditions[END_REF], the technical notes by [START_REF] Hadjiconstantinou | Dissipation in small gaseous ows[END_REF] [START_REF] Hadjiconstantinou | Dissipation in small gaseous ows[END_REF] 1 and Hong and Asako (2010) [START_REF] Hong | Some considerations on thermal boundary condition of slip ow[END_REF] and the experimental and numerical verications/validations by Shih et al. (2001) [START_REF] Shi | Chocked ow of low density gas in a narrow parallel-plate channel with adiabatic walls[END_REF] for adiabatic walls, by [START_REF] Miyamoto | Chocked ow and heat transfer of low density gas in a narrow parallel-plate channel with uniformly heating walls[END_REF] [START_REF] Miyamoto | Chocked ow and heat transfer of low density gas in a narrow parallel-plate channel with uniformly heating walls[END_REF] for isoux walls and [START_REF] Nicolas | Gas ow with heat transfer in micro channels: clarications about Nusselt number[END_REF][START_REF] Nicolas | Revisited analysis of gas convection and heat transfer in micro channels: inuence of viscous stress power at wall on Nusselt number[END_REF] [START_REF] Nicolas | Gas ow with heat transfer in micro channels: clarications about Nusselt number[END_REF][START_REF] Nicolas | Revisited analysis of gas convection and heat transfer in micro channels: inuence of viscous stress power at wall on Nusselt number[END_REF] for isothermal walls, we demonstrate here that the power of the viscous stress at the wall must be included in the total heat ux transmitted by the uid to the wall as soon as a slipping ow occurs at the wall.

A general demonstration and expressions of the right boundary conditions are provided. These BC's are established both for thick and thin walls, and for the H1, H2 and H3 boundary condition types. Finally, we briey remind the published validations of the present formulation for parallel-plate channels submitted to H1 or H2 boundary conditions [START_REF] Shi | Chocked ow of low density gas in a narrow parallel-plate channel with adiabatic walls[END_REF][START_REF] Miyamoto | Chocked ow and heat transfer of low density gas in a narrow parallel-plate channel with uniformly heating walls[END_REF][START_REF] Nicolas | Gas ow with heat transfer in micro channels: clarications about Nusselt number[END_REF][START_REF] Nicolas | Revisited analysis of gas convection and heat transfer in micro channels: inuence of viscous stress power at wall on Nusselt number[END_REF].

Figure 1: Notations for the solid wall, the ow domain, the interface, the boundary conditions and the temperature and velocity proles.

2. General expressions of the thermal conditions on a wall/slipping gas interface

In this paper, we only focus on the thermal boundary conditions. For the governing equations and the dynamical boundary conditions appropriate to model ows of compressible dilute gases in the slip ow regime, one can refer to our previous paper [START_REF] Nicolas | Revisited analysis of gas convection and heat transfer in micro channels: inuence of viscous stress power at wall on Nusselt number[END_REF].

Let us rst consider a gas ow domain of volume Ω g with closed surface Γ g ∪ Γ i (Γ g ∩ Γ i = ), in contact along an interface Γ i with a solid wall of thickness e, volume Ω w , and closed surface Γ w ∪ Γ i = Γ w-∪ Γ w,e ∪ Γ w+ ∪ Γ i (Γ w-∩ Γ w,e ∩ Γ w+ ∩ Γ i = ) (Fig. 1). We are interested in writting the thermal conditions at the interface Γ i between the gas ow domain and the solid wall.

To that aim, the energy equations in the gas and the solid are rst integrated, for a steady problem and without source or sink terms for the sake of simplicity.

Note that, even though the drawing in Fig. 1 is two-dimensional and the wall is at, the present demonstration and formulations are general and can be applied to any three-dimensional geometry of the gas ow domain and solid wall.

By noting h the enthalpy and e c = -→ v 2 /2 the kinetic energy per mass unit of the gas, the steady conservation equation of the total energy of the gas writes (cf. page 341 in [START_REF] Bird | Transport Phenomena[END_REF]):

∇.(ρ - → v h + ρ - → v e c -k g ∇T g -τ . - → v ) = 0 (1)
where the viscous stress tensor τ is dened for a Newtonian-Stokes uid by :

τ = µ(∇ - → v + ∇ - → v t ) - 2 3 µ∇. - → v I (2)
and where -→ v , T g , ρ, k g and µ are the velocity, temperature, density, thermal conductivity and dynamical viscosity of the gas. By integrating Eq. ( 1) on Ω g of closed surface Γ g ∪ Γ i (Fig. 1), considering the wall as impermeable ( -→ v .

-→ n = 0 on Γ i ) and using Gauss'theorem, we get:

ˆΓg ρ(h + e c ) - → v -k g ∇T g -τ . - → v . - → n g dΓ g + ˆΓi -k g ∇T g -τ . - → v = - → q i . - → n i dΓ i =Qi = 0 (3)
where -→ n g is the inward normal unit vector on Γ g , directed from the wall to the gas and denoted -→ n i on Γ i . In Eq. ( 3), the rst integral term is the sum of the enthalpy and kinetic energy convective uxes, the conductive heat ux and the power of the viscous stress through the uid boundary Γ g ; the second integral term represents the total heat ux, Q i [W ], transmitted by the uid to the wall through the interface Γ i . By denition Q i is the integral on Γ i of the total local heat ux density,

q i = - → q i . - → n i [W/m 2 ]
, transmitted by the uid through Γ i . Thus q i is the sum of the diusive heat ux density and the power of the viscous stress at the wall:

q i = -k g,i ∇T g,i -τ . - → v g,i . - → n i (4)
where the subscript g, i denotes quantities on the gas side of the gas/wall interface (slip-related quantities associated with the gas molecules in contact with the wall).

In the solid wall, with the used assumptions, the energy equation simply writes:

∇.(-k w ∇T w ) = 0 [START_REF] Zhang | A review on slip models for gas microows[END_REF] with k w and T w the thermal conductivity and temperature of the solid wall. By integrating Eq. ( 5) on Ω w of closed surface Γ w ∪ Γ i with Γ w = Γ w-∪ Γ w,e ∪ Γ w+ (Fig. 1) and using Gauss's theorem, we get:

ˆΓw (-k w ∇T w ) . - → n w dΓ w + ˆΓi (-k w ∇T w ) = - → q i . - → n i dΓ i =Qi = 0 (6)
where -→ n w is the outward normal unit vector on Γ w . Here the rst integral term is the conductive heat ux through the solid boundary Γ w and the second integral is the conductive heat ux through Γ i . This second term thus represents the total heat ux transmitted by the solid through the interface. It is therefore also equal to Q i since, from the continuum mechanics laws, the heat ux is conserved through a zero volume interface without source term. Furthermore, by identication, the heat ux density transmitted locally by the solid wall through the interface is:

q i = (-k w,i ∇T w,i ) . - → n i (7)
where the subscript w, i denotes quantities on the wall side of the interface. Thus, from Eqs. ( 4) and ( 7), the conservation of the heat ux density, q i , transmitted locally, through an innitesimal gas/wall interface dΓ i , writes:

(-k w,i ∇T w,i ) . - → n i = -k g,i ∇T g,i -τ . - → v g,i . - → n i (8)
When solving the energy equations ( 1) and ( 5) to compute the two unknown temperature elds, T g and T w , for the gas and the wall, two interface conditions are necessary. The rst one is given by Eq. ( 8): it expresses the total heat ux conservation through the interface. The second one expresses the temperature jump between the local interfacial temperatures of the solid wall, T w,i , and the gas, T g,i . It reads [START_REF] Sharipov | Data on the velocity slip and temperature jump on a gas-solid interface[END_REF][START_REF] Kandlikar | Heat transfer in microchannels -2012 status and research needs[END_REF]:

T w,i = T g,i -L T ∇T g,i . - → n i (9)
where L T = ξ T λ > 0 is the thermal jump length, with ξ T the temperature jump coecient and λ the gas mean free path. We insist on the fact that the two conditions ( 8) and ( 9) (total heat ux continuity but diusive heat ux discontinuity, and temperature discontinuity) must be simultaneously satised to compute T g and T w .

H1, H2 and H3 thermal boundary conditions for a slipping ow along a thin impermeable wall

The thermal boundary conditions for a slipping ow along a thin impermeable wall (with a zero solid wall thickness) are deduced now. We rst remind the thermal conditions at the external surface of a thick wall (with a non-zero solid wall thickness). Then we make them degenerate towards the thermal conditions for a thin wall.

Three types of thermal boundary conditions are classically applied at the external surfaces of a wall. They are reminded here, referring to Fig. 1 for the used notations:

• H1-imposed surface temperature distribution, T imp :

T w,e = T imp (10)
• H2-imposed heat ux density distribution, q imp = --→ q imp . -→ n w,e :

k w,e ∇T w,e . - → n w,e = q imp (11)
• H3-mixed (Fourier/Robin) boundary condition for convective heat transfer; for instance, if h is a total heat transfer coecient at the wall and T ∞ a reference temperature (e.g. ambiant temperature), it writes:

k w,e ∇T w,e . - → n w,e = h(T ∞ -T w,e ) (12)
where T is the temperature, k the thermal conductivity and the subscript w, e denotes quantities on the wall side of the external surface of the wall of outward normal unit vector -→ n w,e . For thin walls, these thermal boundary conditions are also applied directly at the boundaries of the ow domain when the Knudsen number is less than about Kn = 0.001.

If the thickness, e, of the wall tends to zero, then the energy equation ( 6) in the solid now writes:

-ˆΓw,e (-k w,e ∇T w,e )

= - → q e . - → n w,e dΓ w,e =Qe = ˆΓi (-k w,i ∇T w,i ) = - → q i . - → n i dΓ i =Qi (13)
where, in the rst integral, Γ w,e is the external wall surface of outward normal unit -→ n w,e (= --→ n i ), Q e is the total heat ux and q e = --→ q e . -→ n w,e the local heat ux density transmitted by the wall to the exterior/surroundings. So, under the present assumption (thin wall), the conservation of the heat ux through the wall locally writes q e = q i that is, from Eqs. ( 4) or ( 8):

k w,e ∇T w,e . - → n w,e = k g,i ∇T g,i . - → n w,e + τ . - → v g,i . - → n w,e (14)
As a consequence, the H2 and H3 boundary conditions applied on a thin wall to compute the temperature eld of the gas in the presence of slip at wall, write as follows:

• H2-The imposed heat ux boundary condition, Eq. ( 11), becomes:

k g,i ∇T g,i . - → n i + τ . - → v g,i . - → n i = -q imp (15)
• H3-The mixed boundary condition, Eq. ( 12), with convective heat transfer, becomes:

k g,i ∇T g,i . - → n i + τ . - → v g,i . - → n i = h(T w,e -T ∞ ) (16)
For the H2 and H3 cases, once the temperature eld T g is solved, the interface gas temperature T g,i is known and the temperature of the thin wall, T w,e = T w,i , is computed from Eq. ( 9). The boundary condition [START_REF] Nicolas | Revisited analysis of gas convection and heat transfer in micro channels: inuence of viscous stress power at wall on Nusselt number[END_REF] can thus be rewriten as a function of the gas temperature only as :

(k g,i + hL T )∇T g,i . - → n i + τ . - → v g,i . - → n i = h(T g,i -T ∞ ) (17)
Lastly, the H1 boundary condition applied on a thin wall in the presence of a slipping gas ow writes as follows:

• H1-The imposed temperature boundary condition, Eq. ( 10), becomes:

T g,i -L T ∇T g,i . - → n i = T imp (18)
In this case, once the gas temperature eld T g is solved, the total heat ux density, q w = -→ q w . -→ n i [W/m 2 ], transmitted through the thin wall is given by Eq. ( 4) with q i = q w , that is:

q w = -k g,i ∇T g,i . - → n i dif f usion heat f lux - τ . - → v g,i . - → n i V iscous Stress P ower = q dif f + q V SP (19)
Thus, in the three cases H1, H2 and H3, the total heat ux transmitted through the wall must take into account two contributions: the diusion heat ux, q dif f , and the power of the viscous stress, q V SP , at the wall (see Eqs. ( 15), ( 16) and ( 19)).

H1 boundary condition for a slipping ow along a thick impermeable wall

At last, the case of a thick wall of thickness e and thermal conductivity k w , with a negligible longitudinal conduction heat ux, is considered (i.e. the diusion heat ux in the direction of the tangential unit vector -→ t and through the wall boundaries Γ w-and Γ w+ on Fig. 1 is negligible). In this case, if the problem is steady, the energy equation does not need to be solved in the solid wall. On the other hand, its thermal resistance r th (r th = e/k w for a plane wall) must be accounted for if a H1 condition is applied. Thus, if T imp is imposed at the external wall of the thick wall, equation ( 18) is replaced by the following condition at the gas/wall interface:

T g,i = T imp -r th q w + L T ∇T g,i . - → n i (20)
where q w is given by Eq. [START_REF] Li | Eect of surface radiation on natural convective ows and onset of ow reversal in asymmetrically heated vertical channels[END_REF]. Therefore the H1 condition for this thick wall writes:

T g,i -(r th k g,i + L T ) ∇T g,i . - → n i = T imp + r th τ . - → v g,i . - → n i (21)
Note that the heat ux, q w , transmitted from the uid through the wall is still given by Eqs. ( 15), ( 16) and [START_REF] Li | Eect of surface radiation on natural convective ows and onset of ow reversal in asymmetrically heated vertical channels[END_REF] for the H2, H3 and H1 conditions in this case.

Discussion about the wall heat ux and Nusselt number

The expressions of the imposed heat ux q imp in Eq. ( 15) or total heat ux q w transmitted to the wall in Eq. ( 19) are similar, for instance, to the one when there are coupled convective and radiative thermal exchanges at a wall [START_REF] Li | Eect of surface radiation on natural convective ows and onset of ow reversal in asymmetrically heated vertical channels[END_REF] or when there are both thermal diusion and phase change at a wall due to condensation or evaporation [START_REF] Sun | Natural convection and wall condensation or evaporation in humid air-lled cavities subjected to wall temperature variations[END_REF]. In these two cases, the heat ux density imposed at the wall also balances the total heat ux density transmitted through the wall and it can be written:

q imp = q w = q dif f + q rad = -(k∇T. - → n ) g,i + ( - → q rad . - → n ) g,i radiation heat f lux (22)
q imp = q w = q dif f + q lat = -(k∇T. - → n ) g,i + ( - → q lat . - → n ) g,i latent heat f lux (23)
One important consequence of Eqs. ( 15), ( 16) and ( 19) concerns the Nusselt number denition that should be adopted to compare theory with measurements in experiments on gas convection in the slip ow regime. The Nusselt number should be dened from the total heat ux transmitted by the uid through the wall and not only from the diusive ux at the wall:

N u tot = q w q ref = q dif f q ref + q V SP q ref (24)
that is:

N u tot = N u dif f + N u V SP = -k g,i ∇T g,i . - → n i q ref + -τ . - → v g,i . - → n i q ref (25)
where q ref is a reference heat ux density. For instance, in a micro-channel ow, q ref = k g (T w,i -T b )/D h with T b the average bulk temperature and D h the hydraulic diameter.

The numerical solutions obtained from the above boundary conditions and the full energy equation in its enthalpic form, that is including the viscous dissipation and the pressure work source terms, are validated by comparisons between several experimental data and numerical simulations of the Nusselt numbers. These comparisons are carried out in [START_REF] Shi | Chocked ow of low density gas in a narrow parallel-plate channel with adiabatic walls[END_REF][START_REF] Miyamoto | Chocked ow and heat transfer of low density gas in a narrow parallel-plate channel with uniformly heating walls[END_REF] for adiabatic and isoux micro-channels and in [START_REF] Nicolas | Gas ow with heat transfer in micro channels: clarications about Nusselt number[END_REF][START_REF] Nicolas | Revisited analysis of gas convection and heat transfer in micro channels: inuence of viscous stress power at wall on Nusselt number[END_REF] for isothermal wall micro-channels. The measured values of the Nusselt numbers in [START_REF] Shi | Chocked ow of low density gas in a narrow parallel-plate channel with adiabatic walls[END_REF][START_REF] Miyamoto | Chocked ow and heat transfer of low density gas in a narrow parallel-plate channel with uniformly heating walls[END_REF] are found again by the authors using the full thermal model associated with the boundary condition [START_REF] Nicolas | Gas ow with heat transfer in micro channels: clarications about Nusselt number[END_REF] and Eqs.

(24-25) for the denition of the Nusselt number. In the same way, using a full thermal model, the authors in [START_REF] Nicolas | Gas ow with heat transfer in micro channels: clarications about Nusselt number[END_REF][START_REF] Nicolas | Revisited analysis of gas convection and heat transfer in micro channels: inuence of viscous stress power at wall on Nusselt number[END_REF] show that the very small values of the average Nusselt numbers obtained in the experiments by Demsis et al. [START_REF] Demsis | Experimental determination of heat transfer coecient in the slip regime and its anomalously low value[END_REF][START_REF] Demsis | Heat transfer coecient of gas owing in a circular tube under rareed condition[END_REF] in a quasi isothermal micro-channel can only be explained from the denition (24-25) of N u tot while N u dif f provides Nusselt number values several orders larger than the measured ones. Thus the computation of the diusive Nusselt numbers, N u dif f , reported in the majority of the published papers, cannot provide on its own the convection heat transfer coecients measured in the experiments in the slip ow regime when the power of the viscous stress is not negligible. About the magnitude order of the power of the viscous stress, a dimensional analysis of the dierent terms of the energy equation and thermal boundary conditions is proposed in appendix A of [START_REF] Nicolas | Revisited analysis of gas convection and heat transfer in micro channels: inuence of viscous stress power at wall on Nusselt number[END_REF].

Lastly, note that these thermal boundary conditions including the viscous stress power at the wall must be used in conjunction with the full energy equation containing both the pressure work and the viscous dissipation source terms when gaseous micro-ows in the slip regime are considered [START_REF] Shi | Chocked ow of low density gas in a narrow parallel-plate channel with adiabatic walls[END_REF][START_REF] Miyamoto | Chocked ow and heat transfer of low density gas in a narrow parallel-plate channel with uniformly heating walls[END_REF][START_REF] Ramadan | Pressure work and viscous dissipation eects on heat transfer in a parallel-plate microchannel gas ow[END_REF][START_REF] Nicolas | Revisited analysis of gas convection and heat transfer in micro channels: inuence of viscous stress power at wall on Nusselt number[END_REF]. Indeed, it can be shown that the sum of the pressure work and viscous dissipation source terms are in the same magnitude order as the viscous stress power at the wall [START_REF] Nicolas | Revisited analysis of gas convection and heat transfer in micro channels: inuence of viscous stress power at wall on Nusselt number[END_REF].

Conclusion

This technical note proves that the power of the viscous stress at the wall must be included in the total heat ux transmitted by the uid to the wall, as soon as a slipping ow is present at the wall. Consequently, it must be included in the thermal boundary conditions and also in the denition of the total Nusselt number at the wall, in particular when heat transfer is computed in weakly rareed gaseous ows in micro-devices. The demonstration is established in a general context, for thick and thin walls, and for the H1, H2 and H3 thermal boundary conditions. Experimental and numerical verications of the necessity to take into account the viscous stress power contribution to the wall heat ux are also discussed. To end, one must remember that heat transfer in dilute gases in the slip ow regime implies both a temperature jump and a conduction heat ux jump between the gas and the wall.

Note that q 0 in Eq. (5) of[START_REF] Hadjiconstantinou | Dissipation in small gaseous ows[END_REF] is the thermal heat ux, that is the diusive part of the heat ux exchanged between the wall and the uid, and not the imposed heat ux as considered by some authors[START_REF] Vocale | Shear work contribution to convective heat transfer of dilute gases in slip ow regime[END_REF], which led them to ill-interpretations of the boundary conditions.


Lucas Joseph

Vincent Padois

Guillaume Morel

Experimental validation of an energy constraint for a safer collaboration with robots

In this paper a platform dedicated to the measure of the energy dissipated by a robot during an impact is presented. This platform is used to validate a controller that explicitly constrains the robot kinetic energy thanks to a linear quadratic problem formulation. This constraint is used to ensure safety at the control level by computing intrinsically safe commands that comply with ISO norm 15066 on collaborative robot safety. This platform has been designed to validate this approach in case of a collision with an obstacle and is experimented on a KUKA LWR4+ robot.

Introduction

The further adoption of robots for collaborative tasks with an operator must go through an enhancement of the user safety. To that extent several research projects have been conducted. They led to the introduction of lightweight robots with a reduced mass and torque sensing capabilities [START_REF] Albu-Schäffer | The DLR lightweight robot: design and control concepts for robots in human environments[END_REF], to new variable impedance actuators [START_REF] Bicchi | Fast and "soft-arm" tactics[END_REF] and solutions to detect and avoid obstacles with exteroceptive sensors [START_REF] Fabrizio Flacco | A Depth Space Approach for Evaluating Distance to Objects[END_REF].

Collaborative robots are designed to work closely with humans. To perform their tasks, these robots have torque/force capacities that make them potentially dangerous for human-robot collaboration. A first measure to improve safety in the vicinity of these robots consists in avoiding unwanted contact with humans. Different obstacle avoidance algorithms have been proposed in the literature. [START_REF] Quinlan | Elastic bands: connecting path planning and control[END_REF] expose a technique called elastic bands that updates the robot trajectory on-line to define a collission-free path. Potential fields methods, first introduced by [START_REF] Khatib | Inertial properties in robotic manipulation: An object-level framework[END_REF], create virtual forces around obstacles. The magnitude of these forces is linked to the distance between the robot and an obstacle. Whether obstacle avoidance algorithms are implemented by mean of control or through path planning, in cluttered environments with unpredictable human motions, they cannot guaranty that no contact can happened between a fixed base robot and a human.

If contact cannot be avoided, it should at least be safe for the operator. A common approach is to implement algorithms to detect and react to a collision.

Many detection methods exist. They range from comparing the robot actual torques to the theoretical ones necessary to perform its task to observing the change of energy in the system [START_REF] De Luca | Collision detection and safe reaction with the DLR-III lightweight manipulator arm[END_REF]. For a complete review on collision detection algorithms, one may refer to [START_REF] Haddadin | Robot Collisions : Detection , Isolation , and Identification[END_REF]. Once a collision is detected, the work of [START_REF] Sami Haddadin | Evaluation of collision detection and reaction for a human-friendly robot on biological tissues[END_REF] proposes to stop the robot or to switch its control mode to a zero-gravity torque control. Alternatively, [START_REF] Magrini | Control of generalized contact motion and force in physical human-robot interaction[END_REF] develops a control solution to realise motion and/or force control at any point on the robot and propose to control the force exerted by a robot at the point where a collision occurred.

As effective as these techniques can be, detecting and reacting to a collision is not sufficient to ensure safety. If at the moment of impact the robot is moving too fast or with an important load, the collision by itself might be fatal. Before reacting to a collision, the robot should be actuated in a way that is intrinsically safe. ISO Norm 15066 [START_REF]Robots and robotic devices collaborative robots[END_REF] proposes a new definition of a robot dangerousness during transient contact, i.e. an impact. The norm proposes to quantify a robot kinetic energy and provides energy limits to respect in order to avoid severe human injuries.

In a previous work [START_REF] Joseph | Towards X-ray medical imaging with robots in the open: safety without compromising performances[END_REF], a robot kinetic energy is expressed as a constraint inside a quadratic programming (QP) problem. This constraint ensures that the robot does not exceed a defined limit considered as dangerous. It shows that by correctly expressing the constraint, it is possible to ensure safety in different cases of collision. However, the kinetic energy computed through this method is based on a theoretical dynamic model of the robot and does not guaranty to be representative of the true robot kinetic energy.

To that extent, a platform has been developed to measure the energy transferred by a robot during contact. This platform is used in this work to validate the approach proposed in [START_REF] Joseph | Towards X-ray medical imaging with robots in the open: safety without compromising performances[END_REF] by comparing the energy measured by the platform to the one computed with the robot model.

In a first section, the QP formulation is explained and the kinetic energy constraint is detailed. In a second section the experimental set-up for the experiments is detailed. In a third section several experiments are realised and experimental results are presented to validate the correct enforcement of the proposed energy constraint. The last section concludes on this work and proposes further improvements that are being investigated.

Constrained convex problem formulation

The control of a robot can be expressed as an optimization problem where cost functions define the robot tasks and constraints modelize the robot actuation limits [START_REF] Rubrecht | Motion safety and constraints compatibility for multibody robots[END_REF]. The optimization problem requires expressing tasks and constraints as functions of the control variable. In this work, the control variable is the joint torque, τ ∈ R n , where n is the robot number of degree of freedom (dof). This section focuses on the expression of a quadratic programming problem to ensure safety by defining a kinetic energy constraint.

Tasks

The robot tasks are formulated in terms of commanded task space acceleration v * ∈ R 6 , where v ∈ R 6 is the end-effector twist expressed at some point of interest. The tracking of this task is ensured by a PID controller. A robot task can thus be expressed as:

T (τ ) = v * -v(τ ) (1)
Using the robot equation of motion, it is possible to express tasks as a function of the robot torque such that

T (τ ) = v * -( J q + JM -1 (τ -b(q, q) -g(q))) (2)
where q and q ∈ R n are respectively the joint configuration and its derivative, J and J ∈ R 6×n represent the robot Jacobian and its derivative expressed at the end-effector point. b(q, q) ∈ R n is the centrifugal and Coriolis induced joint torque, g(q) ∈ R n the gravity induced joint torque and M (q) is the n × n joint-space inertia matrix.

Constraints

Quadratic programming allows expressing constraints as inequalities. These constraints prevent the robot from reaching forbidden states. The robot intrinsic constraints, i.e. its bounds on joint positions, velocities and torques are one of the constraints that should be considered when controlling a robot. These constraints can all be expressed as inequalities and using a proper discretization scheme such as in [START_REF] Rubrecht | Motion safety and constraints compatibility for multibody robots[END_REF] they can overall be written under the general form

C(q, q)τ ≤ h (3)
with C(q, q) the constraint matrix and h its associated limit vector. The specific case of the energetic constraint is dealt with in section 2.4.

Quadratic programming formulation

The control of the robot requires finding the optimal command input, τ opt , satisfying the constraints and minimizing the tasks. This problem can be expressed as a quadratic programming optimization which is defined as

τ opt = argmin 1 2 ||T (τ )|| 2 + ε||r|| 2 τ s.t. C(q, q)τ < h (4)
where ||.|| is the euclidean norm, r is a regularization term ensuring the uniqueness of the optimized solution and ε 1 is a weighting term allowing monitoring the impact of the regularization on the main tasks performances.

For a kinematically redundant robot the choice of r is important as it affects the robot behaviour when the defined tasks do not fully constrain the robot. r is a task using all degrees of freedom. A common regularization task consists in minimizing the control variable, so here r = τ . In [START_REF] Joseph | Towards X-ray medical imaging with robots in the open: safety without compromising performances[END_REF], the controller is implemented on a redundant robot and the regularization task is set to minimize ||τ -g(q)|| 2 . This regularization task minimizes the difference between the computed torque and the gravity induced external torque. It allows performing free motions in the null-space of the robot main tasks by physically interacting with it.

The kinetic energy constraint

In its discrete form, the kinetic energy, E c,k , of the robot end-effector can be written:

E c,k = 1 2 v T k Λ k (q k ) v k (5)
where,

Λ k (q k ) = J k (q k )M -1 k (q k )J T k (q k ) -1 ∈ R 6×6
is the operationalspace inertia matrix and v k ∈ R 6 its current velocity. Considering a time period, ∆t, between two discrete time k and k + 1, the robot velocity at the next time step can be approximated to

v k+1 = v k + vc k ∆t, (6)
where vc k is the current control acceleration. Considering that the modification of the configuration of the robot during the time interval ∆t is small enough, it can be shown that the difference of kinetic energy between two successive discrete times can be written:

E c,k+1 = E c,k + v k ∆t + 1 2 vc k ∆t 2 T ∆x Λ k vc k F c k . (7)
On the one hand, ∆x represents the expected variation of pose given an initial operational state {x k ; v k } and the commanded acceleration trajectory vc k . On the other hand, F c k = Λ k vc k , is the equivalent control wrench. This formulation can be interpreted as the provisional kinetic energy in ∆t seconds. This energy is expressed as a function of the robot torque using the equation of motion. It is then inserted as a constraint in the optimization problem so that E c,k+1 (τ ) ≤ E lim c . In [START_REF] Joseph | Towards X-ray medical imaging with robots in the open: safety without compromising performances[END_REF], it is shown that this constraint can be used to limit the energy that can be transferred from the robot to an obstacle during transient contact and also to limit wrenches applied by the robot when it entraps an obstacle against a fixed surface. However, further validations are required to asses the correct respect of this energy limit.

Experimental setup

This work proposes to use an external device to quantify the energy transferred from the robot to an obstacle during an impact. This platform, depicted in Figure 1, measures the potential energy stored in a spring when a contact occurs. If the friction effects are negligible, this potential energy is equal the energy transferred by the robot at the impact.

This platform consists in a rigid structure on which is mounted a rotating beam. A spring is attached on one side of the beam and is pre-constrained. The robot enters in collision with the other side. Ball bearings are used to reduce friction at best. A 13-bit encoder is placed at the structure centre of rotation and a micro-controller queries its position at 500 Hz. The resulting elongation, ∆x, of the spring is obtained using geometric relations. The spring stiffness, k, is measured beforehand using a micrometric table and a dynamometer with a 0.05N precision. The potential energy, E p loaded in the spring is equal to 1 2 k∆x 2 . The robot and the platform are mounted on a fix and rigid table. A bracing is mounted on the beam carrying the encoder to reduce any deformation of the structure during the collision.

The control framework proposed in section 2 is tested on a KUKA LWR4+. Torque commands are sent to the robot at 1 kHz using the KUKA Fast Research Interface through an OROCOS component [START_REF] Bruyninckx | OROCOS: design and implementation of a robot control software framework[END_REF]. The QP problem is implemented using the qpOASES library [START_REF] Hans | qpOASES: a parametric active-set algorithm for quadratic programming[END_REF]. When contact occurs, strong inertial efforts are applied on the robot. An ATI Gamma sensor is used to record these forces. A threshold is applied to determine the instant of collision. The kinetic energy of the robot at that instant is compared to the maximum potential energy stored in the platform spring.

Experimental results

This section provides experimental results obtained with the platform described previously. First the measurements of the platform are compared with the model based kinetic energy of the robot. In a second part, experiments are realised to verify the respect of the kinetic energy constraint.

In the two experiments, the robot moves along a straight line with a target position located behind the platform. The robot trajectory tracking task is performed using a PID controller. When a contact is detected, the task is cancelled so that it only remains the regularization task, leaving the robot in gravity compensation mode. This is to ensure that the PID controller does not integrate the error resulting from the collision and thus inject more energy to the platform. Figure 2 compares the energy of the robot and the platform when a collision occurs. The orange curve represents E c , the average kinetic energy of the robot during the experiment over 10 trials. The blue curve represents the average potential energy stored in the platform spring, E p . In dark is the average force along the y-axis, F y , recorded by the ATI sensor. It can be seen that prior to contact, the force recorded by the ATI is close to zero. When the collision occurs, a spike in the force is recorded. At the same instant a sudden drop of the robot kinetic energy can be observed as well as an accumulation of potential energy stored in the spring. Overall, the robot average kinetic energy at the instant of contact is 0.516 J. The average potential energy stored in the spring rises up to 0.528 J. It results a difference of 3.17 % and a standard deviation over 10 trials of 0.012 J between the model based kinetic energy and the measurement of the platform. This experiment thus validates the model-based computation of the kinetic energy.

In a second experiment, depicted on Figure 3, the kinetic energy limit, E lim c , is set at 0.2 J, bellow the 0.5 J required to correctly execute the task. The horizon time step ∆t is set at 15 ms. Once again, the experiments are realised 10 times. The red curve represents the kinetic energy limit. The green curve represents the average predicted kinetic energy, E c,k+1 , computed with the robot dynamic model. It is the energy, expressed in [START_REF] Haddadin | Robot Collisions : Detection , Isolation , and Identification[END_REF], that is constrained inside the QP solver. The predicted energy being expressed relatively to a horizon of time ∆t, it represents the energy that the robot would have in that horizon of time. The QP solver finds torque commands to ensure that it never exceeds the limit E lim c (in red). Consequently, the resulting real kinetic energy is inferior to the predicted one. When the collision occurs, this current kinetic energy is on average equal to 0.168 J. The potential energy stored in the spring after impact rises up to 0.170 J. Over 10 trials, the standard deviation of the error is 0.002 J. The resulting energy that is constrained through this method is always inferior to the limit and validates the proposed solution. To be closer to the limit, it would require choosing a horizon of time ∆t as close to the robot control period as possible. However, a too small time step could induce important variation of the robot commanded torques at the next time step which may lead to oscillation and commands that are not feasible by the actuators. Constraint compatibility should be taken into account as thoroughly detailed in [START_REF] Meguenani | Safe control of robotic manipulators in dynamic contexts[END_REF].

Conclusion

Torque sensing robots offer new ways to interact with a robot and to detect collisions. However, depending on the robot current velocity and the tools it carries, the detection of a collision may not be sufficient to ensure safety. Ensuring safety thus also requires considering the case of unwanted contact. To alleviate this problem, ISO Norm 15066 proposes to limit the energy that can be transferred from the robot to a human body.

This work proposes a control solution that directly constrains the robot kinetic energy through a constrained convex optimization formulation. This kinetic energy constraint is expressed according to the theoretical model of the robot and does not mandatorily represents its real kinetic energy. To validate this model, a platform is designed to record the energy transferred from the robot during an impact. The results show that the model based kinetic energy is similar to the real one. This platform is then used to show the correct enforcement of the kinetic energy constraint. It experimentally proves that the formulation of a kinetic energy constraint can efficiently prevent the robot from transferring a dangerous amount of kinetic energy during an impact, thus improving the safety of a robotic solution.

When the robot kinetic energy is not sufficient to realise the tasks, the QP solver finds torque solutions reducing the trajectory tracking performances. This induces a decrease of the robot velocity. The only way to maximise the robot velocity while satisfying this constraint is to minimize the robot operational inertia matrix in the direction of motion. In the work of Mansfeld et.al. [START_REF] Mansfeld | Improving the Performance of Biomechanically Safe Velocity Control for Redundant Robots through Reflected Mass Minimization[END_REF], a gradient descent method is used to reactively compute, at each time step, a joint configuration minimizing the robot perceived mass in the direction of motion. Such algorithms could be used in the control framework presented in this paper and enforced using the regularisation task. It is possible to define a regularisation task that pushes the robot toward a desired position minimizing its perceived mass towards an obstacle. Ongoing work is being performed to test this implementation and yields promising results.

Fig. 1 :

 1 Fig. 1: Platform to measure the energy transferred by a robot during an impact. The elongation of the spring is measured by an encoder to determine the potential energy accumulated when an impact occurs.

Fig. 2 :

 2 Fig. 2: Energy dissipation during an impact without a constraint on the kinetic energy.

Fig. 3 :

 3 Fig.3: Energy dissipation during an impact with a limited kinetic energy of 0.2 J.

Acknowledgement

This work has been partially funded by ANRT under CIFRE grant n o 2015/0288.