Paul Gallot
email: pgallot@ens-paris-saclay.fr

Anca Muscholl

Gabriele Puppis
email: gabriele.puppis@labri.fr

Sylvain Salvati
email: sylvain.salvati@univ-lille1.fr

On the decomposition of finite-valued streaming string transducers

Keywords: 1998 ACM Subject Classification F.1.1 Models of Computation, Automata Keywords and phrases Streaming Transducers, finite valuedness, equivalence Digital Object Identifier 10.4230/LIPIcs

We prove the following decomposition theorem: every 1-register streaming string transducer that associates a uniformly bounded number of outputs with each input can be effectively decomposed as a finite union of functional 1-register streaming string transducers. This theorem relies on a combinatorial result by Kortelainen concerning word equations with iterated factors. Our result implies the decidability of the equivalence problem for the considered class of transducers. This can be seen as a first step towards proving a more general decomposition theorem for streaming string transducers with multiple registers.

Introduction

Data management systems heavily depend upon models of transformation of data that must be efficient both in terms of processing time and in terms of memory resources, and yet enjoy decidable static analysis methods (e.g. algorithms for checking equivalence).

Finite transducers, that is, finite automata extended with outputs, are simple devices that enable some effective, and even efficient reasoning on data transformations. These models come in different variants, depending on whether they use non-determinism or not, on whether the input is scanned only once from left to right (one-way transducers) or several times and in different directions (two-way transducers, or two-way generalised sequential machines 2GSM), and on the number of outputs that can be associated with each input. Concerning the last property, transducers that associate at most one output with each input are called functional transducers.

One may expect that the transformations computed by finite state transducers can be equally described in logic, like monadic second-order logic (MSO), but this holds only up to a certain extent. For instance, two-way transducers are as expressive as MSO-definable transductions [START_REF] Engelfriet | MSO definable string transductions and two-way finite-state transducers[END_REF] when restricted to the functional case, but they become incomparable as soon as unrestricted (i.e. relational) transductions are considered.

Streaming String Transducers (SSTs) [START_REF] Alur | Expressiveness of streaming string transducers[END_REF] have been introduced as a mechanical representation of transducers described by means of MSO. They gained a growing interest in a series of works [START_REF] Alur | Streaming string transducers[END_REF][START_REF] Alur | Expressiveness of streaming string transducers[END_REF][START_REF] Alur | Streaming transducers for algorithmic verification of single-pass list processing programs[END_REF][START_REF] Alur | Nondeterministic streaming state transducers[END_REF], where their formal properties have been investigated and where they have been put to applications to model transformations on data streams, heaps etc.

XX:2

On the decomposition of finite-valued SSTs

Intuitively, SSTs are one-way automata enhanced with a finite number of registers to store and manipulate partial outputs. The registers can be updated by appending and prepending symbols, and possibly by concatenating several registers into one; the register content, however, cannot be inspected to control the flow of the computation.

Contrary to two-way transducers, not only functional SSTs are as expressive as MSOdefinable functional transductions, but also this remains true when considering relational transductions. Therefore, as for MSO transductions, functional SSTs are equally expressive as functional two-way transducers and incomparable to them for relational transductions. Somehow, the equivalence of SSTs with MSO transductions is rather intuitive in view of a result [START_REF] Engelfriet | Macro Tree Transducers, Attribute Grammars, and MSO Definable Tree Translations[END_REF] that characterizes MSO tree transductions in terms of finite copying macro tree transducers with the single use restriction. In SSTs, the finite copying mechanism is represented by the use of a finite number of registers, while the single use restriction for SSTs is formalized as the requirement that, during a transition of the machine, the content of each register can be used at most once to produce the new contents (copyless SSTs). Moreover, this result relates SSTs to much older formalisms, notably the Lindenmayer's L systems called D0L and HDT0L, which can be used to describe transductions and whose generalizations to trees can be seen, in a certain way, as macro tree transducers.

This paper focuses on finite-valued transductions, which lie strictly between functional and relational ones. Formally, a transduction is finite-valued if it associates a uniformly bounded number of outputs (say, at most k outputs) with each input. For one-way transducers it is known how to decide whether it is finite-valued [START_REF] Weber | On the valuedness of finite transducers[END_REF], and in this case compute the maximal number of outputs associated with some input [START_REF] Gurari | A note on finite-valued and finitely ambiguous transducers[END_REF]. While the decidability of this property is still an open question for two-way transducers. What is more interesting is that, even if finite-valued transducers capture more transductions than functional transducers, they often enjoy properties similar to the latter ones, especially concerning the decidability of the fundamental problems and the relationship with logic.

Of course, transducers beyond the classical one-way case pose new challenges with respect to the fundamental problems, notably, the equivalence problem. For example, equivalence is known to be decidable for functional SSTs, even without the copyless restriction [START_REF] Filiot | On streaming string transducers and HDT0L systems[END_REF], but it is undecidable for unrestricted (i.e. relational) ones [START_REF] Griffiths | The unsolvability of the equivalence problem for lambda-free nondeterministic generalized machines[END_REF]. On the other hand, the equivalence problem remains decidable for finite-valued 2GSMs [START_REF] Culik | The equivalence of finite valued transducers (on hdt0l languages) is decidable[END_REF], by an argument relying on Ehrenfeuchts's conjecture. The latter paper actually shows that every HDT0L language L has an effective test set, that is, a finite subset on which equivalence of finite-valued 2GSM w.r.t. L can be tested.

The pervasive similarity between finite-valued and functional transducers can sometimes be explained by a quite strong decomposition theorem of the following form, where C is an appropriate class of transducers: Within C finite-valued transducers are equivalent to finite unions of functional transducers.

It is known from [START_REF] Weber | Decomposing a k-valued transducer into k unambiguous ones[END_REF] that the above statement holds when C is the class of one-way transducers. Our main interest is in proving the decomposition theorem for the class of SSTs, since, as we will see, this implies solutions to a certain number of open problems, notably, the decidability of the equivalence problem for finite-valued SSTs and the equivalence to finite-valued two-way transducers. We begin this investigation by proving a decomposition theorem for the sub-class of SSTs with 1 register. Unfortunately, we are not able to generalize this result to SSTs with multiple registers. Towards the end of the paper we outline a few points of our proof that are problematic for the generalization.

Preliminaries

Two-way transducers. A two-way transducer, or two-way generalized sequential machine (abbreviated 2GSM ), is a tuple T = (Σ, Γ, Q, I, E, F ), where Σ (resp. Γ) is a finite input (resp. output) alphabet, Q is a finite set of states, I (resp. F ) is a set of initial (resp. final) states included in Q, and

E ⊆ Q × Σ × Γ ⋆ × Q × {-1, +1}
is a finite set of transition rules describing, for each state and input symbol, the possible output string, target state, and direction of movement. To correctly define the transitions at the extremities of the input, we use two special symbols ⊳ and ⊲ and assume that the input of a 2GSM is of the form w = a 1 . . . a n , with n ≥ 2, a 1 = ⊳, a n = ⊲, and a i ≠ ⊳, ⊲ for all i = 2, . . . , n -1. We say that T is one-way if it can only move to the right, that is, (q, a, v, q ′ , d) ∈ E implies d = +1.

A configuration of T on input w is a pair (q, p) ∈ Q × {1, . . . , w } consisting of a state and a position in the input. The transitions of T on w connect pairs of configurations and are of the form (q, p) a v → T (q ′ , p ′ ), with a = w(p), (q, a, v, q ′ , d) ∈ E, and p ′ = p + d. We assume that T can only move right (resp. left) at the first (resp. last) position of w, that is, (q, ⊳, v, q ′ , d) ∈ E implies d = +1 and (q, ⊲, v, q ′ , d) ∈ E implies d = -1. A run of T on w is any sequence of transitions of the form (q 0 , p 0 ) w(p0) v1 → T (q 1 , p 1 ) w(p1) v2 → T . . . w(pn-1) vn → T (q n , p n ). The output of a run ρ is the word out(ρ) = v 1 v 2 . . . v n . The run ρ is initial (resp. final) if q 0 ∈ I and p 0 = 1 (resp. if q n ∈ F and p n = w ).

Streaming string transducers.

For convenience, we define streaming string transducers in a slightly different but equivalent way compared to [START_REF] Alur | Expressiveness of streaming string transducers[END_REF] (this concerns in particular the definition of the output). A streaming string transducer (SST ) is a tuple T = (Σ, Γ, Q, X, x out , U, I, E, F ), where Σ, Γ are the usual input and output alphabets, Q is the state space, X is a finite set of registers disjoint from Γ, x out ∈ X is a special register used to describe the final output, U is a finite set of register updates, namely, functions from X to (X ⊎ Γ) * , I is a subset of Q representing the initial states, E ⊆ Q × Σ × U × Q is a set of transition rules, describing, for each state and input symbol, the possible updates and target states, and F ⊆ Q is a set of final states.

To define the semantics of T , we make use of valuations, that is, functions g ∶ X → Γ * . A valuation g can be homomorphically extended to words over X ⊎ Γ and to register updates, as follows. Given a word w ∈ (X ⊎Γ) * , g(w) is the word over Γ obtained from w by replacing every occurrence of a register x with its valuation g(x). Similarly, given an update f ∶ X → (X ⊎Γ) * , g○f is the valuation that maps each register x to the word g(f (x)). A configuration of T is a pair state-valuation (q, g). The configuration is initial (resp. final) if q ∈ I and g(x) = ε for all registers x ∈ X (resp. q ∈ F ). When reading a symbol a, the SST moves from configuration (q, g) to configuration (q ′ , g ′ ) if there is a transition rule (q, a, f, q ′ ) ∈ E such that g ′ = g ○f . We denote such a transition by (q, g) a f → T (q ′ , g ′ ). A run of T on w = a 1 . . . a n is any sequence of transitions of the form (q 0 , g 0 ) a1 f1 →

T (q 1 , g 1 ) a2 f2 → T . . . an fn → T (q n , g n ).
It is initial (resp. successful) if it begins with an initial configuration (resp. if it begins with an initial configuration and ends with a final configuration). The output of a successful run is the last valuation g n (x out ) of the special register x out .

A well-behaved class of SSTs is obtained by requiring that all the updates are copyless. Formally, an SST T = (Σ, Γ, Q, X, x out , U, I, E, F ) is copyless if for every update f ∈ U , every register x ∈ X appears at most once in f (x 1 ) ⋅ . . . ⋅ f (x k ), where X = {x 1 , . . . , x k }. Hereafter we tacitly assume that all SSTs are copyless.

Unambiguity, transductions, functionality. The following definitions apply to both two-way transducers and streaming string transducers. The input automaton of a transducer XX:4

On the decomposition of finite-valued SSTs

T is a finite automaton A obtained from T by removing any information concerned with the construction of the output (e.g. the output alphabet, the registers, etc.). For example, if T is an SST, then the input automaton A of T has transition rules of the form (q, a, q ′ ) for all transition rules (q, a, f, q ′ ) of T . This automaton recognizes precisely the language of input words w that have at least one successful run of T (and hence at least one associated output). We say that T is input-unambiguous (resp. input-k-ambiguous) if its input automaton is unambiguous, namely, it admits at most one successful run on each input (resp. if the input automaton admits at most k successful runs on each input).

A transduction is a relation T ⊆ Σ * × Γ * consisting of pairs of input and output words. It is computed by a transducer T if it contains exactly those pairs (w, v) ∈ Σ * × Γ * for which there is a successful run of T on w with output v. T is called functional if it computes a transduction which is a partial function, namely, it associates at most one output with each input. Similarly, it is k-valued if it associates at most k outputs with each input (in [START_REF] Alur | Nondeterministic streaming state transducers[END_REF] such a transducer is called finitary).

Transductions can be also defined in monadic second-order logic (MSO). Intuitively, this is done by specifying an output (seen as a relational structure) from a fixed number of copies of the input. We only give a short account of the definitions and we refer the reader to [START_REF] Courcelle | Monadic second-order graph transductions: a survey[END_REF] for the details. An MSO transduction with m copies consists of a formula Φ dom ( Z), where Z = (Z 1 , . . . , Z m ) is an m-tuple of free monadic variables, a formula Φ i a ( Z, x) for each i ∈ {1, . . . , m} and a ∈ Γ, and a formula Φ i,j ≤ ( Z, x, y) for each i, j ∈ {1, . . . , m}. For different valuations of the free variables Z, which range over sets of positions of the input, we may have different outputs associated with that input. The formula Φ dom ( Z) describes which valuations generate an output. The formula Φ i a ( Z, x) tells whether, in the output corresponding to the valuation of Z, the position x in the i-th copy of the input is an element of the output and, in this case, if it is labeled with the letter a. Similarly, the formula Φ i,j ≤ (x, y) tells whether, in the output corresponding to the valuation of Z, the element x of the i-th copy of the input precedes the element y of the j-th copy of the input.

3

The conjectured decomposition theorem and its implications

We conjecture the following decomposition theorem for SSTs:

▸ Conjecture 1. k-valued SSTs are effectively equivalent to finite unions of functional SSTs.

In Section 5 we will give a proof of this conjecture in the restricted case of SSTs with a single register. Even if we are not able to prove the result in its full generality, we discuss here some important implications of the conjecture, which motivate our interest in having such a result. A first consequence would be the decidability of equivalence for k-valued SSTs:

▸ Corollary 2. Assuming that Conjecture 1 holds, one can decide if two k-valued SSTs T , T ′ are equivalent. Proof. Conjecture 1 implies that T = T 1 ∪ ⋅ ⋅ ⋅ ∪ T k and T ′ = T ′ 1 ∪ ⋅ ⋅ ⋅ ∪ T ′ k where T 1 , . . . , T k , T ′ 1 , . . . , T ′
k are all functional transducers. From [START_REF] Alur | Nondeterministic streaming state transducers[END_REF], we know that functional SSTs can be made deterministic, and also that the inclusion (as a transduction) of an SST within a finite union of deterministic SSTs is decidable. A consequence is that we can decide whether both

T ⊆ T ′ 1 ∪ . . . ∪ T ′ k and T ′ ⊆ T 1 ∪ . . . ∪ T k hold, that is, whether T is equivalent to T ′ . ◂
Another implication concerns the relationship between SSTs and 2GSMs:

▸ Corollary 3. Assuming that Conjecture 1 holds, k-valued SSTs and k-valued 2GSMs are equally expressive. In addition, this would give a decomposition theorem for k-valued 2GSMs.

Proof. From [START_REF] Alur | Expressiveness of streaming string transducers[END_REF] we know that functional SSTs are expressively equivalent to functional MSO-definable transductions, and from [START_REF] Engelfriet | MSO-definable string transductions and two-way finitestate transducers[END_REF] the latter are expressively equivalent to functional 2GSMs. So functional SSTs can be translated to equivalent functional 2GSMs. Our conjecture would then imply that k-valued SSTs can be transformed to equivalent 2GSMs. The proof that k-valued 2GSMs can be translated to equivalent SSTs is sketched below. Note that this translation does not rely on any decomposition theorem for 2GSMs. In fact, the previous arguments paired with the following proof, do imply a decomposition theorem for k-valued 2GSMs. Consider a 2GSM T and define the crossing number of a successful run ρ of T as the maximum number of configurations that occur in ρ at same position p of the underlying input. Using classical techniques from [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF], one can encode with a regular language any set of successful runs of T with uniformly bounded crossing numbers. Using such an encoding and a number of registers proportional to the bound on the crossing numbers, one can then simulate the output produced by those runs in a single left-to-right pass, that is by means of an SST T ′ . In general, the transduction computed by T ′ is included in that of T . The crucial observation is that, if T is k-valued, then all its outputs can be produced by successful runs that have crossing number at most Q , where Q is the state space of T . The SST T ′ is thus equivalent to T . ◂

The classical decomposition theorem for one-way transducers

We give a short overview of the proof of a classical decomposition theorem for one-way transducers, following the presentation of [START_REF] Sakarovitch | On the decomposition of k-valued rational relations[END_REF]: [START_REF] Weber | Decomposing a k-valued transducer into k unambiguous ones[END_REF]). k-valued one-way transducers are effectively equivalent to finite unions of functional one-way transducers.

▸ Theorem 4 ([
We present this proof, not only for self-containment, but also because it allows us to isolate the key important properties that need to be generalized in order to obtain a decomposition theorem for SSTs. After the proof sketch, we will mention some important implications of the theorem, notably, the decidability of the equivalence problem and the correspondence with a suitable subclass of MSO-definable transductions.

Given two automata or transducers A, B, we say that B is a covering of A if there is a function h from the states of B to the states of A such that (i) h preserves the transitions, that is, if τ = (q, a, ..., q ′ ) is a transition rule of B, then h(τ ) = def h(q), a, ..., h(q ′ ) is a transition rule of A, (ii) h induces a bijection between the initial states of B and the initial states of A, (iii) for all states q of B, h induces a bijection between the transitions of B exiting q and the transitions of A exiting h(q), and (iv) both h and h -1 preserve final states, that is, q is final in A iff h(q) is final in B. Note that when B is a covering of A, there is a bijection between the (successful) runs of B and the (successful) runs of A; in particular, B and A are equivalent (they recognize the same language or compute the same transduction). A common way to define a covering of A consists in equipping the states of A with additional information which can be maintained in a deterministic way during the transitions. In this case, the states of the covering can be denoted by pairs of the form (q, o), where q is a state of A and o is some object (the additional information) associated with q. Accordingly, given a run ρ of such a covering of A, we denote by ρ 1 the corresponding run of A.

Let T be a one-way transducer and ρ, ρ ′ two runs of it on the same input and with possibly different outputs out(ρ), out(ρ ′ ). We would like to give a "measure" of the divergence of these outputs. The size of a pair of words (u, v) ∈ Γ * × Γ * is the sum of the lengths of u and v, i.e. (u, v) = u + v . The lead or delay of a pair of words (x, y), denoted LD(x, y) is either the smallest pair of words (u, v) such that x u = y v, if such a pair exists, or otherwise. Note that if LD(out(ρ), out(ρ ′ )) ≠ , then this is a pair where at least one of the two components is the empty word ε, and it is (ε, ε) iff ρ and ρ ′ produce the same output. We also define the lag of (ρ, ρ ′ ) as the number

∆(ρ, ρ ′ ) = def max ρ = α β, ρ ′ = α ′ β ′ , α = α ′ LD out(α), out(α ′ )
(by convention, we let = ∞ > n for all n ∈ N). Intuitively, ∆(ρ, ρ ′ ) describes how much the partial outputs produced by some prefixes of ρ and ρ ′ of the same length have diverged.

The proof of the decomposition theorem consists in arguing as follows.

The main combinatorial property. Given a k-valued one-way transducer T , one constructs a multi-transducer T k+1 , whose successful runs can be seen as (k + 1)-tuples of successful runs of T spelling out the same input and possibly different outputs. One proves the following combinatorial property (see [START_REF] Weber | Decomposing a k-valued transducer into k unambiguous ones[END_REF]): for every successful run ρ = (ρ 1 , . . . , ρ k+1 ) of T k+1 , there exist distinct components ρ i , ρ j of ρ that not only agree on the output (this is necessary since T is k-valued), but also have ∆(ρ i , ρ j ) ≤ n 0 , where n 0 is a large enough constant computed from T k+1 .

The idea underlying this result is that if two runs ρ, ρ ′ of T on the same input have produced at some point partial outputs that are sufficiently far from each other, i.e. ∆(α, α ′ ) > n 0 for some prefixes α, α ′ of ρ, ρ ′ , then this difference can be augmented so much that it cannot be overtaken by the suffixes of ρ, ρ ′ that come after α, α ′ -this gives two modified runs that produce different outputs. As T is k-valued, if one considers k + 1 pairs of runs, then at least two of them must produce the same output and have lag at most n 0 .

The lag separation covering. Let Q be the state space of T and < a lexicographical order (induced by a total order on transitions) between pairs of runs of T with the same input, i.e. ρ < ρ ′ implies ρ, ρ ′ have the same input. One can construct a covering U n0 of T , whose states are the pairs (q, o), with q ∈ Q and o ∶ Q → 2 Γ * ×Γ * , such that for all initial runs ρ of U n0 ending in (q, o) and all states r ∈ Q, out(ρ) = out(ρ 1 ) (namely, the output produced by the run ρ of Un 0 is the same as that of the underlying run

ρ 1 of T ) o(r) = LD out(ρ 1 ), out(ρ ′ ) ∶ ρ ′ initial run of T ending in r such that ρ ′ < ρ 1 and ∆(ρ 1, ρ) ≤ n0
(note that the above pairs LD(out(ρ 1 ), out(ρ ′ )) have size at most n 0 , so the transducer U n0 is finite; for a proof of how these pairs can be maintained in the transitions of U n0 see [START_REF] Sakarovitch | On the decomposition of k-valued rational relations[END_REF]).

From U n0 , one can then construct a transducer V n0 whose successful runs with input w and output x simulate precisely the least runs among the successful ones of T with input w and output x. Formally, V n0 is obtained from U n0 by restricting the set of final states to those pairs (q, o) such that q is final in T and (ε, ε) ∈ o(r) for all r ∈ Q. Indeed, we have:

1. If ρ is a successful run of V n0 , then ρ 1 is a successful run of T and for all other successful runs ρ ′ of T with the same input and the same output, either ρ 1 < ρ ′ or ∆(ρ 1 , ρ) > n 0 . 2. For all pairs (w, x) in the transduction defined by T , if ρ ′ is the least successful run of T with input w and output x, then there is a successful run ρ of V n0 such that ρ ′ = ρ 1 . This shows that V n0 is equivalent to T .

In addition, the transducer V n0 is input-k-ambiguous. This relies on the choice of n 0 and can be shown by way of contradiction as follows. Suppose that V n0 admits k + 1 distinct successful runs ρ 1 , . . . , ρ k+1 on the same input w. By the combinatorial property stated above, there exist two indices i ≠ j such that ρ i 1 and ρ j 1 have the same input, the same output, and satisfy ∆(ρ i 1 , ρ j 1 ) ≤ n 0 . However, this would contradict property 1. above.

The multi-skimming covering. The last part of the proof is fully generic and consists in decomposing a k-ambiguous automaton A (e.g. the input automaton of V n0 ) into a finite union of unambiguous automata A 1 , . . . , A k (the construction can be easily lifted to the transducer V n0 by copying the outputs generated by the transitions).

Let A be a k-ambiguous automaton with state space Q. One first defines a covering B of A whose states are of the form (q, o), with q ∈ Q and o ∶ Q → {0, . . . , k -1}, such that for all initial runs of B ending in (q, o) and all states r, o(r) = {ρ ′ ∶ ρ ′ initial run of A ending in r such that ρ ′ < ρ 1 } (see again [START_REF] Sakarovitch | On the decomposition of k-valued rational relations[END_REF] for a construction that maintains the function o along the transitions of B).

Finally, one constructs some automata B 0 , . . . , B k-1 that differ from B only in the sets of final states. Formally, for each i = 0, . . . , k -1, one declares a (q, o) final in B i iff q ∈ F and ∑ r∈F o(r) = i, where F is the set of final states of A. Note that an initial run ρ of the automaton B i is successful iff ρ 1 is successful for A and there are exactly i successful runs of A that precede ρ 1 in the lexicographic ordering. In particular, the automata B 0 , . . . , B k-1 are all unambiguous and their union is equivalent to A.

5

The proof of the conjecture for 1-register SSTs

In this section we prove a decomposition theorem for finite-valued SSTs with a single register:

▸ Theorem 5. k-valued 1-register SSTs are effectively equivalent to finite unions of functional 1-register SSTs.

From the sketch of the proof of the decomposition theorem for one-way transducers we see that there are two important results that need to be generalized in order to lift the theorem to SSTs. The first of them is the combinatorial property related to the lag ∆(ρ, ρ ′ ). A noticeable difference is that, in the presence of an SST T with 1 register, partial outputs are constructed by adding symbols both to the right and to the left of the register of T . This means that, to correctly measure the distance between the register contents x, x ′ of runs, we need to take into account the possible contexts that can be added to both endpoints of x and x ′ . We thus modify the definition of lead or delay of a pair (x, x ′ ):

LD(x, x ′ ) = def (u, v, u ′ , v ′ ) ∶ u x v = u ′ x ′ v ′ , (u = ε) ∨ (u ′ = ε), (v = ε) ∨ (v ′ = ε) . The size of a tuple λ = (u, v, u ′ , v ′ ) ∈ LD(x, x ′ ) is λ = u + u ′ + v + v ′ .
Let reg(ρ) denote the register content at the end of an initial run ρ of T . Note that this is precisely the output produced by ρ if ρ is successful. Intuitively, a tuple λ ∈ LD(reg(ρ), reg(ρ ′ )) describes a possible alignment between the register contents at the end of ρ and ρ ′ . Such a tuple has one of the following forms (the annotations under the tuples describe succinctly the type of alignment between reg(ρ) and reg(ρ ′ )):

(ε, v v v, u ′ u ′ u ′ , ε) reg(ρ) reg(ρ ′ ) v u ′ (u u u, ε, ε, v ′ v ′ v ′ ) reg(ρ) reg(ρ ′ ) u v ′ (ε, ε, u ′ u ′ u ′ , v ′ v ′ v ′ ) reg(ρ) reg(ρ ′ ) u ′ v ′ (u u u, v v v, ε, ε) reg(ρ) reg(ρ ′ ) u v XX:8
On the decomposition of finite-valued SSTs Accordingly, we define the lag of a pair of initial runs (ρ, ρ ′ ) as the number

∆(ρ, ρ ′ ) = def max ρ = α β, ρ ′ = α ′ β ′ , α = α ′ min λ ∈ LD(reg(α),reg(α ′ ))
λ (as usual, we assume that min ∅ = ∞ > n for all n ∈ N).

The combinatorial property. Along the same line of the proof in Section 4, given a kvalued SST T with 1 register, we construct the SST T k+1 with k + 1 registers that simulates k + 1 copies of T running in parallel on the same input. Given a run ρ = (ρ 1 , . . . , ρ k+1 ) of T k+1 , we denote by ρ i the i-th run ρ i of ρ. To correctly work with T k+1 , we need to assume that T has been normalized in such a way that the register content can only grow. Formally, we say that T = (Σ, Γ, Q, {x}, x, U, I, E, F ) is normalized if for all register updates f ∈ U , f (x) contains exactly one occurrence of x. It is easy to transform any 1-register SST into an equivalent normalized SST.

▸ Lemma 6. One can normalize any 1-register SST.

We now turn towards the main combinatorial property:

▸ Proposition 7.
Given a normalized k-valued SST T , one can compute n 0 ∈ N such that, for all successful runs ρ of T k+1 , reg(ρ i ) = reg(ρ j ) and ∆(ρ i , ρ j ) ≤ n 0 for some i ≠ j.

Recall that the technique from [START_REF] Weber | Decomposing a k-valued transducer into k unambiguous ones[END_REF] for proving the combinatorial result for one-way transducers consists in augmenting the differences between pairs of runs of ρ, until the runs are shown to produce pairwise distinct outputs. In the case of SSTs, it becomes difficult to apply such a technique. Instead, we rely on a powerful result of Kortelainen [START_REF] Kortelainen | On the system of word equations x 0 u i 1 x 1 u i 2 x 2 . . . 1 2 . . . v m (i =[END_REF] which has been later improved and simplified by Saarela (Theorem 9 below) and that is related to solutions of word equations with iterated factors. Word equations will indeed be obtained by comparing the outputs produced by pumped versions of successful runs of T . Formally, we call loop of a run ρ any factor of ρ that starts and ends in the same state. A loop of ρ is maximal if it is not strictly contained in any other loop of ρ. Given a set L of pairwise non-overlapping loops of ρ, we denote by pump h L (ρ) the run obtained from ρ by repeating h times the loops in the set L (if h = 0 this amounts at removing the loops). The following lemma is simple but crucial for our result (notice that it does not hold in general for SSTs with more than one register).

▸ Lemma 8. Given an initial run ρ of a normalized 1-register SST and a set L of pairwise non-overlapping loops of ρ, one can factorize reg(ρ) as

u 0 v 1 u 1 . . . u 2m-1 v 2m u 2m in such a way that, for all h ∈ N, reg pump h L (ρ) = u 0 (v 1 ) h u 1 . . . u 2m-1 (v 2m ) h u 2m .
▸ Theorem 9 (Theorem 4.3 in [START_REF] Saarela | Systems of word equations, polynomials and linear algebra: a new approach[END_REF]). The set of solutions of an equation of the form

u 0 (v 1 ) h u 1 . . . u m-1 (v m ) h u m = u ′ 0 (v ′ 1 ) h u ′ 1 . . . u m-1 (v ′ m ) h u ′ m
where h is the unknown, is either N or a finite subset of N.

Since the loops of any run ρ of T k+1 can be equally seen as loops of the runs ρ 1 , . . . , ρ k+1 of T , we can write pump h L (ρ i ) whenever L is a set of pairwise non-overlapping loops of ρ. The following property is an immediate consequence of Lemma 8 and Theorem 9: ▸ Corollary 10. For every successful run ρ of T k+1 , every set L of pairwise non-overlapping loops of ρ, and every pair of indices i, j ∈ {1, . . . , k + 1},

reg(ρ i ) ≠ reg(ρ j ) implies ∃h 0 ∈ N ∀h ≥ h 0 reg pump h L (ρ i ) ≠ reg pump h L (ρ j ) .
We are now ready to prove Proposition 7 by way of contradiction, that is, we fix a large enough n 0 (see Lemma 11 below for the precise value of n 0 ) and we assume that there is a successful run ρ of T k+1 such that, for all i, j, reg(ρ i ) = reg(ρ j ) implies ∆(ρ i , ρ j ) > n 0 , and we show that T outputs at least k + 1 different words on the same input w, a contradiction with the k-valuedness of T . We will do so by exploiting an induction on the number of pairs of runs ρ i , ρ j with the same output. For the sake of brevity, we denote by c T the capacity of T , that is, the maximum number of symbols that are added to the content of the register during a single transition of T . We further define E(ρ) = (i, j) ∈ {1, . . . , k +1} ∶ reg(ρ i ) = reg(ρ j ) . We prove the following invariant, which leads towards a contradiction of k-valuedness of T :

▸ Lemma 11. If there is a successful run ρ of T k+1 with E(ρ) ≠ ∅ and ∀i, j (i, j) ∈ E(ρ) implies ∆(ρ i , ρ j ) > c T ⋅ Q k+1 (⋆)
then there is another such run ρ′ of T k+1 satisfying E(ρ ′ ) ⊊ E(ρ) and (⋆).

Proof. For every pair (i, j) ∈ E(ρ), we can split the run ρ at the first point where the lag exceeds the value c T ⋅ Q k+1 , that is, we can factorize ρ as ᾱi,j ᾱ′ i,j in such a way that ᾱi,j is the shortest prefix satisfying ∆(ᾱ i,j i , ᾱi,j j ) > c T ⋅ Q k+1 . Based on this, we choose a pair (i, j) ∈ E(ρ) that induces a factorization of ρ with the longest prefix ᾱi,j . Clearly, for all other pairs (i ′ , j ′ ) ∈ E(ρ), ᾱi ′ ,j ′ is a prefix of ᾱi,j , and hence

∆ ᾱi,j i ′ , ᾱi,j j ′ ≥ ∆ ᾱi ′ ,j ′ i ′ , ᾱi ′ ,j ′ j ′ ) = ∆ ρ i ′ , ρ j ′ > c T ⋅ Q k+1
Now that the pair (i, j) is fixed, we further factorize the suffix ᾱ′ i,j of ρ as follows: ᾱ′ i,j = β0 γ1 β1 . . . βm-1 γm βm where L = {γ 1 , . . . , γm } is a maximal set of pairwise non-overlapping maximal loops of ᾱ′ i,j . Further let ρ(h) = pump h L (ρ), for all h ∈ N, and observe that ρ(1) = ρ. We claim that there exists h i,j ∈ N such that for all h ≥ h i,j , reg(ρ (h) i ) ≠ reg(ρ (h) j ). Indeed, if this were not the case, then there would exist infinitely many h ∈ N such that reg(ρ (h) i ) = reg(ρ (h) j ). In particular, by Theorem 9, we would have reg(ρ (h) i ) = reg(ρ (h) j ) for h = 0. Note that ᾱi,j is also prefix of ρ(0) and the remaining part of ρ(0) has length at most Q k+1 , since otherwise it would contain a loop which is either contained in one of the βi 's, in which case we would get a contradiction with the maximality of L, or is spread between several βi 's, which would then be in contradiction with the maximality of the loops γ i . Now, consider the register contents at the end of the i-th and j-th runs of ᾱi,j and ρ(0) ; that is, let x = reg(ᾱ i,j i ), x ′ = reg(ᾱ i,j j ), x 0 = reg(ρ (0) i ), x ′ 0 = reg(ρ (0) j ). Since T is normalized, there exist some words u, v, u ′ , v ′ such that x 0 = u x v and x ′ 0 = u ′ x ′ v ′ . Moreover, since these words represent the content that is added to the registers by the updates performed along a suffix of ρ(0) of length at most Q k+1 , we know that u v and u ′ v ′ have length at most

c T ⋅ Q k+1 . Since x 0 = reg(ρ (0) i ) = reg(ρ (h) j ) = x ′ 0 , we know that (u, v, u ′ , v ′ ) ∈ LD(x, x ′ ). But, by definition, ∆ ᾱi,j i , ᾱi,j j = min λ ∶ λ ∈ LD(x, x ′ ) ≤ c T ⋅ Q k+1 and therefore, ∆ ᾱi,j i , ᾱi,j j ≤ u + v + u ′ + v ′ ≤ c T Q k+1 which contradicts the definition of ᾱi,j .
We have just proved that there is h i,j ∈ N such that, for all h ≥ h i,j , (i, j) ∈ E(ρ (h) ). Consider now the other pairs (i ′ , j ′ ) ∈ {1, . . . , k + 1} 2 ∖ E(ρ), namely, such that reg(ρ i ′ ) ≠ reg(ρ j ′ ). By Corollary 10, for every such pair (i ′ , j ′ ) there is h i ′ ,j ′ ∈ N such that, for all h ≥ h i ′ ,j ′ , reg ρ(h) i ′ ) ≠ reg ρ(h) j ′ ) . We can thus define ρ′ = ρ(h ′ ) , where h ′ is the maximum of the h i ′ ,j ′ 's for all (i ′ , j ′ ) ∈ E(ρ). In this way we get (i, j) ∈ E(ρ ′ ) and E(ρ ′ ) ⊊ E(ρ). Finally, it remains to verify that ρ′ satisfies the condition (⋆). Consider a pair (i ′ , j ′ ) ∈ E(ρ ′ ). Since ᾱi ′ ,j ′ is a prefix of ρ′ and ∆ ᾱi,j i , ᾱi,j j > c T ⋅ Q k+1 , we conclude that ∆ ρ′ i , ρ′ j > c T ⋅ Q k+1 as well. ◂

The lag separation covering. The second and last point that we need to explain is the construction of a lag separation covering of T , that is, a 1-register SST U n0 with the following properties. The states of U n0 are the pairs (q, o), with q ∈ Q, Q state space of T , and o some stored information determining a certain function ô ∶ Q → 2 Γ * ×Γ * ×Γ * ×Γ * (we will see soon why o cannot be directly defined as the function ô itself). For all initial runs ρ of U n0 ending in (q, o) and all states r ∈ Q, we must have reg(ρ) = reg(ρ 1 ) (namely, the register content at the end of the run ρ of Un 0 is the same as that of the underlying run ρ 1 of T )

ô(r) = ⋃ LD reg(ρ 1 ), reg(ρ ′ ) ∶ ρ ′ initial run of T ending in r such that ρ ′ < ρ 1 and ∆(ρ 1, ρ) ≤ n0 .
One can then transform U n0 into an input-k-ambiguous SST V n0 equivalent to T : this is done as explained in Section 4 by restricting the set of final states to those pairs (q, o) such that q is final in T and (ε, ε, ε, ε) ∈ ô(r) for all r ∈ Q. The proof that V n0 is input-kambiguous relies on the combinatorial property for normalized 1-register SSTs that we gave before. Finally, one applies the multi-skimming covering construction to V n0 in order to obtain k input-unambiguous SSTs T 0 , . . . , T k-1 whose union is equivalent to T . For the sake of brevity, let Λ ≤n0 be the set of tuples λ = (u, v, u ′ , v ′ ) of size at most n 0 , and let LD ≤n0 (x, x ′ ) = LD(x, x ′ ) ∩ Λ ≤n0 . The construction of U n0 boils down to showing that one can maintain the information about the set LD ≤n0 (reg(ρ), reg(ρ ′ )) while processing any two runs ρ, ρ ′ of T , provided that ∆(ρ, ρ ′ ) ≤ n 0 . Indeed, suppose that, by some means, we are able to construct a deterministic automaton A, with state space S, together with a function ˆ∶ S → 2 Λ ≤n 0 such that, whenever A reads an initial run (ρ, ρ ′ ) of T 2 (seen as a sequence of pairs of transition rules of T ), then A reaches a state s ρ,ρ ′ such that ŝρ,ρ ′ is either the set LD ≤n0 (reg(ρ), reg(ρ ′ )) or the empty set, depending on whether ∆(ρ, ρ ′ ) ≤ n 0 or not. Using the automaton A one can construct the covering U n0 as follows:

The states of U n0 are the pairs (q, o), with q ∈ Q and o ∈ S × (2 S ) Q . The component q is for simulating an initial run ρ of T on the given input. The stored information o consists of two parts: a state s ∈ S for simulating the run of A on (ρ, ρ) and a function t ∶ Q → 2 S for simulating the possible runs of A on inputs of the form (ρ, ρ ′ ), for all initial runs ρ ′ of T such that ρ ′ < ρ, with a partitioning based on the last state of ρ ′ . The latter part t also determines the function ô ∶ Q → 2 Λ n 0 associated with the stored information, that is, ô(r) = ⋃ s∈t(r) ŝ for all r ∈ Q.

The possible transitions of U n0 are of the form (q 1 , o 1 ) a f → Un 0 (q 2 , o 2 ), with o 1 = (s 1 , t 1 ) and o 2 = (s 2 , t 2 ), whenever τ = (q 1 , a, f, q 2 ) is a transition rule of T , (s 1 , (τ, τ ), s 2 ) is a transition rule of A, and, for all

r 2 ∈ Q, t 2 (r 2 ) = def s ′ ∶ (s1, (τ, τ ′ ), s ′ ) transition rule of A, τ ′ = (q1, a, f ′ , r2) transistion rule of T , τ ′ < τ
∪ s ′ ∶ s ∈ t1(r1), (s, (τ, τ ′ ), s ′ ) transition rule of A, r1 ∈ Q, τ ′ = (r1, a, f ′ , r2) transition rule of T .

The initial states of U n0 are the pairs (q, o 0 ), with o 0 = (s 0 , t 0 ), q initial state of T , s 0 initial state of A, and t 0 (r) = ∅ for all r ∈ Q. Similarly, the final states of U n0 are the pairs (q, o), with q final state of T .

Maintaining alignments under updates. After the previous argument, we are left to outline the construction of an automaton A that recognizes pairs of runs (ρ, ρ ′ ) and from the states of which we can extract LD ≤n (reg(ρ), reg(ρ ′ )) when ∆(ρ, ρ ′ ) ≤ n ,for some fixed ▸ Lemma 12. For all n ≤ ñ, if LD ≤n (x, x ′ ) is non-empty, then LD ≤ñ (x, x ′ ) ⊆ LD ≤n (x, x ′ ) ∪ G n,n+ñ (x, x ′ ) ∪ H n,n+ñ (x, x ′ ) ⊆ LD(x, x ′ ).

Tuples (LD ≤n (x, x ′ ), L ≤2n+2c T (x), R ≤2n+2c T (x), L ≤2n+2c T (x ′ ), R ≤2n+2c T (x ′ )) thus form an adequate state space for A when x and x ′ are the contents of the registers of the runs A is recognizing. This completes the proof of Theorem 5. And, as for Corollary 2, we obtain:

▸ Corollary 13. One can decide if two k-valued 1-register SSTs T , T ′ are equivalent.

Conclusions

We have proven a decomposition theorem for finite-valued 1-register SSTs, generalizing a similar result of Weber for one-way transducers. This result constitutes a milestone towards a decomposition theorem for finite-valued SSTs with multiple registers paving the way to the decidability of the equivalence problem, and to a correspondence with finite-valued two-way transducers. This way meets however two difficulties. The first difficulty is related to establishing the analogous of Proposition 7. Indeed, the latter proposition relies on the exact correspondence between the number of iterations of loops in a successful run of an SST and the number of iterations of certain factors in the produced output (cf. Lemma 8). This correspondence is broken in the presence of updates that concatenate different registers, namely, functions f such that, for some register x, f (x) contains at least two occurrences of distinct registers. In particular, iterating a loop may not result in iterating factors in the output and, even worse, it can be the case that iterating loops make two different runs become equal for all iteration except a finite number of them. This is a situation which does not show up when we only deal with one register. In view of this, one is either likely to need a more complicated induction in order to prove the analogous of Proposition 7 for SSTs with multiple registers, or has to pertain to an argument about string combinatorics that is more general than that of Kortelainen and Sarelaa.

Another difficulty, which is perhaps even more challenging, lies in the construction of the lag separation covering of T , and more precisely, in the problem of defining an appropriate notion of lead or delay between tuples of registers, and in maintaining this object in bounded memory while the registers are being updated. In particular, it seems that taking the obvious generalization of tuple measure we have taken for the 1-register case cannot be maintained using a finite memory.

number n. More specifically, we can focus on the following sub-goal: for a fixed n ∈ N, maintain a suitable data structure in bounded memory (the set of these structures form the state space of A) that determines LD ≤n (x, x ′ ) while the registers x, x ′ are being updated, as usual under the proviso that this set remains non-empty all along the computation. A possible way to attain this sub-goal is to try to compute the set LD ≤n (s x t, s ′ x ′ t ′ ) directly from a given set LD ≤n (x, x ′ ) and some given words s, t, s ′ , t ′ . Note that the actual content of the registers x, x ′ is not part of the input of this computational problem. Along this idea, we disclose the dependencies of the sets LD ≤n (xa, x ′ ) and LD ≤n (ax, x ′ ) from LD ≤n+1 (x, x ′ ):

Using these dependencies, one can describe any set of the form LD ≤n (x, x′ ), where x = s x t and x′ = s ′ x ′ t ′ , on the basis of the set LD ≤ñ (x, x ′ ) and the words s, t, s ′ , t ′ , where ñ = n + s + t + s ′ + t ′ . However, the fact that ñ may be larger than n seems to require a knowledge of alignments of arbitrarily large size, which we cannot assume. Luckily we can overcome this problem by exploiting the condition that LD ≤n (x, x ′ ) ≠ ∅ and by using an auxiliary data structure for maintaining some knowledge about the periodicities in x and x ′ . We say that a word

For example, abcab has period 3, but also period 5, 6, 7, etc. We define the two sets R(x) = def (u, p) ∶ x = u y and y p is periodic with period p x u p p L(x) = def (v, q) ∶ x = y v and q y is periodic with period q

Intuitively, (u, p) ∈ R(x) iff x begins with u and continues with a word y whose period p is preserved under extensions with p to the right, and similarly for (v, q) ∈ L(x) (see the figure). As usual, we let R ≤m (x) (resp. L ≤m (x)) be the restriction of R(x) (resp. L(x)) to the pairs of size at most m (the size being the sum of the lengths of the words in the pair).

For any fixed m ∈ N, it is possible to devise a bounded-memory data structure that can be maintained while the register x is being updated and that, at every moment, determines, the sets R ≤m (x) and L ≤m (x). The data structure basically recalls the following information: the exact content of x when its length is smaller than m, the unique pair of words (u, p) ∈ R ≤m (x) (if it exists) that has the smallest length u + p , the unique pair of words (v, q) ∈ L ≤m (x) (if it exists) that has the smallest length v + q . From now on we assume that the sets R ≤m (x), L ≤m (x), R ≤m (x ′ ), L ≤m (x ′ ) are known during any sequence of updates of x and x ′ .

Below we show that any non-empty set LD ≤n (x, x ′ ), paired with the information given by the sets R ≤ñ (x), L ≤ñ (x), R ≤ñ (x ′ ), L ≤ñ (x ′ ), fully determines the content of LD ≤ñ (x, x ′ ). Thanks to the dependencies given in Equations ( 1) and (2), this is sufficient for computing also the set LD ≤n (x, x′ ), where x (resp. x′ ) is obtained from x (resp. x ′ ) by prepending/appending at most ñn symbols.

We define two sets, G n,m (x, x ′ ) and H n,m (x, x ′ ), on the basis of the sets LD ≤n (x, x ′ ), L ≤m (x), R ≤m (x), L ≤m (x ′ ), R ≤m (x ′ ). The elements of G n,m (x, x ′ ) represent possible tuples of alignment type :

XX:12 On the decomposition of finite-valued SSTs

The set H n,m (x, x ′ ) is defined in a symmetric way, as if the underlying order of the words were reversed. Accordingly, its elements represent possible tuples of alignment type . For the sake of brevity, we omit the tedious definition of H n,m (x, x ′ ).

The following lemma gives a way to compute the set LD ≤ñ (x, x ′ ) (and hence LD ≤n (x, x′ ) for any x = s x t and x′ = s ′ x ′ t ′ , with s + t + s ′ + t ′ ≤ ñn): for this it suffices to construct LD ≤n (x, x ′ ) ∪ G n,n+ñ (x, x ′ ) ∪ H n,n+ñ (x, x ′ ) and then remove from it the tuples of size larger than ñ. Thanks to the lemma, this results in the set LD ≤ñ (x, x ′ ).


Hélène Prost

Amélie Buirette

Rachid Berbache

Aurélie Halipré

and research institutions in France or abroad, or from public or private research centers.

French


D Grondin

S Geara

P Breuil

J P Viricelle

P Vernoux

Influence of Electrodes Polarization on the Response of Resistive Soot Sensor

Keywords: Soot sensor, On-board diagnostics (OBD), Diesel particulate filter monitoring

This study reports on the influence of the polarization applied between platinum electrodes of a resistive soot sensor. The conductance measured between these electrodes represents the sensor response which increases during soot deposition over time at fixed parameters (soot flow, polarization). It is observed that a maximum response is obtained for an optimum polarization. This behavior is explained by equilibrium between the creation and destruction of inter-electrodes soot bridges.

Introduction

The negative effect of the vehicles exhaust on the health and the environment has clearly been demonstrated. The world health organization has classified the diesel engine exhaust to be carcinogenic [1]. In order to limit these pollutants, emission legislations for diesel engine become more and more stringent. From Euro 5, limits take in consideration the particulate number (PN) of emitted soot. To lower the PM emission, diesel light-duty vehicles have been equipped with diesel particulate filter (DPF). Due to the extreme conditions that take place in the DPF, it can be deteriorated. An on-board diagnostic sensor able to detect diesel particulate filter (DPF) failures is required.

Procedia Engineering, published by Elsevier Ltd. Volume 168, 2016, Pages 31-34, doi: 10.1016/j.proeng.2016.11.124 Therefore, the development of a cheap sensor effective for the measurement of both mass and PN concentration is necessary.

A resistive soot sensor for diesel particulate filter (DPF) failure detection was developed in a previous work [2]. The sensor consists in an alumina substrate with two platinum interdigitated electrodes. A platinum resistance heater on the other side is used for periodic regeneration. In reason of the carbon content of soot, these particles are electrically conductive. The conductance between the platinum electrodes (sensor response) as a function of time increases under a particulate matters (PM) flow during soot deposition.

When a polarization voltage is applied, soot bridges form between the electrodes, contrary to a continuous soot layer deposited without polarization (figure 1) [2]. a) 0 V b) 30 V Sensor response versus time shown in figure 2 strongly depends on the polarization voltage, and an optimum polarization corresponding to a maximum response can be seen, 30 V for given conditions. It was also demonstrated that this optimum value is dependent on the soot characteristics [3]. The objective of this study is the comprehension of this phenomenon. Procedia Engineering, published by Elsevier Ltd. Volume 168, 2016, Pages 31-34, doi: 10.1016/j.proeng.2016.11.124

Experimental

Soot was produced in a synthetic gas bench by the combustion of a mixture of propane/air thanks to a mini Combustion Aerosol Standard (CAST) burner (Jing Ltd. Switzerland). A more complete description of the bench and of the characterization of the produced soot can be found elsewhere [3,4].

Polarization was applied between the sensor electrodes with a Keitley 6430 equipped with remote pre amplification. An avalanche photodiode module Hamamatsu H6956 was used to measure flash emissions that are observed during a polarization voltage ramp. The measurements of the conductance and of the photodiode were synchronized by homemade LabVIEW program that monitors the instruments and records the sensor response.

The sensing element of the sensor was back on the stream to avoid direct impacts. The sensor was preloaded at steady state condition under a polarization voltage of 30 V. Then, it was removed from the bench, placed in a black box including the photodiode, and polarization voltage was continuously increased.

Results and discussion

Some observations were made in ambient air at fixed temperature of 200°C imposed by the heater, on soot preloaded sensors with optimum polarization (30 V for considered operating point). Then, electrode polarization was increased up to 200 V. Optical microscope image (figure 3) reveals flashes interpreted a soot combustion occurring at 200 V polarization. To confirm such visual observation, a similar experience with the simultaneous record of both the conductance and the signal of an avalanche photodiode was performed (figures 4a). When polarization voltage ramp starts from 10 V, the conductance first increases without flash emission, corresponding to soot heating by Joule effect. Indeed, with increasing polarization tension U applied to the sensors, and thus to the inter-electrodes soot bridges of a given resistance R, an electrical power U 2 /R is supplied to them, leading to soot bridge heating and consequent conductance increase due to the carbon soot negative temperature coefficient.

Then, for polarization above 40 V, the conductance decreases simultaneously with flash emissions recorded by the photodiode. This result proves the destruction of soot bridges by combustion ignited by Joule effect and also explains the optimum value observed previously (fig. 2) during soot deposition [3]. Effectively, from a certain value of polarization, as part of the formed soot bridges begins to burn, this value corresponds to an optimum for the soot collection in the fixed operating conditions. The interpretation made at the macro time scale was reinforced by the observations made with high sampling frequency (10 kHz) during previous experiment at around 60 V (figure 4b). It can be seen that each light flash, corresponding to soot combustion coincides momentarily to a positive conductance switch related to brief local temperature increase due to combustion heat.

To conclude, analysis of polarization voltage influence on sensor response allowed to understand the sensing mechanism. An optimum polarization voltage can be attributed to equilibrium between soot bridges creation promoted by polarization effect, and their destruction by combustion ignited at high voltage.

Figure 1 :

 1 Figure 1: Scanning electron Microscopy of a sensor with soot deposited during 2 hours under a) no polarization and b) a polarization of 30 V.

Figure 2 :

 2 Figure 2: Conductance variation versus time for fixed operating point at different polarization voltages and conductance versus polarization at 10 minutes (insert).

Figure 3 :

 3 Figure 3: Optical microscopy image showing flashes on a soot pre-loaded sensor (30V) in ambient air with 200 V polarization.

Figure 4 :

 4 Photodiode signal (mV)

Acknowledgements

The authors wish to acknowledge "Arc Environnement" from Region Rhone-Alpes for the funding and EFI Automotive car supplier for sensors manufacture.