Min Zhang
email: zhangmin@sei.ecnu.edu.cn

Frédéric Mallet
email: frederic.mallet@unice.fr

An Executable Semantics of Clock Constraint Specification Language and its Applications

The Clock Constraint Specification Language (ccsl) is a language to specify logical and timed constraints between logical clocks. Given a set of clock constraints specified in ccsl, formal analysis is preferred to check if there exists a schedule that satisfies all the constraints, if the constraints are valid or not, and if the constraints satisfy expected properties. In this paper, we present a formal executable semantics of ccsl in rewriting logic and demonstrate some applications of the formal semantics to its formal analysis: 1) to automatically find bounded or periodic schedules that satisfy all the given constraints; 2) to simulate the execution of schedules with customized simulation policies; and 3) to verify LTL properties of ccsl constraints by bounded model checking. Compared with other existing modeling approaches, advantages with the rewriting-based semantics of ccsl are that we do not need to assume a bounded number of steps for the formalization, and we can exhaustively explore all the solutions within a given bound for the analysis.

Introduction

Logical time such as defined by Lamport [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] gives a flexible abstraction to compare and order occurrences of events when appealing to more traditional physical measures is either not possible or not desirable. This is the case in a great variety of application domains, from widely distributed systems, for which maintaining a global clock can be costly, to deeply embedded software or in latency-insensitive designs [START_REF] Carloni | Theory of latencyinsensitive design[END_REF], for which the complexity of the control mechanisms (like frequency scaling) makes it neither desirable nor efficient. In the latter case, synchronous languages [START_REF] Benveniste | The synchronous languages 12 years later[END_REF][START_REF] Potop-Butucaru | The Synchronous Hypothesis and Polychronous Languages[END_REF] have shown that logical clocks can give a very adequate tool to represent any recurrent event uniformly, whether occurring in a periodic fashion or not.

The Clock Constraint Specification Language (ccsl) [START_REF] Mallet | CCSL: specifying clock constraints with UM-L/Marte[END_REF] is a language that handles logical clocks as first-class citizens. While synchronous languages mainly focus on signals and values and use logical clocks as a controlling mechanism, ccsl discards the values and only focuses on clock-related issues. The formal The final pulication is available at Springer via http://dx.doi.org/10.1007/978-3-319-29510-7_2 operational semantics of ccsl was initially defined in a research report [START_REF] André | Syntax and semantics of the Clock Constraint Specification Language (CCSL)[END_REF] in a bid to provide a reference semantics for building simulation tools, like TimeSquare [START_REF] Deantoni | Timesquare: Treat your models with logical time[END_REF]. We are interested here in studying the properties of a ccsl specification and we give another formal executable semantics in rewriting logic and demonstrate the benefits of this new semantics. The first benefit is that rewriting logic gives a direct implementation of the operational semantics while TimeSquare provides a Java-based implementation, which is prone to introduce accidental complexity.

The second and most important benefit is that we can directly use rewriting logic tooling to model-check a ccsl specification. Previous works on studying ccsl properties [START_REF] Mallet | Correctness issues on MARTE/CCSL constraints[END_REF], rely on several intermediate transformations to automata and other specific formats so that model-checking becomes possible when a ccsl specification is finite (or safe) [START_REF] Mallet | Safe CCSL specifications and marked graphs[END_REF]. It either meant, reducing to a safe subset of ccsl [START_REF] Gascon | Logical time and temporal logics: Comparing UML MARTE/CCSL and PSL[END_REF] or detecting that the specification was finite even though relying on unsafe operators. In this contribution, we rely on Maude environment [START_REF] Clavel | All about Maude[END_REF] to provide a direct analysis support from the operational semantics and we can explore unsafe specifications by using bounded-model checking and do not restrict to the safe subset. While before, successive intermediate transformations could each introduce variations in the semantics, if not careful enough, we rely here on the strong, widely used, generic tooling provided by Maude, rather than on an ad-hoc manual implementation.

More precisely, in this paper, we introduce the notions of bounded and periodic schedules for a ccsl specification. Periodic schedules are useful to reason on specifications that rely on unsafe operators. With periodic schedules, we can use bounded model-checking to verify temporal logic properties on ccsl models. The tooling and automatic verification directly comes with the newly introduced semantics and the Maude environment.

The rest of the paper is organized as follows. Section 2 and Section 3 give a brief introduction to ccsl and Maude. In Section 4 we present the formal definition of semantics of ccsl in Maude, and in Section 5 we demonstrate four applications of the formal semantics to the analysis of ccsl. Section 6 mentions some related work and Section 7 concludes the paper.

CCSL

Syntax and semantics of CCSL

In ccsl, there are four primitive constraint operators which are binary relations between clocks, and five kinds of clock definitions [START_REF] Mallet | CCSL: specifying clock constraints with UM-L/Marte[END_REF]. The four constraint operators are called precedence, causality, subclock and exclusion; and the five clock definitions are called union, intersection, infimum, supremum, and delay.

The meaning of the nine primitive operators (see Fig. 1) is given using the notions of schedule and history. Given a set C of clocks, a schedule of C is used to decide which clocks can tick at a given step, and a history is used to calculate the number of ticks of each clock at a given step. Note that a schedule must be non-trivial such that there is at least one clock ticking at any execution step. This condition excludes from schedules those steps where no clocks tick. Such steps are called empty steps and are trivial in that adding them to a schedule does not affect the logical relations among clocks.

Definition 1 (Schedule). Given a set C of clocks, a schedule of C is a total function δ ∶ N + → 2 C such that for any n in N + , δ(n) ≠ ∅. 1. δ ⊧ c 1 ≺ c 2 ⇐⇒ ∀n ∈ N + .χ(c 1 , n) = χ(c 2 , n) ⇒ c 2 ∈ δ(n + 1) (Precedence) 2. δ ⊧ c 1 ⪯ c 2 ⇐⇒ ∀n ∈ N + .χ(c 1 , n) ≥ χ(c 2 , n) (Causality) 3. δ ⊧ c 1 ⊆ c 2 ⇐⇒ ∀n ∈ N + .c 1 ∈ δ(n) ⇒ c 2 ∈ δ(n) (Subclock) 4. δ ⊧ c 1 c 2 ⇐⇒ ∀n ∈ N + .c 1 ∈ δ(n) ∨ c 2 ∈ δ(n) (Exclusion) 5. δ ⊧ c 1 ≜ c 2 + c 3 ⇐⇒ ∀n ∈ N + .(c 1 ∈ δ(n) ⇐⇒ c 2 ∈ δ(n) ∨ c 3 ∈ δ(n)) (Union) 6. δ ⊧ c 1 ≜ c 2 × c 3 ⇐⇒ ∀n ∈ N + .(c 1 ∈ δ(n) ⇐⇒ c 2 ∈ δ(n) ∧ c 3 ∈ δ(n)) (Intersection) 7. δ ⊧ c 1 ≜ c 2 ∧ c 3 ⇐⇒ ∀n ∈ N + .χ(c 1 , n) = max(χ(c 2 , n), χ(c 3 , n)) (Infimum) 8. δ ⊧ c 1 ≜ c 2 ∨ c 3 ⇐⇒ ∀n ∈ N + .χ(c 1 , n) = min(χ(c 2 , n), χ(c 3 , n)) (Supremum) 9. δ ⊧ c 1 ≜ c 2 d ⇐⇒ ∀n ∈ N + .χ(c 1 , n) = max(χ(c 2 , n) -d, 0) (Delay)

Definition 2 (History). A history of a schedule

δ ∶ N + → 2 C over a set C of clocks is a function χ ∶ C × N → N such that for any clock c ∈ C and n ∈ N: χ(c, n) = ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ 0 if n = 0 χ(c, n -1) if n ≠ 0 ∧ c ∈ δ(n) χ(c, n -1) + 1 if n ≠ 0 ∧ c ∈ δ(n)
We use δ ⊧ φ to denote that schedule δ satisfies constraint φ. Fig. 1 shows the definition of the satisfiability of a constraint φ with regards to a schedule δ. We take the definition of precedence for example. δ ⊧ c 1 ≺ c 2 holds if and only if for any n in N, c 2 must not tick at step n+1 if the number of ticks of c 1 is equal to the one of c 2 at step n. Precedence and causality are asynchronous constraints and they forbid clocks to tick depending on what has happened on other clocks in the earlier steps. Subclock and exclusion are synchronous constraints and they force clocks to tick or not depending on whether another clock ticks or not in the same step. Union defines a clock c 1 which ticks whenever c 2 or c 3 ticks; intersection defines a clock c 1 which ticks whenever both c 2 and c 3 tick; supremum defines the slowest clock c 1 which is faster than both c 2 and c 3 ; infimum defines the fastest clock c 1 which is slower than both c 2 and c 3 ; and delay defines the clock c 1 which is delayed by c 2 with d steps. More details can be found in a recent study on ccsl [START_REF] Mallet | Correctness issues on MARTE/CCSL constraints[END_REF].

Given a set Φ of clock constraints and a schedule δ, δ satisfies Φ (denoted by δ ⊧ Φ) if for any φ in Φ there is δ ⊧ φ. In particular, we use δ; k ⊧ φ to denote that δ satisfies φ at step k(k ∈ N + ). We use δ; k ⊧ Φ to denote that δ satisfies all the constraints in Φ at step k, i.e., ∀φ ∈ Φ, δ; k ⊧ φ. Bounded schedule is sometimes too restrictive in practice because we usually do not assign a bound to clocks in real-time embedded systems, but assume that reactive systems run forever and only terminate when shutdown. Thus, clocks should tick infinite often from the theoretical point of view. There is another class of schedules which are unbounded and force all the clocks to occur periodically. We call them periodic schedules.

Definition 4 (Periodic schedule).

A schedule δ is periodic if there exists k, p in N such that for any

k ′ ≥ k, δ(k ′ + p) = δ(k ′ ).
Figure 2 depicts a periodic schedule whose period is p. Each node denotes a time point, and each arrow denotes the elapse of a time unit. The dashed line indicates that, for any clock, it ticks at one point if and only if it ticks at the other point. From step k, the schedule starts to repeat every p steps infinitely. To decide whether there exists a periodic schedule for a given set of clock constraints is also an open problem. In the rest of this section, we propose an approach to constructing a periodic schedule from a bounded one when the bounded one satisfies certain conditions which are to be introduced below.

1 start 2 . . . k . . . k1 . . . k ′ . . . x . . . n . . . k ′ -k k1 = k + (x -k)%(k ′ -k) δ δ ′ Fig. 3. Construction of periodic schedule δ ′ from an n-bounded schedule δ Lemma 1. Given a schedule δ ∶ N + → 2 C and two natural numbers k, k ′ , if there exists m ∈ N such that for any c in C χ(c, k) + m = χ(c, k ′ ) and χ(c, k + 1) + m = χ(c, k ′ + 1) then δ(k + 1) = δ(k ′ + 1). Proof. It is equal to prove that for any c ∈ C, c ∈ δ(k + 1) ⇐⇒ c ∈ δ(k ′ + 1). (⇒): c ∈ δ(k + 1) implies that χ(c, k + 1) = χ(c, k) + 1. Thus, χ(c, k + 1) + m = χ(c, k ′ + 1) = χ(c, k) + 1 + m = χ(c, k ′ ) + 1. Thus, c ∈ δ(k ′ + 1). (⇐): c ∈ δ(k ′ +1) implies that χ(c, k ′ +1) = χ(c, k ′ )+1. Namely, χ(c, k+1)+m = χ(c, k) + m + 1. Thus, χ(c, k + 1) = χ(c, k) + 1, and hence we have c ∈ δ(k + 1). ⊓ ⊔ Theorem 1. Given a schedule δ ∶ N + → 2 C , a clock constraint φ, and two natural numbers k, k ′ , δ; k ⊧ φ ⇒ σ; k ′ ⊧ φ if
all the following three conditions are true:

1. δ(k) = δ(k ′ ); 2.
There exists m in N such that m > 0 and for any c in C, χ(c, k

)+m = χ(c, k ′ ) and χ(c, k + 1) + m = χ(c, k ′ + 1); 3. If φ ≡ (c 1 ≜ c 2 $ d), χ(c 2 , k) ≥ d.
Theorem 1 can be proved with Lemma 1. We omit the proof due to the limit of space. From Theorem 1 we can directly derive the following corollary.

Corollary 1. Given a schedule δ ∶ N + → 2 C , a set Φ of clock constraints, and two natural numbers n, k ′ , δ; k ⊧ Φ ⇒ σ; k ′ ⊧ Φ if the three conditions in Theorem 1 are satisfied.

Given an n-bounded schedule δ of a set Φ of clock constraints, if there exist two natural numbers k, k ′ ≤ n, which satisfy the three conditions in Theorem 1, we can define a periodic schedule δ ′ based on δ such that δ ′ satisfies Φ.

δ ′ (x) = δ(x) if x ≤ k ′ δ(k + (x -k)%(k ′ -k)) if x > k ′ Figure 3 shows the construction of δ ′ based on δ. From k ′ , the schedule δ ′ repeats infinitely the steps from k to k ′ -1. By Corollary 1, it is obvious that for any k ′′ such that k ′′ > k ′ , we have δ ′ ; k ′′ ⊧ Φ because we can find a natural number k 1 = k +(k ′′ -k)%(k ′ -k) such that δ; k 1 ⊧ Φ, δ(k 1 ) = δ ′ (k 1 ) and k ′′ , k 1 , δ ′
satisfy the three conditions in Theorem 1. Thus, we have δ ′ ⊧ Φ.

Maude is rewriting-based algebraic language and also an efficient rewriting engine. We assume the readers are familiar with Maude, and only give a brief introduction to Maude meta-level functionality and Maude LTL model checking, which is used in this paper. More details about Maude can be found in the Maude book [START_REF] Clavel | All about Maude[END_REF].

The underlying logic of Maude is rewriting logic, which is reflective in the sense that it can be faithfully interpreted in itself [START_REF] Clavel | All about Maude[END_REF]. The reflectivity allows us to reason with a specified rewrite theory in customized strategies by Maude. Intuitively, we define a rewrite theory R and then define a metatheory U where R is treated as data. A rewrite theory R is a tripe ⟨Σ, E, R⟩, where Σ is called the signature specifying the type structure, E is a set of equations and R is a set of rewrite rules. Maude provides efficient function by command search to find if there exist some pathes from a given term t to a target term t ′ by repeatedly applying the rewrite rules in R. It also provides a corresponding meta-level searching function metaSearch which takes R, t and t ′ as arguments and returns the searching result. An LTL model checker has been implemented based on Maude to verify LTL properties of a rewrite theory when the set of states that are reachable from an initial state in the rewrite theory is finite [START_REF] Eker | The Maude LTL model checker[END_REF].

Formal Semantics of CCSL in Maude

We formalize a clock as a triple (c, , n), consisting of the clock identifier c, a list of records, with each value being tick or idle (abbreviated by t or i respectively), representing that the clock ticks or not at the corresponding step, and a natural number n to indicate the numbers of ticks in . represents a bounded schedule of c whose bound is equal to the length of . Initially, is empty and n is 0. Let C be the set of such clock triples of a set C of clocks. We call C a configuration.

We suppose that the length of the lists in each clock triple in C are equal, e.g. n. C essentially represents an n-bounded schedule for all the clocks in C.

We declare a predicate satisfy which takes three arguments: a configuration C, a non-zero natural number k, and a set Φ of constraints, and returns true if C satisfies Φ at step k, and otherwise false. We consider each possible constraint form in Φ when defining satisfy. For instance, the following two equations are defined to specify a configuration C satisfies precedence and infimum at step k:

1 ceq satisfy (C , k, c1 ≺ c2 ) = ( num ( 1 ,k) >= num ( 2 , k) ) and 2 ( if num ( 1 ,k -1) == num ( 2 , k -1) then t -val ( 2 ,k) =/= t else true fi ) 3 if (c1 , 1 , n1 ) := getConf (C , c1 ) /\ (c2 , 2 , n2 ) := getConf (C , c2 ) . 4 ceq satisfy (C , k, c1 ≜ c2 ∧ c3 ) = ( if n2 > n3 then n1 == n2 else n1 == n3 fi ) 5 if (c1 , 1 , n1 ) := getConf (C , c1 ) /\ (c2 , 2 , n2 ) := getConf (C , c2 ) 6 /\ (c3 , 3 , n3 ) := getConf (C , c2 ) .
The first equation says that satisfy returns true with C, k and c 1 ≺ c 2 when the number of ticks of c 1 up to step k is greater than or equal to the one of c 2 and further if the number of ticks of c 1 up to step k-1 is the same as the one of c 2 then c 2 must not tick at step k (as represented by t-val( 2 ,k) =/= t, where t-val is a function returning the k th value in the list 2 ). The equation has a condition which is a conjunction of two matching equations [START_REF] Clavel | All about Maude[END_REF]. The two conjuncts are used to retrieve the tick list and the number of ticks of c 1 (and c 2 ) by function getConf and assign them to 1 and n 1 (and 2 and n 2 ). The second equation defines the semantics of infimum relation, namely, at any step k the number of ticks of c 1 must be the minimum of those of c 2 and c 3 . The correspondence between the formalization of the constraints and their formal semantics defined in Figure 1 should be clear. Other constraints can be formalized in Maude likewise, and we omit them from the paper.

Next we formalize one-step ticking from k to k + 1 of all clocks by a set of rewrite rules. The basic idea is as follows. From step k to k + 1 each clock decides to tick or not (be idle). After all the clocks make a decision, we check if the bounded schedule satisfies all the constraints at step k + 1. The first rewrite rule at Line 1 specifies the behavior that clock c ticks at step k + 1. The list is changed into t. The rule is conditional because we need the condition that c is not the last clock which makes a decision. If c is the last one, we need to check if all the constraints in Φ are satisfied at step k + 1. The step k can be represented by the length of the list of an arbitrary clock triple in C, i.e., k = size( ), where size( ) returns the length of . Thus, k + 1 is equal to size( ) + 1, and hence we use the latter one in the condition of the fourth equation on Line 6.

Similarly, if c decides to remain idle next step and c is not the last clock, its corresponding tick list is changed from to i, which is specified by the rule on Line 2. If c is the last clock in this case, we also need to guarantee that from step k to k + 1 there must be at least one clock ticking (represented by the formula not allIdle(C ′ )) and all the clocks satisfy the constraints in Φ at step k + 1.

1 crl ((c, , n) C ; C ′ ; Φ) = > (C ; C ′ (c, t, n + 1) ; Φ) if C =/= nil . 2 crl ((c, , n) C ; C ′ ; Φ) = > (C ; C ′ (c, i, n) ; Φ) if C =/= nil . 3 crl ((c, , n) ; C ′ ; Φ) = > ( nil ; C ′ (c, t, n + 1) ; Φ ) 4 if satisfy (C ′ (c, t, n + 1), size ( ) + 1 , Φ) . 5 crl ((c, , n) ; C ′ ; Φ) = > ( nil ; C ′ (c, i, n) ; Φ) 6 if not allIdle (C ′ ) /\ satisfy (C ′ (c, i, n), size ( ) + 1 , Φ) .
We assume that C is a k-bounded schedule of a set Φ of ccsl constraints. If there is a rewriting sequence from (C; nil; Φ) to a new one (nil; C ′ ; Φ) with the above four rules, C ′ must be a k + 1-bounded schedule of Φ because C ′ satisfies Φ up to k + 1 steps. We can define the following rule to specify the one-step ticking of all the clocks from step k to k + 1.

1 crl < C ; k ; Φ > = > < C ′ ; k + 1 ; Φ > if (C ; nil ; Φ) = > ( nil ; C ′ ; Φ) .
The condition of the rule is a rewrite condition [START_REF] Clavel | All about Maude[END_REF], which is true if and only if there exists a rewriting sequence from the term at the left-hand side of => to the one at the right-hand side when the condition is true. In the above rule, C ′ represents an arbitrary immediate successor of C such that C ′ satisfies Φ up to k + 1 steps.

In this section, we show four applications of the executable formal semantics of ccsl in Maude.

Bounded scheduling

Given a bound n and a set of clock constraints Φ, we can use Maude's search function to find automatically if there exists an n-bounded schedule of Φ. If Maude cannot find a schedule within a given bound n, it means that there must not exist such an n-bounded schedule, and further we can conclude that there must not exist a schedule that satisfies Φ. However, if a schedule is found up to bound n, we only can conclude that the returned schedule is n-bounded, but cannot guarantee the existence of a schedule for Φ.

We show an example of finding bounded schedules for a given set of clock constraints using Maude's search command.

Example 1. Given a set of constraints

Φ 1 = {c 1 ≺ c 2 , c 3 ≜ c 1 $ 1 , c 2 ≺ c 3 ,

(c1 ,t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t 5 i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i 6 t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i ,50)

(c2 ,i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i 8 t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t 9 i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t ,50)

(c3 ,i i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t 11 i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i 12 t i t i t i t i t i t i t i t i t i t i t i t i t i t i t i ,49)

Maude's search command takes two optional arguments in the square brackets. The first one is used to specify the number of expected solutions, and the second one is used to specify the maximal depth of searching. Function init takes a set Φ of constraints and generates an initial configuration < C 0 ; 0 ; Φ >, where C 0 is a set of clock triples, each of which is of the form (c, nil, 0). The operator =>* indicates there are zero or more rewritings from the given initial term to the expected term that can be matched by the target term.

In this example, the target term represents those configurations where the current step is 200. C is a configuration which is assigned by Maude. The result is obtained by repeatedly applying the rewrite rule. Maude only returns one result with the command. It means that there is only one possible 100-bounded schedule for the constraints. The schedule shows that c 1 and c 3 only tick at all odd steps except that c 3 does not tick at the first step, because of the constraint c 3 ≜ c 1 $ 1 . c 2 only ticks at all even steps. The returned bounded schedule coincides with the result in an earlier work of the second author [START_REF] Mallet | Correctness issues on MARTE/CCSL constraints[END_REF].

IX

Customized simulation

Given a set Φ of clock constraints, it is also desirable to have a customized schedule which satisfies not only Φ but also some customized requirements, e.g., at each step if a clock can tick it must tick, or if a clock does not have to tick, it must not tick. We only consider three basic scheduling policies, called randomness, maximum and minimum respectively.

-Randomness: If a clock can tick and not tick at next step, we randomly choose one. -Maximum: If a clock can tick at next step, it must tick.

-Minimum: If a clock has not to tick at next step, it must not tick.

Based on the four rewrite rules defined in Section 4, we can achieve customized scheduling for a given set of clock constraints using Maude's meta-level facility. We first find all the possible immediate successors of a set C of clock triples using Maude's metaSearch function, and then choose the successor that satisfies the customized policy given by users. The following rewrite rule is defined for customized scheduling.

1 --the rewrite rule is defined for customized scheduling In the rule, ρ is a variable, denoting the customized policy given by users, e.g. rand for randomness, max for maximum or min for minimum. The function sucs used in the condition returns the set of all the successors of C that satisfy Φ, and conf returns one among them according to the customized policy ρ. The equation above is used to define a recursive function sucsAux, which is the main auxiliary function to define sucs. Function sucsAux takes three arguments, C, Φ and a natural number j, which indicates that we want metaSearch to find the j th (j ≥ 0) successor of C. The metaSearch function takes a meta-module of the module ONE-STEP-TICKING where the four rewrite rules in Section 4 are defined, a term from which searching begins, a target term that the result term can match, and other three arguments, and returns a searching result. The searching result contains a meta-level term which substitute for C ′ . We change it to the object level by the built-in function downTerm. The object-level term represents the i th successor of C. We omit the detailed explanation about the usage of metaSearch. Interested readers can refer to the work [START_REF] Clavel | All about Maude[END_REF] for the details.

2 crl < C ; k ; Φ ; ρ > = > < C ′ ; k+1 ; Φ ; ρ > if C ′ := conf ( sucs (C , Φ) , ρ) .
Example 2. Let Φ 2 be the set of the following constraints:

in 1 ≼ step 1 step 1 ≺ step 3 in 2 ≼ step 2 step 2 ≺ step 3 step 3 ≼ out
We show the simulations of the bounded schedules that satisfy Φ 2 with maximum and minimum policy. We use Maude's rew command to rewrite the initial configuration < C 0 ; 0 ; Φ ; ρ > by applying the rewrite rule defined in this section 10 times with max and min respectively. The initial configuration is generated by function init1, which takes a set Φ of ccsl constraints and a simulation policy ρ as its arguments. The commands and returned results are shown as follow.

1 rew [START_REF] Leroux | Flat counter automata almost everywhere! In: 3rd International Symposium on Automated Technology for Verification and Analysis[END_REF] init1 (Φ2 , max ) .

i i i i i i i i ,0) ( ' in2 , t i t i t i t i t i ,5) 7 ( ' out , i i i i i i i i i i ,0) ( ' step1 , i i i i i i i i i i ,0) 8 ( ' step2 , i t i t i t i t i t ,5) ( ' step3 , i i i i i i i i i i ,0) ...
For the first schedule, the number of ticking clocks is always maximal, while for the second one the number of ticking clocks is always minimal.

Periodic scheduling

We also can find automatically periodic schedules of a given set of ccsl constraints by Maude's search command with the rewriting-based semantics of ccsl in Maude. The basic idea is to compute all possible immediate successors of the current k-bounded schedule at every step k(k ≥ 1) and check if there exists a successor that satisfies all the three conditions in Theorem 1. If such a successor exists, a periodic schedule is found, and the step k + 1 is the first step of the second iteration. We also can compute the period of the schedule. The following rewrite rule is defined for periodic scheduling.

1 --the rewrite rule is defined to represent periodic schedules

2 crl < C ; k ; Φ ; 0 > = > 3 if C ′′ == nil then < C ′ ; k + 1 ; Φ ; 0 > else < C ′′ ; k + 1 ; Φ ; p > fi 4 if (CS1 ,C ′ ,CS2 ) := sucs ( CF , CTS ) /\ <C ′′ ; p> := checkOcc ((CS1 , C ′ ,CS2 ) ,k + 1) .
The terms at left-hand side of the rule is a 4-tuple, where the last argument, i.e., 0 is indicates that the k-bounded schedule does not satisfy the three conditions in Theorem 1. Function checkOcc is used to check if there exists a k +1-bounded schedule that satisfies all the constraints in Φ and also the three conditions in Theorem 1. If that is the case, checkOcc returns the schedule C ′′ and the period p(p > 0), and otherwise nil and 0. Once a periodic schedule is found, the rewrite rule cannot be applied and Maude returns the result. Note that the rule may cause non-termination if no periodic schedule is found and no bound to the times of rewriting is set.

As an example, we use Maude's search command to find periodic schedules of the precedence constraint c 1 ≺ c 2 . The command is as follows:

1 search [4] init2 (c1 ≺ c2 ) = >* < C ; k ; c1 ≺ c2 ; p > such that p =/= 0 .
Function init2 takes a set Φ of ccsl constraints and returns an initial configuration < C 0 ; 0 ; Φ ; 0 >, where the last natural number is used to record the period of the current bounded schedule. We provide an upper bound e.g. 4 to the periodic schedules. In the command, C is a set of two clock triples of c 1 and c 2 returned by Maude when a periodic schedule is found. k indicates the step where the first period of the schedule ends, and p indicates the period of the schedule. The condition p =/= 0 means that C represents a periodic schedule. Table 1 shows four periodic schedules found by Maude for c 1 ≺ c 2 when the bound is set 4. The red steps for each schedule are the beginning of the first and second iteration of the period. We also can give p a concrete value and use Maude to search those periodic schedules with a fixed period.

Bounded model checking

Given a set of clock constraints, it is desired to know if the constraints satisfy some properties, e.g. if all the clocks can tick infinitely often, or a clock must tick immediately after another clock ticks. Based on the formal semantics of ccsl in Maude, we can model check LTL properties of a given set of ccsl constraints by Maude LTL model checker. Maude model checker requires the reachable state space being verified must be finite, while the reachable state space specified by the rewrite theory of a set of clock constraints may be infinite if there exists some non-periodic schedules. For periodic schedules, we force the schedule to repeat from step n to n ′ where n and n ′ are the beginning and ending steps of the first period. As depicting by Fig. 4, by setting a bound we can compute all periodic schedules up to the bound. The periodic schedules compose a finite state space which can be used for model checking. Figure 4 (left) shows an example of an unbounded state space. Each path represents a schedule. The path with a loop represents a periodic schedule. There are three periodic schedules in the figure when the bound is set 3. The three periodic schedules constitute a finite state space which can be model checked, as shown in Figure 4 (right). Next, we show some basic properties that clock constraints are expected to satisfy and their representations in LTL formula. Let tick be a parameterized predicate on states, which takes a clock c as argument and returns true if c ticks in a state and otherwise false. As an example, we model check if the constraints Φ 1 in Example 1 satisfy the alternating ticking property.

1 --definition of the state predicate tick in Maude 2 ceq <(C ; k; Φ; p> |= tick (c) = ( tval ( ,k) == t) if (c, ,n) := getConf (C , c) . 3 --the following command is used for model checking in Maude

4 red modelCheck ( init2 ((c1 ≺ c2 ) (c3 ≜ c1 $ 1 ) (c2 ≺ c3 ) ) , 5 []( tick (c1 ) -> O tick (c2 ) /\ tick (c2 ) -> O tick (c1 ) ) ) . 6 Result : true
The first equation is used to define the state predicate tick, and modelCheck is a built-in function to do model checking in Maude. It takes an initial state (configuration) and an LTL formula. Maude returns true with the above command, which means that the constraints Φ 1 indeed satisfies the alternating ticking property. This result coincides with the one obtained by encoding ccsl into finite-state transition system [START_REF] Mallet | Correctness issues on MARTE/CCSL constraints[END_REF].

By bounded model checking in Maude we also can find invalid schedules of a given set of clock constraints. A schedule is called invalid if it prevent some clock from ticking after some step, namely, it does not satisfy the repeated ticking property. A set Φ of ccsl constraints are called invalid if there exist invalid schedules that satisfy Φ. Once Maude finds such a periodic schedule that violates the repeated ticking property, we can conclude that the constraints A special invalid case of ccsl constraints is that some schedules may prevent all clocks from ticking after some step. We call them deadlock schedules. We can use Maude to find if there exist deadlock schedules within a given bound. Let us consider a case of Example 2. Assume that we introduce the following four new constraints to Φ 2 and denote the new set as Φ ′ 2 :

tmp 1 ≜ in 1 + in 2 tmp 1 ≺ out tmp 2 ≜ tmp 1 $ 1 out ≺ tmp 2
The four constraints mean that clocks tmp 1 and out must alternatively tick. We can find a number of schedules satisfying all the constraints in Φ ′ 2 . However, some of them may cause deadlock. We find 8 deadlock schedules by searching within 3 steps in Maude with the command:

1 search [10 ,3] init (Φ ′ 2 ) = >! CF .
In the command CF is a variable to which a 4-tuple is going to be assigned by Maude, and =>! means that the value assigned to CF must be rewritten by any rewrite rules. Namely, the value assigned to CF is a deadlock schedule. Table 1 shows the eight deadlock schedules. We take the first one as an example.

According to the first schedule, only three clocks, i.e. in 1 , step

Related Works and Discussion

ccsl mainly deals with logical clocks, i.e., unbounded increasing sequences of integers. The semantics of clock constraints may depend on boolean parameters, in which case, we remain in a finite world and can rely on traditional verification and analysis results and tools. The constraints may also depend on unbounded integer values, for instance, the number of times a given clock has ticked. In this latter case, the constraint is called unsafe [START_REF] Mallet | Safe CCSL specifications and marked graphs[END_REF]. A specification is safe if it does not use any unsafe constraint. The reference semantics of ccsl was given in a research report [START_REF] André | Syntax and semantics of the Clock Constraint Specification Language (CCSL)[END_REF] mainly to be able to define a simulation tool called TimeSquare [START_REF] Deantoni | Timesquare: Treat your models with logical time[END_REF]. TimeSquare encodes the operational semantics of ccsl in Java and captures boolean constraints symbolically using Binary Decision Diagrams (BDD). TimeSquare works step by step and at each step, finding a solution reduces to a satisfiability problem. After deciding if and how many valid solutions can be found at a step, TimeSquare clock engine picks one solution according to its simulation policy, updates the state space and moves forward. TimeSquare does not consider the unbounded specification as a whole and only produce one finite possible trace that satisfies all the constraints up to a given number of steps. In this work, we use bounded model-checking, we can then explore all the solutions reached in a given number of steps, instead of only one.

Other works have tried to make an exhaustive exploration of the entire state space (not up to a pre-defined number of steps). A comprehensive list of such works has been summarized in a recent survey [START_REF] Mallet | Correctness issues on MARTE/CCSL constraints[END_REF]. However, one aspect is to be able to decide whether the state space can be represented with a finite abstraction even though the specification is unsafe. Another way is to force a finite space space by restricting to safe constraints [START_REF] Yu | Polychronous controller synthesis from MARTE/CCSL timing specifications[END_REF][START_REF] Gascon | Logical time and temporal logics: Comparing UML MARTE/CCSL and PSL[END_REF][START_REF] Yin | Verification of MARTE/CCSL time requirements in Promela/SPIN[END_REF]. In this work, we do not make any assumptions on whether the specification is safe or not.

The most important achievement in this paper is that, thanks to Maude environment, all the analyses performed result directly from the operational semantics without intermediate transformations, so without the need to prove that the semantics is preserved. Yu et al. proposed to encode ccsl in Signal before transforming it to the internal format of Sigali [START_REF] Yu | Polychronous controller synthesis from MARTE/CCSL timing specifications[END_REF]. We hope that the encoding in Maude will allow to conduct automated verification for all the transformational approaches that use ccsl as a step. Maude also gives a framework to define the simulation policies formally. Some undocumented simulation policies are available in TimeSquare [START_REF] Deantoni | Timesquare: Treat your models with logical time[END_REF]. In Section 4, we give a simple formal interpretation for three of these simulation policies.

Finally, abstract interpretation [START_REF] Cousot | Abstract interpretation[END_REF] or infinite model-checking [START_REF] Leroux | Flat counter automata almost everywhere! In: 3rd International Symposium on Automated Technology for Verification and Analysis[END_REF] would allow reasoning on the global ccsl specification without restrictions. However, the encoding is likely to introduce semantic variations and we do not know at the moment how to encode ccsl constraints in a compositional way.

Conclusion and Future Work

We have proposed a new semantic model for ccsl constraints. We have also introduced the notion of bounded and periodic schedules. The satisfiability problem for ccsl specifications, which is still an open problem in the general case, is proved to be decidable with regards to bounded and periodic schedules even when using unsafe constraints. This is the first main result. The second result is to use the Maude encoding to perform bounded scheduling, customized simulation with different policies, periodic scheduling, and bounded model-checking.

The notion of periodic schedule seems promising but a bit constraining. In the future, we shall try to provide a more general definition where the behavior might slightly vary between successive periods while still maintaining decidability.

#$Fig. 1 .

 1 Fig. 1. Definition of 9 primitive ccsl operators

  we can use Maude's search command to find a 100-bounded schedule.

1

  search [2 ,100] init (Φ1 ) = >* < C ; 100 ; (Φ1 ) > . 2 states : 101 rewrites : 629424 3 C --> 4

3 6 ' 7 ' 8 (

 678 --the equation needs the meta-level function metaSearch to compute all successors 4 ceq sucsAux (C , Φ, j ) = downTerm (T , nil ) , sucsAux (C , Φ, j + 1) 5 if RT := metaSearch ( upModule ( ' ONE -STEP -TICKING , false ) , '( _ ; _ ;_ ') [ upTerm (C ) , ' nil . Conf , upTerm (Φ) ] , '( _ ; _ ;_ ') [ ' nil . Conf , C ′ , upTerm (Φ) ] , nil , '* , unbounded ,i) /\ C ′ <-T ) := g e tS ub s ti tu ti o n ( RT ) .

3 ⇒Fig. 4 .

 34 Fig. 4. Bounded state space of periodic schedulers

  Given a set Φ of clock constraints on clocks in C, and a function δ ∶ N ≤n → 2 C , δ is called an n-bounded schedule if for any i ≤ n, δ; i ⊧ Φ.

						p
	start	1	2	. . .	k	k + 1	. . .	k + p	k + p + 1	. . .
				Fig. 2. Periodic schedule
	2.2 Satisfiability problem of CCSL
	Given a set Φ of ccsl constraints, one of the most important problems is to
	decide if there exist some schedules that satisfy Φ. However, it is still an open
	problem whether the satisfiability of a given arbitrary set of ccsl constraints is
	decidable or not. We consider two kinds of schedules called bounded schedule and
	periodic schedule from the pragmatic point of view and show the satisfiability
	problem of an arbitrary given set of ccsl constraints with regards to bounded
	schedule and periodic schedule is decidable.
	Definition 3 (Bounded schedule). We denote the bounded satisfiability relation by δ ⊧ n Φ, which means that δ is
	an n-bounded schedule of Φ. It is obvious that given a bound n it is decidable to
	check if there exists an n-bounded schedule for a set of ccsl constraints because the number of candidate schedules is finite, i.e., (2 C -1) n , where C denotes
	the number of clocks in C. If there does not exist an n-bounded schedule for a
	set Φ of clock constraints, there must not be a schedule that satisfies Φ, although
	not vice versa.

Table 1 .

 1 Four periodic schedules that satisfy c1 ≺ c2

	schedule clock step	1	2	3	4	5	6	. . . period p
	1	c 1 c 2	t i	t t	t t	t t	t t	t t	. . . . . .	1
	2	c 1 c 2	t i	i t	t i	i t	t i	i t	. . . . . .	2
	3	c 1 c 2	t i	t i	t t	t t	t t	t t	. . . . . .	1
	4	c 1 c 2	t i	t i	t i	i t	t i	i t	. . . . . .	2

Table 2 .

 2 Eight deadlock schedules found by Maude for ccsl constraints Φ ′ are not valid. However, it cannot grantee the constraints are valid if no invalid schedules are found because not all schedules are model checked.

	XIII
	2

  1 and tmp 1 tick at the first step. In next step, no clocks can tick because of the newly introduced four constraints. For instance, in 2 cannot tick in next step. If in 2 ticked, so did tmp 1 (by constraint tmp 1 ≜ in 1 + in 2 ) and tmp 2 (by constraint tmp 2 ≜ tmp 1 $ 1 ), which violates the constraint out ≺ tmp 2 . Because in 2 cannot tick, step 2 can neither by constraint in 2 ≺ step 2 . Other clocks also cannot tick because of the corresponding constraints, leading to a deadlock.


Gabrielle Demange

Mutual rankings

Keywords: ranking, scores, two-sided, overlapping groups, mutual evaluation systems, bipartite graph. JEL D71, D85

est destinée au dépôt

Introduction

The enormous increase in interest in ranking methods based on data is clear in academic life, where students, researchers, universities are graded, or on Internet, where Web pages are ranked, movies and books are rated. Rankings may rely on a simple count, as the Science Citation Index, which adds up citations, or on more sophisticated computations, as in the recursive methods on which Google PageRank is based. A large number of situations involve two sides, each providing data on the other side. For example, buyers rate sellers and vice versa on eBay, or students evaluate their teachers and teachers grade them. The objective of this paper is to analyze some ranking methods in these two-sided settings through their axiomatization.

In a two-sided setting, there are two sets (the sides), M and N , and the members of one side provide evaluations on the other side's members. A ranking method assigns scores to the members of each side based on these mutual evaluations. The vector of scores on a side, say M , is called the ranking of M . The ranking is defined up to a multiplicative factor, meaning that it assigns relative strengths to the elements in M . 2 1 PSE-EHESS, address 48 bd Jourdan, 75014 Paris, France e-mail demange@pse.ens.fr. 2 The ranking thus not only orders the elements of M but also assigns (relative) values to them, as the 1 The ranking on one side naturally depends on the evaluations on its members, say the ranking on M depends on the evaluations provided by N . It may also depend on their own evaluations on N if these convey information on the relevance of the evaluations provided by N 's members. Consider students and teachers for example. The teachers' scores depend on the students' evaluations on them. One may also think that the evaluations provided by a highly-graded student are more relevant than those by a low-graded one. In that case, the teachers' scores should depend not only on how students evaluate them but also on how teachers grade the students. This introduces a feedback between the evaluations of each side. Whether this feedback is desirable is an important feature in the design of a ranking method.

I characterize a method, called mutual centrality method, that takes this feedback into account. The method relies on the dominant eigenvector of the square matrix that stacks the evaluations. The characterization involves two axioms. The first one, called additivity under unanimity, pertains to the situation where all members of one side are unanimous on their evaluations on the other side. The second one, called consistency across sides, requires that replacing the evaluations on the agents of one side by their assigned scores does not affect the rankings. The two axioms are shown to be independent.

In some contexts, one may want the rankings to be insensitive to the total of the evaluations provided by each agent, a property called intensity-invariance. Considering the students-teachers example, a teacher may be much more indulgent than another one. To avoid the degree of indulgence to influence the rankings of the students or of the teachers, a solution is to scale the grades of each teacher so that they sum (say) to one before computing the method. This results in an intensity-invariant 'version' of the mutual centrality method. The resulting method is characterized by intensity-invariance together with the two previous axioms properly restricted to scaled evaluations.

The feedback between the two sides' evaluations may be thought as non desirable in some situations. A method that excludes this feedback is said to be impartial across sides. The axiom requires the ranking on the members of one side to be independent of the evaluations they provide on the other side, say the ranking of the students does not depend on how they evaluate the teachers. Impartiality can be justified by strategic issues: if i's evaluations on the other side do not impact i's score, then i has no incentive to lie. 3 Impartial methods decompose into two methods, each one specifying the ranking on one side as a function impact factors or PageRank. The term 'ranking' might not be appropriate though this is a rather standard terminology.

3 Though, this does not count for reputation effects. On eBay for example, there is evidence that buyers refrain from posting bad ratings in fear of retaliation.

of the sole evaluations provided by the other side on them. The counting method, which assigns scores equal to the totals of the received evaluations, is a prominent impartial method. I characterize it through two axioms, uniformity and homogeneity, in addition to impartiality. Another impartial method, called congruence method, accounts not only on the received evaluations' totals but also on the joint pattern of these evaluations. The method reflects the idea that a concentration of good evaluations by a group of evaluators is a good signal, hence reinforce each other. The ranking on one side is defined by a dominant eigenvector of the evaluation matrix multiplied by its transpose. The congruence ranking can be shown to minimize the distance in the joint evaluations between the observed matrix and that associated to a unanimous ranking.

This paper is related to recent studies that have characterized ranking methods based on evaluations or citations. These studies consider one-sided or peers' settings. In a one-sided setting, a set of 'experts' provide evaluations on the items to be ranked. The peers' setting obtains when the experts coincide with the items, that is, when everybody evaluates every other agent as, for example, journals citing each other or Web pages linking toward other pages.

In the peers' setting, the eigenvalue centrality method defines the ranking to be the dom- Several axioms used in this paper appeared in the literature in various forms and contexts. The consistency 'principle' underlies studies in fair division, bankruptcy problems [START_REF] Young | On dividing an amount according to individual claims or liabilities[END_REF], apportionment problems [START_REF] Balinski | An Axiomatic Approach to Proportionality between Matrices[END_REF] where it is called uniformity) or cooperative games [START_REF] Hart | Potential, value, and consistency[END_REF] for example. As explained in [START_REF] Thomson | The consistency principle[END_REF], the principle requires that changing part of the data of a problem by the solution a method gives to them does not lead to a contradiction, i.e., does not lead to reassess the solution for the others. Consistency across sides requires the principle to apply when the data on a side is changed by its solution. Uniformity and homogeneity are used to characterize the counting method in the one-sided setting [START_REF] Demange | A ranking method based on handicaps[END_REF], and here in the two-sided setting under impartiality across sides. The intensity-invariance property is widely used in peers' settings. In the context of ranking Websites for example, in which the numbers of links from various sites vary widely, PageRank deflates a link from a site by the total number of links from that site, thereby preventing sites to increase their score by inflating the number of links to sites that point to them. In the context of economic journals, in which citations intensities substantially differ across fields, Palacios-Huerta and [START_REF] Palacios-Huerta | The Measurement of Intellectual Influence[END_REF] show that factoring out intensity has a non-negligible impact on the ranking.

inant
In the one-sided setting, the handicap-based method is shown to be the counterpart of the counting method when intensity-invariance is required or when evaluations represent shares (Demange 2014). Finally, Clippel, Moulin, and[START_REF] De Clippel | Impartial division of a dollar[END_REF] introduce the impartial property in the context of 'division of a dollar', in which everybody recommends the (relative) share that every other agent should receive (thus a peers' setting). Impartiality requires that the share of any agent is determined exclusively by the reports of other agents.

The property is extended to a two-sided setting by requiring that the score of any agent is determined exclusively by the evaluations provided by the other side.

The paper is also related to the studies on affiliation networks, sometimes referred to as two-modes networks, conducted in sociology (see e.g. [START_REF] Borgatti | Network analysis of 2-mode data[END_REF] and [START_REF] Faust | Centrality in affiliation networks[END_REF] for discussions on these networks). An affiliation network describes the membership of individuals to groups, clubs, or boards. Analyzing the network may help to uncover underlying friendship or power relationships from the pattern of common membership (overlap between two individuals' participation) and common attendance (overlap between two groups). For example, studies on 'interlocking directorates' consider the participation of business leaders to the boards of different companies, aiming at detecting possible alliance strategies from the overlap of the boards, starting with [START_REF] Mintz | Interlocking directorates and interest group formation[END_REF].

An affiliation network is represented by a bipartite graph in which one side is composed of the individuals, the other side is composed of the groups and an edge connects an individual i and a group λ in this graph if i is a member of λ. [START_REF] Bonacich | Technique for analyzing overlapping memberships[END_REF][START_REF] Bonacich | Simultaneous group and individual centralities[END_REF] proposes to simultaneously assign group and individual centralities to the adjacency matrix associated to the bipartite graph. This matrix is symmetric and has elements either equal to 1 to represent membership of i to λ or 0 otherwise. This paper extends this approach to more general weighted and possibly directed relations between two sides by defining and characterizing the mutual centrality method. [START_REF] Salonen | Equilibria and centrality in link formation games[END_REF] and ( 2016) also proposes to extend Bonacich approach and relates the ranking to the equilibria in a noncooperative games or to minimum norm solutions.4

The paper is organized as follows. Section 2 presents the framework, Section 3 introduces and characterizes the mutual centrality method and its intensity-invariant version. It also introduces the 'competitive' counting method and shows the independence of the used axioms. Section 4 defines impartial methods and characterizes the counting and congruence methods.

2 Ranking methods in two-sided settings The data of a problem is thus summarized by the pair of evaluation matrices (u, v). The pair satisfies the constraints associated with the setting. The first example in Section 2.2 considers affiliation networks, in which v is the transpose of u, denoted by u, whereas in the second and third examples, v is not a priori related to u so that any non-negative pair (u, v) is feasible. Let F denote the feasible set.

Given evaluations (u, v) in F, one seeks to evaluate the members of M and N by assigning them non-negative scores. Let r i denote i's score and s λ denote λ's score. The scores provide the relative strength of the members within each side, M or N . This reflects two properties. First, the members of M and N are not comparable between each other, so comparing their scores, i.e., the r i with the s λ , has no meaning. Second, within a side, not only the order of the scores matters but also their values, up to a multiplicative constant.

Therefore, calling r = (r i ) the ranking on M , all the vectors proportional to r, r = kr for k > 0, written as r ∝ r, provide the same ranking on M . It is often convenient to choose the (unique) unit vector whose components sum to one. Similarly s = (s λ ) is a ranking on N and all s ∝ s provide the same ranking. A ranking method assigns a ranking on each side to each feasible problem (u, v). Formally, Definition 1 Given M , N and the set F of feasible pairs of evaluation matrices, a ranking method F assigns to each feasible pair (u, v) a ranking r = F M (u, v) on M and a ranking

s = F N (u, v) on N .
As an example, the counting method assigns scores proportional to the received evaluations' totals. Given a matrix u, u i+ denotes the total in row i, u λ+ = λ∈M u iλ . (Similar notation is used for any matrix). The counting rankings are

r ∝ ( λ∈N u iλ ) i∈M and s ∝ ( i∈M v λi ) λ∈N . (1)
Other methods are introduced in the next sections.

Finally, it is sometimes convenient to view a problem (u, v) as a weighted, possibly directed, bipartite graph. Recall that a bipartite graph is a graph whose vertices can be divided into two disjoint sets M and N such that every edge connects a vertex in M to one in N or a vertex in N to one in M . Define the bipartite graph with edge (λ, i) if u iλ > 0 and weight u iλ and edge (i, λ) if v λi > 0 and weight v λi ; when v is equal to u, the transpose of u, the graph is 'undirected'. Conversely any weighted directed bipartite graph is associated to a problem.

Examples

Let us illustrate the setting with three examples.

1. Affiliation networks. These networks represent the participation of individuals to events or their affiliations to clubs. M describes the set of individuals and N the set of events or clubs. For example, the studies on interlocking directorates referred to in the introduction consider the participation of business leaders to the boards of different companies, in which M is the set of business leaders and N is the set of boards of various companies.

An affiliation network is represented by an undirected bipartite graph. The evaluations u and v are defined by setting u λi and v iλ both equal to 1 if i is a member of λ and both to 0 otherwise. These evaluations reflect the fact that the affiliation of i to λ represents a mutual agreement: to be affiliated with λ, i must be accepted by λ and be willing to be a member of λ. More generally, allowing for a 'weighted' intensity for the affiliation between i and λ, v λi = u iλ any nonnegative number, an affiliation network has symmetric or dual evaluations: v is equal to the transpose u of u.

2. Mutual applications. Consider the situation in which the members on one side express their preferences on the other side before an assignment. In the academic world for example, the students are asked to weigh the universities and each university provides grades on the students. The evaluations here are respectively the students weights and the universities grades. The students' evaluations are likely to differ because their distance to universities or their preferred specializations differ. Similarly, the universities' evaluations are likely to differ: even if universities have access to the same information on the students, say the results of a general final exam, they may weigh differently the fields. Moreover the evaluations are likely not to be dual.

Consider for example the case where the evaluations are 1 or 0, where a student's evaluation is 1 on a university to which she applies and a university's evaluation is 1 on a student it finds acceptable. A student who applies to a university may not be found acceptable by it and a student who is acceptable to a university may not apply to it: v typically differs from u. Here, a student's score is meant to capture how much she is demanded relative to other students, and similarly for universities.5

3. Mutual recommendations/grades. Recommendations on exchanges are more and more widespread. For example, buyers and sellers rate their transactions on eBay. In what follows, it is assumed that there is a recommendation of each i on each λ and vice versa. In practice, this assumption is not necessarily met at the unit level. One can assign the average of the recommendations or use techniques to group similar users and fill the missing data, as used by Netflix recommendation system. The mutual evaluations of students and teachers fit this example as well. This case illustrates why one may want to consider intensity-invariant methods (see Section 3.2). A teacher may be severe while another one is indulgent, meaning that the average of the former is much lower than the average of the latter. An intensity-invariant method 'normalizes' the evaluations, hence is insensitive to the degree of indulgence.

Mutual centrality

This section introduces and characterizes the mutual centrality method through two axioms. It also introduces the 'competitive' counting method and shows that the axioms are independent. Finally, Section 3.2 defines and characterizes an intensity-invariant version of the mutual centrality method.

Defining and characterizing the mutual centrality method

In a peers' setting, eigenvector centrality considers that a node is important if it is pointed to by other important nodes. This produces the ranking given by the dominant eigenvector of the evaluation matrix. In the two-sided setting, mutual centrality applies a similar principle.

Though, as the sides are not comparable, i.e., as each ranking on M and N is defined up to a scalar, eigenvector centrality has to be adapted.

Let us first consider the square (m + n) × (m + n) matrix gathering the evaluations:

π = 0 u v 0
. Assume π irreducible (the condition is interpreted below). Due to Perron-Frobenius theorem, π has a positive eigenvector, unique up to a scalar, associated to its largest eigenvalue, which is positive. Such an eigenvector is called dominant. Denoting by ρ the largest eigenvalue of π, a dominant eigenvector (r, s) satisfies

r i = 1 ρ λ∈N u iλ s λ for each i ∈ M and s λ = 1 ρ i∈M v λi r i for each λ ∈ N. (2)
The scores given by r and s exhibit a mutually reinforcing relationship. Considering mutual recommendations between sellers and buyers for example, these scores say that a 'good' buyer -one with a high score-is one who is highly evaluated by many good sellers and a good seller is one who is highly evaluated by many good buyers. (This type of justification appears in affiliation networks, as described at the end of this section.)

As the rankings on M and N are each defined up to a scalar, mutual centrality assigns to M the rankings proportional to r and to N those proportional to s. To define and interpret the method, the next Lemma is useful. Let I denote the set of evaluations (u, v) such that π is irreducible. As shown below, the irreducibility of π is equivalent to that of both uv and vu.

Lemma 1 Given (u, v) in I the following properties on positive vectors r and s are equivalent:

(i) r and s are respectively dominant eigenvectors of uv and vu (ii) r is a dominant eigenvector of uv and s ∝ vr (iii) There is positive k for which (r, ks) is a dominant eigenvector of π.

Furthermore the dominant eigenvalues of uv and vu are identical, equal to ρ 2 .

Proof In what follows let us denote by σ the dominant eigenvalue of uv.

(i) is equivalent to (ii). Take r a positive dominant eigenvector of uv: uvr = σr.

Multiplying by v, we obtain vuvr = σvr. Thus vr is a positive eigenvector of vu associated to σ. This implies that σ is the dominant eigenvalue of vu and, by irreducibility of vu, that the dominant eigenvectors of vu are all proportional to vr. This proves the equivalence between (i) and (ii).

(iii) implies (i). Assume (iii). Take (r, ks) a dominant eigenvector of π. This writes: The mutual ranking on M thus satisfies

r i = 1 ρ 2 j∈M (uv) ij r j for each i ∈ M. (3)
The matrix uv reflects some form of competition between the agents in M , as will be studied below. I provide now an axiomatization of the mutual centrality method.

Additivity under unanimity. The members of M are said to be unanimous when their evaluations on N are equal: v λi = y λ for each i and each λ. The matrix v takes the form dg(y)1 1 n,m where dg(y) is the n×n diagonal matrix with the vector y = (y λ ) on the diagonal and 1 1 n,m is the n × m matrix made of 1. Unanimity of N is defined similarly.

Definition 3 The method F is additive under unanimity on F if for all problems (u, v)

for which M is unanimous, v = dg(y)1 1 n,m for some y, then r ∝ ( λ u iλ y λ ) i∈M and s ∝ y (4)
and for all problems (u, v) for which N is unanimous, u = dg(x)1 1 m,n for some x, then r ∝ x and s ∝ (

i v λi x i ) λ∈N (5)
To illustrate the property, consider the example of ratings between buyers and sellers.

Assume that buyers all rate identically each seller. According to (4), the sellers' scores coincide with these common ratings and a buyer's score is obtained as the weighted sum of the ratings that sellers assign to her, where a seller's weight is his score. Additivity under unanimity encompasses two notions. First, the evaluations of one side on the other, say of M on N , are relevant to judge the evaluations provided by N on M . Second, the (unanimous) evaluation obtained by a member of N acts as a 'price' on his own evaluations on M . If the rating of seller λ is twice that of µ, λ's evaluations on the buyers are doubled relative to those of µ.

Consistency across sides. Consistency across sides applies the 'consistency principle'

(see the introduction) to be satisfied when the data on one side is changed by its solution.

Specifically, replacing the evaluations on the members of one side by their assigned scores does not affect the rankings.

Definition 4 The method F is consistent across sides on F if, letting (r, s) = F (u, v):

F (u, v) = F (u, dg(s)1 1 n,m ) and F (u, v) = F (dg(r)1 1 m,n , v).
To understand the first equation, let us replace the evaluations by each member of M by the assigned ranking s on N : the matrix v is replaced by dg(s)1 1 n,m . The first equation thus says that the rankings are not affected by this change. Similarly for the second equation when u is replaced by the unanimous ranking r.

Proposition 1 The mutual centrality method is the only ranking method on I that is additive under unanimity and consistent across sides.

Proof The mutual centrality method is additive under unanimity. Assume the members of M all provide the same evaluation y on N . The equation on the right hand side in (2)

writes s λ = 1 ρ i∈M y λ r i for each λ in N hence s is proportional to y. Plugging these values into the equation on the left hand side of (2) yields that r is proportional to ( λ u iλ y λ ) i∈M : this proves additivity under unanimity. Consistency across sides straightforwardly follows from (2).

Conversely, let F satisfy the axioms. Let (r, s) = F (u, v). By consistency across sides,

r ∝ F M (u, dg(s)1 1 n,m ). By additivity under unanimity, F M (u, dg(s)1 1 n,m ) ∝ ( λ u iλ s λ ) i∈M .
Hence there is k > 0 such that r i = α λ u iλ s λ for each i. Exchanging the roles of M and N , there is β > 0 such that s λ = β i v λi r i for each λ. Combining these relations, we obtain that r and s are respectively dominant eigenvectors of uv and vu: this proves that F is the mutual centrality method .

Next, let us study the matrix uv and introduce the competitive counting method. This method will be useful to show the independence between the two axioms.

The competitive counting method The matrix uv reflects some form of competition between the agents in M . (uv) ij is equal to λ u iλ v λj . In the example of mutual applications with 0-1 values, it is equal to the number of universities to which j applies that find i acceptable. Thus, (uv) ij reflects the competition posed by i on j for i = j, and (uv) ii reflects the adequacy in the demand and acceptance of i. More generally, (uv) ij is high when the members in N who are highly valued by j highly value i. Let us call uv the competitive matrix for M and similarly vu the competitive matrix for N .

The competitive counting method assigns to each side the counting scores computed on its competitive matrix, i.e., the counting scores of uv to M and those of vu to N .

Rearranging the sums:

r ∝ ( λ u iλ v λ+ ) i∈M and s ∝ ( i v λi u i+ ) λ∈N . ( 6
)
The scores of agents in M are thus given by the sums of the received evaluations weighted by the evaluators' counting score, and similarly for the scores of N .

The three methods introduced so far, the counting, competitive counting and mutual centrality ones, generally produce different results. Consider the example

u α β a 0 k b 2 1 v a b α 1 0 β 0 2 uv a b a 0 2k b 2 2 vu α β α 0 k β 4 2
where k is a positive parameter. k has a positive impact on the competitiveness of a over b and α over β. The competitiveness of a over b is equal to 2k due to the fact that a is valued k by β who is valued 2 by b. The competitiveness of α over β is equal to k due to the fact α is valued 1 by a who is valued k by β.

On M , the counting scores are proportional to (k/3, 1), the competitive counting ones to (k/2, 1) and the mutual centrality ones to ( k + 1 4 -1 2 , 1). They differ for generic k. a's competitive counting score is always larger than his counting score: since β's counting score is twice that of α, the competitive counting method, according to (6), values more the evaluations from β than the counting one. The result follows because a is valued by β only whereas b is more valued by α than β.

Comparing a's competitive counting and mutual centrality scores, the former is smaller for k < 2. It can be understood by considering (2) and the double effect of k: k increases a's grade but a is valued only by β whose score decreases with k: we have ra r b = k s β sα+s β ; since the competitiveness of β relative to α decreases with k, β's score decreases relative to α's one, as can be checked by computing the mutual centrality scores on N : ( 1 2 ( k + 1 4 -1 2 ), 1). The relationships between the three rankings are better understood by considering a recursive approach to the mutual centrality scores. 6 The competitive counting method can be seen as intermediate between the counting and mutual centrality methods. Let us start with the counting scores. The idea is to recompute the scores by weighting each evaluation by the evaluators' scores. This provides new scores. Iterating, the algorithm can be shown to converge to a dominant eigenvector of the matrix π, under the additional assumption of ergodicity.Formally, start with the counting rankings r 1 and s 1 . The recursive equations at t + 1 are

r t+1 ∝ ( λ u iλ s t λ ) i∈M and s t+1 ∝ ( i v λi r t i ) λ∈N (7)
that is, at step t + 1, the scores in M are proportional to the sum of the received evaluations weighted by the evaluators' scores at t, i.e. λ's evaluations are weighted by s t λ , and similarly the scores in N are proportional to the sum of the received evaluations weighted by the evaluators' scores at t, i.e. i's evaluations are weighted by r t i . Assume the matrix π to be ergodic, i.e., a power of π has all its elements positive.

Then, choosing unit vectors, the sequence (r t , s t ) converges to an eigenvector of π. Along the algorithm, the rankings are the counting one at step 1, the competitive counting one at step 2 as follows from (7), and the mutual centrality one asymptotically.

Independence between additivity under unanimity and consistency across sides

We show that the two axioms are independent. Clearly, the counting method is consistent across sides but is not additive under unanimity.

Let us show that the competitive counting method is additive under unanimity but not consistent across sides. Additivity under unanimity straightforwardly follows 7 from (6). The method is not consistent across sides: Replace the evaluations v by unanimous evaluations equal to the competitive counting score s of N . Thanks to additivity under unanimity, the scores of M become proportional to the sums of the received evaluations weighted by s, which differ in general from the sums weighted by N 's counting scores. This is illustrated by the previous example. Let us replace the evaluations v on N by unanimous ones equal to (k, 6) the competitive counting scores on N . By additivity under unanimity, the competitive counting scores in M become proportional to (3k, k + 3) (obtained as (0 × 1 + k × 6, 2 × k + 1 × 6)). These are not proportional to the competitive counting scores of N , (k, 2), for k different from 3: the method is not consistent.

Irreducibility The irreducibility of the competitive matrices uv and vu can be interpreted as saying that any two agents in the same side are in competition, directly or indirectly. Consider for example uv. uv is irreducible if for each pair (i, j) there is an integer p for which uv (p) (i, j) > 0. If p = 1, j poses competition on j as we have seen. For p > 1, uv (p) (i, j) > 0 means that there is a succession of p individuals in N starting from i and ending to j such that each one poses competition on the follower. Alternatively, in the underlying directed bipartite graph, there is a (directed) path linking any two agents in M .

The irreducibility of π is equivalent to that of both uv and vu. Since π is irreducible if there is a (directed) path linking any two agents in M ∪ N , it straightforwardly implies the irreducibility of both uv and vu. Conversely, when both uv and vu are irreducible, no row nor column of π can be null, so that any path from an i to a λ can be obtained through a j connected to λ: π is irreducible.

Affiliation networks Recall that an affiliation network represents the affiliation of individuals to groups (see Section 2.2). [START_REF] Bonacich | Technique for analyzing overlapping memberships[END_REF] proposes to simultaneously assign individual and group centralities in an affiliation network by considering the scores that satisfy for some α

r i = α λ/i is in board λ s λ for each i and s λ = α i/ is in board λ r i for each λ (8)
These equations correspond to (2) where u λi and v iλ are both equal to 1 if i is a member of board λ and both to 0 otherwise. The mutual centrality method thus extends this idea to any two-sided problem. Quoting [START_REF] Bonacich | Simultaneous group and individual centralities[END_REF] in the context of the membership to boards, (8) says that A central firm gets its central position from the board membership patterns of its members. They belong to the variety of boards that make that firm central.

If its members belong to a constricted set of other boards, that firm would not be central.

Dually a central individual should be one who belongs to a variety of important firms. One kind of centrality cannot be defined without reference to the other.

In the Web context, [START_REF] Kleinberg | Authoritative sources in a hyperlinked environment[END_REF] uses a similar idea to define the Hits method, based on good 'hubs and authorities'. 8 The method distinguishes two weights for each Web page, one associated with the relevance or authority of a page, which should help users to find the relevant pages, the other with the adequacy of a page to point toward the relevant pages, which identifies the good hubs (not necessarily useful to Internet users). Specifically, the method assigns the (authorities) ranking r = (r i ) and the (hubs) ranking s = (s i ) that satisfy r i = j/j points to i s j for each i and s j = σ i/i points to j r i for each j (9)

for some positive σ. Quoting Kleinberg Hubs and authorities exhibit what could be called a mutually reinforcing relationship: a good hub is a page that points to many good authorities; a good authority is a page that is pointed to by many good hubs.

Comparing ( 9) with (2), the Hits method coincides with the mutual centrality method applied to the bipartite graph in which each side coincides with the set of Websites, and the evaluations are dual, given by u ij = v ji equal to 1 if j points to i or to 0 otherwise, i.e.

this corresponds to an affiliation network.

Proposition 1 does not characterize the mutual centrality method on the set of affiliation networks because the axioms pertain to changes in the evaluations of one side that leave unchanged those of the other side. Applying such a change to an affiliation network, the obtained evaluations are no longer the transpose of each other, hence do not represent an affiliation network.

The invariant mutual centrality method

In some contexts, as explained in the introduction, one may want the rankings to be insensitive to the total of the evaluations provided by each agent, a property called intensityinvariance. In the example of students-teachers, this means that the degree of indulgence or severity of a teacher should not influence the rankings of the students or of the teachers.

Formally, u is a scaled version of u if the columns of u and u are proportional: for each λ in N , λ's evaluations in u and u are proportional, i.e., there is a positive number k λ such that u iλ = k λ u iλ for each i. A scaled version v of v is defined similarly by requiring i's evaluations in v and v to be proportional for each i in M . The axiom of intensity-invariance is defined on any feasible set F that is closed by scaling the evaluations, i.e., starting with 8 Relationships between the invariant and Hits methods are analyzed in [START_REF] Kitti | Axioms for centrality scoring with principal eigenvectors[END_REF].

(u, v) in F, (u , v ) belongs to F for any scaled versions u of u and v of v. Call such a set scaled-invariant.

Definition 5 A method F defined on the scaled-invariant F is intensity-invariant if

F (u, v) = F (u , v
) for any (u, v) in F and for any scaled versions u of u and v of v.

Basically, an intensity-invariant method is characterized by its values on the evaluations that are each normalized say to sum to 1. Denote by [F] the set of irreducible matrices π whose columns sum to 1. Given F , one builds an intensity-invariant method by scaling the evaluations of each agent before applying F . Formally let [π] be the matrix whose columns are proportional to those of π and sum to 1. Define [F ] by: for each π, [F ](π) = F ([π]).

[F ] is intensity-invariant and coincides with F on [F].

The invariant mutual centrality method is defined to be [F ] where F is the mutual centrality method. The dominant eigenvalue of [π] (as well as that of [u][v] and [v][u]) is equal to 1. Thus, applying (2), the unit rankings (r, s)

= [F ](u, v) satisfy r = ( λ∈N [u iλ ]s λ ) i∈M and s = ( i∈M [v λi ]r i ) λ∈N . (10)
The invariant mutual centrality method is characterized in a similar way as the mutual centrality one, by restricting the two axioms on [I] and adding intensity-invariance. This is stated in the following corollary to Proposition 1.

Corollary 1 The invariant mutual centrality method is the only ranking method on I that is intensity-invariant on I, additive under unanimity and consistent across sides on The same approach straightforwardly applies to define methods that are intensityinvariant on one side only. Normalizing the evaluations of one side only, say M , the obtained each row-balanced u in P M . F M is exact if F M (u) = 1 1 M implies that u is row-balanced.

Uniformity and exactness of F N are defined similarly.

The next property is called homogeneity. The property is very natural when evaluations are cardinal.9 Let us start with evaluations on M and multiply each evaluation on i by the same scalar ρ i . Homogeneity requires i's score to be multiplied by the same factor relative to other scores. Formally, starting with u in P M , multiplying each evaluation on i by ρ i multiplies row i by ρ i ; the modified evaluation matrix writes dg(ρ)u where ρ is the vector with i's component equal to ρ i and all others equal to 1. Homogeneity requires F M (dg(ρ)u)

to be (proportional to) the ranking dg(ρ)F M (u). The property is required for each row i, so iteration yields the following equivalent definition.

Definition 8 A method F M is homogeneous on M if for each u in P M and each positive m-vector ρ = (ρ i ), F M (dg(ρ)u) is the ranking dg(ρ)F M (u). Homogeneity of F N is defined similarly.

The following proposition follows straightforwardly from the impartiality axiom and Proposition 3 in [START_REF] Demange | A ranking method based on handicaps[END_REF].

Proposition 2 The counting method is the only method that is impartial, homogeneous and uniform on N and M . The counting method is the only method that is impartial, homogeneous and exact on N and M .

The congruence method The congruence method assigns to (u, v) the rankings r and s respectively dominant eigenvectors of u u and v v, assuming these matrices irreducible.

The word congruence refers to the fact that the method departs from the counting method by considering how evaluations jointly depart from the counting scores, as explained below.

Under unanimous evaluations r, the term (u u) ij is equal to nr i r j . The following proposition states that the method seeks for the unanimous ranking r that minimizes some errors between the unanimous evaluation matrix rr and u u, and similarly for s. The proof extends the argument used in [START_REF] Bonacich | Technique for analyzing overlapping memberships[END_REF] for affiliation networks to the general two-sided setting. The argument bears on the eigenvectors of a symmetric matrix, as is applied in principal components analysis though on centered variables.

Let V be the set of matrices (u, v) such that both u u and v v are irreducible.

  eigenvector of the matrix of evaluations. Several axiomatizations of eigencentrality have been provided (Palacios-Huerta and Volij 2004, Slutzki and Volij 2006 for its intensityinvariant version, Altman and Tennenholtz 2005 for its ordinal version, and Kitti 2016).The mutual centrality method is related to eigenvalue centrality since it is built on the dominant eigenvector of a matrix (it does not coincide with it due to the independence of the rankings between the two sides). The two-sided setting allows for a different characterization.

2. 1

 1 The frameworkIn a two-sided setting, two distinct sets of entities (or 'sides'), denoted by M and N , interact and provide data on each other, called evaluations. An entity may represent an individual, a firm, a school or group, and an evaluation can be interpreted in different ways depending on the context as, say, an application, a recommendation, a grade, or an affiliation, as illustrated in the examples in Section 2.2.In the following, the members of M and N are called agents, keeping in mind the different interpretations. Members of M are indexed by roman letters, generic i, and those of N by greek ones, generic λ. Let m denote the cardinality of M and n the cardinality of N . Each member of one side provides evaluations on each member of the opposite side. For example each i in M provides evaluation v λi on each λ in N . All the evaluations by M are represented by the n × m matrix v = (v λi ), in which i's column represents i's evaluations on the members of N . Row λ thus represents all the evaluations on λ. Similarly, the evaluations by the members of N on those of M are described by the m × n matrix u = (u iλ ), in which λ's column represents λ's evaluations on the members of M .

  kus = ρr and vr = kρs. Multiply the second equation by u: uvr = kρus; using the first equation, we obtain uvr = ρ 2 r. Hence r is a dominant eigenvector of uv (since r is a positive vector) and ρ 2 is its dominant eigenvalue. Similarly, multiplying the first equation kus = ρr by v yields kvus = ρvr = kρ 2 s. Hence s is a dominant eigenvector of vu and ρ 2 its dominant eigenvalue. This proves (i) and σ = ρ 2 . (i) implies (iii). Take r a dominant eigenvector of uv and set s = 1 √ σ vr. We have us = 1 √ σ uvr; since uvr = σr, we obtain us = √ σr. Thus both equations us = √ σr and vr = √ σs hold: this proves that (r, s ) is a dominant eigenvector of π, that is (iii), and √ σ is the dominant eigenvalue of π. Definition 2 The mutual centrality method assigns to each (u, v) in I the rankings r and s given respectively by the dominant eigenvectors of uv and vu, or satisfying the equivalent conditions (ii) or (iii) in Lemma 1.

  [I].Proof Let F be the mutual centrality method. By construction[F ] is invariant. To show additivity under unanimity on [I], let u be in [I], u = [u], and M be unanimous on N with unit evaluations y. We have[F ](u, v) = F (u, dg(y)1 1 n,m ). Since F is additive under unanimity, it follows that [F ] M (u, v) is proportional to ( λ u iλ y λ ) i∈M and [F ] N (u, v) to y; this proves that [F ] isadditive under unanimity on [I]. Similarly [F ] is consistent across sides on [I] (and even on I) because F is. To show the converse, let G be intensity-invariant on I, additive under unanimity and consistent across sides on [I]. Since G is intensity-invariant, (r, s) = G([u], [v]) for any (u, v). Using additivity under unanimity and consistency across sides on [I], the proof of Proposition 1 applies to the pair ([u], [v]). This proves that r and s are respectively dominant eigenvectors of [u][v] and [v][u], i.e., G = [F ].

I thank a referee to point out these works to me.

Note that the problem of determining the scores differs from that of the final assignment of students to universities.

This approach has been used by various authors in the peers' setting.[START_REF] Liebowitz | Assessing the Relative Impacts of Economics Journals[END_REF] use the first steps of the algorithm to rank economic journals.

If M 's members unanimously evaluate N by y, then i v λ,i ui+ = y λ i ui+, hence s ∝ y. Furthermore, since v λ+ = my λ , r ∝ ( λ u iλ y λ )i∈M by (6).

The homogeneity axiom introduced in Palacios-Huerta and Volij (2004) differs since it bears on a given matrix that has two proportional rows.

method is intensity-invariant over M . A similar characterization as in Corollary 1 is obtained, requiring intensity-invariance on M , additivity under unanimity and consistency across sides for all irreducible matrices u and all the normalized ones v.

Impartial methods

The property of impartiality across sides requires that the score of any agent is determined exclusively by the evaluations of the agents of the other side: The ranking on M only depends on u and that on N only on v. Formally

Impartiality across sides implies consistency across sides; actually it is a much stronger axiom. Impartiality is incompatible with additivity under unanimity because the latter precisely requires the ranking on M to vary with their evaluations on N when these are unanimous: For a fixed u, r varies with y as can be seen from ( 4). There are many impartial methods, each one obtained by choosing a ranking method. An impartial method is thus characterized by characterizing each one-sided method, F M and F N . In what follows, I consider methods F M that are defined on the set P M of non-negative m × n evaluation matrices u and similarly for F N .

The counting method defined by (1) is a benchmark. It has been characterized in various settings. The ordinal ranking associated to the counting method has been axiomatized by [START_REF] Rubinstein | Ranking the Participants in a Tournament[END_REF] for tournaments, in which i wins over j or j wins over i, and by [START_REF] Van Den Brink | The outflow ranking method for weighted directed graphs[END_REF] for weighted directed graphs. I use here the characterization in [START_REF] Demange | A ranking method based on handicaps[END_REF], which applies to our framework in which the (relative) values taken by the scores, and not only the order, matter. The characterization relies on two properties, either uniformity and homogeneity, or exactness and homogeneity.

Uniformity and exactness bear on some specific evaluations, hereafter called row-balanced.

A matrix is said to be row-balanced if each row receives the same total. Equivalently, rows obtain equal scores under the counting method. Uniformity views row-balanced matrices as 'neutral': there is no rationale for distinguishing between the agents on one side if they are assigned identical totals by the other side. Exactness asks the converse property that agents obtain equal scores only if they receive identical totals. Formally let P M be the set of evaluation on M , i.e. the set of m × n non-negative matrices.

Definition 7 Let F M a method be defined on P M . F M is uniform if F M (u) = 1 1 M for Proposition 3 The congruence method is the only method on V that is impartial and where r minimizes the sum of the squared errors ij [(u u) ij -nr i r j )] 2 and s minimizes

Proof of Proposition 3 Consider the function ij [(u u) ij -nr i r j )] 2 . The first order conditions for minimization write j [(u u) ij -mr i r j ]r j = 0 for each i, or j (u u) ij r j = (n j r 2 j )r i for each i. Hence r is an eigenvector of u u. Diagonalizing the symmetric matrix u u in an orthogonal basis, one checks that the global minimum is obtained for the largest eigenvalue.

The congruence method is not uniform, as shown by the following example.

Example Let M and N have each three elements and the evaluation matrix u be

.

The counting scores are all equal to 2. The congruent scores satisfy r a = r b ≈ 1.57r c . This proves that the method is not uniform. In the above example, a and b's scores are higher than c's due to the good evaluations of α and β on them, which reinforce each other. More generally, the departure from the counting scores is due to the pattern of joint evaluations.

This can be seen from the following decomposition of the ij-th term of matrix u u. (u u) ij is equal to λ u iλ u jλ or

The term (u u) ij is increasing in the counting scores of each i and j and in the congruence in the evaluations of both: If those who value i more than the average also value j highly, and have dispersed preferences on others agents, then (u u) ij is higher than nu i+ u j+ . Thus, a group of agents tend to have higher scores than their counting scores if those who value them have concentrated high evaluations on them. Roughly speaking, a group of individuals with similar evaluations weigh more than their aggregate.

Finally, note that the mutual centrality and the congruence methods coincide for affiliation networks, since v = u. The characterization in Proposition 3 applies to any pair of evaluation matrices, in particular it applies to affiliation networks (because the minimization of errors does not consider variations in the evaluation matrices).