Elisabetta De Maria
email: edemaria@i3s.unice.fr

Alexandre Muzy
email: muzy@i3s.unice.fr

Daniel Gaffé
email: daniel.gaffe@unice.fr

Annie Ressouche
email: annie.ressouche@inria.fr

Franck Grammont
email: grammont@unice.fr

Verification of Temporal Properties of Neuronal Archetypes Modeled as Synchronous Reactive Systems

There exists many ways to connect two, three or more neurons together to form different graphs. We call archetypes only the graphs whose properties can be associated with specific classes of biologically relevant structures and behaviors. These archetypes are supposed to be the basis of typical instances of neuronal information processing. To model different representative archetypes and express their temporal properties, we use a synchronous programming language dedicated to reactive systems (Lustre). The properties are then automatically validated thanks to several model checkers supporting data types. The respective results are compared and depend on their underlying abstraction methods.

Introduction

Since a few years, the investigation of neuronal micro-circuits has become an emerging question in Neuroscience, notably in the perspective of their integration with neurocomputing approaches [START_REF] Markram | The blue brain project[END_REF]. We call archetypes specific graphs of a few neurons with biologically relevant structures and behaviors. These archetypes correspond to elementary and fundamental elements of neuronal information processing. Several archetypes can be coupled to constitute the elementary bricks of bigger neuronal circuits in charge of specific functions. For instance, locomotive motion and other rhythmic behaviors are controlled by well-known specific neuronal circuits called Central Generator Pattern (CPG) [START_REF] Matsuoka | Mechanisms of frequency and pattern control in the neural rhythm generators[END_REF]. These CPG have the capacity to generate oscillatory activities, at various regimes, thanks to some specific properties at the neuronal and circuit levels.

The goal of this work is to formally study the behavior of different representative archetypes. At this aim, we model the archetypes using a synchronous language for the description of reactive systems (Lustre). Each archetype (and corresponding assumed behavior in terms of neuronal information processing) is validated thanks to model checkers.

Different approaches have been proposed in the literature to model neural networks (Artificial Neural Networks [START_REF] Das | Elements of artificial neural networks [book reviews[END_REF], Spiking Neural Networks [START_REF] Maass | Lower bounds for the computational power of networks of spiking neurons[END_REF], etc.). In this paper we focus on Boolean Spiking Neural Networks where the neurons electrical properties are described via an integrate-and-fire model [START_REF] Gerstner | Spiking Neuron Models: An Introduction[END_REF]. Notice that discrete modeling is well suited because neuronal activity, as with any recorded physical event, is only known through discrete recording (the recording sampling rate is usually set at a significantly higher resolution than the one of the recorded system, so that there is no loss of information). We describe neural networks as weighted directed graphs whose nodes represent neurons and whose edges stand for synaptic connections. At each time unit, all the neurons compute their membrane potential accounting not only for the current input signals but also for the ones received along a given temporal window. Each neuron can emit a spike according to the overtaking of a given threshold. Such a modeling is more sophisticated than the one proposed by McCulloch and Pitts in [START_REF] Mcculloch | A logical calculus of the ideas immanent in nervous activity[END_REF], where the behavior of a neural network is expressed in terms of propositional logic and the present activity of each neuron does not depend on past events.

Spiking neural networks can be considered as reactive systems: their inputs are physiological signals coming from input synapses, and their outputs represent the signals emitted in reaction. This class of systems fits well with the synchronous approach based on the notion of a logical time: time is considered as a sequence of logical discrete instants. An instant is a point in time where external input events can be observed, along with the internal events that are a consequence of the latter. The synchronous paradigm can be implemented using synchronous programming languages. In this approach we can model an activity according to a logical time framing: the activity is characterized by a set of events expected at each logical instant and by their expected consequences. A synchronous system evolves only at these instants and is "frozen" otherwise (nothing changes between instants). At each logical instant, all events are instantaneously broadcasted, if necessary, to all parts of the system whose instantaneous reaction to these events contributes to the global system state. Synchronous programming languages being initially dedicated to digital circuits, this neural implementation could be easily mapped into a physical one.

Each instant is triggered by input events (the core information completed with the internal state computed from instantaneous broadcast performed during the instant frame). As a consequence, inputs and resulting outputs all occur simultaneously. This (ideal) synchrony hypothesis is the main characteristics of the synchronous paradigm [START_REF] Halbwachs | Synchronous Programming of Reactive Systems[END_REF]. Another major feature is also that it supports concurrency through a deterministic parallel composition. The synchronous paradigm is now well established relying on a rigorous semantics and on tools for simulation and verification.

Several synchronous languages respect this synchronous paradigm. All these languages have a similar expressivity. However, we choose here Lustre [START_REF] Halbwachs | Synchronous Programming of Reactive Systems[END_REF] synchronous language to express neuron behaviors more easily. Lustre defines op-erator networks interconnected with data flows and it is particularly well suited to express neuron networks. Lustre respects the synchrony hypothesis which divides time into discrete instants. It is a data flow language offering two main advantages: (1) it is functional with no complex side effects, making it well adapted to formal verification and safe program transformation; also, reuse is made easier, which is an interesting feature for reliable programming concerns;

(2) it is a parallel model, where any sequencing and synchronization depends on data dependencies. Moreover, the Lustre formalism is close to temporal logic and this allows the language to be used for both writing programs and expressing properties as observers. Hence, Lustre offers an original verification means to prove that, as long as the environment behaves properly (i.e., satisfies some assumption), the program satisfies a given property. If we consider only safety properties, both the assumption and the property can be expressed by some programs, called synchronous observers [START_REF] Halbwachs | Synchronous observers and the verification of reactive systems[END_REF]. An observer of a safety property is a program, taking as inputs the inputs/outputs of the program under verification, and deciding (e.g., by emitting an alarm signal) at each instant whether the property is violated. Running in parallel with the program, an observer of the desired property and an observer of the assumption made about the environment have just to check that either the alarm signal is never emitted (property satisfied) or the alarm signal is emitted (property violated). This can be done by a simple traversal of the reachable states of the compound program.

There exists several model checkers for Lustre that are well suited to our purpose: Lesar [START_REF] Halbwachs | Validation of synchronous reactive systems: from formal verification to automatic testing[END_REF], Nbac [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF], Luke [START_REF]Luke webpage[END_REF], Rantanplan [START_REF] Franzén | Using satisfiability modulo theories for inductive verification of lustre programs[END_REF] and kind2 [START_REF] Hagen | Scaling up the formal verification of lustre programs with smt-based techniques[END_REF]. Verification with Lesar is performed on an abstract (finite) model of the program. Concretely, for purely logical systems the proof is complete, whereas in general (in particular when numerical values are involved) the proof can be only partial. Indeed, properties related to values depend on the abstraction performed by the tool. In our experiment, some properties can be validated with Lesar, but some others need powerful abstraction techniques. Hence, we use Lustre tools such as Nbac, Luke, Rantanplan and kind2. To perform abstractions, Lesar and NBac use convex polyhedra [START_REF] Maréchal | Polyhedral Approximation of Multivariate Polynomials using Handelman's Theorem[END_REF] representation of integers and reals. On the other hand, Luke is also another k-induction model checker, however it is based on propositional logic. Finally, Rantanplan and kind2 rely on SMT (Satisfiabitily Modulo Theories) based k-induction. kind2 has been specifically developed to prove safety properties of Lustre models, it combines several resolution engines and it turns out that it is the most powerful model checker used in this paper. This overall approach is used here to verify temporal properties of archetypes using model-checking techniques.

The paper is organized as follows. In Sect. 2 we present the computational model we adopt. In Sect. 3 we introduce the basic archetypes (series, series with multiple outputs, parallel composition, negative loop, inhibition of a behavior, contralateral inhibition) and we show how they can be modeled using Lustre. More precisely, we illustrate how the behavior of a single neuron can be encoded in a Lustre node and how two or more neurons can be connected to form a circuit. In Sect. 4 we express in Lustre important temporal properties concerning the described archetypes and we verify the satisfaction of these properties using the above-mentioned model checkers. Finally, Sect. 5 is devoted to a final discussion on the obtained results and on the future work. For a quick introduction to Lustre and the code of all the tested properties, the reader can refer to [START_REF] De Maria | Verification of Temporal Properties of Neuronal Archetypes Using Synchronous Models[END_REF].

Synchronous Reactive Neuron Model

We refer here to synchronous reactive systems as systems reacting under the synchronous assumption, i.e., as computing their states and sending instantaneously their output events when receiving input events. Synchronous reactive systems can be conceived as an abstraction of digital circuits. Therefore, to fit electronic/computational discreteness and finiteness, some assumptions according to the synchronous paradigm will be introduced.

We describe here first the structure of a neuron network as a graph. The dynamics of usual leaky integrate-and-fire spiking networks is presented later. Definition 1. A network of neurons is a weighted directed graph (G, w), where G = (N, A) is a directed graph with N = {1, 2, . . . , n} the set of neuron indexes and A = {(i, j) | i, j ∈ N } the set of ordered pairs of neuron indexes (synapses), and w : A → R is the synapse weight function 5 .

In a leaky integrate-and-fire neuron, the membrane potential of the neuron integrates the values of the action potentials received from its input neurons. Definition 2. A usual leaky integrate-and-fire model is a structure LIF i = (X i , Y i , S i , T i , ∆ i , Λ i ), where X i = B m is the vector of boolean input values of size m; Y i = B is the boolean output value; S i = R is the set of states defined as the set of values of membrane potential;

T i = R + 0 ∪ {+∞} is the time base; ∆ i : X m i × S i × T i → S i
is the transition function defined as

p i = ∆ i (x i1 , . . . , x im , p i , t i ) = Σ j∈P red(i) w ji x j if p i ≥ τ i r i (t i )p i + Σ j∈P red(i) w ji x j otherwise where P red(i) is the set of m predecessors of neuron i ∈ N , x j is the input of neuron i ∈ N received from neuron j ∈ P red(i), w ji = w(j, i) ∈ R is the synapse weight from neuron j ∈ N to neuron i ∈ N , r i (t i ) is the remaining potential coefficient (a decreasing function in time, usually r i (t i ) = exp(-αt i ), with α a positive constant), and τ i ∈ R + 0 is the firing threshold; and Λ i : S i → Y i is the output function defined as Λ i (p i ) = y i = 1 if p i ≥ τ i 0 otherwise .
For each synapse (j, i) ∈ A between a neuron j ∈ N and a neuron i ∈ N , y i ∈ B is the output spike value emitted by neuron i, and x j ∈ B is the input spike value of neuron i received from neuron j. If the membrane potential p i is above the threshold τ ï, at the next transition the output spike value is set to

y i = 1
and the membrane potential is reset to p i = 0. When the remaining potential coefficient r i is a constant equal to 1, there is no leak, all the potential received at last transition remains in the neuron soma. When r i (t i ) = 0 for each t i , all the potential received at last transition is lost (the model is then equivalent to

McCulloch & Pitts' model [START_REF] Mcculloch | A logical calculus of the ideas immanent in nervous activity[END_REF]).

The usual leaky integrate-and-fire model presented in Definition 2 is not compatible with our synchronous reactive system assumption: both state and time sets are possibly infinite (cf. r i (t i ) = exp(-αt i ), the exponentially decreasing function defined for t i ∈ [0, +∞]). We will show now how to approximate and limit potential values to fit the synchronous reactive system assumption.

Let us define, for each neuron, the remaining potential r(t) = exp(-αt) as r e , where r is a constant (e.g., r = exp(-α) or r ∈ [0, 1]) and e ∈ R + 0 ∪ {+∞} is the time elapsed until the current time t ∈ R + 0 ∪ {+∞}. The membrane potential can now be defined as a sum of input values and a power law of remaining potentials, leading to p(t) = Σ +∞ e=0 Σ m j=1 r e x j (t -e) 6 , where the input value x(t-e) and the potential p(t) are functions depending on the current time t. The membrane potential integrates both current input values and what remains from previous inputs. As remaining input potentials decrease with time following a power law, inputs received a long time ago can nevertheless be neglected. Only remaining input potentials greater than a threshold error can be considered, i.e., r e ≥ . Thus only elapsed times e ≤ ln( ) ln(r) can be taken into account, where σ = ln( ) ln(r) is the integration time window, i.e., the period over which the neuron integrates past input values. For example, an error = 1% and a remaining coefficient r = 50% correspond to an integration window σ = 6.64. This means that, sliding the integration window of a width equal to σ, at each time t, no input older that e = 6.64 will be considered, leading to an error of = 1% in the membrane potential. The time-dependence of the membrane potential is not anymore infinite but bounded to [t-σ, t]. State changes need now to be finite. If we discretize each time step with t, e ∈ N 0 (leading to σ = σ = 6.64 = 7 for the previous example), the membrane potential p(t) consists of a sum

Σ m j=1 x j (t) + rΣ m j=1 x j (t -1) + r 2 Σ m j=1 x j (t -2) + r 3 Σ m j=1 x j (t -3) + . . . + r σ Σ m j=1 x j (t -σ), i.e., p(t) = Σ σ e=0 r e Σ m j=1
x j (t -e). Thanks to the previous time boundness and discreteness, each time t can be considered as a particular transition. The computation of the membrane potential now depends on a finite memory of maximum size m × (σ + 1), with m, σ ∈ N 0 .

A last simplification of the usual leaky integrate-and-fire model presented in Definition 2 concerns the real values of both membrane potential and synaptic weights. Indeed, real numbers are approximated by computers as floating-point values. However, rational numbers are needed to get efficient results from model checkers.

In our case, notice that this assumption well fits with remaining coefficients (that can easily be approximated by Taylor series or simple percentages).

Accounting for all the previous assumptions on usual leaky integrate-andfire neurons, the following definition can be provided for their mapping to synchronous reactive systems (finite state automata are proved to be equivalent to synchronous programs as Lustre or Esterel [START_REF] Berry | The esterel synchronous programming language and its mathematical semantics[END_REF]). Definition 3. A synchronous reactive neuron implements a leaky integrate and fire model as a finite state machine (FSM)

SRN i = (X i , Y i , S i , ∆ i , Λ i ), where X i = B m is the vector of boolean input values of size m; Y i = B is the boolean output value; S i = Q is the set of membrane potential values; ∆ i : X m×(σi+1) i → S i is the transition function defined as p i = ∆ i (X) = W X R, where
• Each past input value x ej ∈ X is reset (i.e., x ej = 0 for e ∈ {1, ..., σ i } and j ∈ {1, ..., m}) when p i ≥ τ i , with τ i ∈ Q,

• W = [w 1 , w 2 , . . . , w m ] is the vector of synaptic weights (each column corresponds to an input j ∈ {1, . . . , m} and w j ∈ Q),

• X =      x 10 x 11 • • • x 1σi x 20 x 21 • • • x 2σi . . . . . . . . . . . . x m0 x m1 • • • x mσi     
is a matrix of Boolean stored input values (each row corresponds to an input j ∈ {1, . . . , m} and each column to an elapsed time e i ∈ {0, . . . ,σ i } with σ i ∈ N 0 ), and

• R =      1 r i . . . r σi i     
is the vector of remaining coefficients with r i ∈ Q and r i ∈]0, 1].

Lastly, Λ i : S i → Y i is the output function, with Λ i (p i ) = 1 if p i ≥ τ i 0 otherwise.
This formalization allows for the characterization of each neuron through a parameter triplet (τ i , r i , σ i ) ∈ Q×Q×N 0 , i.e., the firing threshold τ i , the remaining coefficient r i , and the integration window σ i .

Encoding Neuronal Archetypes in Lustre

The basic archetypes we take into account are the following ones (see Fig. 1). -Simple series. It is a sequence of neurons where each element of the chain receives as input the output of the preceding one. The input (resp. output) of the first (resp. last) neuron is the input (resp. output) of the network. The spike emission of each neuron is constrained by the one of the preceding neuron. -Series with multiple outputs. It is a series where, at each time unit, we are interested in knowing the outputs of all the neurons (i.e., all the neurons are considered as output ones). -Parallel composition. There is a set of neurons receiving as input the output of a given neuron. All neurons working in parallel are considered as output ones. -Negative loop. It is a loop consisting of two neurons: the first neuron activates the second one while the latter inhibits the former one. The inhibited neuron is supposed to oscillate. -Inhibition of a behavior. There are two neurons, the first one inhibiting the second one. After a certain delay, the first neuron is supposed to be activated and the second one to be inhibited. -Contralateral inhibition. There are two or more neurons, each one inhibiting the other ones. The expected behavior is of the kind "winner takes all", that is, starting from a given time only one neuron becomes (and stays) activated and all the other ones are inhibited.

In the following we provide a Lustre implementation of neurons and archetypes. A Boolean neuron with one predecessor (that is, one input neuron), can be modeled as the Lustre node described in Program In the node neuron105 (where the firing threshold is set to 105), X is the Boolean flow representing the input signal of the neuron, w is the synaptic weight of the input edge, rvector is the vector containing the different values the remaining coefficient can take along the integration window (from the biggest to the smallest one), and the vector mem keeps trace of the received signals (from the current one to the one received at the time t -σ) 7 . More precisely, at each time unit the first column of vector mem contains the current input (multiplied by the synaptic weight of the input edge) and, for each i greater than 0, the value of the column i is defined as follows: (i) it equals 0 at the first time unit (initialization) and (ii) for all following time units it is reset to 0 in case of spike emission at the preceding time unit and it takes the previous time unit value of the column i -1 otherwise. Variable localS is used to introduce a delay in the spike emission.

The generalization to a node with m predecessors is straightforward. Thanks to the modularity of Lustre, archetypes can be easily encoded starting from basic neurons. As an example, a simple series composed of three neurons of type neuron105 is described in Program 2.

Program 2 Simple series of three neurons. In the node series3, each position of the vector chain refers to a different neuron of the chain. As far as the first neuron is concerned, it is enough to call the node neuron105 with the input of the series as input. For the other neurons of the chain, their behavior is modeled by calling neuron105 with the output of the preceding neuron as input. The output of the node is the one of the last neuron of the series.

Encoding and Verifying Temporal Properties of Archetypes in Lustre

The behavior of each archetype can be validated thanks to the use of model checkers such as Lesar, Nbac, Luke, Rantanplan, and kind2 (the last four ones have been used to deal with some properties involving integer constraints Lesar is not able to treat). For each archetype, one or two properties have been encoded as Lustre nodes and tested on some instances of the archetype. To illustrate our purpose, we show the encoding of the first two properties (the implementation of the other properties can be found in [START_REF] De Maria | Verification of Temporal Properties of Neuronal Archetypes Using Synchronous Models[END_REF]). Most of the properties are tested here for all possible inputs and one or more set(s) of parameters for the given archetype.

4.1 Simple Series (see Fig. 1(a))

Given two series with the same triplets of parameters (τ, r, σ) ∈ Q × Q × N 0 and the same synaptic weights, the first series being shorter than the second one, we want to check whether the first series is always in advance with respect to the second one. More precisely, the property we test is the following one: Let seriesA_sp (resp. seriesB_sp) be the Lustre node encoding the first (resp. second) series (corresponding neurons in the two series have the same parameter triplets). In the node prop1, C1 (resp. C2) keeps trace of the number of spikes emitted by the first (resp. second) series until the current time unit. The model checkers Lesar, Nbac, Luke, Rantanplan and kind2 verify whether, whatever is the value of the input flow variable X (which is common to the two series), the property is true, that is, C1 is greater or equal than C2.

Another interesting property concerning simple series is the following one:

Property 2.
[Comparison of series with different parameters] Given two series with different neuron parameters and different length, they always have the same behavior.

The node prop2 (described in Program 4) encodes such a property in Lustre.

Program 4 Observer of Property 2 node prop2 (X:bool) returns(S:bool); var s1,s2:bool; let s1=seriesA_dp(X); s2=seriesB_dp(X); S=(s1=s2); tel At each step, the output of the node is true if the output of the two series seriesA_dp and seriesB_dp is the same (provided that they receive the same input flow X). Such a property can be exploited in order to reduce a given neural network (if a given series has exactly the same behavior than a shorter one, it can be replaced by the second one). As an example, we found a series of 3 neurons showing the same behavior than a series of length 4 (neurons in the two series have different firing thresholds and synaptic weights).

Series with Multiple Outputs (see Fig. 1(b))

When dealing with a series with multiple outputs, we are interested in checking whether, soon or later, all the neurons of the sequence are able to emit a spike. It may not be the case if the parameters are not well chosen (for example, if the threshold of the first neuron is too high). The corresponding property formalized here is the following one: Property 3. [Firing ability in a series] Given a series with multiple outputs where the different neurons can have different parameters, there exists a time unit such that all the neurons have emitted.

Let prop3 be the node encoding the observer of Property 3. The output of prop3 becomes (and stays) true after all the neurons of the series have emitted at least one spike. As an example of property violation, we have found a series of length 4 where, even if a flow of 1 (encoded as true in Lustre) is given as input, the last neuron is never able to emit. Observe that, given a series where all the neurons are able to emit, prop3 only becomes true when the last neuron of the series emits a spike. In order to force the property to be immediately true, it is possible to take advantage of the node always_since from Lustre distribution library.

Parallel Composition (see Fig. 1(c))

We are interested in knowing a lower and an upper bound to the number of neurons that can emit a spike at each time unit. The lower (resp. upper) bound is not necessarily 0 (resp. the number of parallel neurons). More precisely, the property we test is the following one: Property 4. [Lower/upper firing bounds in a parallel composition] Given a parallel composition of neurons, all with the same parameters, at each time unit, the number of emitted spike is in between a given interval.

Let the output variable of the node encoding the parallel composition represent the global number of spikes emitted at each time unit by all the neurons in parallel. The observer of Property 4 checks whether the number of emitted spikes is always in between a lower bound and an upper bound. As an example, we have found a parallel composition of 3 neurons where the number of emitted spikes is always strictly lower than 3 (more precisely, it is always in between 0 and 2). This is due to the fact that, for one of the parallel neurons, the synaptic weight of the corresponding input edge is too low and it is never able to emit.

Negative Loop (see Fig. 1(d))

In this case the inhibited neuron is expected to oscillate. In Property 5 we express an oscillation with a period of two time units. Property 5. [Oscillation in a negative loop] Given a negative loop (where the two neurons do not necessarily have the same parameters), the inhibited neuron oscillates with a pattern of the form false, false, true, true.

Let Out be the output of the inhibited neuron of the Lustre node encoding the negative loop archetype. In the observer of Property 5, we check that (i) if Out is true, then it was false two time units ago and (ii) if Out is false then it was true two time units ago. For several parameters, if we inject only 1 as input of the archetype, such a property is satisfied. Observe that, to test the property satisfaction under some specific conditions, e.g., when the input variable X is equal to true, it is sufficient to introduce a new output variable SS defined as the disjunction of the current output variable S and the negation of the condition. (e.g., SS=S or X=false).

Inhibition of a Behavior (see Fig. 1(e))

To validate this archetype we need to verify that, at a certain instant, the inhibited neuron stops emitting spikes. In particular, the property we encoded is the following one: Property 6. [Fixed point inhibition] Given an inhibition archetype (where the two neurons do not necessarily have the same parameters), at a certain time the inhibited neuron can only emit false values.

The output of the observer of Property 6 is true if the variable representing the output of the inhibited neuron of the archetype cannot pass from false to true. For appropriate parameter values, if we inject only 1 values, such a property turns out to be true.

Contralateral Inhibition (see Fig. 1(f ))

For such an archetype the expected behavior is of the kind "winner takes all", that is, at a certain point only one neuron is activated and the other ones cannot emit spikes.

Property 7.

[Winner takes all in a contralateral inhibition] Given a contralateral inhibition archetype with two neurons (where the two neurons do not necessarily have the same parameters), at a given time, one neuron is activated and the other one is inhibited.

In the observer of Property 7 we test whether, at each time unit, one neuron is activated and the other one inhibited. Such a property turns out to be true for several parameters (if only 1 values are injected). Let w2 (resp. w4) be the synaptic weight of the inhibiting input edge of the first (resp. second) node. In Fig. 2, blue points represent the pairs (w2, w4) for which the property is verified starting from a time unit lower than or equal to 4 and red points are associated to the pairs for which the property is not verified within 10 time units (for some fixed parameter triplets).

Comparison of the Model Checkers

A synthesis of the outputs of the five model checkers is summarized for each property in Notice that, when a model checker gives a negative answer, it does not necessarily mean that the property is false; it can be an indication of the fact that the model checker is not able to conclude. In this experiment, Lesar has difficulties to handle complex integer constraints. Nbac goes further but it is quickly stopped by the polyhedra approach. Luke and its extension Rantanplan give similar results with sometimes a very long computation time. kind2 works quickly and it is able to prove more general properties than Luke and Rantanplan. For instance, Luke and Rantanplan allow for the identification of the pair of weights which stabilize the "Contralateral inhibition" (see Fig. 2) while kind2 is able to straightly give us an infinite set of pair solutions. For the sake of completeness, we also tested the nuXmv model checker [START_REF]Nuxmv webpage[END_REF] but perhaps we could not find the good abstraction (neither too coarse, nor too thorough), so we could not get satisfying results.

Discussion and Future Work

In this work, we show how the synchronous language Lustre can be an effective tool to model, specify, and verify neuronal networks. More precisely, we illustrate how some basic neuronal archetypes and their expected properties can be encoded as Lustre nodes and verified thanks to the use of model checkers. For each archetype, we propose one or two representative properties that have been identified after deep discussions with neurophysiologists and, in particular, with the last author of this paper. As a first future work, we intend to propose a more general version of some properties (e.g., expressing oscillation without exactly knowing its period).

We choose to use Lustre because its declarative syntax is more adapted to our class of problems than an imperative language such as Esterel and because several model checkers integrating the symbolic manipulation of integer constraints are at Lustre user's disposition. However, these motivations do not prevent us from considering to use Light-Esterel in the future; the third and fourth author of this work are actually working on extending the expressivity of the declarative part of this language and developing a dedicated model checker. Particularly, this new model checker should integrate a new way to characterize and verify properties based on Linear Decision Diagram (LDD). This representation would allow to identify input parameter intervals of values for which a property holds.

As far as we know, this work constitutes the first attempt to automatically verify the temporal properties of fundamental neuronal archetypes in terms of neuronal information processing (e.g. a negative loop with certain parameters presents a certain oscillating behavior). From there, we will now be able to apply this new approach to all the possible archetypes of 2, 3 or more neurons, up to falling on archetypes of archetypes. One of the questions to ask then will be: are the properties of these archetypes of archetypes simply an addition of the individual constituting archetypes properties or something more? Another one will be: can we understand the computational properties of large ensembles of neurons simply as the coupling of the properties of individual archetypes, as it is for the alphabet and words, or is there something more again?

Fig. 1 .

 1 Fig. 1. The basic neuronal archetypes.

8 Fig. 2 .

 82 Fig. 2. Verification of prop7 for the different values of (w2, w4).

  1.

	Program 1 Basic neuron node.
	node neuron105 (X:bool) returns(S:bool);
	var
	V:int;
	threshold:int;
	w:int;
	rvector: int^5;
	mem:int^1*5;
	localS: bool;
	let
	w=10; threshold=105; rvector=[10,5,3,2,1];
	mem[0]=if X then w else 0;
	mem[1..4]=0^4->if pre(S) then 0^4 else pre(mem[0..3]);
	V=mem[0]*rvector[0]+mem[1]*rvector[1]+mem[2]*rvector[2]
	+mem[3]*rvector[3]+mem[4]*rvector[4];
	localS=(V>=threshold);
	S= false -> pre(localS);
	tel

  Property 1. [Comparison of series with same parameters] Given two series with the same neuron parameters and different length (i.e., with a different number of neurons), at each step, the number of spikes emitted by the shorter series is greater or equal than the number of spikes emitted by the longer one.

	The node prop1 (described in Program 3) expresses an observer of Property 1
	in Lustre.
	Program 3 Observer of Property 1
	node prop1(X:bool) returns(S:bool);
	var
	A1,A2:bool;
	C1,C2;
	let
	A1=seriesA_sp(X);
	A2=seriesB_sp(X);
	C1=bool2int(A1)->if A1 then pre(C1)+1 else pre(C1);
	C2=bool2int(A2)->if A2 then pre(C2)+1 else pre(C2);
	S=(C1-C2)>=0;
	tel
	.

Table 1 :

 1

		lesar	nbac	luke	rantanplan kind2
	Simple series (prop1)	No	Yes	very long time!	Yes	Yes
	Simple series (prop2)	No exit before!	Yes	very long time! Yes
	Series with multiple outputs No exit before!	Yes	Yes	Yes
	Parallel composition	No exit before!	Yes	Yes	Yes
	Negative loop	No exit before!	Yes	Yes	Yes
	Inhibition of a behavior	No	Yes	Yes	Yes	Yes
	Contralateral inhibition	No	Yes	Yes	Yes	Yes

Table 1 .

 1 Comparison of the five model checkers

For the sake of simplicity, we assume that all the synaptic weights are equal to 1; supposing that neuron i has m predecessors, we write Σ m j=1 xj to denote Σ j∈P red(i) xj; when there is no ambiguity on the neuron index, we do not indicate it.

Observe that all the parameters are multiplied by 10 in order to only deal with integer numbers (and thus to be able to use all the model checkers available to Lustre).

Acknowledgements

The authors would like to thank Gérard Berry for an inspiring talk at the Collège de France (concerning the checking of temporal properties of neuronal structures) as well as for having indicated us the researchers competent at the use of synchronous programming language libraries (in Sophia Antipolis).


Natalia Sergeeva-Chollet
email: natalia.sergeeva-chollet@cea.fr

Matthias Pelkner

Thomas Erthner

Marc Kreutzbruck

Claude Fermon

Jean-Marc Decitre

Johannes Paul

Filipe Cardoso

Susana Cardoso

Paulo Freitas

Diogo M Caetano

Jorge Fernandes

Moisés Piedade

Eddy Current Probes Based on Magnetoresistive Array Sensors as Receivers

Eddy Current (EC) Technique is a powerful method for detection of surface notches and of buried flaws during inspection of metallic parts. This technique is used for inspection at different industrial domains like aeronautics and nuclear one. Classical winding coils are the most commonly used EC sensors. Nevertheless, when the size of flaws decreases or the defect is rather buried deep inside the material, traditional winding coil probes turn out to reach their limits. For this reason, other technologies are investigated to improve this technique.

Magnetoresistive sensors present the advantages of flat frequency response and dimensions at the micron size. These sensors are hence very attractive for the detection of buried defects that require low frequencies because of skin depth effect. Also, they are suitable for small surface defects due to high spatial resolution because of their manufacturing down to one hundred µm without losing their field sensitivity.

An optimization of such probes based on magnetoresistive sensors (GMR -giant magnetoresistive and MTJmagnetic tunnel juntions) specially designed to be integrated into an eddy current probe has been experimentally studied. Measurements using MR array probes consisting of 32 GMR-and MTJ-elements, an ASIC, subsequent readout components, and emitters for EC generating inside the material under test are shown. These probes have been developed in the IMAGIC-project1 for detection and imaging of surface breaking defects and buried flaws. The performances of developed probes have been investigated for several mock-ups.

Introduction

Eddy Current (EC) technique is widespread, ensuring buried or surface-breaking flaws detection in conductive materials. However, when the crack's size decreases or the flaws are rather deep, using of conventional EC winding coil probes becomes rather difficult. Probes with magnetoresistive sensors as receivers are investigated as a solution [START_REF] Decitre | New design of Eddy Current Probes[END_REF][START_REF] Marchand | Flexible and array eddy current probes for fast inspection of complex parts[END_REF][START_REF] Dogarun | [END_REF][4]. Magnetoresistive sensors are attractive for EC testing because of their flat frequency response for a large frequency range and high sensitivity. At low frequencies they are more sensitive than conventional winding coils of fixed size. Thus, GMR (Giant Magneto Resistance) sensors are promising for low frequency application, i.e. sub-surface flaws detection, because of the skin depth effect [4][5][START_REF] Pelkner | MR-based eddy current probe design for hidden defects[END_REF]. In order to increase the spatial resolution of detection GMR and TMR (Tunnel Magneto Resistance) could be used [START_REF] Wincheski | [END_REF]. These sensors show good field sensitivity and spatial resolution due to the possibility of their miniaturization during fabrication. Moreover arrays of 32 or more elements could be realized in order to decrease inspection time.

In this paper testing results of GMR/TMR based probes for buried flaws and surface cracks are shown. These probes have been developed in the IMAGIC-project ("Integrated Magnetic imagery based on spIntronics Components", 2011 -2014, EU-project reference: 288381) [START_REF] Pelkner | MR-based eddy current probe design for hidden defects[END_REF][START_REF] Sergeeva-Chollet | Development of Eddy Current probes based on magnetoresistive sensors arrays[END_REF][START_REF] Ribes | Results of MR based ET probes for buried flaw detection over different metallic materials[END_REF]. In the developed probes ASICs (application-specified integrated circuit) for processing of 32 MR-elements sensor signals are placed on board of the PCBs (Printed circuit board) [START_REF] Caetano | A CMOS ASIC for Precise Reading of a Magnetoresistive Sensor Array for NDT[END_REF]. Steel, Aluminum and Titanium samples have been investigated. In case of Aluminum and Steel buried flaws detection has been studied. In case of Titanium, a material with lower conductivity, surface defects in micron range have been tested [START_REF] Pelkner | Eddy Current testing with high-spatial resolution probes using MR arrays as receiver[END_REF].

MR probe design

During IMAGIC-project two different types of GMR/TMR EC probes for buried flaws and small surface breaking cracks detection have been developed. Several geometries of excitation coils have been investigated for these two applications [START_REF] Pelkner | MR-based eddy current probe design for hidden defects[END_REF][START_REF] Sergeeva-Chollet | Development of Eddy Current probes based on magnetoresistive sensors arrays[END_REF]. Simulations of eddy current distribution in materials of interest have been made. These simulations are made using two different simulation tools: semi-analytical model of CIVA software developed in CEA LIST and commercial FEM-software OPERA. Parametric studies for EC probes optimization are made using CIVA. OPERA is employed for magnetic and current distribution.

First, optimization of emitter has been made. Different coil geometries had been investigated: single wire coil in planar alignment, double coil in planar alignment and single wire coil in perpendicular alignment (see Fig. 1). Figure 1 shows the general lay-out of different geometries, current density distribution within the material and current distribution for different frequencies from 100Hz to 8000Hz illustrating the penetration depth.

Based on this study double coil geometry of the emitter has been chosen for buried flaws and sub-surface flaws detection because of the larger penetration depth. The optimal distance between the coils has been found by simulations.

For surface cracks' detections one wire excitation coil has been selected. This arrangement has shown to be most advantageous for high excitation frequencies.

For both applications the emitter frequency has been adapted. In case of small surface breaking defects the frequency should be in the order of some MHz. For buried flaws low frequencies have to be used to generate a sufficiently high eddy current density to detect buried flaws, the simulations have been made for frequency optimization for different depth according to the application cases. For surface cracks' detection GMR/TMR sensor arrays of small size in the order of 60 µm for each element have been developed as receivers. Arrays with 32 and more elements have been fabricated.

One wire has been chosen as emitter for these probes. The advantages of such emitter geometry are following: it could be placed at the same PCB as receiver arrays and ASIC (Fig. 3), and it could be very close to the surface of testing material that will reduce the excitation loss. MR sensor array is placed just behind the wire in order to be placed also very close to the surface of material under test. Emitter consists of a bonding ribbon and is electrically connected to PCB.

Sensors and ASIC are connected with wire bonding and ASIC is connected with PCB also due to wire bonding. Emitter, sensor array, and ASIC are protected by an epoxy resin.

Performances of EC probes based on TMR arrays with a high number of small MR elements have been studied. Spatial resolution and the possibility of detection of µm-sized surface cracks have been evaluated. The excitation frequency f = 1.3 MHz has been chosen for the inspection with TMR probe. The gain of 40 dB has been used for pre-amplification of signals. NI system has been used for recording data [START_REF] Pelkner | Eddy Current testing with high-spatial resolution probes using MR arrays as receiver[END_REF].

Measurements have been performed on Ti mock-up with the notch of following dimensions: length × width × depth = 1000 × 30 × 50 µm 3 .

The extremities of defect are seen as the normal component of the field is detected. This notch is well detected with SNR of 8 dB (Fig. 4).

Conclusions

During the IMAGIC-project EC-probes based on TMR and GMR probes with adapted ASIC have been developed. Performance of these probes have been evaluated in cases of buried flaws and surface cracks detection.

For buried flaws application, developed probes have demonstrated their capability of detection. Defects at ligament of 4.5 mm in Aluminum mock-up are well detected. However, more investigations concerning number of layers of emitter coils should be done in order to increase the performance of developed probes.

For surface cracks detection application the obtained results are very promising in terms of the possibility of detection and spatial resolution.

Using of MRarray based probes will reduce testing time with the possibility of greater area inspection at one time.

Optimization of electronics (ASIC and supporting components, sensing elements and emitter) in the case of buried flaws detection is a subject of future work of probes development.

Fig. 2 .

 2 Fig.2. Probe for buried flaws detection (a) scheme emitter and receiver position (b) Photo of the IMAGIC MR probe for buried flaws detection

Fig. 3 .. Results 3 . 1 Fig. 3 .

 3313 Fig.3. Probe for surface cracks detection (a) scheme emitter, receiver and electronics position (b) Photo of the IMAGIC MR probe for surface cracks detection

Fig. 4 .

 4 Fig.4. EC testing of Ti sample with artificial notch: l × w × d =1000 × 30 × 50 µm 3

Acknowledgement

This work was supported by the European project IMAGIC FP7 288381. We would like to acknowledge all partners of the consortium for their efficient work -Sensitec GmbH, Tecnatom S.A., Airbus Group, INESC-ID and INESC-MN.

1The IMAGIC-project ("Integrated Magnetic imagery based on spIntronics Components", 2011 -2014, project reference: 288381) was funded by the European Commission, Seventh Framework Programme. Further partners involved in the consortium beside BAM and CEA were INESC-ID and INESC-MN (Portugal), Sensitec GmbH (Germany), Tecnatom S.A. (Spain), and Airbus Group (France). //ndt.net/?id=19262

Vertical detection has been proposed after analyzing of receiver/emitter coupling, signature of flaws and signal answer obtained by CIVA and OPERA for both high frequency and low frequency applications.

During the project, the consortium has developed receivers of GMR and TMR sensors arrays for buried flaws and for small surface breaking cracks detection of different size. All arrays are sensitive to the normal component of magnetic field. Sensitivity of GMR elements is 20V/T. Receivers based on TMR sensors consist of arrays of MgO-based magnetic tunnel junctions with sensitivity of 150V/T measured with 2V bias.

IMAGIC consortium also has developed ASICs in order to process the signals coming from a high number of MR-elements [START_REF] Caetano | A CMOS ASIC for Precise Reading of a Magnetoresistive Sensor Array for NDT[END_REF]. The ASIC comprises of amplifying and multiplexing among other functions. Additional electronics has been placed onto PCB of the prototypes to adjust sensor signals and amplification gain.

Probes for buried flaws detection

The emitter coil is realized by printed circuit technology. Double coil emitter has been chosen following the simulation results. PCB with MR sensor array and electronics is fixed perpendicular to the PCB with emitter coils (Fig. 2). The MR sensing elements are placed exactly in the center between two coils otherwise the emitter field is detected by the sensor immediately. MR elements are sensitive to the normal component of magnetic field. To avoid the interference between emitter field and sensor, a compensation circuit is integrated on the emitter coil to balance or unbalance the current between the two coils.

Arrays of size of 1mm for each element have been fabricated for this application. Sensors are connected with bonding wires and protected with epoxy resin.

Performances of the developed probes for detection of buried flaws have been evaluated.