Abbes -Albert Samy

Benveniste

Samy Abbes
email: samy.abbes@pps.jussieu.fr

Albert Benveniste
email: albert.benveniste@inria.fr

Concurrency, σ-algebras, and probabilistic fairness

Keywords: Probabilistic Petri nets, probabilistic event structures, trueconcurrency, probabilistic fairness Réseau de Petri probabiliste, concurrence vraie, équité probabiliste

We extend previous constructions of probabilities for a prime event structure E by allowing arbitrary confusion. Our study builds on results related to fairness in event structures that are of interest per se.

Executions of E are captured by the set Ω of maximal configurations. We show that the information collected by observing only fair executions of E is confined in some σ-algebra F 0 , contained in the Borel σ-algebra F of Ω. Equality F 0 = F holds when confusion is finite (formally, for the class of locally finite event structures), but inclusion F 0 ⊆ F is strict in general. We show the existence of an increasing chain F 0 ⊆ F 1 ⊆ F 2 ⊆ . . . of sub-σ-algebras of F that capture the information collected when observing executions of increasing unfairness. We show that, if the event structure unfolds a 1-safe net, then unfairness remains quantitatively bounded, that is, the above chain reaches F in finitely many steps.

The construction of probabilities typically relies on a Kolmogorov extension argument. Such arguments can achieve the construction of probabilities on the σ-algebra F 0 only, while one is interested in probabilities defined on the entire Borel σ-algebra F. We prove that, when the event structure unfolds a 1-safe net, then unfair executions all belong to some set of F 0 of zero probability. Whence F 0 = F modulo 0 always holds, whereas F 0 = F in general. This yields a new construction of Markovian probabilistic nets, carrying a natural interpretation that "unfair executions possess zero probability".

Introduction

The distinction between interleaving and partial orders semantics (also called true-concurrency semantics), has a deep impact when considering probabilistic aspects. In true-concurrency models, executions are modeled by traces or configurations, i.e., partial orders of events. Corresponding probabilistic models thus consist in randomizing maximal configurations, not firing sequences. It turns out that a central issue in developing true-concurrency probabilistic models is to localize choices made while the executions progress. In a previous work [START_REF] Abbes | Probabilistic models for true-concurrency: branching cells and distributed probabilities for event structures[END_REF][START_REF] Abbes | Probabilistic true-concurrency models: Markov nets and a Law of large numbers[END_REF], the authors have introduced branching cells, which dynamically localize choices along the progress of configurations. In this context, it is natural to introduce the class of locally finite event structures, in which each choice is causally connected to only finitely many other choices-as a particular case, every confusion free event structure is locally finite. In locally finite event structures, maximal configurations are tiled by branching cells. A recursive and non deterministic procedure allows to scan this set of tiling branching cells-of course, non determinism in the procedure is due to concurrency within the configuration. This tiling shows that every execution may be seen as a partial order of choices. Therefore, it is natural to proceed to the randomization of executions by randomizing local choices and imposing probabilistic independence to concurrent choices.

Although quite natural, the class of locally finite event structures is not general enough. Finite 1-safe nets may unfold to non locally finite event structures. Worse, the class of locally finite event structures is not stable under natural operations such as synchronization product. In this paper, to free our theory from external constraints on confusion, we consider general event structures with arbitrary confusion. We still try to build a coherent theory of choice for these, with applications to probabilistic event structures.

As a first contribution, we show that the branching cells that tile a configuration may require infinite ordinals greater than ω for their enumeration. We classify configurations according to their height, that is the number of limit ordinals greater than ω needed to enumerate the branching cells that tile the configuration-thus, for a locally finite event structure, all configurations have height zero. We show that, for event structures unfolding a finite 1-safe net, configurations have their height bounded by the number of transitions of the net. Configurations of strictly positive height turn out to exhibit lack of fairness. Thus our results provide an analysis of the structure of choice in relation with fairness in that the height of a configuration can be seen as a measure of its "unfairness degree".

A second contribution of our paper concerns the construction of probabilities for event structures with arbitrary confusion. When equipping concurrent systems with probabilities, the partial orders semantics attaches probabilities to partial orders of events, not to sequences. Randomizing an event structure is performed by equipping each "local zone" where a choice occurs with a local "routing" probability. Accordingly, local probabilities are attached to branching cells. An event structure is said to be probabilistic when a probability measure is attached to the space (Ω, F) of maximal configurations equipped with its Borel σ-algebra. For locally finite event structures, we have shown in [START_REF] Abbes | Probabilistic models for true-concurrency: branching cells and distributed probabilities for event structures[END_REF] that a Kolmogorov extension argument allows to infer the existence and uniqueness of a probability P on (Ω, F) coherent with a given family of local "routing" probabilities attached to branching cells-see also [START_REF] Varacca | Probabilistic event structures and domains[END_REF] for a similar result valid for confusion free event structures. For event structures with possibly infinite confusion, however, this construction is not sufficient, mainly because bracnhing cells do not entirely tile maximal configurations.

The novel idea of this paper is to introduce an increasing family F n of σ-algebras, where index n ranges over the set of all possible heights for configurations. F 0 captures the information obtained by observing only configurations of height 0 (the fair ones) and F n captures the information obtained by observing only configurations of height up to n. In particular, if the maximal height for configurations is finite and equal to N , then F N = F, the Borel σ-algebra-we show in this paper that this property holds for unfoldings of 1-safe nets.

The Kolmogorov extension argument always allows to construct a probability P 0 over F 0 . However, F 0 ⊆ F holds with strict inclusion unless the event structure is locally finite. The second important result of this paper consists in showing that, for Markovian probabilistic nets, "unfair executions have zero probability". Formally, we show that, for every Borel set A ∈ F, there exist two measurable sets B, B ′ ∈ F 0 such that B ⊆ A ⊆ B ′ and P 0 (B ′ -B) = 0. Consequently, P 0 extends trivially to the Borel σ-algebra F by adding to F 0 all zero probability sets. With these results we fill the gap that remained in our previous studies and therefore complete the landscape of true-concurrency probabilistic systems.

Related work. Our study of related work is structured according to the two contributions of this paper.

The first contribution is concerned with the structure of choice in prime event structures and nets. Confusion freeness and its variants have been extensively considered for Petri nets, particularly in the context of stochastic Petri nets [START_REF] Marsan | Modelling with generalized stochastic Petri nets[END_REF][START_REF] Baccelli | Stationary regime and stability of free-choice Petri nets[END_REF]. Regarding prime event structures, the notion of cell has been introduced by Varacca et al. in [START_REF] Varacca | Probabilistic event structures and domains[END_REF] as equivalence classes of the minimal conflict relation. For this construction to work, confusion-freeness of the event structure is required. Cells are minimal zones of the event structure where local choices occur. Independently, the authors of this paper have developed in [START_REF] Abbes | A projective formalism applied to topological and probabilistic event structures[END_REF][START_REF] Abbes | Probabilistic models for true-concurrency: branching cells and distributed probabilities for event structures[END_REF][START_REF] Abbes | Probabilistic true-concurrency models: Markov nets and a Law of large numbers[END_REF] the theory of locally finite event structures, in which confusion freeness is relaxed to kind of a "bounded confusion". Branching cells generalize cells in this context. They still represent zones of local choice. However, unlike cells in confusion free event structures, branching cells are dynamically defined in that they depend on the configuration enabling them. Local finiteness guarantees that branching cells are finite. Restricting ourselves to confusion free or locally finite event structures ensures that the structure of choice is "simple" enough. With the present paper, however, we show that the concept of local choice is valid and useful for general prime event structures and is still adequately captured by the notion of branching cell. Thus branching cells appear as the central concept when dealing with choice in general event structures. In addition, we have characterized fairness by means of the infinite ordinal needed when incrementally tiling configurations with branching cells.

The second contribution of this paper relates to probabilistic models for systems involving concurrency. The definition and specification of probabilistic systems can be done through process algebra techniques. Probabilistic process INRIA algebra allow to retain performance informations on a system while giving its specifications. According to the different modeling constraints, the definition of synchronization for probabilistic processes will differ. Several variants have thus been proposed, such as PCCS [START_REF] Jou | Equivalences, congruences and complete axiomatiozations of probabilistic processes[END_REF], TIPP [START_REF] Götz | Multiprocessor and distributed system design: the integration of functional specification and performance analysis using stochastic process algebras[END_REF], MPA [START_REF] Buchholz | Compositional analysis of a Markovian process algebra[END_REF], PEPA [START_REF] Hillston | A compositional approach to performance modelling[END_REF], or the κ-calculus [START_REF] Wilkinson | Stochastic modelling for systems biology[END_REF] developed for biological applications. The above theories have been developed in the framework of interleaving semantics, where a probability is assigned to a sequence of events once proper scheduling of nondeterministic choices has been performed. In contrast our work addresses the construction of true concurrency probabilistic models in which probabilities are assigned to partially ordered executions, not sequences.

In the context of interleavings probabilistic semantics, the main focus has been and remains on finding appropriate bisimulation relations for correctly testing and monitoring systems. The original probabilistic bisimulation relation from seminal paper [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF] has thus been extensively developed and generalized until recently [START_REF] Desharnais | Approximating labeled Markov processes[END_REF][START_REF] Danos | Labelled Markov processes: stronger and faster approximations[END_REF][START_REF] Danos | Bisimulation and cocongruence for probabilistic systems[END_REF]. As an instance of this series of developments, in [START_REF] Danos | Labelled Markov processes: stronger and faster approximations[END_REF] simulation relations as well as approximations are studied, relying on techniques of σ-algebras and conditional expectations. The objective is to approximate the state space by a possibly non-injective labeling of its states, thus giving raise to a sub-σ-algebra. Our present work also makes use of σ-algebras but in a totally different way. Our σ-algebras are not attached to the state space but rather to the space of trajectories (i.e., the maximal configurations) and they capture the increasing flow of information gathered while observing the system. Our objectives are not to obtain simulation relations but rather 1/ to develop the bases needed to equip prime structures with probabilities with no restriction, and 2/ to further study their properties when the event structure originates from a 1-safe net (thus yielding Markov nets), and 3/ to carry over to Markov nets the fundamental and highly powerful statistical apparatus attached to infinite behaviours (Law of Large numbers, Central Limit Theorem, etc.). In this paper we address issues 1 and 2; the reader is referred to [START_REF] Abbes | Probabilistic true-concurrency models: Markov nets and a Law of large numbers[END_REF] for issue 3. Note that the present work shows that the ergodic results of [START_REF] Abbes | Probabilistic true-concurrency models: Markov nets and a Law of large numbers[END_REF] also hold without the local finiteness assumption.

Organization of the paper. The paper is organized as follows. Section 1 quickly reviews the decomposition of event structures through branching cells, and recalls the probabilistic construction for locally finite event structures. A generalized induction is introduced in 2, to deal with choices in case of infinite confusion. Probabilistic applications are given in 3. Finally, 4 discusses further research perspectives. Appendix A collects omitted proofs.

Background on Probability and Concurrency

We first describe how choices may be distributed on simple examples of nets. We explain in the same way the randomization that comes with the decomposition of choices.

Branching cells by example.

We recall the construction of branching cells through examples. Formal definitions and results will also be given. Branching cells are best understood in ?>=< 89:; ?>=< 89:; the case of a finite event structure. In a sense, local finiteness is just the most natural extension of the finite case. Consider thus the net N 1 depicted in Figure 1, top left, and its (quite trivial) unfolding event structure E 1 depicted on bottom left. Remember that we randomize maximal configurations of unfoldings, hence the space to be randomized here is simply the set with two elements Ω 1 = {(ac), (b)}, where we note (ac) for the configuration with events a and c, the order between a and c being of no importance. Note that, although a and c are concurrent events, they are not independent. On the contrary, their occurrences are strongly correlated, since any maximal configuration ω 1 has the following property: a ∈ ω 1 if and only if c ∈ ω 1 . Obviously, the set Ω 1 with 2 elements cannot be further decomposed; this shows that concurrency and independence are distinct notions. This also shows that choices, here between (ac) or (b), are not supported by transitions, places or events of nets or event structures. Here, the event structure must be considered as a whole. We shall therefore randomize N 1 by means of a finite probability µ 1 , i.e., two non-negative numbers µ 1 (ac) and µ 1 (b) such that

g g × × × × × × a U U U U U U b y y c ?>=< 89:; U U U U U U g g × × × × × × • ?>=< 89:; U U U U U U g g × × × × ×
U U U U U U g g × × × × × × • • G o G o G o a • G o G o G o b • c • G o G o G o d • e
µ 1 (ac) + µ 1 (b) = 1.
In the same way, consider also the net N 2 depicted on the right column of Figure 1, top, and its event structure equivalent E 2 depicted at bottom-right. Here, the set to be randomized is Ω 2 = {(d), (e)}, so we are given a probability

µ 2 on Ω 2 : µ 2 (d) + µ 2 (e) = 1.
Consider now the net N ′ consisting of the two above nets N 1 and N 2 put side by side-mentally erase the vertical rule of Fig. 1 to get the picture of net N ′ . The corresponding event structure, say E ′ , has the property that any event in E 1 is concurrent and independent of any event in E 2 . To verify this, just observe that the occurrence of any event in E 1 is compatible with the occurrence of any event in E 2 ; and vice versa. Hence N 1 and N 2 , being atomic units of choice, are the branching cells that form net N ′ . As a consequence, the set Ω ′ of maximal configurations of N ′ has the natural product decomposition Ω ′ = Ω 1 ×Ω 2 . It is thus natural to consider the product probability µ ′ = µ 1 ⊗µ 2 on Ω ′ . Hence, for instance, the probability of firing a, c and d is given by µ ′ (acd) = µ 1 (ac) × µ 2 (d). Observe the application here of the principle of correspondence between concurrency and probabilistic independence-see [START_REF] Abbes | Probabilistic models for true-concurrency: branching cells and distributed probabilities for event structures[END_REF][START_REF] Abbes | Probabilistic true-concurrency models: Markov nets and a Law of large numbers[END_REF] for a discussion of this idea.

It remains to continue the construction in case of synchronisation. For this, consider the net N depicted on the top line of Figure 2, with the event structure equivalent E on the right. Observe that net N ′ , itself composed of N 1 and N stands as the "beginning" of net N . We already know how to randomize events that occur in the N ′ area of N , thanks to the product decomposition of N ′ . What happens "next" will be randomized by a classical conditioning process. Let for instance the probability of executing maximal configuration ω = (ac d gi) to be computed. The prefix of ω in N ′ is v = (ac d). Since we know already the probability of execution of v = (ac d) in N ′ , we consider the system after configuration v. Hence we delete from N all transitions that either have already been fired during the execution of v, or either that are now unable to fire. The resulting net is depicted on bottom left of Figure 2-in the event structure model, we would call it the future E v of v, to be detailed below in 1.2. We now start again the analysis we made in the beginning, and realize that f , g, h and i being correlated, they belong to a same third branching cell, say N 3 , or E 3 in the event structure model, and we shall consider a third probability distribution µ 3 on the set Ω 3 of maximal configurations of E 3 . Hence, if µ denotes the global probability on the set Ω of maximal configurations of E, we get that µ(ac d gi) = µ 1 (ac) × µ 2 (d) × µ 3 (gi). Now assume that w = (ace) had fired instead of (ade). Erasing events incompatible with w only leave events f and g (see the result on bottom right of Figure 2). Hence f and g are now still two competing events, but they do not compete in the same context than previously. We have to consider they form a fourth branching cell, to which we attach a fourth probability distribution µ 4 on associated set Ω 4 = {(f ), (g)} of maximal configurations. We would have for instance µ(ac d f ) = µ 1 (ac) × µ 2 (d) × µ 4 (f ). Since a same event, here f or g, may appear in different branching cells according to the context brought by the configuration, we say that the decomposition of configurations through branching cells is dynamic. It is part of the theory that the function µ for which we have explained the construction does indeed sum up to 1 over the set Ω of maximal configurations of E-a fact that can be easily checked by hand on this example. So far for the example, let us formalise the construction.

j j f f f f f f b b | • G o G o G o a } X z V x T v R t I q G o E m B j @ h 8 f 6 d 3 f • G o G o G o g • G o G o G o h • i • G o G o G o a • G o G o G o b • V V V V V V V V V y y g g Ö Ö Ö Ö Ö Ö Ö Ö Ö c • G o G o G o y y g g Ö Ö Ö Ö Ö Ö Ö Ö Ö d • e ?>=<
1.2 Formalisation: stopping prefixes and branching cells.

We refer to the research report [START_REF] Abbes | Concurrency, σ-algebras and probabilistic fairness[END_REF] and to our original publications [START_REF] Abbes | Branching cells as local states for event structrues and nets: probabilistic applications[END_REF][START_REF] Abbes | Probabilistic models for true-concurrency: branching cells and distributed probabilities for event structures[END_REF] for the detailed construction and properties of branching cells. Here we will recall some essential definitions.

Recall that the relation # µ of minimal conflict has been defined by several authors for an event structure (E, ≤, #) as follows:

∀x, y ∈ E, x# µ y ⇐⇒ (↓ x× ↓ y) ∩ # = {(x, y)},
where ↓ x = {e ∈ E : e ≤ x} represents the set of predecessors of event x. Define a stopping prefix of event structure E as a subset B ⊆ E such that:

1. B is downward closed: ∀x ∈ B, ∀y ∈ E, y ≤ x ⇒ y ∈ B; 2. B is # µ -closed: ∀x ∈ B, ∀y ∈ E, y# µ x ⇒ y ∈ B.
Stopping prefixes of E form a complete lattice with ∅ and E as minimal and maximal elements. Say that a stopping prefix is initial if it is minimal among non empty stopping prefixes. In the above example depicted in Fig. 2,E 1 and E 2 were the two initial prefixes of E. Any event structure may not have an initial stopping prefix-see the research report [START_REF] Abbes | Concurrency, σ-algebras and probabilistic fairness[END_REF] for an example of event structure without initial stopping prefix. However if E is the non empty unfolding of a finite Petri net, then any stopping prefix B of E contains an initial stopping prefix-in particular, E itself contains initial stopping prefixes. This is a particular case of the following result:

Theorem 1 Let E be a non empty event structure with the following property: there is a constant K ≥ 0 such that, for any finite configuration v of E, at most K events e ∈ E \ v are such that v ∪ {e} is a configuration. Then for every nonempty stopping prefix B of E, there is an initial stopping prefix A ⊆ B.

We will always consider event structures satisfying the assumption of Theorem 1, even if it is not explicitly formulated.

Finally, if v is a configuration of E (that is, a subset of E downward closed and conflict free), we define the future E v of v in E as the following sub-event structure of E:

E v = {e ∈ E : e is compatible with v} \ v.
If z is a configuration of E v , then the set-theoretic union v ∪ z is a configuration of E, that we denote v ⊕ z to emphasize that we form the concatenation of v and z.

Consider the following recursive construction:

1. Pick an initial stopping prefix of E, pick a maximal configuration x 0 in it, and consider the future E x0 ;

2. Pick an initial stopping prefix of E x0 , pick a maximal configuration x 1 in it, and consider the future E x0⊕x1 ;

3. And so on.

INRIA

Any configuration that can be obtained as some x 0 ⊕ . . . ⊕ x n as in the above construction, or as an increasing union of such, we call a stopped configuration of E. 1 A configuration obtained as some x 0 ⊕. . .⊕x n as in the above construction is called finitely stopped. The reader that would not know about branching cells is encouraged to apply this construction to the previous examples.

The several initial stopping prefixes of nested event structures that appear in the decomposition of some stopped configuration v are called the branching cells in the decomposition of v. Although there is range for non determinism in the decomposition of stopped configurations, it is a result that branching cells encountered in the decomposition of some stopped configuration v only depend on v. Branching cells are thus intrinsic to stopped configurations. We denote by ∆(v) the set of branching cells that occur in the decomposition of any stopped configuration v. If v is a finitely stopped configuration, any initial stopping prefix of E v is called a branching cell enabled at v.

Specializing to the case where E is the unfolding of some finite 1-safe net, it is easy to realize in this case that branching cells of E are finitely many, up to isomorphism of labeled event structures-the labeling originates of course from the unfolding structure. Furthermore, the isomorphism of labelled event structures between isomorphic branching cells is unique. If N is the net being unfolded, we say that the isomorphism classes of branching cells of E are the local states of N . We use the generic notation x to denote local states of nets.

The case of locally finite event structures and Markov nets.

Additional properties of branching cells hold if the event structure satisfies the following property: any event e ∈ E belongs to some finite stopping prefix of E.

In that case, event structure E is said to be locally finite [START_REF] Abbes | Branching cells as local states for event structrues and nets: probabilistic applications[END_REF][START_REF] Abbes | Probabilistic models for true-concurrency: branching cells and distributed probabilities for event structures[END_REF]. In the remaining of this paragraph, we consider a locally finite event structure E, maybe originating from the unfolding of a 1-safe Petri net. The first property is that any branching cell is finite. Furthermore, any maximal configuration of E is stopped. We will give an interpretation of the latter fact through σ-algebras in a next section [START_REF] Abbes | A projective formalism applied to topological and probabilistic event structures[END_REF].

The next steps forward to get to the randomization of locally finite event structures are the following-the following definition of a probabilistic event structure is general, and does not require E to be locally finite. We denote by Ω E the set of maximal configurations of event structure E-this set is always non empty. The Borel σ-algebra on E is the σ-algebra generated by subsets of the form

↑ v = {ω ∈ Ω : v ⊆ ω},
for v ranging over the finite configurations of E. We denote by F the Borel σ-algebra on Ω E . We say the event structure E is probabilistic if we are given a probability measure P on the measurable space (Ω E , F). Next, consider for each branching cell x of E the set Ω x of maximal configurations of x, and a finite probability distribution p x on Ω x . Then define the following function p, for v ranging over the set of finitely stopped configurations of E:

p(v) = x∈∆(v) p x (v ∩ x), (1)
where we recall that ∆(v) denotes the set of branching cells involved in the decomposition of v. Then v ∩ x belongs to Ω x , and thus the finite product above is well defined. It is a result that there is a unique probability measure P on (Ω, F) such that P(↑ v) = p(v) for any finitely stopped configuration v [START_REF] Abbes | Branching cells as local states for event structrues and nets: probabilistic applications[END_REF][START_REF] Abbes | Probabilistic models for true-concurrency: branching cells and distributed probabilities for event structures[END_REF]. This result makes use of the local finiteness assumption, the crucial point being that maximal configurations of E are stopped. Assume, furthermore, that the locally finite event structure E is the unfolding of some 1-safe net N . Then we require the family (p x ) x to satisfy the following additional property: if x and x ′ are isomorphic branching cells, then so are p x and p x ′ . Formally, p x ′ (ω ′ ) = p x (ω), where ω is an arbitrary maximal configuration of x, ω ′ = x,x ′ (ω), and φ x,x ′ is the unique isomorphism of labelled event structures from x to x ′ . Let x denote the local state associated with x and x ′ . Since φ x,x ′ is unique, it makes sense to consider the set Ω x of maximal configurations of x, and the probability distribution p x attached to it, derived from the various p x 's. Such a p x is called a local transition probability.

According to the previous result, the (finite) family of local transition probabilities defines a unique probability measure P on the space (Ω, F). Call Markov net a net equipped with such a probability measure. Markovian and ergodic properties of Markov nets were studied in [START_REF] Abbes | A (true) concurrent Markov property and some applications to Markov nets[END_REF][START_REF] Abbes | Probabilistic true-concurrency models: Markov nets and a Law of large numbers[END_REF].

The aim of this paper is to generalise the above construction to an arbitrary 1-safe net, without the local finiteness assumption.

Non locally Finite Unfoldings and the Height of Nets

In this section we introduce a new notion of height for nets, which formalizes our informal discussion in the introduction regarding fairness. Let us first analyze non locally finite unfoldings on an example. Let N be the 1-safe net depicted in Fig. 3, top. The unfolding E of N is depicted in bottom-left. Events a i , b i and c i , for i = 1, 2, . . . , are respectively labeled by transitions a, b and c. Events named d, e and f are labeled by transitions d, e and f respectively. E has a unique initial stopping prefix, namely x 1 = {a 1 , b 1 }. Observe that the smallest stopping prefix that contains d is E \ {e, f }, since d# µ c i for all i = 1, 2, . . . , and thus E is not locally finite. The finitely stopped configurations associated with x 1 are (a 1 ) and (b 1 ). Now the future E (b1) is depicted in Fig. 3, bottom-right. It contains the two branching cells {c 1 , d} and {e, f }. On the other hand, the future E (a1) is isomorphic to E. Repeating this process, we find all stopped configurations of E. We describe them as follows: let r 0 = ∅, and

r n = a 1 ⊕ • • • ⊕ a n , for n = 1, 2, . . . . Putting s n = r n-1 ⊕ b n for n ≥ 1,
stopped configurations containing b n must belong to the following list:

s n , s n ⊕ c n , s n ⊕ d, s n ⊕ d ⊕ e, s n ⊕ d ⊕ f, n ≥ 1 . (2)
All stopped configurations are those listed in (2), plus all r n for n ≥ 0, and finally the infinite configuration a ∞ = (a 1 , a 2 , . . . ). Branching cells are computed accordingly. They belong to the following list:

x n = {a n , b n }, x ′ n = {c n , d}, n ≥ 1, or x ′′ = {e, f }.
This shows in passing that branching cells can be all finite without E being locally finite. On the other hand, the set Ω E of maximal INRIA ?>=< 89:; 8 8 w w w w w w w w V V q q q q q q q q b G G c ?>=< 89:; G G f ?>=< 89:; ?>=< 89:;

V V q q q q q q q q 8 8 w w w w w w w w • ?>=< 89:;

V V q q q q q q q q 8 8 w w w w w w w w • a G G d ?>=< 89:; G G e e Ò Ò Ò Ò Ò Ò Ò Ò Ò Ò G G e ?>=< 89:; . . . . . . • . . . c 3 • y y e e Ó Ó Ó Ó Ó Ó Ó Ó G o G o G o a 3 • e e Ó Ó Ó Ó Ó Ó Ó Ó b 3 • c 2 • y y c c G o G o G o a 2 • c c b 2 • c 1 • G o G o G o e • f • y y c c G o G o G o a 1 • c c b 1
• y y c c g 9 g 9 g 9 g 9 g 9 g 9 g 9 g 9 configurations is described by:

0 0 0 0 0 0 0 0 0 0 0 % % % % % % % % % % % % % % % % " " " " " " " " " " " " " " " " " " " " d • G o G o G o G o e • f • G o G o G o G o c 1 • Q Q Q Q Q Q i i d
Ω E = a ∞ ⊕ d ⊕ e, a ∞ ⊕ d ⊕ f ∪ s n ⊕ c n , s n ⊕ d ⊕ e, s n ⊕ d ⊕ f, n ≥ 1 .
As a consequence, a ∞ ⊕ d ⊕ e and a ∞ ⊕ d ⊕ f are two maximal configurations that are not stopped. This contrasts with the case of locally finite unfoldings, as we mentioned above.

We may however reach the missing maximal configurations ω e = a ∞ ⊕ d ⊕ e and ω f = a ∞ ⊕ d ⊕ f by a transfinite recursion. Indeed, a ∞ is a stopped configuration of E. Its future is the simple event structure with 3 elements d e, d f , and e#f . E a∞ has two branching cells, namely {d} and {e, f }. Hence if we authorize to perform concatenation, not only with finitely stopped configurations as left-concatenated element, but also on stopped configurations such as a ∞ , we reach more configurations. In this example, in one additional step, we reach the missing elements ω e and ω f of Ω E . We formalize and extend the above discussion in a general context next.

Let E be the unfolding of a 1-safe net N . We set X -1 = {∅}, and we define inductively:

for n ≥ 0, X n = u ⊕ v : u ∈ X n-1 , and v is stopped in E u .
It follows from this definition that X n-1 ⊆ X n for all n ≥ 0, and that X 0 is the set of stopped configurations of E. Then we define a non-decreasing sequence of associated σ-algebras of Ω E as follows: For n ≥ 0, F n is the σ-algebra generated by arbitrary unions of subsets of the form ↑ (u⊕v), with u ∈ X n-1 and v finitely stopped in E u . Then F n ⊆ F n+1 for all n ≥ 0 since X n ⊆ X n+1 . In case of locally finite unfoldings, we have the following:

Proposition 1 If E is locally finite, then F = F 0 .
Example 1 That F = F 0 is not true in general. For instance, in the above example of Figure 3

, consider A =↑ (a ∞ ⊕ d ⊕ f ). Then A / ∈ F 0 . Indeed, considering the σ-algebra G = {↑ a ∞ ∩ K, K ∈ F 0 }, the description that we gave of finitely stopped configurations shows that G = {∅, ↑ a ∞ }. This implies that A / ∈ F 0 .
The following result generalizes the observation made on the above example: maximal configurations are reached after a finite number of (infinite) steps.

Theorem 2 Let N be a 1-safe net with p transitions. Let E be the unfolding of N , and construct as above the sequences (X n ) n and (F n ) n . Then Ω E ⊆ X p and F ⊆ F p+1 .

Definition 1 (height) The height of a maximal configuration ω ∈ Ω E is the smallest integer q such that ω ∈ X q . The height of a 1-safe net is the smallest integer q such that Ω E ⊆ X q .

Theorem 2 says that 1-safe nets have finite height, less than the number of transitions. Nets with locally finite unfoldings have height 0, although all nets of height 0 need not to have a locally finite unfolding, as shown by the following example. Consider the net depicted on Figure 4, left. It is of height 0, but its unfolding is not locally finite. Indeed, we depict at right on Fig. 4 a prefix of the (unique and infinite) initial stopping prefix x 0 of its unfolding. Branching cell x 0 consists of all events a n , b m and c n,m for n, m ≥ 1. To get the entire unfolding, add a fresh copy of x 0 after each event c i,j , i, j ≥ 1, and continue recursively. Maximal configurations of x 0 have the form ω n,m = a 1 ⊕• • •⊕a n ⊕b 1 ⊕. . . b m ⊕c n+1,m+1 , with n, m ≥ 0, or ω ∞ = a 1 ⊕b 1 ⊕a 2 ⊕b 2 ⊕. . . . Any maximal configuration ω of the unfolding is a finite concatenation of ω n,m 's, ended with a ω ∞ , or an infinite concatenation of ω n,m 's. This net has therefore height zero.

Application to the Construction of Probabilistic Nets

From the result on σ-algebras stated in Th. 2, one may wish to construct a probability measure on (Ω E , F) by using recursively and finitely many times formula [START_REF] Abbes | A (true) concurrent Markov property and some applications to Markov nets[END_REF]. For locally finite unfoldings, such a construction amounts to taking a projective limit of measures (see [START_REF] Abbes | A projective formalism applied to topological and probabilistic event structures[END_REF]). We thus want to take nested projective limits of measures. Although this procedure would apply to any event structure (satisfying the hypotheses of Th. 1), considering unfoldings of nets brings a surprising simplification.

INRIA

?>=< 89:;

Ô Ô & & R R R R R R R • ?>=< 89:; Ô Ô & & R R R R R R R • X X a x x c d d b • G G 5 5 q q q q q q q " " E E E E E E E E E E E E E E E E @ @
@ @ @ @ @ @ @ @ @ @ @ @ @ @ @ @ @ @ @ @ @ @ @

b 1 • G G 5 5 q q q q q q q " " E E E E E E E E E E E E E E E E b 2 • b 3 • Y { Y { Y { Y { { Y { Y { Y { Y c 1,1 • Y { Y { Y { Y { s Q s Q s Q s Q s Q s Q s Q s Q s Q s Q s Q s Q s Q c 1,2
• q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I

Y { Y { Y { Y { c 1,3 • 5 5 q q q q q q q C C E E a 1 • r Ø r Ø r Ø r Ø r Ø r Ø r Ø r Ø r Ø r Ø { Y { Y { Y { Y c 2,1 • r Ø r Ø r Ø r Ø r Ø r Ø r Ø r Ø r Ø r Ø s Q s Q s Q s Q s Q s Q s Q s Q s Q s Q s Q s Q s Q c 2,2
• q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I q I

r Ø r Ø r Ø r Ø r Ø r Ø r Ø r Ø r Ø r Ø c 2,3
have infinitely many chances to enable local state x ′ but never do, and thus they have probability zero. This is of course an expected result-see, e.g., [START_REF] Alfaro | From fairness to chance[END_REF] for an account on probabilistic fairness. We shall now see that this situation is indeed general, for Markov nets.

Markov Nets of First Order.

The first result we have is the following:

Theorem 3 Let N be a 1-safe net, and let µ x be a local transition probability for every local state x of N . For each finitely stopped configuration v, let p(v) be defined by:

p(v) = x∈∆(v) µ x (v ∩ x) , (3)
where x denotes the isomorphism class of branching cell x. Then there is a unique probability measure P 0 on (Ω E , F 0 ) such that P 0 ↑ v = p(v) for all finitely stopped configurations v. The pair (N , (µ x ) x ), where x ranges over the set of all local states of N , is called a Markov net of first order.

Comment-The above theorem is formulated only for the case where each local state x has the property that Ω x is at most of countable cardinality. We use it for simplicity. For the general case we would need to consider subsets of the form ↑ x z := {w ∈ Ω x : z ⊆ w}, for z ranging over the finite configurations of x, instead of the mere singletons {v ∩ x}.

Observe the difference with the result stated in 1.3 for nets with locally finite unfoldings. The probability constructed in Th. 3 is defined only on F 0 , and cannot measure in general all Borel subsets. We will see that this is actually not a restriction (see Th. 4 below). In case E is locally finite, we see that both constructions of probability are the same, since F = F 0 by Prop. 1, and since formula (1) and ( 3) are the same.

Completion of Markov Nets of First Order to Markov

Nets.

We now formalize the result observed on the example above ( 3.1), that there is "no room left" for maximal configurations ω not in X 0 . For this we use the notions of complete and of completed σ-algebras. Define first the symmetric difference A△A ′ between two sets A and A ′ by

A△A ′ = (A \ A ′ ) ∪ (A ′ \ A).
Let (Ω, F, P) be a probability space. Say that a subset A ⊆ Ω is P-negligible (or simply negligible if no confusion can occur) if there is a subset A ′ ∈ F such that A ⊆ A ′ and P(A ′ ) = 0. Remark that, in this definition, A is not required to be in F. The σ-algebra F is said to be complete if F contains all P-negligible subsets.

For any σ-algebra F, a σ-algebra H is said to be a completion of F (w.r.t. P) if H is complete, and if for every A ′ ∈ H, there is a A ∈ F such that A△A ′ is negligible. It is well known that every σ-algebra F has a unique completion, which is called the completed σ-algebra of F [START_REF] Breiman | Probability. SIAM[END_REF].

Theorem 4 Let N and (µ x ) x define a Markov net of first order. We assume that µ x (↑ y) > 0 for any local state x and for any finite configuration y of x.

INRIA

Let P 0 be the probability on (Ω E , F 0 ) constructed as in Th. 3, and let H be the completed σ-algebra of F 0 . Then F ⊆ H, and thus P 0 extends to a unique probability P on (Ω E , F), where F is the Borel σ-algebra of Ω E .

Comment-The case when F 0 = F brings an obstruction to a purely topological or combinatorial construction of the probability P on F. A detailed reading of the proof reveals that our construction indeed combines combinatorial arguments (the height) with measure theoretic tools (the Borel-Cantelli lemma).

Conclusion

We have shown how to define and construct probabilistic Petri nets for 1-safe net with arbitrary confusion. The basic idea is that choice is supported by the notion of branching cells, so independent dices can be attached to each branching cell in order to draw maximal configurations at random.

Whereas a countable sequence of drawings is enough for nets with locally finite unfolding, a transfinite induction is needed in the more general case. Surprisingly enough, for Markov nets, this transfinite induction is actually not required.

Limitations of this approach are encountered when we try to construct effective local transition probabilities. Although nets with non locally finite unfoldings can have finite branching cells, we face in general the case of infinite branching cells x, with associated spaces Ω x being infinite also. Worst is when Ω x is not countable. We hope that such more difficult cases can be reached by regarding them as products of simpler probabilistic nets. Composition of true-concurrent probabilistic processes is a field that we currently explore. assumption of the theorem to configuration ∅ yields that E has at most K minimal events. This is a contradiction, and therefore C = ∅.

Zorn's lemma implies then that H has a minimal element, which is the result required.

Proof of of Prop. 1. Assume E is locally finite. Then finitely stopped configurations are finite, so the generators of F 0 are Scott-open and thus F 0 ⊆ F. To show that F ⊆ F 0 , it is enough to show that ↑ v ∈ F 0 for every finite configuration v, since the collection of such ↑ v constitute a basis of open sets of the Scott topology on Ω E . Thus let v be a finite configuration. There is a finite stopping prefix B that contains v. Now ↑ v = ωB ∈ΩB , ωB ⊇v ↑ ω B by Lemma 2. It is shown in [START_REF] Abbes | Probabilistic models for true-concurrency: branching cells and distributed probabilities for event structures[END_REF] that any ω B ∈ Ω B with B finite is finitely stopped. Hence the above finite union shows that ↑ v ∈ F 0 , and thus F ⊆ F 0 .

Proof of of Th. 2. We first show by induction on p that Ω E ⊆ X p . This is trivial for p = 1; assume it holds until p -1, and let N be a net with p transitions. Let ω ∈ Ω E , and we show that ω ∈ X p . We may assume that ω / ∈ X 0 , otherwise we are done. We claim that there is an infinite stopped configuration v with v ⊆ ω. Indeed, take v as the supremum of stopped configurations subset of ω. Then v is stopped thanks to the results of [START_REF] Abbes | Probabilistic models for true-concurrency: branching cells and distributed probabilities for event structures[END_REF]. Assume that v is finite. Then, in particular, v is finitely stopped. Hence v = ω, otherwise ω would be stopped, which is excluded. Therefore E v is nonempty. Theorem 1 implies that E v has an initial stopping prefix, say x. Then, ω \ v is maximal in E v , and thus by Lemma 2, z = (ω \ v) ∩ x is maximal in x. In particular z = ∅, since z is maximal in the nonempty event structure x. But then v ⊕ z is finitely stopped, subset of ω, and strictly larger than v, which contradicts the definition of v. This contradiction shows that v is infinite, as we claimed.

Put w = ω \ v. Then w is a maximal configuration of the future E v . But, since v is infinite, Lemma 1 says that E v is the unfolding of a subnet of N with a number of transitions at most p -1. Hence, by the induction hypothesis applied to this subnet, we have w ∈ X v p-1 , with the obvious notation X v p-1 associated to E v . There is thus a sequence

w 0 ⊆ • • • ⊆ w k = w with k ≤ p -1, w i ∈ X v i and w i \ w i-1 stopped in (E v ) wi-1 for i = 1, . . . , k. It is readily checked that (E v ) wi = E v⊕wi . Hence the sequence v ⊆ v ⊕ w 1 , ⊆ • • • ⊆ v ⊕ w k = ω shows that ω ∈ X p . This shows that Ω E ⊆ X p .
We now show that F ⊆ F p+1 . By the same argument used in the proof of Prop. 1, it is enough to show that ↑ v ∈ F p+1 for every finite configuration v. Hence let v be a finite configuration. For each ω ∈↑ v, let Q v (ω) be the configuration defined by Q v (ω) = inf{w ∈ X p : v ⊆ w ⊆ ω}. This subset is nonempty since Ω E ⊆ X p , thus the infimum defining Q v (ω) is well defined. Moreover we see by induction on p, using again that compatible stopped configurations form a complete lattice ( [START_REF] Abbes | Probabilistic models for true-concurrency: branching cells and distributed probabilities for event structures[END_REF]), that Q v (ω) ∈ X p . We have thus:

↑ v = w0∈Xp ,w0⊇v Q -1 v (w 0 ) . (4)
It follows from properties of branching cells that, if w 0 is a configuration such that w 4) is either empty or a subset of the form ↑ w 0 , with w 0 ∈ X p . By definition of F p+1 , this implies that ↑ v ∈ F p+1 , and completes the proof.

0 = Q v (ω 0 ) for ω 0 ∈↑ v, then Q -1 v (w 0 ) =↑ w 0 . Hence each Q -1 v (w 0 ) INRIA in (
We only sketch the proof of Th. 3, since it does not contain any significantly new idea.

Proof of Th. 3. Consider the so-called normal decomposition of maximal configurations introduced in [6, 4.4]. This defines a sequence of F 0 -measurable mappings π n : Ω E → X 0 . Observe that the σ-algebra generated by the π n , n ≥ 1, is F 0 . Then apply Kolmogorov extension theorem to conclude.

Proof of Th. 4 using Lemma 3 below. Let v be any finite configuration of the unfolding E. According to Lemma 3 below, P 0 -a.s. every ω ∈↑ v satisfies ω = V (ω). Therefore we have, up to P 0 -negligible sets:

↑ v = {ω ∈ Ω E : v ⊆ V (ω)} .
It is readily seen that the σ-algebra V generated by V seen as a random variable coincides with F 0 . Hence ↑ v is F 0 -measurable up to a P 0 -negligible set. This shows that F ⊆ H, as required.

As it is easily seen from the above proof, the essential ingredient lies in Lemma 3 below. We need to introduce a couple of tools for its proof. First define the max-initial stopping prefix of an event structure E, as the union of all initial branching cells of E. Denote it by B 0 (E). Then define inductively, for each maximal configuration ω ∈ Ω E the sequence π n (ω) of configurations as follows:

π 0 (ω) = ∅, n ≥ 0, π n+1 (ω) = π n (ω) ⊕ ω ∩ B 0 (E πn(ω) ) . ( 5
)
If E is locally finite, then we have ω = n≥0 π n (ω) for any ω ∈ Ω E . But in general we only have n≥0 π n (ω) ⊆ ω, and this inclusion may very well be strict. Our goal however is to show that the strict inclusion is a rare event, in the probabilistic sense. To formulate our results more concisely, we introduce the following notation:

∀ω ∈ Ω E , V (ω) = n≥0 π n (ω) .
Lemma 3 Let N and (µ x ) x define a Markov net of first order. We assume that µ x (↑ y) > 0 for any local state x and for any finite configuration y of x. Then the equality V (ω) = ω holds for P 0 -a.s. every ω ∈ Ω E .

Proof of Lemma 3. Let ω ∈ Ω E be such that ω = V (ω). Then there is an event e ∈ E compatible with V (ω), and such that e ∈ V (ω). In other words, we have that e ∈ E V (ω) . Clearly, event e is not in any branching cell in the covering ∆ E (π k (ω)), for k ≥ 0. For any integer k ≥ 0, pick a finite configuration v k of E π k (ω) as in Lemma 4, so that e, as an event of the event structure E π k (ω) , belongs to some branching cell in the covering ∆ E π k (ω) (w) for any stopped configuration w of E π k (ω) with v k ⊆ w. It is a consequence of Lemma 1 that event structures E π k (ω) are finitely many up to isomorphism of labeled event structures. Accordingly, we chose the configurations v k such that they are finitely many up to isomorphism of labeled event structures.

Thanks to our assumption on the probability measures µ x , and by inspecting formula (3) that defines P 0 , we have that P 0 (V (ω) ∈ ↑ v) > 0 for any finite configuration v that can be expressed as concatenation of finite configurations in successive branching cells. Furthermore, the very same formula shows that conditioning the probability P 0 on {V (ω) ∈ ↑ v}, for any stopped configuration v, is equivalent to considering the probability P v 0 on Ω E v constructed by Th. 3 in event structure E v .

Therefore for any integer k ≥ 0, and since configuration v k is finite, there is a real number α k > 0 such that:

P π k (ω) 0 (V (ξ) ∈ ↑ v k ) ≥ α k , (6)
where ξ denotes a generic element of Ω E π k (ω) . But we also have, for the ω ∈ Ω E we have chosen:

V (ω \ π k (ω)) ∈ ↑ v k . (7)
Indeed, otherwise e would be in some branching cell in the covering ∆ V (ω) . Since configurations v k have been chosen among finitely many classes up to isomorphism, we choose α > 0 such that α k ≥ α for all k ≥ 0. Now, using the multiplicative form of P 0 given by formula (3), the P 0 -probability of the statement of Eq. ( 7) to hold N times is less that (1α) N for any integer N ≥ 1. Finally, the P 0 -probability of Eq. ( 7) to hold infinitely often is zero. The above construction was done for any ω ∈ Ω E such that ω = V (ω). It relies only on the existence of the event e chosen at the beginning. Since such events are countable many, the measurable set ω ∈ Ω E : ω = V (ω) appears as a countable union of measurable sets, each of them being of probability zero. Therefore, the conclusion P 0 ω = V (ω) = 0 holds. The proof of Lemma 3 was based on the following result that only concerns event structures and does not involve probabilities.

Lemma 4 Let e be any event in event structure E. Then there is a branching cell x with e ∈ x, and a finite configuration v such that, for any stopped configuration w, we have:

v ⊆ w ⇒ x ∈ ∆(w),
where we recall that ∆(w) denotes the set of branching cells involved in the decomposition of w.

Proof of Lemma 4. We assume first that e is a minimal event of E. If e belongs to some initial branching cell y, then we can take x = y and v =↓ e.

If not, consider the smallest stopping prefix B such that e ∈ B. Such a B exists since stopping prefixes of E form a complete lattice. Denoting by ⊳ the immediate causal successor relation, we see that B consists of all events that can be obtained by forming finite chains of events starting from e, and connected with one another either through relations ⊳ or # µ . According to Th. 1, stopping prefix B contains an initial stopping prefix x 0 , whence a finite chain of events from e to some event of x 0 . Consider such a chain of minimal length. Our aim INRIA is now to make the length of this chain decrease. The last event l of the chain must satisfy g ⊳ l for some event g ∈ x 0 , otherwise it would be g# µ l, but then l would belong to x 0 , contradicting that l is the last event of the chain.

Consider the finite configuration v 0 =↓ l \ {l}, and observe that e is compatible with v 0 . Otherwise e would be in conflict with some event of v 0 , and since e is minimal in E, e would be in minimal conflict with some other event in v 0 , contradicting that we have chosen the chain from e to x 0 of minimal length. If l does belong to some initial branching cell of E v0 , then we have made the length of our chain decrease and we stop. Otherwise, l is now a minimal event of E v0 that does not belong to any initial branching cell in E v0 , so we can repeat with l in E v0 what we have done with e in E. Repeating this process infinitely many times is not possible, since otherwise it would construct infinitely many concurrent events. Hence the process stops, and we will eventually find a finite configuration v 1 such that l belongs to some initial branching cell of E v0⊕v1 . We have thus reduced the length of the chain from e to x 0 , and since the length of the chain is finite we can repeat this construction until we finally obtain a finite configuration v such that e belongs to some initial branching cell of E v . It is now clear that v has the required properties.

Figure 1 :

 1 Figure 1: Two nets (top) and their associated event structures (bottom).

Figure 2 :

 2 Figure 2: Illustrating the decomposition of nets.

Figure 3 :

 3 Figure 3: A 1-safe net that unfolds to a non locally finite event structure.

RR n 6724

Such configurations are called recursively stopped in[START_REF] Abbes | Probabilistic models for true-concurrency: branching cells and distributed probabilities for event structures[END_REF][START_REF] Abbes | Probabilistic true-concurrency models: Markov nets and a Law of large numbers[END_REF].RR n 6724

Analyzing an Example.

Let us informally apply this construction to the example depicted in Fig. 3; justifications of the computations that we perform will be given below. We have already listed configurations from X 0 and associated branching cells

with stopped configurations of E a∞ ). Hence, extending the definition of branching cells to initial stopping prefixes in the future of configurations from X 1 , we add x ′′′ = {d} and the already known x ′′ . Hence the net has four generalized local states (=classes of generalized branching cells) x = {a, b}, x ′ = {c, d}, x ′′ = {e, f } and x ′′′ = {d}. Consider µ, µ ′ , µ ′′ and µ ′′′ , probabilities on the associated sets Ω x , Ω x ′ , Ω x ′′ and Ω x ′′′ . For a finite configuration v ∈ X 0 as listed in (2) and thereafter, the probability P ↑ v is computed by the product formula [START_REF] Abbes | A (true) concurrent Markov property and some applications to Markov nets[END_REF]. We have seen that every maximal configuration ω belongs to X 1 , and that some of them belong to X 0 . We may thus ask: what is the probability that ω ∈ X 0 ? We have: where parameter α = µ(a) is the probability of choosing transition a for a token sitting on the left most place of the net.

We thus obtain that P(X 1 \ X 0 ) = 0 whenever α < 1 (note that α < 1 is a natural situation). In other words, configurations in X 1 are unfair, since they

A Omitted proofs

The proofs presented here are not to be published, because of lack of space. They can however be consulted in the PPS technical report freely available, with URL http://hal.archives-ouvertes.fr/hal-00267518/en.

We first state a simple lemma.

Lemma 1 Let E = (E, λ) be the unfolding of a 1-safe net N = (N, m 0 ), with N = (P, T, F ) and λ : E → T the unfolding labeling, and let v be any configuration of E. Denote by E v the labeled future (E v , λ E v ). Then there is a 1-safe Petri net N ′ = (N ′ , m ′ 0 ), with N ′ = (P ′ , T ′ , F ′ ), such that:

1. E v is the unfolding of N ′ ;

2. N ′ is a sub-net of N , i.e.:

Proof of Lemma 1. Only the last sentence of the lemma needs a proof, since the other statements are well known. If v is infinite, we may take for N ′ the net build upon the following set T ′ of transitions: let G be the set of transitions t ∈ T that appear infinitely many as a label of v. Then take

We also recall the following result:

Proof of of Th. 1. Let B be a non empty stopping prefix of E. Denote by H the poset of non empty stopping prefixes included in B, ordered by reverse inclusion. We show that any chain (B i ) i∈I of H has an upper bound in H. Obviously, since the poset of stopping prefixes of E is a complete lattice, the bound exists as a stopping prefix, it is given by C = i∈I B i , and all we have to show is that C = ∅. Assume that C = ∅, and consider the sequence of events constructed as follows. Fix ω a maximal configuration of E. Then ω ∩ B i is maximal in B i for all i ∈ I according to Lemma 2, and therefore ω ∩

Choose e 0 a minimal event of ω. Assume that n + 1 distinct events e 0 , . . . , e n have been constructed with e k minimal in ω for k = 1, . . . , n. Since i∈I ↓ B i = ∅, there is an index i ∈ I such that B i ∩ {e 0 , . . . , e n } = ∅. As ω ∩ B i is non empty, we pick e n+1 a minimal event of ω ∩ B i . Then e is also minimal in ω since B is prefix, and the induction is complete. Then all e n are pairwise distinct and minimal in ω, and thus minimal in E since ω is prefix. Now, applying the


Nadia Ben Abdallah

Sébastien Destercke

Anne-Laure Jousselme

Frédéric Pichon

University Machin

Sébastien

Logical and Evidential Inconsistencies Meet: First Steps

Keywords: inconsistency, logic, belief functions

Measuring inconsistency has been and is still an active research topic in both logic and evidence theory. However, the two fields have developed distinct notions and measure of inconsistency, following different paths. In this paper, we attempt to build some first bridges between the two trends, suggesting some first means for one to enrich the other, and vice-versa.

Introduction

Evidence theory (a.k.a. Dempster-Shafer theory, Belief function theory) and logic share many common concerns, and one of them is how to deal with inconsistency of information coming from multiple sources. For example, the notion maximal coherent subsets or its dual, minimal unsatisfiable subset, appear in both settings to deal with inconsistencies [START_REF] Thimm | On the evaluation of inconsistency measures[END_REF][START_REF] Dubois | A set-theoretic view of belief functions[END_REF].

One particular problem that has attracted a lot of attention in the two settings is how to measure inconsistency [START_REF] Thimm | On the evaluation of inconsistency measures[END_REF][START_REF] Grant | Measuring inconsistency in knowledgebases[END_REF][START_REF] Destercke | Toward an axiomatic definition of conflict between belief functions[END_REF][START_REF] Pichon | Several shades of conflict[END_REF]. However, as the two fields commonly use different basic models and assumptions (e.g., in the way the set of possible worlds is generated), they have provided different answers to this issue.

Our goal in this paper is not to introduce new ways to measure conflict or inconsistency in belief function theory, as there is already an ample literature on the topic (the reader can check [START_REF] Destercke | Toward an axiomatic definition of conflict between belief functions[END_REF][START_REF] Pichon | Several shades of conflict[END_REF][START_REF] Martin | Conflict management in information fusion with belief functions[END_REF], for instance). Our agenda is rather to explore what logic and belief functions theory can bring to each other when it comes to measure inconsistency. Similarly, while bridges between evidence theory and some logic frameworks such as penalty logic were studied before [START_REF] De Saint-Cyr | Penalty logic and its link with dempster-shafer theory[END_REF], the interconnections of the two settings when it comes to inconsistency is barely mentioned, let alone investigated.

In this paper, we mainly expose why we think tools issued from logic could be interesting for evidential reasoning and inconsistency quantification, and propose a simple way to use them within evidential reasoning. In particular, we think that measures of inconsistency issued from logic can help in identifying the main sources of observed inconsistency, a topic already explored within evidence theory [START_REF] Roquel | Decomposition of conflict as a distribution on hypotheses in the framework on belief functions[END_REF], but never by using a logical perspective.

We start by detailing an example motivating the topic considered on this paper in Section 2, in which we also provide some notations used in the paper.

Nadia Ben Abdallah Sébastien Destercke Anne-Laure Jousselme Frédéric Pichon Section 3 then makes a first simple, yet original proposal 1 to embed inconsistency measures issued from logic within evidential reasoning.

A motivational example

In this section, we first introduce some notations, before detailing an example motivating the interest of using inconsistency measures within the framework of evidence theory.

Needed notations

We consider a finite propositional language L. We denote by Ω the space of all interpretations of L, and by ω an element of Ω. Given a formula φ, ω is a model of φ if it satisfies it, denoted ω |= φ. We denote the models of a formula φ by E φ , that corresponds to usual subsets of Ω, the set of all interpretations. For convenience and to recall that we are assuming that sets are models of propositional logic formulas, we will also sometimes denote by ⊥ and the empty set ∅ and Ω, respectively. Since there is no ambiguity in propositional logic, we will also confuse φ with its sets of models for convenience. A knowledge base KB = {φ 1 , . . . , φ n } is usually formed of a conjunction φ 1 ∧ . . . ∧ φ n of formulas.

We consider that uncertain information is modelled by mass functions, i.e., a non-negative and normalised mapping m : Ω → [0, 1] with E⊆Ω m(E). Subsets with a strictly positive mass are called focal elements. In our case Ω will be the set of models, and focal elements E φ will corresponds to sets of models of formulas φ. Usually, the inconsistency of a mass function m is measured by the quantity m(∅). While there are good reasons (by which we mean properties and axioms) to consider it as a reasonable inconsistency measure [START_REF] Destercke | Toward an axiomatic definition of conflict between belief functions[END_REF], several authors have discussed alternatives [START_REF] Destercke | Toward an axiomatic definition of conflict between belief functions[END_REF][START_REF] Pichon | Several shades of conflict[END_REF][START_REF] Martin | Conflict management in information fusion with belief functions[END_REF]. In this paper, we will not question nor challenge its validity, but will rather increase its expressiveness.

Our discussion does not really depend on the used merging rule between mass functions, except for the fact that the rule should be able to generate some inconsistency, i.e., to produce a non-null mass on ∅, so we will focus on the standard conjunctive rule. Given two mass functions m 1 , m 2 , the mass m 12 on a given set C resulting from the conjunctive rule is

m 12 (C) = A,B⊆Ω,A∩B=C m 1 (A)m 2 (B). ( 1
)
Let us now proceed to an example that will serve as a basis and motivation for our discussion.

1 to our knowledge.

The example

Let us consider the two following masses defined on the propositional langage a, b (Ω = {(a, b), (a, ¬b), (¬a, b), (¬a, ¬b)}) and with focal elements φ 1 = {a ∧ b} and φ 2 = {¬a}, which generates E φ1 = {(a, b)} and E φ2 = {(¬a, b), (¬a, ¬b)}:

m 1 (φ 1 = {a ∧ b}) = α 1 m 1 ( ) = 1 -α m 2 (φ 2 = {¬a}) = α 2 m 2 ( ) = 1 -α 2
Their conjunctive combination gives

m 12 (φ 1 ∧ φ 2 = ⊥) = α 1 α 2 m 12 (φ 1 ) = α 1 (1 -α 2 ) m 12 (φ 2 ) = (1 -α 1 )α 2 m 12 ( ) = (1 -α 1 )(1 -α 2 )
Consider now the situation with three masses

m 1 (φ 1 = {a ∧ b}) = β 1 m 1 ( ) = 1 -β 1 m 2 (φ 2 = {¬a}) = β 2 m 2 ( ) = 1 -β 2 m 3 (φ 3 = {¬b}) = β 3 m 3 ( ) = 1 -β 3
whose conjunctive combination, if we restrict ourselves to those intersections leading to the empty set, is

m 1...3 (φ 1 ∧ φ 2 ∧ φ 3 = ⊥) = β 1 β 2 β 3 m 1...3 (φ 1 ∧ φ 2 = ⊥) = β 1 β 2 (1 -β 3 ) m 1...3 (φ 1 ∧ φ 3 = ⊥) = β 1 (1 -β 2 )β 3 One can see that if α 1 α 2 = β 1 β 2 + β 1 (1 -β 2 )β 3
, the usual measure of inconsistency m(∅) for belief functions will give the same results, and will be unable to distinguish the two different situations.

However, it could well be argued (and has been in standard logic setting) that the first situation is different from the second one, as from a logical perspective, the consistency of knowledge base φ 1 ∧ φ 2 ∧ φ 3 is usually perceived as different from the one of φ 1 ∧ φ 2 or φ 1 ∧ φ 3 . It would therefore be necessary to be able to make such a distinction.

In the next section, we make a first proposal as how this could be done by combining inconsistency measures issued from the logic framework to masses of evidence.

A first step towards a combination

Approach:

-Assume each initial mass is simple support, with m(φ i ) = α i being the ith mass -When combining, keep track of the logical KB produced this way (do not merge all the inconsistent ones into one m(∅)) -For each such KB, use a normalized logical inconsistency measure to weight the contributions to the emptyset.

Interests:

a more discriminative notion of conflict a refined analysis of the sources of conflict (which formula, with which contribution)

3.1 A quick review of logical inconsistency measure 3.2 A simple proposal to embed logical measure in evidence framework 3.3 The case of simple support masses

Conclusion and discussion

-Penalty logic and its link with Dempster-Shafer theory

  hal.archives-ouvertes.fr/hal-03387904 Submitted on 23 Nov 2021


Pierre-Alexandre Léziart

Thomas Flayols

Felix Grimminger

Nicolas Mansard

Philippe Souères

Implementation of a Reactive Walking Controller for the New Open-Hardware Quadruped Solo-12

This paper aims at showing the dynamic performance and reliability of the low-cost, open-access quadruped robot Solo-12, which is developed within the framework of Open Dynamic Robot Initiative. It presents the implementation of a state-of-the-art control pipeline, close to the one that was previously implemented on Mini Cheetah, which implements a model predictive controller based on the centroidal dynamics to compute desired contact forces in order to track a reference velocity. Different contributions are proposed to speed up the computation process, notably at the level of the state estimation and the whole body controller. Experimental results demonstrate that the robot closely follow the reference velocity while being highly reactive and able to recover from perturbations.

I. INTRODUCTION

Performing dynamic locomotion with legged robots in real-life environments raises challenging issues in terms of computational efficiency, embeddability, state estimation and control robustness to both external disturbances and unexpected obstacles. Increasingly impressive running behaviors have been shown in recent years with both bipeds [START_REF] Tajima | Fast running experiments involving a humanoid robot[END_REF], [START_REF] Hubicki | Walking and running with passive compliance: Lessons from engineering: A live demonstration of the atrias biped[END_REF], [START_REF] Gong | Feedback control of a cassie bipedal robot: Walking, standing, and riding a segway[END_REF] and quadrupeds [START_REF] Dynamics | Spot autonomous navigation[END_REF], [START_REF] Robotics | Quadruped robot a1 walks with you to the future[END_REF], [START_REF] Kim | Highly dynamic quadruped locomotion via whole-body impulse control and model predictive control[END_REF], though some performances are limited to flat floor [START_REF] Tajima | Fast running experiments involving a humanoid robot[END_REF], heavily rely on specific system dynamics [START_REF] Hubicki | Walking and running with passive compliance: Lessons from engineering: A live demonstration of the atrias biped[END_REF], or are undocumented [START_REF] Dynamics | Spot autonomous navigation[END_REF].

Over the years various methods have been developed to perform dynamic locomotion with legged robots. In [START_REF] Bellicoso | Dynamic locomotion through online nonlinear motion optimization for quadrupedal robots[END_REF] a Zero Moment Point (ZMP) based motion planner enabled the ANYmal quadruped [START_REF] Hutter | Anymal-a highly mobile and dynamic quadrupedal robot[END_REF] to display a wide range of gaits including a squat jump. A similar approach was successfully applied on IIT HyQ [START_REF] Semini | Design of hyq-a hydraulically and electrically actuated quadruped robot[END_REF] and coupled with an Anytime-Repairing A* (ARA*) planner that explores a tree of possible body motion primitives [START_REF] Winkler | Planning and execution of dynamic whole-body locomotion for a hydraulic quadruped on challenging terrain[END_REF]. The Mini Cheetah [START_REF] Katz | Mini cheetah: A platform for pushing the limits of dynamic quadruped control[END_REF] quadruped developed at MIT has demonstrated high speed running with aerial phase and various gaits using a fast online model predictive controller to compute an optimal reaction force profile [START_REF] Kim | Highly dynamic quadruped locomotion via whole-body impulse control and model predictive control[END_REF]. More data-oriented methods have also been tested, for instance on Cassie with Deep Reinforcement Learning to train control policies in simulation and then transfer them to the real hardware [START_REF] Xie | Learning locomotion skills for cassie: Iterative design and sim-to-real[END_REF], or to make locomotion behaviours emerge using hierarchical reinforcement learning [START_REF] Jain | Hierarchical reinforcement learning for quadruped locomotion[END_REF]. All these methods usually require a preliminary development phase in simulation to fully demonstrate a LAAS-CNRS, Université de Toulouse, CNRS, Toulouse, France b Max Planck Institute for Intelligent Systems, Tubingen, Germany c Artificial and Natural Intelligence Toulouse Institute, France * corresponding author: paleziart@laas.fr This work has been supported by the MEMMO European Union project within the H2020 Program under Grant Agreement No. 780684 and by the RoboCom++ European project. Low cost, easy to repair and highly documented, it is a platform of choice for experimentation of highly dynamic controllers, as well as for the teaching of legged robotics. their potential and better grasp their advantages and drawbacks before being applied to real robots. With experimental validation comes the risk of breaking mechanical parts when pushing robots to their limits. For this reason, experimental test are often limited to conservative secure movements especially when using high-end robots whose cost easily reaches ten of thousands of dollars [START_REF] Dynamics | Spot shopping page[END_REF], [START_REF]Robots IEEE)[END_REF].

The objective of the Open Dynamic Robot Initiative, which is at the heart of this paper, is specially to answer this problem by developing an open-access, low-cost (12k$) and low-complexity quadruped robot with mostly 3D printed and off-the-shelves components [START_REF]Open dynamic robot initiative[END_REF], [START_REF] Grimminger | An open torque-controlled modular robot architecture for legged locomotion research[END_REF]. This project aims at providing the community with reliable legged platforms that can be easily maintained and repaired and could benefit from numerous contributions in their development. The robot Solo-12 presented in Fig. 1 is a 12 degrees of freedom (DoF) quadruped that includes 3 DoF in each leg (adductionabduction and flexion-extension at the hip, flexion-extension at the knee). It is an extension to the Solo-8 prototype, which only included 2 DoF in each leg [START_REF] Grimminger | An open torque-controlled modular robot architecture for legged locomotion research[END_REF]. The aim of this paper is testing the dynamical capabilities of Solo-12 with a state of the art control pipeline which closely follows the scheme developed in [START_REF] Kim | Highly dynamic quadruped locomotion via whole-body impulse control and model predictive control[END_REF] for Mini Cheetah. This control scheme relies on a model predictive control block that uses a simplified centroidal model of the quadruped to output contact forces that should be applied on the ground to reach a reference velocity. Then, a whole-body control block generates the position, velocity and torques that should be followed by the actuators. Contributions to the control scheme with respect to [START_REF] Kim | Highly dynamic quadruped locomotion via whole-body impulse control and model predictive control[END_REF] are two-fold. The introduction of a simplified estimation procedure involving two complementary filters provides a simple, rapid and reliable reconstruction of the robot state. Taking advantage from the constraints at the feet and the Fig. 2: Reactive walking controller architecture base of the robot, the inverse kinematics is solved without having to tackle a complex hierarchical problem. Moreover, the computation of the feedforward torques is simplified thanks to a reformulation of the optimization problem as a box-QP that can be easily solved through the computation of pseudo-inverses [START_REF] Dostál | Box constrained quadratic programming with proportioning and projections[END_REF]. Finally, simulations and experimental result are described to demonstrate the performance of Solo-12 through the implementation of this control scheme. The results show that the robot is highly reactive, able to follow closely the reference input velocity, and shows a robust behaviour despite unexpected perturbations. The algorithms employed in this controller are open-source and coded in Python for ease of use and modification [START_REF]Quadruped reactive walking controller repository[END_REF]. Along with [START_REF] Viereck | Learning a centroidal motion planner for legged locomotion[END_REF], these are the first experiments recorded on Solo-12.

The paper is organized as follows: A rapid description of the Solo-12 is given in section II. The control architecture is presented in Section III. It includes an overview of the control scheme, a description of the foot trajectory generator and of the estimation module. Then, the whole-body controller is presented in section IV. Finally, simulations and experimental results are described in sections V and VI. II. THE SOLO QUADRUPED Open Dynamic Robot Initiative is a collaborative project created to design an open-source, low-cost and lowcomplexity actuator module that can be used to build different types of torque-controlled robots with mostly 3D printed and off-the-shelves components [START_REF]Open dynamic robot initiative[END_REF], [START_REF] Grimminger | An open torque-controlled modular robot architecture for legged locomotion research[END_REF]. Among other motivations, this project aims to allow an easy benchmarking of different control paradigms implemented on a same lowcost and easy to repair platform. The actuator module shown in Fig. 3 consists of a brushless outrunner motor, a high resolution optical encoder and a dual stage timing belt transmission. The module has a segment length of 160mm, weighs 150g and outputs 2,5Nm at 12A. A custom motor controller using a field oriented control algorithm and a local joint impedance controller similarly to [START_REF] Wensing | Proprioceptive actuator design in the mit cheetah: Impact mitigation and high-bandwidth physical interaction for dynamic legged robots[END_REF] is used to drive this actuator. The quadruped robot Solo-12 is a new member of the growing family of robots using this actuator module. It is composed of 12 identical modules with only variation of their shell enclosure. The platform is equiped with an inertial measurement unit embedding an extended Kalman filter for attitude estimation and a custom network bridge to close the control loop with a distant computer at 1kHz via Wifi or Ethernet. Note that this first prototype does not include any computing power other than the one required for the joint controller nor embedded power source (wired powering). Although not suited for industrial applications, this robot Fig. 3: Opened actuator module assembly with its dual stage 9:1 timing belt transmission, its permanent magnet synchronous motor and its optical incremental encoder Fig. 4: A sparse infill structure made by fused deposition modeling has been chosen for its lightness/stiffness trade-off allows the implementation of highly dynamic controllers at the state-of-the-art level, as demonstrated in this paper. The quality of its documentation and the open access of all its components, from high level control interfaces to mechanical design and control electronics, make it a platform of choice for research in legged robotics as well as for teaching.

A model of the quadruped is available in unified robot description format [START_REF]Universal robot description format (urdf)[END_REF] for control and simulation purposes. A particular care has been taken when making the CAD models to limit the sim-to-real gap in terms of inertia matrices with proper weighing and placement of all mechanical parts [START_REF] Grimminger | An open torque-controlled modular robot architecture for legged locomotion research[END_REF].

III. CONTROL ARCHITECTURE

The control scheme of the quadruped is described in Fig. 2. As stated before, it closely follows the pipeline proposed in [START_REF] Kim | Highly dynamic quadruped locomotion via whole-body impulse control and model predictive control[END_REF]. The system receives as inputs the desired gait sequence and the reference velocity, either specified with a joystick or higher level controller. This information is processed by a footstep planner which outputs the desired locations of the upcoming footsteps. The model predictive control (MPC) block uses a simplified centroidal model of the quadruped to find the contact forces that should be applied by the feet in stance phase to follow as closely as possible the reference velocity over a prediction horizon. The wholebody control block translates desired contact forces and foot trajectories into the corresponding actuator accelerations and feedforward torques. A PD controller is used to provide the feedback torques based on the difference between the desired and current joint positions and velocities. The estimator includes complementary filters that combine information coming from the inertial measurement unit (IMU) and from forward kinematics to evaluate the velocity and position of the base. The system dynamics, the footstep planner and the Fig. 5: A dual cascaded complementary filter provides base position and velocity estimate while being easy to tune and simple to implement MPC are textbook reimplementation of the ones presented in [START_REF] Kim | Highly dynamic quadruped locomotion via whole-body impulse control and model predictive control[END_REF] so they won't be described in this paper.

A. Foot trajectory generator

During swing phases, feet have to be guided from their current position on the ground to the target position outputted by the footstep planner. Foot trajectory generators (one per foot) are used to generate reference trajectories in position, velocity and acceleration. Non-slipping constraints are enforced (zero velocity and acceleration during take-off and landing) with the additional constraint to reach a predefined height at the apex of the swing phase. This is done by using a 5-th order polynomials for each horizontal component and a 6-th order polynomial for the vertical one.

B. State Estimation

The on-board IMU which embeds an extended Kalman filter provides a gravity free base acceleration, angular base velocities as well as roll, pitch and yaw angles estimate.

The estimation of the linear base velocity and position can be tackled using a linear approach decoupled from orientation and angular base velocity since they are already measured by the IMU [START_REF] Flayols | Experimental evaluation of simple estimators for humanoid robots[END_REF]. We use a dual cascaded complementary filter [START_REF] Carpentier | A kinematics-dynamics based estimator of the center of mass position for anthropomorphic system-a complementary filtering approach[END_REF] that fuses the information coming from the IMU and the forward kinematics, based on the contact points with the ground, as shown in Fig. 5.

IV. EFFICIENT WHOLE-BODY CONTROL

As its main theoretical contribution, this paper presents a more computationally efficient version of the whole-body controller used in [START_REF] Kim | Highly dynamic quadruped locomotion via whole-body impulse control and model predictive control[END_REF]. The role of this controller is to convert the desired contact forces provided by the MPC and the reference feet position, velocity and acceleration given by the trajectory generators into torque, position and velocity commands that are sent to the low level motor drivers. The whole-body control relies on two successive blocks: inverse kinematics (IK) and a torque computation (Fig. 6).

A. Computing desired accelerations

The first step is to compute command accelerations qIK by IK of the full model of the quadruped. The IK scheme is defined by 3 tasks: Fig. 6: Whole-body control scheme with its two successive steps: inverse kinematics and solving of a QP problem

• Follow the reference trajectory of the swing feet while maintaining feet in contact immobile (3 DoF per leg, 12 DoF in total) For a quadruped robot with 18 DoF, these tasks fully constrain the system but are compatible as the number of DoF is sufficient to satisfy each of them independently. As all tasks are compatible, we prefer to discard the hierarchical inverse kinematic scheme introduced in [START_REF] Kim | Highly dynamic quadruped locomotion via whole-body impulse control and model predictive control[END_REF], and rather implement the following more efficient resolution. By stacking all the task functions in a global vector according to the above description order, a global task Jacobian of size 18 by 18 can be defined as:

        ẋpos ẋang ẋ1 ẋ2 ẋ3 ẋ4         = J q =         o R b 0 0 . . . 0 0 o R b 0 o R b b T 1 × o R b J 1 . . . . . . o R b b T 2 × o R b 0 J 2 . . . o R b b T 3 × o R b . . . . . . J 3 0 o R b b T 4 × o R b 0 . . . 0 J 4                 qpos qang q1 q2 q3 q4        
(1) with o R b the rotation matrix from base to world frame, b T i the position of the i-th foot in base frame (∀i ∈ {1, 2, 3, 4}), J i the Jacobian of the i-th foot, ẋpos , ẋang the base linear and angular velocities in world frame, ẋi the velocity of the i-th foot in world frame, qpos , qang the base linear and angular velocities in base frame and qi the joint velocities of the i-th leg. Computing J -1 i matrices is enough to get the inverse of the whole J matrix:

J -1 =         b R o 0 0 . . . 0 0 b R o 0 -J -1 1 -J -1 1 (T 1 × o R b ) b R o J -1 1 . . . . . . -J -1 2 -J -1 2 (T 2 × o R b ) b R o 0 J -1 2 . . . -J -1 3 -J -1 3 (T 3 × o R b ) b R o . . . . . . J -1 3 0 -J -1 4 -J -1 4 (T 4 × o R b ) b R o 0 . . . 0 J -1 4         (2)
As J i are 3 by 3 invertible matrices (except at leg singularities) damping can be introduced when inverting them although we did not see any gain in practice. Finally we obtain the desired joint accelerations qIK :

qIK = qcmd = (q cmd pos , qcmd ang , qcmd 1 , qcmd 2 , qcmd 3 , qcmd 4
) (3) = J -1 (ẍ cmd -J q) (4)
with ẍcmd the concatenated accelerations of the base position task, base orientation task and foot tracking tasks. These accelerations are defined by:

ẍcmd j = K p,j (x des j -x j ) + K d,j ( ẋdes j -ẋj ) + ẍdes j (5)
with K p,j and K d,j the position and velocity feedback gains associated with task j ∈ {pos, ang, 1, 2, 3, 4}. x des j , x j , ẋdes j and ẋj are respectively the desired and current position and velocity associated with task j. The accelerations qcmd pos , qcmd ang and qcmd i are sent to the second step of the whole-body control to compute feedforward torque commands.

B. Computing reference positions and velocities

As Solo-12 motors are current controlled without torque feedback, the low level consists of a joint-level impedance controller, as shown in Fig. 2. The reference articular configuration and velocity of the i-th leg are computed as follows:

q cmd i = q i + J -1 i (x des i -x i )-(x des pos -x pos ) -(T i × o R b ) b R o (x des ang -x ang ) (6)
qcmd i = J -1 i ẋdes i -ẋdes pos -(T i × o R b ) b R o ẋdes ang (7)
where the desired position and velocity x des i and ẋdes i are determined from the swing reference trajectory.

C. Feedforward torques computation

Following [START_REF] Kim | Highly dynamic quadruped locomotion via whole-body impulse control and model predictive control[END_REF] we compute the feedforward torques using relaxation variables δ q and δ f . The QP problem tries to find contact forces f = f M P C +δ f and accelerations q = qIK +δ q that are as close as possible to the force references decided by the MPC and the command accelerations decided by the IK while taking into account the floating base dynamics.

min δq,δ f δ T q Q 1 δ q + δ T f Q 2 δ f (8) s.t. f M P C + δ f ∈ K (9) S(M (q IK + δ q 0 ) + b) = SJ T c (f M P C + δ f ) (10)
with M the generalized mass matrix, b the vector of nonlinear and gravitational forces, S the matrix selecting the underactuated dynamics, J c the augmented contact Jacobian and K the space inside the friction cone linearized to the first order.

Similarly to IK, we introduce a more computionally efficient way to compute feedforward torques from the reaction forces f M P C outputted by the MPC and the accelerations qIK . We transform the quadratic programming problem introduced in [START_REF] Kim | Highly dynamic quadruped locomotion via whole-body impulse control and model predictive control[END_REF] into an equivalent problem faster to solve as it amounts to a few matrix inversions. It will be useful to separate the variables between the unactuated part consisting of the base and the actuated joints:

M = Y M u M T u M a 18×18 J T c = X J a 18×12 (11)
where subscripts u and a refer to the underactuated and actuated parts respectively. Using the underactuated part of (10) δ q is then expressed as an affine expression of δ f :

δ q = Aδ f + γ (12) A = Y -1 X (13) γ = Y -1 (Xf M P C -Y qIK,u -M u qIK,a -b u ) (14)
Y qIK,u + M u qIK,a + b u can be computed by a cheap Recursive Newton-Euler Algorithm (RNEA) evaluation [START_REF] Carpentier | Pinocchio: fast forward and inverse dynamics for poly-articulated systems[END_REF].

δ q is then replaced in ( 8) using ( 12):

min δ f δ T f Hδ f + 2δ T f g (15) s.t. f M P C + δ f ∈ K (16) H = A T Q 1 A + Q 2 (17) g = A T Q 1 γ (18)
f M P C + δ f ∈ K is equivalent to f M P C + δ f = F T 1 F T 2 F T 3 F T 4 T where ∀k ∈ 1..4, F k = G k λ k with
λ k ≥ 0 and G k the edges of the linearized friction cone of the k-th foot with friction coefficient µ. The final QP problem is thus of the form:

min λ 1 2 λG T HGλ + (G T g -G T H f M P C ) T λ (19) such that ∀k ∈ 1..4, ∀i ∈ 1..4, λ k,i ≥ 0 ( 20
)
G k λ k =   µ µ -µ -µ µ -µ µ -µ 1 1 1 1       λ k,1 λ k,2 λ k,3 λ k,4     (21) λ = λ T 1 λ T 2 λ T 3 λ T 4 T G =     G 1 0 0 0 0 G 2 0 0 0 0 G 3 0 0 0 0 G 4     (22)
This last problem is a box-QP [START_REF] Dostál | Box constrained quadratic programming with proportioning and projections[END_REF], [START_REF] Ye | Approximating quadratic programming with bound constraints[END_REF]. Box constraints are easier to handle than generic linear constraints, and lead to simpler and more efficient implementations. In particular, box-QP algorithms are straightforward to implement, do not imply computing the Lagrange multipliers, and have a much better worst-case performance than regular QP (linear versus exponential) [START_REF] Nocedal | Numerical optimization[END_REF]. Once δ f has been determined, δ q can be deduced. The multi-body dynamics can be written as:

τ u τ a = M (q IK + δ q 0 ) + b -J T c (f M P C + δ f ) (23)
Since only τ a has to be computed ( 23) is reduced to:

τ a = M T u (q IK,u +δ q )+M a qIK,a +b a -J a (f M P C +δ f ) (24
) These feedforward torques τ a are then added to the feedback ones computed by the PD controller. This is beneficial to the locomotion for two reasons: compared to a pure feedforward command, it helps correcting model errors and enables the use of lower gains.

V. SIMULATIONS

A. Simulation setup

A fully-actuated 3D dynamic model of the Solo-12 robot was used to assess the effectiveness of the proposed control scheme. The control framework was implemented in Python for ease of use and prototyping. Achieving real time performance was made possible by exploiting NumPy vectorial capabilities, using libraries that provides Python bindings for their C implementation and compiling computation intensive parts (coded in C++ with Python bindings). The main control loop (footstep planner, foot trajectory generators, whole-body control and state estimator) runs at 500 Hz on a i7-7700 CPU (3.60 GHz) while the MPC runs at 50 Hz in a parallel process and communicates with the main loop through a shared memory. Low-level kinematics and dynamics computation were performed using the Pinocchio library that provides standard rigid body operations and algorithms for poly-articulated systems [START_REF] Carpentier | Pinocchio: fast forward and inverse dynamics for poly-articulated systems[END_REF], [START_REF] Carpentier | The pinocchio c++ library -a fast and flexible implementation of rigid body dynamics algorithms and their analytical derivatives[END_REF]. The MPC exploits the sparcity of its constraint matrices using the OSQP solver [START_REF] Stellato | OSQP: an operator splitting solver for quadratic programs[END_REF]. The simulation environment was set up using PyBullet which offers contacts simulation and a Python API to send torques and retrieve relevant data [START_REF] Coumans | Pybullet, a python module for physics simulation for games, robotics and machine learning[END_REF].

B. Scenarios

Before testing the proposed control scheme on the real hardware we wanted to assess its stabilization capabilities in a simulated environment for a walking trot gait with period set to 0.32s. The first scenario consists in a straight walk and a turn on a flat ground with an external perturbation of +5 N along X at t = 9s and another one of +5 N along Y at t = 11s. The second scenario places the robot on a rough terrain: the ground is full of small bumps whose height is random (uniform distribution between 0 and 5 cm). For both scenarios the reference velocity is initially zero and slowly rises up to 1.5 m/s and 1.0 m/s forwards respectively and to 0.4 rad/s when turning.

In scenario 1 the robot reaches its reference forward velocity of 1.5 m/s and returns to its nominal behaviour after both external perturbations. As the robot moves faster it gets increasingly tilted in pitch despite a reference angle at 0 o . This may be due to a compromise with other quantities in the cost function of the MPC which leads to a minima with a non-zero pitch angle in average. Scenario 2 highlights a limit of the proposed control scheme: the ground is supposed to be flat so feet can slip during stance phase when landing on an unexpected tilted surface such as the sides of bumps. Since the controller expects to work in nominal conditions (flat ground), the contact forces it wants to apply can be out of the friction cone of the actual tilted surface. Without knowledge of the environment a possible solution would be to continuously check for slipping during stance phases and react accordingly if such an event is detected [START_REF] Bloesch | State estimation for legged robots on unstable and slippery terrain[END_REF].

VI. EXPERIMENTAL EVALUATION

A. Experimental setup

Experiments were performed indoors on a flat ground. Small rubber bands have been glued on the robot feet to improve friction with the plastic flooring. To be conservative, we use a friction coefficient of 0.9 with the actual coefficient assessed around 1.0. Ground truth was retrieved thanks to a motion capture system consisting of a set of [START_REF] Viereck | Learning a centroidal motion planner for legged locomotion[END_REF] They are the same as the ones used for Mini Cheetah [START_REF]Cheetah-software repository[END_REF] and worked out of the box for us. The weights for contact force regularization were set to 1 × 10 -5 for all components.

To perform inverse kinematics we used K p = 100 and K d = 2 K p = 20 for all tasks. In the initial formulation of the QP problem (8) we used 0.1 and 1.0 for the weights of the acceleration and contact force relaxation variables (Q 1 and Q 2 respectively). For the on-board impedance controller, all joints shared the same proportional feedback control gains of 6 Nm/rad and 0.2 Nm/(rad/s) respectively. The performed gait was a trot with a period of 0.32s.

During the experiments the robot was powered via an external power supply. Communications with the robot (sensors data retrieval and command sending) were done using an Ethernet link to the control desktop computer.

B. Results

Fig. 8 and 9 present the results of an experiment during which the Solo-12 quadruped is controlled by a user with a gamepad (until t = 18s). The robot performs first a lateral walk to the right then to the left, a clockwise rotation along the vertical axis and finally a short walk forwards. The robot is then ordered to stay immobile (zero velocity command) while it is being pushed sideways by the user (after t = 18s).

Thanks to the motion capture ground truth we can assess both the quality of estimation and of the reference tracking. The quality of the height estimation seems greatly influenced by the variation of others quantities both in orientation and velocity. This can be explained by slight slippings of feet which produce an undesired swaying motion in pitch. Estimation of other quantities seems robust to perturbations except during lateral walks at t = 8s and t = 11s. The velocity reference given by the user is correctly followed when the quadruped does not have to face external perturbations.

In the second half of the experiment the robot manages to recover from the four sideways perturbations that it receives at t = 22s, t = 23s, t = 24.5s and t = 26.5s. The third push also transmits a rotating motion to the robot. In all cases it counters the undesired velocity and returns to a nominal behaviour in less than half a second. A video of locomotion and push recovery can be found online1 . In this paper we demonstrated the capability of the Solo-12 quadruped to perform a dynamic and reactive locomotion in order to track a reference velocity. This result shows that, despite its low-complexity and low-cost, this openaccess robot constitutes a reliable platform for research and teaching that can be easily maintained and repaired. Future work could focus on the implementation of a more elaborate model predictive control taking into account the non-linear effects that were omitted, considering footsteps placements as part of the optimization problem or even working on non-predefined timings for the contact switches, as done in [START_REF] Corbères | Comparison of predictive controllers for locomotion and balance recovery of quadruped robots[END_REF]. The current implementation could also be optimized to reach higher control frequencies and thus more regularly refresh the feedforward torques and target articular positions and velocities to further improve the control quality. The hardware could also be enhanced alongside the software by embedding batteries and a CPU on-board to turn Solo-12 into a truly autonomous robot that could investigate more dynamic motion without the limitation of a cable. If processing the whole control architecture on-board is not possible then a wireless communication with a control computer could also be considered.

Fig. 1 :

 1 Fig. 1: The 12-DoF version of the open-hardware Solo quadruped weights less than 2.5 kg. Low cost, easy to repair and highly documented, it is a platform of choice for experimentation of highly dynamic controllers, as well as for the teaching of legged robotics.

•

  Keep the base at constant height and follow the reference horizontal velocity (3 DoF for base position) • Keep the base orientation horizontal and follow the reference yaw angular velocity (3 DoF for base orientation)

velocity in scenario 2 Fig. 7 :

 27 Fig. 7: (a) (b) The quadruped recovers from both perturbations occurring at 9s and 11s and reaches a maximum lateral velocity of +0.56 m/s at t =11.15s. It returns to its nominal behaviour in around 0.5s. (c) (d) The quality of the estimation is worse than in scenario 1 as feet sometimes slip on bumps sides which breaks our immobile contact assumption.

Fig. 8 :

 8 Fig. 8: Reference, estimated and motion-captured velocities of the base obtained on the real hardware MPC weights chosen for position, orientation, linear velocity and angular velocity errors are respectively [2.0, 2.0, 20.0, 0.25, 0.25, 10.0, 0.2, 0.2, 0.2, 0.0, 0.0, 0.3].They are the same as the ones used for Mini Cheetah[START_REF]Cheetah-software repository[END_REF] and worked out of the box for us. The weights for contact force regularization were set to 1 × 10 -5 for all components.To perform inverse kinematics we used K p = 100 and K d = 2 K p = 20 for all tasks. In the initial formulation of the QP problem (8) we used 0.1 and 1.0 for the weights of the acceleration and contact force relaxation variables (Q 1 and Q 2 respectively). For the on-board impedance controller, all joints shared the same proportional feedback control gains of 6 Nm/rad and 0.2 Nm/(rad/s) respectively. The performed gait was a trot with a period of 0.32s. During the experiments the robot was powered via an external power supply. Communications with the robot (sensors data retrieval and command sending) were done using an Ethernet link to the control desktop computer.

Fig. 9 :

 9 Fig. 9: Reference, estimated and motion-captured height and orientation of the trunk VII. CONCLUSIONS

https://peertube.laas.fr/videos/watch/ 4a8a1bcf-9bd7-4909-af26-ed304ded7df0