Martin Clochard

Claude Marché

Andrei Paskevich

Deductive Verification with Ghost Monitors

Keywords: deductive verification, unstructured programs, ghost code, games, Hoare logic, predicate transformers, infinite behaviors

published or not. The documents may come

Introduction

The traditional approach to deductive program verification, as embodied by the Floyd-Hoare logic and the weakest precondition calculus, ties the verification process to the syntactic structure of the program under consideration: contracts are attached to subprogram boundaries, loop invariants are placed at a fixed place in the loop body, the program state at previous loop iterations is inaccessible, etc. Sometimes, however, the target program is not written in a way that makes its proof straightforward. An algorithm implemented as a simple loop may be best explained through a complex recursive scheme that establishes links between individual loop iterations. Various optimisation techniques may alter the control flow making the original loop invariants inadequate. Finally, compilation into an unstructured language produces code which is difficult to verify directly.

We propose a new method to handle such hard cases by introducing a level of indirection (nod to David Wheeler's aphorism intended). Instead of a frontal assault on the target program, we write, specify, and verify an auxiliary program, called ghost monitor, whose control flow restores the desired algorithmic structure, allowing us to place right invariants in right places. In this regard, a ghost monitor is a reimplementation of the target code in a way best suited for verification. However, the monitor does not perform computations on its own (apart from auxiliary computations needed purely for verification purposes). Instead, it follows-monitors-the execution of the target program, from one breakpoint to another, so that the execution of the monitor and the target advance in lockstep. The only observable side effect of the monitor is when it commands the target program: "continue until the next breakpoint". In other words, the monitor program acts as a debugger for the target program: the former maintains the auxiliary data and the invariants needed for the proof, while the latter performs the actual computations and synchronizes with the monitor at the breakpoints.

It is important to note that we do not mean any kind of run-time checking here. Ghost monitors are subject to the standard static analysis and deductive verification procedures. Since the monitor may observe the state of the target, we can express-as the monitor's specification-all the properties of the target code we may desire to prove. And since the monitor can not alter the execution of the target program in any way (it may only command the target to continue), proving the correctness of the monitor ensures that the target program indeed satisfies the required properties.

It may seem that we do not make the user's job any easier: after all, they have to write and verify a whole new program. However, we are going to show on several examples that the monitor's code and specification, put together, may well be more clear and easier to come up with than the invariants and assertions tied to the control flow of the target code.

Let us demonstrate the essence of our method on a simple example. Consider the following two code fragments, one written in OCaml, and the other in C: The recursive function on the left is the famous "91 function" by John Mc-Carthy [START_REF] Manna | Properties of programs and partial function logic[END_REF], which evaluates to 91 when n ≤ 100, and to n -10 otherwise. To prove that function mcc91 satisfies this specification is a matter of milliseconds using any modern automated program verifier, backed up by an SMT solver. The tricky part here is the proof of termination, which requires finding an appropriate variant (i.e., decreasing measure), for example 101 -n. The iterative C code on the right computes the same function (leaving the result in n), and can in fact be obtained from the recursive code by manual de-recursification, using an extra variable e to represent the number of pending recursive calls. Verifying the iterative version, however, is quite harder: it requires discovering a more complex variant and a non-trivial loop invariant.

Our method allows us to verify the code on the right by "observing" its execution from a ghost monitor program whose control flow would be taken from the recursive code on the left. We start by placing four breakpoints in the C code: breakpoint 0 at the beginning, breakpoint 1 before if (n > 100). . . , breakpoint 2 before if (e = 0). . . , and breakpoint 3 at the end. We choose the breakpoints in such a way that the evolution of the symbolic state of the target program between two breakpoints can be computed statically, e.g., via symbolic execution. In particular, breakpoints must break loops.

This evolution of the symbolic state is translated into the following specification that establishes the relation between the pre-and post-state of the slices of the C code (variables with primes represent the post-state, the additional variable pc denotes the breakpoint number):

pc = 0 → pc = 1 ∧ e = 1 ∧ n = n pc = 1 ∧ n > 100 → pc = 2 ∧ e = e -1 ∧ n = n -10 pc = 1 ∧ n ≤ 100 → pc = 1 ∧ e = e + 1 ∧ n = n + 11 pc = 2 ∧ e = 0 → pc = 3 ∧ e = e ∧ n = n pc = 2 ∧ e = 0 → pc = 1 ∧ e = e ∧ n = n
We attach this specification (with an added precondition 0 ≤ pc ≤ 2) to a procedure named CONT, and define the ghost monitor as shown in Fig. 1. In the monitor code, the variables that refer to the state of the target C program are written in italic. This program, modulo a few syntactic adjustments, is automatically proved by Why3.

The control flow of mcc91 monitor follows that of mcc91. However, the actual computations are performed as side effects of CONT, which simulates the execution of the C program up to the next breakpoint. Each call to mcc91 monitor starts at the beginning of the loop body (breakpoint 1), and ends when variable e is decremented (breakpoint 2). Remember that e represents the number of pending recursive calls to mcc91, and, indeed, at the end of a call to mcc91 monitor, the variable n contains the result of the McCarthy 91 function applied to the pre-state value of n. The function main monitor initiates and finalizes the computation. Its contract ensures that the execution of the monitor begins and ends at the same time as the execution of the target code. Since the monitor does not affect the target program state in any other way than by calling CONT, we can conclude that the iterative C program does indeed compute the 91 function. discovery of appropriate contracts and invariants, as shown in Section 2 on the example of Schorr-Waite algorithm [START_REF] Schorr | An efficient machine-independent procedure for garbage collection in various list structures[END_REF]. Notably, this technique can be applied to verification of programs written in unstructured, assembly-like languages. Our approach is very different from the traditional use of ghost data and ghost code (as explored, e.g., in [START_REF] Filliâtre | The spirit of ghost code[END_REF]), where the auxiliary variables and computations are implanted inside the target code, and the verification process still has to follow the original control flow. One advantage of our method is that the monitor does not need to be written in the language of the target program. Whatever verification framework we use to prove the monitor's correctness, it never interacts with the target program's code. All needed knowledge about the target's behavior and the semantics of the target's language is stated in the specification of the CONT operation. This specification can be generated mechanically, for example, by means of symbolic execution of the target code between the chosen breakpoints. Note that this is a separate effort, not related to the implementation or verification of the monitor.

What is more, a ghost monitor does not even need to be executable. In this paper, we propose a language for ghost monitors that allows us to specify and prove properties of infinite executions of the target program, after a transfinite number of calls to CONT.

This approach also works when we want to establish relational properties, like forward or backward simulation, between two target programs. Indeed, we only need to provide the monitor with two CONT operations, one for each target, and make it follow the execution of both, in an appropriate cadence. In presence of non-determinism, the choices made by one target may be transferred to the other (as arguments given to CONT). Again, we can prove that verifying the monitor program ensures the corresponding properties of the targets. We show our method applied to the proof of relational properties between potentially non-terminating programs in Section 3.

The theoretical foundation of our approach uses the framework of games, as presented in Section 4. This framework is well suited for reasoning about infinite executions. It also lets us adopt a generalized approach with respect to the interpretation of non-determinism. A universal interpretation of non-determinism, commonly termed demonic, is used to prove program correctness for every possible behavior. On the other hand, an existential, angelic, interpretation is used to prove the existence of specific behaviors, or the existence of valid implementation choices. The game-theoretic framework allows us to mix both kinds of non-determinism when reasoning about a given program or programs. We show in Section 4.2 that our approach can be used to formally prove at least three kinds of properties in presence of non-determinism: program correctness, existence of a specific behavior, and, finally, simulation between two programs.

Finally in Section 5, we provide a language and a weakest pre-condition calculus for ghost monitors. This language supports arbitrary recursion, continuations, and fine-grained specification and proof of non-terminating behaviors, both in the target and in the monitor.

Due to lack of space we do not give in this paper the proofs of our theorems. These are partly available in a research report [START_REF] Clochard | Deductive verification via ghost debugging[END_REF] and in the first author's PhD thesis [START_REF] Clochard | Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels[END_REF]. In order to provide stronger guarantees about our results, we mechanized the Hoare logic underlying our language for ghost monitors using the Why3 tool. The development is available online at http://toccata.lri. fr/gallery/hoare_logic_and_games.en.html 2 Extended Example: Schorr-Waite Graph Traversal Since our approach does not exploit the syntactical structure of the target code, it works well for programs written in a low-level or unstructured language, including assembly. A representative example is the Schorr-Waite graph traversal algorithm [START_REF] Schorr | An efficient machine-independent procedure for garbage collection in various list structures[END_REF], which is a landmark example for evaluating proof methods dealing with pointer aliasing [START_REF] Bornat | Proving pointer programs in Hoare logic[END_REF]. To our knowledge, Leino was the first to propose a proof using only automated theorem provers [START_REF] Leino | Dafny: An automatic program verifier for functional correctness[END_REF].

Let us consider the implementation of this algorithm written in a low-level pointer-manipulating C code, given in Fig. 2. Our objective is to traverse the graph of nodes reachable from the given root via the pointers l and r. The specificity is to avoid using extra memory by modifying l and r to perform backtracking. All pointers are restored to their initial values at the end. The informal specification contains three parts: (i) The graph structure induced by pointers l and r is restored at the end of the procedure; (ii) Assuming all nodes in the graph are initially unmarked (m is 0), the ones reachable from root get /* swing */ node q = t; t = p->r; p->r = p->l; p->l = q; p->c = 1 } } else { /* push */ node q = p; p = t; t = t->l; p->l = q; p->m = 1; p->c = 0 } } /* breakpoint 2 */ } Fig. 2. Schorr-Waite graph traversal in C, with breakpoints. marked at the end; (iii) The nodes unreachable from root have their mark unchanged. Figure 3 shows a formal specification, using Bornat-style componentas-array model [START_REF] Bornat | Proving pointer programs in Hoare logic[END_REF] to represent heap memory.

Proving directly that the low-level code meets this specification requires quite complex loop invariants [START_REF] Leino | Dafny: An automatic program verifier for functional correctness[END_REF]. With the ghost monitor approach, we write a new ghost code following the standard structure of a recursive depth-first traversal. As for the McCarthy function, we assume first a CONT procedure is defined, with the break points set as shown in the code. Our monitor is then written as in Fig. 4, annotated with the usual pre-and post-conditions expected for a classical depth-first traversal. This annotated code is proved with automated solvers (see http://toccata.lri.fr/gallery/schorr_waite_with_ghost_monitor. en.html). Unlike [START_REF] Leino | Dafny: An automatic program verifier for functional correctness[END_REF], we do not need complex loop invariants to make explicit the hidden notion of backtracking stack behind Schorr-Waite algorithm.

Among the existing proofs of Schorr-Waite algorithm, the closest to ours might be the one proposed by Yang [START_REF] Yang | Relational separation logic[END_REF], based on a refinement approach. We argue however that our approach based on ghost monitors goes significantly further than classical refinement. Quoting the last paragraph of page 20 of Yang's paper: "One evident shortcoming of our logic is that the proof rules assume that two commands have similar control structures. When this assumption breaks, our new rules for quadruples do not help, and we mostly have to reason about C and C' individually in separation logic". Indeed, our method does not have this limitation. Notably, Yang's proof relates two iterative versions of Schorr-Waite algorithm, while with our method we relate an iterative version to a more abstract recursive version, in which the stack is implicit. Our proof is fully automated, and we argue that the extra annotations we need to add, as postconditions to the monitor, are considerably simpler than in [START_REF] Leino | Dafny: An automatic program verifier for functional correctness[END_REF].

Relational Properties and Infinite Behaviors

The ghost monitor method applies to relational properties like program equivalence. We illustrate this aspect by proving the equivalence of two programs parsing well-parenthesized words (Dyck language): they take an infinite stream of parentheses as input and stop upon finding an unmatched closing parenthesis. The first program (C), written in C, uses a counter to keep track of the number of currently opened parentheses:

n = 0; while (n >= 0) if (getchar() = '(') n++; else n--;
The second program (M), written in ML, uses recursion: We prove that the two programs are equivalent under two simplifying hypotheses: unbounded stack and mathematical integers.

To that end, we write a monitor calling one CONT procedure for each program. Instead of representing the input streams explicitly, as two global variables in the monitor, from which the CONT procedures would take the next character returned by getchar, we opt for a non-deterministic semantics of getchar, in order to illustrate the handling of non-determinism in ghost monitors. The challenge now consists in synchronizing the execution of the two programs, ensuring that they actually process the same input.

Equivalence of Non-Deterministic Programs

The straightforward generalization of ghost monitors to non-determinism is to make CONT perform non-deterministic choices whenever the target program does. In order to ensure that (C) and (M) read the same input values, the choices of one program must be transferred to the other. We achieve this by adding arguments to one of the CONT operations, giving to the ghost monitor the ability to drive the execution of the corresponding target program in the direction that matches the behavior of the other target. In essence, we replace the demonic interpretation of non-determinism for one of the two programs by an angelic one.

In this setting, contracts proved for the ghost monitor are transferred to simulation properties. Formally, the transfer property, illustrated in Fig. 5, states that for every ghost monitor π 0 for target programs π x and π y , where non-determinism is interpreted as demonic (universal) for π y and as angelic (existential) for π x , total correctness contract {P }π 0 {Q} (valid Hoare triple), pair of states x 1 , y 1 for π x and π y that satisfy P , maximal (potentially infinite) execution trace of π y starting from y 1 , there exists a pair of states (x 2 , y 2 ) satisfying Q together with a partial execution trace of π x from x 1 to x 2 such that y 2 belongs to the chosen execution trace of π y .

When P (resp. Q) expresses that both states are initial (resp. final) and equivalent to each other, this simulation result means an inclusion of behaviors. By proving inclusion in both directions, we obtain equivalence. To avoid writing a separate ghost monitor for each direction, we write a single monitor, parametric in the roles of the two programs. To represent these roles, we augment the state with two immutable Boolean variables angel C and angel M that indicate whether non-determinism is interpreted as angelic for the corresponding program.

Let us now build the monitor. First, we identify the relevant breakpoints in both programs, shown in Fig. 6. As these breakpoints break all execution cycles, we can obtain proper specifications for CONT C and CONT M , shown in Fig. 7. To describe the state of each target program, we use variables pc and in that denote, respectively, the current location and the input log (the list of all characters read up to this point). Since program (M) is recursive, we also have to model its stack. We represent it as a sequence of stack frames, each containing the return address in the form of a breakpoint number: 3 when scan is called from the main expression in (M), and 1 when scan is called recursively.

angelC → readC = toReadC pcC = 0 → pc C = 1 ∧ n C = 0 ∧ in C = inC pcC = 1 ∧ nC < 0 → pc C = 2 ∧ n C = nC ∧ in C = inC pcC = 1 ∧ nC ≥ 0 → pc C = 1 ∧ in C = inC + [readC ] ∧ (readC = '(' → n C = nC + 1) ∧ (readC = '(' → n C = nC -1) angelM → readM = toReadM pcM = 0 → pc M = 1 ∧ stack M = [3] + stackM ∧ in M = inM pcM = 1 → in M = inM + [readM ] ∧ (readM = '(' → stack M = [1] + stackM ∧ pc M = 1) ∧ (readM = '(' → stack M = stackM ∧ pc M = 2) pcM = 2 → in M = inM ∧ stack M = tail stackM ∧ pc M = head stackM
To model the non-deterministic nature of getchar, each CONT procedure receives an argument toRead and returns a return value read which represents the character just read, if any. When the program runs in the demonic mode (the corresponding angel variable is false), this return value is not specified in any way, reflecting the fact that read was picked in a non-deterministic manner. When the program runs in the angelic mode (the corresponding angel variable is true), read assumes the value of the toRead argument, allowing the ghost monitor to control the non-deterministic choices.

Equipped with these specifications, we are now ready to write the monitor program. We could use the structure of (M), but to reduce annotations we choose a slightly different structure, which fuses the iterations of the loop in (M) in a single tail-recursive call. We give the monitor in Fig. 8. The core of the monitor is the recursive function sync, which relates: on one hand, iterations of program (C) until the counter has decreased; on the other hand, one full recursive call of scan in program (M).

While this monitor is automatically proved using Why3 without any trouble, there is a catch. Indeed, we did not prove that this monitor terminates, as we do not have any measure to control execution time. However, we can only use the transfer hypothesis to derive program equivalence when we have a total correctness property for the ghost monitor. This means that we need additional ingredients to deal with non-terminating behaviors.

Infinite behaviors

The simplest way to recover total correctness for the ghost monitor is to assume that the program with demonic non-determinism terminates, for example using a variable representing execution fuel. While this would easily lead to a terminating monitor, we would not obtain the right equivalence result. Indeed, to exploit such a termination hypothesis, we need to weaken the transfer property by restricting the universal execution range to terminating executions, i.e., finite maximal executions. In particular, we would only obtain as a result that the two programs have the same terminating behaviors, but may have different non-terminating behaviors.

To make the distinction clear, suppose that we change the semantics of (C) so that getchar() may have a third possible behavior, starting an infinite loop.

Then (C) and (M) still have the same terminating behaviors (we may adjust a fuel-based monitor to prove this), but (C) now has extra non-terminating behaviors in which it reads only finitely many inputs, while (M) cannot.

Hence we need a way to relate infinite executions of the two programs. To do so, we extend our ghost monitors with means to handle divergence. We consider the program clock as a possibly transfinite number and we treat the transition to a limit ordinal as an exceptional situation that can be intercepted in the monitor code. Of course, this cannot be realized in a physically executable code, but ghost monitors only serve for verification and are never executed. In this way, a ghost monitor may call CONT an infinite number of times and then proceed to an exit point, covered by the monitor's post-condition. In terms of the transfer property in Fig. 5, this means that we transfer an execution trace running up to a limit program state located after an infinite sequence of steps.

To be able to proceed with that plan, we first need a way to actually represent that limit program state. We achieve this using least upper bounds: the state of the program after an infinite execution is considered to be the least upper bound of the states during said execution. This matches perfectly the intuition for event traces like our input logs, as the least upper bound becomes the (potentially infinite) trace of events during the entire infinite execution. However, this in general has no meaning for regular variables. In order to treat these values properly, we augment the state with time counters t C and t M which increase at each execution step. Using a proper ordering (see Section 4.2) on states augmented with counters, we can discard the meaningless values in infinite states. By convention, we also set pc C and pc M to ∞ after an infinite execution.

Let us now focus on the verification mechanism. First, we replace decreasing termination measures with increasing progression measures. Instead of representing a termination argument, progression measures serve as constraints over potential divergence behavior. For our running example, we need to enforce that time counters increase between recursive calls to make sure that whenever sync diverges, so does the target program. Similarly, we need to enforce that input log grows to rule out behaviors in which a program stops performing input. Note that we do not impose any condition on the progression ordering itself.

Second, we equip recursive definitions with divergence handlers. Divergence handlers are given by an extra diverges clause after a recursive definition. This clause introduces a statement intended to handle any form of divergence issuing from such recursion. Divergence handlers are entered with the target program state after an infinite recursive descent, that is the least upper bound of the states along the call stack leading to divergence. This call stack is given to the divergence handling clause as a parameter, and is assumed to follow the progression clause, as well as being infinite. Divergence handlers should cut the stack at some point of their choice, which corresponds to completing a leftover recursive call. For verification purposes, this means that the handler should establish the post-condition of this particular call. Note that this is more general than simply recovering from an exception thrown by the recursive function, which is equivalent to closing the bottom call. Indeed, the recursive function may continue executing even after divergence has been caught (potentially infinitely many times through local recursive functions).

let monitor () requires { pcC = 0 ∧ pcM = 0 ∧ inM = inC } requires { angelC = angelM } ensures { (pc C = 2 ∧ pc M = 3) ∨ (pc C = ∞ ∧ pc M = ∞) } ensures { in M = in C } = let ign = '(' in CONTC (ign); CONTM (ign); let rec sync () : unit requires { pcC = 1 ∧ pcM = 1 ∧ inM = inC ∧ nC ≥ 0 } progress { (tC ) × (tM ) × (|inC |) } (* tC , tM , |inC | all increase *) ensures { (pc C = 1 ∧ pc M = 2) ∨ (pc C = ∞ ∧ pc M = ∞) } ensures { pc C = ∞ → stack M = stackM ∧ n C = nC -1 } ensures { in M = in C } = if
In practice, we should also change iterative statements, but the changes would be similar, since loops are essentially calls to anonymous tail-recursive functions. We can now use this framework to turn our earlier ghost monitor into a ghost monitor that proves the equivalence of both programs, taking into account nonterminating behavior. We show the monitor adapted to divergence handling in Fig. 9. We add the progression clause proposed earlier, as well as a divergence handler which merely returns at any level. To account for the extra behaviors, we also add a few tests after calls to sync to treat infinite states appropriately. While we gave a short body for the divergence handler, in practice we need a few assertions (manual proof steps) to recover all the desired post-conditions in a fully automated manner.

So far, we did not explain how the call stack leading to divergence was specified in the divergence handler. There are several choices, and not all of them are equivalent from the perspective of mechanized proofs, nor are they equally powerful. In Section 5, we make the choice of the most general construction available, by representing this stack as a non-empty set of call parameters/state pairs. We constrain this stack to be totally ordered by the chosen progression order, as well as having no maximum. As this set-based representation does not limit the stack to countable sets, we are able to allow recursive calls inside the divergence handler itself, as long as the progression order increases with respect to the elements of the stack.

However, this general choice is typically not the most practical. In most examples, we would prefer to sacrifice the power of making recursive calls inside the divergence handler, as well as the power to return from the handler at any suspended recursive call, in return for consequent advantages for mechanized proof. First, this lets us represent the stack as a sequence of call parameters/state pairs instead of a set. Second, as the divergence handler cannot return at intermediate recursive calls anymore, we may remove alternative post-condition corresponding to divergence from recursive calls. Third, the fact that this alternative post-condition is only linked to the bottom of the recursion stack makes it easier to link this post-condition to the initial parameters and states. Fourth, the use of a sequence for the stack allows us to generalize the progression order to any relation between recursive calls occurring in immediate succession.

Of course, this more practical divergence handler construction can be derived as syntactic sugar from the more general one, by turning the sequence of successive recursive states into a parameter of the monitor and using prefix order as the progression order. Other intermediate schemes may be derived as well in a similar way. Therefore we focus on the more general construction below.

Unifying Transfer Properties through Games

We base our verification approach on the formal model of games, which can be thought as the natural generalization of transition systems in the presence of both angelic and demonic non-determinism. In this setting, the validity of a Hoare triple corresponds to the existence of a winning strategy for the angel. In particular, this turns ghost monitors into tools to prove the existence of such winning strategy. Indeed, in this framework the transfer property now map valid contracts for ghost monitors to winning strategies in the underlying game.

The purpose of the game framework is to unify and generalize the different kinds of transfer properties we have seen so far. Indeed, total correctness amounts to the existence of a strategy in a game whose state is the program state, and where the demon performs non-deterministic choices. Similarly, simulation properties can be expressed as existence of winning strategies in a game corresponding to the execution of two programs, where the demon makes choices for one program and the angel makes choices for the other. We can also express other properties, e.g., by having the angel making all choices for a single program. Then the existence of a winning strategy reduces to the existence of a program behavior from an initial state to a final state satisfying some properties.

In this section, we first present our formal model of games, before demonstrating the embedding of several transfer properties over transition systems as existence of winning strategies in the corresponding games. Note that transition systems abstract small-step operational semantics of programs, which we require for the ghost monitor approach.

Games

As we solely focus on tools to prove the existence of such winning strategies for the angel, we define games asymmetrically with respect to both players. The domain of the game corresponds to angelic states, while demonic states are implicitly defined as sets of angelic states. We define the transition function according to this intuition, as a function mapping angelic states to sets of such implicit demonic states, hence sets of sets of angelic states. Here, the outer set represents the set of angelic choices, while the inner set represents the set of demonic choices. These definitions match the behavior of the CONT routines of Section 3. Angelic choice selects the arguments given to that routine, which from the verification perspective amounts to select a post-condition (a set of angelic states), while demonic choice selects the effective updates performed by that routine as it wishes as long as it respects the behavior specified in the post-condition (non-deterministic choice of a behavior in the set).

In order to handle the case of non-terminating programs with observable effects, we equip our games with an order, so that the state only grows during a play of the game. We then represent the overall infinite execution of a program by the least upper bound of a play, which is typically the sequence of all observable effects. We impose that the order is chain-complete so that the requested least upper bound always exists.

Definition 1 (Chain-Complete Order, Game). A partially ordered set (O, ≤) is chain-complete if for all non-empty X ⊆ O totally ordered by ≤, X admits a least upper bound. A game G = (G, , ∆) is a chain-complete partially ordered set (G, ) equipped with a function ∆ from G to P(P(G)) such that ∀x ∈ G, ∀X ∈ ∆(x), ∀y ∈ X, x ≺ y.

We call G, , and ∆, respectively, the domain, the order, and the transitions of the game.

Note that the current state of a play may contain not enough information for a winning strategy to drive the play in the right direction. Indeed, a monitor keeping track of auxiliary data naturally translates into a strategy that uses memory. Due to our treatment of infinite behaviors, we have not been able to prove that such memory could be systematically eliminated (nor to prove that it is strictly necessary). Thus we introduce the notion of history to represent the complete memory of a play. Definition 2 (History, Prefix Order). Given a game G = (G, , ∆), a history of G is a non-empty subset of G for which the restriction of is a total order, and which admits a maximum for that order. Given two histories H 1 , H 2 for a game G = (G, , ∆), we say that H 1 is a prefix of H 2 if H 1 ⊆ H 2 , and for all x ∈ H 2 \H 1 , x is an upper bound of H 1 .

We then introduce the notion of victory invariant, a notion closely related to the notion of winning strategy. A victory invariant is essentially a set of histories that the angel has the ability to keep following from a source state until a state from the winning set is reached. This is in fact equivalent to the notion of winning strategy with non-deterministic choices.

Definition 3 (Victory Invariant). Given a game G = (G, , ∆) and two subsets P, Q of G, a victory invariant of G for P, Q is a set I of histories of G such that (i) for all x ∈ P , {x} ∈ I, (ii) for all H ∈ I such that H ∩ Q = ∅, there exists X ∈ ∆(max H) such that for all x ∈ X, H ∪ {x} ∈ I, (iii) for every non-empty H ⊆ I that is totally ordered by the prefix order, H ∪ {sup H} ∈ I.

The three propagation rules of victory invariants tell us exactly how to build a winning strategy, except for some choices in rule (ii). Rule (i) means that such a strategy can be built when starting from any element of P . Rule (ii) means that when the current history is H, either the angel has already won the game or a (not necessarily unique) winning decision can be made at that point. Finally, rule (iii) means that if a history grows indefinitely, it continues at the least upper bound. Note that building a play while respecting the invariant guarantees that after some ordinal number of iterations, the winning set Q will be attained. This is implied by the fact that the history strictly increases until Q is reached.

We prefer using victory invariants rather than strategies for two reasons. First, leftover choices in condition (ii) make victory invariants more permissive and more practical to perform proofs. Second, victory invariants are quite similar in nature to loop invariants, which makes them more directly related to program logics than winning strategies.

Linking Games and Transition Systems

We show how to connect transition systems and games, in order to recover more intuitive transfer properties talking about the operational semantics of the target programs. We consider several translations from transition systems to games. The details of the translation differ depending on the actual transfer property. We show here how to translate three different properties as existence of victory invariants: program correctness, existence of behaviors, and simulation.

Note that bare transition systems do not come with any way to describe infinite behaviors except for the complete trace, which may be exceedingly precise. We equip transition systems with observation records to model abstractly the trace of observable effects of the program, which is the natural tool to describe the behavior of a non-terminating program. We then use the least upper bound of observation records along an execution to represent the "state" at infinity.

Definition 4 (Transition System with Observation Records).

A transition system with observation records is a tuple S = (S, →, p, O ) where -(S, →) is a transition system, -(O, ) is a chain-complete order, representing the observation records, p is a monotonic map from (S, → * ) to (O, ) that extracts records.

We now define the two translations corresponding respectively to the angelic (existential) and demonic (universal) interpretation of non-determinism. These two translations share the same support. To represent finite states, we pair the transition system state with a counter to represent effective transition. For infinite states, we use an observation record.

Definition 5 (Timed support). The timed support associated to a transition system with observation records S = (S, →, p, O, ) is the ordered set (G S , S ) defined by

-G S = {(n, x) ∈ (N ∪ {∞}) × (S ∪ O) | (n = ∞ ∧ x ∈ O) ∨ (n = ∞ ∧ x ∈ S)}, -∀n ∈ N, x ∈ S, y ∈ O. (n, x) ≺ S (∞, y) ⇔ p(x) y, -∀n, m ∈ N, x, y ∈ S. (n, x) ≺ S (m, y) ⇔ n < m ∧ p(x) ≺ p(y), -∀x, y ∈ O. (∞, x) ≺ S (∞, y) ⇔ x ≺ y.
Definition 6 (Existential game). The existential game associated to a transition system with observation records S = (S, →, p, O, ) is defined as the game G S,∃ = (G S , S , ∆ S,∃ ) with transitions defined by

∆ S,∃ ((n, x)) = {{(n + 1, y)} | x → y} when n ∈ N, ∅ when n = ∞.
Definition 7 (Universal game). The universal game associated to a transition system with observation records S = (S, →, p, O, ) is defined as the game G S,∀ = (G S , S , ∆ S,∀ ) with transitions defined by

∆ S,∀ ((n, x)) = {{(n + 1, y) | x → y}} -{∅} when n ∈ N, ∅ when n = ∞.
These definitions are valid only because the timed support is chain-complete, which is a routine consequence of chain-completeness of observations. We remove ∅ from the universal transition because when it occurs, it corresponds to a stuck state. In particular, the angel should not be able to progress on such states. Moreover, this enforces that universal and existential games coincide for deterministic transition systems, i.e., the interpretation of non-determinism does not matter in this case.

We prove several results linking the existence of victory invariants in these games to properties about the original transition system. For existential games, this represents the existence of a behavior. For universal games, this means that a certain set of states is unavoidable (possibly after infinitely many steps). If there are no infinite states in the target set, this corresponds to total correctness. Theorem 1. For all S = (S, →, p, O, ), for all P, Q ⊆ S, Q ∞ ⊆ O, there is a victory invariant relative to G S,∃ for N × P, N × Q ∪ {∞} ∪ Q ∞ if and only if for all s 0 ∈ P , one of the following two conditions is true: (i) there exists a finite transition sequence s 0 → . . . → s n of S such that s n ∈ Q, (ii) there exists an infinite sequence s 0 → . . . → s n → . . . of S such that the least upper bound of observation records over the sequence belongs to Q ∞ .

Proof. See [START_REF] Clochard | Deductive verification via ghost debugging[END_REF] (Lemma 4.5, pages 25-26).

Theorem 2. For all S = (S, →, p, O, ), for all P, Q ⊆ S, Q ∞ ⊆ O, there is a victory invariant relative to G S,∀ for N × P, N × Q ∪ {∞} × Q ∞ if and only if for all potentially infinite transition sequences s 0 → . . . → s n (→ . . .) ? of S such that s 0 ∈ P , one of the following conditions is true:

(i) there exists an element s i in the sequence such that s i ∈ Q, (ii) the sequence is infinite, and the least upper bound of observation records along the sequence is in Q ∞ , (iii) the sequence is finite with last element s n , and there exists x ∈ S such that s n → x.

Proof. See [START_REF] Clochard | Deductive verification via ghost debugging[END_REF] (Lemma 4.6, page 26).

Using a product construction, we propose a third translation for simulation. Note that the final result allows arbitrary connections between finite and infinite behaviors of respective transition systems. Definition 8. Given two transition systems with observation records S 1 , S 2 , the simulation game from S 1 to S 2 is the game

G S1→S2 = (G S1 × G S2 , S1 × S2 , ∆ S1→S2 )
with transitions defined by:

∆ S1→S2 ((x, y)) = {{x} × Y | Y ∈ ∆ S2,∃ (y)} ∪ {X × {y} | X ∈ ∆ S1,∀ (x)}. Theorem 3. For all transition systems S 1 = (S 1 , → 1 , p 1 , O 1 , 1 ) and S 2 = (S 2 , → 2 , p 2 , O 2 , 2 ), for all set P ⊆ S 1 × S 2 , set family (Q a,b ) a,b∈{true,f alse} such that Q a,b ⊆ (a ? S 1 : O 1 ) × (b ? S 2 : O 2 )
, there exists a victory invariant for the set pair made of the pre-condition N × P and of the post-condition

{((n, x), (m, y)) ∈ G S1 × G S2 | (x, y) ∈ Q n=∞,m=∞ }
if and only if for all t 0 ∈ S 2 , for all s 0 → . . . → s n (→ . . .) ? maximal transition sequence of S 1 such that (s 0 , t 0 ) ∈ P , there exists t 0 → . . . → t n (→ . . .) ? a transition sequence of S 2 such that: (i) the transition sequence from S 2 ends at t n , and there exists i such that (s i , t i ) ∈ Q f alse,f alse , (ii) the transition sequence from S 2 ends at t n , the transition sequence from S 1 is infinite with least upper bound of observation s ∞ , and (s ∞ , t n ) ∈ Q true,f alse , (iii) the transition sequence from S 2 is infinite with least upper bound of observation t ∞ , and there exists i such that (s i , t ∞ ) ∈ Q f alse,true , (iv) the transition sequences are both infinite with respective least upper bound of observations s ∞ , t ∞ , and (s ∞ , t ∞ ) ∈ Q true,true .

Proof. See [START_REF] Clochard | Deductive verification via ghost debugging[END_REF] (Lemma 4.8, page 27).

Note that Theorem 3 admits a straightforward generalization to arbitrary number of transition systems in universal and existential positions. In particular, for a single transition system, this degenerates to Theorems 2 and 1. We also obtain other equivalences: for two universal transition systems, existence of victory invariants translates to deterministic correlation of behaviors.

Ghost Monitors for Games

We now define the language W G that we use to establish victory invariant on games G = (G, , ∆). This is a mostly functional programming language, where functions are first-order and equipped with contracts. The only non-functional feature is a global variable now ∈ G, which represents the current state of the game. We only permit update of this variable through the use of predefined procedure CONT which performs one transition of the game. Procedure CONT takes as argument an element X of ∆(now) and updates the global variable now to a non-deterministically chosen element of X.

Syntax of W G

The syntax is given in Fig. 10. We deliberately keep the language as small as possible. We exploit the fact that most usual programming constructions (like loops, conditional, assertions and others) with their usual verification rules can be derived as sugar to focus on the core constructions. For example, the missing meta-logic expression programs e can be encoded via continuation and call, as kont k in k(e) end-kont. The continuation mechanism can be used to smoothly simulate constructions like break, continue or return.

In the language definitions, expr and f ormula refer respectively to arbitrary mathematical expressions and formulas in some meta-logic language, whose exact nature is irrelevant here. These expressions can access any immutable variable, as well as the global variable now. Formulas in contract post-conditions can also access the special variable old, which refers to the state of the global variable now before the execution of a function.

Syntactic categories var, f un and typ correspond respectively to immutable variable names, function names, and variable types. For W G , variable types are given by statically known (non-dependent) sets. As functions of W G are necessarily first-order, function types are simply given by A → B, where A is the type of the parameter and B is the type of the return value. We define the typing system for language W G by a standard relation Σ|Γ π : B defined in Fig. 11, where Γ (resp. Σ) is the context of variables (resp. functions) with their types, and B is the derived type for the program. This typing relation is subject to a similarly-structured typing relation for the meta-logic that we do not present here.

There is one unusual construction in our verification language: the recursion, which introduces a recursively-defined function equipped with a handler to process the result of diverging behavior. The progress clause gives the progression order r, with respect to which the game state and function parameters should increase at recursive call. Recursion behaves in a special way in case of infinite execution, as presented in Section 3. If the recursion stack grows indefinitely up to a limit state, the divergence handler is called with that recursion stack, which is the totally ordered set of call parameter/state pairs of uncompleted recursive calls. Then, control flow returns at the end of the recursive call indicated by the result of the handler, with the return value given by the handler. Note that the divergence handler itself is allowed to make recursive calls as long as the pa-rameter/state pair increases further, which may lead to the divergence handler calling itself recursively with an even larger recursion stack.

Predicate Transformer Semantics for W G

We give a predicate transformer semantics for W G , using weakest pre-condition transformers in the style of Dijkstra [START_REF] Dijkstra | Guarded commands, nondeterminacy and formal derivation of programs[END_REF]. Intuitively, the transformer of a program π for a winning set Q gives the largest set P such that π proves the existence of a victory invariant for P, Q.

Due to the presence of continuations as well as defined objects, we parameterize the weakest pre-condition transformer by contextual elements. We add an assignation parameter, which gives the values of variables, and a specification context parameter, which gives the specification of functions. Definition 9 (Assignation, Specification Context). An Γ -assignation for W G is a mapping σ from variables names x : A from Γ to values in the set A. A Σ-specification context for W G is a mapping Φ from function names f : A → B from Σ to pairs P ⊆ A×G, Q ⊆ A×G×B ×G. Intuitively, the pair P, Q = Φ(f) represents the contract for procedure f within specification context Φ.

We define the semantics of W G as a mapping T [Φ, σ] (π, Q), which takes as argument a Σ-specification context Φ, an Γ -assignation σ, a well-typed program π with type derivation Σ|Γ π : B, and a set Q ⊆ B ×G (the post-condition); and returns a subset of G (the weakest pre-condition). The expressions and formulas within the program are interpreted by the mean of a standard interpretation function • • • ••• , which given an expression or a formula and an assignation of its variables, computes the value of the expression as an element of its type, or the satisfaction of the formula as a truth value.

We also define a predicate C[(Φ x ) x∈G , σ] (π : ϕ 0 → y : B. ϕ 1 ) corresponding to the notion of contract satisfaction, which we use for recursion. We give the full definition in Fig. 12.

Technically, the weakest predicate semantics should be defined from the complete type derivation (or a program tagged with all types) in order to get type information. For simplicity, we only write π as parameter and assume that the typing context is known.

The definition of the backward predicate transformer semantics for W G is mostly the standard definition of weakest pre-conditions, except for two cases: continuation and recursion. We define the predicate transformer for continuation introduction by adapting in a natural way the typing scheme of the call-with-current-continuation operator. For introduction of recursive functions, we perform the following modifications to the traditional transformer for total correctness:

-We replace the traditional well-founded decreasing termination measure by a progression order, which must increase along recursive calls, including the ones in the divergence handler. -We add condition (iv) for the divergence handling code π 1 . This condition states that π 1 terminates correctly given any limit recursion stack controlled by the pre-condition and the progression relation of the program.

T [Φ, σ] (f(e), Q) {x ∈ G | (ax, x) ∈ P f ∧ ∀b, y. (ax, x, b, y) ∈ Q f ⇒ (b, y) ∈ Q} where (P f , Q f ) = Φ(f) and ax = e σ[now←x] T [Φ, σ] (let x = π0 in π1, Q) T [Φ, σ] (π0, {(a, y) ∈ A × G | y ∈ T [Φ, σ[x ← a]] (π1, Q)}) (with x : A) T [Φ, σ] (kont f in π end-kont, Q) T [Φ[f ← (Q, ∅)], σ] (π, Q) T [Φ, σ] case x : A. ϕ in π, Q a∈A {x ∈ G | ϕ σ[x←a,now←x] ⇒ x ∈ T [Φ, σ[x ← a]] (π, Q)} Grd[σ](case x : A. ϕ in π) a∈A {x ∈ G | ϕ σ[x←a,now←x] } T [Φ, σ] (switch c1 . . . cn end-switch, Q) i∈ 1;n Grd[σ](ci) ∩ i∈ 1;n T [Φ, σ] (ci, Q) C[(Φx)x∈G, σ] (π : ϕ0 → y : B. ϕ1 ) ∀x ∈ G. ϕ0 σ[now←x] ⇒ x ∈ T [Φx, σ] (π, Qx) where Qx = {(b, y) ∈ B × G | ϕ1 σ[y B ←b,now←y,old←x] } z ∈ T [Φ, σ]   rec f(x) : ϕ0 → y : B. ϕ1 progress(r) = π0 diverges(S) : π1 in π2 , Q   if and only if the following conditions (i)-(iv) hold: (i) z ∈ T [Φ rec ∅ , σ] (π2, Q) (ii) r σ is a strict order (iii) ∀a ∈ A. C[(Φ rec {a,x} )x∈G, σ[x ← a]] (
(c) ∀(a, x) ∈ H. ϕ0 σ[x←a,now←x] then sup (a,x)∈H x ∈ T [Φ rec H , σ[S ← H]] π1, Q lim H where Φ rec H = Φ[f ← (P rec H , Q cont )] and P rec H = {(a, x) ∈ A × G | ϕ0 σ[x←a,now←x] ∧ ∀(a0, x0) ∈ H. (a0, x0) r σ e σ[x←a,now←x] } and Q cont = {(a, x, b, y) ∈ A × G × B × G | ϕ1 σ[x←a,y←b,now←y,old←x] } and Q lim H = {((a, x, b), y) ∈ (A × G × B) × G | (a, x) ∈ H ∧ ϕ1 σ[x←A,

From Weakest Pre-Conditions to Victory Invariants

We now state the main correctness result for our verification language, as a transfer property from language W G to games. Essentially, we claim that weakest pre-conditions for W G induce the existence of victory invariants.

Definition 10. We define the transition contract (P G , Q G ) associated to game G = (G, , ∆) as

P G = {(X, x) ∈ P(G) × G | X ∈ ∆(x)} Q G = {(X, x, 0, y) ∈ P(G) × G × {0} × G | y ∈ X}
We define the base specification context Φ G associated to game G = (G, , ∆) as the single-element specification context mapping CONT of type P(G) → {0} to the transition contract

(P G , Q G ) of G.
Theorem 4. For all games G = (G, , ∆), all well-typed programs CONT : P(G) → {0}|Γ π : {0}, all subsets Q of G, and all Γ -assignations σ, there is a victory invariant for

T [Φ G , σ] (π, {0} × Q) , Q.
We derive from Theorem 4 an immediate corollary, which concludes the existence of a victory invariant for a pair of sets definable in the meta-logic as long as we can find a program satisfying the corresponding contract.

G | ϕ 0 σ[now←x] }, {x ∈ G | ϕ 1 σ[now←x] }.
In order to prove Theorem 4, we need to state a stronger version that generalizes it over both specification contexts and output types. The proof is detailed in [START_REF] Clochard | Deductive verification via ghost debugging[END_REF] (Theorem 3.13, page 18). Theorem 4 is an immediate consequence of Theorem 5. Let us mention an interesting artifact of the proof: in order to prove correction of the continuation/recursive construction, the proof proceeds through games with extra transitions representing the additional function calls. In the case of recursion, this produces games with arbitrary interleaving of angelic and demonic non-determinism. In particular, these games cannot keep the special structure inherited from transition systems of Section 4.2, which justifies a posteriori the generic game framework.

Relative Completeness

For verification, we only need our proof methodology to be sound. However, it is also relatively complete, in the sense that if we can prove directly the existence of a victory invariant for a definable set pair in the meta-logic, then we can also prove its existence by finding a program of W G which satisfy the corresponding contract, via Corollary 1. The proof amounts to create a program that follows the explicit victory invariant. We need to make a few implicit hypotheses about the meta-logic for the proof to work out, notably that it can talk about victory invariants of the considered game, and express the notion in a manner compatible with our definition. We also need to be able to express a few set operators.

Lemma 1. For all games G = (G, , ∆), all well-typed formulas pair ϕ 0 , ϕ 1 well-typed in context Γ, now : G, and all Γ -assignations σ, if the existence of a victory invariant for the set pair {x ∈ G | ϕ 0 σ,now←x }, {x ∈ G | ϕ 1 σ,now←x } is provable in the meta-logic, then there exists a well-typed program CONT : P(G) → {0}|Γ π : {0} such that C[(Φ G ) x∈G , σ] (π : ϕ 0 → u : {0}. ϕ 1 ) holds.

Proof. See [START_REF] Clochard | Deductive verification via ghost debugging[END_REF] (Lemma 3.19, pages 23-24).

Related Work and Future Work

Hoare logic, games and dual non-determinism. Games were introduced as a model for weakest precondition transformers by Back and von Wright in 1990 [START_REF] Back | Duality in specification languages: a latticetheoretical approach[END_REF]. A related Hoare logic is studied by Mamouras in 2016 [START_REF] Mamouras | Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism[END_REF]. In both cases, the goal is to model and verify programming languages containing dual non-determinism. Our work differs in the sense that games are used as a model of small-step semantics, and that the nature of non-determinism is only chosen to obtain the transfer property we are interested in. In particular, we may obtain games with both types of non-determinism when considering relational properties, and also internally since our proof of soundness constructs such hybrid games for the recursion rule.

Hoare logics for machine code. Hoare logics defined for machine code in proof assistants are typically defined by proof rules which are mostly unrelated to the syntax of the underlying program. Such logics are closely related to our work, as proof rules match the syntactic constructs of ghost monitors. Moreover, automation by tactics may simulate a weakest precondition calculus. A typical example is the work of Myreen [START_REF] Myreen | Hoare logic for realistically modelled machine code[END_REF], which corresponds to a While language extended by well-founded recursion for the auxiliary language. Note that wellfounded recursion is inherently tied to the meta-logic induction. In contrast, we support non-terminating recursion and proof of diverging behaviors. Note that step-indexed logics like Iris [START_REF] Krebbers | The essence of higher-order concurrent separation logic[END_REF] support non-terminating recursion by the mean of the Löb rule, as well as arbitrary higher-order programs, but drop any support for total correctness, while we support fine-grained specification and proof for non-terminating recursion, but limited to first-order.

Future work. Our approach can be extended in several directions. A first direction is towards separation logic. We believe that adding a separation logic layer a posteriori in a similar fashion as the first-order fragment of Iris [START_REF] Krebbers | The essence of higher-order concurrent separation logic[END_REF] should pose no trouble. Another direction is to generalize our approach to a higher-order setting. This is reasonably easily if we enforce a restriction of the higher-order features: either by limiting the rank of the allowed functions, or by limiting the usage of recursive calls so that they do not occur under closure themselves passed to recursive calls. It is an open question whether it is possible to remove both limitations. A last possible direction is to consider concurrency: while our approach obviously supports sequential consistency, it is not clear that it is usable for that purpose in practice. In particular, our auxiliary language has no support for parallel program composition.

  let rec mcc91 (n: int) : int = if n if (n > 100) { n = n -10; e = e -1; if (e = 0) break; } else { n = n + 11; e = e + 1; }}

Fig. 1 .

 1 Fig. 1. Ghost monitor for the iterative McCarthy 91 function.

Fig. 3 .

 3 Fig. 3. Schorr-Waite graph traversal, main specification.

Fig. 4 .

 4 Fig. 4. Ghost monitor for Schorr-Waite graph traversal.

π0Fig. 5 .

 5 Fig. 5. Transfer property yielding a simulation.

/Fig. 6 .

 6 Fig. 6. Programs (C) and (M) augmented with breakpoints.

Fig. 7 .

 7 Fig. 7. Specifications of CONTC and CONTM .

Fig. 8 .

 8 Fig. 8. Monitor for equivalence of (C) and (M).

Fig. 9 .

 9 Fig. 9. Monitor for equivalence, with divergence handling.

Fig. 10 .

 10 Fig. 10. Syntax of WG.

ΓFig. 11 .

 11 Fig. 11. Typing rules for WG.

  π0 : ϕ0 → y : B. ϕ1 ) (iv) for all H ∈ P(A × G) such that:(a) H is totally ordered by relation r σ (b) H is inhabited and does not have a maximum

Fig. 12 .

 12 Fig. 12. Predicate transformer semantics for WG.

Corollary 1 .

 1 For all games G = (G, , ∆), all well-typed programs CONT : P(G) → {0}|Γ π : {0} of W G , all formula pairs ϕ 0 , ϕ 1 well-typed in context Γ, now : G, and all Γ -assignations σ, if the contract satisfaction property C[(Φ G ) x∈G , σ] (π : ϕ 0 → u : {0}. ϕ 1 ) holds, then there is a victory invariant for the set pair {x ∈

Definition 11 .

 11 A contract P ⊆ A × G, Q ⊆ A × G × B × G is said to be valid with respect to game G = (G, , ∆) if for all (a, x) ∈ A×G, there exists a victory invariant for the set pair {x}, {y ∈ G | ∃b ∈ B. (a, x, b, y) ∈ Q}. By extension, a Σ-specification context Φ is valid with respect to G if all its contracts are valid with respect to G. Theorem 5. For all games G, all well-typed programs Σ|Γ π : B of W G , all Σ-specification contexts Φ valid with respect to G, all subsets Q of B × G, and all assignations σ, there is a victory invariant for the pair T [Φ, σ] (π, Q) , {y ∈ G | ∃b ∈ B. (b, y) ∈ Q}.


Yann Petot

Pierre Vallois

Alexandre Voisin

Choquet integral with stochastic entries

Keywords: capacity, Choquet integral, density function, moments, exponential distribution, uniform distribution AMS 2000 subject classifications : 60E99, 60K10

teaching and research institutions in France or abroad, or from public or private research centers.

Introduction

Since almost 3 decades, the Choquet integral has become a major "actor" in the field of aggregation function and decision making [START_REF] Grabisch | A decade of application of the choquet and sugeno integrals in multi-criteria decision aid[END_REF][START_REF] Grabisch | A decade of application of the Choquet and Sugeno integrals in multi-criteria decision aid[END_REF]. Thanks to theoretical works, many applications have been developed in finance [START_REF] Joo | Enhancing the decision-making virtuous cycle of ethical banking practices using the choquet integral[END_REF], sustainable development [START_REF] Merad | Using a multi-criteria decision aid methodology to implement sustainable development principles within an Organization[END_REF][START_REF] Bykzkan | Selection of sustainable urban transportation alternatives using an integrated intuitionistic fuzzy choquet integral approach[END_REF], image processing [START_REF] Trabelsi | Choquet Integral based Feature Selection for Early Breast Cancer Diagnosis from MRIs[END_REF], recommender system [START_REF] Fomba | A Recommender system based on MultiCriteria Aggregation[END_REF], clustering [START_REF] Andre | Aggregation of neural classifiers using choquet integral with respect to a fuzzy measure[END_REF], deep-learning [START_REF] Dias | Using the choquet integral in the pooling layer in deep learning networks[END_REF], to only cite few in recent years. Despite the amount of studies, the question of uncertainty in the Choquet integral remains under-considered. Such a question is of first importance in many applications and uses. Few works deal with uncertainty considering the entries of the Choquet integral as random variables. Grabisch and Raufaste have proposed in [START_REF] Grabisch | An empirical study of statistical properties of the choquet and sugeno integrals[END_REF] Monte-Carlo simulations to compute in particular cases the empirical mean and standard deviation of the Choquet integral. They draw as conclusion that the exact distribution seems to be hard to obtain. The Choquet integral requires a linear ordering of the entries which generates difficulties when they are random variables. Note that 1 ordering a family of probability distributions is usually done using the notion of stochastic dominance [START_REF] Yager | Stochastic dominance for measure based uncertain decision making[END_REF]. This new notion of order has permitted to Yager in [START_REF] Yager | On using the shapley value to approximate the choquet integral in cases of uncertain arguments[END_REF] to give an approximation of the mean of the Choquet integral based on the Shapley indices [START_REF] Shapleyd | A value for n-person games[END_REF]. To circumvent the initial issue, Yager has introduced in [START_REF] Yager | Evaluating choquet integrals whose arguments are probability distributions[END_REF] a surrogate that allows to compute "the mean-like aggregated value". In both studies, no clear relation is done between the density function of the entries and the density function of the Choquet integral.

As far as we have investigated the literature, the only one contribution which deals with the probability distribution of the Choquet integral has been done by Kojadinovic and Marichal in [START_REF] Kojadinovic | On the moments and distribution of discrete choquet integrals from continuous distributions[END_REF]. Indeed, they have obtained theoretical formulas concerning the moments of the Choquet integral for any form of input distributions. Explicit expressions of the density function of the Choquet integral has also been given but only in the case where the entries are either exponential or uniform. Let µ be a capacity on a finite set S := {1, • • • , n} and X = (X 1 , • • • , X n ) be the stochastic entries. In our setting, X 1 , • • • , X n are independent random variables. The aim of the paper is to study the Choquet integral C µ (X) as a random variable. We are able to determine the density of C µ (X) in Proposition 3.2. The formula is rather complicated but can be simplified (cf Proposition 3.5) if we suppose furthermore that X 1 , • • • , X n have the same density, i.e. X 1 , • • • , X n are independent and identically distributed (i.i.d.). We have shown a new form of the density of C µ (X) given in Proposition 3.5 using auxiliary exponential random variables. We provide a general formulation of the law of the Choquet integral which generalizes the result of Kojadinovic and Marichal. These authors has given a non-explicit formula for the moments of order n of the Choquet integral. In the case of the expectation (i.e. n = 1), we obtain an explicit formulation which is in consistence with Proposition 4 in [START_REF] Kojadinovic | On the moments and distribution of discrete choquet integrals from continuous distributions[END_REF] but our proof uses a different way. Let us briefly explain the structure of the paper. In Section 2, we recall definition of a capacity and the related Choquet integral. In order that the reader has a synthetic overview of our results, the third and fourth sections provides straightforwardly the results for the density function and resp. for the first order moment. Finally, the proofs of the propositions are postponed in Section 5.

Few reminders related to Choquet integral

We briefly recall the definitions of a capacity and the associated Choquet integral over a finite set S := {1, 2, • • • , n}. Definition 2.1 A capacity, also called a fuzzy measure, µ over S is a function defined over the family P(S) of sets included in S, valued in [0, 1] which is non-decreasing:

µ(A) ≤ µ(B), ∀ A, B, A ⊂ B ⊂ S (2.1)
and satisfying: µ(∅) = 0, µ(S) = 1.

Notation 2.2 1. S n stands for the group of permutations of S.

Let

x := (x 1 , • • • , x n ) ∈ R n .
There exists σ ∈ S n such that:

x σ(1) ≤ • • • ≤ x σ(n) . (2.2)
σ is unique if x i = x j for all i = j. Obviously σ depends on x.

3. It is convenient to adopt the notation: x σ(i) = x (i) for any i ∈ S. Therefore (2.2) takes the form:

x (1) ≤ • • • ≤ x (n) . (2.3)
4. If σ : S → S, we set:

σ(a : b) := {σ(i), a ≤ i ≤ b}, 1 ≤ a ≤ b ≤ n.
We convince that σ(a

: b) = ∅ if b > a.
Definition 2.3 Let µ be a capacity over S and x ∈ R n . The Choquet integral of x with respect to µ is the real number:

C µ (x) := n i=1 x (i) µ σ(i : n) -µ σ(i + 1 : n) (2.4)
where σ is the permutation defined by (2.3).

3 The law of C µ (X)

Let µ be a capacity over S = {1, • • • , n} and X := (X 1 , • • • , X n ) be a random vector. In his Phd-thesis (Contributions aux mesures floues k-additives et à l'intégrale de Choquet stochastique. Application aux analyses médico-économiques) Y. Petot has considered the case where only one coordinate of X is random. However, We suppose here that all the components X 1 , • • • , X n are independent random variables and for any i ∈ {1, • • • , n} the random variable X i has a density function f i . Let µ be a given capacity over S = {1, • • • , n}. We focus in this section on the density function of the Choquet integral C µ (X). We calculate it in Proposition 3.2. Unfortunately the formula is not completely explicit since it is the sum of multiple Lebesgue integrals which cannot be simplified in the general case. To get a more tractable result, we suppose moreover that X 1 , • • • , X n have the same density. In that case, we obtain the simpler formula (3.12). In this identity, it is striking (and unexpected) to see that appear elements of Poisson distributions. Introducing additional exponential random variables, independent of X, we can write in Proposition 3.7 the density of C µ (X) as a sum of functions which can be expressed as expectation of some random variables. This is a new shape of the density function of C µ (X). Along the presentation, some relation with [START_REF] Kojadinovic | On the moments and distribution of discrete choquet integrals from continuous distributions[END_REF] are proposed to show how both are connected. Proof of the proposition are postponed in Section 5.

Since the density function of the Choquet integral is complicated, it is natural to wonder if its moments are easier to calculate. We have been only able to (explicitly) calculate the expectation, see Proposition 4.1. We also compare our results to the ones obtained in [START_REF] Kojadinovic | On the moments and distribution of discrete choquet integrals from continuous distributions[END_REF].

Notation 3.1 1. Let τ be a permutation of S. (a) We set i τ := max 1 ≤ j ≤ n, µ τ (j : n) > 0 . Since i → µ τ (i : n) is non-increasing µ τ (j : n) = 0, j ≥ i τ + 1 µ τ (j : n) > 0, 1 ≤ j ≤ i τ .
(b) We also introduce:

a τ := µ τ (i τ : n) -µ τ (i τ + 1 : n) = µ τ (i τ : n) . (3.1)
Note that a τ > 0.

(c) Let θ τ : R → R be the function:

θ τ (v) := R n-iτ 1 {v≤y 1 ≤•••≤y n-iτ } 1≤j≤n-iτ f τ (j+iτ ) (y j ) 1≤j≤n-iτ dy j , v ∈ R. (3.2)
2. Here, we adher to the conventions:

R 0 = 1, 0 i=1 = 1, 0 i=1 = 0. (3.3) Proposition 3.2 Let φ C be the density function of C µ (X). Then φ C (u) = τ ∈Sn φ τ (u) (3.4)
where

φ τ (u) = 1 a τ R iτ -1 f τ (iτ ) u -b τ a τ θ τ u -b τ a τ 1≤j≤iτ -1 f τ (j) (y j ) ×1 {y 1 ≤•••≤y iτ -1 ≤ u-bτ aτ } 1≤j≤iτ -1 dy j (3.5)
and b τ is the coefficient which depends on (y

1 , • • • , y iτ -1 ): b τ := iτ -1 i=1 y i µ τ (i : n) -µ τ (i + 1 : n) . (3.6)
For the proof of Proposition 3. is the sum of φ (1) and φ [START_REF] Dias | Using the choquet integral in the pooling layer in deep learning networks[END_REF] . Let Φ i be the cumulative distribution function of

X i . Case 1. If µ(2) = 0, then i τ = 1, a τ = 1, b τ = 0 and φ (1) (u) = f 1 (u) +∞ u f 2 (y 1 )dy 1 = f 1 (u) 1 -Φ 2 (u) . If µ({2}) > 0, then i τ = 2, a τ = µ(2), b τ = y 1 1 -µ(2) and φ (1) (u) = 1 µ(2) u -∞ f 2 u -y 1 1 -µ(2) µ(2) f 1 (y 1 )dy 1 . Case 2. If µ(1) = 0, then i τ = 1, a τ = 1, b τ = 0 and φ (2) (u) = f 2 (u) +∞ u f 1 (y 1 )dy 1 = f 2 (u) 1 -Φ 1 (u) . If µ(1) > 0, then i τ = 2, a τ = µ(1), b τ = y 1 1 -µ(1) and
φ (1) (u) = 1 µ(1) u -∞ f 1 u -y 1 1 -µ(1) µ(1) f 2 (y 1 )dy 1 .
We can go further than Proposition 3.2, in the i.i.d. case. Let f (resp. F ) be the common probability density function (resp. cumulative distributive function) of the r.v.'s X i . Before stating our result we fix few notations.

Notation 3.4 Let τ be a fixed element in S n .

1. We set:

α i := µ τ (i : n) -µ τ (i + 1 : n) , 1 ≤ i ≤ n. (3.7)
2. Let l be number of elements of {0 ≤ j ≤ n, α j = 0}. Note that α iτ = 0 and therefore l ≥ 1. We set:

{1 ≤ j ≤ n, α j = 0} = {j 1 , • • • , j l } (3.8)
where

1 ≤ j 1 < • • • < j l ≤ n and δ i := j i -j i-1 -1 2 ≤ i ≤ l, δ 1 = j 1 -1. (3.9)
Note that

i τ = j l , a τ = α j l .
(3.10)

3. Let C τ be the constant:

C τ := 1 a τ 1 δ 1 ! × • • • × δ l !(n -j l )! . (3.11) Proposition 3.5 We suppose that the rv's X 1 , • • • , X n are i.i.d.
Then the density function φ C of C µ (X) is given by (3.4), where

φ τ (u) = C τ R l-1 f (x 1 ) × • • • × f (x l-1 )f u -b l-1 a τ 1 -F u -b l-1 a τ n-j l F (x 1 ) δ 1 l-1 r=2 F (x r ) -F (x r-1 ) δr × F u -b l-1 a τ -F (x l-1 ) δ l 1 {x 1 <•••<x l-1 < u-b l-1 aτ } dx 1 ⊗ • • • ⊗ dx l-1 .
(3.12)

and b l-1 := l-1 r=1 α jr x r . Remark 3.6 1. Let ρ 1 , • • • , ρ k+1 in [0, +∞[. Using the fact that the mul- tiple integral R k f (x 1 )ו • •×f (x k )F (x 1 ) ρ 1 k r=2 F (x r )-F (x r-1 ) ρr × 1 -F (x k ) ρ k+1 dx 1 ⊗ • • • ⊗ dx k equals ρ 1 ! × • • • × ρ k+1 ! (k + ρ 1 + • • • + ρ k+1 )! then we can prove that R φ τ (u)du = 1 n! .
2. In the uniform case (i.e. when the distribution of all the random variables is uniform over [0, 1]), the authors in [START_REF] Kojadinovic | On the moments and distribution of discrete choquet integrals from continuous distributions[END_REF] have shown that

φ C (u) = τ ∈Sn φ * τ (u)
, where φ * τ (u) can be expressed either as an operator iterated (n -1) times or an integral over [0, 1] n-1 . Since the function φ τ defined by (3.12) is an integral over [0, 1] l , then φ * τ (u) and φ τ (u) are a priori different. In the case:

µ(A) < µ(B), ∀ A B ⊂ S (3.13)
Kojodinovic and Marichal proved:

φ C (u) = 1 n! τ ∈Sn n i=0 (µ τ i -u) n-1 + j =i (µ τ i -µ τ j ) (3.14)
where a + stands for the positive part of a and µ τ i := µ τ (1, i) . It is actually possible to recover (3.14) using (3.12) since (3.13

) implies l = n, j 1 =, • • • = j n = 1, δ 1 = • • • = δ n = 0.
3. In the exponential case, a nice formula has been given in [START_REF] Kojadinovic | On the moments and distribution of discrete choquet integrals from continuous distributions[END_REF]:

φ C (u) = 1 n! τ ∈Sn n i=1 (µ τ i /i) n-2 j =i (µ τ i /i -µ τ j /j) exp - u (µ τ i /i) (3.15)
under the additional assumption

µ(A) |A| = µ(B) |B| , ∀ A = B (3.16)
where |C| is the number of elements in C.

Proposition 3.5 is a consequence of Proposition 3.2 and its proof is postponed in Section 5.2. Recall that if Z is a random variable which is Poisson distributed with parameter λ, then

P(Z = k) = λ k k! e -λ , k ∈ N.
It is striking to observe that in the right hand-side of (3.12), appears a product of such quantities. Using a Poisson process, we can write (3.12) as the expectation of a random variable. Let (ξ k ) k≥1 a sequence of i.i.d. random variables exponentially distributed with parameter 1, independent of X 1 , • • • , X n and

T 0 := 0, T n := ξ 1 + • • • + ξ n ∀ n ≥ 1. (3.17)
We keep the assumptions given in Proposition 3.5.

Proposition 3.7 Let τ ∈ S n and u ∈ R. Then,

φ τ (u) = e a τ E f u -B * a τ 1 A 1 A 2 (u) (3.18)
where

A 1 := {T n-l ≤ 1 < T n-l+1 } l-1 r=1 T jr-r ≤ F (X r ) < T jr-r+1 A 2 (u) := X 1 < • • • < X l-1 < u -B * a τ T j l -l ≤ F u -B * a τ < T j l -l+1
and B * =:

l-1 r=1 α jr X r .
The proof of Proposition 3.7 is given in Section 5.3.

Expectation

Since the density function of the Choquet integral is complicated, it is natural to wonder if its moments are easier to calculate. We have been only able to (explicitly) calculate the expectation, see Proposition 4.1. We also compare our results to the ones obtained in [START_REF] Kojadinovic | On the moments and distribution of discrete choquet integrals from continuous distributions[END_REF]. We are interested in the calculation of the expectation and the variance of C µ (X) where X is a random vector and µ is a given capacity. We set:

µ(k) := A⊂S,|A|=k µ(A), 0 ≤ k ≤ n. (4.1)
where |A| is the number of elements of A.

Proposition 4.1 The first moment of C µ (X) is E C µ (X) = n i=1 µ(i)E F (X 1 ) n-i-1 1 -F (X 1 ) i-1 X 1 nF (X 1 ) + i -n . (4.2)
The proof of Proposition 4.1 is given in Subsection 5.4.

Remark 4.2 1. In (Proposition 4, [START_REF] Kojadinovic | On the moments and distribution of discrete choquet integrals from continuous distributions[END_REF]), for any integer r, an expression of the moment of order r of C µ (X) has been given but it involves expectations of random variables. In the case r = 1, the formula coincides with (4.2) The calculation of the second moment of C µ (X) is possible but is very complicated and do not lead to a simple formula.

In the particular case of uniform distribution, Kojadinovic and Marichal

have given an explicit formula for E C µ (X) which takes the form

E C µ (X) = 1 (n + 1)! n i=1 i! (n -i)! µ(i) when r = 1.
It is easy to recover the previous identity from (4.2).

Proofs

Proof of Proposition 3.2

Let g : R → R be a test function. Note that if τ ∈ S n , then

{σ = τ } = {X τ (1) < • • • X τ (n) }. Therefore, E g C µ (X) = τ ∈Sn E g C µ (X) 1 {X τ (1) ≤•••≤X τ (n) } .
Since the random variables X 1 , • • • , X n are independent and X i admits a density function f i , we can write the above expectation as:

E g C µ (X) = τ ∈Sn R n g C µ (x) 1 {x τ (1) ≤•••≤x τ (n) } f 1 (x 1 )ו • • f n (x n ) dx 1 ⊗• • •⊗dx n . (5.1)
Using the definition of i τ , we have

C µ (x) = n i=1 x τ (i) µ τ (i : n) -µ τ (i + 1 : n) = iτ -1 i=1 x τ (i) µ τ (i : n) -µ τ (i + 1 : n) + x τ (iτ ) µ τ (i τ : n) .
In each integral of (5.1), we change the variable x τ (iτ ) , setting

u = iτ -1 i=1 x τ (i) µ τ (i : n) -µ τ (i + 1 : n) + x τ (iτ ) µ τ (i τ : n) = b τ + a τ x τ (iτ )
where

a τ = µ τ (i τ : n) b τ = iτ -1 i=1 x τ (i) µ τ (i : n) -µ τ (i + 1 : n) .
Then,

E g C µ (X) = τ ∈Sn R g(u)   1 a τ R n-1 f τ (iτ ) u -b τ a τ j =iτ f τ (j) (x τ (j) ) ×1 {x τ (1) ≤•••≤x τ (iτ -1) ≤ u-bτ aτ ≤x τ (iτ +1) ≤•••≤x τ (n) } j =iτ dx τ (j)   du
We can integrate with respect to

dx τ (iτ +1) ⊗ • • • ⊗ dx τ (n) E g C µ (X) = τ ∈Sn R g(u) 1 a τ R iτ -1 f τ (iτ ) u -b τ a τ θ τ u -b τ a τ ×1 {x τ (1) ≤•••≤x τ (iτ -1) ≤ u-bτ aτ } 1≤j≤iτ -1 f τ (j) (x τ (j) ) × 1≤j≤iτ -1 dx τ (j)   du with θ τ (v) := R n-iτ 1 {v≤x τ (iτ +1) ≤•••≤x τ (n) } iτ +1≤j≤n f τ (j) (x τ (j) ) iτ +1≤j≤n dx τ (j) .
This proves (3.5).

Proof of Proposition 3.5

Recall that θ τ (v) has been defined by (3.2). This quantity can be calculated explicitly.

Lemma 5.1 For any v:

θ τ (v) = 1 (n -i τ )! (1 -F (v) n-iτ . (5.2)
Proof.

Since the r.v.'s X 1 , • • • , X n are i.i.d., they have the same probability density f . Therefore θ τ (v) takes the simpler form:

θ τ (v) = R m f (y 1 ) × • • • × f (y m )1 {v<y 1 <•••<ym} dy 1 ⊗ • • • ⊗ dy m where m := n -i τ . Let g be a symmetric function of m variables, i.e. g(y 1 , • • • , y m ) = g(y ρ(1) , • • • , y ρ(m) ) for any permutation ρ of {1, • • • , m} and (y 1 , • • • , y m ) ∈ R m . Then R m g(y 1 , • • • , y m )dy 1 ⊗• • •⊗dy m = m! R m g(y 1 , • • • , y m )1 {y 1 <•••<ym} dy 1 ⊗• • •⊗dy m . (5.3) Applying this identity with g(y 1 , • • • , y m ) = f (y 1 )1 {v<y 1 } ו • •×f (y m )1 {v<ym} we get: θ τ (v) = 1 m! R m f (y 1 )1 {v<y 1 } × • • • × f (y m )1 {v<ym} dy 1 ⊗ • • • ⊗ dy m = 1 m! R f (y)1 {v<y} m .
The result follows since

F (v) = v -∞ f (y)dy.
We are now able to prove Proposition 3.5. By Proposition 3.2, Lemma 5.1 and (3.10), we have:

φ τ (u) = 1 a τ (n -j l )! R j l -1 f u -b τ a τ 1 -F u -b τ a τ n-j l ×f (y 1 ) × • • • × f (y j l -1 )1 {y 1 ≤•••≤y j l -1 ≤ u-bτ aτ } dy 1 ⊗ • • • ⊗ dy j l - 1 . By (3.7), (3.8) and (3.10)
, the coefficient b τ defined by (3.6) equals

b τ = j l -1 i=1 α i y i = l-1 i=1 α j i y j i
and therefore only depends on the variables y j 1 • • • y j l-1 . Our strategy is to fix y j 1 • • • y j l-1 and to integrate with respect to the other variables. We integrate first with respect to

dy j l-1 +1 ⊗• • •⊗dy j l -1 the function f (y j l-1 +1 )× • • • × f (y j l -1 ) over y j l-1 , u -b τ a τ with the constrain y j l-1 +1 < • • • < y j l -1 .
Using (5.3), we get :

1 δ l ! F u -b τ a τ -F (y j l-1 ) δ l
which is fixed since y j 1 , • • • , y j l-1 are supposed to be given. We continue, integrating with respect to

dy j l-2 +1 ⊗• • •⊗dy j l-1 -1 the function f (y j l-2 +1 )× • • • f (y j l-1 -1 ) over [y j l-2 , y j l-1 ] with the constrain y j l-2 +1 < • • • < y j l-1 -1 leads to 1 δ l-1 ! F (y j l-1 ) -F (y j l-2 ) δ l-1
.

And so on. The last integration is related to dy 1 ⊗ • • • ⊗ dy j 1 -1 and gives

1 (j 1 -1)! F (y j 1 ) j 1 -1 = 1 δ 1 ! F (y j 1 ) δ 1 .
Finally, setting x 1 = y j 1 , • • • , x l-1 = j l-1 , we get :

φ τ (u) = C τ R l-1 f (x 1 ) × • • • × f (x l-1 )f u -b l-1 a τ 1 -F u -b l-1 a τ n-j l ×F (x 1 ) δ 1 l-1 r=2 F (x r ) -F (x r-1 ) δr F u -b l-1 a τ -F (x l-1 ) δ l ×1 {x 1 ≤•••≤x l-1 ≤ u-b l-1 aτ } dx 1 ⊗ • • • ⊗ dx l-1
where:

C τ = 1 a τ (n -j l )! 1 δ 1 ! × • • • × δ l ! and b l-1 := α j 1 x 1 + • • • + α j l-1 x l-1 .

Proof of Proposition 3.7

According to Proposition 3.5,

φ τ (u) = 1 a τ R l-1 f (x 1 )ו • •×f (x l-1 )ψ 1 (x 1 , • • • , x l-1 )dx 1 ⊗• • •⊗dx l-1 (5.4)
where

ψ 1 (x 1 , • • • , x l-1 ) := f u -b l-1 a τ ψ 2 (x 1 , • • • x l-1 )1 {x 1 <•••<x l-1 < u-b l-1 aτ } and ψ 2 (x 1 , • • • x l-1 ) = F (x 1 ) δ 1 δ 1 ! l-1 r=2 F (x r ) -F (x r-1 ) δr δ r ! × F u-b l-1 aτ -F (x l-1 ) δ l δ l ! 1-F u-b l-1 aτ n-j l (n-j l )!
It is very convenient to introduce:

y 0 := 0, y i := F (x i ) ∀ 1 ≤ i ≤ l -1, y l := F u -b l-1 a τ , y l+1 := 1. Since x 1 < • • • < x l-1 < u -b l-1 a τ , then y 0 ≤ • • • < y l+1 and ψ 2 (x 1 , • • • , x l-1 ) = e l+1 r=1
(y r -y r-1 ) δr δ r ! e -(yr-y r-1 ) .

where δ l+1 := n -j l . Let (N t ) t≥0 be a Poisson process with parameter 1 and independent of

X 1 , • • • , X n . Then 1. The random variables N y 1 , N y 2 -N y 1 , • • • , N y l+1 -N y l are independent,
2. for any r ∈ {1, • • • , l + 1}, the random variable N yr -N y r-1 is Poisson distributed with parameter y r -y r-1 .

We are now able to interpret ψ 2 (x 1 , • • • x l-1 ):

ψ 2 (x 1 , • • • , x l-1 ) = e l+1 r=1 P N yr -N y r-1 = δ r = eP l+1 r=1 {N yr -N y r-1 = δ r } = eP l+1 r=1 {N yr = δ 1 + • • • + δ r }
Let (T n ) n≥1 be the increasing sequence of the jump times of (N t ) t≥0 :

N t = n≥1 1 {Tn≤t} , t ≥ 0.
Consequently:

{N t = k} = {T k ≤ t < T k+1 }, t ≥ 0, k ∈ N
and therefore

ψ 2 (x 1 , • • • , x l-1 ) = eP l+1 r=1
{T jr-r ≤ y r < T jr-r+1 } because relation (3.9) implies:

δ 1 + • • • + δ r = j r -r, 1 ≤ r ≤ l + 1 with the convention j l+1 = n + 1. It is well-know that (T n ) n≥1 is distributed as (ξ 1 + • • • + ξ n ) n≥1
where (ξ k ) k≥1 is a sequence of i.i.d. random variables exponentially distributed with parameter 1. Finally relation (5.4) and the independency of (ξ k ) k≥1 and (X 1 , • • • , X n ) implies (3.18).

Proof of Proposition 4.1

Recall that the quantity µ(k) has been defined by (4.1).

Lemma 5.2 Let 1 ≤ i ≤ n. Then τ ∈Sn µ τ (i : n) = (i -1)! (n -i + 1)! µ(n -i + 1). ( 5.5)
Proof. We have:

τ ∈Sn µ τ (i : n) = A⊂S,|A|=n-i+1 τ ∈Sn,A=τ (i:n) µ τ (i : n) = A⊂S,|A|=n-i+1 µ(A) τ ∈S,A=τ (i:n) 1 = (i -1)!(n -i + 1)! A⊂S,|A|=n-i+1 µ(A) since if A ⊂ S is given and A = τ (i : n) then the image of {1, • • • , i -1} (resp. {i, • • • , n}) is A c (resp. A
) and the number of possibilities is (i -1)! × (n -i + 1)!. Then (5.5) is a direct consequence of (4.1).

Lemma 5.3 For any 1 ≤ i ≤ n,

E X i 1 {X 1 <•••<Xn} = 1 (i -1)!(n -i)! E F (X 1 ) i-1 1-F (X 1 ) n-i X 1 . (5.6) Proof. Let 1 ≤ i ≤ n, then E X i 1 {X 1 <•••<Xn} = E 1 {X 1 <•••<X i-1 <X i } X i 1 {X i <X i+1 •••<Xn} .
Recall that X 1 , • • • , X n are i.i.d. then

E X i 1 {X 1 <•••<Xn} = E θ i-1 (X i )X i θ n-i (X i )
where

θ k (x) := R k f (x 1 ) × • • • × f (x k )1 {x 1 <•••<x k <x} dx 1 ⊗ • • • ⊗ dx k θ k (x) := R k f (x 1 ) × • • • × f (x k )1 {x<x 1 <•••<x k } dx 1 ⊗ • • • ⊗ dx k .
Using (5.3), θ k (x) can be simplified:

θ k (x) = 1 k! R k f (x 1 ) × • • • × f (x k )1 {x 1 <x,••• ,<x k <x} dx 1 ⊗ • • • ⊗ dx k = F (x) k k! .
Similarly,

θ k (x) = 1 -F (x) k k! .
The proof of (5.6) is now complete since X i and X 1 have the same distribution.

We are now able to prove Proposition 4.1. By definition,

C µ (X) = n i=1
X σ(i) µ σ(i : n) -µ σ(i + 1 : n)

where σ is the random permutation such that X σ(1) < • • • < X σ(n) . We modify the previous sum:

C µ (X) = n i=1 X σ(i) µ σ(i : n) - n i=1 X σ(i) µ σ(i + 1 : n) = n i=1 µ σ(i : n) (X σ(i) -X σ(i-1) )
with the conventions: σ(0) = 0, X 0 = 0 and µ σ(n + 1 : n) = 0. Therefore

C µ (X) = τ ∈Sn n i=1 µ σ(i : n) (X σ(i) -X σ(i-1) ) 1 {σ=τ } = τ ∈Sn n i=1 µ τ (i : n) (X τ (i) -X τ (i-1) ) 1 {X τ (1) <•••<X τ (n) } . (5.7)
We take the expectation and we use the crucial fact that (X τ (1) , • • • , X τ (n) ) is distributed as (X 1 , • • • , X n ):

E C µ (X) = τ ∈Sn n i=1 µ τ (i : n) E (X τ (i) -X τ (i-1) )1 {X τ (1) <•••<X τ (n) } = τ ∈Sn n i=1 µ τ (i : n) E (X i -X i-1 )1 {X 1 <•••<Xn} = n i=1 τ ∈Sn µ τ (i : n) E (X i -X i-1 )1 {X 1 <•••<Xn} .
Using Lemma 5.3, we gat for i ≥ 2:

E (X i -X i-1 )1 {X 1 <•••<Xn} = E X i 1 {X 1 <•••<Xn} -E X i-1 1 {X 1 <•••<Xn} = 1 (i -1)!(n -i)! E F (X 1 ) i-1 1 -F (X 1 ) n-i X 1 - 1 (i -2)!(n -i + 1)! E F (X 1 ) i-2 1 -F (X 1 ) n-i+1 ×X 1 . Consequently E (X i -X i-1 )1 {X 1 <•••<Xn} = 1 (i -1)!(n -i + 1)! E F (X 1 ) i-2 1-F (X 1 ) n-i X 1 Y

where

We use finally Lemma 5.2:

ReferencesReferences