David Delfieu
email: david.delfieu@univ-nantes.fr

Maurice Comlan
email: comlan@hotmail.fr

Médésu Sogbohossou
email: sogbohossoumedesu@yahoo.fr

Algebraic Analysis of Branching Processes

Keywords: Petri Nets, Unfolding, Branching process, Algebra

Combinatory explosion is a limit which can be encountered when a state space exploration is driven on large specification modeled with Petri nets. Technics like unfolding have been proposed to cope with this problem. This paper presents an axiomatic model to reduce unfoldings to canonic forms which preserves conflicts.

I. INTRODUCTION

Petri nets are a widely used tool used to model critical real-time systems. The formal verification of properties is then based on the computation of state space [START_REF] Berthomieu | State class constructions for branching analysis of time petri nets[END_REF]. But, this computation faces generally, for highly concurrent and large systems, to combinatory explosion. A major cause is the semantics of interleaving. Partial order semantics [START_REF] Esparza | Unfoldings -a partial-order approach to model checking[END_REF] have been introduced to shunt those interleavings. This work, initiated in [START_REF] Delfieu | An algebra for branching processes[END_REF], go further with the introduction of the conflict equivalence. An operator which is an abstraction of sequence and true parallelism simplifies the representation of processes, only conflicts are preserved. This approach can be used to speed up the identification of the branching processes of an unfolding. The notion of equivalence can be used to make a new type of reduction of unfoldings.

Finite prefixes of net unfoldings constitute a first transformation of the initial Petri Net (PN), where cycles have been flattened. This computation produces a process set where conflicts act as a discriminating factor. A conflict partitions a process in branching processes. An unfolding can be transformed into a set of finite branching processes. Theses processes constitute a set of acyclic graphs -several graphs can be produced when the PN contains parallelism -built with events and conditions, and structured with two operators: causality and true parallelism. An interesting particularity of an unfolding is that in spite of the loss of the concept of global marking, these processes contain enough information to reconstitute the reachable markings of the original Petri nets. In most of the cases, unfoldings are larger than the original Petri net. This is provoked essentially when values of precondition places exceed the precondition of non simple conflicts. This produces a lot of alternative conditions. In spite of that, a step has been taken forward: cycles have been broken and the conflicts have structured the nets in branching processes.

A lot of works have been proposed to improve unfolding algorithms [START_REF] Esparza | Unfoldings -a partial-order approach to model checking[END_REF][4] [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] [START_REF] Mcmillan | Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits[END_REF]. Is there another way to draw on recent works about unfolding? In spite of the eventual increase of the size of the net unfoldings, the suppression of conflicts and loops has decreased its structural complexity, allowing to compute the state space and to the extract of semantics.

From a developer's point of view an unfolding can be efficiently coded by a boolean table of events. This table describes every pair to pair relation between events. This table has been the starting point of our reflection: it stresses the point that a new connector can be defined to express that a set of events belong to the same process. This connector allows to aggregate all the events of a branching process. For example, a theorem is proposed to compute all the branching processes, in canonic form, for chains of conflicts of the kind illustrated in Figure 1. The work presented in this paper takes place in the context of combining process algebra [START_REF] Hoare | Communicating sequential processes[END_REF][8] and Petri nets [START_REF] Petri | Communication with automata[END_REF]. The axiomatic model of Milner's process with Calculus of Communicating Systems (CCS) is compared with the branching processes and related to other works in Section II. Then, after a brief presentation of Petri nets and unfoldings in Section III, Section IV presents our contribution with the definition of an axiomatic framework and the description of properties. The last section presents examples, in particular, illustrating a conflict equivalence.

II. RELATED WORKS

Process algebra appeared with Milner [START_REF] Milner | Communication and concurrency[END_REF] on the Calculus of Communicating Systems (CCS) and the Communicating Sequential Processes (CSP) of Hoare [START_REF] Hoare | Communicating sequential processes[END_REF] in not equivalent but similar approaches. The algebra of branching process we propose in this paper is inspired by the process algebra of Milner. CCS is based on two central ideas: The notion of observability and the concept of synchronized communication; CCS is as an abstract code that corresponds to a real program whose primitives are reduced to simple send and receive on channels. The terms (or agents) are called processes with interaction capabilities that match requests communication channels. The elements of the alphabet are observable events and concurrent systems (processes) can be specified with the use of three operators: sequence, choice, and parallelism. A main axiom of CCS is the rejection of distributivity of the sequence upon the choice. Let p and q be two processes, the complete process of syntax is: Consider an observer. In the first automaton of the Figure 2, after the occurrence of the action a, he can observe either b or c. In the second automaton, the observation of a does not imply that b and c stay observable. The behavior of the two automata are not equivalent.

Capacity α := x | x | τ Proces p ::= α.p | p||q | p + q | D( x) | p\x | 0
In CCS, Milner defines the observational equivalence. Two automata are observational equivalent if there are bisimular. On a algebraic point of view, the distributivity of the sequence on the choice is rejected in the equation (1):

a.(b + c) ≡ behaviorally a.b + a.c (1)
The key point of our approach is based on the fact that this distributivity is not rejected in occurrence nets. The timing of the choices in a process is essential [START_REF] Glabbeek | Petri net models for algebraic theories of concurrency[END_REF]. The nodes of occurrence nets are events. An event is a fired transition of the underlying Petri net. In CCS, an observer observes possible futures. In occurrence nets, the observer observes arborescent past. This controversy in the theory of concurrency is an important topic of linear time versus branching time. In our model the equation (2) holds:

a ≺ (b ⊥ c) ≡ (a ≺ b) ⊥ (a ≺ c) (2)
The equation ( 2) is a basic axiom of our algebraic model. The equivalence relation differs then from bisimulation equivalence. This relation will be defined in the following with the definition of the canonic form of an unfolding.

Branching process does not fit with process algebra on numerous other aspects. For example, a difference can be noticed about parallelism. While unfolding keeps true parallelism, process algebra considers a parallelism of interleaving. Another difference is relative to events and conditions which are nodes of different nature in an unfolding. Conditions and events differ in term of ancestor. Every condition is produced by at most one event ancestor (none for the condition standing for m 0 , the initial marking), whereas every event may have 1 or n condition ancestor(s). In CCS, there is no distinction between conditions and events. Moreover, conditions will be consumed defining processes as set of events. However, a lot of works [START_REF] Mcmillan | Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits[END_REF][10] [START_REF] Best | The box algebra=petri nets+process expressions[END_REF] have shown the interest of an algebraic formalization: it allows the study of connectives, the compositionally and facilitates reasoning (tools like [START_REF] Felleisen | Semantics Engineering With PLT Redex[END_REF]). Let have two Petri nets; it is questionable whether they are equivalent. In principle, they are equivalent if they are executed strictly in the same manner. This is obviously a too restrictive view they may have the same capabilities of interaction without having the same internal implementations. These work resulted to find matches (rather flexible and not strict) between nets. Mention may be made among other the occurrence net equivalence [START_REF] Nielsen | Petri nets, event structures and domains[END_REF], the bisimulation equivalence [START_REF] Baeten | An operational semantics for process algebra[END_REF], the partial order equivalence [START_REF] Boudol | On the semantics of concurrency: partial orders and transitions systems[END_REF], or the ST-bisimulation equivalence [START_REF] Glaabeek | Petri nets for algebraic theories of concurrency[END_REF]. These different equivalences are based either on the isomorphism between the unfolding of nets or on observable actions or traces of the execution of Petri nets or other criteria. This approach in this paper is weaker than a trace equivalence; it does not preserves traces but preserves conflicts. The originality of this approach is to encapsulate causality and concurrency in a new operator which "aggregates" and "abstract" events in a process. This new operator reduces the representation and accelerates the reduction process. This paper intends first, to give an algebraic model to an unfolding, and second, to establish a canonic form leading to the definition of an equivalence conflict.

III. UNFOLDING A PETRI NET

A. Petri Net

A Petri net [START_REF] Petri | Communication with automata[END_REF] N =< P, T, W > is a triple with: P, a finite set of places, T , the finite set of transitions, P ∪ T are nodes of the net; (P ∩ T = / 0), and W : (P × T ) ∪ (T × P) -→ N , the flow relation defining arcs (and their valuations) between nodes of N .

The pre-set (resp. post-set) of a node x is denoted

• x = {y ∈ P ∪ T | W (y, x) > 0} (resp. x • = {y ∈ P ∪ T | W (x, y) > 0}). A marking of a Petri net N is a mapping m : P -→ N . A tran- sition t ∈ T is said enabled by m iff: ∀p ∈ • t, m(p) ≥ W (p,t). This is denoted: m t → Firing of t leads to the new marking m (m t → m ): ∀p ∈ P, m (p) = m(p) -W (p,t) + W (t, p). The initial marking is denoted m 0 . A Petri net is k-bounded iff ∀m, reachable from m 0 , m(p) ≤ k (with p ∈ P).
It is said safe when 1-bounded. Two transitions are in a structural conflict when they share at least one pre-set place; a conflict is effective when these transitions are both enabled by a same marking. The considered Petri nets in this paper are k-bounded.

B. Unfolding

In [START_REF] Engelfriet | Branching processes of petri nets[END_REF], the notion of branching process is defined as an initial part of a run of a Petri net respecting its partial order semantics and possibly including non deterministic choices (conflicts). This net is acyclic and the largest branching process of an initially marked Petri net is called the unfolding of this net. Resulting net from an unfolding is a labeled occurrence net, a Petri net whose places are called conditions (labeled with their corresponding place name in the original net) and transitions are called events (labeled with their corresponding transition name in the original net).

An occurrence net [START_REF] Chatain | Complete finite prefixes of symbolic unfoldings of safe time petri nets[END_REF] O =< B, E , F > is a 1-valued arcs Petri net, with B the set of conditions, E the set of events, and F the flow relation (1-valued arcs), such that:

| • b| ≤ 1 ( ∀b ∈ B), • e = / 0 (∀e ∈ E ), and F + (the transitive closure of F ) is a strict order relation. This net O is a set of acyclic graphs. Min(O) = {b | b ∈ B, | • b| = 0}
is the minimal conditions set: the set of conditions with no ancestor can be mapped with the initial marking of the underlying Petri net. Also,

Max(O) = {x | x ∈ B ∪ E , |x • | = 0} are maximal nodes.
Three kinds of relations could be defined between the nodes of O:

• The strict causality relation noted ≺: ∀x, y ∈ B ∪ E , x ≺ y if (x, y) ∈ F + • The conflict relation noted #: ∀b ∈ B, if e 1 , e 2 ∈ b • (e 1 = e 2 )
, then e 1 and e 2 are in conflict relation, denoted e 1 # e 2 (in Figure 3.b e 4 #e 5 ).

• The concurrency relation noted : ∀x, y ∈ B ∪ E (x = y), x y ssi ¬((x ≺ y) ∨ (y ≺ x) ∨ (x y)). (in Figure 3.b e 2 e 3 ).

F def =< O F , λ F > of a marked net < N , m 0 >, with O F def =< B F , E F , F F > an occur- rence net and λ F : B F ∪ E F → P ∪ T (such as λ (B F ) ⊆ P and λ (E F ) ⊆ T ) a
labeling function, is given by:

1) ∀p ∈ P, if m 0 (p) = / 0, then B p def = {b ∈ B F | λ F (b) = p ∧ • b = / 0} and m 0 (p) = |B p |; 2) ∀B t ⊆ B F such as B t is a cut, if ∃t ∈ T , λ F (B t ) = • t ∧ |B t | = | • t|, then: a) ∃!e ∈ E F such as • e = B t ∧ λ F (e) = t; b) if t • = / 0, then B t def = {b ∈ B F | • b = {e}} is as λ F (B t ) = t • ∧ |B t | = |t • |; c) if t • = / 0, then B t def = {b ∈ B F | • b = {e}} is as λ F (B t ) = / 0 ∧ |B t | = 1; 3) ∀B t ⊆ B F , if B t is not a cut , then e ∈ E F such as • e = B t .
The definition 3.2 represents an exhaustive unfolding algorithm of < N , m 0 >. In 1., the algorithm for the building of the unfolding starts with the creation of conditions corresponding to the initial marking of < N , m 0 > and in 2., news events are added one at a time together with their output conditions (taking into account sink transitions). In 3., the algorithm requires that any event is a possible action: there are no adding nodes to those created in item 1 and 2. The algorithm does not necessary terminate; it terminates if and only if the net < N , m 0 > does not have any infinite sequence. The sink transitions (ie t ∈ T ,t • = / 0) are taken into account in 2.(c).

Let be

E ⊂ E F . The occurrence net O def =< B, E , F > associated with E such as B def = {b ∈ B F | ∃e ∈ E , b ∈ • e ∪ e • } and F def = {(x, y) ∈ F F | x ∈ E ∨ y ∈ E } is a prefix of O F if Min(O) = Min(O F ). By extension, Un f def =< O, λ > (with λ , the restriction of λ F to B ∪ E ) is a prefix of unfolding Un f F .
It should be noted that, according to the implementation, the names (the elements in the sets E and B) given to nodes in the same unfolding can be different. A name can be independently chosen in an implementation using a tree formed by its causal predecessors and the name of the corresponding nodes in N [START_REF] Engelfriet | Branching processes of petri nets[END_REF]. is a labeling fonction such as: The conflits in a unfolding derive from the fact that there is an reachable marking (a cut in an unfolding) such as two or many transitions of a labelled net < N , m 0 > are enabled and the firing of one transition disable other. Whence the proposition:

Definition 3.3: A causal net C is an occurrence net C def =< B, E , F > such as: 1) ∀e ∈ E : e • = / 0 ∧ • e = / 0; 2) ∀b ∈ B : |b • | ≤ 1 ∧ | • b| ≤ 1. Definition 3.4: P i = (C i , λ F ) is a process of < N , m 0 > iff: C i def =< B i , E i , F i > is a causal net and λ : B i ∪ E i → P ∪ T
1) B i ⊆ B F and E i ⊆ E F 2) λ F (B i ) ⊆ P and λ F (E i ) ⊆ T ; 3) λ F ( • e) = • λ F (e) and λ F (e • ) = λ F (e) • 4) ∀e i ∈ E i , ∀p ∈ P : W (p, λ F (e)) = |λ -1 (p) ∩ • e| ∧ W (λ F (e), p) = |λ -1 (p) ∩ e • | 5) If p ∈ Min(P) ⇒ ∃b ∈ B i : • b = / 0 ∧ λ F (b) = p Max(C i ) is the state of N . Min(C i )
Proposition 3.5: Let be e 1 , e 2 ∈ E F . If e 1 ⊥ e 2 , then there ∃(e 1 , e 2 ) ∈ [e 1 ] × [e 2 ] such as • e 1 ∩ • e 2 = / 0 et • e 1 ∪ • e 2 is a cut.

IV. BRANCHING PROCESS ALGEBRA

The previous section showed how unfolding exhibits causal nets and conflicts. Otherwise, every couple of events which are not bounded by a causal relation or the same conflict set are in concurrency. Then, an unfolding allows to build a 2Dtable making explicit every binary relations between events. Practically, this table establishes the relations of causality and exclusion. If a binary relation is not explicit in the table, it means that the couple of events are in a concurrency relation.

Let E B = E ∪ B a finite alphabet, composed of the events and the conditions generated by the unfolding. The event table (produced by the unfolding) defines for every couple in E B either a causality relation C , either a concurrency relation I or an exclusive relation X . These sets of binary relations dot not intersect and the following expressions can be deduced:

Un f / X = C ∪ I (3) Un f / C = X ∪ I (4) Un f / I = C ∪ X (5)
To illustrate these relation sets, the negation operator noted ¬ can be introduced. Then, the equations ( 3),( 4),( 5) leads to ( 6),( 7), [START_REF] Milner | Communication and concurrency[END_REF]:

¬((e 1 , e 2 ) ∈ I ) ⇔ (e 1 , e 2 ) ∈ C ∪ X (6) ¬((e 1 , e 2 ) ∈ C ) ⇔ (e 1 , e 2 ) ∈ I ∪ X (7) ¬((e 1 , e 2 ) ∈ X ) ⇔ (e 1 , e 2 ) ∈ C ∪ I (8)
The equation [START_REF] Milner | Communication and concurrency[END_REF] expresses that if two events are not in conflict they are in the same branching process. Let us now define the union of binary relations C and I : P = C ∪ I For every couple (e 1 , e 2 ) ∈ P, either (e 1 , e 2 ) are in causality or in concurrency: P is the union of every branching process of an unfolding. a) Example: Let us consider an unfolding (left part) on the Figure 4 and the table T (right part) which is its representation: In Figure 4, the table T contains 7 causal relations and 4 conflict relations. (e 0 , e 4 ) is not (negation) in the table, expresses that e 0 and e 4 are concurrent. Moreover, if two events are not in conflict (consider e 0 and e 6 ): (e 0 , e 6 ) is not a key of the table, (e 0 , e 6 ) are in concurrency and thus, those events belongs to the same branching process.

A. Definition of the Algebra

The starting point of this work is based on the fact that the logical negation operator articulates the relation between two sets: the process set P, and the exclusion set X . As mentioned in Section IV, C , I and , P does not intersect, then semantically, if a couple of events is not in a relation of exclusion (noted ⊥), the events are in P. P contains binary relations between events that are in branching process.

To express that events are in the same branching process, a new operator noted ⊕ is introduced. An algebra describing branching process can be defined as follow: {U , ≺ , , ⊥ , ⊕, ¬} Let us note; * = ⊕, ≺, or ⊥, #t the void process, and # f the false process. Here is the formal signature of the language:

• ∀e ∈ E B, e ∈ U , #t ∈ U , # f ∈ U • ∀e ∈ U , ¬e ∈ U • ∀(e 1 , e 2 ) ∈ U 2 , e 1 * e 2 ∈ U
Properties, neutral/absorbing elements, distributivities and semi-distributivities have been defined in [START_REF] Delfieu | An algebra for branching processes[END_REF]. However, let us now just recall the definitions (equations ( 9),( 10),( 11),( 12)):

1) Causality: C is the set of all the causalities between every elements of E B. e 1 ≺ e 2 if e 1 is in the local configuration of e 2 :

e 1 ≺ e 2 if e 1 ∈ [e 2 ] (9)
2) Exclusion: X is the set of all the exclusion relations between every elements of E B. Two events are in exclusion iff they are either in direct conflict, either it exists a conflict at any level with an ancestor:

e 1 ⊥
This operator constitutes an abstraction which hides in a black box causalities and concurrency. The meaning of this operator is similar to the linear connector ⊕ of MILL [START_REF] Girard | Linear logic[END_REF]. It allows to aggregates resources. But, in the context of unfolding, events or conditions are unique and then they cannot be counted. Thus, this operator is here idempotent.

The expression e 1 ⊕ e 2 defines that e 1 and e 2 are in the same process.

Note that (⊕ e 1 e 2 ... e n-1 e n ) will abbreviate (e 1 ⊕ e 2 ⊕ e 3 ⊕ ...e n-1 ⊕ e n )

B. Axioms

The following axioms stem directly from previous assumptions and definitions made upon the algebraic model: The first axiom constitutes the basis of our approach. As discussed in the Section II, on the contrary of CCS, e is distributed onto two expressions, giving alternative process. ⊕ aggregates two elements in a process. Two elements are in a process if they are concurrent or in a causality relation. A causality can be expressed by two processes in exclusion: either ¬e 1 : e 1 has not occurred either e 1 ⊕ e 2 : e 1 and e 2 within the same process. This axiom comes from the introduction of the operator ¬ discussed in the beginning of the Section IV. It expresses that P and X are complementary sets.

Axiom 4.5 (Exclusion):

e 1 ⊥ e 2 ≡ de f (¬e 1 ⊕ e 2 ) ⊥ (e 1 ⊕ ¬e 2 )
The fifth axiom expresses that a conflict can be considered as two processes in conflict Axiom 4.6 (Distributivities):

• ≺, ⊥, ⊕ are distributive over .

• ≺, ⊕, are distributive over ⊥ (axiom 4.3).

• ⊥, are distributive over ⊥ and ⊕.

The distributivities over ⊥ are used in the transformation of an expression in the canonic form. The other distributivities will be used in the reduction process.

C. Canonic Form 1) Definition: The definition of the canonic form allows to define an equivalence called a "conflict equivalence". Definition 4.1: A canonic process is a formula expressed on elements of E B and with the operators ⊕, ⊥ ordered by an alphanumeric sort on the name of its symbol. where

P i = (⊕ e i 1 ... e i n )
This form is canonic and exhibits every processes P i of the unfolding.

Proof: In an unfolding every causality (≺) and every partial order ( ) can be reduced in ⊕ by deduction rules Modus Ponens (MP, MP 1 , MP 2 ), Simplification rule (S) and Par (see Section IV-C2). Moreover, ⊕ and ⊥ are mutually distributive, so ⊥ can be factorized in every sub-formula to reach the higher level of the formula. In fine, an alphanumeric sort on symbols of the processes can be applied to assure the unicity of the form.

This canonic form preserves conflicts, let us now define a conflict equivalence:

U 1 ≈ con f U 2
iff they have the same canonic form.

Remark 4.4:

A process is an aggregate set of events where ≺ and are hidden. This equivalence is lower than a trace equivalence: each process P i is an abstraction of a set of traces.

2) Derivation Rules: This section gives a set of rules which transform branching processes toward a canonical form. Theses transformations preserve conflicts whereas ≺ and are transformed in ⊕.

Let us note b a condition, e an event and E a well formed formula on the algebra. Theses rules allow to reduct process: 2) Dual form:

¬e 1 e 1 ≺ e 2 ¬e 1 ⊕ ¬e 2 MP
3) Simplification:

¬e 1 ⊕ E E S 1 ⊕b... E E S 2
Those rules are applied, in fine, to clear not pertinent informations in the process. S 1 rule is applied, to clear the negations whereas S 2 is applied to clear the conditions which have not been consumed.

4) Reduction of :

e 1 e 2 e 1 ⊕ e 2 Par
This rule corresponds to the definition of ⊕ These rules have been defined to lead to a canonic form.

D. Theorems

The properties of operators (definition, axioms and distributivites) allow to define theorems which are congruences w.r.t the operators of Section IV-A (proofs have been already stated in [START_REF] Delfieu | An algebra for branching processes[END_REF]). Let us now consider the following conventions: Let us note:

• l 1 = (e 1 , e 2 , ...e n ), l 2 = (e 2 , ...e n )

• l i the i th element of a list l.

• If e i is an element of the list l, let us note indice(e i ) the position of e i in l.

Remark 4.7: In the list of event constituting a chain of conflict (l = (e 1 , e 2 , ...e n )), for every event e i , the next (resp. previous) event in the same branching process is e i+2 or e i+3 (resp. e i-2 or e i-3 )

The next definition defines two processes U n and V n which are aggregation of events where the possible successor of an event e i is either l (indice(e i )+2) either l (indice(e i )+3) . Definition 4.8: Let us consider that n <= p (p: index of the last event implied in the chain of conflict):

       U 0 = e 1 U 1 n = l 1 n+2 ⊕U 2 n+2 U 2 n = l 1 n+3 ⊕U 2 n+3 U n = U 1 n ⊕U 2 n U n : processes beginning by e 1        V 0 = e 2 V 1 n = l 2 n+2 ⊕V 2 n+2 V 2 n = l 2 n+3 ⊕V 2 n+3 V n = V 1 n ⊕V 2 n
V n : processes beginning by e 2 binary relations on events (see Section IV) which is represented by the following algebraic expression U 2 :

U 1 = (⊕ b 1 b 2 b 3 b 4 b 5 (b 1 ≺ (e 1 ⊥ e 2 )) (b 2 ≺ (e 2 ⊥ e 3 )) ...)
After some steps of reduction (MP + S), U 1 becomes:

(e 1 ⊥ e 2 ⊥ e 3 ⊥ e 4 ⊥ e 5 ) (13)
The theorem (T 4.9) allows to compute from (13) its following canonic form: The two unfoldings of example 1 and 2 have the same canonic form, they are conflict-equivalent: U 1 ≈ con f U 2 1) Reasoning about processes: Let us consider all the process p of U 2 : (⊕ e 1 e 3 e 5 ), (⊕ e 1 e 4 ), ...

• ∀p ∈ U 2 whenever e 3 is present, e 1 is present.

• ∀p ∈ U 2 , ¬e 3 ⊥ (e 1 ⊕ e 3 ⊕ e 5 )
This is the algebraic definition of ≺. Finally from this chain of conflicts, the following causality can be deduced:

e 3 ≺ (e 1 ⊕ e 5 ) (16)
• A similar reasoning can be made:

∀p ∈ U 2 , ¬(e 1 ⊕ e 5 ) ⊥ (e 1 ⊕ e 3 ⊕ e 5 )
This is the algebraic definition of:

(e 1 ⊕ e 5 ) ≺ e 3 (17)
(16) and ( 17) expresses that there is a strong link between e 3 and the process (e 1 ⊕ e 5 ) but ≺ is no well suited to encompass this relation. Theses two processes are like "intricated". • In the same manner:

Equations ( 18) and [START_REF] Steele | Common LISP: the language[END_REF] show that e 1 and e 2 transform the chain of conflict in a unique conflict. New relations between events or processes can be introduced:

• Alliance relation: e 1 , e 3 and e 5 are in "an alliance relation". Every event of this set is enforced by the occurrence of the other events: e 1 ⊕ e 3 enforces e 5 , e 1 ⊕ e 5 enforces e 3 and e 3 ⊕ e 5 enforces e 1 .

• Intrication: the occurrence of e 3 forces e 1 ⊕ e 5 and reciprocally e 1 ⊕ e 5 forces e 3 .

• Resolving conflicts (liberation):

• e 1 resolves 3 conflicts on 4 (as e 2 , e 4 and e 5 )

• e 3 resolves every conflicts.

Semantically, e 3 can be identified as an important event in the chain. Moreover (⊕e 1 e 3 e 5 ) is a process aggregated with "associated events". This chain of conflict can be seen as two causalities in conflicts: (e 1 ≺ (e 4 ⊥ (e 3 ⊕ e 5 ))) ⊥ (e 2 ≺ (e 4 ⊥ e 5 ))

2) Example 3 (Cash dispenser): Let us consider the cash dispenser of the Figure 8, its unfolding in canonical form is: U3 = (⊥ (⊕ Consult EnterCode OKcode GetConsult) (⊕ Consult EnterCode OKcode Getcash) (⊕ Consult EnterCode BadCode) (⊕ Cash EnterCode OKcode Getcash) (⊕ Cash EnterCode OKcode GetConsult) (⊕ Cash EnterCode BadCode))

This expression enlightens that GetCash and BadCode are neither in the same process.

VI. CONCLUSION AND FUTURE WORK

This work is a first attempt to present an axiomatic framework to the analyze of the processes issued of an unfolding. From a set of axioms, distributivities and derivation rules, theorems have been established and a reduction process can lead to a canonic form The unfolding process, definitions, theorems and reduction rules have been coded in LISP [START_REF] Steele | Common LISP: the language[END_REF] with a package named PLT/Redex [3][12]. This canonic form assets an equivalence conflicts (≡ con f ) between unfoldings and then Petri nets.

Several perspectives are into progress. First, news theorems have to be established allowing to speed up the procedure of canonic reduction and to extend extraction of knowledge on relationship between events. Different kinds of relationship between events have to be defined and formalized: Alliance relation, Intrication, etc. Moreover, as already outlined in the last part of the example section, algebraic reasoning can raise semantic informations about events from the canonic form. Another perspective is to extend this approach to Petri nets with inhibitor and drain arcs.

Fig 1 .

 1 Fig 1. Chain of conflicts.

Fig 2 .

 2 Fig 2. Milner: rejection of distributivity of sequence on choice.

Remark 3 . 1 :

 31 The transitive aspect of F + implies a transitive definition of strict causality. A set B ⊆ B of conditions such as ∀b, b ∈ B, b = b ⇒ b b is a cut. Let B be a cut with ∀b ∈ B, b ∈ B\B, b b , B is the maximal cut. Definition 3.2: The unfolding Un f

Fig 3

 3 Fig 3. a) Petri net, b) Unfolding.

  and Max(C i ) are maximum cuts. Generally, any maximal cut B ⊆ B i corresponds to a reachable marking m of < N , m 0 > such as ∀p ∈ P, m(p) = |B p | avec B p = {b ∈ B | λ (b) = p}. The local configuration of an event e is defined by: [e] def = {e | e ≺ e} ∪ {e} and is a process. For example of unfolding in Figure 3.b: [e 4 ] def = {e 1 , e 3 , e 4 }.

  Fig 4. Unfolding.

Axiom 4 . 1 (

 41 Distributivity of ≺): e ≺ (e 1 ⊥ e 2 ) ≡ de f (e ≺ e 1 ) ⊥ (e ≺ e 2 )

Axiom 4 . 2 (

 42 Definition of ⊕):e 1 ⊕ e 2 ≡ de f (e 1 ≺ e 2 ) ⊥ (e 2 ≺ e 1 ) ⊥ (e 1 e 2 )

1 ≺ e 2 ≡

 12 de f ¬e 1 ⊥ (e 1 ⊕ e 2 )

Axiom 4 . 4 (

 44 Duality between ⊕ and ⊥):e 1 ⊕ e 2 ≡ de f e 1 ¬⊥e 2 e 1 ¬⊕e 2 ≡ de f e 1 ⊥ e 2

Theorem 4 . 2 (

 42 Canonical form): Let us consider an unfolding U, this form can be reduced in the following form: U = (⊥ P 1 P 2 ... P n )

Definition 4 . 3 (

 43 Conflict Equivalence): Let us U 1 ,U 2 unfoldings of Petri nets:

1 )

 1 Modus Ponens: ⊕ b... ⊕ b... ≺ e e MP 1 e e ≺ ⊕ b... ⊕ e b... MP 2 Where ⊕b... stands for the general form for ⊕b 1 b 2 ... b n . MP 1 expresses that b... are consumed by the causality, whereas, in MP 2 e stays in the conclusion.

Theorem 4 . 5 (

 45 Conflict): e 1 ≺ (e 2 ⊥ e 3 ) ≡ (e 1 ≺ (e 2 ⊕ ¬e 3 )) ⊥ (e 1 ≺ (¬e 2 ⊕ e 3 )) This theorem expresses how to develop a conflict and the following theorem allows to reduce processes: Theorem 4.6 (Absorption): Let E, F some processes: E ⊥ (E ⊕ F) ≡ E ⊕ F 1) Chain of conflicts: This section presents a theorem which computes the branching process in canonic form of a chain of conflict illustrated in Figure 5.

Fig 5 .

 5 Fig 5. Chain of conflicts. The axiomatic representation of the unfolding is: U = ((⊕ b 0 b 1 ... (b 0 ≺ (e 1 ⊥ e 2 ))(b 1 ≺ (e 2 ⊥ e 3 ))...) After some steps of reduction (MP + S): U = (e 1 ⊥ e 2 ⊥ ... ⊥ e p )

Theorem 4 . 9 :

 49 The canonic form of a chain of conflict C isU n ⊕V n : (e 1 ⊥ e 2 ⊥ ... ⊥ e p ) ≡ U n ⊕V n V. EXAMPLES A. Example 1The Figure6gives a Petri net which represents a chain of conflicts and its unfolding. The unfolding gives a tableof

Fig 6 .

 6 Fig 6. PN and unfolding of a chain of conflicts.

(Fig 7 . U 2 .expression U 2 :

 722 Fig 7. U 2 .

¬e 2 ⊥

 2 (e 2 ⊕ e 4 ) ⊥ (e 2 ⊕ e 5 ) ≡ dist ¬e 2 ⊥ (e 2 ⊕ (e 4 ⊥ e 5 ))≡ de f e 2 ≺ (e 4 ⊥ e 5 )(18)e 2 leads to a conflict ¬e 1 ⊥ ((⊕e 1 e 3 e 5 ) ⊥ (e 1 ⊕ e 4 ) ≡ dist ¬e 1 ⊥ (e 1 ⊕ ((e 3 ⊕ e 5 ) ⊥ e 4 )) ≡ de f e 1 ≺ ((e 3 ⊕ e 5 ) ⊥ e 4 )

Fig 8 .

 8 Fig 8. Cash dispenser.

  e 2 ≡ ((•e 1 ∩ •e 2 = / 0) or (∃e i , e i ≺ e 2 and e 1 ⊥ e i ))[START_REF] Glabbeek | Petri net models for algebraic theories of concurrency[END_REF] 3) Concurrency: I is the set of every couple of element of E B in concurrency. e 1 and e 2 are in concurrency if the occurrence of one is independent of the occurrence of the other. So, e 1 e 2 iff e 1 and e 2 are neither in causality neither in exclusion.e 1 e 2 ≡ ¬((e 1 ⊥ e 2 ) or (e 1 ≺ e 2 ) or (e 2 ≺ e 1 ))[START_REF] Best | The box algebra=petri nets+process expressions[END_REF] 4) Process: ⊕ aggregates events in one process. Two events e 1 and e 2 are in the same process if e 1 causes e 2 or if e 1 is concurrent with e 2 : e 1 ⊕ e 2 ≡ (e 1 ≺ e 2 ) or (e 2 ≺ e 1 ) or (e 1 e 2 )


David Delfieu
email: david.delfieu@irccyn.ec-nantes.fr

Médésu Sogbohossou
email: sogbohossoumedesu@yahoo.fr

An algebra for branching processes

The unfolding process of Petri Nets produces a set of causal nets where nodes are conditions or events and arcs express relations of causality, conflict or concurrency called branching processes. We propose in this paper an algebra and reduction rules allowing to extract informations, relation on events and a canonic representation of branching processes.

I. INTRODUCTION

Petri nets are a modeling tool widely used in the formal study of concurrent discrete-event systems. Verification of properties is based on a computable state graph [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF] if the net is bounded. For a highly concurrent system, this computation is hindered by a combinatory explosion. One cause of this explosion is the semantics of interleaving used to approximate the concurrency aspects of a system under modeling. Technics of unfolding [START_REF] Esparza | Unfoldings: A Partial-Order Approach to Model Checking[END_REF]- [START_REF] Mcmillan | Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits[END_REF] produce a-cyclic nets keeping concurrent aspects with partial order semantics.

Unfolding Petri nets give a set of causal nets where nodes are conditions or events. The arcs specify the causality relations. The exhibition of conflicts allows to partition this set in term of branching process. This paper proposes an algebra dedicated to the extraction of semantics in branching processes. This formal framework is based on a few basic assumptions and concepts and proposes a logical growth from expressions (well formed formulae) on terms to derivation rules and laws. In figure 1 is an unfolding. The events e i stand for events and b i for conditions: The algebra presented in this paper offers a syntax to express this unfolding and the reduction rules proposed in this paper, determine all the maximal processes of the unfolding. By example, which are expressed by the following expressions:

(e 1 ⊕ e 3 ⊕ e 5 ) ⊥ (e 1 ⊕ e 4 ) ⊥ (e 2 ⊕ e 4 ) ⊥ (e 2 ⊕ e 5 ) (e 1 ⊕ e 3 ) ⊥ e 2

Where ⊥ stands for the exclusion and ⊕ aggregates events in a processus, whereas e 1 ⊕e 3 ⊕e 5 is a compact representation of e 1 ⊕ e 2 ⊕ e 3 ⊕ e 4 ⊕ e 5 .

The originality of this approach is that it allows to extract non intuitive causalities from this set of events in conflicts, for example (figure 1), we will exhibit:

• Strong causalities: e 3 (e 1 ⊕ e 5 ) and e 4 (e 1 ⊥ e 2 ), or e 6 e 8

• Weak causalities e 1 e 3 , e 1 e 5 ,...

II. RELATED WORKS

A process algebra (CCS) has been already developed by Milner [START_REF] Milner | Calculus of Communicating Systems Lecture Notes in Computer Science[END_REF]. CCS is based on two central ideas: The notion of observability and the concept of synchronized communication. The elements of the alphabet are observable events and concurrent systems (processes) can be specified with the use of three operators: sequence, choice and parallelism.

A main property of CCS is the rejection of distributivity of the sequence upon the choice. This rejection is based on the fact that a.(x + y) and a.x + a.y are "language equivalent" but they are not equivalent in term of behavior.

Let's consider the expression x + y. It represents a choice: either x or either y can be observed. Let's now consider the expression a.(x + y), after the observation of a, (x + y) stay observable which means that either x or either y can be observable. But, in the expression a.x + a.y the distributivity has made a choice and this expression expresses two scenarios: one with a followed by x and one followed by y.

In CCS, Milner defines a finer law, the behavior law rejecting the distributivity of the sequence on the choice: a.(x + y) ≡ behaviorally a.x + a.y

In the context of unfolding, branching processes differ from the concurrents systems of Milner. Branching process are constituted with occurred events. The notion of observability loses sense in term of realized process. An unfolding produces all the prefixes (a is a prefix) called branching processes, a.x and b.x are the maximal processes for the considered expression.

The distributivity is then kept valid and a (x ⊕ y) can be reduced in (a x) ⊕ (a y) where a x and a y stands for two (distinct) branching processes. This last expression asserts that a causes x and a causes y. Unfolding can be represented with a set of a-cyclic graph. In an unfolding, every arc carries a unique label because it identifies an event which represent is the firing of a transition of the underlying Petri net. e 1 represents the firing of a transition in a given state corresponding to a particular marking. Another label e 2 can represent the firing of the same transition with different state of the system (marking).

Branching process does not feet with process algebra on numerous other aspects. For example a difference can be noticed about parallelism. While unfolding keeps true parallelism, process algebra considers a parallelism as interleavings.

Another difference is relative to events and conditions which are nodes of different nature in an unfolding. Conditions and events differ in term of ancestor. Every condition is produced by at most one event ancestor (none for the condition standing for m 0 , the initial marking), whereas every event may have 0, 1 or n condition ancestor(s). In CCS, there is no distinction between conditions and events and process can be cyclic.

However the works developed in CCS have shown the interest of an algebraic formalization: it allows to extract information, to propose reduction rules, and it defines equivalences. And this proposed algebra is dedicated to branching process tends to yield the same objective than CCS:

• a syntax that expresses in non ambiguous way the relations between the events ; • equivalence and reduction rules ; • extraction of semantics ; • a canonical form of an unfolding. For example, in the figure 1, e 1 , e 3 and e 5 are bounded by a particular relation. If two of these, for example e 1 and e 5 are in a process then e 3 must belong also, to the same process. This particular relation is captured by properties of ⊕ operator. In particular, we will establish that in a following theorem (VI):

(e 1 ⊕ e 5 ) ⊥ (e 1 ⊕ e 3 ⊕ e 5 ) ≡ (e 1 ⊕ e 3 ⊕ e 5 )

The second section exposes the basics notions about Petri net and unfolding. The third section depicts the new algebra, which is the contribution of this paper. The fourth section illustrates the use of the algebra on the unfolding of a non safe Petri Net.

III. UNFOLDING A PETRI NET

A. Petri net

A Petri net [START_REF] Meir | Recoverability of communication protocol -implications of theoretical study[END_REF] N =< P, T , W > is a triple with: P, a finite set of places, T , the finite set of transitions (P ∪ T are nodes of the net; (P ∩T = ∅), and W : (P ×T ) ∪ (T ×P) -→ N, the flow relation defining arcs (and their valuations) between nodes of N . In the sequel, we will consider only 1-valued Petri nets.

The pre-set (resp. post-set) of a node x is denoted

• x = {y ∈ P ∪ T | W(y, x) > 0} (resp. x • = {y ∈ P ∪ T | W(x, y) > 0}).
A marking of a Petri net N is a mapping m : P -→ N. A transition t ∈ T is said enabled by m iff: ∀p ∈ • t, m(p) ≥ W(p, t). This is denoted: m A Petri net is k-bounded iff ∀m, reachable from m 0 , m(p) ≤ k (with p ∈ P). It is said safe when 1-bounded. Two transitions are in a structural conflict when they share at least one preset place; a conflict is effective when these transitions are both enabled by a same marking.

B. Unfolding

In [START_REF] Engelfriet | Branching processes of Petri nets[END_REF], the notion of branching process is defined as an initial part of a run of a Petri net respecting its partial order semantics and possibly including non deterministic choices (conflicts). It is another Petri net that is acyclic and the largest branching process of an initially marked Petri net is called the unfolding of this net. Resulting net from an unfolding is a labeled occurrence net, a Petri net whose places are called conditions (labeled with their corresponding place name in the original net) and transitions are called events (labeled with their corresponding transition name in the original net).

An occurrence net [START_REF] Chatain | Complete finite prefixes of symbolic unfoldings of safe time Petri nets[END_REF] O =< B, E, F > is a 1-valued arcs Petri net, with B the set of conditions, E the set of events, and F the flow relation (1-valued arcs), such that:

| • b| ≤ 1 ( ∀b ∈ B), • e = ∅ (∀e ∈ E), and F + (the transitive closure of F) is a strict order relation, from which O is acyclic. M in(O) = {b | b ∈ B, | • b| = 0} is the minimal conditions and corresponds to the initial marking. Also, M ax(O) = {x | x ∈ B ∪ E, |x • | = 0} are maximal nodes.
Three kinds of relations could be defined between the nodes of an occurrence net. First, two nodes x, y ∈ B ∪ E are in strict causal relation if (x, y) ∈ F + , and will be denoted

x y. ∀b ∈ B, if e 1 , e 2 ∈ b • (e 1 = e 2 )
, then e 1 and e 2 are in conflict relation, denoted e 1 e 2 . More generally, for x, y ∈ B ∪ E, if e 1

x et e 2 y, then x y, x e 2 and e 1 y. Symbol represents concurrency relation:

x y iff ¬((x y) ∨ (y x) ∨ (x y)).
A cut is a set of conditions all in mutually concurrency relation. A B-cut is a maximal cut according to inclusion and represents a marking of the original net.

The local configuration of an event e, denoted [e], is the set of events e such that e e (relation ≺ is defined on F * where F * is the transitive and reflexive closure of F).

Let be a net N = (P, T , W). < N , m 0 > admits U nf =< O, λ > as branching process (or unfolding) if:

• O =< B, E, F > is an occurrence net; • λ is the labeling function such that λ : B ∪ E → P ∪ T .
It verifies the following properties:

-λ(B) ⊆ P, λ(E) ⊆ T ; -λ(M in(O)) = m 0 ;
for all e ∈ E, restriction of λ to • e (resp. e • ) is a bijection between • e (resp. e • ) and • λ(e) (resp. λ(e) • ). We have • λ(e) = λ( • e) and λ(e

) • = λ(e • ),
what means that λ preserves the environment of a transition. The resulting labeled occurrence net is defined up to isomorphism, what means that we obtain a same structure of net up to the name of nodes, and with same labeling of nodes.

A causal net C is an occurrence net C =< B, E, F > with an adding restriction: ∀b ∈ B, |b • | ≤ 1. So, all conflicts are resolved in a causal net, and this net corresponds to a partial order run in an unfolding. The set of events of a causal net is called a process. Notice that only the order relations ≺ and are admitted between events of a process.

IV. DEFINITION OF THE ALGEBRA

We have shown in the previous section, how unfolding exhibits causal nets and conflicts. Otherwise, every couple of events which are not bounded by a causal relation or the same conflict set are in concurrency. We have developed a software producing the unfolding which builds a table making explicit every binary relations between events. In fact, this table establishes only the relations of causality and exclusion. If a binary relation is not explicit in the table, it means that the couple of events are in a concurrency relation. We show in this section that this table has led us to introduce a new operator which collapses events in a process.

Let EB = E ∪ B a finite alphabet, composed of the events and the conditions generated by the unfolding. In this set every couple of elements satisfies:

• a causality relation C • a concurrency relation I • an exclusive relation X The set of binary relations is partitioned in three parts as illustrated in figure 2: This last figure makes appear the operators of this algebra. A couple of events can be bounded by a relation of causality, exclusion or concurrency. The causality and concurrency set can be collapsed to constitute the set of all the processes of an unfolding. And this set is the complementary of the exclusion set. If some events are not in a relation of exclusion, they are in the same process. To express the fact that events are in the same process, a new operator noted ⊕ is introduced.

The negation operator allows to switch from exclusion set to the process set. The algebra is then defined by A = {EB, ( , , ⊥ , ¯, ⊕)} ⊕ and ⊥ are almost similar to boolean operator "." and " + ", except that boolean operators are mutually distributive and we will show in the section IV-B2, that ⊥ is not distributive over ⊕.

The internal composition laws are: Obviously, if e 1 ≺ e 2 then e 1 e 2 . The occurrence of e 1 is a necessary condition to the occurrence of e 2 .

Properties:

• is associative and transitive;

• has a neutral element t e ≡ e; • every element of EB has an opposite: f e ≡ ē.

2) Exclusion: X is the set of all the exclusion relations between every elements of EB. To define the this operator let's first go back to it's definition given in the section concerning the unfolding:

e 1 e 2 ≡ ((•e 1 ∩ •e 2 = ∅) and (e 1 = e 2 )
The definition of ⊥ is more generally: two events are in exclusion iff they are either in direct conflict, either it exists a conflict at the level of a common ancestor. And so they belongs to different processes: (e 1 e 2 ), (e 2 e 3 ), (e 3 e 4 )...

4) Process:

The figure fig. 2) illustrates that ⊕ aggregates events in one process. Two events e 1 and e 2 are in the same process if e 1 causes e 2 or if e 1 is concurrent with e 2 : e 1 ⊕ e 2 ≡ (e 1 e 2 ) or (e 1 e 2 )

The meaning of this operator is similar to the linear connector ⊕ of MILL [START_REF] Yves | Linear logic[END_REF] in the sense that its allows to aggregates resources. But in the context of unfolding, events or conditions are unique and then they cannot be counted. Thus, this operator is idempotent.

The relation e 1 ⊕ e 2 defines that e 1 and e 2 are in the same process. This operator is n-ary. In n-ary expressions we will use the pre-fixed notation (⊕e 1 e 2 e 3 ...) which abbreviates (e 1 ⊕ e 2 ) and (e 2 ⊕ e 3 ).... Properties:

• ⊕ is commutative, associative and transitive;

• Idempotency: e ⊕ e ≡ e • Neutral element: e ⊕ t ≡ e • Absorbing element: e ⊕ f ≡ f • e ⊕ ē ≡ t In the same manner used for ⊥, we will use a pre-fixed notation for ⊕ for an n-ary use (n > 2): (⊕ e 1 e 2 e 3 e 4 ...) which abbreviates the set of concurrencies: (e 1 ⊕ e 2 ), (e 2 ⊕ e 3 ), (e 3 ⊕ e 4 ) ...

B. Relations between operators

The distributivities over ⊥ are used in the transformation of an expression in the canonical form. The other distributivities will be used in the reduction process.

1) Distributivities:

• est distributive over . • ⊥ is distributive .

• ⊕ is distributive over ⊥ 1 and .

• is distributive over ⊥ and ⊕.

2) Non-distributivities: For the first and the second item, the right member these items are of the form: (e op e 1 ) (e op e 2 ) (with op = ⊕, ⊥ ). Theses expressions establish a temporal precedence between (e op e 1 ) over (e op e 2 ) which does not exist in the left member. For example, in the second member of the first "non distribitivity", (e ⊕ e 1 ) cannot precede (e ⊕ e 2 ) because of the presence of e in the two expressions.

e ⊥ (e 1 ⊕ e 2 ) ≡ (e ⊥ e 1 ) ⊕ (e ⊥ e 2 ) if e ⊥ (e 1 ⊕e 2 ) implies (e ⊥ e 1 )⊕(e ⊥ e 2 ) the reciprocal is false. This is a semi-distributivity. Because (e e 1 )⊕(e e 2 ) can derive in e (e 1 ⊥ e 2 ). To resume the distributivities ( √ ) and the non distributivities (×) are expressed in the following table. The distributivities must be read from in rows. For example, the first line expresses that is only distributive over ⊥. The following axiom explicits a conflict: Axiom 2 (Exclusion):

e 1 ⊥ e 2 ≡ def ( ē1 ⊕ e 2 ) ⊥ (e 1 ⊕ ē2 )
The following axiom expresses that a concurrency relation encompasses three alternative processes: the occurrence of e 1 , the occurrence of e 2 , or the process composed with e 1 and e 2 :

Axiom 3 (Concurrency):

e 1 e 2 ≡ def e 1 ⊥ e 2 ⊥ e 1 ⊕ e 2
2) Derivation Rules: Theses rules allow to reduct process:

ē1 (e 1 ⊕ e 2 . . . ⊕ e n ) e ē GM P 5) (⊕ b ... E) (⊕ b ...) (⊥ e 1 e 2 ) (⊥ (⊕ e 1 (e 2 ) E)(⊕ e 2 (e 2 )E)) D
This rule expresses that a conflict divides a process.

6)

ē1

⊕ E E S
This rule is applied on canonical form to clear the negations.

V. CANONICAL FORM

We give first, the definitions of algebraic definition of unfolding and process:

A. Preliminar definitions Definition 1 (AEU ): An Algebraic Expression of Unfolding (AEU ) is a well formed formulae inductively defined by:

• t stand for true, f stand for false are terms ;

• ∀e ∈ EB, e, ē are terms ;

• a term is an AEU • if φ, φ 1 , φ 2 are AEU : * φ 1 ⊕ φ 2 is an AEU ; * φ 1 ⊥ φ 2 is an AEU ; * φ 1 φ 2 is an AEU ; * φ 1 φ 2 is an AEU ;
Theorem 1: Every unfolding of Petri nets is an algebraic expression of unfolding.

Proof: As the unfolding process produces only three types of relation between events: causality, concurrency and exclusion, every unfolding can be translated in a AEU . As evoked in the figure 1, by definition, every pair of elements (e 1 , e 2 ) in EB| X -either e1 ≺ either e 1 e 2 is bounded by the ⊕ operator. An AEU is composed of processes.

Definition 2 (Process):

A process is a well formed formulae inductively defined by:

• t, f are terms ;

• ∀e ∈ EB are terms ;

• a term is a process ; • If p 1 , p 2 , . . . p n are processes: * p 1 ⊕ p 2 . . . ⊕ p n is a process ; * p 1 p 2 . . . p n is a process ; * p 1 p 2 . . . p n is a process ; ⊥ is an operator that partitions the AEU into processes.

B. Canonical form

Definition 3: A canonic process is a formula expressed on elements of EB and with the operators ⊕ and ordered by an alphanumeric sort on the name of its symbol.

Theorem 2 (Canonical form): Let's consider an unfolding U , this form can be reduced in the following form:

U = p 0 ⊥ p 1 ⊥ ... ⊥ p n
This form is canonic and allows to extract all the canonic processes p i .

Proof: In an unfolding every operator can be reduced in ⊕ by deduction rule Caus (see section IV-C2). Moreover, ⊕ is distributive on the other operators ⊥ and and ⊥ is distributive over . So ⊥ can be factorized in every sub-formula. In fine an alphanumeric sort on symbols of the process can then be applied to assure the unicity of the form. Definition 4 (member of a canonic process): Let e ∈ EB, φ a term, p a process • e ∈ p iff e is a term of the process p.

• φ ∈ p iff φ is a process and φ is a sub-formula of p. Now we can define the membership of an unfolding. An element e ∈ EB, e belongs to an unfolding U iff ∃p i ∈ U such that e ∈ p i . Let's now define how a formula can be interpreted.

Let U = p 0 ⊥ p 1 ⊥ ... ⊥ p n be an unfolding, constituted by n processes, e an event, φ a term:

• |= e if e ∈ U • p i |= e if e ∈ p i . • |= ē if e ∈ U • p i |= ē if e ∈ p i . • |= φ if φ ∈ p i , ∀p i ∈ U, • p i |= φ if φ ∈ p i . • |= φ ⊥ ψ if ∃p i , p j ∈ U such as p i |= φ p j |= ψ
The canonical form of the upper graph of the example of the figure 1: (⊥ e 1 e 2 e 3 e 4 e 5 ) ≡ (⊥ (⊕ e 1 e 2 e 3 e 4 e 5 )

(⊕ e 1 e 2 e 3 e 4 e 5 ) (⊕ e 1 e 2 e 3 e 4 ) (⊕ e 1 e 2 e 3 e 5 ))

C. Extraction of semantics

The extraction of semantics is based on the formulation in canonical form and the analysis of membership of events in processes.

In the unfolding the causality (≺) is defined by the transitive closure of F + , where F is the flow relation in causal nets which is a strict notion of causality, because it induces a path between nodes to be causal. We introduce here a larger notion of causality ( ) where two events can be causal event even if it does not exist a path between them.

Definition 5 (Strong causality): e 1 e 2 iff for every p i in U , whenever e 1 belong to process p i , e 2 belongs to p i , else if e 1 does not belong to a process p j then e 2 cannot belong to p j .

In the previous example, ∀p i ∈ U , whenever p i |= e 3 then p i |= (e 1 ⊕ e 5 ). Moreover, if p i |= e 4 then p i |= (e 1 ⊥ e 2 ), in the same manner if p i |= e 5 then p i |= (e 1 ⊥ e 2 ). So, we can deduce of the canonical form the following causalities: In this example, it is obvious that e 6 forces e 8 and vice versa. A weaker causality can be defined relaxing the second assertion in the definition of : Definition 6 (Weak causality): e 1 e 2 iff for every p i in U , whenever e 1 belong to process p i , e 2 belongs to p i , else if e 1 does not belong to a process p j then e 2 can belong to p j .

In the previous example (introduction), whenever ∀p i ∈ U, if p i |= e 2 then p i |= e 4 , but it exists a process p j = e 1 ⊕ e 4 where p j |= e 4 but p j e 2 . In the same manner ∀p i ∈ U, if p i |= e 3 then p i |= e 5 , but it exists a process p j = e 2 ⊕ e 5 where p j |= e 5 but p j e 2 :

• e 2 e 4 • e 3 e 5

VI. THEOREMS

The first theorem of this section allows to build the canonic form of the generalized of the example of the introduction. Let's consider the following conventions:

• The set of conflicts (e 1 ⊥ e 2 ) ⊕ (e 2 ⊥ e 3 )... can be aggregated with C = (⊥ e 1 e 2 e 2 e 3 e 4 ... e p )

• Lets note l i the i th element of a list l.

• if e i is an element of the list l, let's note indice(e i ) the position of e i in l

The next definition defines two U n and V n union of lists where the possible successor of an element e i is l(indice(e i )+ 2) either l(indice(e i ) + 3):

Definition 7: Let's consider that n <= p:

       U 0 = e 1 U n = U 1 n ∪ U 2 n U 1 n =l n+2 ∪ U 2 n+2 U 2 n =l n+3 ∪ U 2 n+3
U n defines all the processes beginning par e 1 .

       V 0 = e 2 V n = V 1 n ∪ V 2 n V 1 n =l 1 n+2 ∪ V 2 n+2 V 2 n =l 1 n+3 ∪ V 2 n+3
V n defines all the processes beginning par e 2 . Then this conflict can be canonically rewritten with the following form

C ≡ U n ∪ V n
Proof: Correctness Let's consider an incorrect process q ∈ L p . q = (⊕ e q1 e q2 e q3 e q4 ... e qp )

This incorrectness implies the existence of two events in q such as e qi ⊥ e qi+1 and e qi , e qi+1 corresponding to two successive events of l. This is in contradiction with the definition of the functions (U

1 n , U 2 n , V 1 n , V 2
n ) for which events are added with either l n+2 either l n+3 . So the indices cannot be consecutive. Completeness Let's consider a valid process q = (⊕ e q1 e q2 e q3 e q4 ... e qp ) not included in L p . ∀e ∈ q, if q is valid then ∀(e i , e j ) ∈ q, ¬(e i ⊥ e j ) so it implies that e i and e i are not successive in l and every enabled event is in q. Moreover, as q is not included in L p , it exist at least one couple (e qi , e qij ) which does not correspond to the construction defined by the functions (

U 1 n , U 2 n , V 1 n , V 2
n ) which define the possible successor of an event. This means that indice(e qj ) > indice(e qi + 3). For every n = indice(e qj ) -indice(e qi ) greater than 3, lets note i2 = indice(qi) + 2 the event e qi2 is an possible event which is not in q (contradiction).

The following theorem is evoked in the introduction (section II), allows to compute maximal process: VII. APPLICATION

In the following example we show how to translate an unfolding and how to produce reduction to obtain the maximal processes of the unfolding. Let's considerer the Petri net in the figure 4:

The unfolding builds a table that explicit every relations between events and conditions, its representation is given in the figure 5: This net is unsafe, P 3 may have 2 tokens, this appears in the unfolding with the two parts of the figure which distinguish between the token coming from P 1 and those from P 2 .

The algebraic translation is produced with the following transformations:

• Each arc is a causal relation e 1 e 2 • Each conflict: e (⊥ e 1 e 2 . . . e n )

• When more than one condition b i is expressed on an event:

(⊕ b 1 b 2 . . . b n ) e The same simplifications are applied twice to the left part of the unfolding: ē6 treats the conflict b 3 (e 6 ⊥ e 4 ) and P 1 becomes:

  Fig. 1. Unfolding

t→.

  Firing of t leads to the new marking m (m t → m ): ∀p ∈ P, m (p) = m(p) -W(p, t) + W(t, p). The initial marking is denoted m 0 .

Fig. 2 .

 2 Fig. 2. Partition of binary relations

e 1 ⊥Fig. 3 .e 2 e 2 e 3 -but e 1 ⊥ e 3 •

 1333 Fig. 3. Non-transitivity of

•

  ⊕, ⊥ and are non distributive over ≺: e ⊕ (e 1 e 2 ) ≡ (e ⊕ e 1 ) (e ⊕ e 2 ) e ⊥ (e 1 e 2 ) ≡ (e ⊥ e 1 ) (e ⊥ e 2 ) e (e 1 e 2 ) ≡ (e e 1 ) (e e 2 )

•

  is non distributive over ⊕:e (e 1 ⊕ e 2 ) ≡ (e e 1 ) ⊕ (e e 2 )

e 1 ⊕ e 2 ≡ def e 1 ⊥e 2 e 1

 1221 ⊕e 2 ≡ def e 1 ⊥ e 2

• e 3

 3 (e 1 ⊕ e 5 ) • e 4 (e 1 ⊥ e 2 ) • e 5 (e 2 ⊥ e 3 ) • e 6 e 8 • e 8 e 6

Theorem 3 :

 3 If we consider the conflict C = (⊥ e 1 e 2 e 2 e 3 e 4 ... e p )

Theorem 4 :e 1 (e 2 ⊥ e 3 )

 4123 Let E an EAU , e ∈ EB: e ⊥ (e ⊕ E) ≡ e ⊕ E Proof: e ⊥ (e ⊕ E) ≡ (e ⊕ t) ⊥ (e ⊕ E)≡ dist e ⊕ (t ⊥ E) ≡ prop⊥ e ⊕ EThe following theorem expresses how to develop a conflict: Theorem 5 (Conflict): e 1 (e 2 ⊥ e 3 ) ≡ (e 1 (e 2 ⊕ e 3 )) ⊥ (e 1 (e 2 ⊕ e 3 )) Proof: ≡ def e 1 ((e 2 ⊕ e 3 ) ⊥ (e 2 ⊕ e 3 ) ≡ dist (e 1 (e 2 ⊕ e 3 )) ⊥ (e 1 (e 2 ⊕ e 3 ))

  Fig. 4. Petri net

Fig. 5 .P 1 =P 1 =

 511 Fig. 5. Unfolding

In this process, e 3 corresponds to the firing of T 5 , this process illustrates the case where the activity of the net comes from the token in P 1 . Another proof sequence (firing of T 2 ) can be conducted to lead to the two other processes. One for the case leading to the event e 5 and the other leading to the event e 7 .

VIII. IMPLEMENTATION ASPECTS

The unfolding has been implemented in Racket/Scheme [START_REF] Jay | Scheme: An Interpreter for Extended Lambda Calculus MIT AI Lab[END_REF] (a recent evolution of LISP language). The unfolding produces an hashing table. The couples of events are associative keys for the table. For every couple of events, the relation is explicated as follow:

• table[e 1 , e 2 ] = t if e 1 e 2 (≺ corresponds to the definition of section III-B) ;

is not a key of the table then e 1 e 2 . The axiomatisation of the algebra allows to solve the previous example like a fixed-point formulae. When non more rules can be applied the final formulas (the leaves of the prove tree) gives the set of maximal processes.

The algebra and reduction rules have been defined with a package named "PLT/Redex" [START_REF] Felleisen | Semantics Engineering with PLT Redex[END_REF]. A Redex Model is formed of two parts: a regular-tree grammar and reduction rules.

The following part of code is the grammar. It defines the Algebraic Expression of Unfolding AEU , the process P , X the conflicts (section 1) and E a well formed expression. The following code gives the S -expression (programs, expressions, variables, or literal constants) and contexts which are parts of the syntax of the language.

The def ine -language key-world specify the abstract syntax with a fully parenthesized notation:

• The second line defines the set of terms: e

• The following defines boolean type, the events and the conditions, then n -ary operator and unary operator. • Then comes the definitions of process (P ), conflicts (X) and Expression. • The keyword variable means that a variable can be instantiated: for example e can be instantiated by e 1 , e 2 , ... • The ellipse F... represent the regular expression F * • Finally, C -P , C -X and C -E are respectively the contexts of the processes, the conflicts and the expressions. This second part describes pattern-based formulation of reduction possibly in context. ------------------------------------------------------; (⊕ ; Absorbing element (--> (in-hole C-P (⊕ Q_1 ... f Q_2 ... )) (in-hole C-P f)) ;------------------------------------------------------; Falsification (--> ;------------------------------------------------------; associativity (--> ------------------------------------------------------; Conflict between n events (--> (in-hole C-E (⊥ e ...)) (in-hole C-E (f (⊥ e ... )))) ;≺ ------------------------------------------------------ The first part express basics properties: absorbing element and associativity of ⊕. The second part illustrates how causal-ity and conflicts are reduced.

f is a meta-function which has several rules: It is first used to ease the resolution of conflicts:

• The first item sorts the symbol in alphabetic order. It is useful to assure the canonicity of the expression; • The second verifies that if b 1 is member of the sequence b 0 ... then b 1 is substituted by e. • The third verifies that if the sequence b 1 .. is a subsequence of b 0 ... then b 1 ... is substituted by e. The second rule of f is to implement the computing of

The auxiliary function lproc is the implementation of the theorem (3). f builds for every list of event in conflicts of type:

(⊥ e 1 ...e n )

the set of resulting processes.

A. Example 1

Let's consider the examples given in the introduction of the paper, if we apply the reduction rules defined in our algebra of the first graph, 4 maximal processes expressed in canonical form are obtained: Concerning the Petri Net presented in this section, the analyze of the unfolding gives 138 applications of derivation rules and theorem. It finally exhibits four maximal processes in canonical form which are the leaves of the demonstration tree (two frames from which where none rules can be applied any more):

IX. CONCLUSION

This work is a first attempt to establish an algebra for reasoning about branching process. It shows that an unfolding of a Petri net can be represented in an algebraic way. This algebra leads to express the unfolding in a canonical form.

This algebraic framework has been implemented in P T L/Redex, which is a module based on the language Racket (last evolution of LISP ).

The canonical form is induced by the structure of the algebra and the consideration of an alphanumeric sort on the symbols. This form illustrates processes that are in exclusion. From this form, non intuitive relations can be established. Some perspectives of this work can be evoked. First, the procedure of extraction of semantics needs to be automatized and other types of relations between events need to be explored.

This paper propose an analyze of the unfolding of nontemporized Petri net. A second perspective, could be to extend this work to temporized Petri nets. In P LT /redex, some works shows how to introduce rules to extends models with the axiomatics calculus on integer (based on λ calculus ). Theses adding rules could help to manage the computing of temporalities.


Guiggiani

A J Kassab

E Divo

Marc Bonnet

Massimo Guiggiani

Comments about the paper entitled "A generalized boundary integral equation for isotropic heat conduction with spatially varying thermal conductivity" by

HAL is

The purpose of the paper under discussion [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF] was to establish a boundary-only integral formulation for heat conduction with isotropic but spatially varying conductivity k(x) (x = (x, y): field point), i.e. for temperature distributions T such that div [k(x)∇T (x)] = 0 [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF] In order to do so, a variant kind of fundamental solution, denoted E(x, ξ), associated to a forcing term D(x, ξ) containing a singular source at a given point ξ = (x i , y i ), is introduced:

div [k(x)∇E(x, ξ)] = -D(x, ξ) (2)
1 Examination of the sampling property

The following, crucial, requirement on the forcing term D(x, ξ) (Eqs. (5c-d) of [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF]) must be met in order to get rid of the domain integral that arises in the reciprocal theorem (Ω denotes an arbitrary domain required only to enclose the source point ξ):

Ω T (x)D(x, ξ) dΩ(x) = T (ξ)A(ξ) with A(ξ) = Ω D(x, ξ) dΩ(x) (3)
The above relation is the analogue, for the particular fundamental solution at hand, of the sampling property of the Dirac distribution (the term sifting property was used in [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF]). However, the kernel E(x, ξ) obtained by the authors, i.e. (Eq. ( 23) of [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF]):

E(x, ξ) = - 1 2π dr r k(r; x i , y i ) (4)
where (in 2D) (x, y) = (x i + r cos θ, y i + r sin θ) and having introduced for convenience the 'averaged' conductivity k:

k(r; x i , y i ) = 1 2π 2π 0 k(r, θ; x i , y i )dθ (5)
happens to violate the crucial requirement (3). Indeed, the kernel given by Eq. ( 4) is readily seen to solve the equation

div [ k∇E] = -δ(x -ξ) = 1 r ∂ ∂r r k ∂E ∂r (6)
(the second equality holds because ∂E/∂θ = 0). Hence, by subtracting the above equation from Eq.

(2), one gets the following expression for the forcing term D:

D(x, ξ) = δ(x -ξ) + 1 r ∂ ∂r r( k -k) ∂E ∂r = δ(x -ξ) + 1 2πr ∂ ∂r 1 - k k ≡ δ(x -ξ) + ∆D (7)
Except when the material is homogeneous, the complementary term ∆D is therefore in general nonzero at x = ξ, ie outside the source point ξ; this is indeed obvious in some of the examples of the paper under discussion (see Eqs. (40,46) and Figs. 3,5,12). In fact, for sufficiently smooth conductivities, k -k = O(r) so that ∆D is even nonsingular at x = ξ. But then, it is impossible for properties (3) to hold. In fact, using the definition of A(ξ) for a given domain Ω, one has:

Ω T (x)D(x, ξ) dΩ = A(ξ)T (ξ) + Ω [T (x) -T (ξ)]∆D(x, ξ) dΩ ≡ A(ξ)T (ξ) + J(ξ) (8)
and property (3) would mean that the integral J(ξ) in the above formula, which measures the absolute error in the realization of (3), vanishes for any domain shape and temperature distribution, which is false by Haar's lemma since D is not identically zero outside the source point. For example, Eq. (5c-d) of [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF] for the same function T (which incidentally is required to have compact support) but two different domains Ω 1 ⊂ Ω 2 would lead to:

Ω 2 \Ω 1 T (x)D(x, ξ) dΩ(x) = T (ξ)[A 2 (ξ) -A 1 (ξ)]
and a contradiction arises. From the above equation, the integral in the l.h.s. should, apart from the geometrical arrangement of ξ, Ω 1 , Ω 2 , depend only on the value of T at the source point ξ.

But since Ω 2 \ Ω 1 does not contain ξ, the above equation should hold true for any extension of T outside Ω 2 \ Ω 1 , which is absurd. In other words, as soon as

D(x, ξ) is nonzero over Ω 2 \ Ω 1 , the integral Ω 2 \Ω 1 T (x)D(x, ξ) dΩ(x)
cannot depend on T only through the value T (ξ). Thus, Eq. ( 3) is in general not true. As a consequence, the two members of the integral equation (10) in [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF] are in general not equal.

Limiting process for vanishing neighbourhood

Let ξ be a fixed point on the boundary ∂Ω of a two-dimensional domain Ω. We consider an exclusion neighbourhood v ε (ξ) of ξ, of radius ≤ ε (Figure 1). For any ε > 0, ξ is always an external point for the domain Ω ε (ξ) = Ω \ v ε (ξ) whose boundary ∂Ω ε is given by

∂Ω ε = (∂Ω -e ε ) + s ε = Γ ε + s ε ,
where The singular integral equation for heat conduction problems (T : unknown temperature field) in non-homogeneous media can then be sought as the limiting case, for ε → 0, of the integral identity

s ε = Ω ∩ ∂v ε , e ε = ∂Ω ∩ vε , and Γ ε = ∂Ω -e ε (v ε is the closure of v ε ). r ξ e ε s ε v ε Ω ε Γ ε
Γε+sε E(x, ξ)k(x) ∂T ∂n (x) dS x - Γε+sε k(x) ∂E ∂n (x, ξ)T (x) dS x - Ωε T (x)D(x, ξ) dΩ(x) = 0 (9)
where E(x, ξ) is the fundamental solution defined by Eqs. (4,5).

Source point interior to the domain. First, consider an internal source point ξ ∈ ∂Ω.

Then s ε is a closed surface, and one has:

Ωε D(x, ξ) dΩ(x) = - sε k(x) ∂E ∂n (x, ξ) dS x - ∂Ω k(x) ∂E ∂n (x, ξ) dS x (10)
Since Γ ε = ∂Ω, identity (9) becomes (note that D = ∆D on Ω ε ):

∂Ω E(x, ξ)k(x) ∂T ∂n (x) dS x - ∂Ω k(x) ∂E ∂n (x, ξ)T (x) dS x + sε E(x, ξ)k(x) ∂T ∂n (x) dS x - sε k(x) ∂E ∂n (x, ξ)[T (x) -T (ξ)] dS x - Ωε [T (x) -T (ξ)]∆D(x, ξ) dΩ(x) + T (ξ) ∂Ω k(x) ∂E ∂n (x, ξ) dS x = 0 (11)
Assuming that T is C 0,α -regular at x = ξ, the integrals over s ε vanish in the limit ε → 0 in the same way, due to the fact that the kernel E exhibits the usual ln r singularity at x = ξ. Hence, the following integral identity is obtained from Eq. (11) in the limit ε → 0:

T (ξ) Ã(ξ) = ∂Ω E(x, ξ)k(x) ∂T ∂n (x) dS x - ∂Ω k(x) ∂E ∂n (x, ξ)T (x) dS x -J(ξ) (12)
where the free-term Ã(ξ) is given by

Ã(ξ) = - ∂Ω k(x) ∂E ∂n (x, ξ) dS x (13)
It is worth noting (still using the C 0,α regularity assumption for T ) that

Ωε [T (x) -T (ξ)]D(x, ξ) dΩ(x) = Ωε [T (x) -T (ξ)]∆D(x, ξ) dΩ(x) = J(ξ)
Hence, from the analysis of Sec. 1, a boundary-only representation formula for T cannot be obtained in general.

Source point on the boundary. A similar analysis can be conducted. Using the fact that

Ωε D(x, ξ) dΩ(x) = - Γε+sε k(x) ∂E ∂n (x, ξ) dS x
one obtains in the limit ε → 0 the following statement:

T (ξ) Â(ξ) = ∂Ω E(x, ξ)k(x) ∂T ∂n (x) dS x -lim ε→0 Γε k(x) ∂E ∂n (x, ξ)T (x) dS x -J(ξ) (14)
where the free-term Â(ξ) is given by

Â(ξ) = -lim ε→0 Γε k(x) ∂E ∂n (x, ξ) dS x = - ∂Ω k(x) ∂E ∂n (x, ξ) dS x ( 15
)
Here again, the domain integral is not expected to vanish. The above integral is convergent in the ordinary sense in the limit ε → 0 because ∂E/∂n is proportional to ∂r/∂n.

Discussion

From the analysis conducted in Sec. 1, the integral representation (13) and the integral equation (15) involve in general a domain term. It is thus not correct to state, as was done in [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF], that recourse to the kernel E leads to boundary-only integral formulations for heat conduction problems in non-homogeneous media. However, since E is in some sense an 'averaged' version, associated with the 'averaged' conductivity k, of the (unknown) fundamental solution associated with the 'true' conductivity k, it is reasonable to expect the domain integrals in Eqs. ( 13) and ( 15) to be lower than those associated with the usual fundamental solution G(x, ξ) = -(2πk) -1 ln r for homogeneous conductivity k.

The kernel E given by Eqs. (4,5) is not strictly speaking a fundamental solution: the conductivity k, and hence the partial differential operator in Eq. ( 6), depends on the source point ξ. However, for a fixed choice of ξ the kernel E behave like the more usual fundamental solutions.

It is also important at this juncture to remark that using the relative accuracy of satisfaction of Eq. 8 as a measure of the exactness of is misleading. The ratio of A(ξ)T (ξ) to the integral term J(ξ) can assume any arbitrarily small value by adding a constant to the sought-for temperature. The reason for this behaviour is that J is insensitive to the choice of this constant. On the other hand, fact, what is under scrutiny here is the exactness of a mathematical formulation, and hence the absolute validity of Eq. (3).

Besides, when k(x) is a polynomial in x, y (or x, y, z in 3D) involving only odd powers of the coordinates, k = k(ξ): in this case, E(x, ξ) reduces to the classical fundamental solution for a medium with a constant conductivity equal to k(ξ). This is the case for the bi-and tri-linear conductivity distributions (Eqs. (33,36) in [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF]).

The free terms Ã(ξ) and Â(ξ) correspond to Eqs. ( 8) and (30) of [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF]. They depend on the source point location and on the domain geometry, and therefore must be numerically computed for each equation of the BEM discrete system and for each interior-point temperature evaluation requested by the user. For homogeneous media, Ã(ξ) = 1 and Â(ξ) = 1/2 at smooth boundary points (i.e the usual geometry-independent values are recovered as special cases) while of course all domain integrals vanish.

Illustrative numerical examples

In order to illustrate tha above considerations and have some quantitative idea of the approximate character of Eq. (3), two 2D examples are now considered.

The first example is analytical. We take k = (1 + x)(1 + y) and Ω = {0 ≤ x, y ≤ 2}. A solution to Eq. ( 1) is

T = (1 + x) 2 -(1 + y) 2 . One then finds k = (1 + x i )(1 + y i ) (i.e. constant) ∂ ∂r ( k -k) = (1 + y i ) cos θ + (1 + x i ) sin θ + 2r cos θ sin θ
To keep analytical calculations simple, we consider only source points on the horizontal median of Ω, i.e. such that y i = 1. After some calculations, one finds for such source points:

A(x i , 1) = 1 + 1 2π(1 + x i ) (2 -x i )θ 1 -x i θ 2 -Log 1 + x 2 i 5 -4x i + x 2 i (16) J(x i , 1) = 1 π(1 + x i ) 3(x i -1) + 3(2 -x i ) 2 θ 1 + (13 -11x i + 3x 2 i )θ 2 -(1 + x i )π + 1 2 Log 1 + x 2 i 5 -4x i + x 2 i ( 17
)
The functions A(x i , 1) and J(x i , 1) are plotted for 0 ≤ x ≤ 2 in Fig. 2, where J(x i , 1) is clearly nonzero. The source distribution D(x, ξ), shown in Fig. 3 for x i = 0.505, y i = 1.255, visibly assumes nonzero values outside the source point. The second example is numerical (it is Ex. 1 of [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF]). We take k = (1 + x/a) 3 and Ω = {0 ≤ x, y ≤ a}, for some length a. A solution to Eq. ( 1) is T = 4a 2 /(3(a + x) 2 ) (having dropped the factor T 0 = 100 and the additive constant). Here, one has k = k(ξ) + 3r 2 (x i + a)/(2a 3 ). The integral J(ξ) has been evaluated numerically (cutting the square domain into four triangles meeting at ξ, mapping each triangle onto a square and using a 200×200 point Gaussian quadrature rule on each subdomain). The values of J(ξ) for 0 < x i , y i < a, shown in Fig. 4, are clearly nonzero. For completeness, the values J(ξ) taken by J(ξ) using the homogeneous medium fundamental solution associated with the constant conductivity k(ξ) is depicted in Fig. 5. A numerical calculation gives: In other words, for this particular example, J(ξ) as a function of ξ is, in a L 2 -norm average sense, 0.367 times smaller than the domain integral J2 (ξ) encountered when using the 'best' homogeneous-medium fundamental solution.

Ω J 2 (ξ) dΩ(ξ) 1/2 ≈ 0.367 × Ω J2 (ξ) dΩ(ξ)

Conclusion

From the present analysis, our contention is that the approach proposed in [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF], contrarily to the claim made in that paper, does not lead to an integral equation without domain integrals. In particular, the integral equation, Eq. (10) of [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF], is found to be only approximately, not exactly, satisfied. The arguments detailed here for two-dimensional situations extend to three dimensions as well.

One may notice that equations (3) are not discussed or verified a posteriori in the developments of [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF]; they are treated as a priori requirements, then implicitly assumed to be satisfied by the proposed fundamental solution. Equations (3) are tested numerically in an example given in the end of the paper, but (i) the formulation is presented in [START_REF] Kassab | A generalized boundary integral solution for heat conduction problems in non-homogeneous media[END_REF] as an exact statement, which truth thus cannot established through numerical examples, and (ii) it has been pointed out above that such comparison can be made arbitrarily favorable by adjusting the value of the additive constant in T (x).

The comments made herein address only the mathematical exactness of the formulation being examined; they are not meant to imply or suggest that the latter is without merit as an approximation.

Figure 1 :

 1 Figure 1: Exclusion of the singular point ξ by a vanishing neighbourhood v ε .

1 Figure 2 :

 12 Figure 2: Example 1: variation of A(x i , 1) (dashed line) and J(x i , 1) (solid line).

Figure 3 :

 3 Figure 3: Example 1: forcing function D(x, ξ) for x i = 0.505, y i = 1.255 (horizontal units refer to a regular 50 × 50 grid used for the plot).

Figure 4 :

 4 Figure4: Example 2: variation of J(x i , 1) (horizontal units refer to a regular 50 × 50 grid used for the plot).

Figure 5 :

 5 Figure 5: Example 2: variation of J(x i , 1) (horizontal units refer to a regular 50 × 50 grid used for the plot).