Ilgam Khalilov

June Hirsch

Rosa Cossart

Yehezkel Ben-Ari

Paradoxical Anti-Epileptic Effects of a GluR5 Agonist of Kainate Receptors

Khalilov, Ilgam, June Hirsch, Rosa Cossart, and Yehezkel Ben-Ari. Paradoxical anti-epileptic effects of a GluR5 agonist of kainate receptors. J Neurophysiol 88: 523-527, 2002; 10.1152/jn.00838.2001. Kainate generates in adult hippocampal neurons a seizure but also a massive excitation of interneurons and a dramatic increase of the inhibitory drive that impinges on principal cells. This "overinhibition" is largely mediated by GluR5-containing kainate receptors that are enriched on interneurons. Here, using the neonatal intact hippocampus in vitro and the triple chamber, we first show that this mechanism is fully operative in neonatal neurons. We then report that application to one hippocampus of (RS)-2-amino-3-(5-tert-butyl-3-hydroxy-4-isoxazolyl)propionic acid-a relatively selective agonist of GluR5 containing kainate receptors-depresses the propagation of seizure generated in the opposite hippocampus by a convulsive agent. We conclude that the selective excitation of interneurons by GluR5-containing kainate receptor agonists opens a new therapeutic approach for the epilepsies.

I N T R O D U C T I O N

Systemic or intracerebral administration of kainate-an excitatory amino acid extracted from sea weeds-generates a seizure and brain-damage syndrome that mimics several central properties of human temporal lobe epilepsy (Ben-Ari 1985;[START_REF] Nadler Jv | Minireview: kainic acid as a tool for the study of temporal lobe epilepsy[END_REF]. Studies using kainate and kainate analogues in vivo and in slice preparations have shown that kainate generates seizures in the CA3 region-by far the most susceptible brain region to the adverse effect of kainate [START_REF] Gho M | Long-lasting modification of the synaptic properties of rat CA3 hippocampal neurones induced by kainic acid[END_REF][START_REF] Sa | Kainic acid produces depolarization of CA3 pyramidal cells in the vitro hippocampal slice[END_REF]. These events then propagate to the CA1 region and from there to other limbic structures leading to the occurrence of recurrent limbic seizures and a status epilepticus that will propagate to the rest of the cortical mantle [START_REF] Cossart R | Kainate, a double agent that generates seizures: two decades of progress[END_REF][START_REF] Gho M | Long-lasting modification of the synaptic properties of rat CA3 hippocampal neurones induced by kainic acid[END_REF][START_REF] Sa | Kainic acid produces depolarization of CA3 pyramidal cells in the vitro hippocampal slice[END_REF]. The mechanisms underlying these effects have been in part elucidated. Kainate activates high-affinity kainate receptors that are highly expressed on CA3 pyramidal neurons and their mossy fiber synapses [START_REF] Gaiarsa | Neonatal irradiation prevents the formation of hippocampal mossy fibers and the epileptic action of kainate on rat CA3 pyramidal neurons[END_REF][START_REF] Monaghan | The distribution of [3H]kainic acid binding sites in rat CNS as determined by autoradiography[END_REF][START_REF] Tremblay E | Autoradiographic localization of kainic acid binding sites in the human hippocampus[END_REF], leading to the generation of synchronized bursts via the recurrent collateral excitatory synapses that interconnect CA3 pyramidal neurons [START_REF] Rk | Excitatory synaptic interactions between CA3 neurons in the guinea pig hippocampus[END_REF][START_REF] Smith Kl | Diverse populations of neurons mediated by local circuit excitation in developing hippocampus[END_REF].

Kainate receptors are, however, also enriched on interneurons [START_REF] Bahn | Kainate receptor gene expression in the developing rat brain[END_REF][START_REF] Bureau | Kainate receptormediated responses in the CA1 field of wild-type and GluR6-deficient mice[END_REF][START_REF] Mulle | Altered synaptic physiology and reduced susceptibility to kainate-induced seizures in GluR6-deficient mice[END_REF][START_REF] Mulle | Subunit composition of kainate receptors in hippocampal interneurons[END_REF][START_REF] Petralia Rs | Histological and ultrastructural localization of the kainate receptor subunits, KA2 and GluR6/7, in the rat nervous system using selective antipeptide antibodies[END_REF]) and the activation of these receptors [START_REF] Cossart R | GluR5 kainate receptor activation in interneurons increases tonic inhibition of pyramidal cells[END_REF][START_REF] Frerking | Synaptic activation of kainate receptors on hippocampal interneurons[END_REF]) produces a massive excitation of interneurons and a dramatic increase of the tonic inhibitory drive that impinges on the principal cells. Because of the important role of GABAergic inhibition in preventing the generation of seizures, this action is somewhat paradoxical as it may exert an anti epileptic effect. The aim of the present study was therefore to examine the functional consequences of a selective activation of kainate receptors located on interneurons. We relied on the observation that GluR5-containing kainate receptors are enriched in interneurons [START_REF] Bahn | Kainate receptor gene expression in the developing rat brain[END_REF][START_REF] Bureau | Kainate receptormediated responses in the CA1 field of wild-type and GluR6-deficient mice[END_REF][START_REF] Mulle | Altered synaptic physiology and reduced susceptibility to kainate-induced seizures in GluR6-deficient mice[END_REF][START_REF] Mulle | Subunit composition of kainate receptors in hippocampal interneurons[END_REF][START_REF] Petralia Rs | Histological and ultrastructural localization of the kainate receptor subunits, KA2 and GluR6/7, in the rat nervous system using selective antipeptide antibodies[END_REF]) and that their activation by the relatively selective agonist (RS)-2-amino-3-(5-tert-butyl-3-hydroxy-4-isoxazolyl)propionic acid (ATPA) [START_REF] Vr | A hippocampal GluR5 kainate receptor regulating inhibitory synaptic transmission[END_REF]) excites interneurons and augments the tonic GABAergic inhibition that impinges on pyramidal neurons [START_REF] Cossart R | GluR5 kainate receptor activation in interneurons increases tonic inhibition of pyramidal cells[END_REF]. We have used the in vitro intact neonatal hippocampus (Khalilov et al. 1997b) and a triple chamber that enables the two hippocampi and their connecting commissures to be in three independent chambers (Khalilov et al. 1999a). In this chamber, it is possible to apply a convulsive agent to one hippocampus and test whether a putative anti-epileptic agent prevents the propagation of the seizure to the other hippocampus. This enables to avoid possible interferences between convulsive and anti-epileptic agents.

M E T H O D S

The intact preparation that we used as well as the triple chamber have been described elsewhere [START_REF] Khalilov I | A novel in vitro preparation: the intact hippocampal formation[END_REF][START_REF] Khalilov | Maturation of kainate-induced epileptiform activities in interconnected intact neonatal limbic structures in vitro[END_REF]. We used the intact hippocampal formations (IIHFs) of neonatal (P6-P7) Wistar rats that were placed into a conventional fully submerged chamber and perfused with ACSF at 30 -32°C at a rate of 8 -10 ml/min. Whole cell recordings were performed with patch electrodes with a resistance of 5-8 M⍀ when filled with solutions containing (in mM): 135 K-gluconate, 0.1 CaCl 2 , 2 MgCl 2 , 2 Na2ATP, 1 EGTA, and 10 HEPES, pH 7.25, ([ Cl Ϫ ]in ϭ 4.2 mM), pH 7.25, osmolarity, 280 mosm. Tungsten bipolar electrodes disposed in the stratum radiatum of CA3 area were used to evoke synaptic responses. All neurons were filled with dyes and reconstructed post hoc for identification.

Group measures are expressed as means Ϯ SE, error bars also indicate SE. Statistical significance of differences was assessed with the Students t-test, the level of significance was set at P Ͻ 0.05. Drugs Address for reprint requests: Y. Ben-Ari, Inmed U29 INSERM, 163, route de Luminy, 13273 Marseille Ce ´dex 09, France (E-mail:ben-ari@inmed. univ-mrs.fr).

The costs of publication of this article were defrayed in part by the payment of page charges. The article must therefore be hereby marked ''advertisement'' in accordance with 18 U.S.C. Section 1734 solely to indicate this fact.

RAPID COMMUNICATION

ATPA excites interneurons and inhibits pyramidal neurons in the neonatal hippocampus

In an earlier study, we had demonstrated that the activation of GluR5-containing kainate receptors increased GABAergic inhibition in adult hippocampal slices [START_REF] Cossart R | GluR5 kainate receptor activation in interneurons increases tonic inhibition of pyramidal cells[END_REF]. We thus first tested whether this effect is also valid in neonatal neurons. We used P6 -P7 intact preparations as the activation of GABAergic synapses generates at this age primarily a hyperpolarization [START_REF] Coradetti | Giant synaptic potentials in immature rat CA3 hippocampal neurones[END_REF]. Bath application of ATPA (1 M) produced opposite effects on cell excitability in simultaneously recorded CA1 interneurons and pyramidal neurons. In cell-attached recordings (Fig. 1, A andB), ATOA (1 M) increased the action potential discharges of interneurons and reduced that of pyramidal neurons. In whole cell record-ings at resting membrane potential, ATPA produced a hyperpolarization of pyramidal neurons (x ϭ 7.1 Ϯ 1.1 mV, n ϭ 10) in current-clamp conditions (Fig. 1C) and a dramatic increase of the frequency of spontaneous inhibitory postsynaptic currents (sIPSCs; x ϭ 1,250.4 Ϯ 201.2%, n ϭ 5). Therefore in neonatal neurons, the activation of GluR5 agonists induces an increase of the inhibitory drive via a depolarization of interneurons.

ATPA prevents the propagation of seizures from one hemisphere to the other

To determine the effects of ATPA on the propagation of epileptiform activities from one hemisphere to the other, field and patch-clamp recordings were made from both hemispheres. Bath application of high [K ϩ ] o (7 mM), bicuculline (3 M), or 4-AP (50 M) to one hippocampus generated recurrent spontaneous and evoked inter-ictal episodes (Fig. 2). These are mediated by glutamatergic excitatory postsynaptic currents and are inward at V m Ϫ45 mV(Fig. 2C). These events rapidly propagated to the contralateral hippocampus, (Fig. 2D, mean latency of 25.3 Ϯ 0.8 ms, n ϭ 24). Applications of ATPA (1 M) to the contralateral naı ¨ve hippocampus that did not receive the convulsive agent considerably reduced the propagation of seizures (Fig. 2C). Thus in most experiments (65% of the experiments, n ϭ 17), it produced a complete blockade of epileptiform events in the remaining experiments it reversibly decreased both the amplitude and duration of inter-ictal events (66.4 Ϯ 1.2 and 75 Ϯ 5.0% of the control value, respectively, n ϭ 6). During the application of ATPA, GABAergic currents were recorded in the contralateral hippocampus and glutamatergic ones in the treated hippocampus (Fig. 2C). On wash-out of ATPA, the seizures rapidly propagated to the opposite hippocampus (Fig. 2D). Bath applications of ATPA after the seizures had been generated in the contralateral hippocampus, similarly blocked the propagated seizures (not shown).

D I S C U S S I O N

We show that the activation of GluR5-containing kainate receptors by ATPA prevents the propagation of epileptiform events from one hemisphere to the other. Although the exact mechanisms underlying these effects have not been determined, the powerful excitation of interneurons and the dramatic increase of the tonic inhibition that it generates most likely play an important role. However, ATPA is not entirely specific for GluR5-containing receptors [START_REF] Paternain Av | GluR5 and GluR6 kainate receptor subunits coexist in hippocampal neurons and coassemble to form functional receptors[END_REF], and the present results are in disagreement with studies by Lerma and co-workers that suggest that kainate reduces inhibition in adult neurons (Ben-Ari andCossart, 2000, 2001;[START_REF] Lerma | Kainate receptors keep the excitement high[END_REF][START_REF] Lerma | Molecular physiology of kainate receptors[END_REF]. Also, the effects of ATPA on interneurons are reduced but not fully blocked by a selective KO of GluR5-containing receptors; a double KO of GluR5 and -6 is required to produce a full blockade of the actions of ATPA [START_REF] Mulle | Subunit composition of kainate receptors in hippocampal interneurons[END_REF]. Finally, several interneurons-in particular in stratum radiatum-are not excited by ATPA (Cossart et al.) suggesting that other mechanisms may be involved in the actions of kainate. In spite of this, our data are best explained by a direct excitation of interneurons and a reduction of the excitability in principal cells. Our observations should provide a novel approach to reduce the excitability of principal cells in a cortical network and possibly prevent seizure generation. The use of the triple chamber provides a unique opportunity to test these actions without the possible interferences between the convulsive and anti-epileptic actions of an agent.

Several features of the actions of ATPA, kainate-or other activators of kainate receptors located on interneurons-are particularly useful to consider in relation to its suggested anti-epileptic properties. First, the excitation of CA1 interneurons by these agents is specific because similar applications of kainate or ATPA do not excite CA1 pyramidal neurons [START_REF] Cossart R | GluR5 kainate receptor activation in interneurons increases tonic inhibition of pyramidal cells[END_REF]. Second, this effect is dramatic and persistent, it is associated with an 8-to 10-fold increase of the frequency of GABAergic IPSCs in pyramidal neurons that can persist for long durations [START_REF] Cossart R | GluR5 kainate receptor activation in interneurons increases tonic inhibition of pyramidal cells[END_REF]present study). Third, the FIG. 2. ATPA prevents the propagation of seizures from 1 hemisphere to the other. A: triple chamber preparation, recordings include both field and whole cell recordings from both hippocampi. B: application of bicuculline (2 M) to 1 hippocampus generated inter-ictal-like seizures (ILS) that propagated to the contralateral side. C: bicuculline-induced seizures failed to propagate to the contralateral hemisphere when ATPA (1 M) was present. D: washing out of ATPA enabled the propagation of seizures to the contralateral hippocampus. Bottom: the same data at a faster display. Quantification of the effects of ATPA is shown in E.

synaptic input activated by kainate receptors in interneurons is quite powerful as it readily generates action potentials and produces an important increase in the excitability of interneurons [START_REF] Cossart R | GluR5 kainate receptor activation in interneurons increases tonic inhibition of pyramidal cells[END_REF]present study). Nevertheless, it is important to stress that other actions of ATPA could contribute to the observed effects. Recent studies suggest that kainate receptor activation could also reduce glutamate release by a presynaptic mechanism [START_REF] Contractor | Identification of the kainate receptor subunits underlying modulation of excitatory synaptic transmission in the CA3 region of the hippocampus[END_REF][START_REF] Frerking | Kainate receptors depress excitatory synaptic transmission at CA3-ϾCA1 synapses in the hippocampus via a direct presynaptic action[END_REF]. Further studies are required to determine the contributions of these actions to the anti-epileptic actions of GluR5 agonists.

Our suggestion of paradoxical anti epileptic effects of a kainate receptor agonist is not incompatible with the epileptogenic effects of kainate. Kainate exerts a multitude of actions on different types of neurons and different channels. The result-the seizure-is the consequence of these diverse actions. Thus seizures are generated in the adult hippocampus primarily because of the activation of the mossy fiber synapses that are enriched with the GluR6-containing kainate receptors. Both the knock-out of the GluR6 genes [START_REF] Mulle | Altered synaptic physiology and reduced susceptibility to kainate-induced seizures in GluR6-deficient mice[END_REF]) and the selective lesion of the mossy fibers by neonatal irradiation prevent the effects of kainate. Also, GABAergic inhibition is not abolished in epileptic animals; there is rather a reduction of tonic inhibition restricted to the dendrites of pyramidal neurons-as a result of the degeneration of a subpopulation of interneurons during the initial status epilepticus. In contrast, tonic inhibition is increased in the somata of the principal cells raising the possibility of a paradoxical increase of inhibition in the epileptic circuit [START_REF] Cossart R | GluR5 kainate receptor activation in interneurons increases tonic inhibition of pyramidal cells[END_REF][START_REF] Cossart R | Dendritic but not somatic GABAergic inhibition is decreased in experimental epilepsy[END_REF]. As interneurons are capable of high-frequency discharge, we suggest that the activation by GluR5 agonists of surviving interneurons may in part replace the missing inhibitory drive. Preliminary experiments suggest that the actions of ATPA are preserved in neurons recorded in slices obtained from epileptic rats (Hirsch, unpublished observations).

Further studies are also required to determine the maturation of the actions of ATPA. Indeed early during development, GABA provides most of the excitatory drive because of a different chloride gradient [START_REF] Cossart R | Kainate, a double agent that generates seizures: two decades of progress[END_REF][START_REF] Coradetti | Giant synaptic potentials in immature rat CA3 hippocampal neurones[END_REF]). In our studies, ATPA prevented the propagation of seizures even when GABA generated a depolarization in the recorded neuron (not shown). This is best explained by the dual excitatory and shunting actions of GABA shown in neonatal hippocampal neurons (Khalilov et al. 1999a). Future studies will also have to compare the maturation of the epileptogenic actions of kainate (see Khalilov et al. 1999b) to the development of the effects of ATPA. Immuno-cytochemical data suggest that interneurons possess GluR5 mRNA already at birth [START_REF] Bahn | Kainate receptor gene expression in the developing rat brain[END_REF].

In conclusion, our results suggest that the activation of GluR5-containing kainate receptors can prevent the propagation of seizure from one hemisphere to the other. Kainate will generate seizure but at the same time augment the excitatory input to interneurons and thus lead to an increased inhibition. The observation that these actions may be mediated by different subunits will enable to develop selective drugs that predominantly act to reduce seizures. The use of the newly developed triple chamber provides a unique possibility to record from both hemispheres and determine the effects of various procedures and agents on the generation and propagation of activities from one hemisphere to the other.

  FIG. 1. (RS)-2-amino-3-(5-tert-butyl-3-hydroxy-4-isoxazolyl)propionic acid (ATPA) excites interneurones and inhibits pyramidal cells. A: paired recordings in the cell attached configuration from a P6 intact hippocampus in vitro. Note that ATPA produced a more than 40-fold increase of the frequency of action potentials in the interneuron and an almost full blockade of the discharge of the pyramidal neuron. B: electrical stimulation generated a barrage of action potentials in a pyramidal neuron. This was fully blocked by ATPA. C: paired recordings from 2 pyramidal neurons in whole cell configuration current clamp (top) and voltage clamp (bottom). Note that ATPA produced a hyperpolarization (top) and a massive increase of the frequency of the ongoing spontaneous inhibitory postsynaptic currents (sIPSCs; bottom). Quantitative data are presented in the right side of the figure.

  Sigma (bicuculline, kainate, biocytin), and Alamone (TTX). ATPA was kindly provided by Lilly (Lilly Research Center).

			J Neurophysiol
			88: 523-527, 2002; 10.1152/jn.00838.2001.
	used were purchased from Cookson-Tocris [6-cyano-7-nitroquinox-
	alene-2,3-dione (CNQX) and 2-amino-5-phosphonovaleric acid (D-
	APV)], R E S U L T S
			Downloaded from
			jn.physiology.org
			on May 19, 2010
	www.jn.org	0022-3077/02 $5.00 Copyright © 2002 The American Physiological Society	523

J Neurophysiol• VOL 88 • JULY 2002 • www.jn.org on May 19, 2010 jn.physiology.org Downloaded from

This work was supported by Institut National de la Sante ´et de la Recherche Me ´dicale, the French League against Epilepsy (LFCE), and a grant from the Foundation Electricity of France to I. Khalilov.

Present address of I. Khalilov: Kazan Institute of Biochemistry and Biophysics, Kazan, Russia.


J Julliand
email: julliand@lifc.univ-fcomte.fr

N Stouls

P.-C Bué

P.-A Masson
email: masson@lifc.univ-fcomte.fr

Syntactic Abstraction of B Models to Generate Tests

Keywords: Abstraction, Test Generation, (Bi-)Simulation, Slicing

In a model-based testing approach as well as for the verification of properties, B models provide an interesting solution. However, for industrial applications, the size of their state space often makes them hard to handle. To reduce the amount of states, an abstraction function can be used, often combining state variable elimination and domain abstractions of the remaining variables. This paper complements previous results, based on domain abstraction for test generation, by adding a preliminary syntactic abstraction phase, based on variable elimination. We define a syntactic transformation that suppresses some variables from a B event model, in addition to a method that chooses relevant variables according to a test purpose. We propose two methods to compute an abstraction A of an initial model M. The first one computes A as a simulation of M, and the second one computes A as a bisimulation of M. The abstraction process produces a finite state system. We apply this abstraction computation to a Model Based Testing process.

Introduction

B models are well suited for producing tests of an implementation by means of a model-based testing approach [START_REF]Model-Based Testing of Reactive Systems[END_REF][START_REF] Utting | Practical Model-Based Testing -A tools approach[END_REF] and to verify dynamic properties by modelchecking [START_REF] Leuschel | ProB: An automated analysis toolset for the B method[END_REF]. But model-checking as well as test generation require the models to be finite, and of tractable size. This is not usually the case with industrial applications, for which the exploration of the executions modelled frequently comes up against combinatorial explosion problems. Abstraction techniques allow for projecting the (possibly infinite or very large) state space of a system onto a small finite set of symbolic states. Abstract models make test generation or model-checking possible in practice [START_REF] Bouquet | Instantiation of parameterized data structures for model-based testing[END_REF]. In [START_REF] Bouquet | Test generation based on abstraction and test purposes to complement structural tests[END_REF], we have proposed and experimented with an approach of test generation from abstract models. It appeared that the computation time of the abstraction could be very expensive, as evidenced by the Demoney [START_REF] Marlet | Demoney: A demonstrative electronic purse[END_REF] case study. We had replaced a problem of time for searching in a state graph with a problem of time for solving proofs, as the abstraction was computed by proving enabledness and reachability conditions on symbolic states [START_REF] Bert | GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications[END_REF].

In this paper, we contribute to solving this proving time problem by defining a syntactic abstraction function that requires no proof. Inspired from slicing techniques [START_REF] Weiser | Program slicing. Software Engineering[END_REF], the function works by suppressing some state variables from a model. In order to produce a state system that is both finite and sufficiently small, we still have to perform a semantic abstraction. This requires that some proof obligations are solved, but there are less of them than with the initial model, since it has been syntactically simplified. This approach results in semantic pruning of generated proof obligations as proposed in [START_REF] Couchot | Graph-based Reduction of Program Verification Conditions[END_REF].

In Sec. 2, we introduce the notion of B event system and some of the main properties of substitution computation. Section 3 presents an Electrical System case study that illustrates our approach. In Sec. [START_REF] Bouquet | Instantiation of parameterized data structures for model-based testing[END_REF], we first define the set of variables to be preserved by the abstraction function and then we define the abstraction function itself. We prove that this function is correct in the sense that the generated abstract model A simulates or bisimulates the initial model M. In this way, the abstraction can be used to verify safety properties and to generate tests. In Sec. 5, we present an end to end process to compute test cases from a set of observed variables by using both the semantic and the syntactic abstractions. In Sec. 6, we compare this process to a completely semantic one on several examples, and we evaluate the practical interest for test cases generation. Section 7 concludes the paper, gives some future research directions and compares our approach to other abstraction methods.

B Event Systems and Refinement

We use the B notation [START_REF] Abrial | The B Book: Assigning Programs to Meanings[END_REF] to describe our models: this section gives the background required for reading the paper. Let us first define the following B notions: primitive forms of substitution, substitution properties and refinement. Then we will summarize the principles of before-after predicates, and conjunctive form (CF) of B predicates.

First introduced by J.-R. Abrial [START_REF] Abrial | Extending B without changing it (for developing distributed systems)[END_REF], a B event system defines a closed specification of a system by a set of events. In the sequel, we use the following notations: x, x i , y, z are variables and X, Y , Z are sets of variables. Pred is the set of B predicates. I (∈ Pred) is an invariant, and P , P 1 and P 2 (∈ Pred) denote other predicates. The modifications of the variables are called substitutions in B, following [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] where the semantics of an assignment is defined as a substitution. In B, substitutions are generalized : they are the semantics of every kind of action, as expressed by formulas 1 to 4 below. We use S, S 1 and S 2 to denote B generalized substitutions, and E, E i and F to denote B expressions. The B events are defined as generalized substitutions. All the substitutions allowed in B event systems can be rewritten by means of the five B primitive forms of substitutions of Def. 1. Notice that the multiple assignment can be generalized to n variables. It is commutative, i.e. x, y := E, F = y, x := F, E.

Definition 1 (Substitution). The following five substitutions are primitive:

single and multiple assignments, denoted as x := E and x, y := E, F substitution with no effect, denoted as skip guarded substitution, denoted as P ⇒ S bounded nondeterministic choice, denoted as S 1 []S 2 -substitution with local variable z, denoted as @z.S.

Notice that the substitution with local variable is mainly used to express the unbounded nondeterministic choice denoted by @z.(P ⇒ S). Let us specify that among the usual structures of specification languages, the conditional substitution IF P THEN S 1 ELSE S 2 END is denoted by (P ⇒ S 1 )[](¬P ⇒ S 2 ) with the primitive forms.

Given a substitution S and a post-condition P , it is possible to compute the weakest precondition such that if it is satisfied, then P is satisfied after the execution of S. The weakest precondition is denoted by [S]P . [x := E]P is the usual substitution of all the free occurrences of x in P by E. For the four other primitive forms, the weakest precondition is computed as indicated by formulas 1 to 4 below, proved in [START_REF] Abrial | The B Book: Assigning Programs to Meanings[END_REF].

[skip]P ⇔ P

(1)

[P1 ⇒ S]P2 ⇔ (P1 ⇒ [S]P2) (2) [S1[]S2]P ⇔ [S1]P ∧ [S2]P (3)
[@z.S]P ⇔ ∀z.

[S]P if z is not free in P (4)

Distributivity: [S](P1 ∧ P2) ⇔ [S]P1 ∧ [S]P2 (5)
Definition 2 defines correct B event systems. To explicitly refer to a given model, we add the name of that model as a subscript to the symbols X, I, Init and Ev. I M is for example the invariant of a model M.

Definition 2 (Correct B Event System).

A correct B event system is a tuple X, I, Init, Ev where:

-X is a set of state variables, -I (∈ Pred) is an invariant predicate over X, -Init is a substitution called initialization, such that the invariant holds in any initial state: [Init]I, -Ev is a set of event definitions in the shape of ev i = S i such that every event preserve the invariant:

I ⇒ [S i ]I.
In Sec. 4, we will prove that an abstraction A that we compute is refined by its source event system M, and so we give in Def. 3 the definition of a B event system refinement.

Definition 3 (B Event System Refinement).

Let A and R be two correct B event systems. Let I R be their gluing invariant, i.e. a predicate that indicates how the values of the variables in R and A relate to each other. R refines A if:

any initialization of R is associated to an initialization of A according to I R :

[Init R ]¬[Init A ]¬I R -any event ev = S R of R is an event of A defined by ev = S A in Ev A that satisfy I R : I A ∧ I R ⇒ [S R ]¬[S A ]¬I R .
This paper also relies on two more definitions: the before-after predicate and the CF form. We denote by P rd X (S) the before-after predicate of a substitution S. It defines the relation between the values of the variables of the set X before and after the substitution S. A primed variable denotes its after value. From [START_REF] Abrial | The B Book: Assigning Programs to Meanings[END_REF], the before-after predicate is defined by: Section 4 will define predicate transformation rules. We put the predicates in CF according to Def. 4 before their transformation. This allows the transformation to be correct although the negation is not monotonic w.r.t a transformation T of the predicates: T (¬P ) = ¬T (P ).

P rdX(S) = ¬[S]¬( x∈X (x = x ′ )). ( 6

Electrical System Example

We describe in this section a B event system that we will use in this paper as a running example to illustrate our proposal.

Fig. 1. Electrical System

A device D is powered by one of three batteries B 1 , B 2 , B 3 as shown in Fig. 1. A switch connects (or not) a battery B i to the device D. A clock H periodically sends a signal that causes a commutation of the switches, i.e. a change of the battery in charge of powering the device D. The working of the system must satisfy the three following requirements:

-Req 1 : no short-circuit, i.e. there is only one switch closed at a time, -Req 2 : continuous power supply, i.e. there is always one switch closed, -Req 3 : a signal from the clock always changes the switch that is closed.

The batteries are subject to electrical failures. If it occurs to the battery that is powering D, the system triggers an exceptional commutation to satisfy the requirement Req 2 . The broken batteries are replaced by a maintenance service. We assume that it works fast enough for not having more than two batteries down at the same time. When two batteries are down, the requirement Req 3 is relaxed and the clock signal leaves unchanged the switch that is closed.

This system is modeled in Fig. 2 by means of three variables. H models the clock and takes two values: tic when it asks for a commutation and tac when this commutation has occurred. Sw models the state of the three switches by an integer between 1 and 3: Sw = i indicates that the switch i is closed while the others are opened. This modelling makes that requirements Req 1 and Req 2 necessarily hold. Bat models the electrical failures by a total function. The ko value for a battery indicates that it is down. In addition to the typing of the variables, the invariant I expresses the assumption that at least one battery is not down by stating that Bat(Sw) = ok. Notice that the requirement Req 3 is a dynamic property, not formalized in I. The initial state is defined by Init in Fig. 2. The behavior of the system is described by four events:

-Tic sends a commutation command, -Com1 performs a commutation (i.e. changes the closed switch), -Fail simulates an electrical failure on one of the batteries, -Rep simulates a maintenance intervention replacing a down battery.

X = {H, Sw, Bat} I = H ∈ {tic, tac} ∧ Sw ∈ 1..3 ∧ (Bat ∈ 1..3 → {ok, ko}) ∧ Bat(Sw) = ok Init = H, Sw, Bat := tac, 1, {1 → ok, 2 → ok, 3 → ok} T ic = H = tac ⇒ H := tic Com = card(Bat⊲ {ok}) > 1 ∧ H = tic ⇒ @ns.(ns ∈ 1..3 ∧ Bat(ns) = ok ∧ ns = Sw ⇒ H, Sw := tac, ns) F ail = card(Bat ⊲ {ok}) > 1 ⇒ @nb.(nb ∈ 1..3 ∧ nb ∈ dom(Bat ⊲ {ok}) ⇒ (nb = Sw ⇒ @ns.(ns ∈ 1..3 ∧ ns = Sw ∧ Bat(ns) = ok ⇒ Sw, Bat(nb) := ns, ko)) [](nb = Sw ⇒ Bat(nb) := ko)) Rep = @nb.(nb ∈ 1..3 ∧ nb ∈ dom(Bat ⊲ {ko}) ⇒ Bat(nb) := ok)

Fig. 2. B Specification of the Electrical System

Syntactic Abstraction

We define in this paper a syntactical abstraction method that applies to B models. Similar rules could be adapted for more generic formalisms such as pre-post models or transition systems.

Our intention is to obtain an abstract model A of a model M by observing only a subset X A of the state variables X M of M. For instance, to test the electrical system in the particular cases where two batteries are down, we observe only the variable Bat. But to preserve the behaviors of M related to the variables of X A , we also keep in A the variables used to assign the observed variables or to define the conditions under which they are assigned.

We first present two methods to compute a set of abstract variables according to a set of observed variables. Using these variables we define a predicate and substitution transformation function. Then we describe how to compute an abstraction of a B event model M. The abstraction is a bisimulation of M when the abstract variables were computed according to the second method. We also prove that if they were computed according to the first method, the abstraction is a simulation of M.

Choosing the Abstract Variables

As proposed in [START_REF] Brückner | Slicing an Integrated Formal Method for Verification[END_REF], we distinguish between the observed variables and the abstract ones. A set X A of abstract variables is the union of a set of observed variables with a set of relevant variables. The Observed variables are the ones used by the tester in a test purpose, while the relevant variables are the ones used to describe the evolutions of the observed variables. More precisely, the relevant variables are the ones used to assign an observed variable (data-flow dependency), augmented with the variables used to express when such an assignment occurs (control-flow dependency).

A naive method to define X A is to syntactically collect the variables that are either on the right side or in the guard of the assignment of an observed variable. But this method will in most cases select a very large amount of variables, mainly because of the guard. For instance, if x is the observed variable, then y is not relevant in (y ⇒ x, z := E, F )[](¬y ⇒ x := E). A similar weakness goes for the unbounded non-deterministic choice @z.(P ⇒ S).

Hence our contribution consists of two methods for identifying the relevant variables. The first one only considers the data-flow dependency. It is efficient, but may select a set too small of relevant variables, resulting in a set with too many behaviors in the abstracted model. The second one uses both data and control flow dependencies, but requires a predicate simplification to restrict the size of X A . It produces abstract models that have the same set of behaviors as the original model, w.r.t. the abstract variables. This second method may select a set with too many relevant variables because predicate simplification is an undecidable problem.

Proposition 1: Data-Flow Dependency Only This first method considers as relevant only the variables that appear on the right side of an assignment symbol to an abstract variable. Starting from the set of observed variables, the set of all abstract variables is computed as the least fix-point when adding the relevant variables. For instance, the set of relevant variables of the electrical system is empty if the set of observed variables is {Bat}. Hence if a test purpose is only based on Bat, then X A = {Bat}. A drawback of this method is that it can introduce in A new execution traces w.r.t. M. Indeed, it may weaken the guards of some of the events, that would thus become enabled more often.

Proposition 2: Data-Flow and Control-Flow Dependencies This second method first computes a predicate characterizing a condition under which an abstract variable is modified, then simplifies it, and finally considers all its free variables as relevant. We express by means of formula 7 the modifications really performed by a substitution S on a set X A :

M odX A (S) = P rdX A (S) ∧ ( x∈X A x = x ′ ). ( 7
)
Our intention is that the predicate, that defines the condition under which an abstract variable is modified, only involves the variables really required to modify it. Hence primed variables are not quantified, but are allowed to be free. For instance, consider X A = {x} and the substitution x

:= y[](z > 0 ⇒ x := w)[]v := 3.
The predicate has to be in the shape of:

x ′ = y ∨ (z > 0 ∧ x ′ = w)
, where the variables y, w and z are relevant whereas v is not.

The M od X A predicate can also be defined by induction on the primitive substitutions, as described in appendix A.

Finally, X A is computed as a least fix-point, by iteratively incrementing for each event the initial set of observed variables with the relevant variables. This process terminates since the set of variables is finite. For instance, M od {Bat} gives an empty set of relevant variables when applied to the example, as shown in Fig. 3, while M od {H} gives X A = {Bat, H}.

Mod {Bat} (Init) ⇔ Bat = {1 → ok, 2 → ok, 3 → ok} Mod {Bat} (T ic) ⇔ f alse (no assignment of Bat) Mod {Bat} (Com) ⇔ f alse (no assignment of Bat) Mod {Bat} (F ail) ⇔ card(Bat ⊲ {ok}) > 1 ∧∃nb.(nb ∈ 1..3 ∧ nb ∈ dom(Bat ⊲ {ok}) ∧ Bat ′ (nb) = ko) Mod {Bat} (Rep) ⇔ ∃nb.(nb ∈ 1..3 ∧ nb ∈ dom(Bat ⊲ {ko}) ∧ Bat ′ (nb) = ok)

Predicate Transformation

Once the set of abstract variables X A (⊆ X M ) is defined, we have to describe how to abstract a model according to X A . We first define the transformation function T X A (P ) that abstracts a predicate P according to X A . We define T X on predicates in the conjunctive form (see Def. 4) by induction with the rules given in Fig. 4.

An elementary predicate is left unchanged when all the variables used in the predicate are considered in the abstraction (see the rule R 1 ). Otherwise, when an expression depends on some variables not kept in the abstraction, an elementary predicate is undetermined (see the rule R 2 ). As we want to weaken the predicate, we replace an undetermined elementary predicate by true. Consequently, a predicate P 1 ∧ P 2 is transformed into P 1 when P 2 is undetermined, and a predicate P 1 ∨ P 2 is transformed into true when P 1 or P 2 is undetermined (see the rules R 3 and R 4 ). Finally, the transformation of a quantified predicate is the transformation of its body w.r.t. the observed variables, augmented with the quantified variable (see the rule R 5 ).

TX (E(Y ) r E(Z)) = E(Y ) r E(Z) if Y ⊆ X and Z ⊆ X (R1) TX (E(Y ) r E(Z)) = true if Y ⊆ X or Z ⊆ X (R2) TX (P1 ∨ P2) = TX (P1) ∨ TX (P2) (R3) TX (P1 ∧ P2) = TX (P1) ∧ TX (P2) (R4) TX (αz.P ) = αz.T X∪{z} (P ) (R5)
Fig. 4. CF Predicate Transformation Rules For example the invariant I of the electrical system is transformed, according to the single variable Bat, into T {Bat} (I) = Bat ∈ 1..3 → {ok, ko} as in Fig. 5. Proof. As we said before, T X (P ) is weaker than P . Indeed, for any predicate P in CF there exist p 1 and p 2 such that P = p 1 ∧ p 2 and such that it is transformed either into p 1 ∧ p 2 , or into p 1 , or into p 2 , or into true, by application of the transformation rules R i . For any disjunctive predicate P there exist p 1 and p 2 such that P = p 1 ∨ p 2 and p 1 ∨ p 2 is transformed either into p 1 ∨ p 2 or into true.

T {Bat} (H ∈ {tic, tac} ∧ Sw ∈ 1..3 ∧ Bat ∈ 1..3 → {ok, ko} ∧ Bat(Sw) = ok) = T {Bat} (H ∈ {tic, tac}) ∧ T {Bat} (Sw ∈ 1..3) ∧ T {Bat} (Bat ∈ 1..3 → {ok, ko}) ∧ T {Bat} (Bat(Sw) = ok) applying R4 = Bat ∈ 1..3 → {ok, ko} applying

Substitution Transformation

The abstraction of substitutions is defined through cases in Fig. 6 on the primitive forms of substitutions. Intuitively, any assignment x := E is preserved into the transformed model if and only if x is an abstract variable. According to both of the two methods described in sec. 4.1, if x is an abstract variable, then so are all the variables in E. Therefore, in rules R 6 to R 11 , we do not transform the expressions E and F . A substitution is abstracted by skip when it does not modify any variable from X (see rules R 6 , R 8 , R 9 and R 10 in which y := F is abstracted by skip).

The assignment of a variable x is left unchanged if x is an abstract variable (see rules R 7 , R 10 , R 11 ). The transformation of a guarded substitution S is such that T X (S) is enabled at least as often as S, since T X (P ) is weaker than P from Prop. 1 (see rule R 12 ). The bounded non deterministic choice S 1 [] S 2 becomes a bounded non deterministic choice between the abstraction of S 1 and S 2 (see rule R 13 ). The quantified substitution is transformed by inserting the bound variable into the set of abstract variables (see rule R 14 ).

TX (x := E) = skip if x / ∈ X (R6) TX (x := E) = x := E if x ∈ X (R7) TX (skip) = skip (R8) TX (x, y := E, F ) = skip if x / ∈ X and y / ∈ X (R9) TX (x, y := E, F ) = x := E if x ∈ X and y / ∈ X (R10) TX (x, y := E, F ) = x, y := E, F if x ∈ X and y ∈ X (R11)
TX (P ⇒ S) = TX (P ) ⇒ TX (S) (R12)

TX (S1[]S2) = TX (S1)[]TX (S2) (R13)
TX (@z.S) = @z.T X∪{z} (S) (R14) Fig. 6. Primitive Substitution Transformation Rules

B Event System Transformation

According to the predicate and substitution transformation functions (see figure 4 and figure 6), we define the transformation of a B event model according to a set of abstract variables (section 4.1) in Def. 5. This transformation translates a correct model M into a model A that simulates M (Sec. 4.5). The electrical system is transformed as shown in Fig. 7 for the set of abstract variables {Bat}.

Definition 5 (B Event System Transformation). Let X A be a set of abstract variables, defined as in Sec. 4.1 from a set of observed variables X with X ⊆ X M . A correct B event system M = X M , I M , Init M , Ev M is abstracted as the B event system A = X A , I A , Init A , Ev A as follows:

-X A ⊆ X M , the set of abstract variables is a subset of the state variables, -

I A = T X A (I M ), the invariant is transformed, -Init A = T X A (Init M ), the initialization is transformed, -to each event ev = S M in Ev M is associated ev = T X A (S M ) in Ev A .

Correctness

When the set of abstract variables X A preserve both the data and control flows as defined in Sec. 4.1 (Proposition 2), the transition relation, restricted to X A , is preserved, as proved (see appendix C) by theorem 1. A and M have an equivalent before-after relation P rd X A , therefore they are bisimilar. Hence when a CTL* property is verified on A it holds on M and test cases generated from A can always be instantiated on M.

Theorem 1. Let S be a substitution. Let X be a set of abstract variables composed of any free variable of M od X (S), we have P rd X (S) ⇔ P rd X (T X (S)).

With the method defined in Sec. 4.1 by Proposition 1, A is a simulation of M. The B refinement relation (see Def. 3) is proven in [START_REF] Bellegarde | Ready-simulation is not ready to express a modular refinement relation[END_REF] to be a simulation: A simulates M by a τ -simulation. τ is a silent action corresponding in our case to an event reduced to skip or to P ⇒ skip. Theorems 2 and 3 establish that M refines A, and thus that A simulates M. The safety properties are preserved, but some tests generated from A might be impossible to instantiate on M. Theorem 2. Let I be a CF invariant of a correct B event system, let S be a substitution and let X be a set of abstract variables. The transformation rules R 6 to R 14 are such that S refines T X according to the invariant I. Theorem 3. Let X be a set of abstract variables defined as in Proposition 1. Let T X be the transformation defined in Fig. 6, and let A be an abstraction of an event system M defined according to Def. 5. A is refined by M in the sense of Def. 3.

Theorem 2 establishes that any substitution S refines its transformation T X (S) for a given set of abstract variables X. The proof is given in Appendix B. Theorem 3 establishes that a B event system M refines the B abstract system obtained according to Def. 5 by applying to M the transformation rules of Fig. 4 and Fig. 6.

Proof (of theorem 3)

. This is a direct consequence of theorem 2 and Def. 5 since the substitution Init A = T X (Init M ) is refined by Init M , and that for any event ev = S M , the substitution S A = T X (S M ) is refined by S M .

X = {Bat} I = Bat ∈ 1..3 → {ok, ko} Init = Bat := {1 → ok, 2 → ok, 3 → ok} T ic = skip Com = card(Bat ⊲ {ok}) > 1 ⇒ @ns.(ns ∈ 1..3 ∧ Bat(ns) = ok ⇒ skip) F ail = card(Bat ⊲ {ok}) > 1 ⇒ @nb.(nb ∈ 1..3 ∧ nb ∈ dom(Bat ⊲ {ok}) ⇒ Bat(nb) := ko) Rep = @nb.(nb ∈ 1..3 ∧ nb ∈ dom(Bat ⊲ {ko}) ⇒ Bat(nb) := ok)

Application of the Method to a Testing Process

We show in this section how to use the syntactic abstraction in a model-based testing approach.

Test Generation from an Abstraction

We have described in [START_REF] Bouquet | Test generation based on abstraction and test purposes to complement structural tests[END_REF] a model-based testing process using an abstraction as input. It can be summarized as follows. A validation engineer describes by means of a handwritten test purpose TP how he intends to test the system, according to his know-how. We have proposed in [START_REF] Julliand | Generating security tests in addition to functional tests[END_REF] a language based on regular expressions, to describe a TP as a sequence of actions to fire and states to reach (targeted by these actions). The actions can be explicitly called in the shape of event names, or left unspecified by the use of a generic name. The unspecified calls then have to be replaced with explicit event names. However, a combinatorial explosion problem occurs, when searching in a concrete model for the possible replacements that lead to the target states. This leads us to use abstractions instead of concrete models. Figure 8 shows our approach.

Fig. 8. Generating Tests from Test Purpose by Abstraction

We perform a synchronized product between an abstraction A and the automaton of a TP. This results in a model SP whose executions are the executions of A that match the TP. An implementation [START_REF] Thimbleby | The directed chinese postman problem[END_REF] of the Chinese Postman algorithm is applied to SP to cover its transitions. The result is a set of abstract symbolic tests AST. These tests are instantiated from M as a set IT of instantiated tests.

Abstraction Computation

We show in this section two ways of producing an abstraction A that can be used as an input of the process of Fig. 8. The syntactic abstraction of Sec. 4 is used in one of these two ways.

In order to compute the synchronized product of an abstraction A with the automaton of a TP, we compute the semantics of A as a labelled transition system. We use GeneSyst [START_REF] Bert | GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications[END_REF] for that purpose. This tool computes a semantic abstraction of a B model in the shape of a symbolic labelled transition system. The semantic abstraction relies on feasibility proofs of the transitions between two symbolic states. GeneSyst generates proof obligations (POs) for each of the potential transitions between two symbolic states, and tries to solve them automatically.

The two main drawbacks of this process are its time cost and the proportion of POs not automatically solved. Indeed, each unsolved PO results in a transition that is kept in the symbolic labelled transition system, although it is possibly unfeasible. An abstract symbolic test going through such a transition may be impossible to instantiate from the concrete model M. By applying a preliminary phase of syntactic abstraction, we reduce the impact of that problem by reducing the number and the size of the POs, since GeneSyst operates on an already abstracted model. For example, no proof obligation is generated for an event reduced to skip (it becomes a reflexive transition on any symbolic state).

Fig. 9. Abstraction Process

The experimental results presented in Sec. 6 compare two approaches. The first one (see Fig. 9/Process 1) is only semantic, while the second one (see Fig. 9/Process 2) combines a syntactic and a semantic abstraction.

Experimental Results

We have applied our method to four case studies. They are various cases of reactive systems: an automatic conveying system (Robot [START_REF] Bouquet | Génération de tests à partir de critères dynamiques de sélection et par abstraction[END_REF]), a reverse phone book service (Qui-Donc [START_REF] Utting | Practical Model-Based Testing -A tools approach[END_REF]), the electrical system2 (Electr.) and an electronic purse (DeMoney [START_REF] Marlet | Demoney: A demonstrative electronic purse[END_REF]). Each one is abstracted w.r.t. two sets of abstract variables. These sets have been computed according to Proposition 1 of Sec. 4.1. We also have tried to compute the abstract variables according to Proposition 2, but all the variables have been computed as abstract in three case studies. Only for the electrical system the set of abstract variables was the same as with Proposition 1. These case studies reveal a limit in the application of Proposition 2.

In Sec. 6.1 we present an experimental evaluation of the syntactic abstraction. Then, in Sec. 6.2 we compare A M with A A respectively computed by the semantic abstraction process or by its combination with the syntactic one.

Impact of the Syntactic Abstraction on Models

Table 1 indicates the size of the case studies and the syntactically abstracted models. The Symbols "♯", "Ev.", "Var." and "Pot." respectively stand for number of, Events, Variables and Potential. For example the Robot, defined by 9 events and 6 variables is abstracted w.r.t. two sets of respectively 3 and 4 abstract variables. Table 1. Size of the Case Studies and of their Syntactical Abstractions A direct observable result of the syntactic abstraction is a reduction of the number of potential states of the model. Also notice that the simplification reduces from 10% up to 50% the number of lines of the model. 2 compares the abstractions computed either directly from the behavioral models (see process 1 in Fig. 9), or from their syntactic abstractions (see process 2 in Fig. 9). The abbreviations "Trans.", "Unau.", "Inst." and "Cover." stand respectively for transitions, unauthorized, instantiated and coverage.

Comparison of the Abstraction Processes 1 and 2

We see on our examples that there is between 1.8 and 2.3 fewer POs to compute with process 2 than with process 1, except for the Qui-Donc. The semantic abstraction computation in process 2 takes from twice up to five times less time than in process 1, where no previous syntactic abstraction have been performed. For the Qui-Donc, the syntactical abstraction has too much over-approximated the initial model, which explains the augmentation of the POs w.r.t. the process 1. Finally, there are four cases out of eight where the abstraction A A is more precise than A M in the sense that it has less transitions, due to the reduction of the number of unproved POs. In these four cases, the set of traces of A A is included in the set of traces of A M . In the case of the electrical system, the set of traces are equal. In the Qui-Donc case, the traces cannot be compared. The simplification by the syntactic abstraction of the events and of the invariant makes that A A may contain more transitions (thus more traces) than A M . But the number and the difficulty of the POs is greater to get A M than to get A A , so that proof failures may occur more often with A M . As a result, A M can also contain transitions that are not in A A .

As for the ratios of tests instantiated and of transitions covered of the abstraction, we observe their stability with or without syntactic abstraction. Although the ratios are a bit better (or equal) for the Robot and the Electrical System, and a bit worse for Qui-Donc and Demoney, they are mainly very close to each other. But, due to the reduction of the number of POs, the time to obtain these comparable results is improved with process 2, i.e. when there is a preliminary syntactic abstraction phase. Again, this is not true for the Qui-Donc since on the contrary, its number of POs has increased.

Finally, the method had no interest with the Qui-Donc, which was the smallest example. But, as shown by DeMoney, its efficiency in terms of gain of the abstraction computation time, of reduction of the number of unproved POs and of precision of the abstraction, grows with the size of the examples.

Conclusion, Related Works and Further works

We have presented in the B framework a method for abstracting an event system by elimination of some state variables. In this context, we have proposed two methods to compute the set of variables kept in the abstraction according to the set of observed variables. We have proved that when using the first method, the generated abstraction simulates the concrete model, while when using the second method, the generated abstraction bi-simulates the concrete model. This is useful for verifying safety properties and generating tests.

In the context of test generation, our method consists in initializing the test generation process from event B model described in [START_REF] Bouquet | Test generation based on abstraction and test purposes to complement structural tests[END_REF], by a syntactic abstraction. Since the syntactic abstraction reduces the size of the model, the main advantage of this method is that it reduces the set of uninstantiable tests, by reducing the level of abstraction (reduces the number of PO generated and facilitates the proof of the remaining PO). Moreover, this results in a gain of computation time. We believe that the bigger the ratio of the number of state variables to the number of observed variables is, the bigger the gain is. This conjecture needs to be confirmed by experiments on industrial size applications.

Many other works define model abstraction methods to verify properties or to generate tests. The method of [START_REF] Friedman | Projected state machine coverage for software testing[END_REF] uses an extension of the model-checker Murφ to compute tests from projected state coverage criteria that eliminate some state variables and project others on abstract domains. In [START_REF] Dick | Automating the generation and sequencing of test cases from model-based specifications[END_REF], an abstraction is computed by partition analysis of a state-based specification, based on the pre and post conditions of the operations. Constraint solving techniques are used. The methods of [START_REF] Graf | Construction of abstract state graphs with PVS[END_REF][START_REF] Bensalem | Computing abstractions of infinite state systems compositionally and automatically[END_REF][START_REF] Colon | Generating finite-state abstractions of reactive systems using decision procedures[END_REF] use theorem proving to compute the abstract model, which is defined over boolean variables that correspond to a set of a priori fixed predicates. In contrast, our method first introduces a syntactical abstraction computation from a set of observed variables, and further abstracts it by theorem proving. [START_REF] Chan | Combining Constraint Solving and Symbolic Model Checking for a Class of Systems with Non-Linear Constraints[END_REF] also performs a syntactic transformation, but requires the use of a constraint solver during a model checking process.

Other automatic abstraction methods [START_REF] Clarke | Model Checking and Abstraction[END_REF] are limited to finite state systems. The deductive model checking algorithm of [START_REF] Sipma | Deductive model checking[END_REF] produces an abstraction w.r.t. a LTL property by an iterative refinement process that requires human expertise. Our method can handle infinite state space specifications. The paper [START_REF] Namjoshi | Syntactic program transformations for automatic abstraction[END_REF] presents a syntactic abstraction method for guarded command programs based on assignment substitution. The method is sound and complete for programs without unbounded non determinism. However, the method is iterative and does not terminate in the general case. It requires the user to give an upper-bound of the number of iterations. The paper also presents an extension for unbounded non deterministic programs that is sound but not complete, due to an exponential number of predicates generated at each iteration step. In contrast, our syntactic method is iterative on the syntactic structure of the specifications. It is sound but not complete. It handles unbounded non deterministic specifications with no need for other iterative process and always terminates. Above all, our method does not compute any weakest precondition whereas the approach in [START_REF] Namjoshi | Syntactic program transformations for automatic abstraction[END_REF] does, which possibly introduces infinitely many new predicates.

The syntactic method that we have presented is correct, but, in the case of Proposition 1, may sometimes produce inaccurate over-approximations due to a too strong abstraction (see for example the experiments on the Qui-Donc). Proposition 2 produces a bisimulation, but may leave the initial model unchanged, i.e. not abstracted, if all the variables are computed as abstract. We have to find a compromise between the two propositions, that would reduce the number of abstract variables, but that would keep at least partially the control structure of the operations. Also, we think that rules could be improved to get a finer approximation. For instance, improving the rules is possible when the invariant contains an equivalence such as x = c ⇔ y = c ′ . If y is an eliminated variable and x an observed one, we could substitute all the occurrences of the elementary predicate y = c ′ with x = c. This would preserve the property in the syntactic abstraction A A , so that the following semantic abstraction would be more accurate. Such rules should prevent the addition of transitions in the Qui-Donc abstraction A A w.r.t. A M .

We think that extending the test generation method introduced in [5] by using a combination of syntactic and semantic abstractions will improve the method, since the abstraction is more accurate if there are less unproved POs.

A Inductive Definition of M od X

The M od X predicate can be defined by induction through primitive substitutions, as described in Table 3. Intuitively, an assignment x := E is associated to f alse if and only if x is not in X or x already has the same value as E. Other assignment cases are just some generalizations. This implements the data-flow dependency. For control flow dependency, a non-deterministic choice is an union between control-flow branches, thus a disjunction between predicates, and a guarded substitution P ⇒ S is associated to the whole condition P augmented with the result of the analysis of S. Once this predicate is expressed, it needs to be logically simplified. Table 3. M od X (S) Predicate Defined through Primitive Substitutions Property 2. M od X (S) defined in Table 3 satisfy the definition in formula [START_REF] Bert | GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications[END_REF].

Proof (of property 2). For any case of S, we prove that M od X (S) defined as in Formula (7) replacing P rd X (S) by its definition given in formula [START_REF] Marlet | Demoney: A demonstrative electronic purse[END_REF] and transformed by the formulas (1) to ( 4) is equal to its value in Table 3.

B Proof of Theorem 2

Proof. The refinement theory as defined in B [START_REF] Abrial | The B Book: Assigning Programs to Meanings[END_REF], requires that variable sets from abstraction and variable sets from refinement are disjoint. If a variable x is preserved through the refinement process, then it has to be renamed, i.e.

x renamed , and associated by a gluing invariant, i.e. x = x renamed . In order to prove the correctness of the refinement, we introduce the Ren() function, which renames every variable from a substitution or a predicate. Hence, the invariant I A abstracted from I M and the substitution S A abstracted from any S M are defined as follows: To prove that S M is a correct refinement of S A , we need to prove (Def. 3):

P C A ∧ P C M ∧ I A ∧ I M ∧ I G ⇒ [S M ]¬[S A ]¬(I M ∧ I G ) (R15)

Fig. 3 .

 3 Fig. 3. M od {Bat} Computation Applied to the Example

R1 and R2 Fig. 5 .

 R25 Fig. 5. Example of Predicate Transformation

Fig. 7 .

 7 Fig. 7. B Syntactically Abstracted Specification of the Electrical System

  ModX (x := E) = f alse x / ∈ X ModX (x := E) = x ′ = E ∧ z∈X-{x} (z ′ = z) ∧ x = x ′ x ∈ X ModX (x, y := E, F ) = f alse x / ∈ X ∧ y / ∈ X ModX (x, y := E, F ) = x ′ = E ∧ z∈X-{x} (z ′ = z) ∧ x = x ′ x ∈ X ∧ y / ∈ X ModX (x, y := E, F ) = x ′ = E ∧ y ′ = F ∧ z∈X-{x,y} (z ′ = z) ∧ z∈{x,y} (z = z ′ ) x ∈ X ∧ y ∈ X ModX (skip) = f alse ModX (P ⇒ S) = P ∧ ModX (S) ModX (S1 [] S2) = ModX (S1) ∨ ModX (S2) ModX (@z • S) = ∃(z, z ′ ) • Mod X∪{z} (S)

I

  A = Ren(TX(I M )) S A = Ren(TX(S M ))

)

  Definition 4 (Conjunctive Form). A B predicate P ∈ Pred is in CF when it is a conjunction p 1 ∧ p 2 ∧ . . . ∧ p n where every p i is a disjunction p 1

	i ∨ p 2 i ∨ . . . ∨ p m i i is an elementary predicate in one of the following two forms: such that any p j
	-E(Y ) r F (Z), where E(Y ) and F (Z) are B expressions on the sets of vari-
	ables Y and Z and r is a relational operator,
	-∀z.P or ∃z.P , where P is a B predicate in CF.

  Case Study ♯Ev.Model M Syntactically abstracted model A ♯Var. ♯B lines ♯Pot. states ♯Var. ♯B lines ♯Pot. states ♯Symb. states

	Robot	9	6	100	384	3 4	90 90	48 144	6 8
	QuiDonc	4	3	170	13	2 2	160 160	16 16	5 6
	Electr.	4	3	100	36	1 1	50 40	5 2	2 2
	DeMoney	11	9	330	10 30	1 2	140 180	65536 7	3 4

Table 2 .

 2 Comparison of the semantic and syntactic/semantic abstraction processes

	Case study ♯Trans. Robot 42 51	Process 1 : A M ♯Unau. ♯PO Time ♯Inst./ Trans. Cover. ♯Trans. Trans. (s) ♯Tests. of A M 5 263 64 4/11 29/37 (78%) 36 0 402 76 4/23 35/51 (68%) 50	Process 2 : A A ♯Unau. ♯PO Time ♯Inst./ Trans. Cover. inclusion Traces Trans. (s) ♯Tests. of A A 0 143 35 7/11 31/36 (86%) A A ⊂ A M 0 242 49 8/23 38/50 (76%) A A ⊂ A M
	Qui-	20	2	71	19	9/11	12/18 (66%)	25	7	89	21	6/11	11/18 (61%) A A	A M
	Donc	25	2	89	21	4/10	6/23 (26%)	29	6	103	23	4/10	6/23 (26%) A A	A M
	Electr. De-Money	13 7 38 53	5 0 5 0	26 21 116 290	7 5 189 17/18 25/33 (76%) 2/2 8/8 (100%) 3/3 7/7 (100%) 172 22/38 30/53 (56%)	13 7 38 50	5 0 5 0	16 9 68 130	5 2 38 65	2/2 3/3 17/18 25/33 (76%) A A ⊂ A M 8/8 (100%) A A = A M 7/7 (100%) A A = A M 20/35 26/50 (52%) A A ⊂ A M

Table

An expression r ⊲ E denotes a relation where the range is restricted by the set E. For example, {1 → ok,

→ ko,

→ ok} ⊲ {ok} = {1 → ok, 3 → ok}.

The 100 lines length of the model, in Table1, refer to a "verbose" version of the model, much more readable than our version of Fig.2.

where I G is the gluing invariant I G = xi∈X (x i = Ren(x i )). In order to prove formula (R 15 ), it is sufficient to establish that the following two formulas hold:

Since free variable sets from I A and I M are strictly disjoint, (R 16 ) can be rewritten as:

that holds, since the initial model M is correct. Hence, we only have to establish (R 17 ) to prove Theorem 2. The proof is by induction on the five primitive forms of substitutions. We make a case analysis for each rule in Fig. 6. We use Prop. 1 of Sec. 4.2 and axioms (1 to 5) defined in Sec. 2. We denote by Hyps the repetitive predicate

Rules R9 to R11 proofs are similar to the first case.

This formula is valid because the two induction hypotheses are valid:

[Ren(T X∪{z} (S))]¬I G -applying (4) It is valid since the following formula is implied by the induction hypothesis:

Hence, Theorem 2 holds.

C P rd X (M ) = P rd X (T X (M )) ?

Let S be a substitution. Let X be a set of abstract variables composed of any free variable of M od X (S) (see Proposition 2 in Sec. 4.1). We propose to prove that the following formula holds: P rd X (S) ⇔ P rd X (T X (S)).

Since P rd X (S) = ¬[S]¬ x∈X x = x ′ (see formula [START_REF] Marlet | Demoney: A demonstrative electronic purse[END_REF] in Sec. 2), we verify it by induction through primitive substitutions proving that [S]P ⇔ [T X (S)]P holds when P is defined only in terms of abstract variables in X.

Let [T X (S)]P ⇔ [S]P be the induction hypothesis: Notice that the hypothesis when P is defined only in terms of abstract variables X induces that [x := E]P = P when x / ∈ X because there is no occurrence of x in P .

We can then conclude that the set of behaviors on the set of abstract variables X of an event ev is unchanged when we simplify it by T X .


Anne-Laure Basdevant

Arvind Singh

Continuous time vertex reinforced jump processes on Galton-Watson trees

Keywords: Reinforced processes, phase transition, random walks on trees, branching processes A.M.S. Classification. 60G50, 60J80, 60J75

 by providing a characterization for the recurrence/transience of the walk.

Introduction

The model of the continuous time vertex reinforced jump process (VRJP) introduced by Davis and Volkov [START_REF] Davis | Continuous time vertex-reinforced jump processes[END_REF] may be described in the following way: let G be a locally finite graph and pick c > 0. Call VRJP(c) a continuous time process (X(t), t ≥ 0) on the vertices of G, starting at time 0 at some vertex v 0 ∈ G and such that, if X is at a vertex v ∈ G at time t, then, conditionally on (X(s), s ≤ t), the process X jumps to a neighbour u of v with rate:

L c (t, u) def = c + t 0 1 {X(s)=u} ds. (1)
Equivalently, the walk stays at site v an exponential time of parameter u∼v L c (t, u) and then jumps to a neighbour u with a probability proportional to L c (t, u).

The case G = Z was investigated by Davis and Volkov [START_REF] Davis | Continuous time vertex-reinforced jump processes[END_REF] who proved that, for any c > 0, the VRJP(c) is recurrent and the proportion of time spent at each site converges jointly to some non-degenerate distribution. In a subsequent article [START_REF] Davis | Vertex-reinforced jump processes on trees and finite graphs[END_REF], the same authors studied the VRJP on more general graphs. They showed that when the G is a tree the walk can either be recurrent or transient. For a regular b-ary tree (more generally, a tree satisfying a so-called L-property), they proved the existence of two constants

0 < c r (b) ≤ c t (b) (2)
such that:

• For c < c r , the VRJP(c) visits every vertex infinitely often a.s.

• For c > c t , the VRJP(c) visits every vertex only a finite number of time a.s. * Laboratoire Modal'X, Université Paris X, France. email: anne.laure.basdevant@normalesup.org † Laboratoire de Mathématiques, Université Paris XI, France. email: arvind.singh@math.u-psud.fr Although they did not prove that c r = c t , the computation of the bound c t obtained in [START_REF] Davis | Vertex-reinforced jump processes on trees and finite graphs[END_REF] already implies that the VRJP(1) is transient on a 4-ary tree. More recently, Collevecchio [START_REF] Collevecchio | On the transience of processes defined on Galton-Watson trees[END_REF][START_REF] Collevecchio | Limit theorems for vertex-reinforced jump processes on regular trees[END_REF] showed that the VRJP(1) on a 3-ary tree is also transient with positive speed (and a C.L.T. holds) and asked whether this result also holds for a VRJP(1) on a binary tree.

The main result of this paper states that, for almost every realization of an infinite super critical Galton-Watson tree with mean offspring distribution b, one has c t (b) = c r (b) and recurrence occurs at the critical value. In fact, recalling Lyons-Pemantle's criterion for recurrence/transience of a random walk in random environment (RWRE) on a Galton-Watson tree (see Theorem 3 of [START_REF] Lyons | Random walk in a random environment and first-passage percolation on trees[END_REF]), Theorem 1.1 states that the phase transition of a VRJP(c) is exactly the same as that of a discrete time random walk in an i.i.d. random environment where the law of the environment is given by the random variable m c (∞) defined below.

Concerning the discrete time model of the linearly edge reinforced random walk (LERRW), de Finetti's theorem implies, that any LERRW on an acyclic graph may be seen as a RWRE in a Dirichlet environment. However, the non-exchangeability of the increments of a VRJP forbids a direct interpretation of the process in terms of a time change of a RWRE and we do not have a convincing argument why the VRJP should have the same phase transition as a RWRE. For example, using Theorem 1.5 of [START_REF] Aidékon | Transient random walks in random environment on a Galton-Watson tree[END_REF], one can check that, on a regular tree, the random walk in the random environment defined by m c (∞) always has a positive speed when it is transient. Does this result somehow imply that a transient VRJP always has positive speed? Theorem 1.1. For c > 0, let m c (∞) denote a random variable on (0, ∞) with density:

P{m c (∞) ∈ dx} def = c exp -(c(x-1)) 2 2x √ 2πx 3 dx. (3)
Define

µ(c) def = inf a∈R E m c (∞) a = c √ 2π ∞ 0 x -1 exp - (c(x -1)) 2 2x dx. ( 4
)
Let T denote a Galton-Watson tree with mean 1 < b < ∞. On the event that T is infinite, we have, for almost every realization of T:

• If bµ(c) ≤ 1, the VRJP(c) on T visits every vertex infinitely often a.s.

• If bµ(c) > 1, the VRJP(c) on T visits every vertex only finitely many times a.s.

For c = 1, we have 1/µ(1) ≃ 1.095. Therefore the VRJP(1) is transient on any regular b-ary tree with b ≥ 2. Making a change of variable (see Appendix of [START_REF] Davis | Vertex-reinforced jump processes on trees and finite graphs[END_REF]), the function µ may be rewritten in the form

µ(c) = 1 √ 2π ∞ -∞ e -y 2 /2 1 + y 2 /(4c 2 ) dy.
Thus, µ is continuous, strictly increasing on [0, ∞) with lim 0 µ = 0 and lim ∞ µ = 1 (see Figure 1). Denoting by µ -1 its inverse, we get Corollary 1.2. For any supercritical Galton-Watson tree with mean 1 < b < ∞, with the notation (2), we have, for almost every realization where the tree is infinite,

c t (b) = c r (b) = µ -1 (1/b).
In particular, the recurrence/transience phase transition for VRJP on the class of Galton-Watson tree is monotonic w.r. Let us note that, although this monotonicity result w.r.t. the parameter c seems quite natural, we do not know how to prove it without using the explicit computation of µ to assert that this function is monotonic. More generally, we do not know how to prove a similar result for an infinite graph which contains loops.

Preliminary results

In this section, we recall some important results concerning VRJP obtained by Davis and Volkov in [START_REF] Davis | Continuous time vertex-reinforced jump processes[END_REF][START_REF] Davis | Vertex-reinforced jump processes on trees and finite graphs[END_REF] which will play a key role in the proof of Theorem 1.1. We start with the so-called restriction principle for VRJP which follows from the lack of memory of the exponential law.

Proposition 2.1 (Restriction principle, Davis, Volkov [START_REF] Davis | Vertex-reinforced jump processes on trees and finite graphs[END_REF]). Let G be a connected graph and let G 1 be a connected subgraph with the property that for any path starting in any v ∈ G\G 1 and ending in G 1 , the first "port of entry" into G 1 is uniquely determined. Assume moreover that on each connected component of G\G 1 , the VRJP(c) is recurrent. Then the VRJP(c) on G starting at v ∈ G 1 restricted to G 1 has the same law as the VRJP(c) on the subgraph G 1 starting from the same point.

We shall make intensive use of this result in the case where G is a rooted tree and G 1 is a subtree of G (for instance, the ball of radius N centered at the root).

VRJP on the graph {0, 1}

In view of the restriction principle stated above, many properties of the VRJP on an acyclic graph can be derived from the study of the VRJP on the simpler graph G 0 def = {0, 1}. A detailed analysis of the VRJP on G 0 is undertaken in [START_REF] Davis | Continuous time vertex-reinforced jump processes[END_REF]. Consider a VRJP(c) on G 0 , starting at 0. For t ≥ c, define the stopping time

ξ(t) def = inf{s > 0, L c (s, 0) = t} and A c (t) def = L c (ξ(t), 1). ( 5
)
The quantity A c (t)c corresponds to the time spent at site 1 before spending time tc at site 0. The variable A c (t) takes values in [c, ∞) and has an atom at c. More precisely, denoting by E(c) an exponential random variable with parameter c, we have

P{A c (t) = c} = P{the VRJP(c) does not jump before time t -c} = P{E(c) > t -c} = e -c(t-c) . (6)
For t > c, the law of A c (t) conditioned on {A c (t) > c} is absolutely continuous w.r.t. the Lebesgue measure, with strictly positive density on (c, ∞). Considering only the time spent at site 1 before the first return to site 0, we get the lower bound:

P{A c (t) ≥ α | A c (t) > c} ≥ P{E(t) > α -c} = e -(α-c)t . (7)
For t ≥ c, define

m c (t) def = A c (t) t .
It is proved in [START_REF] Davis | Continuous time vertex-reinforced jump processes[END_REF] that the process (m c (t), t ≥ c) is a positive martingale which converges a.s. toward the random variable m c (∞) defined in Theorem 1.1. The moments of m c (∞) can be computed explicitly using [START_REF] Athreya | Branching processes[END_REF]. For θ ∈ R, we get

E[m c (∞) θ ] = 2 π ce c 2 K θ-1/2 (c 2 ) < ∞
where K α (x) denotes the modified Bessel function of the second kind of order ν (c.f. [START_REF] Abramowitz | Handbook of mathematical functions with formulas, graphs, and mathematical tables[END_REF] for details on this class of special functions). Using

K α = K -α and K α ≤ K α ′ for 0 ≤ α ≤ α ′ , it follows that min θ∈R E m c (∞) θ = E m c (∞) , (8)
which entails the second equality of (4).

VRJP on trees

Let T be a deterministic locally bounded tree rooted at some vertex o. According to Theorem 3 of [START_REF] Davis | Vertex-reinforced jump processes on trees and finite graphs[END_REF], any VRJP on T is either recurrent (every vertex is visited infinitely often a.s.) or transient (every vertex is visited only finitely many times a.s.). Moreover, we have the following characterization of recurrence and transience in terms of the local time of the walk at the root:

The VRJP(c) on

T is recurrent ⇐⇒ lim t→∞ L c (t, o) = ∞. (9)
Define, for t > c, ξ(t)

def = inf{s > 0, L c (s, o) = t},
and let (v 0 = o, v 1 , . . . , v n ) be a nearest neighbour self-avoiding path starting from the root of T and ending at v n . For 0

≤ k ≤ n, set Z k def = L c (ξ(t), v k ). ( 10
)
If T is a finite tree, then the VRJP(c) on T is recurrent. Applying the restriction principle to the subgraph (v 0 = o, v 1 , . . . , v n ), it follows that the process (Z k ) 0≤k≤n is a Markov chain starting from Z 0 = t with transition probabilities

P{Z k+1 ∈ E | Z 0 , . . . , Z k = x} = P{A c (x) ∈ E} (11)
where A c is the random variable defined in [START_REF] Collevecchio | On the transience of processes defined on Galton-Watson trees[END_REF]. Let us note that Z takes values in [c, ∞) and that c is an absorbing point. Moreover, since (A c (t)/t) t≥c is a martingale starting from 1, the process Z is also a (positive) martingale. Therefore, Z n converges a.s. as n tend to infinity and the limit is necessarily equal to c a.s.

3 Proof of Theorem 1.1

We first set some notation. Let T be the set of all locally finite rooted trees. Given a tree T ∈ T , we denote its root by o. For v ∈ T , we use the notation ← v for the father of v and

→ v 1 , → v 2 , . . . for
the sons of v. We also denote by |v| the height of the vertex v in the tree (i.e. its graph distance from the root). For n ≥ 0, T n will stand for the subtree of T of vertices of height smaller or equal to n.

In the following, ν will always denote a probability measure on the non-negative integers with finite mean b > 1 and Q ν will denote the probability measure on T under which the canonical r.v. T is a Galton-Watson tree with offspring distribution ν.

For c > 0, we consider on the same (possibly enlarged) probability space a process X = (X(t), t ≥ 0) and a collection of probability measures (P T,c , T ∈ T ) called quenched laws such that X under P T,c is a VRJP(c) on T with X(0) = o. The annealed probability is defined by

P ν,c def = P T,c ⊗ Q ν .
We say that X under P ν,c is a VRJP(c) on a Galton-Watson tree with reproduction law ν. In the following, we shall omit the subscripts c, ν when it does not lead to confusion.

Restriction to trees without leaves

The Harris decomposition of a super-critical Galton-Watson tree states that conditionally on non extinction, T under Q ν can be generated in the following way:

• Generate a Galton-Watson tree T g with no leaf called the backbone.

• Attach at each vertex v of T g a random number N v of i.i.d. subcritical trees T 1 l , . . . , T Nv l .
See for instance [START_REF] Athreya | Branching processes[END_REF] for a precise description of the laws of N v , T g and T l . Let us simply note that the expected number of children per vertex of T g is also equal to b. Consider now a VRJP(c) on T on the event that T is infinite. The restriction principle applied with G = T and G 1 = T g implies that the VRJP(c) on T is transient if and only if the VRJP(c) on T g is transient. Since the criterion for the transience/recurrence of the walk of Theorem 1.1 only depends on b, it suffices to prove the result for trees without leaves. In the sequel, we will always assume that this is the case, that is:

ν(0) = 0.

Proof of recurrence when bµ(c) < 1

In [START_REF] Davis | Vertex-reinforced jump processes on trees and finite graphs[END_REF], Davis and Volkov prove that a VRJP(1) is recurrent when b ≤ 1.04. In fact, their argument shows recurrence whenever bµ(c) < 1 by simply fine-tuning some parameters. We provide below a sketch of the proof and we refer the reader to [START_REF] Davis | Vertex-reinforced jump processes on trees and finite graphs[END_REF] for further details. Consider a VRJP(1) on the non-negative integers {0, 1, . . .} and denote by σ n the first time the walk reaches level n. It is proved in the appendix of [START_REF] Davis | Vertex-reinforced jump processes on trees and finite graphs[END_REF] that, for any a > 1,

P{L 1 (σ n , 0) < a n } ≤ (E[ m 1 (∞)]a 1/2 ) n . ( 12
)
Adapting the proof for any c > 0, it is immediate to check that, for any VRJP(c) on the non-negative integers,

P{L c (σ n , 0) < a n } ≤ (E[ m c (∞)]a 1/2 ) n = (µ(c)a 1/2 ) n . ( 13
)
We now copy the argument of the proof of Theorem 5 of [START_REF] Davis | Vertex-reinforced jump processes on trees and finite graphs[END_REF] using the bound (13) in place of (12). Let T ∈ T be an infinite tree. Let V n denote the number of vertices of T of height n and set

G n = L c (inf{t > 0, |X t | = n}, o)
so that G nc is the total time spent by X at the root before reaching a vertex of height n.

Conditioning on the position of the VRJP(c) when it reaches level n and applying the restriction principle to the path connecting this vertex to the root, we find, using (13),

P T {G n < a n } ≤ (µ(c)a 1/2 ) n V n . ( 14
)
Assume now that the tree T satisfies

lim inf n→∞ V 1/n n < µ(c) -1
then (14) yields, taking a sufficiently close to 1,

P T {G n k < a n k } ≤ (1 -ε) n k
for some subsequence (n k ) and some ε > 0. Letting k go to infinity, we conclude that

lim t→∞ L c (t, o) = ∞. P T -a.s.
Thus, the VRJP(c) on T is recurrent according to [START_REF] Freedman | Another note on the Borel-Cantelli lemma and the strong law, with the Poisson approximation as a by-product[END_REF]. We conclude the proof for the VRJP(c) on the Galton-Watson tree T noticing that, when bµ(c) < 1, we have for Q ν -almost any tree

T ∈ T , lim n→∞ V 1/n n = b < µ(c) -1 .

The branching Markov Chain F

Recall that we assume ν(0) = 0 so the tree T is infinite Q ν -a.s. We introduce a branching Markov chain F indexed by the vertices of T and taking values in [c, ∞),

F def = (f (v), v ∈ T) ∈ T ∈T [c, ∞] T .
More precisely, the population at time n is indexed by {v ∈ T, |v| = n} and the set of positions of the particles of F at time n is

F n def = (f (v), |v| = n).
Thus, the genealogy of this branching Markov chain is chosen to be exactly the Galton-Watson tree T. In particular, under the annealed probability P, each particle v splits, after a unit of time, into a random number B of particles

→ v 1 , . . . , → v B
where B is distributed as ν. In order to characterize F , it remains to specify the law of the position f (v) of the particles. We choose the dynamics of F , conditionally on its genealogy T in the following way:

(a) For any n > 0, conditionally on (f (u), |u| < n), the random variables (f (v), |v| = n) are independent.

(b) For any

v = o, conditionally on (f (u), |u| < |v|), the random variable f (v) is distributed as A c (f ( ← v ))
where A c is defined by [START_REF] Collevecchio | On the transience of processes defined on Galton-Watson trees[END_REF].

We use the notation P x 0 for the annealed law where F starts with the initial particle o being located at f (o) = x 0 . Note that, since the tree is infinite, the Markov chain F never becomes extinct. However, recalling that c is an absorbing point for A c , it follows that if a particle v is located at f (v) = c, then all its descendants are also located at c. Thus, we will say that the process F dies out if there exists a time n such that all the particle at time n are at position c. Otherwise, we say that the process survives.

Proposition 3.1. For any x ≤ y, the process F under P x is stochastically dominated by F under P y .

Proof. Recalling it is clear that A c (x) ≤ A c (y) for any c ≤ x ≤ y and the result follows by induction.

Proposition 3.2. Let x 0 > 0 and N > 0 and let (X N (t), t ≥ 0) denote a VRJP(c) on the finite subtree

T N = {v ∈ T, |v| ≤ N }, with X N (0) = o. Set ξ N (x 0 ) def = inf{s > 0, L N c (s, o) = x 0 },
where L N is defined as in (1) for X N . Then, the random variables (L N c (ξ N (x 0 ), v), v ∈ T N ) under P and (f (v), v ∈ T N ) under P x 0 have the same law.

Proof. Simply notice that since the T N is finite, X N is recurrent and ξ N is finite a.s. and apply the restriction principle for VRJP.

The VRJPs X on T and X N on T N coincide up to the first time they reach a site of height N , therefore, P{X reaches level N before spending time x 0c at the origin} = P{X N reaches level N before spending time x 0c at the origin} = P x 0 {the process F does not die out before time N }.

Letting N and then x 0 tend to infinity, and using (9), we get P{X visits every vertex of T finitely many times} = lim↑

x 0 →∞ P x 0 {F survives}. ( 15
)
The next proposition extends the 0-1 law proved in [START_REF] Davis | Vertex-reinforced jump processes on trees and finite graphs[END_REF] for deterministic trees to Galton-Watson trees.

Proposition 3.3 (0 -1 law for VRJP on Galton-Watson trees). Let T be a Galton-Watson tree T without leaves and with mean b > 1. Then, for any c > 0, the VRJP(c) X on T is either recurrent or transient under the annealed law:

P{X visits every vertex of T finitely many times} = 1 -P{X visits every vertex of T infinitely often} ∈ {0, 1}.

Proof. Since the 0 -1 law holds for any deterministic tree, we just need to show that the r.h.s. limit of (15) is either 0 or 1. Suppose that this limit is non-zero. We can find x 0 > c and α > 0 such that P x 0 {F survives} ≥ α.

Given an interval I, let N I k denote the number of particles in F located inside I at time k i.e.

N I k def = #{v ∈ T, |v| = k and f (v) ∈ I}. (16)
Since the particles in F evolve independently, conditionally on (f (v), |v| ≤ k), the process (f (v), |v| ≥ k) has the same law as the union of #{v ∈ T, |v| = k} independent branching Markov chains F starting from the positions F k = (f (v), |v| = k). Making use of the stochastic monotonicity of F w.r.t. to the position of the initial particle (Proposition 3.1), we deduce that, for any ε > 0, we can find m large enough such that, for any k and any x,

P x {F survives} ≥ P x {N [x 0 ,∞) k ≥ m and F survives} ≥ P x {N [x 0 ,∞) k ≥ m} (1 -P x 0 {F dies out} m ) ≥ P x {N [x 0 ,∞) k ≥ m} (1 -(1 -α) m ) ≥ P x {N [x 0 ,∞) k ≥ m}(1 -ε). (17)
On the one hand, we have, for any y > c,

P x {f (v) > y for every v of height 1} = ∞ b=1 ν(b)P{A c (x)/x > y/x} b .
Since the sequence A c (x)/x converges as x → ∞ towards a random variable which has no atom at 0 (c.f. Section 2.1), the previous equality implies

lim x→∞ P x {f (v) > y for every v of height 1} = 1.
Using again the stochastic monotonicity of F w.r.t. its starting point, it follows by induction that, for any fixed k,

lim x→∞ P x {f (v) > x 0 for every v ∈ T s.t. |v| = k} = 1. ( 18
)
On the other hand, the tree T grows exponentially so that, for any m,

lim k→∞ P{#{v ∈ T, |v| = k} ≥ m} = 1. ( 19
)
Combining ( 18) and ( 19), we deduce that, for any m, we can find k and x large enough such that

P x {N [x 0 ,∞) k ≥ m} ≥ 1 -ε. ( 20
)
which yields, using (17),

P x {F survives} ≥ (1 -ε) 2 .

Proof of Transience when bµ(c) > 1

Let (Z n ) n≥0 be a Markov chain on [c, ∞) with transition probabilities given by (11) and denote by P x the probability under which Z starts from Z 0 = x. Let T ∈ T and fix v ∈ T . It follows from the definition of the branching Markov chain F that

P x {f (v) ∈ E | T = T } = P x {Z |v| ∈ E}.
Let us for the time being admit that, for some x 0 > c, we have lim inf

n→∞ P x 0 {Z n ≥ x 0 } 1/n ≥ µ(c). (21) Recalling that N [x 0 ,∞) k
denotes the number of particles of F located above level x 0 at time k, we find, when µ(c)b > 1, that for k 0 large enough,

E x 0 [N [x 0 ,∞) k 0 ] = E x 0 |v|=k 0 1 {f (v)≥x 0 } = E[#{v ∈ T, |v| = k 0 }]P x 0 {Z k 0 ≥ x 0 } = bP x 0 {Z k 0 ≥ x 0 } 1/k 0 k 0 ≥ 2.
Just as in the proof of Proposition 3.3, making use of the branching property of F and keeping only the particles located above x 0 at times k 0 n, n ≥ 0, it follows by induction that, under P x 0 , the process (N

[x 0 ,∞) k 0 n
) n≥0 stochastically dominates a classical Galton-Watson process with

reproduction law N [x 0 ,∞) k 0 . Since E x 0 [N [x 0 ,∞) k 0
] ≥ 2, this Galton-Watson process has probability α > 0 of non extinction, which implies

P x 0 {F survives} ≥ α.
We conclude using (15) and Proposition 3.3 that P{X visits each vertex of T finitely many times} = 1.

It remains to prove (21) which is a consequence of Lemma 3.4. Let (S(x), x ∈ R) be a collection of real-valued random variables. Assume that the following holds.

(a) For any x < y, the random variable x + S(x) is stochastically dominated by y + S(y).

(b) S(x) converges in law, as x tend to +∞, towards a random variable S(∞) whose law is absolutely continuous w.r.t. the Lebesgue measure and P{S(∞) > 0} > 0.

(c) The Laplace transform φ(λ) ∞) ] reaches its minimum at some point ρ > 0 which belongs to the non-empty interior of the its definition domain

def = E[e λS(
D def = {λ ∈ R, φ(λ) < ∞}. Let Y = (Y n , n ≥ 0) denote a real valued Markov chain with transition kernel P{Y n+1 ∈ E | Y n = y} = P{S(y) + y ∈ E}
and let τ x be the first time Y enters the interval (-∞, x). Denoting by P x the law of Y starting from x, we have, for all x large enough,

lim n→∞ P x {τ x > n} 1/n ≥ φ(ρ). (22)
We apply the lemma to the Markov chain Y defined by

Y n def = log Z n .
According to (11), we have

P{Y n+1 ∈ E | Y n = y} = P{S(y) + y ∈ E} with S(y) def = log m c (exp(y)) and S(∞) def = log m c (∞)
where m c is the martingale of Section 2.1. On the one hand, Assumption (a) holds since A c (x) ≤ A c (y) for all x ≤ y. On the other hand, the results of Davis and Volkov [START_REF] Davis | Continuous time vertex-reinforced jump processes[END_REF][START_REF] Davis | Vertex-reinforced jump processes on trees and finite graphs[END_REF] recalled in Section 2.1 imply that Assumptions (b),(c) also hold and inf λ∈R E[e -λS(∞) ] = µ(c).

Thus, we conclude that, for x 0 large enough, lim inf n→∞

P x 0 {Z n ≥ x 0 } 1/n ≥ lim n→∞ P log x 0 min 1≤i≤n Y i ≥ log x o 1/n ≥ µ(c).
Proof of Lemma 3.4. Assumption (a) implies that for x < y, the Markov chain Y under P x is stochastically dominated by Y under P y . Thus, using the Markov property, we get that, for any n, m,

P x {τ x > n + m} ≥ P x {τ x > n}P x {τ x > m}.
The superadditivity of the sequence log P x {τ x > n} now implies that the limit in ( 22) exists. It remains to prove the lower bound for x large enough. Set g x (t) def = P{S(x) > t} and g(t

) def = P{S(∞) > t}.
In view of Assumption (b), as x goes to +∞, g x converges uniformly towards g. Define

ĝx (t) def = inf y≥x g y (t).
For each x, the function ĝx is càdlàg, non increasing, with lim t→-∞ ĝx (t) = 1 and lim t→+∞ ĝx (t) = 0. Thus, for each x, we can consider a random variable Ŝ(x) such that P{ Ŝ(x) > t} = ĝx (t). By construction the sequence of random variables Ŝ(x) is stochastically monotonic and converges in law toward the random variable S(∞). Let Ŷ x denote a random walk with step Ŝ(x) i.e. Ŷ x n+1 -Ŷ x n law = Ŝ(x). By construction, the random variable Ŝ(x) is stochastically dominated by S(y) for any y ≥ x. Combining this fact and the stochastic monotonicity of the Markov chain Y w.r.t. its starting point, it follows by induction that the random walk Ŷ x started from x and killed when it enters the interval (-∞, x) is stochastically dominated by Y under P x . In particular, denoting by τ x 0 the first time Ŷ x enters the interval (-∞, 0), it follows that τ x 0 under P 0 (i.e. the walk Ŷ x started from 0), is stochastically dominated by τ x under P x . Hence,

lim n→∞ P x {τ x > n} 1/n ≥ lim inf n→∞ P 0 {τ x 0 > n} 1/n . (23)
Let φx (λ)

def = E[e λ Ŝ(x) ] with definition domain Dx def = {λ ∈ R, φx (λ) < ∞}. Since, Ŝ(x) is stochastically dominated by S(∞), we have D ∩ [0, ∞) ⊂ Dx ∩ [0, ∞). According to Assumption (c), we can choose a > 0 such that I a def = [ρ -a, ρ + a] ⊂ D ∩ [0, ∞).
On I a , as x goes to +∞, the functions φx converge uniformly toward φ. Making use of the strict convexity of a Laplace transform, it follows that, for all x large enough, the function φx verifies Assumption (c) i.e. φx reaches its minimum on Dx at some point ρ x ∈ I a . Moveover, we have:

lim x→∞ φx (ρ x ) = φ(ρ). (24)
Applying now Theorem 1 of [START_REF] Biggins | A branching random walk with a barrier[END_REF] to the random walk Ŷ x with step distribution Ŝ(x) gives lim inf

n→∞ P 0 {τ x 0 > n} 1/n = φx (ρ x ). (25)
Combining ( 23) and (25), we get that

lim n→∞ P x {τ x > n} 1/n ≥ φx (ρ x ). (26)
Assumption (b) also implies that, for some ε, η > 0 small enough, there exists x 0 such that, for all x ≥ x 0 , we have P{S(x) > ε} > η, thus

P{Y n+1 > ε + Y n | Y n = x} > η.
In particular, for x > y > x 0 , the event E(x, y) = {Y enters [x, ∞) before entering (-∞, y)} has a strictly positive probability under P y . Therefore, using again the Markov property and the stochastic monotonicity of Y w.r.

E[ξ(t)] = E t v∈T (f (v) -c) = ∞ n=0 b n E t [Z n -c] = ∞ n=0 b n (t -c) = ∞ (29)
for any t > c. In particular, denoting by ζ o the first time the walk returns to the root of the tree, it easily follows from (29), by conditioning on the time the walk makes its first jump and applying the restriction principle that any recurrent VRJP on T is "null" recurrent in the sense that E[ζ o ] = ∞.

3.5

The critical case bµ(c) = 1.

The following proposition directly implies that the VRJP(c) on a Galton-Watson tree is recurrent in the critical case bµ(c) = 1 since we already know that recurrence occurs when bµ(c) < 1.

Proposition 3.6. Assume that the VRJP(c) is transient on some Galton-Watson tree T without leaves and with mean b > 1. Then, there exists a Galton-Watson tree T (with leaves) with mean 1 < b < b such that the VRJP(c) on T is also transient on the event that T is infinite.

The proof of Proposition 3.6 uses again the characterization of transience in terms of the positive probability of survival of the associated branching Markov chain F . Roughly speaking, we show that, conditionally on survival, the number of particles of F not located at c grows exponentially with time. This implies that the branching Markov chain on a small percolation of the original tree still survives with positive probability. Hence the VRJP on this percolated tree is also transient.

In the following, we assume as before that the Galton-Watson tree T with reproduction law ν has no leaves and has mean b > 1 so that it is infinite and grows exponentially. Recall the definition of the branching Markov chain F = (f (v), v ∈ T) constructed in Section 3.3. We denote by (F n ) the natural filtration of F : For any starting point x 0 > c, we have, E(x 0 , 2) = {F survives} P x 0 -a.s.

F n def = σ(T n , (f (v), v ∈ T n )).
Proof. The inclusion E(x 0 , 2) ⊂ {F survives} is trivial. Let ε > 0 and set, for k ≤ n,

B k,n def = E x 0 N (c,∞) n 1 {N [c+ε,∞) k =0,N [c+ε,∞) k+1 =0,...,N [c+ε,∞) n-1
=0} .

Recall that each particle v of F evolves independently and gives birth to a random number B (with mean b) of children. Moreover, conditionally on F n , the positions f (

→ v 1 ), . . . , f ( → v B
) of the children of a particle v at time n (i.e. |v| = n) are i.i.d. and distributed as A c (f (v)). Thus, in view of ( 6), it follows that

E[N (c,∞) n+1 | F n ] ≤ b(1 -e -cε )N (c,∞) n on the event {N (c+ε,∞) n = 0}.
Choosing ε small enough such that b(1e -cε ) < 1/2, we get

B k,n+1 = E x 0 E[N (c,∞) n+1 | F n ]1 {N [c+ε,∞) k =0,N [c+ε,∞) k+1 =0,...,N [c+ε,∞) n-1 =0} ≤ 1 2 E x 0 N (c,∞) n 1 {N [c+ε,∞) k =0,N [c+ε,∞) k+1 =0,...,N [c+ε,∞) n-1 =0} ≤ 1 2 B k,n .
which yields,

E x 0   ∞ n=k N (c,∞) n 1 N [c+ε,∞) i = 0 for all i ≥ k   ≤ ∞ n=k B k,n < ∞.
Therefore, the process F dies out P x 0 -a.s. on the event N

[c+ε,∞) i = 0 for all i ≥ k . Taking the limit as k goes to infinity, we obtain

E(c + ε, 1) ⊃ {F survives} P x 0 -a.s. ( 30
) Let now U n def = 1 {N [x 0 ,∞) n ≥2} .
Using the stochastic monotonicity of Proposition 3.1 and the facts that ν[2, ∞) > 0 (since b > 1) and ( 7), we find that (with the convention M = 0 when σ x = ∞). We have,

E[U n+1 | F n ] ≥ E[U n+1 1 {N [c+ε,∞) n ≥1} | F n ] ≥ 1 {N [c+ε,∞) n ≥1} E c+ε [U 1 ] ≥ 1 {N [c+ε,∞)
E x [ M ] ≥ E x [ M 1 {σx≤γ} 1 {Tγ = Tγ } ] ≥ 2P x {σ x ≤ γ and T γ = Tγ } ≥ 2 P x {σ x ≤ γ} + Q ν {T γ = Tγ } -1 ≥ 2 P x {σ x ≤ γ} + Q ν {#T γ ≤ b 2γ }(1 -η) b 2γ -1 . ( 33
)
Recalling that the distribution of offsprings ν has mean b, we get

lim γ→∞ Q ν {#T γ ≤ b 2γ } = 1. (34)
Combining (32),(33) and (34), we can choose x, γ large enough and η > 0 small enough such that E x [ M ] > 1.

Finally, using again the branching structure of F and the stochastic monotonicity of the process w.r.t. the position of the initial particle, it follows by induction that the random variable #{v ∈ T, f (v) > x} under P x is stochastically larger than the total progeny of a Galton-Watson process with reproduction law M . Since E[ M ] > 1, this process is supercritical hence

P x { F survives} ≥ P x {#{v ∈ T, f (v) > x} = ∞} > 0
which in turn implies that the VRJP(c) on the percolated tree T is transient on the event that T is infinite.

Figure 1 :

 1 Figure 1: Graph of the function µ.

Lemma 3 . 7 .

 37 Recall the definition of N I n given in(16). Let E(x, k) be the eventE(x, k) def = {There exist infinitely many n such that N [x,∞) n ≥ k }.

n 1 ) ≥ x 0 and f ( → o 2 ) ≥ x 0 = 1

 1201 ≥1} P c+ε the initial particle o has at least two children with f (→ o {N [c+ε,∞) n ≥1} ν[2, ∞)P{A c (c + ε) > x 0 } 2 = C1 {N [c+ε,∞) n ≥1} (31)for some constant C > 0. Combining (30) and (31), we get∞ n=1 E[U n+1 | F n ] = ∞on the event {F survives}.A direct application of the conditional Borel-Cantelli Lemma (c.f.[START_REF] Freedman | Another note on the Borel-Cantelli lemma and the strong law, with the Poisson approximation as a by-product[END_REF]) yields∞ n=1 U n = ∞ on the event {F survives}.which exactly means that E(x 0 , 2) ⊃ {F survives}.Proof of Proposition 3.6. Assume that the VRJP(c) X on the Galton-Watson tree T with reproduction law ν is transient. According to Proposition 3.3 and (15), we havelim x→∞ P x {F survives} = 1.Define the (possibly infinite) F n -stopping timeσ x def = inf{k ≥ 1, N [x,∞) k ≥ 2}.Using the result of the previous lemma, we getlim x→∞ lim γ→∞ P x {σ x ≤ γ} = lim x→∞ P x {F survives} = 1. (32)Let now T be the tree obtained from T be removing each vertex (and its descendants) with probability η > 0. The tree T is again a Galton-Watson tree with mean b = b(1η) < b. We denote by F the restriction of F to T,F def = (f (v), v ∈ T).The restriction principle states that F is the branching Markov chain associated with the VRJP(c) on T. Let M be the number of particles in F located above x at time σ x ,M def = #{v ∈ T, |v| = σ x , f (v) > x}

  t. its starting point, we get P y {τ y > n} ≥ P y {E(x, y)}P x {τ x > n} Suppose that the VRJP(c) is recurrent on T. Recall that ξ(t) denotes the time where the local time of the walk at the origin reaches tc. We can express ξ(t) in terms of the branching Markov chain F and we get, using that E t [Z n ] = t for all n,

	which yields
	lim n→∞	P y {τ y > n} 1/n ≥ lim n→∞	P x {τ x > n} 1/n .	(27)
	Combining (24), (26) and (27), we conclude that, for y ≥ x 0 , lim n→∞ P y {τ y > n} 1/n ≥ lim x→+∞ φx (ρ x ) = φ(ρ).	(28)
	Remark 3.5.