Ramzi Ben Salah
email: ramzi.salah@imag.frmarius.bozga@imag.froded.maler@imag.fr

Marius Bozga

Oded Maler

On Interleaving in Timed Automata

We propose a remedy to that part of the state-explosion problem for timed automata which is due to interleaving of actions. We prove the following quite surprising result: the union of all zones reached by different interleavings of the same set of transitions is convex. Consequently we can improve the standard reachability computation for timed automata by merging such zones whenever they are encountered. Since passage of time distributes over union, we can continue the successor computation from the new zone and eliminate completely the explosion due to interleaving.

Introduction

Exploring the state space of timed automata [START_REF] Alur | A Theory of Timed Automata[END_REF] is a fundamental activity with numerous potential applications in circuit timing analysis, scheduling, verification of real-time software, performance analysis, etc. It is, however, a very difficult problem still waiting for a performance breakthrough despite efforts invested during the last 15 years. We hope that the results of this paper will advance us in this respect.

Partial-order methods have been widely reported in the discrete verification literature. They focus on that part of the state-explosion problem posed by the interleaving semantics, as illustrated by the example of Figure 1 where we see two automata and their asynchronous composition. Actions a and b are mutually independent and hence, in the product automaton, state 11 can be reached via two paths1 that commute in a "diamond". For certain simple reachability properties that do not mention paths and intermediate states, it is sufficient to explore only one of those paths. However, if additional non-commuting transitions are possible from the intermediate states, or if the properties are more sequential and less invariant under path permutations, the situation is more involved and has been a subject of numerous publications. This is not the topic of the present paper.

In the analysis of timed automata, diamonds pose additional problems. Due to the clock variables, paths that seem to commute on the transition diagram do not necessarily converge to the same extended state which includes also the clock values. Consider the timed automata appearing in Figure 2 together with their composition. In each automaton the transition from 0 to 1 resets the respective clock. The standard reachability computation algorithm for timed automata computes a discrete directed graph, the nodes of which are "symbolic states" of the form (q, Z) where q is a discrete state and Z is a zone, a convex set of clock valuations satisfying some conjunction of inequalities. Apply this algorithm to the automaton we obtain two zones associated with state 11, one in which x ≤ y (because in all runs along this path x is reset after y) and the other with y ≤ x. So here, in a situation where untimed reachability will converge to single state, timed reachability will generate several symbolic states from which the computation can be continued, leading very quickly to explosion. Roughly speaking, while the ordinary explosion associated with a product of n automata, each with m states will lead in the worst case to O(m n ) states, the additional splitting due to interleaving may result in O(n mn ) states, a fact that prevents verification of systems of modest size. 2In this paper we propose a solution to this problem, which is based on a new surprising3 result which shows that the set of all points in the clock space reached by runs consisting of interleaving of the same set of actions is convex. Since evolution distributes over union, zones that have been reached through different paths in the transition graph can be merged during reachability computation, thus eliminating the interleaving explosion. The rest of the paper is organized as follows. In Section 2 we give the definition of timed automata and their interaction. In Section 3 we prove our main result which is used in Section 4 to define a modified reachability algorithm whose superiority is experimentally confirmed. In Section 5 we discuss the applicability of the results to various forms of interaction, and conclude in Section 6 with a discussion of related work, in particular the idea of local time scales.

Timed Automata

We consider a composition A 1 ||A 2 || • • • ||A n of timed automata. Interaction can be defined using two types of mechanisms, the first one is by synchronized transitions and the other one, which is more expressive and useful, is by shared variables. To simplify the presentation we will use the former to present our result and discuss later its extension to state-based synchronization. For the same pedagogical reasons, we make additional simplifying assumptions concerning the form of invariants and guards, but the results extend naturally to any conjunction of timed inequalities. As for non-convex (disjunctive) conditions allowed by the original definition of timed automata, we have found no use of them in more than 10 years experience in the domain. 4 We also do not pay much attention to the distinction between strict and non strict inequalities which are irrelevant to convexity.

Definition 1 (Timed Automaton). A timed automaton is

A = (Σ, Q, C, I, ∆)
where Σ is a finite set of transition labels, Q is a finite set of states, C is a finite set of clocks, I is the staying condition (invariant), assigning to every q ∈ Q a conjunction I q of inequalities of the form c ≤ u, for some clock c and integer u, and ∆ is a transition relation consisting of elements of the form (q, g, a, r, q ) where q and q are states, a ∈ Σ is a transition label, g (the transition guard) is a conjunction of formulae of the form (c ≥ l) for some clock c and integer l and r ⊆ C is a set of clocks to be reset by the transition.

We assume one transition labelled a for every a ∈ Σ. A clock valuation is a function v : C → R ≥0 and a configuration of the automaton is a pair (q, v) consisting of a discrete state (location) and a clock valuation. We use r also to denote the reset function on clock valuation that sets the clock in r to zero and leaves the other intact. We use v + d to denote the clock valuation obtained from v by adding d to all clock values. A step of the automaton is one of the following:

-A discrete step: (q, v) a -→ (q , v ), for some transition (q, g, a, r, q ) ∈ ∆ such that v satisfies g and v = r(v).

-A time step: (q, v) d -→ (q, v + d) for some d ∈ R ≥0 such that v + d satisfies I q .
A compound step is a time step (possibly of a zero duration) followed by a discrete step:

(q, v) d,a -→ (q , v ) ≡ (q, v) d -→ (q, v + d) a -→ (q , v ).
A run of the automaton starting from a configuration (q 0 , v 0 ) is a finite sequence of compound steps ending in a time step.

ξ : (q 0 , v 0 ) d1,a1 -→ (q 1 , v 1 ) d2,a2 -→ • • • d k ,a k -→ (q k , v k ) d * -→ (q k , v k + d * ).
We use also the notation (q, v) ξ -→ (q , v ) for runs. We will define the interaction between the automata via a "distributed alphabet" Σ in the sense of the theory of traces [START_REF]The Book of Traces[END_REF]. For each automaton A i , let Σ i be its local alphabet, that is the set of transition labels it uses. Our composition semantics requires that all A i such that a ∈ Σ i should participate in an a-labelled global transition. Hence in any run of the global automaton an a-transition will be taken the same number of times in all A i such that a ∈ Σ i .

Definition 2 (Composition of Timed Automata). A composition of timed automata is

A = A 1 ||A 2 || • • • ||A n where each automaton is of the form A i = (Σ i , Q i , C i , I i , ∆ i ).
The sets of states and clocks of the automata are mutually disjoint.

The global automaton obtained from the composition is

A = (Σ, Q, C, I, ∆) where Q = Π n i=1 Q i , C = n i=1 C i and Σ = n i=1 Σ i .
We write global states as q = (q 1 , . . . , q n ) ∈ Q and global clock valuations over C as v = (v 1 , . . . , v n ). The semantics of the composition is given in terms of global steps as follows:

-A discrete step: (q, v) a -→ (q , v ), such that for every i either a ∈ Σ i and (q i , v i ) a -→ (q i , v i ) is a step of A i , or a ∈ Σ i and (q i , v i ) = (q i , v i ). -A time step: (q, v) d -→ (q, v + d) for some d ∈ R + such that v + d satisfies n i=1 I q i .
Global compound steps and runs are defined similarly to their local counterparts. It is sometimes (and this time in particular) useful to speak of the projection of a global run on each automaton. The projection ξ i of a global run ξ is obtained from ξ in two stages. First we "hide" transitions in which A i does not participate and collapse the time passages, that is apply successively the following transformation:

(q, v) d,a -→ (q , v ) d ,a -→ (q , v ) -→ (q, v) a,d+d -→ (q , v )
whenever a ∈ Σ i . After all such external transitions have been eliminated we project the run on the states and clocks of A i .

Finally let us define two additional notions. Two runs ξ, ξ of A are qualitatively equivalent if they go through the same sequence of discrete transitions and differ only in timing. We denote this fact by ξ ≈ ξ and write equivalence classes of ≈ by [ξ]. We say that ξ and ξ are locally equivalent, denoted by ξ ∼ ξ , if all their local projections are equivalent, that is, ξ i ≈ ξ i for every i. We denote equivalence classes of ∼ as ξ . Clearly, ≈ is stronger than ∼, and perhaps too strong. When ξ ∼ ξ , both runs agree on the order of local transitions while ξ ≈ ξ means that they agree also on their interleaving.

Main Result

We can now formulate our main result.

Theorem 1 (Convexity). Let Z be a convex timed polyhedron and let q and q be two global states of A. Let ξ be a run starting at q and ending in q . Then the set

R Z, ξ ≡ ξ ∈ ξ {v : ∃v ∈ Z (q, v) ξ -→ (q , v )} is convex.
The proof is given via a characterization of the reachable clock valuations by a quantified formula consisting of conjunctions of inequalities over clock values and auxiliary variables. Since convex sets are closed under projection the result follows. For economy of notation we assume that ξ is such that each automaton A i makes exactly k steps. The restriction of A i to the states and transitions involved in the run is of the form depicted in Figure 3.

• • • g i 1 , a i 1 , r i 1 g i k , a i k , r i k I i 0 I i 1 I i k-1 I i k q i 0 q i 1 q i k-1 q i k Fig. 3. The part of A i which participates in ξ i .
As a first step we extend the description of local runs to include the time stamps of the transitions:

ξ i : (q i 0 , v i 0 , t i 0 ) → (q i 1 , v i 1 , t i 1 ) → • • • → (q i k , v i k , t i k ) → (q i k , v i k+1 , t i k+1
). Each t i j variable denotes the absolute time in which the corresponding transition has been taken. Every global run in ξ is completely characterized by the values t i j and v i j for i = 1..n and j = 0..k + 1. All those runs satisfy the natural local ordering among time stamps, i.e. t i j ≤ t i j+1 , while those that are also ≈-equivalent agree also on the ordering of time stamps of different automata, which characterize the particular interleaving (shuffle) of the local runs.

We can now proceed to the logical characterization. We will use the following auxiliary notations and abbreviations: q j = (q 1 j , . . . q n j ) for global states, v j = (v 1 j , . . . v n j ), for global clock valuations, v i = {v i 0 , . . . , v i k }, for the set of valuations appearing in a local run ξ i and t i = {t i 0 , . . . , t i k } for the set of local time stamps. The set of all values that characterize a run are v = i v i , and t = i t i . The predicates {Φ i j } characterize the clock values and time stamps in a valid step j of A i .

Φ i j (v i j-1 , t i j-1 , v i j , t i j ) ≡        ∃d d = t i j -t i j-1 ∧ I i j-1 (v i j-1 + d) ∧ g i j (v i j-1 + d) ∧ v i j = r i j (v i j-1 + d)
This is nothing but a recapitulation of the definition of a compound step, namely that time passage does not violate the staying condition, the transition guard is satisfied and that a reset takes place. Note that this definition is invariant under a shift of global time, that is, Φ i j (v, t, v , t ) is equivalent to Φ i j (v, t + d, v , t + d) for every d. We can now define what constitutes a valid run of A i in isolation, without taking into account synchronization constraints. We keep this definition shift-invariant as well and do not yet insist on the initial zone which is defined globally.

Φ i (t i , v i ) = k j=1 Φ i j (v i j-1 , t i j-1 , v i j , t i j )
The predicate which defines what constitutes a valid global run is a conjunction of the conditions for local runs with additional conditions that take care of all the synchronization aspects, including the fact that all runs start and terminate simultaneously. For every a ∈ Σ let S a = {(i, j) : a i j = a} be the set of steps that synchronize on a. To force all a-transitions to take place at the same time we define the predicate

Ψ a (t) ≡ (i,j),(i ,j )∈Sa t i j = t i j .
The conditions for a valid global run starting at Z 0 are then:

Φ(t, v) =            t 1 0 = t 2 0 = • • • = t n 0 ∧ v 0 ∈ Z 0 ∧ n i=1 Φ i (v i , t i ) ∧ a∈Σ Ψ a (t) ∧ t 1 k+1 = t 2 k+1 = • • • = t n k+1
Note that the first and last conditions can be viewed as synchronization conditions for two additional fictitious transitions "start" and "end" in which all automata participate. This set is a convex subset of the space consisting of all valuations and time stamps in the run, and so is its projection on the last n dimensions which is the reachable set:

R Z, ξ (v k+1 ) ≡ ∃t∃v 1 , . . . , v k Φ(t, v 1 , . . . v k , v k+1 ).
Let us mention that the result extends naturally to arbitrary "linear" hybrid automata with convex guards and invariants.

Application to Reachability Computation 4.1 A Modified Algorithm

We will now modify the standard reachability computation algorithm for timed automata to take advantage of this result. The idea is to generate symbolic states in a breadth-first manner and at each level merge those reached by the same set of compound steps. To identify those we need to decorate symbolic states with (partially ordered) path information. A shuffle expression over Σ is α = α 1 || . . . ||α n with α i ∈ (Σ i ) * . Concatenation of a shuffle expression and a symbol a is defined as

(α 1 || . . . ||α n ) • a = (β 1 || . . . ||β n ) where β i = α i if a ∈ Σ i and β i = α i • a otherwise.
Reachability computation for timed automata [START_REF] Henzinger | Symbolic Model-checking for Real-time Systems[END_REF] is based on zones (timed polyhedra) which are expressed as conjunctions of rectangular inequalities of the form c ≤ d or c ≥ d and diagonal inequalities of the form cc ≤ d for clocks c, c and integer d. A symbolic state is a pair (q, Z) where Z is a zone. The a-successor of a symbolic state (q, Z) such that q admits an a transition is defined as

Suc a (q, Z) = {(q , v ) : ∃v ∈ Z ∃d ≥ 0 (q, v) d,a -→ (q , v ).
The computation (q , Z ) = Suc a (q, Z) is done by first applying "time passage" to Z, intersecting the result with I q and with the transition guard and then applying the corresponding reset. This computation costs O(n 3 ) time for n clocks.

Algorithm 1 performs this computation. At each iteration Waiting is a list of extended zones to be explored, all reached by the same number of transitions. We compute the successors of all those symbolic states and put them in a list New. The Merge procedure scans New and replaces every subset of symbolic states of the form {(q, Z 1 , α), . . . , (q, Z m , α)} by a single state (q, Z, α) where Z is the convex hull of all these zones. From our result it follows that Z is exactly the union of the zones. Note that the path labels of a zone need not be kept after its successors have been computed. This also guarantees termination due to the finite number of zones.

Algorithm 1 (New Reachability Algorithm)

Explored:= New:=∅ Waiting:={(q 0 , Z 0 , ε||..||ε)} while Waiting = ∅ do for each (q, Z, α) ∈ Waiting such that (q, Z) ∈ Explored do for each a ∈ Σ do New :=New∪{(Suc a (q, Z), α • a)} Explored := Explored ∪{(q, Z)} Waiting := Merge(New) return(Explored)

Experimental Results

To confirm the complexity reduction empirically we have first tested a preliminary implementation of Algorithm 1 restricted to products of chain-like automata. Such automata are notorious for generating state explosion due to interleaving. We have considered two simple families of synthetic benchmarks shown in Figure 4. The first consists of parallel compositions of n independent reset sequences of length m each. The second class consists of parallel compositions of k independent synchronization chains, each being a parallel composition of n synchronized sequences of length m. A synchronized sequence (A ij ) alternates between actions that synchronize with the left (a i,j ) and the right (a i+1,j ) neighbor while separating them by at least 4 time units. The experimental results obtained for the two benchmarks for different values of n, m and k are summarized in Table 1. Each entry in the table is of the form B/C where B is the number of symbolic states encountered in an ordinary breadth-first exploration, while C is the number of states explored by Algorithm 1. We limit ourselves to instances with less than 10 6 symbolic states, and use the ⊥ symbol to denote the fact that this limit has been reached. Let us note that we achieve an exponential reduction both for the interleaving of independent actions (reset sequences) and for strongly-synchronized actions (a single synchronization chain with k = 1). The reduction is clearly much more impressive in the synchronized case, where reductions based on partial order or symmetry [HBL + 03] are not directly applicable.

q i 1 q i 0 q i m τ i /x i 0 n i=1 τ i /x i := 0 q ij 0 q ij 1 q ij m a ij /x ij := 0 [x ij ≥ 4] a i+1j a ij /x ij := 0 r ij 0 n i=1 k j=1
We have then implemented Algorithm 1 into the IF toolset [START_REF] Bozga | IF-2.0: A Validation Environment for Real-Time Systems[END_REF] and tested its performance on several publicly-available benchmarks. Table 2 compares the performance of the new algorithm on the Fisher mutual-exclusion protocol benchmark with other reported results. We compare with old Kronos results reported in [T98], Uppaal results reported in [U] and results obtained with IF without using the new algorithm. It is interesting to note that although our new algorithm performs much better than the standard Uppaal machinery, their performances are similar when the convex-hull approximation option of the latter is employed. Our result shows that this "approximation" can be easily made exact.

Generalizations and Limitations

Let us discuss briefly the applicability of our result to more general modes of interaction between timed automata. A crucial condition for expressing synchronization constraints in a conjunctive form is that in every abstract run, every transition admits a unique set of transitions with which it is has to synchronize. This condition is fulfilled by requiring that whenever an a-transition takes place, all automata having a in their alphabet must participate. If a transition could choose some subset of the other transitions to synchronize with, Φ may contain disjunctions that cannot be eliminated and the result no longer holds. State-based synchronization in which the state of one or more automata may appear in the invariants and transition guards of other automata is more general and has a more asymmetric flavor as one automaton may enable a transition in the other without being obliged to take a transition by itself. Suppose A 1 can take a transition when A 2 is in state q and consider an abstract run in which A 1 takes this transition and A 2 passes through q twice (see Figure 5). Let t be the time stamp of the A 1 transition, and let [t 1 , t 2 ] and [t 3 , t 4 ] be the time intervals in which A 2 stays in q. The synchronization condition in this case will be disjunctive:

t ∈ [t 1 , t 2 ] ∨ t ∈ [t 3 , t 4 ].
If, however, the disabling of the A 1 transition is always accompanied by an explicit transition in A 1 the run that synchronizes with the first sojourn in q and the one synchronizing with the second one, are not qualitatively equivalent and the result is preserved. This property holds, for example, in the automata we use to model bi-bounded inertial delays [START_REF] Maler | Timing Analysis of Asynchronous Circuits using Timed Automata[END_REF] as well as in models derived from free-choice Petri nets. Another illuminating example which is particularly important for our motivating application domain (circuits) is the following: let A x , A y and A z be three Boolean automata modeling an AND gate z = x ∧ y and consider runs in which both x and y rise from 0 to 1 and consequently z rises as well. Denoting the respective time stamps by t x , t y and t z , the synchronization condition is of the form

q true A 1 A 2 A 1 q ¬q q q ¬q q
(t x ≤ t y = t z ) ∨ (t y ≤ t x = t z )
or equivalently t z = max{t x , t y }, which does not define a convex set. In order to apply Algorithm 1 correctly to systems admitting this type of synchronization we need to split every such transition to several copies, each with a unique synchronization context.

Let us remark that when the local automata are acyclic and reverse-deterministic (no state is entered via two different sequences of transitions), all global symbolic states that agree on the discrete state are reached via the same set of transitions. Hence our result can be exploited without decorating the states with path information.

Related Work and Discussion

The application of partial-order techniques to timed systems has been subject to several publications [R94,YS97,DGKK98,BJJY98,M99,LNZ05,ZYN03] but nothing that resembles our simple and easily-usable result has been explicitly stated. Neither has any solution that works in practice been reported so far.

The closest work, at least in spirit, to ours is that of Niebert et al. [ZYN03,LNZ05] who are more ambitious with respect to full-fledged partial-order reductions and use "event zones" rather than the standard "clock zones" used in the present paper. Event zones contain sufficient additional dimensions to represent dependency such that all representatives of a trace lead to the same event zone. It might be the case that the union that we compute here could be extracted (and proved to be convex) using their results. It would be interesting to compare the reductions provided by the two approaches in terms of scope and performance.

An interesting idea which was first proposed in [START_REF] Bengtsson | Partial Order Reductions for Timed Systems[END_REF], inspired by distributed simulation, is to use local time scales, that is to compute successors for each automaton separately on its own clock subspace, and somehow combine these local zones upon synchronization. Although the idea is aesthetically pleasing, it suffers from several problems including the implicit global synchronization that takes place at time zero, and the fact that you need to augment each automaton with an additional clock that measures its corresponding total elapsed time. This idea, however, inspired our proof of convexity.

We prove, nevertheless, a small result which indicates the circumstances under which local time scales can be effectively exploited. We present the result informally. Consider two automata A 1 and A 2 and a prefix of a global run that reaches a global state (q 1 , q 2 ), and in which each of the two has passed through a local state in which all its clocks were inactive. 5 If no synchronized action has taken place since then, one can see that if q 1 → q 1 and q 2 → q 2 via synchronization-free local runs, then (q 1 , q 2 ) → (q 1 , q 2 ) in the product automaton. The reason is that because of the clock inactivity, each of the local runs can be "delayed" and every local state that can be reached at time t can be reached as well at any t ≥ t and hence any pair of local states can be made to be reached simultaneously. This implies that after such a "desynchronization" point, reachable sets can be computed separately for each automaton and be merged via intersection before the next synchronization. This observation can be useful for verifying products of automata that repeatedly go through such inactive states.

As a final remark, let us note that reducing the number of zones by taking their convex hull has been considered in the past [START_REF] Daws | Model Checking of Real-Time Reachability Properties Using Abstractions[END_REF] but always as an over-approximation. We speculate that the reason for not discovering the result of the present paper is due to the fact that the systems studied were cyclic, in which the same discrete state could be reached by different paths, not all of which being permutations of the same set of transitions. That is why the possibility of exact convex hull escaped the attention. In general we think that looking at the structure of individual runs can give insights that are sometimes masked by focusing exclusively on the reachability graph representation.

Fig. 1 .

 1 Fig. 1. Two automata with independent action a and b, and their composition.

Fig. 2 .

 2 Fig. 2. Two timed automata, their composition and an example of reachability computation.

Fig. 4 .

 4 Fig. 4. structure of the synthetic benchmarks.

Fig. 5 .

 5 Fig. 5. Automata A 1 ||A 2 do not satisfy Theorem 1 while 1 ||A 2 do.

Table 1 .

 1 results on the synthetic acyclic benchmarks.

		n=2		n=4		n=6	n=8	n=10
	Independent reset sequences
	m=1	5 / 4		65 / 16	1957 / 64 109601 / 256 ⊥ / 1024
	m=2	13 / 9		633 / 81	75973 / 729	⊥ / 6561	⊥ / 59049
	m=3	25 / 16		2713 / 256 732529 / 4096 ⊥ / 65536	⊥ / ⊥
	Synchronization chains k = 1
	m=1	4 / 4		6 / 6		8 / 8	10 / 10	12 / 12
	m=2	8 / 8		37 / 17	236 / 30	1600 / 47	10949 / 68
	m=3	12 / 12		86 / 32	1441 / 72	30841 / 140 660615 / 244
	Synchronization chains k = 3
	m=1	2012 / 64 812375 / 216	⊥ / 512	⊥ / 1000	⊥ / 1728
	m=2 97142 / 512	⊥ / 4913	⊥ / 27000	⊥ / 103823 ⊥ / 314432
	m=3 745197 / 1728 ⊥ / 32768	⊥ / 373248	⊥ / ⊥	⊥ / ⊥
	Size Kronos Uppaal Uppaal-A	IF	IF-U
	2	-/-	-/0.01s	-/0.00s	29/0.003s	18/0.002s
	3	-/-	-/0.03s	-/0.01s	165/0.01s	53/0.01s
	4	752/-	-/0.23s	-/0.06s	1099/0.07s	164/0.03s
	5 3552/-	-/5.09s	-/0.29s	8453/1.07s	527/0.04s
	6 16320/--/310.97s	-/1.34s	74939/21.06s	1726/0.20s
	7 73620/--/51598.17s -/5.89s 762429/595.75s	5693/1.75s
	8	⊥/⊥		⊥/⊥	-/25.83s	⊥/⊥	18792/5.73s
	9	⊥/⊥		⊥/⊥	-/113.53s	⊥/⊥	61883/28.42s
	10	⊥/⊥		⊥/⊥	-/498.88s	⊥/⊥	202994/367.76s
	11	⊥/⊥		⊥/⊥	-/2525.31s	⊥/⊥	662873/4489.23s

Table 2 .

 2 Results on the Fisher protocol benchmark. The Uppaal-A column corresponds to results obtained using the convex-hull approximation, while the IF-U column represents our new algorithm. Table entries represent the number of symbolic states and computation time. The symbol "-" means " not reported" (or "irrelevant" for the case of computation time on older computers) and ⊥ means "too big".

In general, n! paths when there are n transitions.

Note that if we can push the size limit of timed verification toward non-trivial systems, the rest of the battle against explosion can continue from there using abstraction-based methods like the ones we have recently proposed[START_REF] Ben Salah | On Timing Analysis of Combinational Circuits[END_REF][START_REF] Ben Salah | Automatic Abstraction of Timed Components[END_REF].

What is surprising is the fact that it has not been discovered before by all those working in the domain, the authors included.

The tendency to look for results proved for the "most general" definition, inherited uncritically from mathematics, can be sometimes very counter-productive in domains which are still evolving. Perhaps this could be one of the reasons for the sterility of certain branches of theoretical computer science.

A clock is inactive in a state if along any path starting in that state it will be reset before being tested. This fact has been used to reduce the dimension of reachability computation[START_REF] Daws | Reducing the Number of Clock Variables of Timed Automata[END_REF].

Acknowledgment This paper has benefitted from discussions with P. Niebert.


J M Anderlohr
email: jorg.anderlohr@ifp.fr

A Piperel

A Pires Da Cruz

R Bounaceur

F Battin-Leclerc

P Dagaut

X Montagne

INFLUENCE OF EGR COMPOUNDS ON THE OXIDATION OF AN HCCI-DIESEL SURROGATE

Keywords: HCCI, EGR, JSR, kinetic modelling, n-heptane/toluene blend

This paper presents an experimental and numerical study of the impact of various additives on the oxidation of a typical automotive surrogate fuel blend, i.e. n-heptane and toluene. It examines the impact of engine re-cycled exhaust gas compounds on the control of a Homogeneous Charge Compression Ignition (HCCI) engine. A series of experiments were performed in a highly diluted Jet-Stirred Reactor (JSR) at pressures of 1 and 10atm (1atm = 101325Pa). The chosen thermo-chemical conditions were close to those characteristic of the pre-ignition period in an HCCI-engine. The influence of various additives, namely nitric oxide (NO), ethylene (C 2 H 4 ) and methanol (CH 3 OH), on the oxidation of a n-heptane/toluene blend was studied over a wide range of temperatures (550-1100K), including the zone of the Negative Temperature Coefficient (NTC).

A new detailed chemical kinetic reaction mechanism is proposed for the oxidation of the surrogate fuel. It includes reactions of NO, methanol (CH 3 OH) and ethylene (C 2 H 4 ) and is used to explain the obtained experimental data. The mechanism is further used to theoretically study the impact of other Exhaust Gas Recirculation (EGR) compounds on the hydrocarbon oxidation, namely ethane (C 2 H 6 ), formaldehyde (HCHO) and carbon monoxide (CO).

INTRODUCTION

The mode of Homogeneous-Charge-Compression-Ignition (HCCI) in internal combustion engines is currently the subject of many research projects [1][2][3]. The HCCI-engine combines advantages of Spark Ignition (SI) engines with those of Compression Ignition (CI) engines. The homogenous fuel/air mixture guarantees low particulate emissions and the high dilution permits very low production of nitric oxides (NO x ), while the principle of CI assures a high efficiency close to that of a diesel engine. The main challenge of operating HCCI combustion engines is the control of auto-ignition. Various strategies for auto-ignition control are known [1]. A promising one is Exhaust Gas Recirculation (EGR) [4]. The principle of EGR is to induct an exhaust gas fraction into the combustion chamber together with the fresh gases. EGR has also the advantage of reducing the maximum combustion temperature in the engine and so the production rate of thermal-NO. However, HCCI exhaust gases are composed of many different species including products from condensed fuel, Unburned HydroCarbons (UHC) and traces of NO x . Piperel et al. [8] have recorded along the EGR pipe concentrations of CO between 0.032 and 0.74%, NOx between 2 and 100 ppmv, ethylene between 45 and 115 ppmv and formaldehyde between 20 and 50 ppmv. It is known that the dilution by EGR impacts strongly on HCCI-engine control, but it is also supposed that the chemical composition of the EGR-gases governs HCCI combustion processes. While the impact of recycled NO x is known to be important for the kinetics of oxidation of UHC [START_REF] Amano | 27 th Symposium of Combustion[END_REF][START_REF] Dubreuil | [END_REF][7], the influence of other recycled species has not yet been comprehensively assessed [4]. A n-heptane/toluene mixture was used as a diesel surrogate with n-heptane having a cetane number close to diesel and toluene representing the aromatic fraction of a diesel fuel.

In the first part of this study, we focus on the impact of nitric oxide (NO), ethylene (C 2 H 4 ) and methanol (CH 3 OH) on the surrogate fuel oxidation. Ethylene is an important intermediate in the combustion of hydrocarbons and therefore it is present in the EGR. Methanol is a potential component of future automotive fuel blends [9] and the comprehension of its interactions with the proposed automotive surrogate n-heptane/toluene is of interest.

A series of experiments were performed to evaluate the influence of NO, ethylene and methanol on the oxidation of the surrogate fuel using a Jet Stirred Reactor (JSR) over a wide range of temperatures, covering the zone of the Negative Temperature Coefficient (NTC). The experiments were limited to fuel-lean conditions (equivalence ratio 0.75), relevant for HCCI operation, and were conducted at 1 and 10atm (1atm = 101325Pa).

A detailed chemical kinetic reaction mechanism for the oxidation of a n-heptane/toluene mixture including effects of NO, ethylene and methanol addition is proposed to explain the experimental data obtained. In the second part of this study, the mechanism was used to numerically analyze the impact of other EGR components on the fuel oxidation, namely ethane (C 2 H 6 ), formaldehyde (HCHO) and carbon monoxide (CO).

EXPERIMENTAL PROCEDURE AND RESULTS

The experiments were performed in a fused silica JSR heated by a regulated electrical resistance system. The JSR and heating system are surrounded by insulating material and a pressure-resistant jacket, allowing operating pressures up to 10atm [START_REF] Dubreuil | [END_REF]- [9]. It consists of a sphere with an internal volume of 29.5cm 3 equipped with four injectors. N-heptane (99% pure) and toluene (99% pure)

were premixed at the desired composition after thorough ultrasonic degassing. The fuel was pumped using a micro piston High-Performance-Liquid-Chromatography (HPLC) pump and sent to an atomizer-vaporizer assembly. Thermal mass-flow controllers were used for all gases. For atomization, a nitrogen gas-flow of 0.05m 3 /h was used. Samples were taken at steady state using a sonic quartz probe.

A high degree of dilution was applied (~98% in mole of molecular nitrogen) minimizing the fuels' heat release. Temperature gradients measured inside the reactor by a thermocouple lay below 10K (typically 2-5K) while concentration gradients could not be detected. Good thermal and mixture homogeneities, as well as experimental reproducibility, equivalent to those obtained in previous experiments performed with the same equipment were achieved [10], [11]. Samples of reacting mixtures were taken by sonic probe sampling and collected in 1x10 -3 m 3 Pyrex bulbs at around 40x10 -3 atm for immediate analysis with two Gas-Chromatographs (GC). One GC was equipped with a Flame-Ionization-Detector (FID) and the other one with a Thermal-Conductivity-Detector (TCD). In addition, on-line Fourier-Transform-InfraRed (FTIR) analyses were performed. The sampling probe was connected to a temperature controlled gas cell (413K) via a heated Teflon tube.

The sample pressure in the cell was 0.2atm. This equipment enabled the measurements of water (H 2 O), carbon dioxide (CO 2 ), CO, C 1 -C 5 hydrocarbons, n-heptane and toluene (by FTIR-GC) and permanent gases, molecular hydrogen (H 2 ) and oxygen (O 2 ) (by TCD-GC). The carbon balance was checked for every sample (100±5%). In order to observe the fuel oxidation from low to high conversion, the experiments were performed at a constant mean residence time of 0.7s at 10atm (0.07s at atmospheric pressure) and an equivalence ratio of 0.75 by increasing stepwise the gas-temperature inside the reactor from 560 to 1190K.

Experiments were performed for the oxidation of the n-heptane/toluene blend with addition of various concentrations of methanol, ethylene and NO. Because at atmospheric pressure the addition of these species shows only little impact on the oxidation of n-heptane and toluene due to a lower global reactivity, results are only shown for a pressure of 10atm. Figure 1 presents the measured concentrations of different species as functions of temperature at an equivalence ratio of 0.75 for pure fuel, a fuel/NO mixture and a mixture of fuel/ethylene/methanol. The initial concentrations of n-heptane and toluene were held constant at 900 and 100 ppmv respectively, and the influence of the additives methanol (130ppmv), ethylene (200ppmv) and NO (100ppmv) was tested separately and together. The additive concentrations chosen may slightly exceed those found in EGR [8], but the objective is to understand their general impact on fuel oxidation. The impact of the addition of ethylene on the mixture's reactivity as well as on the formation of intermediates is similar to that caused by the addition of methanol. Experimental results are then only shown for the addition of both ethylene and methanol together. Concerning the addition of NO, results are shown for mixtures of n-heptane/toluene with the addition of NO only.

FIGURE 1

Figures 1a (n-heptane) and 1b (toluene) show that the addition of NO inhibits the oxidation of the fuel at low temperatures (<700K), accelerates it at high temperatures (>850K) and reduces the intensity of the NTC. The accelerating effect above 800K is also observed on the oxygenconcentration profile (Fig. 1c), showing that the addition of NO induces a strong depletion above 900K. This result agrees with the observations of Dubreuil et al. [START_REF] Dubreuil | [END_REF] and Moréac et al. [7] in their studies on the complex impact of NO on HC oxidation. At temperatures below 850K, the addition of ethylene and methanol leads to a slightly retarded oxidation of the fuel, whereas at higher temperatures, this addition has no impact on the fuel oxidation.

For temperatures below 850K, the effect of NO on the ethylene concentration profile (Fig. 1d) is negligible. Above 850K, the formation of ethylene is strongly reduced when NO is added and the ethylene peak-concentration, observed at 850K, decreases strongly. Below 850K, when ethylene is added, its measured concentrations are increased by the magnitude of the initially added amounts.

At higher temperatures, ethylene addition does not affect its measured concentration profiles, which become quasi independent of the initially added ethylene concentration.

Figure 1e shows that generally, at around 650K, a production peak of methanol from the fuel oxidation is observed. This production is reduced when NO is added. For temperatures above 700K and in the case of methanol-addition, the methanol concentration profile includes also a NTC-zone.

One observes that the ethane concentration (Fig. 1f) is not greatly affected by the addition of ethylene and methanol, but is strongly reduced when NO is added. The presence of NO leads to an increase of the formaldehyde concentration in the NTC-region (700-800K) and to a decrease at higher temperatures. This result is consistent with the observations made by Dagaut et al. [12]. At temperatures below 850K the addition of methanol and ethylene increases the measured formaldehyde concentration (Fig. 1g), but at higher temperatures, the formaldehyde concentration profile is unchanged by their addition.

Ethylene and methanol addition has little effect on the formation of CO (Fig. 1h), H 2 (Fig. 1i), H 2 O (Fig. 1j) and CO 2 (Fig. 1k). At temperatures above 800K, these additives slightly increase the concentrations of these oxidation products. In contrast, the addition of NO increases the CO and hydrogen production between 800K and 900K, and considerably decreases it at higher temperatures. Consequently, the formation of H 2 O and CO 2 is also increased by the addition of NO at these temperatures.

DESCRIPTION OF THE DETAILED KINETIC MODEL

To explain the obtained experimental results, a new kinetic reaction mechanism was developed and used to simulate the oxidation of n-heptane/toluene blends in presence of ethylene, methanol and NO x . This model is based on a mechanism generated by EXGAS-ALKANES (EA) according to the rules described by Buda et al. [13] and on the toluene mechanism of Bounaceur et al. [14]. It also includes reactions for the co-oxidation of n-heptane and toluene. Thermochemical data for molecules and radicals were calculated by the THERGAS software [15], which is based on group and bond additivity methods proposed by Benson [START_REF] Benson | Thermochemical Kinetics[END_REF] and yields 14 polynomial coefficients according to the CHEMKIN-II formalism [START_REF] Kee | [END_REF].

Mechanism for the oxidation of n-heptane

The mechanisms generated by EA include three sub sets [13], [18]:

A C 0 -C 2 reaction base [19] involving species with up to two carbon atoms and including kinetic data mainly taken from the evaluations of Baulch et al.

[20] and Tsang and Hampson [21]. The reactions of ethylene and methanol are part of this base. Reactions of methanol are mainly taken from Tsang [22]. The pressure dependent rate coefficients are obtained using the formalism proposed by Troe [23].

A comprehensive primary mechanism. It considers only initial organic compounds together with oxygen as reactants. It includes all the usual low and intermediate temperature reactions of alkanes (unimolecular and bimolecular initiations, additions to oxygen, radical isomerizations, formation of conjugated alkenes, smaller alkenes, cyclic ethers, aldehydes, ketones, hydroperoxides species, H-abstractions by small radicals, disproportionation between alkylperoxy and hydroperoxy (•OOH) radicals). The disproportionation between methylperoxy and other alkylperoxy radicals, leading to the formation of oxygen, aldehyde and methanol molecules, as proposed by Lightfoot et al. [24], was also added in order to explain the observed formation of methanol around 650K.

A lumped secondary mechanism [18]. The molecules formed in the primary mechanism, with The improved mechanism will be further referenced as modified EA-version.

Mechanism for the oxidation of toluene and co-oxidation reactions

The toluene model includes sub-mechanisms for :

The oxidation of benzene.

The oxidation of unsaturated C 3 -C 4 species.

A primary mechanism including reactions of toluene and benzyl, methylphenyl, peroxybenzyl, alcoxybenzyl and cresoxy free radicals.

A secondary mechanism involving reactions of benzaldehyde, benzyl hydroperoxyde, cresol, benzylalcohol, ethylbenzene, styrene and bibenzyl [14].

Due to the strong electronic delocalization of benzyl radicals, the following co-oxidation reactions with alkyls are considered for the oxidation of toluene [25]:

• Metathesis of benzyl radicals with n-heptane yielding toluene and heptyl radicals.

• Terminations between benzyl and heptyl radicals.

• Metathesis of secondary allylic radicals with toluene.

• Reactions between toluene and alkylperoxy radicals.

Mechanism of nitrogen containing species

Reactions of nitrogen containing compounds were taken from a previous modeling work on the conversion of NO to nitric dioxide (NO 2 ) promoted by methane, ethane, ethylene, propane, and propene [26]. The kinetic model was primarily based on the GRI-MECH-3.0 [27] and the research performed by Dean and Bozzelli [START_REF] Dean | Combustion Chemistry[END_REF] and Atkinson et al. [START_REF] Atkinson | [END_REF]. The thermochemical data proposed by Marinov [30] was used for nitrogen compounds. N-heptane-NO x reactions and rate constants were derived from a mechanism published by Glaude et al. [31] for the oxidation of n-butane and n-pentane in the presence of NO x . These include:

Reactions of alkylperoxy ROO• and hydroperoxy-alkylperoxy (HOOQOO•) radicals with NO leading to NO 2 and partially oxidized products. ROO• radicals react with NO forming NO 2 and alkoxy radicals RO•. Furthermore, the decomposition of RO• radicals was included. HOOQOO• radicals reacting with NO are decomposed by a global reaction to NO 2 , a hydroxyl radical, two formaldehyde molecules and the corresponding alkene.

Reactions of resonance stabilized allylic radicals with NO 2 yielding NO, acrolein and an alkyl radical.

Toluene-NO x reactions are also proposed within the framework of the present study. These include:

Conversion of benzyl with NO 2 generating alkoxybenzyl radicals with the same reaction-rate constants as defined for the reaction between methyl radicals and NO 2 [32].

Reactions of peroxybenzyl and peroxyphenyl radicals with NO yielding alkoxybenzyl and phenoxy radicals with the same reaction-rate constants as defined for alkylperoxy radicals [31].

Reactions of alkoxybenzyl radicals with NO and NO 2 yielding benzaldehyde and benzoyl radicals, with the same rate reaction-constants as the corresponding reactions of methoxy radicals [27], [33].

Reaction of benzaldehyde with NO producing benzoyl radicals and HNO. Reaction-rate constants have been defined similar to the analogous reaction of formaldehyde and NO [34].

DISCUSSION

Figure 1 shows that the proposed mechanism successfully predicts the consumption of the fuel and oxygen and the formation of products without any additive. Figure 2 compares the measured concentration profiles of n-heptane, ethylene and methanol with the profiles calculated using n-heptane models generated by the standard EA-version and by the modified EA-version. The changes made in the secondary mechanism for the oxidation of n-heptane allowed a significant improvement in the reproduction of species concentration profiles. Despite an overestimation of n-heptane consumption below 800K (Fig. 2a), the amplitude of the reduction of fuel conversion in the NTC-region is better predicted by the modified EA-version. In addition, the calculated ethylene concentration profile (Fig. 2b) is closer to the experimental observations and the methanol concentration peak around 650K is more accurately reproduced.

FIGURE 2

The following section first discusses the comparison between experimental and simulated results in the presence of NO, ethylene and methanol (Fig. 1) and analyzes the reactions leading to the observed effects. The model is further used for predicting the impact of the addition of formaldehyde, ethane and CO on the fuel oxidation (Fig. 3).

Kinetic study of the influence of the addition of NO, ethylene and methanol

Addition of NO

Figures 1a, 1b and 1c show that the complex impact of NO on the consumption of reactants is accurately predicted throughout the whole considered temperature range. The slight retarding effect of NO which is observed below 700K is mainly caused by reactions (1) of alkylperoxy radicals (ROO•) with NO to give alkoxy radicals:

ROO•+NO=RO•+NO 2 (1)
These reactions compete with the isomerization of ROO• radicals followed by a second addition of oxygen yielding branching agents (hydroperoxides). The NO promoting effect observed above 700K is due to the reaction (2) between NO and •OOH radicals, transforming these rather unreactive radicals into •OH radicals. The following catalytic cycle can be written, with reaction (2)

consuming NO and reactions (3-5) regenerating it:

NO+•OOH=NO 2 +•OH (2) NO 2 +•H=NO+•OH (3) NO 2 +•CH 3 =NO+CH 3 O• (4) NO 2 +•C 2 H 5 =NO+C 2 H 5 O• (5)
The effect of this cycle is to noticeably reduce the concentration of •OOH radicals and to increase that of •OH radicals.

Figures 1d to 1k

show that the effects of NO addition on the formation of the main products are correctly reproduced. In the main, these effects are:

The important reduction in the formation of ethylene above 800K (Fig. 1d) which is caused by reaction (5) becoming competitive with reaction (6), which is the main ethylene formation channel:

•C 2 H 5 +O 2 =•OOH+C 2 H 4 (6)
The decrease in the formation of methanol around 650K (Fig. 1e) due to the NO consumption of methylperoxy radicals by reaction (7), which are the main source of methanol via reaction (8):

CH 3 OO•+NO=CH 3 O•+NO 2 (7) ROO•+CH 3 OO•=RCHO+CH 3 OH+O 2 (8)
The lower production of ethane (Fig. 1f) which is caused by reaction (4) consuming •CH 3 radicals and thus reducing the formation of ethane, obtained via reaction (9):

CH 3 •+CH 3 •=C 2 H 6 (9)
The complex impact on the formation of formaldehyde above 700K (Fig. 1g). As reactions ( 4) and ( 5) favour the formation of formaldehyde by an enhanced production of CH 3 O• and C 2 H 5 O• radicals, the production of aldehydes increases due to the rapid decomposition of these radicals. This effect, enhanced by the increased global reactivity, explains the higher concentration of formaldehyde between 750 and 850K resulting from the addition of NO. At higher temperatures, the increased formation of •OH radicals promotes the consumption of formaldehyde and explains its lower concentration in presence of NO.

The effects of NO on the concentrations of CO (Fig. 1h), H 2 (Fig. 1i), H 2 O (Fig. 1j) and CO 2 (Fig. 1k). The enhanced global reactivity induced by NO at temperatures above 650K results in an increased formation of CO and H 2 . However, above 900K, the production of •OH radicals by reactions (2) and (3) becomes important and induces a larger consumption of CO thus producing a larger concentration of CO 2 . As •OH radicals are consumed by formaldehyde producing •CHO radicals and H 2 O, the production of water also increases. As the main source of H 2 is the H-abstractions by H-atoms from aldehydes, an increase of •OH production results in a H 2 concentration drop off (>900K) due to the competition between reactions (10) and (11):

HCHO+•H=•CHO+H 2 (10)
HCHO+•OH=•CHO+H 2 O (11)
The favoured formation of CO 2 and water comes along with the increased consumption of oxygen above 900K when NO is added. For temperatures up to 1000K the production of ethylene, which is an important intermediate product of hydrocarbons oxidation, exceeds its consumption (Fig. 1d). Only at higher temperatures the ethylene consumption is so strong that its concentration becomes quasi-independent of the initially added amount of ethylene.

Addition of ethylene and methanol

At temperatures around 600K, the methanol concentration exceeds the amount of introduced methanol (Fig. 1e). The observed concentration peak corresponds to the amount of methanol which is produced via reaction (8). At higher temperatures (>700K), the consumption of methanol exceeds its production and thus its concentration profile corresponds to that observed for the oxidation of n-heptane and toluene which is characterized by a NTC-zone between 700 and 800K. The presence of ethylene and methanol enhances the formation of formaldehyde through the depletion of •C 2 H 3,

•CH 2 OH and •CH 3 O radicals.

Study of the effect of the addition of ethane, formaldehyde and CO

The good agreement between experimental and modeling results justifies using the model for predicting the impact of various organic additives on the fuel oxidation. Ethane, formaldehyde and CO are known to be present in EGR and may influence the HCCI-engine control. The model was then used to study the chemical impact of these species on the fuel oxidation.

FIGURE 4

Figure 3a compares the impact of various amounts of formaldehyde on the oxidation of n-heptane.

The simulations show that the addition of formaldehyde has a retarding effect on the n-heptane oxidation at low temperatures (<800K) but that it also increases the NTC-amplitude. At high concentrations of added formaldehyde (1600ppmv), the resulting retarding effect becomes so strong that up to 750K no reactivity of the mixture is predicted. Formaldehyde is consumed by the attack of •OH radicals via reaction (12), while the •CHO radicals react themselves by reaction (13):

HCHO+•OH=•CHO+H 2 O (12) •CHO+O 2 =CO+•OOH (13)
The sum of reactions ( 12) and ( 13) results in a net transformation of the reactive •OH into the less reactive •OOH radicals thus explaining the increased NTC-amplitude and the lack of reactivity at temperatures below 800K for high concentrations of added formaldehyde.

Figure 3b shows the impact of various amounts of ethane on the oxidation of n-heptane. The addition of ethane yields an inhibition at low temperatures, but also leads to a slight increase of the NTC-amplitude, which is less apparent than when formaldehyde is added. This amplification caused by ethane can be explained by the formation of ethyl radicals yielding an increased production of •OOH radicals via reaction [START_REF] Dubreuil | [END_REF].

Figure 3c compares the impact of various amounts of CO on the oxidation of n-heptane. The addition of CO slightly inhibits the n-heptane oxidation at low temperatures due to the consumption of •OH radicals via reaction ( 14), whereas at higher temperatures, the CO addition accelerates the consumption of n-heptane and the NTC-amplitude decreases via the •OH producing reaction (15):

CO+•OH=CO 2 +•H (14) CO+•OOH=CO 2 +•OH (15)
These observations are in agreement with the analysis performed by Subramanian et. al. [4] on the impact of CO on ignition delay times.

CONCLUSION

Our study points out the influence of EGR compounds on the fuel oxidation in HCCI-engine applications. The experimental results and the developed kinetic model contribute to a deeper understanding of complex chemical impacts of EGR on the fuel oxidation control. Further work are planned by our group to also assess these effects on autoignition.

It confirms the observations made by Dubreuil [START_REF] Dubreuil | [END_REF] and Moréac [7], who have emphasized the importance of the impact of NO on the oxidation of hydrocarbons. Generally, the presence of NO lowers the overall fuel reactivity at low temperatures and increases it at higher temperatures.

Therefore, the content of recycled NO might impact strongly the ignition delay in an HCCI-engine.

The addition of NO reduces considerably the formation of ethylene, ethane, CO and H 2 above 900K and promotes those of CO and H 2 O. Ethylene and methanol were experimentally and theoretically found to have little impact on the oxidation of n-heptane/toluene mixtures, even if a slight retarding effect on the fuel oxidation is observed at low temperatures. In contrast, a strong increase in the NTC-amplitude is predicted for the addition of formaldehyde. At high concentrations and at temperatures below 750K, its presence can completely inhibit the fuel oxidation. It was further shown that CO influences the oxidation kinetics of hydrocarbons and that therefore the impact of CO on HCCI-engine control might not only be limited to a diluting effect. Further experimental investigation is necessary since CO is among the main components of HCCI-engine EGR.

FIGURES

Figure 1:

a) b) c) d) e) f) g) h) i) j) k)

  the same molecular formula and the same functional groups, are lumped into one unique species without distinction between the different isomers. It includes global reactions producing, in the smallest number of steps, molecules or radicals whose reactions are included in the C 0 -C 2 base.These reactions produce C 1 -C 2 species in large amounts. The standard EA[13] mechanisms tend to over-predict ethylene concentrations at low temperatures. Since the modeling of ethylene concentrations is of major importance for this study, the ethylene producing reactions, defined in the secondary mechanism, were improved. The applied modifications concern the decompositions of hydroperoxides and cyclic ethers, as well as the H-abstractions by •O•, hydroxy (•OH), •OOH and methyl radicals (•CH 3 ) from olefins. This promotes the formation of larger alkyl or alkenyl radicals, instead of producing small C 0 -C 2 -radicals in one step reaction.

Figures 1a and 1b

  Figures 1a and 1b show that the addition of ethylene and methanol results in a reduced global

Figure 2

 2 Figure 2:

Figure 1 :

 1 Figure 1: Experimental (symbols) and simulated (lines) mole fractions of (a) n-heptane, (b)

Figure 2 :

 2 Figure 2: Experimental (symbols) and simulated (lines) mole fractions of (a) n-heptane, (b)

Figure 3 :

 3 Figure 3: Simulated mole fractions of n-heptane with (a) formaldehyde-additive, (b)

LIST OF SUPPLEMENTAL MATERIAL :

1 supplemental file: KINETIC-MECHANISM.S1.txt

CAPTION FOR SUPPLEMENTAL MATERIAL :

Kinetic reaction mechanism for the oxidation of n-heptane-toluene blends, valid for the addition of C 1 -C 2 carbon species and NO written in the CHEMKIN format.


Truong-Thanh Ma
email: truongthanh1511@gmail.com

Salem Benferhat
email: benferhat@cril.fr

Zied Bouraoui
email: bouraoui@cril.fr

Karim Tabia
email: tabia@cril.fr

Thanh-Nghi Do

Nguyen-Khang Pham

An Automatic Extraction Tool for Ethnic Vietnamese Thai Dances Concepts (Preprint version)

Keywords: Vietnamese Traditional Dance, Prioritized Ontology, machine learning, Ethnic Vietnamese Thai Dance

In recent year, preservation and promotion of the ICHs are one of the problems of interest. In this paper, we focus on modelling the traditional dance domain, particularly modelling traditional Vietnamese dances. To conserve significant characteristics of dances, we proposed an ontology to represent the significant movements features of Ethnic Vietnamese Thai Dances (EVTDs). Particularly, a detailed description of the movement schemas of EVTDs is presented in this paper. Additionally, we present how to build an automatic extraction tool to collect the fundamental movements data of EVTDs using machine learning. Finally, we represented explicitly how to store those extracted features from raw dance videos into prioritized Ontology-based proposed.

I. INTRODUCTION

Preservation and promotion of the intangible cultural heritage (ICH) are one of the problems of interest in the world. Therefore, many scientists in computer science domain applying the theoretical and practical knowledge to the field of Intangible Cultural Heritage, particularly in this paper focusing on Southeast Asia countries, because Southeast Asia region is one of the most dynamic regions in the world with a rich cultural heritage. We concentrated primarily on the Vietnam's traditional dances.

Vietnam is a multi-ethnic country existing many different cultures [START_REF] Canh | Đại cương nghệ thuật múa[END_REF] with fifty-four-ethnic groups living in a territory. The traditional dances had became "spiritual foods" of each Vietnamese people, it influences directly the real life from urban to rural. Most of the traditional Vietnamese dance (TVD) is transfered by "word of mouth" [START_REF] Loc | Mua dan gian cac dan toc Viet Nam[END_REF], the present generation would instruct fundamental movements to the adjacent generation. Additionally, traditional Vietnamese Dances are a steady bridge in educating about human dignity, morality and even historical knowledge. Instead of learning the historical lesson in regular classes as well as participating in the training the course of life skills, the dances has became the digital channel for efficiently educating personality, knowledge and even ethnicity to the generations.

Almost Vietnamese traditional dances built up from the ethnic groups culture, life environments and regions, it con-tains the large number of the significant characteristics of region-zone. Particularly, the dance movements of the ethnic groups originated from the life activities, each posture is depicted an characteristic action of their life. Therefore, the fundamental movements would be one of the stable foundation as well as being the essential features to determine the different dances. In this paper, we selected a remarkable dance of Thai community in Vietnam to illustrate how to represent the important features. The movements of EVTDs are the combination of fundamental postures presented in [START_REF] Son | Mua dan gian mot so dan toc vung Tay Bac[END_REF].

Classifying, detecting, identifying and storing dance videos is a great challenge because most of the Vietnamese dances are stored in raw videos. Therefore, we proposed a methodology to manage the heterogeneous data of EVTDs in order to search, store and query-answer dance videos.

One of the main contributions of this paper is to build an automatic extraction tool using machine learning in order to store the significant features of ethnic Vietnamese Thai dance movements (EVTDMs). These characteristics are put into a lightweight prioritized ontology-based (LPO) attached to recognized probabilistic of each body part in the same frame. Based on the probabilistic of each posture to decide whether the tool put those features into LPO or not.

In the research process, we decomposed our approach into two main stages: the first aspect is to reconstruct a schema of panorama overview of traditional Vietnamese dances; the second aspect concerns a character with the fundamental movements of each EVTD. In this paper, we concentrate primarily on the second stages with respect to detecting, extracting and storing automatically the fundamental movements. Our primary challenge is to determine the principle concepts from EVTD's movements combined with a set of desirable properties to build a useful dance search engine, moreover, because the movements of the performers is quite uncertain and inconsistent regarding the different cases (amateur, speed of music, etc.) as well as the sequential frame of videos is not explicit to recognize those extract movements, our remarkable aim is how to handle the uncertainties and inconsistencies in processing.

The remainder of this paper is structured as follows. In the next section (section 2) we give recent related works. Section 3 provides a description of EVTD's features and how to encode them into Ontology. How to detect automatically concepts and a methodology to build a LPO are discussed in section 4. Finally, section 5 concludes the paper.

II. RELATED WORKS

During the last two decades, people have tried to develop different algorithms for human activity analysis [START_REF] Aggarwal | Human activity analysis: Areview[END_REF][20] for wide applications in the area of surveillance, patient monitoring and many more. Most of the works have been reported on classifying human activity from videos. Recently researchers are trying to classify an activity from a single image [START_REF] Yang | Recognizing human actions from still images with latent poses[END_REF] [27] [START_REF] Yao | Classifying actions and measuring action similarity by modeling the mutual context of objects and human poses[END_REF]. In the video based activity recognition, people have tried with different human activities like walking, jogging, running, boxing, hand waving, hand clapping, pointing, digging and carrying for a single actor [24][4].

Furthermore, with the rapid development of computer science, the large number of applications of management of large and heterogeneous data is built and explored. In the dance domain, several authors using ontology to manage the dance databases, evidences as BalOnSe application [START_REF] El Raheb | Ballet Ontology for Annotating and Searching Video performances[END_REF], a Labanotation based ontology [START_REF] Raheb | A Labanotation based Ontology for Representing Dance Movement[END_REF]. Moreover, there are a few works on group activities as [16][12]. Due to the increase in multimedia data access through the internet, multimedia data specially video data indexing becomes more and more important. Not only in the retrieval but also for digitization of cultural heritage, this can be an interesting problem. It can be used to analyze a particular dance language. Some researchers use space time features to classify the human action. Blank et al. represent the human action as three dimensional shapes included by the silhouettes in the space-time volume [START_REF] Blank | Actions as space-time shapes[END_REF]. They use space-time features such as local space-time saliency, action dynamics, shape structure and orientation to classify the action. In [START_REF] Seo | Action recognition from one exam-ple[END_REF], they recognise human action based on space-time locally adaptive regression kernels and the matrix cosine similarity measure. Klaser et al. localize the action in each frame by obtaining generic spatio temporal human tracks [START_REF] Klaser | Hu-man focused action localization in video[END_REF]. They have used sliding window classifier to detect specific human actions.

There are several attempts to recognize the movement from multiple videos sources [START_REF] Seo | Action recognition from one exam-ple[END_REF] [START_REF] Aggarwal | Human activity analysis: Areview[END_REF]. Aggarwal et al. [START_REF] Aggarwal | Human activity analysis: Areview[END_REF] classify the human activity recognition in two classes namely, singlelayered approach and hierarchical approach. In single layer approach, activities are recognized directly from videos, while in hierarchical approach, an action is divided into sub-actions [START_REF] Gupta | Understand-ing videos, constructing plots: Learning a visually groundedstoryline model from annotated videos[END_REF]. The action is represented by classifying it into subactions. Wang et al. [START_REF] Wang | Human action recognition by semi-latent topic models[END_REF] have used topic model to model the human activity. They represent a video by Bag-of-Wards representation. Later, they have used a model which is popular in object recognition community, called Hidden Conditional Random Field (HCRF) [START_REF] Wang | Hidden part models for human ac-tion recognition: Probabilistic vs. max-margin[END_REF].

III. ETHNIC VIETNAMESE TRADITIONAL DANCES

A. Ethnic Vietnamese Thai Dances

Thai community in Vietnam is one of the ethnic groups existing the large number of the traditional dances. There are many significant festivals of Thai ethnic group to be held in villages as well as regions during the whole year. In order to understand explicitly with respect to EVTDs, in this section, we present several fundamental movement features to identify the EVTDs in the Vietnam's territory.

In each EVTD, the remarkable characteristics to determine EVTDs is the fundamental movements, in which is the foundation of the creative combination in each motion in order to create the specific dances of Vietnamese Thai people. Correspondingly, the detection of the basis movements is one of the important steps collected automatically the dance dataset for LPO. The following we would present a basis movements schema of EVTDs as well as represent EVTD's LPO based on the schema proposed. Basis movements of EVTDs are divided in five characteristics [START_REF] Son | Mua dan gian mot so dan toc vung Tay Bac[END_REF]: Orientation, Arm Posture, Leg Posture, Sitting Posture, Standing Posture as figure 1. They are described in detail as follows:

B. Encoding EVTD Movements into Prioritized Ontology

This section proposes implementing a modelling of EVTD using lightweight ontology by DL-Lite. One of the main advantage of DL-Lite is that query-answering is down in an efficient way. Realizing the significance of DL-Lite in representing ontology-based model as well as perceiving further what is the motivation behind using DL-Lite in order to build an application (semantic Web) for EVTDs through OWL2-QL language, therefore, we proposed to select DL-Lite to represent implementing ontology-based modelling of EVTDs in this paper.

1) Presentation of DL/DL-Lite: Description Logics (DLs) provide the formal foundation for ontologies, and the tasks related to the use of ontologies in various application domains are posing new and challenging requirements with respect to the trade-off between the expressive pover of a DL and the efficiency of reasoning over knowledge bases (KBs) expressed in the DL. Description Logics [?] are also the logical frameworks underlying the ontology language. A description logic knowledge base is formed by a terminological base, called TBox, and an assertional base, called ABox. The TBox contains inclusion axiom concepts and rules regarding knowledge of the application domain whereas the ABox stores data (individuals and constants) DL-Lite is a family of tractable DLs specifically altered for applications that utilize the huge number of data, for which query answering is the significant reason assignment.

2) DL-Lite syntax: Let [?] N C , N R and N I be three pairwise disjoint sets of atomic concepts, atomic roles and individuals respectively. Let A ∈ N C , P ∈ N R , three connectors ¬ , ∃ ,are used to define complex concepts and roles. We only present DL -Lite core the core fragment of all the DL-Lite family and we would utilize DL-Lite R instead of DL-Lite core . Nevertheless, we concentrate on two important members of the DL -Lite family in this paper, including DL-Lite R . Considering basic concepts (resp. roles) B (resp. R), complex concepts (resp. roles) C (resp. E) are defined in DL-Lite as follows:

B → A | ∃ R C → B | ¬B B → A | P - E → R | ¬R
where P -represents the inverse of P and A is an atomic concept, P is an atomic role.

A DL-Lite knowledge base (KB) is a pair K = T , A where T is the TBox and A is the ABox. The TBox T includes a finite set of inclusion axioms on concepts and on roles respectively of the form: B C and R E. The ABox contains a finite set of assertions (facts) of the form A(a) and P(a,b) where A ∈ N C , P ∈ N R and a, b ∈ N I .

3) Implementing EVTD movements ontology using DL-Lite: We built a prioritized ontology of EVTD movements based on the schema proposed as figure 1. We present how to encode EVTD movements into LPO using DL-Lite, as follows:

TBox: T EV T D The explanation of (1) that the accuracy of ArmPosture-3 is 67% in Frame 10. At the same frame 10, left shoulder with orientation-1 obtained 94% of accuracies represented in (4) and so on. Our primary aim is to store each motion of each body part of performer/dancer in the same frame into prioritized ontology-based where collect the dance movement dataset to serve for searching, reasoning and query-answering.

The reason why we built prioritized ontology because a dance video is sequential frames where we are difficult to determine explicitly how dance postures and movements are right. Therefore, the probability and accuracy of each motion based on machine learning algorithms is quite expected. Example: considering a dance video from frame 1 to frame 100, just exiting frame 20 satisfied the essential requirements of those motions. Based on the accuracies classified of machine learning which we identified whether the features are set into LPO or not (above 80% to be selected).

IV. ON THE AUTOMATIC DETECTION OF CONCEPTS

In order to detect the concepts automatically, we had utilized TF-Openpose to identify skeletons of performers. We also aggregated Deep Convolutional Neural Networks to recognize primary postures in each frame. The principle purpose of the automatic detection is to enrich the ontology by assertions representing concepts of LPO presented in each frame. In this section, a description of how to detect automatically significant features through machine learning will be discussed, particularly using human pose estimation and DCNN architectures to build a detection tool.

A. Human Pose Estimation

We utilize TF-Openpose (written in python using Tensorflow library instead of Caffe library) for estimating the positions of human joints and articulated pose estimation in order to support for depicting each movements in EVTD. Moreover, we ameliorated and improved TF-Openpose through algorithms of input image processing and modified several essential arguments of CNNs.

The primary purpose of using HPE for EVTD movements is to determine concretely parts of body in raw dance videos to aim at extracted and represent the motions in each dance movement. The architecture simultaneously predicts detection confidence maps and affinity fields that encode part-to-part association as in Figure5. The network is split into two branches: Branch 1 is responsible for predicting confidence maps, and Branch 2 is to predict the affinity fields. TF-Openpose takes a 2D color image as input and produces the 2D location of anatomical key-points for each person. The (x,y) coordinates of the final pose data array could be normalized to the range depending on the key-point scale. It can be estimated 18 key-point body pose from COCO 2016 dataset. Realizing the requirements of a high configuration regarding GPU for Openpose handled, we proposed to utilize TF-Openpose1 instead of orginal Openpose version. It is a human pose estimation library developed based upon the foundation of the Openpose library using Tensorflow and OpenCV. It also provides several variants that have made the changes to the network structure for real-time processing on the CPU or lowpower embedded devices. We concentrated on two variations of models to find optimized network architecture: CMU [START_REF] Cao | Realtime Multi-Person 2D Pose Estimation using Part Affinity Fields[END_REF] and Mobile-Net [START_REF] Howard | MobileNets: Efficient Convolutional Neural Networks for Mobile Vision Applications[END_REF]. ( 1) With respect to CMU, it is the model based VGG pre-trained network which described in the Openpose's original paper using COCO dataset for training, it is converted from Caffe format to utilize in Tensorflow; [START_REF] Seo | Action recognition from one exam-ple[END_REF] Based on the Mobile-Net paper [START_REF] Howard | MobileNets: Efficient Convolutional Neural Networks for Mobile Vision Applications[END_REF], with 12 convolutional layers are used as feature-extraction layers. The experimental result as in figure 6.

B. Using Deep Convolutional Neural Networks

In order to detect and recognize the significant postures (particularly in Leg, Standing and Sitting Posture), we proposed to utilize deep convolutional neural networks (DCNNs) which have been applied to visual tasks since the late 1980s.

As we had known, there are three main types of layers used to build Deep CNN architectures: convolutional layer, pooling layer and fully connected layer. Most of the CNN architectures is obtained by stacking the number of these layers. Deep convolutional neural networks, trained on large datasets, achieve convincing results and are currently the stateof-the-art approach for this task illustrated in figure7. 9). Realizing that each CNN architecture deals with the different cases of the particular dataset as well as combining the features to represent a vector is quite expected because it will be boosted strongly the discrimination between the classifications. In addition, the dataset of ETVDs focus principally on the high resolution image frames of dance videos, specially, the resolution and size of images will be grown rapidly in the future. For these reasons, we selected the methodology using deep CNNs to extract the significant features and ML algorithms to classify. After having sets of the collected images, we used several algorithms to advance the quality of images (image pre-processing). In each image frame, we extracted the features from three CNN architectures, particularlly, including Xceptions [START_REF] Chollet | Xception: Deep learning with depthwise separable convolutions[END_REF] (2048 features), InceptionV3 [START_REF] Xia | Inception-v3 Flower Classification, 2017 2nd International Conference on Image, Vision and Computing[END_REF] (2048 features), Mobilenet [START_REF] Howard | MobileNets: Efficient Convolutional Neural Networks for Mobile Vision Applications[END_REF] (1024 features). The next step, we aggregated consequently (respectively) the extracted features to have a feature vector with 5120 dimensions. After that, the comparison among several ML algorithms to have a best selection for classification is fully essential presented in section V.

The main idea of this model is a classification tool to update flexibly the novel architectures which will be published in the future aimed at advancing the accuracy in classification as soon as the dataset accelerated. In addition, we are also able to extract the features in parallel with each CNN architecture, nevertheless, we do not experiment the parallel models in this paper.

C. An automatic detection tool

In order to store and to detect the fundamental features into LPO, we implemented an automatic extraction tool of EVTD's movements (poses) by python language illustrated in figure 12. We utilized DCNN's architecture models proposed to classify the postures (leg, sitting and standing postures). Additionally, we also used HPE to describe each body parts of performer/dancer. Furthermore, we selected Owlready2 library (using python language) with HermiT reasoner to build our lightweight prioritized ontology. Our tool allowing users is able to extract automatically or extract manually (in each frame) features to put into ontology. As presented in above sections, each feature we inserted the probability of each movements to serve for selecting the suitable features in many sequential frames.

On the other hand, because the contrast between light and shade is different as well as the resolution of each video is also distinct, our tool implemented a simple adjustable set of image processing manually to support detection and classification. In order to be compatible for extracting the features of EVTDs where existing many fundamental movements separately. We also designed a simple function to change flexibly the classes/concepts for storing easily the different movements. In the next section, we will present experimental results and how to represent the extracted features into LPO with the probability. We implemented the propositional tool on the computer supporting graphical card (NVIDIA GeForce GTX 950M with total memory is 8107 MB) to run TensorFlow on multiple GPUs. In this section, we would present two parts: (1) the experimental result of classifying the postures, (2) presenting LPO implemented and how to put the features into LPO by the tool implemented.

A. Classification of significant postures

We used python programming language and Keras libary to implement the EVTD postures automatic detection framework on each frame. We randomly split the dataset into two different training(2/3) and test (1/3) sets (with the posture image datasets collected as in Table I, collected from 15 videos). In addition, we also implemented scikit-learn library 3 to use several ML algorithms including logic regression, Support vector machine (SVM -C=10000, Gama=0.002), Random Forest (200 decision trees), Stochastic Gradient Descent classifier (SGD), K-Nearest Neighbors (KNN -K=5), Naïve Bayes classifier. The experimental results of the propositional CNN model are in Table II for Rank-1 accuracy). The result achieved the high accuracy (F1) using Logic Regression as follows: 98.88% of Leg postures (for 06 classes), 99.84% of Sitting Posture (for 03 classes), 99.37% of Standing Posture (for 04 classes). In general, most of the classification results achieved the high accuracy around above 90%.

The result of this classification will be one of the preliminary of dataset collected. In implementation process, we realized that this collected dataset is not able to represent and reflect most of the different angle in dance. It exists some difficulties in classification including the difference between the postures of a professional dancer and an amateur person as well as the distinction from the distinct directions to look. Therefore, the necessary to collect a huge dataset is absolute expected in the future.

B. Implementation of EVTD's Lightweight Prioritized Ontology-based

Our LPO has 105 classes, 09 object properties, 09 data properties, 321 individuals and 2322 axiom including orientations, postures and body parts. It is implemented by owlready2 library 4 , to store fundamental features (including the possibility of each movements characteristics). In this subsection, we present how to manage significant features of EVTD postures into LPO. We proposed two methodologies to structure prioritized ABox as follows:(1) storing each significant feature with the specific probability as the left side of figure 12 (from 0% to 100%), (2) storing each essential characteristic with the probability range as right side of 12 that be classify including the levels: High (80%-100%), Above Average (60%-80%), Average (40%-60%), Below Average (20%-40%), Low (0%-20%) illustrated as top part of figure12.

In order to represent body parts, we implemented TF-Openpose to detect skeleton. From each body part extracted, we classified into eight orientations (O i (i=1..8)) as in Figure 13. From each image flat and each body part, we identified the angle between x-axis with the body part orientation to classify, for example right-shoulder has the 93-degree angle, being O 5 . In this demonstration, we only experimented with one dancer to represent and to store movements of EVTDs. Regarding the case of postures that did not belongs to the fundamental knowledge in [START_REF] Son | Mua dan gian mot so dan toc vung Tay Bac[END_REF], "non-posture" classification is utilized to represent. As discussed above, based on the probability of postures and poses that we will decide the selection of the essential frame to store into ontology.

VI. CONCLUSION AND FUTURE WORKS

With the aim of the preservation and promotion in the intangible cultural heritage in general as well as developing an application to store the Vietnamese traditional dances. In particular, we presented a methodology to identify automatically the significant concepts of EVTDs to build an intelligent repository. Using the machine learning algorithms combines with the CNN architectures and HPE to detect the important features are discussed in this paper. On the basis of the propositional tool, we collected and managed the heterogeneous dance data of EVTDs (from raw videos with low revolution).

The work presented in this paper is one of the important first steps regarding preserving and promotion of EVTDs based on the background of artificial intelligent. These initial steps would be the foundation for creating universal traditional dance repository to aim to support for advanced heterogeneous digital storage, indexing, classification, reasoning and searching dance videos. Based on the concepts extracted automatically and stored into prioritized ABox, the next step will classify, annotate and query-answering the dance videos of EVTDs. Our next plans include the collection of the dance dataset, improve how to detect the fundamental movements which is more compatible and build an universal lightweight ontologybased for EVTDs.

Figure 1 :

 1 Figure 1: A taxonomic Hierarchy of EVTDs

Figure 2 :Figure 3 :

 23 Figure 2: Orientations of EVTDs

Figure 4 :

 4 Figure 4: Sitting postures and standing postures of EVTDs

For

  each raw video, we represented each feature in each frame, particularly, for an example of Frame10 presented in ABox as follows: ABox: T EV T D ... hasConf idence(V N -Orientation -1 -94, 94) hasOrientation(RightShoulder, V N -Orientation -1 -94) hasOrientation(Lef tShoulder, V N -Orientation -2 -74) ... 1. hasArmP osture(F rame10, V N -T hai-ArmP osture-3-67) 2. hasLegP osture(F rame10, V N -T hai -LegP osture -1 -89) 3. hasP ose(F rame10, RightShoulder -Orientation -5 -73) 4. hasP ose(F rame10, Lef tShoulder -Orientation -1 -94) 5. hasP ose(F rame10, Lef tHip -Orientation -1 -55) 6. hasP ose(F rame10, RightHip -Orientation -6 -34) ...

Figure 5 :

 5 Figure 5: The architecture using CNN in Openpose

Figure 6 :

 6 Figure 6: Using HPE and DCNN to detect the basis features

Figure 7 :

 7 Figure 7: Neural network with many convolutional layers

Figure 8 :Figure 9 :

 89 Figure 8: Framework to detect automatically dance postures

Figure 10 :

 10 Figure 10: An automatic extraction tool of EVTDs

Figure 11 :

 11 Figure 11: An Ontology-based Modelling of EVTDs

Figure 12 :Figure 13 :

 1213 Figure 12: Range of Probability

Table I :

 I Datasets of the fundamental posture of EVTDs

				Postures (Pos)
		P1	P2	P3	P4	P5	Pos None	Total
	Leg Postures	1260	685	1185	494	673	1407	5704
	Sitting Posture	1252	798	none	none	none	2163	4213
	Standing Posture	none	685	none	494	673	2084	3936
			V. EXPERIMENTAL RESULT

Table II :

 II Comparisons of Rank-1 accuracy of algorithms

	Algorithm	Leg Posture	Postures Sitting Posture	Standing Posture
	Logic Regression	98,88	99.84	99,37
	SVM (Linear)	98,84	99.80	99,27
	SGD Classifier	92,18	94,23	93,78
	Random Forest	96,47	97,63	98,02
	K-Nearest Neighbors	94,11	96,15	95,07
	Naïve Bayes	96,30	97,06	97,34

https://github.com/ildoonet/tf-pose-estimation

https://keras.io/models/model/

http://scikit-learn.org/stable/

https://pypi.org/project/Owlready2/

VII. ACKNOWLEDGEMENTS This work has received support from the European Project H2020 Marie Sklodowska-Curie Actions (MSCA), Research and Innovation Staff Exchange (RISE): Aniage project (High Dimensional Heterogeneous Data based Animation Techniques for Southeast Asian Intangible Cultural Heritage Digital Content), project number 691215.