François Laroussinie
email: francois.laroussinie@liafa.jussieu.fr

Antoine Meyer
email: antoine.meyer@univ-mlv.fr

Eudes Pétonnet

Eudes Petonnet
email: eudes.petonnet@liafa.jussieu.fr

Counting CTL

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Among the existing approaches to the formal verification of automated systems, model checking [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF][START_REF] Queille | Specification and verification of concurrent systems in CESAR[END_REF] aims at automatically establishing the validity of a certain formal specification (modeled as a formula in a suitable logic) over the system under study (modeled for instance as a finite automaton). This set of techniques is now well-established and successful, with many real-world applications.

To formalize the specification of temporal properties, for instance in the case of reactive systems, temporal logics (TL) were proposed thirty years ago [START_REF] Pnueli | The temporal logic of programs[END_REF] and widely studied since. They are today used in many model-checking tools. There exists a wide variety of temporal logics, differing for instance by the models over which formulas are interpreted or by the kind of available temporal modalities. Two well-known examples are LTL in the linear-time framework (where formulas are interpreted over infinite runs) and CTL for the branching-time case (where formulas are interpreted over states of Kripke structures). See [START_REF] Emerson | Temporal and modal logic[END_REF] for a survey of classical temporal logics for systems specification.

Temporal logics have been extended in various ways in order to increase their expressive power. For example, while LTL and CTL only contain future operators, it is also possible to consider past-time modalities to express properties of the past of a run. One can also extend temporal logics with regular expressions (see for instance [START_REF] Wolper | Temporal logic can be more expressive[END_REF][START_REF] Emerson | Generalized quantitative temporal reasoning: An automata-theoretic approach[END_REF]). Other extensions were proposed to handle quantitative aspects of systems. For example, some logics can contain timing constraints to specify that some event P 1 has to occur less than 10 time units before another event P 2 . Such temporal logics, like TCTL [START_REF] Alur | Model-checking in dense real-time[END_REF][START_REF] Emerson | Quantitative temporal reasoning[END_REF], have been especially studied in ⋆ Partly supported by ANR project DOTS and project QUASIMODO (FP7-ICT).

the framework of timed model checking. Another quantitative extension consists in probabilistic logics where one can specify probability bounds over the truth of some property (see for example [START_REF] Bianco | Model checking of probabilistic and nondeterministic systems[END_REF]).

We propose several extensions of CTL with constraints over the number of states satisfying certain sub-formulas along runs. For example, considering a model for an ATM, we can express the property "whenever the PIN is locked, at least three erroneous attempts have been made" by: ¬EF [♯error≤2] lock (one cannot reach a state where the PIN is locked but less than two errors have occurred). Similarly, ¬EF [♯error≥3] money states that three mistakes forbid cash retrieval. We use subscripts on the temporal modality (as in TCTL) to associate a constraint with the run for which the modality holds. Note that these two properties could be clearly stated in CTL by nesting E U modalities, but the resulting formulas would probably be too big to be easily handled by the user of a model checker. For each extension we consider, we study its expressiveness compared to CTL. In some cases, there is no formal gain of expressiveness because there exist natural translations to obtain equivalent CTL formulas, but these extensions are often exponentially more succinct than CTL: they allow writing concise specifications that would require formulas of exponentially larger size in CTL. In other cases, we show that adding some constraints increases the expressive power of CTL.

We consider the model checking problem for various sets C of constraints, and denote by CCTL C the corresponding extension of CTL. We show that polynomialtime algorithms exist when considering Until modalities with constraints of the form 3i ♯ϕ i ∼ c with ∼∈ {<, ≤, =, ≥, >} and c ∈ N. Additionally allowing Boolean combinations of such constraints or integer coefficients in the sum (or both) makes model checking ∆ P 2 -complete. We also consider the case of diagonal constraints ♯ϕ -♯ψ ∼ c and their more general form i ±♯ϕ i ∼ c with c ∈ Z and show that model checking can be done in polynomial time. However, allowing Boolean combinations of such constraints leads to undecidability. Finally we define a version of CCTL with freeze variables and show that it induces a complexity blow-up: model checking becomes PSPACE-complete.

Several existing works provide related results. In [START_REF] Emerson | Generalized quantitative temporal reasoning: An automata-theoretic approach[END_REF], an extension of LTL with a kind of regular expressions containing quantitative constraints over the number of occurrences of sub-expressions is presented. This extension yields algorithms whose time complexity is exponential in the size of formulas and the value of integer constants. In [START_REF] Emerson | Parametric quantitative temporal reasoning[END_REF], extensions of CTL are defined including parameters in constraints. One of these formalisms, namely GPCTL, allows one to express properties with constraints defined as positive Boolean combinations of sums of the form i P i ≤ c where every P i is an atomic proposition. Modelchecking E U formulas with such a constraint is shown to be NP-complete and a polynomial algorithm is given for a restricted logic (with parameters). In [START_REF] Yang | Symbolic model checking for event-driven real-time systems[END_REF], a branching-time temporal logic with general counting constraints (using a variant of freeze variables) is defined to specify event-driven real-time systems. To obtain decidability, they restrict the analysis to systems verifying some bounded progress condition. In [START_REF] Bouajjani | Verifying infinite state processes with sequential and parallel composition[END_REF][START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF], extensions of LTL and CTL with Presburger constraints over the number of states satisfying some formulas are considered, for some class of infinite state processes. The complexity of these problems is much higher than the cases we are concerned with. Finally there also exist timed extensions of CTL interpreted over Kripke structures (see for instance [START_REF] Emerson | Quantitative temporal reasoning[END_REF]).

The paper is organized as follows. In Section 2, we introduce the definitions of the main formalisms we will use. In Section 3, we show that several of our proposed logics are not more expressive than the classical CTL, yet exponentially more succinct. In Section 4, we address the model-checking problem and provide exact complexity results for most of the logics we introduce. Finally we present in Section 5 a different logic with freeze variables, together with the complexity of its model-checking problem.

Definitions

Models

Let AP be a set of atomic propositions. In branching-time temporal logics, formulas are interpreted over states of Kripke structures.

Definition 1. A Kripke structure (or KS) S is a tuple Q, R, ℓ where Q is a finite set of states, R ⊆ Q × Q is a total accessibility relation 4 and ℓ : Q → 2 AP
is a labelling of states with atomic propositions.

A run ρ of S is an infinite sequence of states q 0 q 1 q 2 . . . such that (q i , q i+1 ) ∈ R for every i. We use ρ(i) to denote the state q i and ρ |i to denote the prefix q 0 • • • q i of ρ. Runs(q) denotes the set of runs starting from some state q ∈ Q. We write σ ≤ ρ when σ is a prefix of ρ.

We will also consider Durational Kripke Structures (DKS), where an integer duration is associated with every transition. Thus for a DKS S = Q, R, ℓ , we have R ⊆ Q × N × Q. The duration of a transition is also called a weight or a cost. We use DKS 0/1 to denote the DKSs where the durations belong to {0, 1}. The notion of duration is naturally extended to finite runs of DKSs.

Counting CTL

We define several extensions of CTL able to express constraints over the number of times certain sub-formulas are satisfied along a run. Definition 2. Given a set of atomic propositions AP and a set of constraints C, we define:

CCTL C ∋ ϕ, ψ ::= P | ϕ ∧ ψ | ¬ϕ | EϕU [C] ψ | AϕU [C] ψ
where P ∈ AP and C ∈ C. The sets of constraints we consider are defined as follows, with l, k ∈ N, k ′ ∈ Z and ∼∈ {<, ≤, =, ≥, >}. First we have the sets of atomic constraints:

C 0 ∋ C ::= ♯ϕ ∼ k with ϕ ∈ CCTL C0 C 1 ∋ C ::= (Σ l i=1 ♯ϕ i ) ∼ k with ϕ i ∈ CCTL C1 αC 1 ∋ C ::= (Σ l i=1 α i • ♯ϕ i ) ∼ k with ϕ i ∈ CCTL αC1 , α i ∈ N C 2 ∋ C ::= (♯ϕ -♯ψ) ∼ k ′ with ϕ, ψ ∈ CCTL C2 C 3 ∋ C ::= (Σ l i=1 ± •♯ϕ i ) ∼ k ′ with ϕ i ∈ CCTL C3 αC 3 ∋ C ::= (Σ l i=1 α i • ♯ϕ i ) ∼ k ′ with ϕ i ∈ CCTL αC3 , α i ∈ Z Let L a be the set {C 0 , C 1 , αC 1 , C 2 , C 3 , αC 3 }.
We also consider the set of constraints B(C) for every C ∈ L a , defined as the set of Boolean combinations of atomic constraints in C with sub-formulas in CCTL B(C) . We use

L b for {B(C) | C ∈ L a }. Finally L cons def = L a ∪ L b .
We make use of the standard abbreviations ∨, ⇒, ⇔, ⊥, ⊤, as well as the additional modalities

EF [C] ϕ def = E⊤U [C] ϕ, AF [C] ϕ def = A⊤U [C]
ϕ, and their duals

AG [C] ϕ def = ¬EF [C] ¬ϕ and EG [C] ϕ def = ¬AF [C] ¬ϕ.
Any formula occurring in a constraint C associated with a modality in Φ is considered as a sub-formula of Φ. The size |Φ| of Φ takes the size of these constraints and their sub-formulas into account, assuming that integer constants are encoded in binary (unless explicitly stated otherwise). The DAG-size of Φ is the total number of distinct sub-formulas of Φ. As model-checking algorithms compute only once the truth value of a subformula, this is generally more relevant to the complexity of model-checking.

The semantics of CCTL C formulas (with C ∈ L cons ) is defined over Kripke structures as follows: Definition 3. The following clauses define the conditions for a state q of some KS S = Q, R, ℓ to satisfy a CCTL C formula ϕ -written q |= S ϕ -by induction over the structure of ϕ (we omit Boolean modalities):

q |= S EϕU [C] ψ iff ∃ρ ∈ Runs(q), ∃i ≥ 0, ρ(i) |= S ψ, ρ |i-1 |= S C, and ∀0 ≤ j < i, ρ(j) |= S ϕ q |= S AϕU [C] ψ iff ∀ρ ∈ Runs(q), ∃i ≥ 0, ρ(i) |= S ψ, ρ |i-1 |= S C, and ∀0 ≤ j < i, ρ(j) |= S ϕ
Let C ∈ L cons be a set of constraints and C be a constraint in C, the semantics of ρ |i |= S C is based on the interpretation of ♯ϕ over ρ |i , denoted by |ρ |i | ϕ and defined as:

|ρ |i | ϕ def = |{j | 0 ≤ j ≤ i ∧ ρ(j) |= S ϕ}|. Given these values, C is interpreted in a natural way.
In the following we omit the subscript S for |= when no confusion is possible. We use ≡ to denote the standard equivalence between formulas.

Remark 1. The classical X operator ("neXt") can be expressed in CCTL C0 as EXϕ ≡ EF [♯⊤=1] ϕ, and that basic constraints in C 0 can be expressed in

C 2 because ♯ϕ ≡ ♯ϕ-♯⊥. Moreover, for CCTL B(C) with C ∈ L a , since ϕU [C] ψ ≡ F [C∧♯(¬ϕ)=0] ψ
the modality F is sufficient to define U; thus such a logic CCTL B(C) can also be built from atomic propositions using Boolean operators and modalities

EF [C] ϕ and AF [C] ϕ (or EG [C] ϕ).
Note that all these translations are succinct (linear in the size of formulas) and do not have any impact on complexity results.

Remark 2. The related temporal logic TCTL [START_REF] Alur | Model-checking in dense real-time[END_REF], whose semantics are defined over timed models, allows one to label temporal modalities with duration constraints. For instance, one may write ϕU <k ψ to express the fact that ϕ is consistently true until, before k time units have elapsed, ψ eventually holds. When all transitions in a durational Kripke structure have duration 1 (i.e. the duration of any run is equal to its length), TCTL (or RTCTL in [START_REF] Emerson | Quantitative temporal reasoning[END_REF]) formulas can be directly coded into the logic CCTL C0 by only using the sub-formula ⊤ inside constraints. A similar coding is also possible when one uses a proposition tick to mark time elapsing as in [START_REF] Laroussinie | On the expressivity and complexity of quantitative branching-time temporal logics[END_REF].

Examples of CCTL formulas.

Consider a model for an ATM, whose atomic propositions include money, reset and error, with the obvious meaning. To specify that it is not possible to get money when three mistakes are made in the same session (i.e. with no intermediate reset), we can use the formula AG ¬EF [♯error≥3∧♯reset=0] money that belongs to CCTL B(C0) . Note that this could also be expressed by the

CCTL C0 formula AG ¬E(¬reset)U [♯error≥3] money .
Consider a mutual exclusion algorithm with n processes trying to reach their critical section. We can specify that it verifies the bounded waiting property with bound 10 (i.e. when a process P tries to reach its CS, then at most 10 other processes can reach theirs before P does) by the following CCTL B(C1) formula:

AG i request i ⇒ ¬EF [ P j =i ♯CSj >10∧♯CSi=0] ⊤ . AG [♯send-♯receive<0]
⊥ belongs to CCTL C2 and states that along any finite run, the number of receive events cannot exceed the number of send events.

Quantitative constraints can also be useful for fairness properties. For example AG AF [ V i 5≤♯ϕi≤10] ⊤ expresses that the ϕ i 's occur infinitely often along every run (as stated with the CTL formula i (AG AF ϕ i )) but it also ensures some constraint on the number of states satisfying the ϕ i 's along every execution: for example, it is not possible to have a sub-run where ϕ 1 holds for 11 states and ϕ 2 holds only for 4 states.

Note that with CCTL αC3 one can express properties over the ratio of two kinds of states along a run. For example, EF [100•♯error-♯⊤<0] P is true when there is a path leading to P such that the rate of error states is less than 1 percent. Thus constraints of the form " ♯P ♯P ′ ∼ k" can easily be expressed with this logic. Finally note that we can use any temporal formula inside a constraint (and not only atomic propositions). For example, AG(EF [♯(EXalarm)≤5] init) states that it is always possible to reach init with a path along which at most 5 states have a successor satisfying alarm.

These examples illustrate the ability of CCTL formulas to state properties over the portion of a run leading to some state. A similar kind of properties could also be expressed with past-time modalities (like S or F -1 ), but unlike these modalities our constraints cannot easily describe the ordering of events in the past: they "only" allow to count the number of occurrences of formulas. We will see in the next sections that our extensions do not always induce a complexity blow-up, while model-checking CTL + F -1 is known to be PSPACE-complete [START_REF] Laroussinie | Specification in CTL+Past for verification in CTL[END_REF].

CCTL expressiveness and succinctness

When comparing two logics, the first question which comes to mind is the range of properties they can be used to define, in other words their expressiveness. When they turn out to be equally expressive, a natural way to distinguish them is then to ask how concisely each logic can express a given property. This is referred to as succinctness, and is also relevant when studying the complexity of model-checking for instance, since it may considerably influence the size of a formula required to express a given property, and hence the time required to model-check it. In this section we study the expressiveness of the different logics defined in the previous section, and provide partial results and comments about their respective succinctness with respect to CTL.

Expressiveness

We first show that only allowing boolean combinations and positive sums in constraints does not allow CCTL to express more properties than CTL. Proof (sketch). Let Φ be a CCTL B(αC1) formula of the form EF [C] ϕ whose constraint C contains n counting arguments ♯ϕ 1 to ♯ϕ n , each preceded by a multiplicative constant α i , and m atomic constraints. We inductively translate Φ to CTL by building a family of formulas whose intended meaning (up to technical details) is as follows:

-If constraint C holds with ♯ϕ i = 0 for all i, then ϕ may be true immediately.

-Otherwise, successively check for every i which of the ϕ i hold in the current state, updating constraint C along the way by decreasing by α i the constant to which ϕ i is compared in Φ. -Once all ϕ i have been scanned, proceed to the next state and reevaluate C

for the new values of the constants.

Each of these steps corresponds to a sub-formula of the form Φ C ′ ,i,b in the CTL translation of Φ, where C ′ is the current constraint to be checked, i is the index of the formula ϕ i being scanned, and b is a boolean flag used to enforce termination, Φ C,0,⊥ being the translation of Φ itself. By counting the number of distinct Φ C ′ ,i,b , one can show that the DAG-size of

Φ C,0,⊥ is O(n.k m ),
where k is the maximal constant appearing in Φ. A similar argument holds for formulas of the form EG [C] ϕ with the same resulting DAG-size.

⊓ ⊔

Note that the upper bound for the above translation is parametric, and can be interpreted for all variants of CCTL below CCTL B(αC1) . An example of this translation on a CCTL αC1 formula is given in the next section. In contrast to this result, introducing subtractions in constraints yields a strict increase in expressiveness.

Proposition 5. The CCTL C2 formula ϕ = AG [♯A-♯B<0] ⊥ cannot be translated into CTL.

Proof (sketch). Formula ϕ (already seen in Sec. 2 with different atomic propositions) states that the number of B-labeled states cannot exceed the number of A-labeled states along any path. As shown by [START_REF] Bernholtz | An automata-theoretic approach to branching-time model-checking[END_REF] and also presented in [START_REF] Wilke | CTL + is exponentially more succinct than CTL[END_REF], the set of models of any CTL formula can be recognized by a finite alternating tree automaton. From such an automaton, one can easily build a finite alternating automaton over words, whose accepted language is the set of all prefixes of branches in models of the formula, seen as words over 2 AP .

Suppose there exists a CTL formula ϕ ′ equivalent to ϕ, and let A be the alternating tree automaton accepting its set of models. As stated above, from A one can derive a finite alternating automaton recognizing the set of all words over 2 {A,B} labeling a finite prefix of a branch in a model of ϕ, namely words whose prefixes contain at most as many B's as A's. Since this language is clearly not regular, this leads to a contradiction. ⊓ ⊔

Succinctness

Our extensions of CTL come with three main sources of possible concision, which appear to be orthogonal : the encoding of constants in binary, the possibility to use boolean combinations in the constraints, and the use of sums. However, only the first two prove out to yield an exponential improvement in succinctness : Proposition 6. For every formula Φ ∈ CCTL C1 with unary encoding of integers, there exists an equivalent CTL formula of DAG-size polynomial in |Φ|.

This proposition is a direct consequence of Prop. 4 where m, the number of atomic constraints, is set to 1. For instance, to translate Φ = EF [Σ n i=1 ♯pi=K] ϕ, we define ∀0 ≤ k ≤ K the family of CTL formulas:

∀1 ≤ i ≤ n, 0 ≤ j < n, Φ i,j,k = (p i ∧ Φ i+1,j+1,k ) ∨ (¬p i ∧ Φ i+1,j,k ) ∀1 ≤ j ≤ k, Φ n+1,j,k = EXE(¬ n i=1 p i )U(( n i=1 p i ) ∧ Φ 1,0,k-j ) Φ n+1,k,k = EXE(¬ n i=1 p i )Uϕ ∀j > k, Φ n+1,j,k = ⊥
By construction, we have Φ ≡ Φ 1,0,K . The size of this family is O(n.k), thus the DAG-size of Φ 1,0,K is also polynomial in |Φ|, even if its literal size is exponential. This example relies on the fact that constants are encoded in unary, to measure the impact of the addition operation in constraints. We now look at the succinctness gap due to the binary encoding of constants.

Proposition 7. CCTL C0 can be exponentially more succinct than CTL.

Proof. In [START_REF] Laroussinie | On the expressivity and complexity of quantitative branching-time temporal logics[END_REF], it is shown that the logic TCTL, when interpreted over Kripke structures with a special atomic proposition tick used to mark the elapsing of time, can be exponentially more succinct than CTL. More precisely, the TCTL formulas EF <n A and EF >n A, which are of size O(log(n)) since n is encoded in binary, do not admit any equivalent CTL formula of temporal height (and hence also size) less than n. These formulas express the existence of a path where A eventually holds and less (resp. more) than n clock ticks are seen until then.

They are clearly equivalent to the O(log(n))-size CCTL C0 formulas EF [♯tick<n] A and EF [♯tick>n] A respectively.

⊓ ⊔

This exhibits a first aspect in which CCTL logics can be exponentially more succinct than CTL. However, as expressed in the next proposition, another orthogonal feature of the logic may yield a similar blow-up. Proposition 8. CCTL B(C0) with unary encoding of integers can be exponentially more succinct than CTL.

Proof. It was shown by [START_REF] Wilke | CTL + is exponentially more succinct than CTL[END_REF][START_REF] Adler | An n! lower bound on formula size[END_REF] that any CTL formula ϕ equivalent to the CTL + formula ψ = E(FP 0 ∧ . . . ∧ FP n ) must be of length exponential in n. It turns out ψ is equivalent to the CCTL B(C0) formula ψ ′ = EF [ V i ♯Pi≥1] ⊤, which entails the result. Note that ψ ′ only contains the constant 1, which means that this gap cannot be imputed to the binary encoding.

⊓ ⊔

The intuitive reason for this blow-up is that a CTL formula expressing the property that atomic propositions P 1 to P n are each seen at least once along a path would have to keep track of all possible interleavings of occurrences of P i 's.

To summarize, we showed that two different aspects of the extensions of CTL presented in this paper, while not increasing the overall expressiveness of the logic, may yield exponential improvements in succinctness We still have to study similar succinctness properties of the remaining CCTL fragments with respect to CTL and to each other.

Model checking

Model checking CCTL C0 and CCTL C1

It turns out that model-checking CCTL C1 is polynomially equivalent to modelchecking CCTL C0 (or CTL), as both problems are P-complete.

Theorem 9. The model-checking problem for CCTL C1 is P-complete.

Proof. P-hardness comes from the P-hardness of CTL model-checking. For membership in P, we provide polynomial-time procedures to deal with the subformulas EψU

[C] ψ ′ and AψU [C] ψ ′ with C def = Σ l i=1 ♯ϕ i ∼ k.
Consider a Kripke structure S = (Q, R, ℓ), and inductively assume that the truth values of ψ, ψ ′ and ϕ i over each state of S are known: these sub-formulas will be seen as atomic propositions in the following.

To each state q occurring along a path, we associate a cost |q| C = |{i | q |= ϕ i }|, and note that the value of |q| C is in O(|C|). This cost is additively extended to paths in the usual way. Deciding the truth value of the path formula ψU [C] ψ ′ over any path ρ verifying ψUψ ′ then amounts to checking whether there exists a finite prefix ρ ′ q of ρ such that

|ρ ′ | C ∼ k, q |= ψ ′ and ∀i ≤ |ρ ′ |, ρ ′ (i) |= ϕ.
We reduce this problem to the model-checking of a TCTL formula over a DKS 0/1 (DKS with 0/1-durations) for which there exists a polynomial-time algorithm [START_REF] Laroussinie | On the expressivity and complexity of quantitative branching-time temporal logics[END_REF]. We build from S a DKS 0/1 S ′ = (Q ′ , R ′ , ℓ ′ ) as follows: for each state q ∈ Q with |q| C = n, Q ′ contains n + 1 additional states q 0 , . . . , q n . R ′ is then defined as {q

0 -→ q 0 | q ∈ Q} ∪ {q i 1 -→ q i+1 | q ∈ Q, i < |q| C } ∪ {q n 0 -→ q ′ | (q, q ′ ) ∈ R, n = |q| C }. Finally, we set ℓ ′ (q i ) = ∅ for all q i ∈ Q ′ \ Q and ℓ ′ (q) = ℓ(q) ∪ {ok} for all q ∈ Q ′ ∩ Q, where ok is a new atomic predicate.
To each path ρ = qσq ′ in S, we associate the path ρ = qq 0 . . . q n σq ′ in S ′ . It can now be shown by induction on run lengths that ρ satisfies ψU [C] ψ ′ if and only if ρ satisfies the TCTL path formula (ok ⇒ ψ)U [∼k] (ok ∧ ψ ′ ).

⊓ ⊔

Since CCTL C0 includes CTL and is included in CCTL C1 , we get:

Corollary 1. The model-checking problem for CCTL C0 is P-complete.

Model-checking CCTL B(C0) and CCTL αC1

We now establish the ∆ P 2 -completeness of model-checking for the fragments CCTL B(C0) , CCTL αC1 and CCTL B(αC1) . Let us first recall the definition of the complexity class ∆ P 2 , one of the classes of the polynomial hierarchy.

Definition 10. ∆ P 2 = P NP is the class of problems solvable in polynomial time with access to an oracle for some NP-complete problem.

We now prove ∆ P 2 -hardness of the model-checking problem for CCTL B(C0) .

Theorem 11. The model-checking problem for CCTL B(C0) is ∆ P 2 -hard.

Proof. We proceed by reduction from the ∆ P 2 -complete problem SNSAT [START_REF] Laroussinie | Model checking CT L + and F CT L is hard[END_REF]. Given p families of variables X 1 , . . . X p with X i = {x 1 i , ..., x m i } and a set Z = {z 1 , . . . , z p } of p variables, an instance I of SNSAT is defined as a collection of p propositional formulas ϕ 1 , . . . , ϕ p under 3-conjunctive normal form (3-CNF), where each ϕ i involves variables in X i ∪ {z 1 , ..., z i-1 }, and the values of each z i is defined as

z i def = ∃X i . ϕ i (z 1 , ..., z i-1 , X i ).
The instance I is positive iff the value of z p is ⊤. We denote by v I the unique valuation of variables in Z induced by I.

From I, we define the KS described in Figure 1. Every state is labeled by its name, and in addition every state zi is labeled by some new atomic proposition P z . We use X to denote the set X 1 ∪ • • • ∪ X p and V for X ∪ Z. A path ρ from q p to q F describes the valuation v ρ such that v ρ (y) = ⊤ if ρ visits state y and ⊥ if it visits ȳ for every variable y in V. We use a CCTL B(C0) formula to ensure that v ρ coincides with v I over Z, that is:

zp zp-1 z1 x 1 p x 2 p x m 1 qp qp-1 qp-2 • • • q1 q0 • • • • • • qF zp zp-1 z1
v ρ (z i ) = ⊤ iff v I (z i ) = ⊤ for any i ∈ {1, . . . , p}.
Let ϕ i be the formula ϕ i where every occurrence of the literal x is replaced by ♯x = 1. We define the CCTL B(C0) formula Ψ 0 as ⊤ and for every 1

≤ k ≤ p, Ψ k as EX E(P z ⇒ ¬Ψ k-1 )U [C k ] q F , with C k def = l≤k (♯z l = 1) ⇒ ϕ l ∧ k j=1 (♯q = j) ⇒ ϕ j .
The first part of the constraint C k aims at ensuring that v ρ (z l ) = ⊤ is witnessed by a valuation for {z 1 , . . . , z l-1 } ∪ X l satisfying ϕ l . The second part ensures the formula ϕ j is satisfied by v ρ when Ψ k is interpreted from z j or zj (i.e. when the number of qs along the path leading to q F is j). The formula Ψ j holds for a state q i with i ≤ j when v I (z i ) is ⊤. The embedding of Ψ j-1 inside Ψ j is used to ensure that going through a zm with i ≥ m is always necessary w.r.t. I (i.e. there is no way to satisfy the corresponding ϕ m ): Lemma 12. For any i = 1, . . . , p and i ≤ j ≤ p, we have:

z i |= Ψ j ⇔ v I (z i ) = ⊤ and zi |= Ψ j ⇔ v I (z i ) = ⊥
Now it is sufficient to check whether q 0 satisfies Ψ p or not, and then deduce the truth value of v I (z p ).

⊓ ⊔

Theorem 13. The model-checking problem for CCTL αC1 is ∆ P 2 -hard.

Proof. We provide a reduction from the model checking problem for TCTL specifications over Durational Kripke structures. TCTL formulas allow to deal with the cost (or duration) of paths (i.e. the sum of the weight of every transition occurring along the path). This problem is ∆ P 2 -complete [START_REF] Laroussinie | Efficient timed model checking for discrete-time systems[END_REF]. Let S = (Q, R S , ℓ) be a DKS. Let W be the set of weights occurring in S. We define the Kripke structure S ′ = (Q ′ , R S ′ , ℓ ′ ) as follows:

-Q ′ def = Q ∪ {(q, d, q ′ ) | ∃(q, d, q ′ ) ∈ R S }, - for
any (q, d, q ′ ) ∈ R S , we add (q, (q, d, q ′ )) and ((q, d, q ′ ), q ′ ) in R S ′ ; and

-ℓ ′ : Q ′ → 2 AP ′ with AP ′ def = AP∪{ok}∪{P d | d ∈ W } -we assume ok, P d ∈ AP.
And we have: ℓ ′ (q) def = ℓ(q) ∪ {ok} for any q ∈ Q, and ℓ ′ (q, d, q ′ ) = {P d }.

Now we can easily see that q |=

S Φ with Φ ∈ TCTL is equivalent to q |= S ′ Φ where P def = P , ¬ψ def = ¬ ψ, ϕ ∧ ψ def = ϕ ∧ ψ, EϕU ∼c ψ def = E(ok ⇒ ϕ)U [C(∼c)] (ok ∧ ψ) and AϕU ∼c ψ def = A(ok ⇒ ϕ)U [C(∼c)] (ok∧ ψ) with C(∼ c) def = d∈W d•♯P d ∼ c. ⊓ ⊔
Theorem 14. The model-checking problem for CCTL B(αC1) is in ∆ P Proof (sketch). Let S = Q, R, ℓ be a KS. For this proof, we only need to provide NP procedures to deal with sub-formulas of the form EF

[C] ϕ and EG [C] ϕ. First let {C 1 , . . . , C l } be the set of αC 1 constraints occurring in C. Each C i is of the form j≤li α i j • ♯ϕ i j ∼ i d i .
And let d max be the maximal integer constant occurring in C. Now we can present the algorithms:

-Φ def = EF [C] ψ: If q |= Φ
, then there exists a run ρ starting from q and leading to some q ′ such that (1) q ′ |= ψ and (2) ρ without q ′ satisfies the constraint C. First note that we can assume that the length of ρ is bounded with respect to the model and formula: a sequence of |Q| states contributes for at least 1 to some linear expressions in C and then the length of ρ is in O(|Q|.2 |C| ) due to the binary encoding of the constants. An easy NP algorithm consists in guessing the Parikh image of the transitions in ρ, which can be represented in polynomial size. Moreover it is possible to check (in polynomial time) that q ′ satisfies ψ, ρ without q ′ satisfies C, and F ρ corresponds to a path in S.

-Φ def = EG [C] ψ: For this case we have to find an infinite path ρ satisfying the property "if the current prefix satisfies the constraint C, then the next state has to satisfy ψ". Every constraint C i ∈ αC 1 in C may change its truth value at most twice along ρ. Therefore ρ can be decomposed in a bounded number of parts over which the truth value of every constraint is constant. As previously, the length of every part is bounded and its Parikh image can be encoded in polynomial size. Moreover it is possible to ensure that the juxtaposition of all ρ m is correct.

⊓ ⊔

A direct corollary of Theorems 11, 13 and 14 is:

Corollary 2. The model-checking problem for CCTL C is ∆ P 2 -complete for each C ∈ {αC 1 , B(C 0 ), B(C 1 ), B(αC 1 )}.

Diagonal constraints

We now show that even if diagonal constraints lead to strictly more expressive logics than CTL, model checking CCTL C2 and CCTL C3 is not more difficult than model checking CTL itself.

Theorem 15. The model-checking problem for CCTL C2 is P-complete.

Proof (sketch). P-hardness comes from that of CCTL C0 model-checking. Using the fact that Aϕ

′ U [C] ψ ′ ≡ AF [C∧♯¬ϕ ′ =0] ψ ′ ≡ ¬EG [C∧♯¬ϕ ′ =0] ¬ψ ′ ,
to show membership in P, we only need to provide polynomial-time procedures to verify sub-formulas of the form

Eϕ ′ U [C] ψ ′ and EG [C∧♯ϕ ′ =0] ψ ′ with C def = ♯ϕ -♯ψ ∼ k. Consider a Kripke structure S def = (Q, R, ℓ).
As previously, we associate a "cost" to each state q ∈ Q. In this case however, |q| C can only be -1, 0 or 1 depending on the truth values of ϕ and ψ. Inductively assume that the truth values of ϕ, ψ, ϕ ′ and ψ ′ over each state of S are known: these sub-formulas will be seen as atomic propositions in the following. We distinguish the two main cases below:

-Φ def = Eϕ ′ U [C] ψ ′ :
We consider the weighted and directed graph G S = (V, E) representing the transition relation of S restricted to states verifying the formula Eϕ ′ Uψ ′ , where edges are weighted by the cost of their source state and where only edges whose source verifies ϕ ′ are considered. If C def = ♯ϕ -♯ψ ≤ k, then the formula holds true on state q if and only if there exists a state q ′ such that q ′ |= S ψ ′ and either an elementary (i.e. acyclic) path ρ in G S of weight less than k from q to q ′ , or a path from q to some state q ′′ appearing on a negative-weight cycle, and from q ′′ to q ′ . Using a classical reachability algorithm over G S , one can determine the existence of such paths in polynomial time. If C def = ♯ϕ -♯ψ = k with k ≥ 0, we will compute the relation R k over V 2 denoting the existence of a run of weight k between states q and q ′ and simply test whether (q, q ′ ) ∈ R k for some q ′ verifying ψ ′ . Using dichotomy and simple fixed-point computations, we are able to compute R k in time polynomial in |Φ|, i.e. logarithmic in k The treatment of negative weights is omitted.

- Proof (sketch). In this setting, each state contributes to the cost of a path by a certain positive or negative number whose absolute value is bounded by some integer d. Similarly to the technique used in the proof of Theorem 9, the idea is to build a durational Kripke structure, this time with weights in {-1, 0, 1}, by adding intermediate states. Once this DKS is built, relations R i , R + i and R - i may be computed as previously, and the satisfaction of the formula under consideration tested.

Φ def = EG [C∧♯ϕ ′ =0]
⊓ ⊔

Theorem 16. The model-checking problem for CCTL B(C2) is undecidable.

Proof (sketch). This is done by reduction from the halting problem of a twocounter machine M with counters C and D. We define a Kripke structure S M with one state to simulate each of M's instructions, plus some auxiliary states. We use labels ϕ + X and ϕ - X with X ∈ {C, D} to witness increments and decrements, and additional labels ok X , ko X to simulate the positive test "X = 0": whenever the counter's value is assumed to be zero, and before simulating the next instruction, the run goes through an auxiliary state labeled ko X whose unique successor is labeled ok X . Hence along any run in S M , a prefix satisfies ♯ko X > ♯ok X right after counter X was deemed equal to zero, and only then. By counting occurrences of these predicates, one can write a CCTL B(C2) formula expressing the fact that M is correctly simulated by S M and never halts.

⊓ ⊔ Instead of using counting constraints associated with temporal modalities, we now consider freeze variables and explicit constraints inside formulas.

Definition 17. Given a set of atomic propositions AP and a set of variables V , we define: CCTL fv ∋ ϕ, ψ ::

= P | ϕ ∧ ψ | ¬ϕ | z[ψ].ϕ | C | EϕUψ | AϕUψ where P ∈ AP and C is a constraint l i=1 α i • z i ∼ c with z i ∈ V , α i ∈ N, c ∈ N and ∼∈ {<, ≤, =, ≥, >}.
Intuitively z[ψ].ϕ means that (1) the variable z is reset to zero and associated with the sub-formula ψ (i.e. z will evolve like ♯ψ in the future) and (2) given this semantics for z, ϕ holds for the current state. We say that an occurrence of some variable z is free in ϕ when this occurrence does not appear in the scope of a reset operator "."; a formula without any free variable is closed. For example, the CCTL B(C0) formula EF [♯P ≤5∧♯P ′ >2] P ′′ can be expressed in CCTL v as the formula z

[P ].z ′ [P ′ ].EF(z ≤ 5 ∧ z ′ > 2 ∧ P ′′ ).
A CCTL v formula ϕ is interpreted in a state of a KS extended with a valuation for any free variable in ϕ and an environment associating a sub-formula to any free variable. We use dom to denote the domain of such functions and ⊥ to represent undefined values. Given a function f and x ∈ dom(f ), we use f [x ← a] to denote the function mapping x to a, and every element y to f (y) if y = x. Finally let SubF(ϕ) be the set of all ϕ sub-formulas.

Given a valuation v : V → N ∪ {⊥} for a set of variables occurring in a CCTL v formula ϕ, and an environment ε : V → SubF(ϕ) ∪ {⊥} such that dom(v) = dom(ε), and given a finite run π, we define the valuation (v + ε π) as follows: (v+ ε π)(z) def = ⊥ if z ∈ dom(v), and otherwise (v+ ε π)(z) def = v(z)+|{j|0 ≤ j ≤ |π| ∧ π(j) |= ε(z)}|. The semantics of CCTL v is defined as follows: Definition 18. The following clauses define when a state q of some KS S = Q, R, ℓ and a valuation v satisfy a CCTL v formula ϕ in an environment εwritten (q, v) |= S,ε ϕ -by induction over the structure of ϕ (we omit the cases of Boolean modalities):

(q, v) |= S,ε EϕUψ iff ∃ρ ∈ Runs(q), v |= ρ,ε ϕUψ (q, v) |= S,ε AϕUψ iff ∀ρ ∈ Runs(q), v |= ρ,ε ϕUψ

(q, v) |= S,ε z[ψ].ϕ iff (q, v[z ← 0]) |= S,ε[z←ψ] ϕ (q, v) |= S,ε Σ l i=1 α i • z i ∼ c iff Σ l i=1 α i • v(z i ) ∼ c
where v |= ρ,ε ϕUψ iff ∃i ≥ 0, (ρ(i), v + ε ρ |i-1 ) |= S,ε ψ and ∀0 ≤ j < i, (ρ(j), v + ε ρ |j-1 ) |= S,ε ϕ.

Theorem 19. Model checking closed CCTL v formulas is PSPACE-complete.

Proof. PSPACE-hardness can be proved by a reduction from QBF. PSPACEmembership is obtained by considering a non-deterministic algorithm working in polynomial space to decide whether a CCTL v formula holds for a state q within a KS S. The main idea is to encode a configuration (q, v, ε) in polynomial size: this is possible for v since we just have to record the value for the counter z up to d max + 1 where d max is the maximal constant used in a constraint with z. In order to verify EϕUψ -we assume that ϕ and ψ have already been treated -we guess, from the current configuration (q, v, ε), the next configuration (q ′ , v ′ , ε) and then we verify that there is a transition in S leading from q to q ′ such that the valuation v is updated with v ′ w.r.t. the environment ε. Then it remains to verify that either ψ or ϕ holds for (q ′ , v ′ ) (and in the latter case, guess a new configuration etc.). The same holds for EG. The operator z[ψ].ϕ changes the environment ε and resets z to zero. And for any configuration one can decide the truth value of a constraint C. ⊓ ⊔

Conclusion

In several cases (up to B(αC 1 ) constraints) the logics we introduce are not more expressive than CTL, but can concisely express properties which would be difficult to write in that logic. In particular, CCTL C0 and CCTL B(C0) can be exponentially more succinct than CTL. As for the remaining fragments, even though CCTL C2 is strictly more expressive than CTL, model-checking remains polynomial up to CCTL C3 (complexity results are summarized in Figure 2). Further work on CCTL will include completing the study of succinctness of its fragments with respect to each other and to other logics, looking for an upper complexity bound for the model-checking of CCTL αC3 , as well as investigating new kinds of constraints and extensions to LTL and CTL * .

Proposition 4 .

 4 Any CCTL B(αC1) formula can be translated into CTL.

x1 p x2 p xm 1 Fig. 1 .

 11 Fig. 1. Kripke structure associated to an SNSAT problem.

Corollary 3 .

 3 ψ ′ : We use the weighted and directed graph G S representing the transition relation of S where edges are weighted by the cost of their source state, to build a new Kripke structure S ′ and a classical CTL formula Ψ such that S satisfies Φ if and only if S ′ satisfies Ψ .⊓ ⊔By combining the techniques used in the previous construction with those used in the proof to Theorem 9, we obtain a similar result for the logic CCTL C3 . The model-checking problem for CCTL C3 is P-complete.

2 CCTLC 1 CCTLC 3 1 3 CCTLCCTL B(αC 3 )Fig. 2 .

 2131332 Fig. 2. Summary of model-checking complexity results.

For complexity results, we always assume that integer constants are encoded in binary.


Renaud Coulomb
email: coulomb@pse.ens.fr.

Marc Sangnier
email: marc.sangnier@sciences-po.org.

Jel Codes

: C58

Impacts of Political Majorities on French Firms: Electoral Promises or Friendship Connections?

Keywords: Political Majority, Prediction Markets, Firms Value, Abnormal Returns, Social Network, Political Connections Political majority, prediction markets, firms value, abnormal returns, social network, political connections. JEL Codes: C58, D72, D84, H50, G14

This paper analyzes the impact of changes in the winning chances of candidates running for the 2007 French presidential election on abnormal stock returns of firms that could benefit from a candidate's victory. We use prices formed by transactions on a political prediction market to reveal the probabilities of victory of S. Royal and N. Sarkozy. We find that changes in S. Royal's probability of victory have no impact on firms that should benefit from her party platform. On the opposite, abnormal returns of firms that should benefit from reforms announced by N. Sarkozy or that are directed or owned by his friends are positively correlated with changes in his probability of victory. Both effects appear to be independent and the network effect is fifty percents larger than the other one. All these results persist when we take into account specific characteristics of firms.

Introduction

Political majorities have an impact on global economic activity. This effect is driven by ideology or by the nature of the competition to access the power (see [START_REF] Alesina | Partisan Politics, Divided Government, and the Economy[END_REF] and [START_REF] Alesina | Political Cycles and the Macroeconomy[END_REF] for seminal surveys of this issue). At a micro-level, political majorities can impact the value of firms, either through their political orientations or friendship connections of individuals in office. In this paper, we analyze returns of firms listed on the French stock market induced by anticipated changes in the political majority during the 2007 French presidential election.

To achieve this, we compare the effect of changes in the different candidates' probability of victory on the value of firms. We use prices from a prediction market to assess changes in each candidate's probability of victory. We correlate abnormal returns of stocks of firms belonging to different groups to these changes. Firms that should benefit of S. Royal's platform do not exhibit high abnormal returns. On the opposite, firms that should benefit from reforms announced by N. Sarkozy or whose top executives or main shareholders are friends of him exhibit significantly positive abnormal returns. The effect of the raise of N. Sarkozy on the latter group is stronger than the effect on the first group.

All in all, results presented in this paper uncover the value attached to the political platforms of candidates and to the friendship connections of N. Sarkozy. Other papers show that friendship connections are priced by the market. [START_REF] Fisman | Estimating the Value of Political Connections[END_REF] shows that Indonesian firms linked with Suharto have seen their value decreasing with Suharto's health problems. [START_REF] Do | Out of Sight, Out of Mind:The Value of Political Connections in Social Networks[END_REF] show that US firms whose top executives are connected to politicians running for the Congress exhibit positive abnormal returns if the politician wins. [START_REF] Khwaja | Do Lenders Favor Politically Connected Firms? Rent Provision in an Emerging Financial Market[END_REF] present the advantage of politically connected firms to have access to the financial market in Pakistan. [START_REF] Claessens | Political connections and preferential access to finance: The role of campaign contributions[END_REF] study political connections and preferential access to finance. [START_REF] Fan | Politically connected CEOs, corporate governance, and Post-IPO performance of China's newly partially privatized firms[END_REF] and [START_REF] Li | Political connections, financing and firm performance: Evidence from Chinese private firms[END_REF] estimate the value of political connections in China. [START_REF] Goldman | Do Politically Connected Boards Affect Firm Value?[END_REF] determines the impact of politically connected boards on firms value in the United States.

Prediction markets offer an interesting source of data concerning political expectations as shown by [START_REF] Knight | Are policy platforms capitalized into equity prices? Evidence from the Bush/Gore 2000 Presidential Election[END_REF] and [START_REF] Snowberg | Partisan Impacts on the Economy: Evidence From Prediction Markets and Close Elections[END_REF]. They consist in betting markets where betters can exchange contracts whose payoffs depend on the outcome of a contingent event. For the 2007 French presidential election, News-Futures proposed "Winner-take-all" contracts linked to the victory of S. Royal or N. Sarkozy. Under the market efficiency assumption, the literature interprets the price of a "Winner-take-all" contract as the average probability of the candidate's victory as estimated by the market. This is the best prevision of future outcomes on the basis of past and current public information. In that case, a change in prices of such contracts reflects the arrival of unexpected and relevant news. Prediction markets have often formulated accurate predictions about political outcomes. Using Iowa Electronic Market data about American presidential elections of 1988of , 1992of , 1996of , and 2000[START_REF] Berg | Accuracy and Forecast Standard Error of Prediction Markets[END_REF] show that these data are more accurate than opinion polls. [START_REF] Rhode | Historical Presidential Betting Markets[END_REF] point out that a large political prediction market correctly anticipated the outcomes of the American presidential elections from 1868 to 1940 while no scientific opinion poll was available. Studying betting on district-level political elections in Australia, [START_REF] Wolfers | Three Tools for Forecasting Federal Elections: Lessons from 2001[END_REF] find that market predictions are accurate in spite of the fact that no scientific opinion poll is available for this type of elections. [START_REF] Wolfers | The network of N.Sarkozy includes other people not present that[END_REF] reach similar conclusions. See also [START_REF] Snowberg | Partisan Impacts on the Economy: Evidence From Prediction Markets and Close Elections[END_REF] who highlight how prediction market data help in event studies. By separating a single event window into many small sub-windows, prediction markets data make estimates of relations more precise than traditional event studies.

Using a panel data set made of the 119 largest firms listed on the French stock market, we analyze the correlation between the time series of variations of the probability of a candidate's victory and abnormal stock market returns of these firms from January 1 st 2007 to the election day. Abnormal returns of a firm are defined as the part of its returns that cannot be simply explained by the average stock market evolution: they represent the idiosyncratic evolution of a firm value. Under the assumption that stock market's actors use all the available information in the best possible way, abnormal returns of firms evolve before the election as its outcome is anticipated. Firms that should benefit in one way or another from the victory of a specific candidate should have abnormal returns positively correlated with changes in this candidate's probability of victory. Contrary to [START_REF] Herron | Measurement of Political Effects in the United States Economy: A Study of the 1992 Presidential Election[END_REF] who investigates impacts of political majority at the sector level, or [START_REF] Snowberg | Partisan Impacts on the Economy: Evidence From Prediction Markets and Close Elections[END_REF] who analyze these impacts on aggregate values (stock markets index, oil price, bonds, future price of dollars etc.), we propose a semi-disaggregated analysis to point out impacts of political majorities on specific groups. This allows us to test two potential channels of transmission from politics to the firms' value: the announced reforms included in programs and the friendship network channel. Accordingly, we create three different groups of firms on the basis of available information. Two of them are made of firms that should benefit from reforms announced by N. Sarkozy and S. Royal. The last one is made of firms owned or directed by friends of N. Sarkozy whose connections with businessmen as been largely discussed by French medias. We find that N. Sarkozy 's winning probability is positively associated with abnormal returns of firms listed in his network or supposed to benefit from his political program. Both effects seem independent. The effect on firms' abnormal returns associated with membership to his network is however around fifty percents larger than the other one. Isolating from his network his close friends, we find that the effect is the strongest for firms ruled or owned by his closest friends. There is also partial evidence that firms listed in the network of N. Sarkozy have abnormal returns negatively correlated with changes in the winning probability of S. Royal and abnormal returns of firms that should benefit from S. Royal's program are not correlated with changes in her winning probability. All these results take into account that changes in the candidates' probability of victory may also impact firms differently depending on their characteristics such as the industry in which they are active, their size or whether they are partially owned by the state or not.

The remainder of the paper is organized as follows. Section 2 presents the Newsfutures data and the way the different groups are constructed. Section 3 describes and discusses the identification strategy based on the efficiency market hypothesis. Empirical results are presented in section 4. Finally, section 5 provides concluding remarks.

Data

This section presents the data used in this paper: the firms value data set and the political expectations data set.

Stock market returns and groups of firms

The SBF 120 is a reference index composed by the 120 most actively traded stocks on the Paris stock Exchange. In this paper, we use daily stock values of firms composing the SBF 120 from mid-2006 to mid-2007. Data are from Euronext. 1The daily return of each firm is simply the change in percentage between the opening price and the closing price. We extract information about ownership of each firm by the state from [START_REF] Ernst | Étude sur l'actionnariat et le contrôle des principales entreprises française cotées[END_REF].

Before the election, experts from "La Société Générale", a French leading bank, had analyzed the electoral programs of N. Sarkozy and S. Royal and defined two portfolios composed of 27 selected firms that could benefit from reforms announced by each candidate. In this paper, we take these two groups as given by La Société Générale (2007). The detailed composition of both groups is presented in appendix.

Medias have reported strong connections between N. Sarkozy and some businessmen. The term "valeurs Sarkozy" has been used sometimes in media to name firms like Dassault, Lagardère, and Bouygues for example. We build a list of businessmen connected to N. Sarkozy using information provided by various sources such as [START_REF] Chemin | La Nuit du Fouquet's[END_REF] and [START_REF] Dély | Sarkozy et l'argent roi[END_REF]. We associate firms of the SBF 120 to people who direct the firm or own it. To assess ownership, we check whether an individual holds over 5% of shares or of voting rights. We take into account indirect participation. The precise description of firms we listed in the network of N. Sarkozy is presented in appendix.

The full list of firms included in the different groups can be found in table 8 in appendix. The number of firms within each group is given by figure 1. Table 1 presents descriptive statistics for average returns of firms belonging to the different groups from January 1 st 2007 to the first round of the presidential election.

Prediction market data

The French presidential election follows a two-round process to elect by direct vote a president for a five-year term. This election orientates the political majority at the French parliament. For the 2007 presidential election, the first round of voting took place on April 22 nd . The main political candidates were known by the beginning of January 2007: F. Bayrou, S. Royal, and N. Sarkozy.2 Since no candidate obtained a majority of fifty percents plus one vote, a second round between the two leading candidates took place on May 6 th . N. Sarkozy, leader of the main right-wing party was opposed to S. Royal, candidate of the main left-wing party. N. Sarkozy was elected.

We use data from a predictive market website -NewsFutures -to measure daily changes in each candidate's probability of victory between January 1 st 2007 and the first round of the election. NewsFutures was the prediction market with the strongest activity for this election. On this website, players sell and buy "Winnertake-all" contracts over a candidate's name (S. Royal or N. Sarkozy) that offer a 100 units payoff if this candidate finally wins the election. The exchange price of these contracts between player depends on instantaneous matching of demand and supply. After receiving a free initial endowment, betters can set limit orders. N contracts are issued (destroyed) when a better wants to buy (to sell) N contracts and another better wants to buy (to sell) N opposite contracts. The historic of prices, bid and ask orders, the number of contracts in circulation are common knowledge among betters. Until the outcome is decided, the trading price reflects to a certain extent the collective consensus among betters about the expected value of the contract, i.e. the average probability of each candidate's victory as estimated by the market. For an interesting discussion over the interpretation of prediction prices as probabilities, see [START_REF] Manski | Interpreting the Predictions of Prediction Markets[END_REF] and [START_REF] Wolfers | The network of N.Sarkozy includes other people not present that[END_REF].

A transaction is registered at a given price as soon as two opposite orders match. It was active 7 days a week and 24 hours a day, from the end of 2005 to May 6 th 2007. We gathered the whole historic record of transactions of "Winner-take-all" contracts associated with S. Royal and N. Sarkozy. We reconstruct opening and closing prices to match the daily pattern of the French stock market. 3 We then define the daily change in percentage of each candidate's probability to be elected as the ratio of the difference between closing and opening prices to the opening price.

Note that NewsFutures uses virtual currency as requested by French law. This may raise an issue concerning the quality of the prediction made by players on the election's outcome. There are however some points that allow to alleviate some of these doubts. For instance, the best betters are ranked on the website. The ranking of top betters and the virtual wealth can be considered as a symbolical payoff, and seem to be a sharp incentive to predict well, if we trust the enthusiasm of betters on the website forum. In addition, gains in virtual money allow the better to participate to auctions to win "real" goods, so payoffs are indirectly real. See [START_REF] Servan-Schreiber | Prediction Markets: Does Money Matter?[END_REF] for additional comments on this issue.

Activity on NewsFutures has increased until the 2007 French presidential election. As shown by figure 2, the number of transactions per day sharply increased from December 2006. All days without any exchange occur before December 2006. Even if days without any exchange or a weak activity do not necessarily mean that the prediction market is inefficient (if no relevant information is revealed, no change in prices should occur), information conveyed by such low flows of transactions may be scarce. Note that activity sharply increases when the main candidate became confirmed and publicly known. In this paper, we use only data from January 1 st 2007 on.

Figure 3 plot the victory probabilities of N. Sarkozy and S. Royal as the price of associated "Winner-take-all" contracts from December 2006 on. Assuming that only three candidates could have won the elections from the point of view of investors and betters and that the market is balanced, we compute the probability of victory of F. Bayrou as Max {0, 100 -P Royal -P Sarkozy }, where P Candidate is the price of "Winner-take-all" contract on Candidate. NewsFutures has correctly predicted the two winners of the first round (N. Sarkozy and S. Royal) and the final winner of the election. We globally observe three periods. Up to February, contracts associated with S. Royal and N. Sarokzy are exchanged at the same price of 50 virtual curency units. From February on, the probability of victory of N. Sarkozy steady increases. This went alongside with a regular decrease of the one of S. Royal. In March, F. Bayrou appeared as an credible alternative during a short period of time.

Estimation strategy

This section briefly describes the estimation strategy to uncover and estimate the market value of political orientations and friendship connections of the different candidates who ran for the 2007 French presidential election. To achieve this, we look at the correlation between winning probability changes of one candidate and abnormal returns of firms listed on the French stock market.

We first construct abnormal returns of each firm by estimating the relation of its return to the market return before the events period and predicting them over the period of interest (see [START_REF] Mackinlay | Event Studies in Economics and Finance[END_REF]). Concretely, we run the following regression for each firm i using daily returns between September 1 st and December

31 st 2006: R t = α + β × Rt + ε t , (1)
where R t is firm i stock return on day t, Rt is the market return on day t, and ε t is the error term. 4 We estimate this expression separately for each firm, what gives us distinct pairs of parameters α and β for each firm. These estimated parameters are used to compute abnormal returns of each firm from January 1 st 2007 to the election date using the following formula:

Rt = R t -α + β × Rt , ( 2
)
where Rt is abnormal return of firm i and the other notations are as defined above.

The method we use to identify correlations between changes of candidates' winning probabilities and abnormal returns of firms consists mainly in the estimation of interaction terms. The expression we estimate includes daily firm level observations from January 1 st to April 22 nd 2007. It can be written as follows:

Rit = α + β × ∆Candidate jt + γ × 1 {Group c } i × ∆Candidate jt + I i + ε it , (3)
where ∆Candidate jt is the change in percentage of candidate j winning probability on day t, 1 {Group c } i is equal to 1 if firm i belongs to group c, I i is a firm fixed effect, and ε it is the error term. This flexible expression allows us to include additional interaction terms with different terms and different candidates. We estimate this expression using ordinary least squares and correct standard errors to take heteroscedasticity into account. Parameter β captures the average effect of changes in winning probability of candidate j on all firms abnormal returns. Parameter γ captures the effect of changes in winning probability of candidate j on firms that belong to group c.

Considering abnormal returns allows to directly look at the over or underperformance of a group of firms according to a political scenario and to point out redistribution effects among firms (as used by [START_REF] Knight | Are policy platforms capitalized into equity prices? Evidence from the Bush/Gore 2000 Presidential Election[END_REF] for example). In addition, it reduces the simultaneity bias that would arise if the stock market affected individuals votes or if a third variable impacted both elements.

To be valid, our method requires that the prediction market incorporates unexpected relevant information in a similar way that the stock market does. Investors and betters must have access to the same set of information, use the same implicit model to infer the probability of victory of a candidate from political news, and react at the same speed. [START_REF] Fama | Efficient Capital Markets: A Review of Theory and Empirical Work[END_REF] categorizes the efficiency of a market into three levels: strong form, semi-strong form and weak form of efficiency depending on the set of information already embedded in current prices (respectively: all the public and private information, all the public information, the whole historic of prices). Performing runs tests of independence of "Winner-take-all" prices variations and logarithmic random walk tests for prices, we do not find empirical evidence to reject the assumption that we face a weakly efficient market. 5Testing if prices incorporates instantly all the public relevant information available, requires first to be able to define this arrival of new pieces of information and then to infer from them winning probabilities i.e to be able to define how good prices must be. Semi-strong form efficiency tests are always joint-hypothesis tests: a first hypothesis concerning what good prices must be, the second one concerning the similarity between good prices and observed prices. Defining the relevant set of information and its dynamics, and inferring probabilities from it appear highly impossible to do in our case; so testing semi-strong form of efficiency seems out of reach. We make the assumption that the market is efficient in the semi-strong form. As indicated above, prices well reflect the general dynamics of the campaign, the winners of both rounds, the rise and fall of F. Bayrou, and other events that support our assumption.

Private information concerning the electoral outcome is scarce enough not to be analyzed at all.

Results

In this section, we present the main results on the effect of changes in candidates winning probabilities on the abnormal returns of firms. The period used from this analysis runs from January 1 st to April 22 nd 2007. The second date is the first round of the 2007 French presidential election.6 All estimated effects must be interpreted as impacts perceived by the stock market (that may wrongly consider that a candidate is favorable to some firms) under the assumption that variations of "Winner-take-all" prices reflect changes in the probability of a candidate's victory.

We start by investigating the average effect of changes in the three candidates winning probabilities on listed firms irrespective of their characteristics. Table 2 presents estimates of equation (3) without any interaction terms. In columns 1 to 3, we regress daily abnormal returns of firms on changes in winning probabilities of the three candidates separately. In columns 4 to 6, we run the same exercise using all combinations of changes in winning probabilities. 7 According to results presented in this table, there is no evidence of any aggregate effect of changes in winning probabilities on firms abnormal returns.

Interaction terms are included in regressions presented in table 3. In the upper part of the table, we investigate the effect of change in winning probabilities of the three different candidates on firms belonging to N. Sarkozy 's network. The estimated expression is thus equation (3) where group c is the network of N.

Sarkozy. In the middle part of table 3, the group of interest is constituted of firms that should benefit of reforms announced by N. Sarkozy. In the bottom part of the table, the group of interest contains firms that should benefit of reforms planned by S. Royal. The first three columns of each part separately test the effect of change in winning probability of a single candidate. The last three columns test how effects change when an alternative candidate is taken into account.

Results presented in the upper and middle parts of table 3 show that changes of N. Sarkozy winning probability are positively associated with abnormal returns of firms listed in this candidate's network or supposed to benefit from his planned reforms. Figures 4 and5 illustrate these facts. In each figure, we plot average daily abnormal returns of firms belonging to one of the groups and the daily changes in N. Sarkozy's probability of victory. In both cases, series are positively correlated. Table 3 provides also partial evidence that firms listed in the network of N. Sarkozy have abnormal returns negatively correlated with changes in the winning probability of S. Royal as shown by estimated coefficients presented in columns 4 and 6. Results presented in the bottom part of the table suggest that abnormal returns of firms that should benefit from the platform of S. Royal are not correlated with changes in winning probability of any candidate. Taking account of the changes in the winning probabilities of the other candidates, we find that this effect is stronger when changes in N.Sarkozy's chances of winning go along with opposite changes of the same magnitude in S. Royal's chances, suggesting that this political alternative is real for investors.

All in all, table 3 suggests that market operators interpret the possible victory of N. Sarkozy in the presidential election as beneficial for firms listed in his network or which should benefit from his political program. These results may however be due to specific characteristics of firms listed in these two groups. For example, N. Sarkozy is maybe more connected with influential individuals belonging to particularly large firms or to firms operating in specific activities. We tackle these issues in tables 4 and 5 where we add new interaction terms to equation (3). In table 4, the group of interest is made of firms belonging to the candidate's network. In table 5 the group of interest contains firms that should benefit from the platform of N. Sarkozy. In column 1 of tables 4 and 5, we introduce interaction terms of changes in the winning probability of N. Sarkozy and dummy variables equal to 1 if a firm belongs to a particular industry. In column 2 of both tables, we control for interactions with dummy variables capturing the extent of ownership by the state. In column 3, we introduce an interaction term with a dummy variable equal to 1 if the firm belongs to the CAC 40 which is the index of the 40 largest firms listed on the French stock market. Finally, the last column of both tables presents estimates from a regression where all the above described interactions are entered simultaneously. Interestingly, none of the added interaction terms is found to be statistically significant in tables 4 and 5. Furthermore, the estimated coefficient of interaction terms of interest is remarkably stable accross specification. Whatever the group of interest, it is virtually identical to the corresponding estimate presented in table 3: around 0.035 for the network and around 0.025 when the group is defined as firms that should benefit from reforms announced by N. Sarkozy.

A natural question is whether effects found for firms belonging to the two groups are redundant or not. As shown by figure 1, the two groups are clearly distinct but have still some firms in common. In table 6, we present estimates of a horse race between effects associated with membership to the two groups. The estimated coefficients correspond to equation (3) when two different interaction terms are entered simultaneously. In even-numbered columns, we include the set of interaction terms capturing firms characteristics as in 4 and 5. In columns 3 and 4, we also include an interaction term for firms belonging to both groups. As shown by estimates presented in table 6, the effect of changes in winning probability of N. Sarkozy on firms belonging to his network has still the same order of magnitude. The same remark may be done about the interaction term for firms that should benefit from the reforms of this candidate, although the coefficient looses some statistical significance. Interestingly, we do not find any evidence of a supplementary effect for the few firms belonging to both groups. All in all, both effects seems to be fairly independent. The effect associated with membership to the network of this candidate is however around fifty percents larger than the other one: changes in winning probability of N. Sarkozy have a stronger influence on abnormal returns of firms listed in his network.

The last exercise we conduct in this paper consists in a decomposition of the network of N. Sarkozy into "close friends" and firms that belong only to his network. The list of firms included in the first group can be found in table 8 in appendix.

Reasons to classify firms in this group are also presented in appendix. According to estimates presented in the first column of table 7, there is no statistically significant effect of changes in winning probability of the candidate on abnormal returns of firms belonging only to his network. On the contrary, the effect is stronger than all previous estimates for firms listed in the group made of "close friends". In column 2, we add the large set of additional interactions with firms characteristics already used above. Estimated coefficients are not altered by the addition of these co-variates. These results suggest that distance to the candidate does matter in the evaluation made by market actors of consequences from the expected victory of N. Sarkozy on firms returns.

Concluding remarks

How large is the sum of money represented by excess returns induced by the raise of N. Sarkozy during the 2007 campaign? A back of the envelope calculation allow us to estimate that firms belonging to the network of N. Sarkozy experienced together a 11, 953 millions euros excess capitalization due to his election. The back of the envelope calculation is following. By the end of December 2006 total stock market capitalization of firms listed in the network of N. Sarkozy amounts 341, 530 millions euros. From January 1 st 2007 to the election, the probability of victory of this candidate went from 0.5 to 1, which represents total increase of 100 percents. Taking the effect of changes in this candidate's probability of victory on abnormal returns of firms belonging to his network equal to 0.035 (which corresponds approximately to the average effect estimated across the different specifications), we obtain a total increase of 0.035 × 341, 530 = 11, 953 millions for the value of firms.8 Under the same reasoning, the 0.035 effect can also be compared to the return of an asset which value would increase by 3.5% over a four months period on top of the average market evolution.

We have analyzed returns of firms listed on the French stock market induced by anticipated changes in the political majority during the 2007 French presidential election. We have targeted three groups of firms that should benefit from a candidate 's victory. Two of them are made of firms that should benefit from reforms announced by N. Sarkozy and S. Royal. The last one is made of firms owned or directed by friends of N. Sarkozy whose connections with businessmen as been largely discussed by French medias. We have examined the correlation of abnormal stocks returns of firms belonging to these groups with changes in each candidate's probability of victory as revealed by a political prediction market. Firms that should benefit of S. Royal's platform do not exhibit high abnormal returns. On the opposite, firms that should benefit from reforms announced by N. Sarkozy or whose top executives or main shareholders are friends of him exhibit significantly positive abnormal returns. The effect on firms' abnormal returns associated with membership to his network is however around fifty percents larger that the other one. Isolating from his network his close friends, we find that the effect is the strongest for firms ruled or owned by his closest friends. There is also partial evidence that firms listed in the network of N. Sarkozy have abnormal returns negatively correlated with changes in the winning probability of S. Royal and abnormal returns of firms that should benefit from S. Royal's program are not correlated with changes in her winning probability. All these results take into account that changes in the candidates' probability of victory may also impact firms differently depending on their characteristics such as the industry in which they are active, their size or whether they are partially owned by the state or not. See the text to get information about the composition of each group and table 8 for the list of firms within each of them. The logarithmic random walk of a price P can be written as: ln(P ) = ln(P t-1 ) + ε t (6)

where, ε t is a white noise. Return at time t can be written as Pt-P t-1 P t-1 , and approximated by ln( Pt P t-1 ). Results of Dickey-Fuller augmented tests presented in table 10 do not incite us to reject that ln(P t ) has a unit root and so that prices of "Winner-take-all' contracts follow a logarithmic random walk.

Figure 1 :

 1 Figure 1: Repartitions of firms between the different groups.

Figure 2 :

 2 Figure 2: Number of daily transactions on the predictive market from September 1 st 2006 to May 6 th 2007.

Figure 3 :

 3 Figure 3: Winning probabilities of S. Royal, N. Sarkozy, and F. Bayrou at the 2007 French presidential election.

Figure 4 :

 4 Figure 4: Changes in N. Sarkozy probability of victory and abnormal returns of firms that should benefit from his reforms, from January 1 st to April 22 nd 2007.

Figure 5 :

 5 Figure 5: Changes in N. Sarkozy probability of victory and abnormal returns of firms listed in his network, from January 1 st to April 22 nd 2007.

Table 1 :

 1 Returns of firms from January 1 st to April 2 nd 2007.This table presents descriptive statistics on average returns of firms belonging to different groups from January 1 st 2007 to the first round of the presidential election. Returns over the period correspond to the ratio of the difference between the opening price on January 2 d and the closing price on April 20 th over the opening price on January 2 nd . See the text for definitions of the different groups.

		Obs	Mean	Std.	Min	Max
	Network of N. Sarkozy	19	0.065	0.118	-0.097	0.399
	Program of N. Sarkozy	23	0.120	0.165	-0.276	0.487
	Program of S. Royal	21	0.113	0.125	-0.276	0.244
	None of the above groups	72	0.077	0.119	-0.355	0.421
	All firms	119	0.089	0.128	-0.355	0.487

Table 2 :

 2 Effect of changes in winning probability of the different candidates on abnormal returns of firms. Robust standard errors in parentheses. All regressions include firm fixed effects and a constant term. OLS regressions. Each column presents estimates from a separate regression. ∆Candidate is the daily change in percentage of winning probability of Candidate.

	Dependent variable: daily abnormal return.
		(1)	(2)	(3)	(4)	(5)	(6)
	∆ Sarkozy	0.000			0.000	-0.000
		(0.004)			(0.004)	(0.005)
	∆ Royal		0.000		0.000		0.000
			(0.003)		(0.003)		(0.003)
	∆ Bayrou			-0.000		-0.000	-0.000
				(0.000)		(0.000)	(0.000)
	Observations	9,118	9,118	9,118	9,118	9,118	9,118
	R-squared	0.036	0.036	0.036	0.036	0.036	0.036
	*** p<0.01, ** p<0.05, * p<0.1.

Table 3 :

 3 Effect of changes in winning probability of the different candidates on abnormal returns of firms belonging to specific groups. Robust standard errors in parentheses. All regressions include firm fixed effects and a constant term. OLS regressions. Each column presents estimates from a separate regression. ∆Candidate is the daily change in percentage of winning probability of Candidate. Variables Group are equal to 1 for firms that belong to the group mentioned in the first line of each part of the table. See the text for definitions of the different groups.

	Dependent variable: daily abnormal return.
	Group: Sarkozy (network)
		(1)	(2)	(3)	(4)	(5)	(6)
	∆Sarkozy	-0.006			-0.006	-0.008
		(0.005)			(0.005)	(0.006)
	∆Royal		0.002		0.002		0.003
			(0.003)		(0.003)		(0.004)
	∆Bayrou			0.000		-0.000	0.000
				(0.000)		(0.000)	(0.000)
	Group × ∆Sarkozy	0.036***			0.037***	0.047***
		(0.011)			(0.011)	(0.013)
	Group × ∆Royal		-0.011		-0.012*		-0.017**
			(0.007)		(0.007)		(0.008)
	Group × ∆Bayrou			-0.001		0.001	-0.001*
				(0.001)		(0.001)	(0.001)
	Observations	9,118	9,118	9,118	9,118	9,118	9,118
	R-squared	0.037	0.036	0.036	0.037	0.037	0.036
	Group: Sarkozy (program)
		(7)	(8)	(9)	(10)	(11)	(12)
	∆Sarkozy	-0.005			-0.005	-0.005
		(0.005)			(0.005)	(0.006)
	∆Royal		0.001		0.001		0.002
			(0.003)		(0.003)		(0.004)
	∆Bayrou			0.000		-0.000	0.000
				(0.000)		(0.000)	(0.000)
	Group × ∆Sarkozy	0.024**			0.025**	0.027**
		(0.011)			(0.011)	(0.014)
	Group × ∆Royal		-0.004		-0.005		-0.009
			(0.008)		(0.008)		(0.008)
	Group × ∆Bayrou			-0.001		0.000	-0.001
				(0.001)		(0.001)	(0.001)
	Observations	9,118	9,118	9,118	9,118	9,118	9,118
	R-squared	0.036	0.036	0.036	0.036	0.036	0.036
	Group: Royal (program)
		(13)	(14)	(15)	(16)	(17)	(18)
	∆Sarkozy	-0.000			-0.000	0.001
		(0.005)			(0.005)	(0.006)
	∆Royal		-0.002		-0.002		-0.002
			(0.003)		(0.003)		(0.004)
	∆Bayrou			0.000		0.000	0.000
				(0.000)		(0.000)	(0.000)
	Group × ∆Sarkozy	0.003			0.002	-0.005
		(0.011)			(0.011)	(0.014)
	Group × ∆Royal		0.011		0.011		0.009
			(0.007)		(0.007)		(0.008)
	Group × ∆Bayrou			-0.001		-0.001	-0.000
				(0.001)		(0.001)	(0.001)
	Observations	9,118	9,118	9,118	9,118	9,118	9,118
	R-squared	0.036	0.036	0.036	0.036	0.036	0.036
	*** p<0.01, ** p<0.05, * p<0.1.

Table 4 :

 4 Effect of changes in winning of N. Sarkozy on abnormal returns of firms belonging to his network, controlling for industries, state ownership and the size of firms. Robust standard errors in parentheses. All regressions include firm fixed effects and a constant term. OLS regressions. Each column presents estimates from a separate regression. ∆Candidate is the daily change in percentage of winning probability of Candidate. Variables Group are equal to 1 for firms that belong to the group mentioned in the first line of the table. See the text for definitions of the different groups. The reference industry is "Technology". The reference category for state ownership is[40, 100]. Intervals indicate the share of capital owned by the state.

	Dependent variable: daily abnormal return.
	Group: Sarkozy (network)
		(1)	(2)	(3)	(4)
	∆ Sarkozy	-0.019	0.011	-0.009	-0.010
		(0.014)	(0.020)	(0.006)	(0.027)
	Group × ∆Sarkozy	0.034***	0.039***	0.033***	0.034***
		(0.011)	(0.011)	(0.012)	(0.013)
	Gas and petroleum × ∆Sarkozy	0.019			0.019
		(0.024)			(0.025)
	Basic materials × ∆Sarkozy	-0.013			-0.013
		(0.026)			(0.026)
	Industrials × ∆Sarkozy	0.015			0.013
		(0.017)			(0.018)
	Consumer goods × ∆Sarkozy	0.003			0.003
		(0.018)			(0.018)
	Health care × ∆Sarkozy	0.004			0.001
		(0.024)			(0.025)
	Consumer services × ∆Sarkozy	0.020			0.020
		(0.017)			(0.017)
	Telecommunications × ∆Sarkozy	0.019			-0.026
		(0.041)			(0.048)
	Utilities × ∆Sarkozy	0.030			0.018
		(0.025)			(0.029)
	Financials × ∆Sarkozy	0.022			0.022
		(0.017)			(0.018)
	No state ownership × ∆Sarkozy		-0.021		-0.013
			(0.021)		(0.024)
	State ownership ∈ (0, 5) × ∆Sarkozy		0.005		0.006
			(0.023)		(0.025)
	State ownership ∈ [5, 10) × ∆Sarkozy		-0.026		-0.020
			(0.027)		(0.030)
	State ownership ∈ [10, 25) × ∆Sarkozy		-0.032		-0.030
			(0.029)		(0.030)
	State ownership ∈ [25, 40) × ∆Sarkozy		0.013		0.026
			(0.028)		(0.033)
	Cac 40 × ∆Sarkozy			0.010	0.010
				(0.009)	(0.011)
	Observations	9,118	9,118	9,118	9,118
	R-squared	0.037	0.037	0.037	0.038
	*** p<0.01, ** p<0.05, * p<0.1.

Table 5 :

 5 Effect of changes in winning of N. Sarkozy on abnormal returns firms that should benefit from his reforms, controlling for industries, state ownership and the size of firms. ** p<0.01, ** p<0.05, * p<0.1. Robust standard errors in parentheses. All regressions include firm fixed effects and a constant term. OLS regressions. Each column presents estimates from a separate regression. ∆Candidate is the daily change in percentage of winning probability of Candidate. Variables Group are equal to 1 for firms that belong to the group mentioned in the first line of the table. See the text for definitions of the different groups. The reference industry is "Technology". The reference category for state ownership is[40, 100]. Intervals indicate the share of capital owned by the state.

	Dependent variable: daily abnormal return.
	Group: Sarkozy (program)
		(1)	(2)	(3)	(4)
	∆ Sarkozy	-0.018	0.013	-0.009	-0.012
		(0.014)	(0.020)	(0.006)	(0.027)
	Group × ∆Sarkozy	0.021*	0.028**	0.022**	0.024**
		(0.011)	(0.011)	(0.011)	(0.012)
	Gas and petroleum × ∆Sarkozy	0.018			0.021
		(0.024)			(0.025)
	Basic materials × ∆Sarkozy	-0.008			-0.009
		(0.026)			(0.026)
	Industrials × ∆Sarkozy	0.013			0.011
		(0.017)			(0.018)
	Consumer goods × ∆Sarkozy	0.004			0.005
		(0.018)			(0.018)
	Health care × ∆Sarkozy	-0.005			-0.013
		(0.024)			(0.025)
	Consumer services × ∆Sarkozy	0.024			0.024
		(0.017)			(0.017)
	Telecommunications × ∆Sarkozy	0.018			-0.032
		(0.041)			(0.048)
	Utilities × ∆Sarkozy	0.038			0.026
		(0.025)			(0.029)
	Financials × ∆Sarkozy	0.018			0.018
		(0.018)			(0.018)
	No state ownership × ∆Sarkozy		-0.021		-0.010
			(0.021)		(0.023)
	State ownership ∈ (0, 5) × ∆Sarkozy		0.002		0.001
			(0.024)		(0.025)
	State ownership ∈ [5, 10) × ∆Sarkozy		-0.034		-0.024
			(0.027)		(0.030)
	State ownership ∈ [10, 25) × ∆Sarkozy		-0.034		-0.033
			(0.029)		(0.030)
	State ownership ∈ [25, 40) × ∆Sarkozy		0.011		0.029
			(0.028)		(0.032)
	Cac 40 × ∆Sarkozy			0.014	0.016
				(0.009)	(0.010)
	Observations	9,118	9,118	9,118	9,118
	R-squared	0.037	0.037	0.037	0.038

*

Table 6 :

 6 Effect of changes in winning N. Sarkozy on abnormal returns of firms that should benefit from his reforms and firms belonging to his network. ** p<0.01, ** p<0.05, * p<0.1. Robust standard errors in parentheses. All regressions include firm fixed effects and a constant term. OLS regressions. Each column presents estimates from a separate regression. ∆Candidate is the daily change in percentage of winning probability of Candidate. Variables Group are equal to 1 for firms that belong to the group mentioned. See the text for definitions of the different groups.

	Dependent variable: daily abnormal return.
		(1)	(2)	(3)	(4)
	∆Sarkozy	-0.009*	-0.010	-0.010*	-0.013
		(0.005)	(0.027)	(0.005)	(0.027)
	Network × ∆Sarkozy	0.034***	0.032**	0.037***	0.035**
		(0.011)	(0.013)	(0.013)	(0.014)
	Program × ∆Sarkozy	0.020*	0.021*	0.023*	0.024*
		(0.011)	(0.012)	(0.013)	(0.013)
	Network × Program × ∆Sarkozy			-0.011	-0.014
				(0.025)	(0.025)
	Industry fixed effects × ∆Sarkozy		Yes		Yes
	State ownership × ∆Sarkozy		Yes		Yes
	Cac 40 × ∆Sarkozy		Yes		Yes
	Observations	9,118	9,118	9,118	9,118
	R-squared	0.037	0.038	0.037	0.038

*

Table 7 :

 7 Effect of changes in winning probability of N. Sarkozy on abnormal returns of firms belonging to his network, decomposed in different groups. ** p<0.01, ** p<0.05, * p<0.1. Robust standard errors in parentheses. All regressions include firm fixed effects and a constant term. OLS regressions. Each column presents estimates from a separate regression. ∆Candidate is the daily change in percentage of winning probability of Candidate. Variables Group are equal to 1 for firms that belong to the group mentioned. See the text for definitions of the different groups.

	Dependent variable: daily abnormal return.
		(1)	(2)
	∆Sarkozy	-0.006	-0.012
		(0.005)	(0.027)
	Close friends × ∆Sarkozy	0.045***	0.048***
		(0.013)	(0.015)
	Only network × ∆Sarkozy	0.021	0.008
		(0.018)	(0.019)
	Industry fixed effects × ∆Sarkozy		Yes
	State ownership × ∆Sarkozy		Yes
	Cac 40 × ∆Sarkozy		Yes
	Observations	9,118	9,118
	R-squared	0.037	0.038

*

Only 119 firms are used in this paper. We exclude Eurotunnel from the analysis because its quotation was stopped during part of the period.

S. Royal was declared as the official candidate of her party after the primaries of the "Parti Socialiste", on November 16 th 2006. F. Bayrou presented his will to run the election for the "Modem" on December 2 nd 2006. Finally, although the primaries of the "Union pour un Mouvement Populaire" occurred only in January 2007, it was already clear that N. Sarkozy would be the candidate of this party.

3 For each contract, we define the opening price as the price of the closest transaction to 9 a.m., and the closing price as the price of the closest transaction to 5 : 30 p.m. French legal time.

In this paper, we use average daily return of stocks that are part of the SBF 120 as market return. Results using the SBF 120 index, i.e. taking into account relative sizes of firms, to compute the market return are fairly identical.

See section B in appendix for a presentation of these tests.

Results are qualitatively and quantitatively similar if we extend the period up to the second round of the 2007 French presidential election.

As changes in F. Bayrou 's winning probability have been indirectly constructed using information from winning probabilities of N. Sarkozy and S. Royal, we do not include the three changes of winning probabilities simultaneously.

Applying the same method, we would obtain a 7, 236 millions euros excess capitalization for firms that should benefit from the platform announced by N. Sarkozy. Although not statistically significant, results obtained using the platform of S. Royal suggest that 3, 614 millions euros is a upper bound for the value of her program.

See La Société Générale (2007).

Appendices

A Groups of firms

A.1 Firms should benefit of reforms announced by Royal and N. Sarkozy

Both groups have been constructed by analysts from "La Société Générale". 9 The first regroups firms that could be favored by reforms announced by S. Royal. It is made of the following firms: Alstom, Carrefour, Derichebourg, CNP Assurance, Delachaux, Dexia, EDF Energies Nouvelles, EDF, Géophysique, Haulotte Group, Iliad, Kaufman and Broad, Lafarge, Legrand, Michelin, Nexity, Peugeot, Publicis Group, Rhodia, Saint-Gobain, Schneider, Seloger.com, Suez, Théolia, Véolia environ., and Vinci. Firms of this group that belong to SBF 120 are listed under the heading "Program of S. Royal" in table 8.

The second regroups firms that could be favored by reforms announced by N. Sarkozy and is composed as follows: Accor, Alstom, Alten, April Group, Assystem, AXA, Bouygues, Derichebourg, Crédit Agricole, Delachaux, Dexia, EDF Energies Nouvelles, Eiffage, Essilor, Icade, Kaufman and Broad, Legrand, Metropole TV, Nexity, Peugeot, Saint-Gobain, Sodexo, Teleperformance, TF1, Théolia, Véolia environ., Vinci. Firms of this group that belong to SBF 120 are listed under the heading "Program of N. Sarkozy" in table 8.

A.2 N. Sarkozy's network

To select firms belonging to the network of N. Sarkozy, we used information provided by [START_REF] Chemin | La Nuit du Fouquet's[END_REF] and [START_REF] Dély | Sarkozy et l'argent roi[END_REF]. We associate firms to people who direct the firm or own it. To assess ownership, we check whether an individual holds over 5% of shares or of voting rights. We take into account indirect participation.

On May 6 th 2007 evening, the night that immediately followed his election, N. Sarkozy invited at the Fouquet's, a famous high-class restaurant in Paris, a group B Tests on NewsFutures data

B.1 The runs

The runs test -also known Wald-Wolfowitz test -is a non-parametric statistical test that checks the mutual independence of a sequence of elements (null hypothesis).

A "run" of a sequence is a maximal (non-empty) segment of the sequence composed by equal elements. For instance, the sequence [-++++--] contains three runs: [-], [+ + ++], and [--]. Noting N the number of observations, N A (resp.

N b ) the number of positive (negative) elements of X t , for N large (> 20), R the number of observed runs, given N A (N b ), is approximately normally distributed with

and

If there are many runs in excess or in shortage, we may reject the hypothesis of statistical independence. A small (large) number of runs indicates positive (negative) serial correlation.

, thus we must reject the null hypothesis of statistical randomness if |Z| > 1.96. In table 9, we consider the sign of X t = ∆Candidate -Φ, where Φ is either the mean or the median of the series, and ∆Candidate is the daily change in percentage of the price of the relevant "Winner-take-all" contract. For both series (∆Sarkozy and ∆Royal), no evidence indicates that we must reject the hypothesis of serial independence of variations of prices.

B.2 Unit-root tests

Weak efficiency test are generally associated with random walk tests. If "Winnertake-all" contracts price time series follow a logarithmic random walk, then the returns follow a white noise process.