F Herbreteau

B Srivathsan

I Walukiewicz

Efficient Emptiness Check for Timed Büchi Automata

The Büchi non-emptiness problem for timed automata concerns deciding if a given automaton has an infinite non-Zeno run satisfying the Büchi accepting condition. The standard solution to this problem involves adding an auxiliary clock to take care of the non-Zenoness. In this paper, we show that this simple transformation may sometimes result in an exponential blowup. We propose a method avoiding this blowup.

Introduction

Timed automata [START_REF] Alur | A theory of timed automata[END_REF] are widely used to model real-time systems. They are obtained from finite automata by adding clocks that can be reset and whose values can be compared with constants. The crucial property of timed automata is that their emptiness is decidable. This model has been implemented in verification tools like Uppaal [START_REF] Behrmann | Uppaal 4.0[END_REF] or Kronos [START_REF] Bozga | Kronos: a mode-checking tool for real-time systems[END_REF], and used in industrial case studies [START_REF] Havelund | Formal modeling and analysis of an audio/video protocol: An industrial case study using UPPAAL[END_REF][START_REF] Bérard | Analysing the pgm protocol with UPPAAL[END_REF][START_REF] Jessen | Guided controller synthesis for climate controller using UPPAAL TiGA[END_REF].

While most tools concentrate on the reachability problem, the questions concerning infinite executions of timed automata are also of interest. In the case of infinite executions one has to eliminate so called Zeno runs. These are executions that contain infinitely many steps taken in a finite time interval. For obvious reasons such executions are considered unrealistic. In this paper we study the problem of deciding if a given timed automaton has a non-Zeno run passing through accepting states infinitely often. We call this problem Büchi non-emptiness problem.

This basic problem has been of course studied already in the paper introducing timed automata. It has been shown that using so called region abstraction the problem can be reduced to the problem of finding a path in a finite region graph satisfying some particular conditions. The main difference between the cases of finite and infinite executions is that in the latter one needs to decide if the path that has been found corresponds to a non Zeno run of the automaton.

Subsequent research has shown that the region abstraction is very inefficient for reachability problems. Another method using zones instead of regions has been proposed. It is used at present in all timed-verification tools. While simple at the first sight, the zone abstraction was delicate to get right. This is mainly because the basic properties of regions do not transfer to zones. The zone abstraction also works for infinite executions, but unlike for regions, it is impossible to decide if a path in a zone graph corresponds to a non-Zeno run of the automaton.

There exists a simple solution to the problem of Zeno runs that amounts to transforming automata in such way that every run passing through an accepting state infinitely often is non-Zeno. An automaton with such a property is called strongly non-Zeno. The transformation is easy to describe and requires addition of one new clock. This paper is motivated by our experiments with an implementation of this construction. We have observed that this apparently simple transformation can give a big overhead in the size of a zone graph.

In this paper we closely examine the transformation to strongly non-Zeno automata [START_REF] Tripakis | Checking timed büchi automata emptiness efficiently[END_REF], and show that it can inflict a blowup of the zone graph; and this blowup could even be exponential in the number of clocks. To substantiate, we exhibit an example of an automaton having a zone graph of polynomial size, whose transformed version has a zone graph of exponential size. We propose another solution to avoid this phenomenon. Instead of modifying the automaton, we modify the zone graph. We show that this modification allows us to detect if a path can be instantiated to a non-Zeno run. Moreover the size of the modified graph is |ZG(A)|.|X|, where |ZG(A)| is the size of the zone graph and |X| is the number of clocks.

In the second part of the paper we propose an algorithm for testing the existence of accepting non-Zeno runs in timed automata. The problem we face highly resembles the emptiness testing of finite automata with generalized Büchi conditions. Since the most efficient solutions for the latter problem are based on the Tarjan's algorithm, we take the same way here. We present an algorithm whose running time is bounded by |ZG(A)|.|X| 2 . We also report on the experiments performed with a preliminary implementation of this algorithm.

Related work

The zone approach has been introduced in Petri net context [START_REF] Berthomieu | An enumerative approach for analyzing time petri nets[END_REF], and then adapted to the framework of timed automata [START_REF] Dill | Timing assumptions and verification of finite-state concurrent systems[END_REF]. The advantage of zones over regions is that they do not require to consider every possible unit time interval separately. The delicate point about zones was to find a right approximation operator. Indeed while regions are both pre-and post-stable, zones are not pre-stable, and some care is needed to guarantee post-stability. Post-stability is enough for correctness of the reachability algorithm, and for testing if a path in the zone graph can be instantiated to a run of the automaton. It is however not possible to determine if a path can be instantiated to a non-Zeno run. The solution involving adding one clock has been discussed in [START_REF] Tripakis | Verifying progress in timed systems[END_REF][START_REF] Tripakis | Checking timed büchi automata emptiness efficiently[END_REF][START_REF] Alur | Decision problems for timed automata: A survey[END_REF]. Recently, Tripakis [START_REF] Tripakis | Checking timed büchi emptiness on simulation graphs[END_REF] has shown a way to extract an accepting run from a zone graph of the automaton. Combined with the construction of adding one clock this gives a solution to our problem. A different approach has been considered in [START_REF] Gómez | Efficient detection of zeno runs in timed automata[END_REF] where syntactic conditions are proposed for a timed automaton to be free from Zeno runs. Notice that for obvious complexity reasons, any such condition must be either not complete, or of the same algorithmic complexity as the emptiness test itself. Organization of the paper In the next section we formalize our problem, and discuss region and zone abstractions. As an intermediate step we give a short proof of the above mentioned result from [START_REF] Tripakis | Checking timed büchi emptiness on simulation graphs[END_REF]. Section 3 explains the problems with the transformation to strongly non-Zeno automata, and describes our alternative method. The following section is devoted to a description of the algorithm.

The Emptiness Problem for Timed Büchi Automata

Timed Büchi Automata

Let X be a set of clocks, i.e., variables that range over R ≥0 , the set of nonnegative real numbers. Clock constraints are conjunctions of comparisons of variables with integer constants, e.g. (x ≤ 3 ∧ y > 0). Let Φ(X) denote the set of clock constraints over clock variables X.

A clock valuation over X is a function ν : X → R ≥0 . We denote R X ≥0 for the set of clock valuations over X, and 0 : X → {0} for the valuation that associates 0 to every clock in X. We write ν |= φ when ν satisfies φ, i.e. when every constraint in φ holds after replacing every x by ν(x).

For a valuation ν and δ ∈ R ≥0 , let (ν + δ) be the valuation such that

(ν + δ)(x) = ν(x) + δ for all x ∈ X. For a set R ⊆ X, let [R]ν be the valuation such that ([R]ν)(x) = 0 if x ∈ R and ([R]ν)(x) = ν(x) otherwise.
A Timed Büchi Automaton (TBA) is a tuple A = (Q, q 0 , X, T, Acc) where Q is a finite set of states, q 0 ∈ Q is the initial state, X is a finite set of clocks, Acc ⊆ Q is a set of accepting states, and

T ⊆ Q × Φ(X) × 2 X × Q is a finite set of transitions (q, g, R, q ′ )
where g is a guard, and R is a reset of the transition.

A configuration of A is a pair (q, ν) ∈ Q × R X ≥0 ; with (q 0 , 0) being the initial configuration. A discrete transition between configurations (q, ν) t ⇀ (q ′ , ν ′ ) for t = (q, g, R, q ′ ) is defined when ν g and ν ′ = [R]ν. We also have delay transitions between configurations: (q, ν) δ ⇁ (q, ν + δ) for every q, ν and δ ∈ R ≥0 . We write (q, ν)

δ,t -→ (q ′ , ν ′ ) if (q, ν) δ ⇁ (q, ν + δ) t ⇀ (q ′ , ν ′ ).
A run of A is a finite or infinite sequence of configurations connected by δ,t -→ transitions, starting from the initial state q 0 and the initial valuation ν 0 = 0:

(q 0 , ν 0 ) δ0,t0 ---→ (q 1 , ν 1 ) δ1,t1 ---→ • • •
A run σ satisfies the Büchi condition if it visits accepting configurations infinitely often, that is configurations with a state from Acc. The duration of the run is the accumulated delay: i≥0 δ i . A run σ is Zeno if its duration is bounded.

Definition 1. The Büchi non-emptiness problem is to decide if A has a non-Zeno run satisfying the Büchi condition.

The class of TBA we consider is usually known as diagonal-free TBA since clock comparisons like xy ≤ 1 are disallowed. Since we are interested in the Büchi non-emptiness problem, we can consider automata without an input alphabet and without invariants since they can be simulated by guards.

The Büchi non-emptiness problem is known to be Pspace-complete [START_REF] Alur | A theory of timed automata[END_REF].

Regions and region graphs

A simple decision procedure for the Büchi non-emptiness problem builds from A a graph called the region graph and tests if there is a path in this graph satisfying certain conditions. We will define two types of regions.

Fix a constant M and a finite set of clocks X. Two valuations ν, ν ′ ∈ R X ≥0 are region equivalent w.r.t. M , denoted ν ∼ M ν ′ iff for every x, y ∈ X:

1. ν(x) > M iff ν ′ (x) > M ; 2. if ν(x) ≤ M , then ⌊ν(x)⌋ = ⌊ν ′ (x)⌋; 3. if ν(x) ≤ M , then {ν(x)} = 0 iff {ν ′ (x)} = 0; 4. if ν(x) ≤ M and ν(y) ≤ M then {ν(x)} ≤ {ν(y)} iff {ν ′ (x)} ≤ {ν ′ (y)}.
The first three conditions ensure that the two valuations satisfy the same guards. The last one enforces that for every δ ∈ R ≥0 there is δ ′ ∈ R ≥0 , such that valuations ν + δ and ν ′ + δ ′ satisfy the same guards.

We will also define diagonal region equivalence (d-region equivalence for short) that strengthens the last condition to

4 d . for every integer c ∈ (-M, M ): ν(x) -ν(y) ≤ c iff ν ′ (x) -ν ′ (y) ≤ c
This region equivalence is denoted by ∼ d M . Observe that it is finer than ∼ M . A region is an equivalence class of ∼ M . We write [ν] ∼ M for the region of ν, and R M for the set of all regions with respect to M . Similarly, for d-region equivalence we write:

[ν] d ∼ M and R d M .
If r is a region or a d-region then we will write r g to mean that every valuation in r satisfies the guard g. Observe that all valuations in a region, or a d-region, satisfy the same guards.

For an automaton A, we define its region graph, RG(A), using ∼ M relation, where M is the biggest constant appearing in the guards of its transitions. Nodes of RG(A) are of the form (q, r) for q a state of A and r ∈ R M a region. There is a transition (q, r)

t -→ (q ′ , r ′ ) if there are ν ∈ r, δ ∈ R ≥0 and ν ′ ∈ r ′ with (q, ν) δ,t -→ (q ′ , ν ′ ).
Observe that a transition in the region graph is not decorated with a delay. The graph RG d (A) is defined similarly but using the ∼ d M relation. It will be important to understand the properties of pre-and post-stability of regions or d-regions [START_REF] Tripakis | Checking timed büchi automata emptiness efficiently[END_REF]. We state them formally. A transition (q, r) t -→ (q ′ , r ′ ) in a region graph or a d-region graph is:

-Pre-stable if for every ν ∈ r there are ν ′ ∈ r ′ , δ ∈ R ≥0 s.t. (q, ν)

δ,t -→ (q ′ , ν ′ ).
-Post-stable if for every ν ′ ∈ r ′ there are ν ∈ r, δ ∈ R ≥0 s.t. (q, ν)

δ,t -→ (q ′ , ν ′ ).
The following lemma (cf. [START_REF] Bouyer | Forward analysis of updatable timed automata[END_REF]) explains our interest in ∼ d M relation. Lemma 1 (Pre and post-stability). Transitions in RG d (A) are pre-stable and post-stable. Transitions in RG(A) are pre-stable but not necessarily poststable.

Consider two sequences

(q 0 , ν 0 ) δ0,t0 ---→ (q 1 , ν 1 ) δ1,t1 ---→ • • • (1) (q 0 , r 0 ) t0 -→ (q 1 , r 1 ) t1 -→ • • • (2)
where the first is a run in A, and the second is a path in RG(A) or RG d (A). We say that the first is an instance of the second if ν i ∈ r i for all i ≥ 0. Equivalently, we say that the second is an abstraction of the first. The following lemma is a direct consequence of the pre-stability property.

Lemma 2. Every path in RG(A) is an abstraction of a run of A, and conversely, every run of A is an instance of a path in RG(A). Similarly for RG d (A).

This lemma allows us to relate the existence of an accepting run of A to the existence of paths with special properties in RG(A) or RG d (A). We say that a path as in (2) satisfies the Büchi condition if it has infinitely many occurrences of states from Acc. The path is called progressive if for every clock x ∈ X:

-either x is almost always above M : there is n with r i x > M for all i > n; -or x is reset infinitely often and strictly positive infinitely often: for every n there are i, j > n such that r i (x = 0) and r j (x > 0).

Theorem 1 ([1]

). For every TBA A, L(A) = ∅ iff RG(A) has a progressive path satisfying the Büchi condition. Similarly for RG d (A).

While this theorem gives an algorithm for solving our problem, it turns out that this method is very impractical. The number of regions [START_REF] Alur | A theory of timed automata[END_REF] and constructing all of them, or even searching through them on-the-fly, has proved to be very costly.

RA(A) is O(|X|!2 |X| M |X| )

Zones and zone graphs

Timed verification tools use zones instead of regions. A zone is a set of valuations defined by a conjunction of two kinds of constraints : comparison of the difference between two clocks with a constant, or comparison of the value of a single clock with a constant. For example (xy ≥ 1) ∧ (y < 2) is a zone. While at first sight it may seem that there are more zones than regions, this is not the case if we count only those that are reachable from the initial valuation.

Since zones are sets of valuations defined by constraints, one can define discrete and delay transitions directly on zones. For δ ∈ R ≥0 , we have (q, Z) δ ⇁ (q, Z ′ ) if Z ′ is the smallest zone containing the set of all the valuations ν + δ with ν ∈ Z. Similarly, for a discrete transition we put (q, Z) t ⇀ (q ′ , Z ′ ) if Z ′ is the set of all the valuations ν ′ such that (q, ν) t ⇀ (q ′ , ν ′ ) for some ν ∈ Z; Z ′ is a zone in this case. Moreover zones can be represented using Difference Bound Matrices (DBMs), and transitions can be computed efficiently on DBMs [START_REF] Dill | Timing assumptions and verification of finite-state concurrent systems[END_REF]. The problem is that the number of reachable zones is not guaranteed to be finite [START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF].

In order to ensure that the number of reachable zones is finite, one introduces abstraction operators. We mention the three most common ones in the literature. They refer to region graphs, RG(A) or RG d (A), and use the constant M that is the maximal constant appearing in the guards of A.

-Closure M (Z): the smallest union of regions containing Z; -Closure d M (Z): similarly but for d-regions; -Approx M (Z): the smallest union of d-regions that is convex and contains Z.

The following lemma establishes the links between the three abstraction operators, and is very useful to transpose reachability results from one abstraction to the other.

Lemma 3 ([6]). For every zone

Z: Z ⊆ Closure d M (Z) ⊆ Approx M (Z) ⊆ Closure M (Z).
A symbolic zone S is a zone approximated with one of the above abstraction operators. Now, similar to region graphs, we define simulation graphs where after every transition a specific approximation operation is used, that is each node in the simulation graph is of the form (q, S) with S being a symbolic zone . So we have three graphs corresponding to the three approximation operations.

Take an automaton A and let M be the biggest constant appearing in the guards of its transitions. In the simulation graph SG(A) the nodes are of the form (q, Closure M (Z)) where q is a state of A and Z is a zone. The initial node is (q 0 , Closure M (Z 0 )), with q 0 the initial state of A, and Z 0 the zone setting all the variables to 0. The transitions in the graph are (q, Closure M (Z))

t -→ (q ′ , Closure M (Z ′ )) where Z ′ is the set of valuations ν ′ such that there exist ν ∈ Closure M (Z) and δ ∈ R ≥0 satisfying (q, ν) δ,t -→ (q ′ , ν ′ ). Similarly for SG d (A)
and SG a (A) but replacing Closure M with operations Closure d M and Approx M , respectively. The notions of an abstraction of a run of A, and an instance of a path in a simulation graph are defined in the same way as that of region graphs.

Tools like Kronos or Uppaal use Approx M abstraction. The two others are less interesting for implementations since the result may not be convex. Nevertheless, they are useful in proofs. The following lemma (cf. [START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF]) says that transitions in SG(A) are post-stable with respect to regions. Lemma 4. Let (q, S) t -→ (q ′ , S ′ ) be a transition in SG(A). For every region r ′ ⊆ S ′ , there is a region r ⊆ S such that (q, r)

t -→ (q ′ , r ′ ) is a transition in RG(A).
We get a correspondence between paths in simulation graphs and runs of A.

Theorem 2 ([16]

). Every path in SG(A) is an abstraction of a run of A, and conversely, every run of A is an instance of a path in SG(A). Similarly for SG d and SG a .

Proof. We first show that a path in SG(A) is an abstraction of a run of A. Take a path (q 0 , S 0 ) t0 -→ (q 1 , S 1 ) t1 -→ . . . in SG(A). Construct a DAG with nodes (i, q i , r i ) such that r i is a region in S i . We put an edge from (i, q i , r i ) to (i + 1, q i+1 , r i+1 ) if (q i , r i ) ti -→ (q i+1 , r i+1 ). By Lemma 4, every node in this DAG has at least one predecessor, and the branching of every node is bounded by the number of regions. Hence, this DAG has an infinite path that is a path in RG(A). By Lemma 2 this path can be instantiated to a run of A.

To conclude the proof one shows that a run of A can be abstracted to a path in SG d (A). Then using Lemma 3 this path can be converted to a path in SG a (A), and later to one in SG(A). We omit the details.

Observe that this theorem does not guarantee that a path we find in a simulation graph has an instantiation that is non-Zeno. It is indeed impossible to guarantee this unless some additional conditions on paths or automata are imposed.

In the subsequent sections, we are interested only in the simulation graph SG a . Observe that the symbolic zone obtained by the approximation of a zone using Approx M is in fact a zone. Hence, we prefer to call it a zone graph and denote it as ZG a . Every node of ZG a is of the form (q, Z) where Z is a zone.

Finding non Zeno paths

As we have remarked above, in order to use Theorem 2 we need to be sure that a path we get can be instantiated to a non-Zeno run. We discuss the solutions proposed in the literature, and then offer a better one. Thanks to pre-stability of the region graph, the progress criterion on regions has been defined in [START_REF] Alur | A theory of timed automata[END_REF] for selecting runs from RG(A) that have a non-Zeno instantiation (see Section 2.2). Notice that the semantics of TBA in [START_REF] Alur | A theory of timed automata[END_REF] constrains all delays δ i to be strictly positive, but the progress criterion can be extended to the stronger semantics that is used nowadays (see [START_REF] Tripakis | Checking timed büchi automata emptiness efficiently[END_REF] for instance). However, since zone graphs are not pre-stable, this method cannot be directly extended to zone graphs.

Adding one clock

A common solution to deal with Zeno runs is to transform an automaton into a strongly non-Zeno automaton, i.e. such that all runs satisfying the Büchi condition are guaranteed to be non-Zeno. We present this solution here and discuss why, although simple, it may add an exponential factor in the decision procedure.

The transformation of A into a strongly non-Zeno automaton SN Z(A) proposed in [START_REF] Tripakis | Checking timed büchi automata emptiness efficiently[END_REF] adds one clock z and duplicates accepting states. One copy of the state is as before but is no longer accepting. The other copy is accepting, but it can be reached only when z ≥ 1. Moreover when it is reached z is reset to 0. The only transition from this second copy leads to the first copy. (See V k and W k on Figure 1 for an example.) This construction ensures that at least one unit of time has passed between two visits to an accepting state. A slightly different construction is mentioned in [START_REF] Alur | Decision problems for timed automata: A survey[END_REF]. Of course one can also have other modifications, and it is impossible to treat all the imaginable constructions at once. Our objective here is to show that the constructions proposed in the literature produce a phenomenon that causes proliferation of zones that can sometimes be exponential in the number of clocks. The discussion below will focus on the construction from [START_REF] Tripakis | Checking timed büchi automata emptiness efficiently[END_REF], but the one from [START_REF] Alur | Decision problems for timed automata: A survey[END_REF] suffers from the same problem.

The problem comes from the fact that the constraint z ≥ 1 may be a source of rapid multiplication of the number of zones in the zone graph of SN Z(A). Consider V k and W k from Figure 1 for k = 2. Starting at the state b 2 of V 2 in the zone 0 ≤ y ≤ x 1 ≤ x 2 , there are two reachable zones with state b 2 . Moreover, if we reset x 1 followed by y from the two zones, we reach the same zone 0

≤ y ≤ x 1 ≤ x 2 . In contrast starting in b 2 of W 2 = SN Z(V 2 ) from . . . c k 0 c k 1 . . . c k k c k y . . . {x k } {x k-1 } {x1} {y} R k b k a k . . . . . . y ≤ d {x1, . . . , x k-1 } V k b k a k 1 a k 2 . . . . . . y ≤ d ∧ z ≥ 1 {z} y ≤ d ∧ z < 1 {x1, . . . , x k-1 } W k = SN Z(V k ) Rn Vn . . . R2 V2 An Rn Wn . . . R2 W2 Bn Fig. 1. Gadgets for A n and B n = SN Z(A n ). 0 ≤ y ≤ x 1 ≤ x 2 ≤
z gives at least d zones, and resetting x 1 followed by y still yields d zones.

We now exploit this fact to give an example of a TBA A n whose zone graph has a number of zones linear in the number of clocks, but B n = SN Z(A n ) has a zone graph of size exponential in the number of clocks. A n is constructed from the automata gadgets V k and R k as shown in Figure 1. Observe that the role of R k is to enforce an order 0 Let us now consider B n , the strongly non-Zeno automaton obtained from A n following [START_REF] Tripakis | Checking timed büchi automata emptiness efficiently[END_REF]. Every gadget V k gets transformed to W k . While exploring W k , one introduces a distance between the clocks x k-1 and x k . So when leaving it one gets zones with x kx k-1 ≥ c, where c ∈ {0, 1, 2, . . . , d}. The distance between x k and x k-1 is preserved by R k . In consequence, W n produces at least d + 1 zones. For each of these zones W n-1 produces d + 1 more zones. In the end, the zone graph of B n has at least (d + 1) n-1 zones at the state b 2 .

≤ y ≤ x 1 ≤ • • • ≤ x k between clock
We have thus shown that A n has O(n) zones while B n = SN Z(A n ) has an exponential number of zones even when the constant d is 1. Observe that the construction shows that even with two clocks the number of zones blows exponentially in the binary representation of d. Note that the automaton A n does not have a non-Zeno accepting run. Hence, every search algorithm is compelled to explore all the zones of B n .

A more efficient solution

Our solution stems from a realization that we only need one non-Zeno run satisfying the Büchi condition and so in a way transforming an automaton to strongly non-Zeno is an overkill. We propose not to modify the automaton, but to introduce additional information to the zone graph ZG a (A). The nodes will now be triples (q, Z, Y ) where Y ⊆ X is the set of clocks that can potentially be equal to 0. It means in particular that other clock variables, i.e. those from X -Y are assumed to be bigger than 0. We write (X -Y ) > 0 for the constraint saying that all the variables in X -Y are not 0. Definition 2. Let A be a TBA over a set of clocks X. The guessing zone graph GZG a (A) has nodes of the form (q, Z, Y ) where (q, Z) is a node in ZG a (A) and Y ⊆ X. The initial node is (q 0 , Z 0 , X), with (q 0 , Z 0 ) the initial node of ZG a (A). There is a transition (q, Z, Y )

t -→ (q ′ , Z ′ , Y ∪ R) in GZG a (A) if there is a transition (q, Z) t -→ (q ′ , Z ′
) in ZG a (A) with t = (q, g, R, q ′ ), and there are valuations ν ∈ Z, ν ′ ∈ Z ′ , and δ such that ν + δ (X -Y ) > 0 and

(q, ν)

δ,t
-→ (q, ν ′ ). We also introduce a new auxiliary letter τ , and put transitions

(q, Z, Y ) τ -→ (q, Z, Y ′ ) for Y ′ = ∅ or Y ′ = Y .
Observe that the definition of transitions reflects the intuition about Y we have described above. Indeed, the additional requirement on the transition (q, Z, Y ) t -→ (q ′ , Z ′ , Y ∪ R) is that it should be realizable when the clocks outside Y are strictly positive; so there should be a valuation satisfying (X -Y ) > 0 that realizes this transition. As we will see later, this construction entails that from a node (q, Z, ∅) every reachable zero-check is preceded by the reset of the variable that is checked, and hence nothing prevents a time elapse in this node. A node of the form (q, Z, ∅) is called clear. We call a node (q, Z, Y ) accepting if it contains an accepting state q.

Example. Figure 2 depicts a TBA A 1 along with its zone graph ZG a (A 1 ) and its guessing zone graph GZG a (A 1 ) where τ -loops have been omitted.

a b x ≥ 1 x ≤ 1 {x} A1 a, x = 0 b, x ≥ 1 x ≥ 1 x ≤ 1 {x} ZG a (A1) a, x = 0, {x} a, x = 0, ∅ b, x ≥ 1, {x} b, x ≥ 1, ∅ x ≥ 1 τ x ≥ 1 x ≤ 1 {x} τ x ≤ 1 { x } GZG a (A1)
Fig. 2. A TBA A 1 and the guessing zone graph GZG a (A 1 ).

Notice that directly from the definition it follows that a path in GZG a (A) determines a path in ZG a (A) obtained by removing τ transitions and the third component from nodes.

A variable x is bounded by a transition of GZG a (A) if the guard of the transition implies x ≤ c for some constant c. More precisely: for (q, Z, Y ) (q,g,R,q ′ ) ------→ (q ′ , Z ′ , Y ′ ), the guard g implies (x ≤ c). A variable is reset by the transition if it belongs to the reset set R of the transition.

We say that a path is blocked if there is a variable that is bounded infinitely often and reset only finitely often by the transitions on the path. Otherwise the path is called unblocked.

Theorem 3.

A TBA A has a non-Zeno run satisfying the Büchi condition iff there exists an unblocked path in GZG a (A) visiting both an accepting node and a clear node infinitely often.

The proof of Theorem 3 follows from Lemmas 5 and 6 below. We omit the proof of the first of the two lemmas and concentrate on a more difficult Lemma 6. It is here that the third component of states is used.

At the beginning of the section we had recalled that the progress criterion in [START_REF] Alur | A theory of timed automata[END_REF] characterizes the paths in region graphs that have non-Zeno instantiations. We had mentioned that it cannot be directly extended to zone graphs since their transitions are not pre-stable. Lemma 6 below shows that by slightly complicating the zone graph we can recover a result very similar to Lemma 4.13 in [START_REF] Alur | A theory of timed automata[END_REF]. Lemma 5. If A has a non-Zeno run satisfying the Büchi condition, then in GZG a (A) there is an unblocked path visiting both an accepting node and a clear node infinitely often. Lemma 6. Suppose GZG a (A) has an unblocked path visiting infinitely often both a clear node and an accepting node then A has a non-Zeno run satisfying the Büchi condition.

Proof. Let σ be a path in GZG a (A) as required by the assumptions of the lemma (without loss of generality we assume every alternate transition is a τ transition):

(q 0 , Z 0 , Y 0 ) τ -→ (q 0 , Z 0 , Y ′ 0 ) t0 -→ • • • (q i , Z i , Y i ) τ -→ (q i , Z i , Y ′ i ) ti -→ • • •
Take a corresponding path in ZG a (A) and one instance ρ = (q 0 , ν 0 ), (q 1 , ν 1 ) . . . that exists by Theorem 2. If it is non-Zeno then we are done. Suppose ρ is Zeno. Let X r be the set of variables reset infinitely often on σ. By assumption on σ, every variable not in X r is bounded only finitely often. Since ρ is Zeno, there is an index m such that the duration of the suffix of the run starting from (q m , ν m ) is bounded by 1/2, and no transition in this suffix bounds a variable outside X r . Let n > m be such that every variable from X r is reset between m and n. Observe that ν n (x) < 1/2 for every x ∈ X r .

Take positions i, j such that i, j > n, Y i = Y j = ∅ and all the variables from X r are reset between i and j. We look at the part of the run ρ:

(q i , ν i ) δi,ti ---→ (q i+1 , ν i+1 ) δi+1,ti+1
------→ . . . (q j , ν j ) and claim that every sequence of the form

(q i , ν ′ i ) δi,ti ---→ (q i+1 , ν ′ i+1 ) δi+1,ti+1 ------→ . . . (q j , ν ′ j )
is a part of a run of A provided there is ζ ∈ R ≥0 such that the following three conditions hold for all k = i, . . . , j:

1. ν ′ k (x) = ν k (x) + ζ + 1/2 for all x ∈ X r , 2. ν ′ k (x) = ν k (x) + 1/2 if
x ∈ X r and x has not been reset between i and k. 3. ν ′ k (x) = ν k (x) otherwise, i.e., when x ∈ X r and x has been reset between i and k.

Before proving this claim, let us explain how to use it to conclude the proof. The claim shows that in (q i , ν i ) we can pass 1/2 units of time and then construct a part of the run of A arriving at (q j , ν ′ j ) where ν ′ j (x) = ν j (x) for all variables in X r , and ν ′ j (x) = ν j (x) + 1/2 for other variables. Now, we can find l > j, so that the pair (j, l) has the same properties as (i, j). We can pass 1/2 units of time in j and repeat the above construction getting a longer run that has passed 1/2 units of time twice. This way we construct a run that passes 1/2 units of time infinitely often. By the construction it passes also infinitely often through accepting nodes.

It remains to prove the claim. Take a transition (q k , ν k )

δ k ,t k ---→ (q k+1 , ν k+1 ) and show that (q k , ν ′ k ) δ k ,t k ---→ (q k+1 , ν ′ k+1
) is also a transition allowed by the automaton. Let g and R be the guard of t k and the reset of t k , respectively.

First we need to show that ν ′ k + δ k satisfies the guard of t k . For this, we need to check if for every variable x ∈ X the constraints in g concerning x are satisfied. We have three cases:

-If x ∈ X r then x is not bounded by the transition t k , that means that in g the constraints on x are of the form (x > c) or (x ≥ c). Since (ν k + δ k )(x) satisfies these constraints so does (ν

′ k + δ k )(x) ≥ (ν k + δ k )(x). -If x ∈ X r
and it is reset between i and k then ν ′ k (x) = ν k (x) so we are done. -Otherwise, we observe that x ∈ Y k . This is because Y i = ∅, and then only variables that are reset are added to Y . Since x is not reset between i and k, it cannot be in Y k . By definition of transitions in GZG a (A) this means that g ∧ (x > 0) is consistent. We have that 0

≤ (ν k + δ k )(x) < 1/2 and 1/2 ≤ (ν ′ k + δ k )(x) < 1. So ν ′ k + δ k satisfies all the constraints in g concerning x as ν k + δ k does.
This shows that there is a transition (q k , ν ′ k )

δ ′ k ,t k ---→ (q k+1 , ν ′ ) for the uniquely determined ν ′ = [R](ν ′ k + δ k ). It is enough to show that ν ′ = ν ′ k+1 .
For variables not in X r it is clear as they are not reset. For variables that have been reset between i and k this is also clear as they have the same values in ν ′ k+1 and ν ′ . For the remaining variables, if a variable is not reset by the transition t k then condition (2) holds. If it is reset then its value in ν ′ becomes 0; but so it is in ν ′ k+1 , and so the third condition holds. This proves the claim.

Finally, we provide an explanation as to why the proposed solution does not produce an exponential blowup. At first it may seem that we have gained nothing because when adding arbitrary sets Y we have automatically caused exponential blowup to the zone graph. We claim that this is not the case for the part of GZG a (A) reachable from the initial node, namely a node with the initial state of A and the zone putting every clock to 0.

We say that a zone orders clocks if for every two clocks x, y, the zone implies that at least one of x ≤ y, or y ≤ x holds.

Lemma 7. If a node with a zone Z is reachable from the initial node of the zone graph ZG a (A) then Z orders clocks. The same holds for GZG a (A).

Suppose that Z orders clocks. We say that a set of clocks Y respects the order given by Z if whenever y ∈ Y and Z implies x ≤ y then x ∈ Y . Lemma 8. If a node (q, Z, Y ) is reachable from the initial node of the zone graph GZG a (A) then Y respects the order given by Z.

Lemma 7 follows since a transition from a zone that orders clocks gives back a zone that orders clocks, and the Approx M operator approximates it again to a zone that orders clocks. Notice that the initial zone clearly orders clocks. The proof of Lemma 8 proceeds by an induction on the length of a path. The above two lemmas give us the desired bound. The theorem follows directly from the above two lemmas. Of course, imposing that zones have ordered clocks in the definition of GZG a (A) we would get the same bound for the entire GZG a (A).

Algorithm

We use Theorem 3 to construct an algorithm to decide if an automaton A has a non-Zeno run satisfying the Büchi condition. This theorem requires to find an unblocked path in GZG a (A) visiting both an accepting state and a clear state infinitely often. This problem is similar to that of testing for emptiness of automata with generalized Büchi conditions as we need to satisfy two infinitary conditions at the same time. The requirement of a path being unblocked adds additional complexity to the problem. The best algorithms for testing emptiness of automata with generalized Büchi conditions are based on strongly connected components (SCC) [START_REF] Schwoon | A note on on-the-fly verification algorithms[END_REF][START_REF] Gaiser | Comparison of algorithms for checking emptiness on büchi automata[END_REF]. So this is the way we take here.

We apply a variant of Tarjan's algorithm for detecting maximal SCCs in GZG a (A). During the computation of the maximal SCCs, we keep track of whether an accepting node and a clear node have been seen. For the unblocked condition we use two sets of clocks U B Γ and R Γ that respectively contain the clocks that are bounded and the clocks that are reset in the SCC Γ . At the end of the exploration of Γ we check if:

1. we have passed through an accepting node and a clear node, 2. there are no blocking clocks: U B Γ ⊆ R Γ .

If the two conditions are satisfied then we can conclude saying that A has an accepting non-Zeno run. Indeed, a path passing infinitely often through all the nodes of Γ would satisfy the conditions of Theorem 3, giving a required run of A. If the first condition does not hold then the same theorem says that Γ does not have a witness for a non-Zeno run of A satisfying the Büchi condition.

The interesting case is when the first condition holds but not the second. We can then discard from Γ all the edges blocking clocks from U B Γ -R Γ , and reexamine it. If Γ without discarded edges is still an SCC then we are done. If not we restart our algorithm on Γ with the discarded edges removed. Observe that we will not do more than |X| restarts, as each time we eliminate at least one clock. If after exploring the entire graph, the algorithm has not found a subgraph satisfying the two conditions then it declares that there is no run of A with the desired properties. Its correctness is based on Theorem 3.

Recall that by Theorem 4 the size of GZG a (A) is |ZG a (A)| • |X|. The complexity of the algorithm follows from the complexity of Tarjan's algorithm and the remark about the number of recursive calls being bounded by the number of clocks. We hence obtain the following.

Conclusions

Büchi non-emptiness problem is one of the standard problems for timed automata. Since the paper introducing the model, it has been widely accepted that addition of one auxiliary clock is an adequate method to deal with the problem of Zeno paths. This technique is also used in the recently proposed zone based algorithm for the problem [START_REF] Tripakis | Checking timed büchi emptiness on simulation graphs[END_REF].

In this paper, we have argued that in some cases the auxiliary clock may cause exponential blowup in the size of the zone graph. We have proposed another method that is based on a modification of the zone graph. The resulting graph grows only by a factor that is linear in the number of clocks. In our opinion, the efficiency gains of our method outweigh the fact that it requires some small modifications in the code dealing with zone graph exploration.

It is difficult to estimate how often introducing the auxiliary clock may cause an exponential blowup. The example in Figure 1 suggests that the problem appears when there is a blocked cycle containing an accepting state. A prototype implementation of our algorithm shows that a blowup occurs in the Train-Gate example (e.g. [START_REF] Gómez | Efficient detection of zeno runs in timed automata[END_REF]) when checking for bounded response to train access requests. For 2 trains, the zone graph has 988 zones whereas after adding the auxiliary clock it blows to 227482 zones. The guessing zone graph has 3840 zones. To be fair, among the 227482 zones, 146061 are accepting with a self-loop, so in this example any on-the-fly algorithm should work rather quickly. Our prototype visits 1677 zones (in 0.42s). The example from Figure 1 with n = 10 and d = 1 has a zone graph with 151 zones and a guessing zone graph with 1563 zones. Its size grows to 36007 when adding the extra clock. Raising d to 15, we obtain 151, 1563 and 135444 zones respectively, which confirms the expected blowup.

It is possible to apply the modification to the zone graph on-the-fly. It could also be restricted only to strongly connected components having "zero checks". This seems to be another source of big potential gains. We are currently working on an on-the-fly optimized algorithm. The first results are very encouraging. Often our prototype implementation solves the emptiness problem at the same cost as reachability when the automaton has no Zeno accepting runs. For instance, the zone graph for Fischer's protocol with 4 processes has 46129 zones and is computed in 14.22s1 . To answer the mutual exclusion problem it is necessary to visit the entire zone graph. Our algorithm does it in 15.77s. Applying the construction from [START_REF] Tripakis | Checking timed büchi automata emptiness efficiently[END_REF] we get the graph with 96913 zones, and it takes 37.10s to visit all of them. Hence, even in this example, where all the runs are non-Zeno, adding one clock has a noticeable impact. In this section, we describe the zone graphs of the gadgets V and W shown in Figure 3. Observe that they correspond to gadgets V 2 and W 2 in Figure 1. Figure 4 gives the set of zones obtained by successive transitions of V starting from the zone (b, 0 ≤ y ≤ x 1 ≤ x 2 ). After two traversals of the cycle formed by b and a in V, we reach a zone that was already seen. Hence we have just two different zones with the state b. ZG(W) in Figure 5 gives the sequence of transitions in the zone graph of W starting from the zone (l 0 , 0 ≤ y ≤ x 1 ≤ x 2 ≤ z). After a certain point, every traversal induces an extra distance between the clocks y and z. Clearly, there are at least d zones in this case.

b 0 ≤ y ≤ x1 ≤ x2 a 0 ≤ y ≤ x1 ≤ x2 ∧ y ≤ d b 0 = x1 ≤ y ≤ x2 a 0 ≤ x1 ≤ y ≤ x2 ∧ y ≤ d . . . . . . . . . y ≤ d {x1} y ≤ d {x1} Fig. 4. Part of ZG(V). . . . . . . b 0 ≤ y ≤ x1 ≤ x2 ≤ z a1 0 = z ≤ y ≤ x1 ≤ x2 ∧ y ≤ d a2 0 ≤ z ≤ y ≤ x1 ≤ x2 . . . b 0 = x1 ≤ z ≤ y ≤ x2 a1 0 = z ≤ x1 ≤ y ≤ x2 ∧ y -z ≥ 1 ∧ y ≤ d a2 0 ≤ z ≤ x1 ≤ y ≤ x2 ∧ y -z ≥ 1 . . . b 0 = x1 ≤ z ≤ y ≤ x2 ∧ y -z ≥ 1 . . . . . . . . . b 0 = x1 ≤ z ≤ y ≤ x2 ∧ y -z ≥ d -1 a1 0 = z ≤ x1 ≤ y ≤ x2 ∧ y -z = d ∧ y = d a2 0 ≤ z ≤ x1 ≤ y ≤ x2 ∧ y -z = d . . . b 0 = x1 ≤ z ≤ y ≤ x2 ∧ y -z = d y ≤ d ∧ z ≥ 1 {z} {x 1 } y ≤ d ∧ z ≥ 1 {z} {x 1 } y ≤ d ∧ z ≥ 1 {z} {x 1 } y ≤ d ∧ z ≥ 1 {z} {x 1 } Fig. 5. Part of ZG(W).
Take now the automaton B n considered in Figure 1. The set of zones obtained with the state b k is 0

= x 1 = . . . = x k-1 ≤ z ≤ y ≤ x k ≤ . . . ≤ x n ∧ x n -x n-1 ≥ c 1 ∧ x n-1 -x n-2 ≥ c 2 . . . . . . ∧ x k+2 -x k+1 ≥ c n-k-1 ∧ x k+1 -x k ≥ c n-k ∧ y -z ≥ c n-k+1
where c i ∈ {0, 1, 2, . . . , d} for i ∈ {1, . . . , nk + 1}. So the zone graph has at least (d + 1) n-k+1 zones at the state b k . Hence, the zone graph of SN Z(B n ) contains at least (d + 1) n-1 zones.

B Another example of a blowup

We take a simple automaton U, shown in Figure 6. Due to the inherent non determinism, one obtains n! zones at a that describe an ordering of the form x i1 ≤ x i2 . . . ≤ x in with {i 1 , i 2 , . . . , i n } = {1, 2, . . . , n}. U has a Zeno cycle between a and b, with b being the only accepting state. Obviously, any algorithm that searches for a non-Zeno accepting cycle has to explore the entire zone graph. Consequently, an algorithm that first transforms U into a strongly non-Zeno automaton needs to explore at least n!(d-1) n zones. This is because the modified automaton SN Z(U) yields a zone graph that includes zones describing distances, similar to the case shown in Figure 3. Note that the zone graph of U has O(n!) number of zones. We hence see an exponential blowup in this case too, although it is somehow hiden in the size of the original graph.

C Examples of guessing zone graphs

At the beginning of Section3 we had recalled that the progress criterion in [START_REF] Alur | A theory of timed automata[END_REF] characterizes the paths in region graphs that have non-Zeno instantiations. We had mentioned that it cannot be directly extended to zone graphs since their transitions are not pre-stable. Theorem 3 and Lemma 6 show that by slightly complicating the zone graphs we can recover a result very similar to Lemma 4.13 in [START_REF] Alur | A theory of timed automata[END_REF]. We would like to illustrate the construction with several examples. -----→ a time must not elapse in b. This emphasizes that ZG a (A 1 ) is not pre-stable since not all valuations in (b, x ≥ 1) have a successor following this transition. Notice that GZG a (A 1 ) is also not pre-stable. Moreover, the third component Y does not help to detect that time cannot elapse in b as in GZG a (A 1 ) the transition is allowed for both Y = {x} and Y = ∅. However, as soon as an SCC contains a transition x ≥ 1 and a transition that resets x, it has a non-Zeno run, and the third component does not play any role.

C.1 On Pre-and Post-Stability

The third component is only useful for the case where an SCC contains no transition with a guard implying x > 0 for some clock x that is also reset on some transition in the SCC. In such a case, zero checks may prevent time to elapse. We illustrate this case on the next two examples that emphasize how the third component added to the states of the zone graph allows to distinguish between Zeno runs and non-Zeno runs.

C.2 A Zeno TBA with Zero Checks

The TBA A 2 below only has one infinite run that is Zeno as time does not elapse at all. This is detected in GZG a (A 2 ) as all states in the only non-trivial SCC have Y = {x, y} as the third component. This means that from every state there exists a reachable zero check that is not preceded by the corresponding reset, hence preventing time to elapse. Notice that the correctness of this argument relies on the fact that for every (q, Z, Y ) in GZG a (A 2 ), and for every transition t = (q, g, R, q ′ ), even if t is fireable in ZG a (A 2 ) from (q, Z), it must also be fireable under the supplementary hypothesis (X -Y ) > 0 given by Y in GZG a (A 2 ). Notice that τ -loops in GZG a (A 2 ) have not been represented for clarity of the figure.

C.3 A non-Zeno TBA with Zero Checks

The TBA A 3 below admits a non-Zeno run. This can be read from GZG a (A 3 ) since the SCC composed of the four zones with Y = {x, y} on the one hand, and (z 2 , ∅) and (z 3 , {y}) on the other hand, contains a clear state. This is precisely the state where time can elapse as every reachable zero check is preceded by the corresponding reset.

D Proofs from Section 3

Proof (Of Lemma 5). Let ρ be a non-Zeno run of A:

(q 0 , ν 0 ) δ0,t0 ---→ (q 1 , ν 1 ) δ1,t1 ---→ • • • By Theorem 2, it is a concretization of a path σ in ZG a (A):

(q 0 , Z 0 ) t0 -→ (q 1 , Z 1 ) t1 -→ • • •
Let σ ′ be the following sequence:

(q 0 , Z 0 , Y 0 ) τ -→ (q 0 , Z 0 , Y ′ 0 ) t0 -→ (q 1 , Z 1 , Y 1 ) τ -→ (q 1 , Z 1 , Y ′ 1 ) t1 -→ • • •
where Y 0 = X, Y i is determined by the transition, and Y ′ i = Y i unless δ i > 0 when we put Y ′ i = ∅. We need to see that this is indeed a path in GZG a (A).

  values. By induction on k one can compute that there are only two zones at locations b k since R k+1 made the two zones in b k+1 collapse into the same zone in b k . Hence the number of nodes in the zone graph of A n is O(n).

Theorem 4 .

 4 Let |ZG a (A)| be the size of the zone graph, and |X| be the number of clocks in A. The number of reachable nodes of GZG a (A) is bounded by |ZG a (A)|.(|X| + 1).

Theorem 5 .

 5 The above algorithm is correct and runs in time O(|ZG a (A)|.|X| 2 ).

Fig. 3 .

 3 Fig. 3. Construction adding one clock

Fig. 6 .

 6 Fig. 6. The TBAs U and SN Z(U).

Figure 2

 2 Figure 2 depicts a TBA A 1 along with ZG a (A 1 ) and GZG a (A 1 ) (where the τ -loops have been omitted). In order to fire transition b x≤1,{x}

2 z2

 2 : (1, 0 = x ≤ y), ∅ z2, {x} z2, {x, y} z1 : (0, 0 = x = y), ∅ z1, {x, y} z3 : (2, 0 = y ≤ x), ∅ z3, {y} z3, {x,Reachable part of GZG a (A 2 )

  2, 0 = x = y), ∅ z2, {x, y} z3 : (0, 0 = y ≤ x), ∅ z3, {y} z3, {x, y} z4 : (1, 0 = x ≤ y), ∅ z4, {x} z4, {x, y} z1 : (0, 0 = x = y), ∅ z1, {x, y} {x} Reachable part of GZG a (A 3 )Notice that τ -loops in GZG a (A 3 ) have not been represented for clarity of the figure.

On a

2.4GHz Intel Core 2 Duo MacBook with 2GB of memory.

For this we need to see that every transition (q i , Z i , Y ′ i ) t0 -→ (q i+1 , Z i+1 , Y i+1 ) is realizable from a valuation ν such that ν (X -Y ′ i ) > 0. But an easy induction on i shows that actually ν i (X -Y ′ i ) > 0. Since σ is non-Zeno there are infinitely many i with Y ′ i = ∅. It is also straightforward to check that ρ is unblocked.

Proof (Of Lemma 7). First notice that in the initial zone, all the clocks are equal to each other. Now, consider any zone Z that orders clocks. Let (q, Z) t -→ (q ′ , Z ′ ) be a transition of ZG a . This means that (q, Z)

. Directly from the definition of transitions we have that Z ′ 1 orders clocks. It remains to check that, the clock ordering in

. Suppose not, then for an ordering constraint c satisfied by Z ′ , Z ′ ∧ c would be a smaller convex zone in R d M that contains Z ′ 1a contradiction. Finally, for every node (q, Z, Y ) in GZG a (A), (q, Z) is reachable in ZG a (A).

Proof (Of Lemma 8). The proof is by induction on the length of a path. In the initial node (q 0 , Z 0 , X), the set X obviously respects the order as it is the set of all clocks. Now take a transition (q, Z, Y ) t -→ (q ′ , Z ′ , Y ′ ) with Y respecting the order in Z. We need to show that Y ′ respects the order in Z ′ . By the definition of transitions in GZG a (A) there are ν ∈ Z, ν ′ ∈ Z ′ and δ such that (q, ν) δ,t -→ (q ′ , ν ′ ) and ν + δ (X -Y ) > 0. Take y ∈ Y ′ and suppose that Z ′ implies x ≤ y for some clock x. There are three cases depending on which of the variables y, x are being reset by the transition.

If x is reset by the transition then, by definition x ∈ Y ′ . If y is reset then Z ′ implies y = 0. Hence Z ′ implies that x = 0. Since x is not reset, Z implies x = 0. We are done, since Y preserves the ordering.

The remaining case is when none of the variables is reset by the transition. As ν ′ ∈ Z ′ , we have that ν ′ x ≤ y; and in consequence ν x ≤ y. Since Z orders clocks and ν ∈ Z, we must have that Z implies x ≤ y. As y has not been reset, y ∈ Y . By assumption that Y orders clocks, x ∈ Y .


Denis Geraads
email: denis.geraads@evolhum.cnrs.fr

Biogeographic relationships of Pliocene and Pleistocene North-western African Mammals

Keywords:

North-western Africa, today included in the Palaearctic realm, is well separated from the Ethiopian province by the Sahara, but the distribution of large mammals shows that these biogeographic domains cannot simply be extrapolated to the late Cenozoic. In the latest Miocene and earliest Pliocene, there were close connections with central Africa, but also remarkable similarities with East Africa, in some instances reaching the species level. There is no evidence of northern influence among large mammals, although several small mammals had a wide range in the Mediterranean. East African or pan-African forms are also largely predominant in the well sampled Late Pliocene, their low diversity resulting probably from local environmental conditions. There are but a few immigrants from Eurasia, mostly carnivores. During the Early Pleistocene, limited exchanges occur with the Middle East, but many more with the rest of Africa. By the Middle Pleistocene similarities with East Africa reach their climax, and it is only with the latest part of this period that some northern immigrants put a Palaearctic stamp on this fauna, the "Ethiopian" character of which decreases by extinction of many of its elements.

Introduction

The present-day Sahara, the largest dry desert in the World, is the main geographic feature of Africa, establishing between areas at higher and lower attitudes a biogeographic barrier far more efficient than, e.g., the East African rift. It separates a southern, so-called Ethiopian faunal realm from the Palaearctic one, which incorporates the areas south of the Mediterranean. I believe that looking at such a formidable barrier today has influenced many conceptions about the past biogeographic relationships of North African mammals. In spite of the abundant evidence showing that, as recently as the Holocene, the Sahara was wet and inhabited by a variety of large mammals, the groundless idea that there must have been a proto-Sahara barrier perhaps as early as the Miocene has long been admitted [START_REF] Thomas | Le rôle de barrière écologique de la ceinture saharo-arabique au Miocène: arguments paléontologiques[END_REF][START_REF] Thomas | Origines du peuplement mammalien en Afrique du Nord durant le Miocène terminal[END_REF]. However, no detailed comparison of North-African mammalian faunas with European and Ethiopian ones, supporting a North-South distinction, has ever been undertaken. It is likely that the fact that late Cainozoic North African mammalian faunas were mostly studied by French palaeontologists (the first of whom being Camille Arambourg), more acquainted with European faunas than with East African ones, and more prone to compare the North African ones with the ones they knew best, contributed to increase their apparent Palaearctic aspect.

I shall review below the Late Miocene to Late Pleistocene mammalian faunas of Northwestern Africa, roughly in chronological order. There is virtually no absolute dating for the sites of this area, and all ages are estimated by biochronology but, except for some uncertainties mentioned below, these estimates are rather satisfactory.

-Biogeographic affinities of mammalian faunas

-Late Miocene and Early Pliocene

This period is poorly documented in North Africa. The main site is Sahabi in Libya, referred by [START_REF] Bernor | Zoogeographic Relationships of the Sahabi Large Mammal Fauna (Early Pliocene, Libya)[END_REF] to the Early Pliocene, but now usually referred to the Late Miocene [START_REF] Howell | Preliminary observations on Carnivora from the Sahabi formation (Libya)[END_REF][START_REF] Geraads | Vertébrés fossiles du Miocène supérieur du Djebel Krechem El Artsouma (Tunisie centrale). Comparaisons biostratigraphiques[END_REF], although probably encompassing more than a short time slice. Its African affinities are numerous [START_REF] Geraads | Vertébrés fossiles du Miocène supérieur du Djebel Krechem El Artsouma (Tunisie centrale). Comparaisons biostratigraphiques[END_REF], with for instance Redunca, Damalacra, Stegotetrabelodon, and Brachypotherium, all unknown outside this continent at that time. An antelope assigned to a Eurasian genus (Prostrepsiceros for [START_REF] Lehmann | Fossil Bovidae (Mammalia) from the Mio-Pliocene of Sahabi, Libya[END_REF], Dytikodorcas for [START_REF] Bouvrain | Ruminants (Mammalia, Artiodactyla: Tragulidae, Cervidae, Bovidae) des gisements du Miocène supérieur (Turolien) de Dytiko (Grèce)[END_REF] could well be close instead to the African impala (Aepyceros), thus removing one of the very few northern affinities of the fauna. The Sahabi boselaphine, Tragoportax cyrenaicus, could be closer to the Lothagam one in Kenya [START_REF] Harris | Bovidae from the Lothagam succession[END_REF] than to European forms. Sahabi shares some specific similarities with the fauna of Toros Menalla, in the Late Miocene of Chad. It has an anthracothere [START_REF] Lihoreau | Anthracothere dental anatomy reveals a late Miocene Chado-Libyan bioprovince[END_REF], probably the same species of Machairodus [START_REF] Peigné | A new machairodontine (Carnivora, Felidae) from the Late Miocene hominid locality of TM 266, Toros-Menalla, Chad[END_REF], and a primitive hippotragine, Tchadotragus [START_REF] Geraads | New Hippotragini (Bovidae) from the late Miocene of Toros-Menalla, Chad[END_REF]. This speaks in favour of a Chado-Libyan sub-province within a larger African one, because hipppotragines are unknown outside Africa at that time, and anthracotheres went extinct in Europe much earlier. This is confirmed by the discovery of late Miocene paleo-rivers flowing north into the Mediterranean from paleo-lake Chad [START_REF] Griffin | The late Neogene Sahabi rivers of the Sahara and their climatic and environmental implications for the Chad basin[END_REF], thus providing easy connection for a variety of mammals.

In the Maghreb, no fauna comparable in richness to that of Sahabi is known. Douaria in Tunisia, the age of which is imprecise but certainly in the 5-8 Ma range, yielded an anthracothere [START_REF] Pickford | Revision of the Neogene Anthracotheriidae of Africa[END_REF] and two species of rhinos, one of which (Guérin, 1966, and pers. obs.) is close to brachypotheres, a group which also went extinct in Europe much earlier. In East Africa instead, it survives until the Late Miocene at Lothagam (Harris and Leakey, 2003), and the fauna of Douaria is thus clearly of African character, showing no definite northern influence.

Such northern forms are also absent from the later site of Hamada Damous, in the same country, which yield a suid intermediate between Nyanzachoerus and Notochoerus [START_REF] Coppens | Une nouvelle espèce de Suidé du Villafranchien de Tunisie, Nyanzachoerus jaegeri nov. sp[END_REF]; both genera are best known in Early and Middle Pliocene East African sites, but unknown in Europe.

Further West, at Lissasfa in Morocco, close to the Miocene-Pliocene boundary, we [START_REF] Raynal | Contribution du site paléontologique de Lissasfa (Casablanca, Maroc) à une nouvelle interprétation du Mio-Pliocène de la Méseta[END_REF] discovered a bovine skull close to Ugandax from Central and Eastern Africa, and a canid with upper molars large relative to the carnassial, thus quite distinct from the contemporaneous Spanish form, Canis cipio [START_REF] Pons-Moyá | El Canis cipio Crusafont (1950), comparación con los canidos del Plioceno y Pleistoceno europeo[END_REF].

Lissasfa yielded an interesting rich fauna of rodents (Geraads, 1998b) which allowed its precise dating, but also show that they do not follow the same biogeographic pattern as large mammals. We will see that this difference is a steady feature for the whole late Cainozoic.

Lissasfa yielded one of the earliest Mus of the western part of the Old World, probably originating from the Siwalik Mus, but this microfauna also includes several taxa that are also present in Western Europe, especially in Spain, or elsewhere in the Mediterranean basin, but are wholly unknown in East or South Africa at that time. These are Paraethomys, Ruscinomys, Myocricetodon, and Protatera. Myocricetodon had a much larger range earlier in the Miocene, but the other three genera were definitely involved in a latitudinal dispersal phase in the latest Miocene. Several other rodents, absent from Lissasfa but present in other North African localities, Apodemus, Castillomys, Eliomys, and Stephanomys (Coiffait-Martin, 1991) confirm the existence of rodent exchanges between North-western Africa and Spain (Geraads, 1998a).

Remarkably, very few large mammals were involved in these exchanges. The earliest North African records of the Cercopithecinae Macaca are at Sahabi and at Menacer, a Turolian site in Algeria [START_REF] Thomas | Révision de la faune de mammifères du Miocène supérieur de Menacer (ex-Marceau), Algérie : discussion sur l'âge du gisement[END_REF]; [START_REF] Delson | Evolutionary History of the Cercopithecidae[END_REF] surmised that it could be the vicariant sister-taxon of the Papionini, known further south, but this genus has also been reported from the earliest Pliocene of the Middle Awash in Ethiopia. Its occurrence in the latest Miocene of Casablanca-M in Spain [START_REF] Fortelius | Neogene of the Old World Database of Fossil Mammals (NOW)[END_REF] shows that it certainly crossed the Gibraltar straits.

Hippos followed the same route, as they probably originated in Africa from a form close to the Middle and Late Miocene Kenyapotamus [START_REF] Pickford | On the origins of Hippopotamidae together with decriptions of two new species, a new genus and a new subfamily from the Miocene of Kenya[END_REF], and are present in Spain by the Late Miocene (Venta del Moro, El Arquillo). Camelus (or Paracamelus) is also sometimes cited as an example of trans-Gibraltar connection, but its fossil record in the western part of the Old World is far too incomplete to reconstruct its history. It suddenly appears as early as the latest Miocene in Spain [START_REF] Morales | Camelido finimioceno en Venta del Moro, primera cita para Europa Occidental[END_REF], so that whatever route it followed left no track, which is not surprising, as this group is always quite rare in any site. Subsequent records in the Early Pliocene of Chad [START_REF] Likius | Le plus vieux Camelidae (Mammalia, Artiodactyla) d'Afrique : limite Mio-Pliocène, Tchad[END_REF], and Middle Pliocene of North Africa [START_REF] Arambourg | Vertébrés villafranchiens d'Afrique du Nord -Carnivores, Artiodactyles, Primates[END_REF], could well be the result of a more southern east-west migration. A seemingly Palaearctic element in Pliocene North African faunas is the Caprini of Aïn Brimba in Tunisia [START_REF] Arambourg | Vertébrés villafranchiens d'Afrique du Nord -Carnivores, Artiodactyles, Primates[END_REF].

Caprini have a very sparse record in Africa, but it should be noted that the modern Barbary "sheep", Ammotragus, has been shown to be more distant from goats than previously thought, so that this group could have a long history in Africa (but see below).

-Late Pliocene

Ahl al Oughlam, a fissure filling near Casablanca, is by far the richest site of this period in North Africa, and one of the richest in the Old World, with over 100 vertebrate species, of which 58 are mammals (Geraads, 2006, and refs therein). The large mammals can be divided into 4 groups, according to their biogeographic affinities.

1) Those which already had a very wide distribution before the Late Pliocene, so that it is hard to say if they originate from African forms, or immigrated from elsewhere. Uncertainties may be increased by doubts about the monophyly of some of these genera, which are: Elephas, Anancus, Hystrix, and several carnivores: Hyaenictitherium, Chasmaporthetes, Dinofelis, Felis, Homotherium.

2) Those which are certainly of African origin, as they are known in this continent before the time of Ahl al Oughlam, while they are unknown elsewhere. These include a number of carnivores [START_REF] Geraads | Carnivores du Pliocène terminal de Ahl al Oughlam (Casablanca, Maroc)[END_REF]; see also [START_REF] Hendey | The late Cenozoic Carnivora of the South-Western Cape Province[END_REF][START_REF] Petter | Diversification des Civettes (Carnivora, Viverridae) dans les gisements pléistocènes de l'Omo[END_REF][START_REF] Barry | Large carnivores (Canidae, Hyaenidae, Felidae) from Laetoli[END_REF][START_REF] Petter | Small carnivores (Viverridae, Mustelidae, Canidae) from Laetoli[END_REF] for the other localities): Herpestes, Ichneumia and Genetta (known as early as the Late Miocene), Civettictis (known from Omo as Viverra leakeyi), Crocuta, Panthera, Acinonyx (all known at Laetoli), Vulpes (known from the Late Miocene of Chad: [START_REF] Bonis | The oldest African fox (Vulpes riffautae n.sp., Canidae, Carnivora) recovered in late Miocene deposits of the Djurab desert, Chad[END_REF], Prepoecilogale (known at Laetoli), Mellivora (known in the Early Pliocene of Langebaanweg in South Africa) and probably Ictonyx (Poecilictis), unknown in the Pliocene, but with no extra-African record. Other definitely African forms are: Theropithecus (mostly represented earlier by Th. darti both in East and South Africa: [START_REF] Alemseged | Theropithecus atlanticus (Thomas, 1884) (Primates: Cercopithecidae) from the late Pliocene of Ahl al Oughlam, Casablanca, Morocco[END_REF], Lepus (reported from Kanapoi: Harris et al., 2003), Hipparion pomeli (which belongs to the H. hasumense group, known at Hadar: [START_REF] Eisenmann | The hipparion from the late Pliocene of Ahl al Oughlam, Morocco, and a revision of the relationships of Pliocene and Pleistocene African hipparions[END_REF], Kolpochoerus (with no Pliocene extra-African record), Sivatherium (definitely known at Langebaanweg), and several bovids [START_REF] Geraads | La faune du gisement à Homo erectus de l'Aïn Maarouf, près de El Hajeb (Maroc)[END_REF]: Tragelaphus and Kobus (two African genera first documented at Langebaanweg), and Beatragus (unknown outside Africa). The North African Late Miocene and Early Pliocene record is too patchy to rule out the hypothesis that some of these taxa had a North African origin, but it is likely that most of them arose instead in East or South Africa, later to expand northwards across the present-day Sahara. Non-mammalian Ahl al Oughlam taxa with East African close relatives are the viper Bitis [START_REF] Bailón | Amphibiens et reptiles du Pliocène terminal d'Ahl al Oughlam (Casablanca, Maroc)[END_REF], and the love-birds Agapornis, a genus known only in Africa (C. Mourer-Chauviré, pers. comm.).

3) Those, mostly carnivores, which are probably of northern (European) origin. They include Pliocrocuta, a widespread taxon in Eurasia, but with no record in Africa besides Ahl al Oughlam, Lynx, doubtfully present at Ahl al Oughlam, and known at Çalta and Perpignan [START_REF] Ginsburg | Le gisement de vertébrés pliocènes de Çalta, Ankara, Turquie.5[END_REF], but the systematics of this genus is debated: [START_REF] Morales | Caracal depereti nov. sp. y Felis aff. silvestris (Felidae, Mammalia) del Plioceno inferior de Layna (Soria, España)[END_REF], Nyctereutes, a mainly Eurasian genus, known since the Early Pliocene in Europe before its first (uncertain) record in Africa at Laetoli [START_REF] Barry | Large carnivores (Canidae, Hyaenidae, Felidae) from Laetoli[END_REF], and Ursus, well known in Europe [START_REF] Werdelin | Plio-Pleistocene Carnivora of eastern Africa: species richness and diversity patterns[END_REF], mentioned also an ursine bear from East Africa, but this report is so unexpected that it has to be confirmed). The latter taxon provides the best evidence of crossing of the Gibraltar straits, certainly easy for such a good swimmer. Nyctereutes could have followed the same route, as the species from Ahl al Oughlam bears special resemblance to Spanish forms.

Pliocrocuta could be of Asiatic origin, but systematics of this group is still imperfectly understood. African otters display a clear disjunction in two groups: all North African ones belong to Lutra, a Eurasian genus unknown at that time south of the present-day Sahara, where it is replaced by Aonyx and Enhydriodon, two genera absent from North Africa; needless to say that Lutra is also a good swimmer. 4) Those whose origin is still debatable. There is a medium size canid whose affinities with Canis and "Eucyon" have not yet been fully worked out. Leporids other than Lepus belong either to Serengetilagus (an East African genus) or to Trischizolagus (a Mediterranean one), while Prolagus is a Mediterranean genus. An alcelaphine antelope, referred to Parmularius, a purely African genus, by Geraads and Amani (1998) might belong instead to Damalops, a genus also known in the latest Pliocene of the Siwaliks [START_REF] Pilgrim | The Fossil Bovidae of India[END_REF] and Tajikistan [START_REF] Dmitrieva | Neogene Antelopes of Mongolia and adjacent territories. The joint Soviet-Mongolian Paleontological Expedition[END_REF], but still almost certainly of African origin. The affinities of the Bovini from Ahl al Oughlam are still unclear because no reasonably complete horn-core has been found, but its primitive premolars suggest that they might lie with the "Leptobos" from Eurasia.

In spite of the clear similarities of Ahl al Oughlam with East African faunas, some significant elements of the latter are missing in the Moroccan site. These are first the Hominidae, as there is no evidence whatsoever of human presence at Ahl al Oughlam, all Cercopithecidae other than Theropithecus, Deinotherium, all Suidae except Kolpochoerus, Giraffa, and Aepyceros. Remarkably, most of these taxa, if not all of them, are ecologically linked to at least some kind of wood cover. This is in agreement with the high proportion of alcelaphine and antilopine bovids at Ahl al Oughlam, a definite indicator of dry open landscape, so that their absence in Morocco might be due to local ecological conditions.

The list of genera that are present in Europe and Western Asia in the Late Pliocene, but absent from North Africa, is much longer. It includes many carnivores: the viverrids Viverra and Megaviverra, the felid Puma (or Jansofelis), the canid Cuon (to which can be added Vulpes of alopecoides type, with long carnassials), and the mustelids Baranogale, Martes, Mustela, and Meles. There are also some large ungulates, such as the rhino Stephanorhinus, the proboscidean Mammut (= Zygolophodon), Tapirus, and a cercopithecid primate, Paradolichopithecus. But the main differences lie in the composition of the artiodactyl faunas, whose northern representatives unknown in the Maghreb at this time include the wild boar Sus, perhaps a palaeotragine giraffid (Mitilanotherium), the various members of the family Cervidae, with at least four genera, Cervus, Croizetoceros, Eucladoceros and Alces s.l., of which there is not a single tooth or bone in Africa, and several bovids whose systematic position is not always clear, but which are definitely not members of the dominant African tribes (Tragelaphini, Reduncini, Hippotragini and Alcelaphini): Gazellospira, Procamptoceras, Pliotragus, Gallogoral, Hemitragus, Megalovis, Ovis.

To express more objectively the similarities between Ahl al Oughlam and other sites of comparable age, I have computed some indices from their faunal lists of large mammals. There are many such indices, based upon the number of taxa shared by the two faunal lists (A), and the numbers of taxa peculiar to each of them (B and C). I chose Simpson index of similarity, A / (A + 1: they clearly show that it is with East African that the similarities are greater, in spite of the difference in latitude. Compared with European sites, even those of closely similar age, the indices are much smaller. Thus, the difference in faunal composition is quite clear, and so sharp that it cannot merely be explained by differences in ecological conditions. By contrast, the rodents tell again a very different story [START_REF] Geraads | Rongeurs et insectivores (Mammalia) du Pliocène final de Ahl al Oughlam (Casablanca, Maroc)[END_REF]. In spite of the great number of rodent teeth that have been collected by screening, only five species have been found, besides the widespread Hystrix. They mainly belong to lineages already present in earlier sites, such as Mus, also known in East Africa and the Siwaliks, but totally absent from Europe, and Paraethomys, a genus now extinct in Europe, but which will continue in North Africa, as an endemic lineage, until the end of the Middle Pleistocene. Gerbillus also appears there, at about the same time as at Omo in Ethiopia [START_REF] Wesselman | The Omo micromammals[END_REF], and will also have a long history in the Maghreb. Ahl al Oughlam lacks the diversity of murids found in East African sites of this age, but also fully lacks any arvicolid, the dominant group in Europe at that time. Remarkably, this original composition of North African rodent faunas will remain virtually unchanged until the end of the Pleistocene [START_REF] Jaeger | Les Muridae (Mammalia, Rodentia) du Pliocène et du Pléistocène du Maghreb. Origine; Evolution; Données biogéographiques et paléoclimatiques[END_REF]. Other small mammals show less endemicity. Asoriculus, also known in Morocco at Irhoud Ocre, is present in Europe, while Suncus has been described from East Africa [START_REF] Wesselman | The Omo micromammals[END_REF].

B) if B < C or A / (A + C) if C < B,

-Early Pleistocene

Faunas of this period are much less rich than that of Ahl al Oughlam. The stratigraphic succession at Aïn Jourdel in Algeria [START_REF] Thomas | Recherches stratigraphiques et paléontologiques sur quelques formations d'eau douce de l'Algérie[END_REF] includes several levels, the lowest being probably of Late Pliocene age, with a new alcelaphine, likely of East African origin, Oreonagor, and an upper level with Tragelaphus gaudryi, a species well-known at Omo [START_REF] Gentry | The Bovidae of the Omo deposits, Ethiopia[END_REF] in Ethiopia. Aïn Boucherit has one more alcelaphine genus, certainly immigrated from East Africa, Parmularius (described as Redunca eulmensis by [START_REF] Arambourg | Vertébrés villafranchiens d'Afrique du Nord -Carnivores, Artiodactyles, Primates[END_REF], together with a more derived species of Oreonagor. Parantidorcas is certainly an antilopine, but its affinities remain unclear; it could be related to African Antidorcas, although the strong homonymous torsion of its horn-cores reminds of the Late Miocene Eurasian Oioceros. In any case, there are thus at least two more East African immigrant bovids near the Plio-Pleistocene boundary. However, the best evidence for connections between equatorial Africa and the Maghreb at that time is the arrival of hippos of modern type (tetraprotodont Hippopotamus). They are recorded only slightly later, at perhaps 1.4 Ma, in Western Europe (Atapuerca faunal unit 1: Cuenca-Bescós and García, 2007), where they probably arrived from the East, as they are known in the Early Pleistocene of Ubeidiya in Israel [START_REF] Faure | Les Mammifères du Pléistocène inférieur de la vallée du Jourdain à Oubeidiyeh[END_REF] and at Kapetanios in Greece [START_REF] Koufos | Biochronology and succession of the Plio-Pleistocene macromammalian localities of Greece[END_REF].

Indices of similarity (Table 2) are again much greater when compared with East Africa than with Eurasia.

The site of Aïn Hanech, stratigraphically above that of Aïn Boucherit, yielded a fauna ecologically similar to that of the latter level, but rather sharply distinct in its faunal composition, suggesting that they are separated by a significant amount of time, and the fauna of Aïn Hanech, probably the earliest North African site documenting human presence, points to an age of perhaps 1.2 to 1.4 Ma. (Geraads et al., 2004, contra Sahnouni et al., 2002). It attests the first immigration of a large canid, considered as closed to Lycaon by Martínez-Navarro and Rook (2003) but lacking the derived features of this genus, and probably closer to Canis atrox from South Africa, to which it was first referred by [START_REF] Arambourg | Vertébrés villafranchiens d'Afrique du Nord -Carnivores, Artiodactyles, Primates[END_REF]. Other definite immigrants from the south are Oryx, also known in the roughly contemporaneous site of Mansourah [START_REF] Chaid-Saoudi | The fauna and associated artefacts from the lower Pleistocene site of Mansourah (Constantine, Algeria)[END_REF] and the large alcelaphine Numidocapra, of which Aïn Hanech is the typelocality of the type-species, but which is also present in Djibouti [START_REF] Bonis | Vertébrés du Pléistocène de Djibouti[END_REF] and the Middle Awash [START_REF] Vrba | New fossils of Alcelaphini and Caprinae (Bovidae : Mammalia) from Awash, Ethiopia, and phylogenetic analysis of Alcelaphini[END_REF].

There are, however, some possible connections with Eurasia, and especially with the Near East. The bovine described under two different names, Bos bubaloides and B. praeafricanus, by [START_REF] Arambourg | Vertébrés villafranchiens d'Afrique du Nord -Carnivores, Artiodactyles, Primates[END_REF] is probably closer to Eurasian Leptobos than to African Pelorovis, in spite of a similar course of its horn-cores. In any case, Pelorovis is also present at Ubeidiya [START_REF] Geraads | Les Mammifères du Pléistocène inférieur de la vallée du Jourdain à Oubeidiyeh[END_REF]. A very poorly known giraffid, described as Giraffa pomeli by Arambourg but definitely not of this genus, might be close to the Giraffa sp. of Ubeidiya but certainly distinct from East African forms. Giraffids are extinct in Europe at that time. North African representatives of the suid Kolpochoerus seem to belong to a local lineage (Kolpochoerus maroccanus), distinct from the East African ones [START_REF] Geraads | New skulls of Kolpochoerus phacochoeroides (Suidae: Mammalia) from the late Pliocene of Ahl al Oughlam, Morocco[END_REF], but its possible connection with the poorly documented Ubeidiya form remains conjectural. The asinian equid Equus tabeti has been described from both Aïn Hanech (Arambourg, 1970) and Ubeidiya [START_REF] Eisenmann | Les Mammifères du Pléistocène inférieur de la vallée du Jourdain à Oubeidiyeh[END_REF].

However, these similarities should not be overestimated, as the Aïn Boucherit and Aïn Hanech faunas remain very different from the Dmanisi [START_REF] Lordkipanidze | Postcranial evidence from early Homo from Dmanisi, Georgia[END_REF] and Ubeidiya ones, which are almost fully Eurasian in character, with especially an overwhelming majority of cervids among ruminants. Indices of similarity (Table 3) show that these latter sites are still much less similar to Aïn Hanech than are the East African ones.

-Middle Pleistocene

The site of Tighenif (= Ternifine) is still the earliest with fossil hominid remains in North Africa, dated to close to the Early / Middle Pleistocene boundary (Geraads et al., 1985).

Ecologically, the fauna reminds of those of the earlier sites, with a majority of dry open country forms, oryx, gazelles and Alcelaphini. Most of its genera are also found in East and South Africa, the most characteristic ones being: Lycaon, Theropithecus, Ceratotherium, Loxodonta, Metridiochoerus, and most bovids (Tragelaphus, Oryx, Hippotragus, Parmularius, Connochaetes: Geraads, 1981), although its bovine could be a descendant of the one found at Aïn Hanech, perhaps more closely related to European Leptobos than to the African Pelorovis, and its dominant gazelle, G. dracula, could be related to the earlier European G. borbonica [START_REF] Gentry | Evolution and Dispersal of African Bovidae[END_REF]. Trans-African connections far outweigh this only possible evidence of migration from the north, and Tighenif is perhaps the most "East African" of all sites in the Maghreb: the first Eurasian site in Table 4, Ubeidiya, has a far lower similarity index with Tighenif than many East African sites.

Rodents [START_REF] Jaeger | Les Muridae (Mammalia, Rodentia) du Pliocène et du Pléistocène du Maghreb. Origine; Evolution; Données biogéographiques et paléoclimatiques[END_REF][START_REF] Geraads | The pleistocene Hominid site of Ternifine, Algeria: new results on the environment, age, and human industries[END_REF] mostly include North African endemic lineages (Paraethomys, gerbillids) plus an East African murid (Arvicanthis) and the only arvicolid of North Africa, Ellobius, definitely of Central Asiatic origin.

Aïn Maarouf near El Hajeb in Morocco yielded a small fauna [START_REF] Geraads | La faune du gisement à Homo erectus de l'Aïn Maarouf, près de El Hajeb (Maroc)[END_REF] similar to that of Tighenif, but with the addition of a new alcelaphine, Rabaticeras, also reported from a few earlier East and South African sites, testifying to a new immigration from the South.

Recent excavations in the former "Thomas Quarries" near Casablanca allowed refining of the stratigraphy and biochronology of the various archaeological levels in these quarries, now referred to as "Thomas Quarry" (= former Thomas Quarry 1), and "Oulad Hamida 1", (= former Thomas Quarry 3), the latter including mainly the "Grotte des Rhinocéros" [START_REF] Raynal | La grotte des Rhinocéros (carrière Oulad Hamida 1, anciennement Thomas III, Casablanca), nouveau site acheuléen du Maroc atlantique[END_REF][START_REF] Rhodes | New age estimates for the Paleolithic assemblages and Pleistocene succession of Casablanca, Morocco[END_REF]. Although definitely of various ages, all these levels are younger than Tighenif, from which they can be distinguished by a significant, but not major, turnover:

Metridiochoerus is replaced by Phacochoerus, the origin of which is certainly to be sought close to the East African M. hopwoodi, while Kolpochoerus survives; the most common alcelaphine looks close to a strange form from the Okote member of Koobi Fora, referred to ? Damaliscus by [START_REF] Harris | Family Bovidae[END_REF]. The strongest evidence of a European immigration is a lynx [START_REF] Geraads | Un nouveau félidé (Fissipeda, Mammalia) du Pléistocène du Maroc : Lynx thomasi n.sp[END_REF] which might share a relatively recent common ancestry with the modern Spanish Lynx pardina.

Despite recent claims to the contrary [START_REF] Martínez-Navarro | The Olduvai buffalo Pelorovis and the origin of Bos[END_REF] I do not believe that the origin of Bos is to be sought in Africa, the Middle Pleistocene East African Bos (Geraads et al., 2004) being probably of Asiatic origin, while North African late Middle Pleistocene Bos primigenius probably came from Eurasia.

Among rodents, Eliomys re-appears for the first time since the earliest Pliocene, but its similarities with the garden dormouse of the Balearic Islands suggest a new immigration.

5 -Late Pleistocene

Several new taxa appear during this period, but the documentation during the latter part of the Middle Pleistocene is relatively poor, and they might in fact have arrived earlier. Among bovids, the giant buffalo Pelorovis (or Syncerus) antiquus, and the hartebeest Alcelaphus definitely came from East Africa, where they are known much earlier [START_REF] Gentry | Fossil Bovidae (Mammalia) of Olduvai Gorge, Tanzania. Part I[END_REF][START_REF] Vrba | New fossils of Alcelaphini and Caprinae (Bovidae : Mammalia) from Awash, Ethiopia, and phylogenetic analysis of Alcelaphini[END_REF]. Ammotragus could be the end product of a North African caprine lineage, or alternatively could be of European origin, as the genus has recently been reported from Le Vallonnet, a ca. 1 Ma site in Southern France [START_REF] Moullé | Ammotragus europaeus : une nouvelle espèce de Caprini (Bovidae, Mammalia) du Pléistocène inférieur à la grotte du Vallonnet (France)[END_REF]. Two deer, a small variety of the red deer Cervus elaphus, and a megacerine, Megaceroides algericus, also appear during this period, although the precise date of their arrival is unknown. Deer are good swimmers, and the Gibraltar straits, only about 15 km wide at its narrowest stage, was certainly not impassable, neither for them, nor for Sus, which has been reported from the late Middle Pleistocene [START_REF] Michel | Contribution à l'étude paléontologique des Vertébrés fossiles du Quaternaire marocain à partir de sites du Maroc atlantique, central et oriental[END_REF], and persists until the present-day. This crossing is much less likely for the rhino Stephanorhinus, certainly present during the first half of the Late Pleistocene, and its occurrence at Haua Fteah [START_REF] Klein | Re-analysis of Faunal Assemblages from the Haua Fteah and other Late Quaternary Archaeological Sites in Cyrenaican Libya[END_REF] in Eastern Libya suggests that it came from the east, following the southern Mediterranean shore. These new immigrants increase the Palaearctic component in North-western African faunas, while the "Ethiopian" component decreases because of the extinction of several of its elements in the course of the Late Pleistocene:

Tragelaphini, Hippotragus, Reduncini, Camelus (later re-introduced as a domestic form), Phacochoerus, hippos, Ceratotherium, all disappear before historic times. So, although there is no definite new evidence of immigration from the south during this period, it might well be that this faunal turnover was more related to climatic change in the area itself than to the establishment of the Sahara barrier, the loss of diversity experienced by both the large and small mammals being a clear indicator of environmental stress.

-Conclusion

From the Late Miocene to the Middle Pleistocene, many new lineages of large mammals arose throughout Africa, but most of the centers of origins were probably located in the eastern part of the continent. Then, they expanded their ranges within Africa, as far as no geographical or ecological barrier stopped them. The regular immigration of these new taxa of southern origin in the north-western part of the continent demonstrates that no such efficient barrier can have existed for any long period. This does not mean that there was no desert in the Sahara area: indeed, recent finds have demonstrated the occurrence of desertification as early as the Miocene [START_REF] Schuster | The age of the Sahara desert[END_REF] but the mammalian evidence demonstrates that these desert zones were either not large or not permanent enough to set a barrier preventing migration across it. Our present-day conception of the Sahara is clearly not applicable to this period. Surprisingly, the human fossil evidence in North-western Africa does not seem to conform to this biogeographic history based upon regular latitudinal exchanges. The complete absence of Hominids at Ahl al Oughlam is most unexpected, given the strong East African aspect of the fauna of this site, which is so rich that this can probably be taken as an evidence of absence of hominids in North Africa at that time. As noted above, other eastern African taxa that are lacking at Ahl al Oughlam are those that require some amount of tree cover, and this suggests that the dominant physiognomy of the landscape in North-western Africa in the late Pliocene / early Pleistocene was very open. By contrast, the abundance of cervids in early Eurasian hominid-bearing sites such as Dmanisi or Ubeidiyeh testifies to the preference of early Homo for some wood cover, and their immediate ancestors by the time of Ahl al Oughlam may have had similar requirements, although the presence of Australopithecus in Chad in sites wholly lacking woodland bovids [START_REF] Geraads | Pliocene Bovidae (Mammalia) from the Koro-Toro Australopithecine sites, Chad[END_REF] precludes any simple interpretation.

Based upon present knowledge, it is only in the middle part of the Early Pleistocene that hominids appear in North Africa, at Aïn Hanech and Mansourah but, since the environment of these sites was not significantly more wooded than that of Ahl al Oughlam, this can perhaps be seen as an evidence of their increasing adaptability. Later, North African Homo mauritanicus may have followed his own local evolution, without any further connection with African and Eurasian members of the genus. Obviously, environmental conditions were no longer the main determinant of the geographic distribution of these hominids.

Figure captions

Fig. 1. Situation of the localities mentioned in Tables 1234. Fig. 2. Range of some North-African mammalian taxa, together with their range (when larger) in the rest of Africa (dotted line) and in Eurasia (dashed line). The main sites are listed at left at their approximate chronological position, but they may not sample all contemporaneous taxa. Chronological scale is logarithmic.

  and Pickford index of distance, transformed to 1-(Pickford index) for homogeneity, thus becoming A(A + B + C) / (A + B)(A + C). They are less sensitive to unequal sampling than some other commonly used indices. Results, at generic level, are provided in Table

Table 1 .

 1 Simpson index of similarity and 1-(Pickford index of distance) of Ahl al Oughlam compared with some North African (AFN), Central African (AFC), East African (AFE), South African (AFS), Western European (EURW), Eastern European (EURE), and Central Asian (ASC) sites of comparable age. Faunal lists have been updated from a variety of sources.

		AHL AL OUGHLAM
	SIMPSON INDEX		1-PICKFORD INDEX
	Turkana Late Plioc.	AFE	0.737	Turkana Late Plioc.	AFE	0.825
	Turkana Early Pleisto.	AFE	0.632	Peninj	AFE	0.799
	Aïn Boucherit	AFN	0.615	Ichkeul+Brimba	AFN	0.789
	Ichkeul+Brimba	AFN	0.6	Aïn Boucherit	AFN	0.777
	Bouri-Hata	AFE	0.579	Hadar-KH	AFE	0.776
	Konso Gardula 1 2	AFE	0.579	Tighenif	AFN	0.776
	Peninj	AFE	0.579	Turkana Early Pleisto.	AFE	0.754
	Hadar-KH	AFE	0.526	Bouri-Hata	AFE	0.744
	Tighenif	AFN	0.526	Konso Gardula 1 2	AFE	0.744
	Chiwondo3A	AFS	0.474	Olduvai up. + mid. bed II AFE	0.699
	Hadar-DD	AFE	0.474	Hadar-SH	AFE	0.689
	Hadar-SH	AFE	0.474	Hadar-DD	AFE	0.671
	Laetoli upper bed	AFE	0.474	Chiwondo3A	AFS	0.637
	Olduvai up. + mid. bed II AFE	0.474	Laetoli upper bed	AFE	0.637
	Aïn Hanech	AFN	0.462	Aïn Hanech	AFN	0.632
	Koro-Toro	AFC	0.429	Koro-Toro	AFC	0.609
	Olduvai bed I	AFE	0.368	Olduvai bed I	AFE	0.601
	Ubeidiya	EURE 0.333	Ubeidiya	EURE 0.544
	Makapan 3-4	AFS	0.263	Makapan 3-4	AFS	0.417
	St Vallier	EURW 0.214	Sterkfontein 4	AFS	0.368
	Sterkfontein 4	AFS	0.211	St Vallier	EURW 0.338
	Atapuerca FU1	EURW	0.2	Atapuerca FU1	EURW 0.284
	La Puebla	EURW 0.182	La Puebla	EURW 0.268
	Almenara	EURW 0.167	Kromdraai A	AFS	0.254
	Kromdraai A	AFS	0.167	Sesklon	EURE 0.254
	Sesklon	EURE 0.167	Kuruksai	ASC	0.225
	Kuruksai	ASC	0.133	Almenara	EURW 0.211
	Kopala 2	ASC	0.111	Kopala 2	ASC	0.158
	Tegelen	EURW 0.111	Tegelen	EURW 0.158
	Chilhac	EURW	0.1	Gerakarou	EURE 0.147
	Gerakarou	EURE	0.1	Podpusk-Lebyazhje	ASC	0.147
	Podpusk-Lebyazhje	ASC	0.1	Chilhac	EURW 0.147
	Senèze	EURW 0.059	Senèze	EURW 0.108
	Dmanisi	EURE	0	Dmanisi	EURE	0
	Livakos	EURE	0	Livakos	EURE	0
	Varshets	EURE	0	Varshets	EURE	0

Table 3 .

 3 Same as for Table 1, but for Aïn Hanech.

			AÏN HANECH
	SIMPSON INDEX		1-PICKFORD INDEX
	Bouri Daka	AFE	0.846	Bouri Daka	AFE	0.917
	Turkana Early Pleisto.	AFE	0.846	Turkana Early Pleisto.	AFE	0.893
	Turkana Late Plioc.	AFE	0.846	Turkana Late Plioc.	AFE	0.886
	Konso Gardula 1 2	AFE	0.769	Aïn Boucherit	AFN	0.852
	Elandsfontein	AFS	0.692	Konso Gardula 1 2	AFE	0.852
	Konso Gardula 3 4	AFE	0.692	Peninj	AFE	0.824
	Olduvai bed IV	AFE	0.692	Elandsfontein	AFS	0.808
	Peninj	AFE	0.692	MK-Garba IV	AFE	0.808
	Aïn Boucherit	AFN	0.615	Olduvai bed IV	AFE	0.808
	MK-Garba IV	AFE	0.615	Konso Gardula 3 4	AFE	0.799
	Tighenif	AFN	0.615	Ubeidiya	EURE 0.786
	Ubeidiya	EURE 0.615	Tighenif	AFN	0.777
	Asbole	AFE	0.538	Asbole	AFE	0.692
	Olduvai up. + mid. bed II AFE	0.538	Olduvai up. + mid. bed II	AFE	0.692
	Ahl al Oughlam	AFN	0.462	Isenya	AFE	0.677
	Isenya	AFE	0.462	Ahl al Oughlam	AFN	0.632
	Mosbach 5	EURW	0.4	Olduvai lower bed II	AFE	0.59
	Bou Knadel	AFN	0.385	Mosbach 5	EURW 0.585
	Olduvai I	AFE	0.385	Bou Knadel	AFN	0.556
	Olduvai lower bed II	AFE	0.385	Olduvai I	AFE	0.547
	Atapuerca FU4 5	EURW 0.333	France MNQ20	EURW 0.492
	Kopala 2	ASC	0.333	Atapuerca FU4 5	EURW 0.487
	Livakos	EURE 0.333	Kopala 2	ASC	0.487
	France MNQ20	EURW 0.308	Livakos	EURE 0.487
	Gerakarou	EURE	0.3	Gerakarou	EURE 0.462
	Untermassfeld	EURW	0.25	Untermassfeld	EURW 0.423
	Dmanisi	EURE 0.231	Dmanisi	EURE 0.396
	Ichkeul+Brimba	AFN	0.231	St Vallier	EURW 0.396
	St Vallier	EURW 0.231	Ichkeul+Brimba	AFN	0.385
	Sterkfontein 4	AFS	0.231	Sterkfontein 4	AFS	0.346
	Tegelen	EURW 0.222	Tegelen	EURW 0.342
	Atapuerca FU1	EURW	0.2	Atapuerca FU1	EURW 0.323
	Chilhac	EURW	0.2	Chilhac	EURW 0.323
	Varshets	EURE 0.167	Senèze	EURW 0.253
	Makapan3-4	AFS	0.154	Varshets	EURE 0.231
	Senèze	EURW 0.154	Makapan 3-4	AFS	0.224
	Apollonia	EURE 0.143	Apollonia	EURE 0.209

Table 4 .

 4 Same as for Table 1, but for Tighenif.

			TIGHENIF
	SIMPSON INDEX		1-PICKFORD INDEX
	Turkana Late Plioc.	AFE	0.947	Turkana Late Plioc.	AFE	0.97
	Turkana Early Pleisto.	AFE	0.842	Elandsfontein	AFS	0.921
	Elandsfontein	AFS	0.789	Turkana Early Pleisto.	AFE	0.912
	Bouri Daka	AFE	0.684	Bouri Daka	AFE	0.855
	Konso Gardula 3 4	AFE	0.684	Konso Gardula 3 4	AFE	0.842
	Peninj	AFE	0.632	Peninj	AFE	0.842
	MK-GarbaIV	AFE	0.625	MK-GarbaIV	AFE	0.822
	Aïn Hanech	AFN	0.615	Aïn Hanech	AFN	0.777
	Olduvai bed IV	AFE	0.579	Ahl al Oughlam	AFN	0.776
	Isenya	AFE	0.533	Olduvai bed IV	AFE	0.772
	Ahl al Oughlam	AFN	0.526	Olduvai up. + mid. bed II	AFE	0.752
	Lainyamok	AFE	0.526	Bou Knadel	AFN	0.737
	Olduvai up. + mid. bed II AFE	0.526	Lainyamok	AFE	0.732
	Bou Knadel	AFN	0.5	Isenya	AFE	0.73
	Olduvai I	AFE	0.474	Olduvai I	AFE	0.723
	Aïn Boucherit	AFN	0.462	Ubeidiya	EURE 0.678
	Ubeidiya	EURE 0.444	Asbole	AFE	0.642
	Asbole	AFE	0.421	Aïn Boucherit	AFN	0.632
	Olduvai lower bed II	AFE	0.4	Olduvai lower bed II	AFE	0.589
	Atapuerca FU4 5	EURW 0.333	Sterkfontein 4	AFS	0.521
	Ichkeul+Brimba	AFN	0.333	Ichkeul+Brimba	AFN	0.509
	Makapan 3-4	AFS	0.316	Makapan 3-4	AFS	0.487
	Sterkfontein 4	AFS	0.316	Atapuerca FU4 5	EURW 0.439
	Atapuerca FU1	EURW	0.3	Atapuerca FU1	EURW 0.411
	Kromdraai A	AFS	0.25	Kromdraai A	AFS	0.368
	Untermassfeld	EURW	0.25	Untermassfeld	EURW 0.368
	Kopala 2	ASC	0.222	Kopala 2	ASC	0.304
	Livakos	EURE 0.222	Livakos	EURE 0.304
	Gerakarou	EURE	0.2	Gerakarou	EURE 0.284
	Mosbach 5	EURW	0.2	Mosbach 5	EURW 0.284
	Apollonia	EURE 0.143	Dmanisi	EURE 0.233
	Dmanisi	EURE 0.143	St Vallier	EURW 0.233
	St Vallier	EURW 0.143	France MNQ20	EURW 0.225
	Vergranne	EURW 0.143	Apollonia	EURE 0.188
	France MNQ20	EURW 0.133	Vergranne	EURW 0.188
	Chilhac	EURW	0.1	Chilhac	EURW 0.112
	Senèze	EURW 0.059	Senèze	EURW 0.108

Acknowledgments I thank J.-P. Brugal and M. R. Palombo for having invited me to contribute this article, which is largely based upon the results of the excavations in Morocco, undertaken in the frame of the "Programme Casablanca", of the INSAP, Rabat, co-directed by F.-Z. Sbihi-Alaoui and J.-P. Raynal. I also thank A. Prieur (Université de Lyon), C. Sagne and C. Argot (Muséum National d'Histoire Naturelle, Paris), M. Boutakiout (Université de Rabat), for access to collections, A. Guillaumont for help with computing indices, and two anonymous reviewers who suggested useful improvements.