Anais Guignard
email: anais.guignard@lurpa.ens-cachan.fr

Jean-Marc Faure
email: jean-marc.faure@lurpa.ens-cachan.fr

A conformance relation for model-based testing of PLC

Keywords: Finite state machine, Programmable logic controller, Conformance test, Test sequence, Applications 1

This paper focuses on the execution of conformance testing of PLC with I/O scanning which executes a control code; it is assumed that the test sequence has been built from a finite state machine that represents the specified behavior. It is first shown that the conformance relation which allows to decide whether the implementation conforms to the specification or not must be defined from a sequence of observations, and not from only one observation, to take into account the delays introduced by the I/O scanning. Then, a second conformance relation is proposed to avoid that asynchronous detection of synchronous input changes leads to biased or non-valid verdicts; this new relation is defined from the analysis of concurrent transitions and accepted sequences in the specification model.

INTRODUCTION

Model-based conformance testing is a formal analysis method that aims to check whether an implementation, seen as a black-box with inputs and outputs, behaves as specified. Several worthwhile theoretical results have been already obtained in this field by using specification models in the form of finite state machines (FSM) [START_REF] Lee | Principles and methods of testing finite state machines-a survey[END_REF], [START_REF] Li | Model-based automatic test generation for simulink/stateflow using extended finite automaton[END_REF]), transition systems [START_REF] Brinksma | Testing transition systems: An annotated bibliography[END_REF], [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF]) or Petri nets [START_REF] Bochmann | Testing k-safe petri nets[END_REF]). Globally, these works have shown how errors in a model of the implementation can be detected by observing its output sequences in response to input sequences.

The issue of conformance test of real devices, like Programmable Logic Controllers (PLC 1 ) that execute a control code, has been addressed more recently [START_REF] Provost | Translating Grafcet specifications into Mealy machines for conformance test purposes[END_REF]). This approach benefits from the previous results on testing of FSM (or Mealy machines) and is decomposed in two phases:

• Construction of a test sequence from the specification model; • Execution of this sequence by a test-bench, electronic device that sends input signals to the PLC and observes its responses (Fig. 1); comparison of these responses to those expected according to a conformance relation permits to emit a verdict. It must be underlined that this test is non-invasive. No piece of code or electronic component must be introduced in the PLC for test reasons; the PLC is tested in its real operation conditions. When critical systems are considered, a usual objective to build the test sequence is to cross at least once every transition of the machine. To limit the length of this sequence, therefore the duration of the test execution, an optimization criterion is commonly introduced: the test sequence must be minimum-length; the algorithm proposed in [START_REF] Naito | Fault detection for sequential machines by transitions tours[END_REF] can be then selected to build the sequence from the specification model. However, the obtained sequence is a MIC (Multiple Input Change) sequence, i.e. several input values may be changed synchronously by the test-bench from one test step to the following one. This feature may lead to erroneous test verdicts as described in Provost et al. (2011a) because synchronous input changes may be detected as asynchronous by the PLC during test execution.

To solve this issue, a new algorithm to construct the test sequence has been presented in [START_REF] Provost | SICtestability of sequential logic controllers[END_REF]; the aim of this algorithm is to build a SIC (Single Input Change) sequence to avoid asynchronous detections of synchronous input changes. Unfortunately, a SIC test sequence does not generally cover at least once every transition of the machine; some transitions are not testable with such a sequence. To meet the test objective for critical systems, MIC test steps must be added at the end of the SIC sequence and the above-mentioned problem remains for these steps.

The objective of this paper is to propose a conformance relation which permits to provide a correct verdict even in case of asynchronous detection of synchronous input changes. This relation will be applicable when using a (fully or partially) MIC sequence. The paper is organized as follows. The section 2 presents a reminder on test sequence construction from a Mealy machine. A first conformance relation based on sequences of observations is defined in section 3. As it is shown in section 4 that this relation leads to an erroneous verdict when synchronous input changes are seen as asynchronous by the PLC, the appropriate conformance relation for testing of PLC is presented at section 5 while section 6 proposes different solutions to pursue the test after this happened. Concluding remarks and perspectives for further work are drawn up in the last section.

BACKGROUND

Programmable Logic Controllers

This work focuses on testing of mono-tasking PLC which are commonly integrated in automated systems. In this case, the control code is executed according to a cyclic I/O scanning that can be periodic or not and comprises 4 phases:

• Inputs reading,

• Internal and output variables computation,

• Outputs updating,

• Waiting time until the end of the period, if the cycle is periodic.2

It must be also reminded that a PLC does not receive (emit) input (output) events but input and output signals.

Events can be built by sampling the signals and considering either the rising and falling edges of one input (output) signal or the changes of the whole set of inputs (outputs).

The cyclic I/O scanning may provoke two phenomena that can hinder the implementation of theoretical results on PLC:

• synchronisation of asynchronous input changes,

• desynchronization of synchronous input changes.

The first phenomenon occurs when several inputs are modified asynchronously during the same cycle; these changes will be detected synchronously at the beginning of the next cycle. This issue has been already studied by authors who focused on implementation of the SCT (supervisory control theory) [START_REF] Fabian | PLC-based implementation of supervisory control for discrete event systems[END_REF]). The second phenomenon has been presented and quantified in (Provost et al. (2011a)). It occurs when synchronous changes of several inputs happen during the input reading phase; some changes may be detected during this phase and other ones only at the next cycle (Fig. 2).

Fig. 2. Asynchronous detection of synchronous input changes

As during the execution of a conformance test, the inputs are changed synchronously by the test-bench, only the second phenomenon will be considered in what follows.

Test sequence construction

This work assumes that the specification is described by a Mealy machine; this formalism is widespread to represent the specifications of non-timed systems in conformance testing. Formally, a Mealy machine is a 6-tuple M = (I M , O M , S, s init , δ, λ) where:

• I M is the input alphabet • O M is the output alphabet • S is the set of states s ∈ S • s init ∈ S is the initial state • δ : S × I M → S
M (O M ) is |I M | = 2 |V I | (|O M | = 2 |V O |
) and each element of the input (output) alphabet is represented by a minterm3 defined on V I (V O ). Hence, every input (output) event of the model corresponds to a combination of the input (output) variables of the PLC

The following assumptions are to be made to build a conformance test sequence from this specification model:

• The transition function is complete and deterministic (i.e. every transition δ(s × i M ) with s ∈ S and i M ∈ I M is defined once and only once). • Each state is distinguishable from the other ones by observation of the output. • There is no transient evolution, i.e. no input change causes successive changes of state or emitted output. This implies that for any transition leading from an upstream state to a downstream state and labeled by a given input event, there is a self-loop on the downstream state with the same input event.

The basic example presented at Fig. 3 will be used to illustrate the results of this paper. This model represents the specified behavior of a PLC with two input variables V I = {a, b} and one output variable V O = {o}. The input alphabet of the specification is thus I M = {a.b, a.b, a.b, a.b}4 and the output alphabet O M = {o, o}. This specification contains 2 states S = {s 1 , s 2 } with s init = s 1 and 8 transitions.

Fig. 3. A basic example of specification

The three assumptions introduced are verified on this Mealy machine:

• The transition function is complete and deterministic.

• When the state s 1 (s 2 ) is active, the output of the PLC is F alse (T rue). • It can be easily checked that there is no transient evolution. The state s 2 , for instance, is reached from s 1 when the input event of the machine is a.b (the two inputs of the PLC are T rue) and there is a self-loop on s 2 with this input event.

A test sequence can be then built from this specification. Formally, a test sequence is an ordered list of elementary test steps et = (s u , I exp , s d , O exp ) where:

• s u × s d ∈ S × S • I exp ∈ I M , O exp ∈ O M • s d = δ(s u , I exp ) • O exp = λ(s u , I exp )
A test step represents a transition from an upstream state s u to a downstream state s d provoked by an input event I exp and during which the output event O exp is emitted.

It must be noted that, as there is no transient evolution, it is possible to test two successive transitions of the Mealy machine with only one input event, i.e. one change of the inputs of the PLC: the transition (s u , I exp , s d , O exp ) and the transition (s d , I exp , s d , O exp ), self-loop on the downstream state of the previous transition. In the case of the example of Fig. 3, it is possible for instance to test the transitions (s 1 , a.b, s 2 , o) and (s 2 , a.b, s 2 , o) by using the input event a.b from the state s 1 . This strategy will be used for every self-loop on a state which is labeled by an input event that is also the label of an incoming transition of this state.

The test sequence must be initializable, i.e. the upstream state of the first test step must be the initial state, and consistent, i.e. the upstream state of any step, except the first one, must be identical to the downstream state of the previous state. An initializable and consistent test Mealy machine where only some states and transitions are represented; each transition is labeled with a couple of input event/output event (I i /O i ) where I i ∈ I M and O i ∈ O M . More precisely, the following test sequence will be considered: 4) and it will be assumed that this sequence is MIC, i.e. that several inputs of the PLC may be changed when the input event is changed from I i to I j or from I j to I t . • The test bench applies the input combination I exp to the logic inputs of the PLC under test. • Then, the test bench observes the output combinations emitted by the PLC. This observation phase must be long enough to permit all output computations and updates to be finished. As the maximal value of the causality delay, delay between the date of an input combination change and the date of the corresponding change of the output combination is two PLC cycles5 , the duration of this phase must be at least equal to two PLC periods, for a periodic mode, or two times the maximal value of the PLC cycle, for a cyclic mode. Moreover, the observed output combinations are obtained by sampling the output signals of the PLC; the sampling frequency must be high enough to guarantee that at least one combination is observed for every cycle so that every change of the output combination is observed. • At the end of the observation phase, the observed sequence is compared to the expected one according to a given conformance relation. The Fig. 5 shows, for the second test step of (4) and for several PLC cycles, the input combinations applied to the PLC Fig. 5a, as well as the input combinations read by the PLC Fig. 5b and the observable output combinations Fig. 5c) by assuming that the PLC behaves as specified, i.e. the implementation conforms to the specification. It is reminded that the inputs of a PLC are read at the beginning of each cycle and the outputs updated at the end of this cycle. It matters also to underline that the input combinations read by the PLC are not observable because the test is non-invasive; they are only represented in this figure to explain from which input combinations the observable combinations are computed.

T S = ((s 0 , I i , s 1 , O i ), (s 1 , I j , s 2 , O j ), (s 2 , I t , s 3 , O t )) (

Fig. 5. Expected, read and observable combinations

As the test-bench is not synchronized with the PLC, the expected input combination is changed at any date during a PLC cycle. This input combination is read by the PLC at the beginning of the following cycle and the corresponding output combination is updated at the end of this cycle. The expected input combination remains unchanged during a given number of cycles; the minimal value of this number is equal to 3 according to the above discussion.

Conformance relation

A Mealy machine that represents an implementation conforms to another machine that represents the specification if and only if O obs is equal to O exp for every test step. This simple theoretical conformance relation cannot be directly applied for conformance testing of PLC because the observable output combination O obs changes during one experimental test step as shown at Fig. 5. A first solution would be to consider only the last output combination observed at the end of the observation phase but this solution does not permit to distinguish a correct evolution from s u to s d through the considered transition to a sequence of two transitions from s u to s d via a third state s ′ . This is why a solution which is based on the sequence of observed output combinations will be proposed; this sequence6 :

σ Obs = (O obs1 , ..., O obsn ) where ∀i ∈ N * , O obsi ∈ O M (5)
is composed of the n (n ∈ N * , n ≥ 3) output combinations observed during this experimental test step.

A first conformance relation for a PLC can be then defined.

Definition 1.

Let et c = (s b , I j , s c , O j ) be the current test step Let et p = (s a , I i , s b , O i ) be the previous test step The implementation conforms to the specification if for every test step: If s b = s c : It exists k ∈ N * such as k < n and:

• If k > 1: ∀l ∈ N * such as l < k, O obs l = O i , • O obs k = O j • ∀m ∈ N * such as k < m ≤ n, O obsm = O j If s b = s c : ∀k ∈ N * such as k ≤ n, O obs k = O j
This relation means that, to declare that an implementation conforms to a specification, the sequence of output combinations observed during every experimental test step must be composed of a sequence of identical combinations that correspond to the expected output combination for the current test step (O j in Fig. 5) that may be preceded (if s b = s c and k > 1) by a subsequence of identical combinations that correspond to the expected output combination for the previous test step (O i in Fig. 5). This relation will be illustrated on the example of Fig. 3 by using the test sequence (1); it will be assumed for this example that every experimental test step lasts three PLC cycles and that one output combination is observed for every cycle. Hence, n will be equal to 3.

• Therefore, Definition 1, which is based only on analysis of a sequence of observations, is not sufficient to separate non-conformance cases from evolutions due to concurrent transitions in case of asynchronous detection of synchronous input changes; a more complete definition of a conformance relation that permits to distinguish these two cases will be given in section 5. It is necessary to study how a sequence of observations is modified when a transition which is concurrent to the considered transition is fired, however; this is the aim of the next section.

IMPACT OF AN ASYNCHRONOUS DETECTION OF SYNCHRONOUS INPUT CHANGES

An example of sequence of output combinations that can be observed when synchronous changes of the inputs of the PLC are detected as asynchronous, for the second test step of (4) and always assuming that the implementation behaves as specified (the PLC code is correct), is presented at Fig. 6. While the input combination sent to the PLC is I j , the combinations read by the PLC are successively I l (at the beginning of the cycle (k + 1)) then I j (at the beginning of the cycle (k + 2)). If several inputs are changed from I i to I j and these changes occur during the input reading phase, they may be indeed detected at two successive cycles and a combination I l is used to compute the output combination during the cycle (k + 1).

If p variables are changed from I i to I j , this unplanned input combination is obtained from I i by changing only a subset of these variables; changing the remaining ones in I l provides I j . Fig. 6. Sequence of observable combinations when several synchronous input changes are detected as asynchronous

From this sequence of read input combinations, a correct implementation will emit the sequence (O i , O l , O m ) that corresponds to the successive firing of the transitions from s 1 to s 4 and from s 4 to s 5 . As the expected output sequence is (O i ,O j ,O j ) the relation defined at the previous section will deliver a negative verdict: the implementation does not conform with the specification. This verdict is biased, i.e. a correct implementation is declared flawed (false negative).

A non-valid verdict (a flawed implementation is declared correct (false positive)) is also possible, as illustrated at the Fig. 7. This machine represents a flawed implementation if the specification is the model depicted at Fig. 4; however, the sequence observed will be (O i ,O j ,O j ) with the input sequence of Fig. 6 and the verdict will be positive.

Fig. 7. A model of an erroneous implementation

To avoid these erroneous verdicts, the conformance relation must be modified as explained in the next section.

AN APPROPRIATE CONFORMANCE RELATION

The principle of the new conformance relation is not to limit the comparison of the sequence of observations with only one sequence, as in Definition 1, but, if this first comparison is negative, with other sequences which are possible in case of asynchronous detection of synchronous PLC input changes. Therefore, this new relation is an extension of Definition 1 by adding a supplementary comparison phase. The aim of this phase is to check whether the sequence of observations may be obtained from the current state by firing in the specification a sequence of two transitions such that:

• the first transition is labeled by an input event which can be obtained from the expected event of the previous elementary test step (I i in the discussion of the previous section) by changing a subset of the variables which are changed when this event is replaced by that of the considered test step (I j in the discussion of the previous section); • the second transition is labeled by the expected input event of the considered test step.

Definition

From the non-formal definition above, a formal definition of the appropriate conformance relation for conformance test of PLC can be given. It is assumed that there is one observed output combination per PLC cycle in σ Obs .

Definition 2.

Let et c = (s b , I j , s c , O j ) be the current test step. Let et p = (s a , I i , s b , O i ) be the previous test step.

The implementation conforms to the specification if for every test step there is:

Either: If s b = s c : It exists k ∈ N * such
as k < n and:

• If k > 1: ∀l ∈ N * such as l < k, O obs l = O i , • O obs k = O j • ∀m ∈ N * such as k < m ≤ n, O obsm = O j If s b = s c : ∀k ∈ N * such as k ≤ n, O obs k = O j
Or: It exists k ∈ N * such as:

• k < n -1, • If k > 1, ∀l ∈ N * such as l < k, O obs l = O i , • It exists I x ∈ I M such as: • I x \I i ∪ I i \I x ⊂ I i \I j ∪ I j \I i , • λ(s b , I x ) = O obs k • Let s = δ(s b , I x ) be the downstream state of the transition, • It exists a transition such as λ(s, I j ) = O obs k +1 • and ∀m ∈ N * such as k + 1 < m ≤ n, O obsm = O obs k +1
This conformance relation is split into two parts. The first one is identical to Definition 1. If the verdict is negative after this first comparison, a second analysis is performed. The transitions that start from the upstream state of the considered test step (s b ) and which are labeled with input events that are intermediate combinations (I x ) between I i and I j are first searched. If it is possible by firing one of these transitions to emit an output event that corresponds to the k th observation and to reach a state s from which a transition labeled by the couple of events I j /O obs k+1 , where O obsk+1 is the (k + 1) th observation, is possible and that leads to a state s ′ with a self-loop with this same label, the verdict is positive.

The intermediate input combinations are defined by the expression

I x \I i ∪ I i \I x ⊂ I i \I j ∪ I j \I i (6)
where I 1 \I 2 is the set of PLC input variables which are T rue in I 1 and not in I 2 . Hence, the term I x \I i (I i \I x ) represents the set of variables which are T rue in I x (I i ) and not in I i (I x ). The disjunction of these two sets must be a subset of the set of variables changed from I i to I j .

These notations can be illustrated on the example of Fig. 3. At last, it must be noted that Definition 2 requires a longer observation phase than Definition 1 because it is based on a sequence of three firings: the first one caused by the intermediate input combination, the second one by the expected input combination and the latter one that corresponds to a self-loop on the final state of this sequence, while at most two firings were considered in Definition 1. As the causality delay is always the same, the observation phase must last at least four PLC cycles. This increased duration is the price to pay to avoid erroneous test verdicts, by distinguishing the unexpected observed sequences which come from errors in the implementation from those which are provoked by asynchronous detection of synchronous changes of the PLC inputs.

If I i =

Illustration

This relation may be applied to the third step of the test sequence (1) already analyzed according to Definition 1 in subsection 3.2. As this was the case in this section, it is assumed that the observed sequence is (o, o, o, o) while (o, o, o, o) is expected because the objective of this step is to test the self-loop on s 2 that corresponds to the label (a.b/o). This observed sequence will be interpreted with Definition 2 as the successive firings of the transition from s 2 to s 1 then of the self-loop on s 1 that corresponds to the input combination a.b; the test verdict will be positive. This verdict is correct because the synchronous changes of a and b from the second to the third test step may be detected as asynchronous and the intermediate input combination will be a.b or a.b during one PLC cycle; an implementation that conforms to the specification (Fig. 3) will then fire the transition from s 2 to s 1 then the self-loop on s 1 .

In other words, the new definition provides a positive verdict if the observed sequence is accepted by the specification even if it is not the one expected because synchronous input changes have been detected by the PLC as asynchronous. If the sequence is not accepted, a negative verdict must be obviously delivered. If for instance, for the third step of the test sequence (1), the observed sequence from state s 2 is (o, o, o, o), the verdict is negative because this sequence cannot be obtained in the model of Fig. 3.

DISCUSSION

The definition proposed in subsection 5.1 permits that erroneous verdicts are avoided whatever the way that the PLC input changes are detected. However, when an accepted sequence of observations, which is not the one expected, is found, the test sequence built off-line cannot be pursued because the active state is no more the one that was planned; in the first example of subsection 5.2, this state is s 1 while s 2 is expected as the upstream state of the next test step.

Three solutions can be then considered:

• a test sequence that covers every transition which has not been tested is recomputed from the new active state (this state becomes the initial state for test sequence construction); • the initial test sequence that has been built off-line prior to test execution is kept but the next test step will start from the new active state; • a partial sequence that starts from the new active state and ends at the state where synchronous input changes have been detected as asynchronous is determined; the initial test sequence is executed again, once the latter state reached.

In the rest of this section the pros and cons of these solutions will be discussed and illustrated. This discussion will be presented assuming that a test step et j = (s b , I j , s c , O j ) has been executed and that a desynchronization phenomenon lead to s new as active state.

Recomputation of a new test sequence from s new

In this case, a new sequence starting from s new and covering at least once every transition which has not been previously tested is built. This solution is always possible if the set of transitions which have been already tested during the test steps et 1 to et j-1 has been stored.

On the considered example of the test sequence (1) executed as explained in subsection 5.2, the test steps et 1 and et 2 have been correctly performed; hence only 6 transitions remain to be tested. The new test sequence, from s new = s 1 , to be executed by the test-bench is:

T S α =((s 1 , a.b, s 2 , o), (s 2 , a.b, s 2 , o), (s 2 , a.b, s 1 , o), (s 1 , a.b, s 2 , o), (s 2 , a.b, s 1 , o)) (7
It must be noted that the test sequences ( 7) and ( 8) are identical ; as no recomputation of a test sequence is necessary to build (8), the second solution is preferable.

Coming back to the previous test step

This solution may be applied when the preceding assumption does not hold. It consists in recomputing a SIC test sequence that leads from s new to s b then to re-execute the initial test sequence from et j . The SIC condition is introduced to avoid erroneous interpretations of synchronous events during the test steps from s new to s b . However it is not always possible to build a SIC sequence from two states [START_REF] Provost | SICtestability of sequential logic controllers[END_REF]); hence this solution is not always possible.

For the considered example, the SIC sequence can be built and the whole test sequence from s new is :

T S δ =((s 1 , a.b, s 1 , o), (s 1 , a.b, s 2 , o), (s 2 , a.b, s 2 , o), (s 2 , a.b, s 1 , o), (s 1 , a.b, s 2 , o), (s 2 , a.b, s 1 , o))

It may be noted that ( 9) is longer than ( 7) and ( 8) and requires to compute SIC test steps; the third solution is not the most efficient.

CONCLUSION

This paper has shown that the theoretical results obtained for conformance testing of Mealy machines cannot be directly used when testing real PLC. The technological features of these devices (cyclic I/O scanning and noninstantaneous reading of the input signals) require to adapt the conformance relation defined when only models are considered, to obtain correct verdicts. A first relation based on a sequence of observations during several PLC cycles has been introduced. This relation is not sufficient when synchronous input changes are detected as asynchronous; biased and non-valid verdicts may be delivered.

To solve this issue, a second conformance relation has been proposed; it is based on analysis of the possible concurrent transitions which start from the current active state and the sequences of observations which are accepted by the specification model.

On-going work is aiming at extending these results to validation of PLC by using HIL (hardware-in-the-loop) techniques. In this case, a real (hardware) PLC is connected to a software simulation of the plant to form a closed-loop system. The HIL approach differs from testing because the PLC is no more considered in isolation; hence, the state space to analyze is that of the PLC constrained by the plant. Up to now, only non-exhaustive simulation has been considered in this approach. Our objective is to investigate whether formal analysis techniques which have been developed for conformance testing of PLC can be used to automatically check the correctness of the PLC behavior from sequences of observations of the inputs and outputs of the simulated plant.

Fig. 1 .

 1 Fig. 1. Conformance test execution

  is the transition function • λ : S × I M → O M is the output function Let V I (resp. V O ) be the set of Boolean input (resp. output) variables of the PLC. The input alphabet I M (output alphabet O M ) of the machine is composed of all the combinations of input (output) variables. The dimension of I

Fig. 4 .

 4 Fig. 4. Part of a generic Mealy machine 3.1 Execution of a test sequence Each physical input of the PLC must be connected to one output of the test-bench and each physical output of the PLC must be connected to one input of the test-bench before test execution. Once the controller is connected to the test bench, each elementary test step et = (s u , I exp , s d , O exp ) is executed as follows:

  The first test step is et 1 = (s 1 , a.b, s 1 , o) which corresponds to a self-loop on the initial state; a sequence of observations for a correct implementation is σ Obset1 = (o, o, o) because the output combination is unchanged when the corresponding transition is fired. • The second test step is et 2 = (s 1 , a.b, s 2 , o). If the sequence of observations is σ Obset2 = (o, o, o), the implementation conforms to the specification; the state s 2 has been reached. • The third test step is et 3 = (s 2 , a.b, s 2 , o). If the following sequence is observed: (o, o, o), the implementation conforms to the specification. This is not the case according to Definition 1 when the observed sequence is (o, o, o). However this unexpected sequence may come either from a flawed implementation or an asynchronous detection of synchronous input changes. It must be noted indeed that the values of the two PLC input variables are modified synchronously from et 2 to et 3 ; if the change of b is detected before that of a, a correct implementation will fire the transition from s 2 to s 1 labeled with the input event a.b then will execute the self-loop on s 1 where both variables a and b are F alse.

  a.b and I j = a.b, the intermediate combinations are a.b and a.b. More generally, if n PLC input variables are changed from the input event of the previous test step to the input event of the considered test step, 2 n -2 intermediate input combinations can be defined.

  If this assumption holds, the initial test sequence is executed from this step. If it does not hold, this solution cannot be selected because some transitions might remain not tested what is in conflict with the test objective.Despite this solution induces no recomputation of the test sequence, it is not always applicable without a violation of the test objective.On the example, the assumption holds. Indeed, the current situation (s 1 , a.b) corresponds to the situation reached after the execution of the first test step et 1 = (s 1 , a.b, s 1 , o). The initial test sequence is thus restarted since the second test step.T S β =((s 1 , a.b, s 2 , o), (s 2 , a.b, s 2 , o), (s 2 , a.b, s 1 , o), (s 1 , a.b, s 2 , o), (s 2 , a.b, s 1 , o))

	)
	6.2 Repositioning in the initial test sequence
	This solution does not require any computation of a
	test sequence during test execution but relies on the
	assumption that it is possible to find, in the initial test
	sequence, a previously executed test step that corresponds
	to the same situation than the current one (active state
	s

new and input values I j ): ∃k < j such as

et k = (s x , I j , s new , O x ) with (s x ∈ S, O x ∈ O M )

This waiting time is equal to zero for a cyclic but not periodic I/O scanning.

A minterm defined on a set of n Boolean variables is the conjunction of all these variables in their positive or complemented form.

(.) represents the operator of conjunction and ( ) represents the complement.sequence can be built by using either the algorithm presented in[START_REF] Naito | Fault detection for sequential machines by transitions tours[END_REF] or that described in[START_REF] Provost | SICtestability of sequential logic controllers[END_REF]. A minimum-length MIC sequence which crosses at least once every transition of the specification is obtained in the first case (the sequence is termed complete). A SIC sequence which does not compulsorily satisfy this objective is produced in the second case and MIC test steps are to be added to obtain a complete test sequence.For the example of Fig.3and assuming that the two input variables of the PLC (a and b) are initially F alse, the complete minimum-length MIC test sequence is: T S M IC =((s 1 , a.b, s 1 , o), (s 1 , a.b, s 2 , o), (s 2 , a.b, s 2 , o), (s 2 , a.b, s 1 , o), (s 1 , a.b, s 2 , o), (s 2 , a.b, s 1 , o))(1)This test sequence is complete whereas it contains only six test steps. This is due to the fact that, even if the same transition is tested on steps et 2 and

et 5 , the previously defined strategy is applied three times. For the test steps et 2 , et 4

and et 6 , two transitions are tested during one test step.For the same example, the SIC test sequence is:T S SIC =((s 1 , a.b, s 1 , o), (s 1 , a.b, s 1 , o), (s 1 , a.b, s 2 , o), (s 2 , a.b, s 1 , o), (s 1 , a.b, s 2 , o), (s 2 , a.b, s 1 , o))(2)In this case, the sequence has the same length but is not complete. Indeed, using the defined

strategy, only 7 transitions are tested and the self loop on state s 2 labelled with a.b is missing. There is indeed no possible test step et l = (s l , i l , s 2 , o) that can be followed by the one which tests this transition (s 2 , a.b, s 2 , o) without breaking the Single-Input-Change rule because the only two candidates (s 1 , a.b, s 2 , o) and (s 2 , a.b, s 2 , o) require two input value changes.Hence, to ensure that all the transitions are tested at least once, MIC test steps must be added and the final complete sequence is given below:T S mixed =((s 1 , a.b, s 1 , o), (s 1 , a.b, s 1 , o), (s 1 , a.b, s 2 , o), (s 2 , a.b, s 1 , o), (s 1 , a.b, s 2 , o), (s 2 , a.b, s 1 , o), (s 1 , a.b, s 2 , o), (s 2 , a.b, s 2 , o))(3)This sequence is obviously longer than T S M IC and includes one test step (the last one) where asynchronous detection of synchronous input changes may happen; therefore this issue is not completely solved.3. A BASIC CONFORMANCE RELATIONOnce an initializable, consistent and complete test sequence built from the specification, it can be used to verify whether the implementation under test, a PLC that executes a control code in this work, behaves as specified. The aim of this section is to explain how this sequence is executed by the test-bench then to propose a relation that permits to emit a verdict about the conformance of the implementation. This presentation will be illustrated by means of the example of Figure4, a generic

This maximal value is obtained when the input change occurs just after the input reading phase of a cycle k. This change is detected at the beginning of the cycle k + 1 and the outputs are updated at the end of this cycle.

Where N * is the set of strictly positive integers.

ACKNOWLEDGMENT

This work is funded by the French research agency (ANR) as part of the VACSIM project (ANR-11-INSE-004).


Matthieu Perrinel
email: matthieu.perrinel@ens-lyon.fr

On paths-based criteria for polynomial time complexity in proof-nets

Several variants of linear logic have been proposed to characterize complexity classes in the proofs-as-programs correspondence. Light linear logic (LLL) ensures a polynomial bound on reduction time, and characterizes in this way the class P time. In this paper we study the complexity of linear logic proof-nets and propose two sufficient criteria, one for elementary time soundness and the other one for P time soundness, based on the study of paths inside the proof-net. These criteria offer several benefits: they provide a bound for any reduction sequence and they can be used to prove the complexity soundness of several variants of linear logic. As an example we show with our criteria a strong polytime bound for the system L 4 (light linear logic by levels).

To investigate these questions we propose here a kind of reverse approach: instead of defining strata by syntax we will define them by interaction. We believe this will contribute to establish these strata-based systems on solid ground. In a second step this could help in designing more general systems, and possibly also in analyzing the intrinsic limitations of strata-based systems.

.

Note that it is harder to control complexity in a higher order than in a first-order language. Thus, variants of LL for P time have to enforce strict control. Therefore, many polynomial time λ-terms can not be typed in those variants. For example, the λ-calculus type-system DLAL [3] (obtained from the LL subsystem LLL [10]) is P time extensionally complete. It means that for any function f computable in polynomial time, there exists a λ-term computing f typable in DLAL. This is proved by showing that it is possible to simulate any Turing machine for a polynomial number of steps with a DLAL typed term. However, DLAL is not intensionally complete: there are λ-terms which compute in polynomial time but are not typable in DLAL.

Introduction

Implicit computational complexity is a research field aiming to characterize complexity classes by syntactically restricting models of computation. The main application is to achieve automated certification of a program's complexity. Due to its focus on resources management, linear logic (LL) [START_REF] Girard | Linear logic[END_REF] is a promising setting for this field. One of the interests of the linear logic approach is that it admits higher order types: functions are basic objects (e.g. functions can take functions as arguments and return functions).

In the linear logic approach, programs are proofs and program execution is done by the elimination of the cut rule in the proof. Proofs are either presented as sequent calculus derivations or as proof-nets, a graph based syntax for proofs. Programming in proof-nets is unnatural for most people. Fortunately, the proofsas-programs correspondence states that a logical system corresponds to a type system for the λ-calculus [START_REF] Baillot | Light types for polynomial time computation in lambda calculus[END_REF]. λ-calculus is not used directly as a programming language but functional programming languages (e.g. Haskell) are based on it.

Most of the works controlling complexity in linear logic define a subsystem of LL enjoying some bounds on the length of cut-elimination sequences. Typically, the subsystem is defined in such a way that the programs are decomposed in strata and communication between strata is constrained. So syntax defines strata which in turn controls interaction. However a bunch of distinct subsystems have been defined in this way, corresponding to different notions of strata. How are these systems related and are there general principles underlying them?

Contributions In this paper, for any proof-net G, we define two relations ։ and 2 between some special elements of G called "boxes". A proof-net is said stratified if ։ is acyclic, and controls dependence if 2 is acyclic. A stratified proof-net normalizes in a number of steps bounded by an elementary function of its size. A proof-net satisfying both criteria normalizes in a number of steps bounded by a polynomial on its size. The elementary function and the polynomial only depend on the depth of the proof-net in terms of boxes and the depth of the ։ and 2 relations. Our approach has a number of benefits:

(i) strong vs weak complexity bounds; (ii) use of the criteria to prove complexity bounds for variants of linear logic; (iii) better understanding of existing linear logic systems for complexity. Concerning (i), a programming language comes with a reduction strategy which determines the reduction order. For example: do we reduce the arguments before passing them to functions (call by value) or not (call by name)? Complexity bounds are sometimes proved for farfetched strategies, which are unlikely to be implemented in a real programming language. The bounds proved in this paper do not depend on the strategy (strong complexity bounds).

As to (ii), we show how to use our approach to study variants of linear logic: we can establish the complexity soundness of a system by showing that all its proofs satisfy our criteria. Here, we will apply this technique to L 4 , for which only a weak P time bound was previously known. Note that it is relatively easy to prove that all proof-nets of a given system are stratified and control dependence. The more difficult work is done in the proof that those properties entail complexity bounds, and this is independent of the system. Factorizing proofs of complexity bounds may ease the search and the understanding of such proofs. Actually, an important progress had already been made in this direction by Dal Lago with context semantics [START_REF] Dal | Context semantics, linear logic, and computational complexity[END_REF]: he provided a common method to prove complexity bounds for several systems like ELL, LLL and SLL [START_REF] Lafont | Soft linear logic and polynomial time[END_REF]. Here we go a step further by designing higher level criteria, based on context semantics.

Concerning point (iii), we believe the present work can shed a new light on variants of linear logic for complexity. Indeed, the elaboration of such a system can be divided in two steps: first finding an abstract property implying a complexity bound and then finding a way to entail this property by syntactic means. Several extensions of LLL have been studied, like L 4 [START_REF] Baillot | Linear logic by levels and bounded time complexity[END_REF] and M S [START_REF] Vercelli | On the Complexity of Stratified Logics[END_REF]. As those systems verify our criteria, we think those criteria illustrate a common property underlying these logics. Moreover we have found some λ-terms satisfying our criteria without being in any system of the above list. Thus, it seems we could define more expressive systems by being closer to our criteria.

Related works

In the search for an expressive system for complexity properties, Dal Lago and Gaboardi have defined the type system dlP CF [START_REF] Lago | Linear dependent types and relative completeness[END_REF] which characterizes exactly the execution time of P CF programs. Type-checking in dlP CF is undecidable, but one can imagine restricting dlP CF to a decidable fragment. Their framework can be seen as a top-down approach. Here we follow a bottom-up approach: we take inspiration from previous decidable type systems characterizing P time and relax conditions losing neither soundness nor decidability.

Our main tool will be context semantics, a tool related to geometry of interaction [START_REF] Danos | Proof-nets and the Hilbert space[END_REF]. Baillot and Pedicini used geometry of interaction to characterize elementary time [START_REF] Baillot | Elementary complexity and geometry of interaction[END_REF]. Dal Lago adapted context semantics to study quantitative properties of cut-elimination [START_REF] Dal | Context semantics, linear logic, and computational complexity[END_REF]. From this point of view, an advantage of context semantics compared to the syntactic study of reduction is its genericity: some common results can be proved for different variants of linear logic, which allows to factor out proofs of complexity results for these various systems. We use the context semantics of Dal Lago, adapted to classical linear logic.

Here, we only give the statement of theorems, proofs can be found in [START_REF] Perrinel | On paths-based criteria for polynomial time complexity in proof-nets (long version)[END_REF].

Linear Logic

Linear logic [START_REF] Girard | Linear logic[END_REF] can be thought of as a refinement of System F [START_REF] Girard | Une extension de l'interpretation de gödel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types[END_REF] which focuses on the duplication of arguments. In LL, A ⇒ B is decomposed into !A ⊸ B. !A means "infinitely many proofs of A" and A ⊸ B means "using one proof of A, I can prove B". In fact, A ⊸ B is a notation of A ⊥ `B. We can view ( ) ⊥ as a negation and `as a disjunction. The conjunction is written ⊗. Finally ∀ and ∃ allow us to quantify over the set of formulae. Compared to full linear logic, we use neither additives, nor constants and we add a modality: §, introduced by Girard for the expressive power of LLL. Precisely, formulae of LL are defined inductively as follows (X ranges over a countable set of variables).

F = X | X ⊥ | F ⊗ F | F `F | ∀XF | ∃XF | !F | ?F | §F
As examples, let us notice that ∀X.X ⊸ X is provable (for any formula X, using one proof of X, we get a proof of X). On the contrary, ∀X.X ⊸ (X ⊗ X) is not provable because, in the general case, we need two proofs of X to prove X ⊗ X.

We define inductively ( ) ⊥ on F, which can be viewed as a negation: (

X) ⊥ = X ⊥ , (X ⊥ ) ⊥ = X, (A ⊗ B) ⊥ = A ⊥ `B⊥ , (A `B) ⊥ = A ⊥ ⊗ B ⊥ , (∀X.A) ⊥ = ∃X.A ⊥ , (∃X.A) ⊥ = ∀X.A ⊥ , (!A) ⊥ =?(A ⊥ ), (?A) ⊥ =!(A ⊥ ) and ( §A) ⊥ = §(A ⊥ ).
Definition 1. A proof-net is a graph-like structure defined inductively by the graphs of Figure 1 (G and H being proof-nets). Edges are labelled by formulae.

ax A ⊥ A G H cut A A ⊥ G H ⊗ A B A ⊗ B G À B A `B G ∃ A[B/X] ∃X.A G ∀ A ∀X.A G ?D A ?A G ?C ?A ?A ?A G ?W ?A G !P ?P ?P A1 An B ?A1 ?An !B G § A §A
Fig. 1. Construction of proof-nets. For the ∀ rule, we require X not to be free in the formulae labelling the other conclusions of G

Readers familiar with linear logic may notice the absence of the digging principle (!A ⊸ !!A). We removed it from this article to simplify the definitions. The way we deal with digging is described in [START_REF] Perrinel | On paths-based criteria for polynomial time complexity in proof-nets (long version)[END_REF].

The set of edges is written E G . The rectangle in the left-most proof-net on the second row of Figure 1 is called a box. Formally a box is a subset of the nodes of the proof-net. We say that an edge (l, m) belongs to box B if l is in B. The number of boxes containing an edge e is its depth written ∂(e). ∂ G is the maximum depth of an edge of G. The set of boxes of G is B G . Let us call B the box in Figure 1. The node labelled !P is the principal door of B, its outgoing edge is written σ(B). The ?P nodes are the auxiliary doors of box B. D G (B) is the set of doors of B. The doors of box B do not belong to box B.

Lists are written in the form [a 1 ; . . . ; a n ], l 1 @l 2 represents the concatenation of l 1 and l 2 , and . represents "push" ([a 1 ; . . . ;

a n ].b = [a 1 ; . . . ; a n ; b]). If X is a set, |X| is the cardinal of X. If b, h, n ∈ N, we define b n h by b n 0 = n and b n h+1 = b b n h .
The λ-terms correspond, through the proofs-as-programs paradigm, to proofnets. Intuitively, proof-nets are λ-terms where applications and abstractions are respectively replaced by ⊗ and `and with additional information on duplication. Cut-elimination is a relation, described in Figure 2, on proof-nets which corresponds to β-reduction. Proof-nets are stable under cut-elimination. 2. Rules of cut-elimination. In the ∀/∃ rule, the substitution of the variable X by B takes place on the whole net.

`⊗ cut cut cut cut ax cut cut cut ∀ ∃ A ⊥ A[B/X] ∀X, A ⊥ ∃X, A cut A[B/X] ⊥ A[B/

Context Semantics

Let us first give an informal explanation. The usual way to prove strong bounds on a rewriting system is to assign a weight T G to each term G such that, if G reduces to H, T G > T H . In LL, the !P/?C step makes the design of such a weight hard: a whole box is duplicated, increasing the number of edges, cuts,... Let us suppose that G reduces to H, an element (box, edge or node) x ′ of H is said to be a residue of an element x of G if x ′ "comes" from x. In Figure 3, e, e 1 , e 2 , e 3 and e 4 are residues of e. A duplicate of x ∈ G is a residue of x which has at most 1 residue (it can not be copied). In Figure 3, the duplicates of e are e 1 , e 3 and e 4 . Then, e∈E G |{duplicates of e}| does not increase, even during !P/?C steps. We will define a weight based on this sum.

Context semantics determines, among the paths in a proof-net G, which paths are preserved by cut-elimination (such paths are called persistent in the literature [START_REF] Danos | Proof-nets and the Hilbert space[END_REF]). Computing those paths is somehow like reducing the proof-net, and the persistent paths starting at the principal door of a box correspond to the duplicates of this box. In context semantics, persistent paths are captured by tokens (contexts) travelling across the proof-net according to some rules. The following definitions introduce the components of the tokens.

A signature is a list of l and r. A signature corresponds to a list of choices of premises of ?C nodes, to designate a particular duplicate of a box. The signature A potential is a list of signatures: a signature corresponds to the duplication of one box, but an element is copied whenever any of the boxes containing it is cut with a ?C node. The set of potentials is written P. A potential is meant to represent duplicates. The duplicates of e in Figure 3, e 1 , e 3 and e 4 , will be respectively

represented by potentials [[l]; []], [[r]; [r]] and [[r]; [l]

]. The canonical potentials, will characterize exactly the potentials corresponding to a duplicate.

A trace element is one of the following characters: `l, `r, ⊗ l , ⊗ r , ∀, ∃, §, ! t , ? t with t a signature. A trace element means "I have crossed a node with this label, from that premise to its conclusion". A trace is a non-empty list of trace elements. The set of traces is T. A trace is a memory of the path followed, up to cut-eliminations. We define duals of trace elements:

`⊥ l = ⊗ l , ! ⊥ t =? t ,. . .

and extend the notion to traces by ([a

1 ; • • • ; a k ]) ⊥ = [a ⊥ 1 ; • • • ; a ⊥ k ].
A polarity is either + or -. It will tell us in which way we are crossing the arrows. We define + ⊥ = -and -⊥ = +.

A context is a tuple (e, P, T, p) with e ∈ E G , P ∈ P, T ∈ T and p a polarity. It can be seen as a state of a token that will travel around the net. It is located on edge e (more precisely its duplicate corresponding to P ) with orientation p and carries information T about its past travel.

The nodes define two relations and ֒→ on contexts. The rules are presented in Figure 4. Observe that these rules are deterministic. For any rule (e, P, T, p) (g, Q, U, q) presented in Figure 4, we also define the dual rule (g, Q, U ⊥ , q ⊥ ) (e, P, T ⊥ , p ⊥ ). We define → as the union of and ֒→. In other words, → is the smallest relation on contexts including every instance of rules in Figure 4 together with every instance of their duals and every instance of the ֒→ rule.

For every sequence (e 1 , P

]; [l]], [`r], +) → (a, [[r]], [`r; ! [l] ], +) → (b, [], [`r; ! [l] ; ! [r] ], +) → (c, [], [`r; ! [l] ; ! [r] ], -) → (d, [], [`r; ! [l] ; ! [] ], -) → (f, [], [`r; ! [l] ], -) → (g, [], [`r; ! [] ], -) → (h, [], [`r; ! [] ], +) → (i, [], [`r; ! [] ; ⊗ r ], +) becomes the path (e 4 , [[]], [`r], +) → (h, [], [`r; ! [] ], +) → (i, [], [`r; ! [] ; ⊗ r ], +) in the third proof-net of Figure 3.
We want to capture the potentials which correspond to duplicates of a box. The definition can be difficult to understand. To give the reader a grasp of it, we will introduce the notion of →-copy progressively, proceeding by successive refinements. For the sake of simplicity, we will start with the case of depth 0.

-First, we could say that t corresponds to a duplicate of box B iff t corresponds to a sequence of choices of residues along a cut-elimination sequence, and the box residue we chose either will not be part of a cut, or the cut will open it. The →-paths are exactly the paths preserved by cut-elimination. So, we could make the first attempt: "t corresponds to a duplicate of B iff (σ(B), [], [! t ], +) → * (e, P, T, p) →". However, this definition would allow potentials which refuse choices, corresponding to residues which have several residues themselves (e.g. [] for B in Figure 3). ], -) →. So we add the condition that the left-most trace element in the last context must be ! [] , the signature must be used entirely.

Indeed (σ(B), [], [! [] ], +) → * (c, [], [! [] ], -) →.
Such a signature will be called a copy of (B, []).

If B k ⊂ • • • ⊂ B 1 , duplicates of B k will be represented by [t 1 ; • • • ; t k ] with [t 1 ; • • • ; t k-1 ] corresponding to a duplicate of B k-1 and t k a copy of (B k , [t 1 ; • • • ; t k-1 ]).
Definition 2. Let → be a relation on contexts, a →-copy of (B, P ) (with B ∈ B G and P ∈ P) is a signature t such that there exists n ∈ N such that ∀u ∈ S, (σ(B), P,

[! u.t ], +) → n (e, Q, [! u ], -) →
The set of →-copies of (B, P ) is denoted C → (B, P ). Intuitively, C → (B, P ) represents the duplicates of B, given the duplicates of the outer boxes.

.; s ∂(e) ] such that ∀i ≤ ∂(e), s i ∈ C → (B i , [s 1 ; • • • ; s i-1 ]).
So, a →-canonical potential for e is the choice, for all box B i containing e, of a →-copy of B i . In particular, in the case of →= →, L → (e) corresponds to all duplicates of e. For example, in Figure 3

L → (e) = {[[l]; []]; [[r]; [l]]; [[r]; [r]]}. We define L → (B) = L → (σ(B)).
The next theorem is due to Dal Lago [4]. The intuition behind it is that each cut-elimination step either erases a node or copies a box. Thus, if we know the number of duplicates of each edge, we can bound the number of cut-elimination steps. This result allows to prove strong complexity bounds for several systems.

Theorem 1 (Dal Lago's weight theorem). For every proof-net G, the length of any cut-elimination sequence beginning by G is bounded by:

T G = e∈E G |L → (e)| + 2 • B∈B G   |D G (B)| P ∈L → (B)

Stratification

Motivations

Stratification designates a restriction of a framework, which forbids the identification of two objects belonging to two morally different "strata". Russell's paradox in naive set theory relies on the identification of two formulae which belong morally to different strata. The non-terminating λ-term Ω = (λx.(x)x)λy.(y)y depends on the identification of a function and its argument. In recursion theory, to create from the elementary sequences θ m (n) = 2 n m (tower of exponential of height m in n), the non elementary sequence n → 2 n n , we also need to identify n and m which seem to belong to different strata. Stratification restrictions have been applied to those frameworks (naive set theory, linear logic, lambda calculus and recursion theory) to entail coherence or complexity properties [START_REF] Baillot | Linear logic by levels and bounded time complexity[END_REF]. ELL [START_REF] Girard | Light linear logic[END_REF] can be seen as linear logic deprived of the dereliction (!X ⊸ X) and digging (!X ⊸ !!X) principles. This is a stratification restriction on linear logic. The stratum of an edge is the depth of the edge in terms of box inclusion. One can observe in the rules of cut-elimination that without the ?D dereliction node (here, we did not present the node of digging), the depth of an edge never changes during cut-elimination, so during cut-elimination, a residue of e can be cut with a residue of f only if e and f have same depth. Any proof-net of ELL reduces to its normal form in a number of steps bounded by an elementary function of its size [START_REF] Danos | Linear logic and elementary time[END_REF]. In [START_REF] Baillot | Linear logic by levels and bounded time complexity[END_REF], Baillot and Mazza present an analysis of the concept of stratification and L 3 , a generalization of ELL. Their stratification condition is enforced by a labelling of edges and also entails elementary time.

Here, we present an even more general stratification condition. This generalization is not given by a LL subsystem but by a criterion on proof-nets. Then, to prove that a system is elementary time sound, we only have to prove that all the proof-nets of the system satisfy the criterion. ELL and L 3 satisfy the criterion.

Preliminary intuition: stratification on λ-calculus

Our definition of stratification is based on context semantics paths and may be difficult to grasp at first read. To motivate the criterion, we first state a criterion on λ-calculus, the formal system whose terms are generated by

Λ = x | λx.Λ | (Λ)Λ.
We define hole-terms as λ-terms with a variable • appearing free exactly once.

If t ∈ Λ, h[t] denotes h[t/•] and, if t is not a variable, t is said a subterm of h[t].
For t ∈ Λ, |t| is the size of t.

If g[u] → β v, the residues of u are the copies by β-reduction of u where free variables may have been substituted. Let us consider t = (λx.λy.(x)(x)y)λz.z → β λy.(λz.z)(λz.z)y = t ′ , then the residues of λz.z are the two occurrences of λz.z in t ′ . The residue of (x)y is (λz.z)y. Finally t and λx.λy.(x)(x)y have no residue.

Let u, v be subterms of t, we capture "u belongs to a higher stratum than v" by the following relation u ։ v. Definition 4. Let t ∈ Λ and u, v be subterms of t, u ։ v if t → * β t ′ and there exists a subterm of t ′ of shape

(v ′ )h[u ′ ] with u ′ , v ′ residues of u, v.
A λ-term is stratified if ։ is acyclic. Thus, Ω is not stratified because Ω → β (λy.(y)y)λy.(y)y so λy.(y)y ։ λy.(y)y. For any stratified term t, we define S t as the depth of ։ (i.e. the maximum n such that ∃(t i ),

t 0 ։ • • • ։ t n ). Theorem 2. If t ∈ Λ is stratified, then there is a normalization sequence for t of length ≤ |t| |t| 3.St .
Proof (sketch). Let t be a stratified λ-term. The strategy is to reduce first the set R 0 of subterms of t at stratum 0. By definition, these subterms have no residue inside the right part of an application. So there are never copied, they only have one duplicate. Thus we can reduce all the elements of R 0 in at most |R 0 | steps, obtaining a term t ′ in which elements of R 0 have no residue. We have

|t ′ | ≤ |t| 2 |R 0 | ≤ |t| 2 |t| .
If u ′ and v ′ are subterms of t ′ such that u ′ ։ v ′ and u ′ , v ′ are residues of u, v, then u ։ v. Thus, S t ′ < S t . In at most S t such rounds of reduction, we reach a normal form.

Stratification on proof-nets

We define a relation ։ between boxes of proof nets. It loosely correspond to the relation on Λ. In terms of context semantics paths, B ։ C means that there is a path beginning by the principal door of B which enters C by its principal door.

B ։ C ⇔ ∃P, Q ∈ P, t ∈ S, T ∈ T, (σ(B), P, [! t ], +) * (σ(C), Q, T, -)
To illustrate the correspondence with the criterion on Λ, we can observe that in the proof-net of Figure 5,(σ(B u ),[], [! e ], +) → 5 (σ(B v ), [], [! e ; ⊗ l ; ? e ], -) so B u ։ B v . Let u, v be the λ-terms corresponding to B u and B v , then the whole proof-net corresponds to (λx.h[(x)u])v which reduces to h[(v)u] so u ։ v. 5. This proof-net corresponds to (λx.h[(x)u])v for some h.

?D ⊗ !P Bu • • • • • • ⊗ cut !P • • • Bv ax Fig.
Definition 5. A proof-net G is stratified if ։ is acyclic.
For example, in Figure 6,(σ(B),[],[!

[l] ], +) * (σ(C), [], [! [] ; ⊗ l ; ! [r] ], -) so B ։ C.
This is the only relation in ։ so the proof-net is stratified.

The weak bounds for ELL and L 3 were proved using a stratum by stratum strategy, for a specific notion of stratum. They prove that reducing the cuts at strata ≤ i does not increase too much the size of the proof-net at stratum i + 1. Similarly, we will bound the number of copies of a box when we only reduce cuts in the strata ≤ i + 1 by the maximum number of copies of a box when reducing only cuts in strata ≤ i. Thus, we need a notion of copy corresponding to reduction of cuts only in strata ≤ i. This means we need a relation → i on contexts which simulates cut-elimination restricted to strata ≤ i.

First, we define the stratum of a box B, written S(B) as the depth of B in terms of ։, i.e. max{s | ∃(B i ) i≤s , B 0 ։ B 1 . . . ։ B s }. Then, the stratum of a Let s ∈ N, we define C → s D by: C → s D iff C → D and S(D) ≤ s. Thus, if B is a box of stratum > s, then for every P, t, (σ(B), P, [! t ], +) → so C →s (B, P ) = {[]}. This is the expected behaviour: we forbid the reduction steps involving a box of stratum > s, so B will never be duplicated. For matters of readability, we will often write L s (x) for L →s (x) and C s (x, P ) for C →s (x, P ). For any s ∈ N, → s ⊆ → so → s -copies of a box B are suffixes of →-copies of B.

Lemma 1. For any s ∈ N, any copy t ∈ C → (B, P ) there is a unique t /s ∈ C s (B, P ) such that t /s is a suffix of t. For any s ∈ N and for any P = [t 1 ; . . . ; t ∂(B) ] ∈ L → (B), there is a unique

P /s = [t ′ 1 ; . . . ; t ′ ∂(B) ] ∈ L s (B) such that for all 1 ≤ i ≤ ∂(B), t ′ i is a suffix of t i .
By Theorem 1, proof-nets are acyclic. So no → path may go through two contexts of the shape (e, Q, [! u ], p) and (e, Q, [! v ], p). In fact, we can prove the following refinement. Let us assume e ∈ B ∂(e) ⊂ • • • ⊂ B 1 , then no → path beginning by (σ(B), P, [! t ], +) may go through two contexts of the shape (e, [q 1 ; • • • ; q ∂(e) ], [! u ], p) and (e, [r 1 ; • • • ; r ∂(e) ], [! v ], p) where q i = r i whenever B ։ B i . This gives us the following "strong acyclicity" lemma.

Lemma 2 (strong acyclicity). Let us suppose that G is stratified and e

∈ E G . If (e, P, [! t ], p) → + s (e, Q, [! u ], p) then P /s-1 = Q /s-1 .
Theorem 3. If a proof-net G is stratified, then the length of its longest reduction sequence is bounded by 2 3.n 3.S G +1 with n = |E G |. Proof (sketch). Let us consider a → s path beginning by (σ(B), P, [! t ], +). Lemma 2 bounds the number of times we can go through the same ?C node with a

[! u ] trace by max (C,Q) |C s-1 (C, Q)| ∂ G .
So the length of any → s -copy of (B, P ) will be inferior to

|E G |•max (C,Q) |C s-1 (C, Q)| ∂ G . We get |C s (B, P )| ≤ 2 |E G |•max (C,Q) |Cs-1(C,Q)| ∂ G .
This gives an elementary bound on |C s (B, P )|, by induction on s. Then, the result folows by Theorem 1.

Dependence Control

Motivations

Though stratification gives us a bound on the length of the reduction, elementary time is not considered as a reasonable bound. Figure 7 illustrates how the complexity arises, despite stratification. On this proof-net, the box A duplicates the box B and each copy of B duplicates C. If we extended this chain to n boxes, it will normalize in time 2 n . In [START_REF] Vercelli | On the Complexity of Stratified Logics[END_REF], this situation is called a chain of spindles. We call "dependence control condition" any restriction on linear logic which aims to limit chains of spindles. The solution chosen by Girard [START_REF] Girard | Light linear logic[END_REF] was to limit the number of ?P -doors of each !-boxes to 1. To keep some expressivity, he introduced a new modality § with §-boxes which can have an arbitrary number of ?P -doors. However, this solution forbids many proof-nets whose complexity is polynomial. The complexity explodes in Figure 7 because two copies of a box B merge with the same box A. A box with several auxiliary doors is harmful only if two of its auxiliary edges are contracted. Besides, we study the complexity of functions, not stand-alone proof-nets. We say that a proof-net G is in polynomial time if there is a polynomial P G such that whenever G is cut with a proof-net H in normal form, the resulting proof-net normalizes in time P G (|E H |). G is fixed and P G depends on G. Thus, the sub-proof-net G of Figure 7 normalizes in constant time.

In fact, what really leads to an exponential blowup is when the length of such a chain of spindles depends on the input, as in Figure 8. If we replace the sub proof-net H (which represents 3) by a proof-net H ′ representing n, the resulting proof-net normalizes in time 2 n .

A Dependence Control Criterion

We will define a relation B 2 C on boxes meaning that at least 2 residues of B have their principal doors cut with an auxiliary door of C (spindle from B to C). We say that a proof-net controls dependence if 2 is acyclic. Then, if a proof-net G is stratified and controls dependence, the length of a chain of spindles in reducts of G is bounded by the number of boxes of G. Definition 6.

B 2 C ⇔ ∃t = u ∈ S, (σ(B), P, [! t ], +) → + (σ(C), Q, [! e ], -) (σ(B), P, [! u ], +) → + (σ(C), Q, [! e ],
n 3+16N •∂ 2•N •S
We can represent binary words in linear logic by the proof-nets of conclusion B = ∀X.!(X ⊸ X) ⊸ !(X ⊸ X) ⊸ !(X ⊸ X). Let us notice that the number of boxes in a cut-free binary words (or any other inductive data-type in Church encoding) is fixed. Let us suppose that G is a proof-net of type B ⊸ A (A being a formula) and for any cut-free binary word l, G cut with l is stratified and controls dependence. Then, there exists a polynomial P such that for all normal proof-net l representing a binary word of length n, the application of G to l normalizes in at most P (n) cut-elimination steps.

We can notice that the degree of the polynomial rises very fast. During the proof we used rough bounds. Otherwise, the statement of the bound would have been too complex. The bound is so high because, given S G and N G , we must consider the worst possible case (for example that there are boxes of nest N G in each stratum). Given the exact ։ and 2 relations on a stratified proof-net G controlling dependence, one can statically infer tighter bounds (if we are not in the worst possible case) by following the proofs of Lemmas 24 and 25 in [START_REF] Perrinel | On paths-based criteria for polynomial time complexity in proof-nets (long version)[END_REF].

Applications

L 4 (Light Linear Logic by Levels) is a system introduced by Baillot and Mazza [START_REF] Baillot | Linear logic by levels and bounded time complexity[END_REF] which generalizes LLL. L 4 is defined as the set of proof-nets for which we can label each edge e with an integer l(e) verifying the rules of Figure 9, and whose boxes have at most one auxiliary door. We define l G as max{l(e) | e ∈ E G }. Baillot and Mazza proved a weak polynomial bound for L 4 proof-nets for a particular strategy [START_REF] Baillot | Linear logic by levels and bounded time complexity[END_REF], but no strong bound1 . Obtaining a strong polynomial bound is important to define a type system for λ-calculus based on L 4 , because it is unclear whether the particular strategy on proof-nets of [START_REF] Baillot | Linear logic by levels and bounded time complexity[END_REF] could be converted into a β-reduction strategy.

ax A i A ⊥ i cut A i A ⊥ i ⊗ A i B i A ⊗ B i À i B i A `B i ∀ A i ∀X.A i ∃ A i ∃X.A i ?D A i ?A i-1 ?C ?A i ?A i ?A i § A i §A i-1 !P ?P ?P A i !A i-1 A i ?A i-1 A i ?A i-1
Fig. 9. Relations between levels of neighbour edges in L 4 In L 4 , the level of a box is stable by cut-elimination. This property has an equivalent in the context semantics presentation: the sum of the depth of the edge and the number of exponential trace elements is stable. Let T ∈ T, the number of !, ? and § trace elements in T is denoted T . Notice that the following Lemma only holds for the relation, not for the → relation. This makes the reasonings on L 4 more complex and partly explains why it was difficult to prove a strong bound for L 4 . Lemma 3. If G is a L 4 proof-net and (e, P, T, p) * G (f, Q, U, q), then

l(e) + T = l(f ) + U Lemma 4. If G is a L 4 proof-net and B ։ B ′ then l(σ(B)) > l(σ(B ′ )).
Thanks to Lemma 4, we can prove that L 4 proof-nets are stratified with strata of boxes being bounded by the maximum level of edges. It gives us an elementary bound on cut elimination. To prove a polynomial bound, one can prove that L 4 proof-nets control dependence. In fact, in L 4 , the 2 relation is empty so acyclic.

Theorem 5. Let G be a L 4 proof-net, with n = |E G |, of maximal level l, then the length of the longest reduction path is inferior to

n 3+16∂ 2l G +2 G
In L 4 , binary words are represented using the Church encoding with the type: B 4 = ∀X.!(X ⊸ X) ⊸!(X ⊸ X) ⊸ §(X ⊸ X). In Theorem 5, the polynomial only depends on the level and depth of the proof-net. Let G be a L 4 proof-net representing a function on binary words, i.e. the only conclusion of G has type B 4 ⊸ A for some A. Then, there exists a polynomial P such that for all normal proof-net H representing a binary word of length n, the application of G to H normalizes in at most P (n) cut-elimination steps.

Other systems The framework M S [START_REF] Vercelli | On the Complexity of Stratified Logics[END_REF] is a set of subsystems of ELL where ! connectives are indexed by integers. ELL is stratified so all proof-nets of M S are stratified. In [START_REF] Vercelli | On the Complexity of Stratified Logics[END_REF], Vercelli characterizes the "most general" P time sound subsystems of M S. Those systems allow !-boxes with several auxiliary doors. In those systems, if B 2 B ′ , σ(B) and σ(B ′ ) are labelled by formulae of respective shape ! n A and =! n ′ A ′ , then n < n ′ . The dependence control follows immediately. The strong polynomial bound, however, was already proved in [START_REF] Vercelli | On the Complexity of Stratified Logics[END_REF].

We also prove a strong bound for L 4 0 , a refinement of L 4 [START_REF] Baillot | Linear logic by levels and bounded time complexity[END_REF]. L 4 0 does not enjoy stratification but we can derive a strong bound for L 4 0 from the strong bound for L 4 . No polynomial bound was previously proved for this system.

Comparison with L 3 . Our criteria allowed to show strong polynomial bounds for systems for which only weak bounds were known. In addition, it shows that the stratification constraints of L 3 could be relaxed. Indeed, we found stratified proof-nets controlling dependence corresponding to the λ-term ((2)λn.((n)S)1)0 (with n being the representation of n ∈ N in Church numerals) and the λ-term with pair2 (λ f, g . (f )g, (g)f ) λx.x, λy. y, y (Figure 6). It seems that there are no L 3 proof-net corresponding to those terms. However, those examples are contrived, and it is still not clear how much expressive power can be gained in practice by relaxing the stratification conditions of L 3 .

Comparison with M S. For any P time sound M S system S, the length of chains of spindles is bounded by an integer k S . Let us fix S, we can extend the chain of spindles of G in Figure 7 to k S + 1 spindles, so that G is still constant time but not in S. Our criteria are more general. First, we do not fix a priori a limit on the length of chains of spindles, but only forbid cycles. So G, even with an extended chain of spindles, satisfies our criteria. Let t = k(λ x, y, z . x, ((+)x)y, y ) and u = λ x, y, z . z, z, z , then (t)(u)(t) • • • (u)t is stratified and controls dependence, whatever the length of the chain of applications, whereas in M S the maximum length of such a chain is bounded. Moreover, our bound is still valid in presence of dereliction (?D) and digging (dealing with the latter is more complex and is only presented in the long version [START_REF] Perrinel | On paths-based criteria for polynomial time complexity in proof-nets (long version)[END_REF]).

Conclusion

We defined two criteria on proof-nets which imply bounds on the complexity of cut-elimination. These are then used to prove strong bounds for systems for which only weak bounds were known. A major advantage of our approach is that, once our general lemmas are established, proving bounds for various systems is quite simple. There are P time proof-nets which do not verify our criteria, however the expressive power of those criteria is still unclear. In future work, we plan to define more expressive systems based on these.

Let us comment on decidability issues. One can compute all the → paths in a proof-net, for example by reducing the proof-net. So, stratification and dependence control of a proof-net are decidable. However, as we are interested by the complexity of functions, the interesting problem of certifying complexity of a proof-net G is "Is there any cut-free proof-net H such that G cut with H is not stratified or does not control dependence?". This problem seems undecidable. As a future work, we want to design a decidable type system, inspired by our criteria, capturing P time.

A Discussion on previous work on L 4

strong bound

In Section 8.2.2 of [START_REF] Vercelli | On the Complexity of Stratified Logics[END_REF], Vercelli claims a proof of strong polynomial bounds for some subsystems of M S † . L 4 is one of these systems. However, the proof of the strong bound contains some flaws. Indeed, the → relation used in this section has no rule to leave a box by its principal door. Moreover, the weight T G used differs from the weight used by Dal Lago [4] and us. In the following, T G designs the weight defined by Vercelli and we will show that the lemma 8.2.15 -which corresponds to the "Dal Lago's weight theorem" -is false. Indeed, in Figure 10, G → cut H but T G = 0 + 2 + 2 + 10 = 14: 0 for box B door because no maximal CS-path begin by σ(B), 2 for both boxes at depth 0, 1 for each node which is neither an axiom nor a door. And T H = 2.4.2 + 2 + 2 + 10 = 22: 2.4.2 for B door because each of the 4 B copies has length 2, 2 for the box at depth 0, 1 for each node which is neither an axiom nor a door. So T G < T H . If we fix this problem by taking our → relation, then lemma 8.2.17 would fail. Indeed, crossing a ?D node changes the number of exponential stack element in the stack without changing the length of the potential. If we fixed it by replacing the length of the potential by the level of the edge in the enunciation of lemma 8.2.17 then the lemma would fail on the ֒→ steps because the doors of a same box may have different levels. So the correct form of the lemma is:

If G is a L 4 proof-net and (e, P, T, p) * G (f, Q, U, q), then l(e) + T = l(f ) + U This is exactly our lemma 3. However, proving that this weaker lemma is enough is far from trivial.

Fig. 3 .

 3 Fig. 3. Cut-elimination of a proof-net.

Fig. 4 .

 4 Fig. 4. Exponential rules of the context semantics

Definition 3 .

 3 Let → be a binary relation on contexts and e ∈ E G such that e ∈ B ∂(e) ⊂ ... ⊂ B 1 . The set L → (e) of canonical potentials for e is the set of potentials [s 1 ; ..

  t∈C → (B,P ) |t|   Moreover, G is acyclic: there exists no path of the form (e, P, [! s ], b) → + (e, P, [! t ], b).

Fig. 7 .

 7 Fig. 7. If H is in normal form, this proof-net reduces in 32 cut-elimination steps

Fig. 8 .

 8 Fig. 8. The sub proof-net G is not polynomial time

  -) If G controls dependence and B ∈ B G , we define the nest of B (written N (B)) as the depth of B in terms of the 2 relation. N G refers to max B∈B G N (B).

Theorem 4 .

 4 If G is stratified and controls dependence, let n = |E G |, N = N G +1, S = S G + 1 and ∂ = ∂ G + 1, the maximal reduction length of G is bounded by

Fig. 10 .

 10 Fig. 10. The proof-net G reduces to H, but T G < T H

Fig. 11 .

 11 Fig. 11. The →-path beginning by (σ(B), [[l]; []], [! t ], +) does not cross the contraction node.

  , p n ), the sequence of directed edges (e 1 , p 1 ), • • • , (e n , p n ) is a path (i.e the head of e i is the same node as the tail of e i+1 ). The ֒→ relation breaks this property as it is non-local, in the sense that it deals with two non-adjacent edges. It is the main relation that distinguishes Dal Lago's context semantics from geometry of interaction. The trace keeps track of the history of previously crossed nodes to enforce path persistence: the → paths are preserved by cut-elimination. The study of paths, sequences of the shape C 1 → C 2 → . . . , will give us information on complexity.

	e	cut	f	g	ax	h	(e, P, T, +) (g, P, T, -)	(f, P, T, -) (h, P, T, +)
		à c	b		e	⊗ g	f	(a, P, T, +) (b, P, T, +) (e, P, T, +) (f, P, T, +)	(c, P, T.`l, +) (c, P, T.`r, +) (g, P, T.⊗ l , +) (g, P, T.⊗r, +)
	e f	∀			g h	∃		(e, P, T, +) (g, P, T, +)	(f, P, T.∀, +) (h, P, T.∃, +)
	e				g	h		(e, P, T, +)	(f, P, T.? [] , +)
	?D			?C		(g, P, T.?t, +)	(i, P, T.?t. l, +)
	f				i			(h, P, T.?t, +)	(i, P, T.?t. r, +)
	e				g			(e, P.t, T, +)	(f, P, T.?t, +)
	?P			!P		(g, P.t, T, +)	(h, P, T.!t, +)
	f				h			(f, P, !t, -) ֒→ (h, P, !t, +)

1 , T 1 , p 1 ) (e 2 , P 2 , T 2 , p 2 ) • • • (e n , P n , T n

  The duplicates of B in this figure are B 1 and B 2 , which correspond to [l] and[r]. [] corresponds to B, which can be copied. -Thus, our second try would be "(B, t) corresponds to a duplicate iff ∃n ∈

	N, ∀u ∈ S, (σ(B), [], [! u.t ], +) → n →". However, this definition would allow
	potentials which make too many choices. For example (B, [l; r]) in Figure 3
	satisfies this definition. Indeed (σ(B), [], [! [l;r] ], +) →

* (d, [], [! [l]

In fact, a proof of a strong bound is claimed in[START_REF] Vercelli | On the Complexity of Stratified Logics[END_REF], but it contains flaws which do not seem to be easily patchable. See Appendix A and[START_REF] Perrinel | On paths-based criteria for polynomial time complexity in proof-nets (long version)[END_REF] for more details.

The pairs are here represented by using the connective ⊗


Cong Nguyen

Nicolas Tam

Thierry Galanis

Erwan Maré

Eveillard

Tam Cong

Nicolas Nguyen

New Viscosity Data for CuO-water Nanofluid -The Hysteresis Phenomenon Revisited

Keywords: Nanofluids, CuO-Water nanofluid, Thermal properties, Dynamic viscosity, Hysteresis, Stability

come   L'archive ouverte pluridisciplinaire

phenomenon did not occur for the temperature range considered. For a higher particle concentration, 5% in particular, the hysteresis behaviour was clearly observed when fluid temperature exceeded 52ºC approximately. Beyond this critical temperature, the nanofluid viscosity has increased, and such an increase even continued with a decrease of temperature during the cooling phase.

Subsequent measured viscosity and observations in laboratory after the first occurrence of the hysteresis phenomenon have confirmed that the alterations on the particle suspension and on the nanofluid stability appear indeed permanent. Such alterations were found to worsen with further heating/cooling cycles.

Conclusion

We have experimentally studied the stability and hysteresis behaviors of CuO-water nanofluid.

It was found that for the nanofluid with 1.6% particle volume fraction, the hysteresis phenomenon did not occur, and the effects due to the heating/cooling process, although present, seem to be slight.

For a higher particle concentration, 5%, the hysteresis behaviour was clearly observed when fluid temperature exceeded 52ºC approximately. Measured viscosity data and observations after the first occurrence of the hysteresis phenomenon have confirmed that the damages due to repeated heating/cooling cycles on the particle suspension and on the nanofluid stability appear indeed permanent. Such damages were found to become worsened with further heating/cooling cycle.