Xavier Allamigeon
email: xavier.allamigeon@inria.fr

Axel Legay
email: axel.legay@inria.fr

Uli Fahrenberg
email: ulrich.fahrenberg@inria.fr

Ricardo D Katz
email: katz@cifasis-conicet.gov.ar

Stéphane Gaubert
email: stephane.gaubert@inria.fr

Tropical Fourier-Motzkin elimination, with an application to real-time verification

Keywords: Tropical polyhedra, strict inequalities, Fourier-Motzkin elimination, mean payoff games, real-time verification, timed automata Mathematics Subject Classification 2010: 14T05, 52A01, 52B55

Introduction 1.Tropical convexity

Tropical or max-plus algebra refers to the set R max := R ∪ {-∞} equipped with x ⊕ y := max(x, y) as addition and x ⊗ y := x + y as multiplication (the latter will be also denoted by concatenation xy). In this setting, an inequality constraint on variables x 1 , . . . , x n is said to be (tropically) affine if it is of the form:

a 0 ⊕ a 1 x 1 ⊕ • • • ⊕ a n x n b 0 ⊕ b 1 x 1 ⊕ • • • ⊕ b n x n , (1.1)
or equivalently, with usual notation, max(a 0 , a 1 + x 1 , . . . , a n + x n ) max(b 0 , b 1 + x 1 , . . . , b n + x n ) ,

where a i , b i ∈ R max for i = 0, 1, . . . , n. By analogy with the terminology of usual convex geometry, a tropical (convex) polyhedron is defined as a set composed of all the vectors x ∈ R n max satisfying finitely many such inequalities. An example is depicted on the left-hand side of Figure 1.

Tropical polyhedra and, more generally, tropically convex sets, have been introduced and studied in various contexts, including optimization [START_REF] Zimmermann | A general separation theorem in extremal algebras[END_REF], control theory [START_REF] Cohen | Max-plus algebra and system theory: where we are and where to go now[END_REF], idempotent functional analysis [START_REF] Litvinov | Idempotent functional analysis: an algebraic approach[END_REF], or combinatorics [START_REF] Develin | Tropical convexity[END_REF]. Several basic results of convex analysis and geometry have been shown to have tropical analogues. These include Hahn-Banach [START_REF] Zimmermann | A general separation theorem in extremal algebras[END_REF][START_REF] Litvinov | Idempotent functional analysis: an algebraic approach[END_REF][START_REF] Cohen | Max-plus convex sets and functions[END_REF][START_REF] Develin | Tropical convexity[END_REF], Minkowski [START_REF] Gaubert | The Minkowski theorem for max-plus convex sets[END_REF][START_REF] Butkovič | Generators, extremals and bases of max cones[END_REF][START_REF] Joswig | Tropical halfspaces, in Combinatorial and computational geometry[END_REF], and Carathéodory/Helly-type [START_REF] Briec | B-convexity[END_REF][START_REF] Gaubert | Cyclic projectors and separation theorems in idempotent convex geometry[END_REF][START_REF] Gaubert | Carathéodory, Helly and the Others in the Max-Plus World[END_REF] theorems. Some algorithmic aspects have also been studied (e.g. [START_REF] Butkovič | An elimination method for finding all solutions of the system of linear equations over an extremal algebra[END_REF][START_REF] Joswig | Tropical convex hull computations[END_REF][START_REF] Allamigeon | Computing the vertices of tropical polyhedra using directed hypergraphs[END_REF]). We refer the reader to [START_REF] Allamigeon | Computing the vertices of tropical polyhedra using directed hypergraphs[END_REF] for further references.

Motivation

The present work is motivated by a specific application of tropical algebra to the verification of real-time systems. Indeed, a remarkable property of tropical polyhedra is their ability to concisely encode possibly non-convex sets expressed as disjunctions of closed zones. A closed zone, also known in the literature as polytrope, is a set of vectors x ∈ R n defined by inequalities of the form x i m i , x i M i , and x i k ij + x j , for certain constants m i , M i , k ij ∈ R. More generally, zones are obtained by replacing some of the previous inequalities by strict ones. See the right-hand side of Figure 1 for an illustration. Zones are extensively used in the area of verification of real-time systems, where these systems are modelled by formalisms such as e.g. timed automata [START_REF] Alur | A theory of timed automata[END_REF] or timed Petri nets [START_REF] Bowden | Modelling time in Petri nets[END_REF]. More precisely, zones are used by model checking tools as symbolic states, typically representing infinitely many states of the system. They can be represented using difference-bound matrices (DBM), which are essentially adjacency matrices of weighted graphs. This allows for efficient algorithms for the manipulation of zones during the verification process.

An inherent drawback of zones is that they are convex sets, and consequently they are not closed under set union. This means that during the analysis process, symbolic states cannot generally be combined, which potentially leads to statespace explosion. Due to this, tropical polyhedra have been proposed in [START_REF] Lu | Reachability analysis for timed automata using max-plus algebra[END_REF] as a replacement for zones. However, an important drawback in this approach is that the analysis of timed automata often requires to express strict constraints, for instance in the analysis of communication protocols [START_REF] David | Model-based framework for schedulability analysis using UPPAAL 4[END_REF][START_REF] Kot | Modeling selected real-time database concurrency control protocols in Uppaal[END_REF], while tropical polyhedra are by definition topologically closed. An example illustrating these drawbacks will be given in Section 5.

Contributions

In this paper we first introduce (Section 2) a class of non-necessarily closed tropically convex sets. This class is called tropical polyhedra with mixed constraints. It can express not only inequalities of the form (1.2) in which the relation has been replaced by <, but also finer constraints exploiting the disjunctive character of tropical inequalities. For instance, the inequality

x 1 max(1 + x 2 , 0 -+ x 3 )
is going to represent the disjunction of the inequalities x 1 1 + x 2 and x 1 < x 3 . These mixed inequalities are defined using coefficients in a semiring of affine germs, which represent infinitesimal perturbations of reals.

In the second place, we present a tropical counterpart of Fourier-Motzkin elimination (Section 3). It provides a constructive method to show that the projection in R n-1 max of a tropical polyhedron with mixed constraints P ⊂ R n max is a polyhedron with mixed constraints (Theorem 3.4). It computes a representation by mixed inequalities of the projection by combining the defining inequalities of P. Actually, this approach handles more generally systems of inequalities with coefficients in a totally ordered idempotent semiring, modulo some assumptions. Note that such an analogue of Fourier-Motzkin algorithm has not been considered previously in the tropical setting, even in the case of standard (closed) tropical polyhedra. Fourier-Motzkin elimination also appears as a useful tool to show the polyhedral character of some non-closed tropically convex sets. As an application, we indeed prove that tropical polyhedra with mixed constraints are precisely the tropically convex union of finitely many zones, and the intersection of finitely many tropical hemispaces (i.e. tropically convex sets whose complements are also tropically convex, which were studied in e.g. [START_REF] Briec | Halfspaces and Hahn-Banach like properties in B-convexity and max-plus convexity[END_REF][START_REF] Katz | Characterization of tropical hemispaces by (P, R)-decompositions[END_REF]), see Theorem 3.6 and Corollary 3.10.

Superfluous inequalities may be produced by Fourier-Motzkin algorithm, so that the size of the constraint systems can grow in a double exponential way during consecutive applications of the method. In order to eliminate such redundant inequalities, in Section 4 we extend to mixed inequalities a result of [START_REF] Akian | Tropical polyhedra are equivalent to mean payoff games[END_REF] and its subsequent refinement in [START_REF] Allamigeon | Tropical polar cones, hypergraph transversals, and mean payoff games[END_REF], building on techniques of these two papers. The result of [START_REF] Akian | Tropical polyhedra are equivalent to mean payoff games[END_REF] shows that deciding the feasibility of a system of tropical linear inequalities is (Karp) polynomial-time equivalent to solving mean payoff games. The result of [START_REF] Allamigeon | Tropical polar cones, hypergraph transversals, and mean payoff games[END_REF] shows that deciding logical implications over tropical linear inequalities is also equivalent to solving mean payoff games. Theorem 4.7 generalizes these two results to mixed inequalities. We note that the present approach (through germs) also yields an alternative, simpler derivation of the result of [START_REF] Allamigeon | Tropical polar cones, hypergraph transversals, and mean payoff games[END_REF]. Indeed, deciding whether a given inequality of the form (1.2) is logically implied by a system of other inequalities of the same kind amounts to checking if the intersection of a tropical polyhedron with the complement of a closed half-space is empty or not. Such an intersection is obviously a tropical polyhedron with mixed constraints.

Experimentally efficient algorithms have been developed to solve mean payoff games, but no polynomial time algorithm is known. Hence we also provide a weak criterion which allows to eliminate some of the superfluous inequalities in polynomial time (Section 4.2). We prove that, in the case of non-strict inequalities, this weak elimination is sufficient to obtain a single-exponential bound for Fourier-Motzkin elimination (Section 4.3).

Finally, Section 5 illustrates the application of tropical polyhedra with mixed constraints to the verification (reachability analysis) of timed automata. We show that the operations necessary for forward exploration of timed automata can be defined on tropical polyhedra with mixed constraints, using Fourier-Motzkin elimination and the algorithms developed to eliminate redundant inequalities.

Related work

The algorithms developed so far for tropical polyhedra usually benefit from the fact that these can be represented either externally, using inequalities (as in (1.1)), or internally, as sets generated by finitely many points and rays (see [START_REF] Gaubert | Minimal half-spaces and external representation of tropical polyhedra[END_REF] for details). In contrast, non-closed tropically convex sets may not be finitely generated. Generating representations of (non-necessarily closed) tropical convex cones have been studied in [START_REF] Butkovič | Generators, extremals and bases of max cones[END_REF], and in [START_REF] Katz | Characterization of tropical hemispaces by (P, R)-decompositions[END_REF] in the particular case of tropical hemispaces. A certain class of possibly infinite generating representations was treated in [START_REF] Gaubert | Rational semimodules over the max-plus semiring and geometric approach to discrete event systems[END_REF], however, the associated algorithms rely on the expensive Presburger arithmetic. Defining non-closed polyhedra using infinitesimal perturbations of generators also presents some difficulties, see Remark 2.6 below. Moreover, we should warn the reader that some geometric aspects of tropical polyhedra, in particular the notion of faces, are still not yet understood [START_REF] Develin | Tropical polytopes and cellular resolutions[END_REF]. Thus it does not seem easy to manipulate non-closed polyhedra from closed ones by excluding some "facets" or "edges".

The present tropical Fourier-Motzkin algorithm may be thought of as a dual of the tropical double description method [START_REF] Allamigeon | Computing the vertices of tropical polyhedra using directed hypergraphs[END_REF], in which one successively eliminates inequalities rather than variables. In both algorithms, redundant intermediate data (inequalities or generators) are produced, and the key to the efficiency of the algorithm lies in the dynamic elimination of such data. Redundant generators can be eliminated in almost linear time using a combinatorial hypergraph algorithm, however the hypergraph criterion appears to have no natural dual analogue which can detect redundant inequalities.

As mentioned above, the equivalence between mean payoff games and the emptiness problem for tropical polyhedra with mixed constraints generalizes a result of [START_REF] Akian | Tropical polyhedra are equivalent to mean payoff games[END_REF]. Moreover, it generalizes an earlier result [START_REF] Möhring | Scheduling with AND/OR precedence constraints[END_REF] concerning finite solutions of a class of non-strict disjunctive constraints appearing in scheduling. The non-strict inequality satisfiability problem has also been studied under the name of "max-atom problem" in [START_REF] Bezem | The max-atom problem and its relevance[END_REF], with motivations from SMT solving. Note here a fundamental difference between strict and non-strict constraints: in the latter case, for inequalities with integer coefficients, it is shown in [START_REF] Akian | Tropical polyhedra are equivalent to mean payoff games[END_REF] that emptiness over the integers is equivalent to emptiness over the reals. The same is not true for strict inequalities (consider for example the open hypercube ]0, 1[ n which is non-empty, but contains no integer points), so that the present result for mixed inequalities cannot be deduced from earlier ones.

The infinitesimal perturbation of reals used in mixed inequalities is based on a semiring of affine germs, which was used in [START_REF] Gaubert | The duality theorem for min-max functions[END_REF][START_REF] Dhingra | How to solve large scale deterministic games with mean payoff by policy iteration[END_REF] to provide policy iteration based methods to solve mean payoff games. It also appeared in the context of tropical linear programming, see [31, § 3.7]. The idea here is that germs allow one to determine algebraically the value of a perturbed game. Related perturbation or parametric game ideas were used in [START_REF] Allamigeon | Tropical polar cones, hypergraph transversals, and mean payoff games[END_REF][START_REF] Gaubert | The level set method for the two-sided max-plus eigenproblem[END_REF].

Tropical Polyhedra with Mixed Constraints

In the semiring (R max , ⊕, ⊗), addition and multiplication admit neutral elements, namely -∞ and 0. Addition does not generally admit inverses. In contrast, any nonzero (in the tropical sense) element x admits a multiplicative inverse, which is given by -x and will be denoted x -1 . The semiring operations are extended to vectors and matrices in the usual way, i.e. (A⊕B) ij := A ij ⊕B ij and (A⊗B) ij := ⊕ k (A ik ⊗B kj ). We will work in the semimodule R n max , for n ∈ N. Its elements can be seen as points or vectors and are denoted x, y, etc. The order on R max is extended to vectors entry-wise. We equip R max with the topology induced by the metric (x, y) → |exp xexp y|, and R n max with the product topology. In the sequel, we also use the completed max-plus semiring R max := R max ∪ {+∞}, with the conventions

x < +∞ for all x ∈ R max , x ⊗ (+∞) = +∞ if x = -∞, and (-∞) ⊗ (+∞) = -∞.
Finally, given a positive integer n, we denote by [n] the set {1, . . . , n}.

The notion of convexity can be transposed to tropical algebra.

A subset C of R n max is said to be (tropically) convex if it contains the tropical segment {λx ⊕ µy | λ, µ ∈ R max , λ ⊕ µ = 0}
joining any two points x and y of C. This is analogous to the usual definition of convexity, except that in the tropical setting the non-negativity constraint on λ and µ is implicit (any scalar x ∈ R max satisfies x -∞).

We now introduce the algebraic structure which will allow us to handle possibly strict tropical inequalities. We use a disjoint copy R -of R composed of elements denoted α -for α ∈ R, and we set G := R max ∪ R -. The modulus |x| of an element x ∈ G is defined by:

|x| := x if x ∈ R max ; α if x = α -∈ R -.
The set G is totally ordered by the order relation G defined by:

x G y ⇐⇒ |x| < |y| if x ∈ R max and y ∈ R -; |x| |y| otherwise.
We use the notation x < G y when x G y and x = y. As an illustration, the Hasse diagram of G over the elements with modulus in Z ∪ {±∞} is given in Figure 2.

The element α -can be interpreted as an infinitesimal perturbation of α of the form αε with ε > 0. Formally, given x ∈ G and ε > 0, the valuation of x at ε, denoted by x(ε), is the element of R max defined as follows:

x(ε) := x if x ∈ R max ; |x| -ε if x ∈ R -.
The valuation is extended to vectors and matrices entry-wise.

The set G has a semiring structure when equipped with the sum of two elements x, y ∈ G defined as the greatest element among them, and the multiplication given by: By abuse of notation, the multiplication in G will be simply denoted by concatenation and the sum by ⊕, as in the case of R max . Observe that in G the neutral elements are still -∞ and 0, and that only the elements x ∈ R are invertible with respect to multiplication. Also note that the modulus map is a semiring morphism. We begin with a technical lemma on the arithmetic operations in the semiring G.

+∞ 2 2 - 1 1 - 0 0 - -1 (-1) - -∞ . . . . . . . . . . . .
           x ⊗ y if x, y ∈ R ; (|x| ⊗ |y|) -if x ∈ R -or y ∈ R -,
Lemma 2.1. The following properties hold:

(i) for any x, y ∈ G, x G y if, and only if, x(ε) y(ε) for ε > 0 sufficiently small; (ii) for any x, y ∈ G and ε > 0 sufficiently small, (x ⊕ y)(ε) = x(ε) ⊕ y(ε); (iii) for any x ∈ R max , y ∈ G, and ε > 0, (xy)(ε) = xy(ε); (iv) for any x, y, z ∈ G, x G y implies xz G yz, and the converse holds if z ∈ R; (v) for any x, y ∈ R max , x < y is equivalent to x G 0 -y when x ∈ R, and to 0 G (+∞)y when x = -∞.

Proof. (i) The only non-trivial case is when x ∈ R and y ∈ R -, so assume we are in this case. Then, x G y amounts to x < |y|. This is equivalent to x(ε) = x |y|ε = y(ε) for ε > 0 sufficiently small. (v) In the first place, we suppose that x ∈ R. If x < y, then y ∈ R and 0 -y = y -. Thus, x < y implies x G y -, i.e. x G 0 -y. Conversely, if the latter inequality holds, then y is distinct from -∞. Thus, 0 -y = y -, and x G y -ensures that x < y.

Assume now that x = -∞. Note that (+∞)y is equal to +∞ if y = -∞, and to -∞ otherwise. Thus, we have 0 G (+∞)y if, and only if, y > -∞ = x.

A mixed tropical affine inequality is defined as a constraint of the form

a 0 ⊕ a 1 x 1 ⊕ • • • ⊕ a n x n G b 0 ⊕ b 1 x 1 ⊕ • • • ⊕ b n x n , (2.1)
where the coefficients a i on the left-hand side belong R max , while the coefficients b i on the right-hand side are in G. When the set of x in R n max satisfying a mixed inequality is a non-empty proper subset of R n max , it is called mixed half-space.

Lemma 2.2. A vector x ∈ R n max satisfies (2.1) if, and only if, there exists ε > 0 such that

a 0 ⊕ a 1 x 1 ⊕ • • • ⊕ a n x n b 0 (ε) ⊕ b 1 (ε)x 1 ⊕ • • • ⊕ b n (ε)x n .
(2.2)

Proof. If (2.1) is satisfied, then by Property (i) of Lemma 2.1 we have

a 0 ⊕ a 1 x 1 ⊕ • • • ⊕ a n x n (b 0 ⊕ b 1 x 1 ⊕ • • • ⊕ b n x n )(ε)
for ε > 0 sufficiently small, since the left-hand side of (2.1) belongs to R n max . Besides, by Properties (ii) and (iii) of Lemma 2.1, it follows that

(b 0 ⊕ b 1 x 1 ⊕ • • • ⊕ b n x n )(ε) = b 0 (ε) ⊕ b 1 (ε)x 1 ⊕ • • • ⊕ b n (ε)x n
for ε > 0 sufficiently small, which shows that (2.2) holds.

Conversely, suppose that (2.2) is satisfied for some ε > 0. Then

a 0 ⊕ a 1 x 1 ⊕ • • • ⊕ a n x n b 0 (ε ′ ) ⊕ b 1 (ε ′ )x 1 ⊕ • • • ⊕ b n (ε ′ )x n for any ε ′ < ε (the map ε ′ → b 0 (ε ′ ) ⊕ b 1 (ε ′ )x 1 ⊕ • • • ⊕ b n (ε ′ )
x n is non-increasing). It follows that (2.1) holds, by Properties (i), (ii) and (iii) of Lemma 2.1 and the fact that the left-hand side of (2.1) belongs to R max .

A tropical polyhedron with mixed constraints is defined as a set composed of the vectors x ∈ R n max which satisfy finitely many mixed tropical affine inequalities.

To contrast with, we use the term closed tropical polyhedron when the defining mixed inequalities only involve coefficients in R max , i.e. they are of the form (1.1).

The following proposition establishes that polyhedra with mixed constraints are (possibly non-closed) tropically convex sets.

Proposition 2.3. Any tropical polyhedron with mixed constraints is a tropically convex set.

Proof. Let x, y be two solutions of (2.1), and λ, µ ∈ R max be such that λ ⊕ µ = 0. By Lemma 2.2, there exist ε, ε ′ > 0 such that:

a 0 ⊕ a 1 x 1 ⊕ • • • ⊕ a n x n b 0 (ε) ⊕ b 1 (ε)x 1 ⊕ • • • ⊕ b n (ε)x n , a 0 ⊕ a 1 y 1 ⊕ • • • ⊕ a n y n b 0 (ε ′ ) ⊕ b 1 (ε ′ )y 1 ⊕ • • • ⊕ b n (ε ′ )y n .
These inequalities are still valid if we replace ε and ε ′ by min(ε, ε ′ ). Hence, we can assume, without loss of generality, that ε = ε ′ . Then, z = λx ⊕ µy satisfies

a 0 ⊕ a 1 z 1 ⊕ • • • ⊕ a n z n b 0 (ε) ⊕ b 1 (ε)z 1 ⊕ • • • ⊕ b n (ε)z n ,
which proves that z is a solution of (2.1) by Lemma 2.2. Thus, any mixed halfspace is tropically convex. We conclude that every tropical polyhedron with mixed constraints is tropically convex, as the intersection of finitely many tropically convex sets.

Example 2.4. The vectors x ∈ R 2 satisfying the strict inequality x 1 < max(-1 + x 2 , 0), depicted on the left-hand side of Figure 3, are obtained as the real solutions of the mixed affine inequality x 1 G (-1) -x 2 ⊕0 -. Similarly, the solutions of x 1 G (-1) -x 2 ⊕ 0 correspond to the previous set in which the half-line {(0, λ) | λ 1} is added (middle of Figure 3). The set depicted on the right-hand side of Figure 3 is the tropical polyhedron with mixed constraints defined by the following mixed inequalities:

(-2)x 2 G 0 -⊕ 0 -x 1 -3 G x 1 0 G 1x 1 ⊕ 0 -x 2 -2 G x 2 x 1 G 3 -x 2 (-2)x 1 G 0 -⊕ (-1)x 2 (2.3)
Observe that the inequalities in (2.3) have the property that no variable (or constant term) ever appears on both the left-and right-hand sides. The following lemma ensures that this situation is not restrictive, and that in any inequality of the form (2.1), we can always assume a i = -∞ or b i = -∞ for all i ∈ {0, . . . , n}. Proof. In the first place, suppose that a G c. Then, ax G cx for all x ∈ R max by Property (iv) of Lemma 2.1. It follows that ax G cx ⊕ d is always satisfied. Suppose now that a > G c. If x ∈ R, we have ax⊕b G ax > G cx by Property (iv) of Lemma 2.1. As a consequence, any x ∈ R max such that ax ⊕ b G cx ⊕ d also satisfies ax ⊕ b G d. This completes the proof.

Remark 2.6. Following the analogy with closed tropical polyhedra, we could also consider subsets of G n generated by finitely many points and rays (given by vectors with entries in G), having in mind to encode non-closed subsets of R n max thanks to infinitesimal perturbation of generators. More precisely, we could consider that a subset C of G n encodes the subset C of R n max given by the points y ∈ R n max such that for all ε > 0 there exist ε ′ ∈ ]0, ε[ and x ∈ C verifying y = x(ε ′ ). However, this approach presents several difficulties. For example, consider the segment S of G 2 joining the points v = (0 -, 1) and w = (1 -, 1), i.e.

S = {λv ⊕ µw ∈ G 2 | λ, µ ∈ G, λ ⊕ µ = 0} . Then, it can be checked that S = {(α, 1) ∈ R 2 max | α ∈ [0, 1[}.
Now, observe that if we consider the segment S ′ joining v ′ = (1 -, 0) and w ′ = (0, 1), we have S ′ = S. Noticing that v ′ ∈ S and v ∈ S ′ , we see that different polyhedra of G n can encode the same subset of R n max . Consequently, it seems far from trivial to determine the equality of two subsets of R n max when they are encoded as polyhedra of G n .

Remark 2.7. As a complement of Remark 2.6, we point out that the closure of a polyhedron with mixed constraints is apparently harder to compute than in the case of usual convex polyhedra. Indeed, in the latter case, the closure can be simply obtained by substituting < by in the defining inequalities. In contrast, in the current setting, replacing the coefficients b i of the form β - i by β i on the right-hand side of mixed inequalities provides a closed tropical polyhedron which may be larger than the closure. For example, consider the polyhedron with mixed constraints defined by the inequalities: which is depicted on the left-hand side of Figure 4. The mixed half-space defined by the last inequality is represented in blue. The closure of the polyhedron is the usual unit square. However, the closed polyhedron defined by the inequalities:

0 G x 1 x 1 ⊕ x 2 G 1 0 G (-1) -x 1 ⊕ 0 -x 2 , x 1 x 2 x 1 x 2
0 x 1 x 1 ⊕ x 2 1 0 (-1)x 1 ⊕ x 2 ,
contains additionally the half-line {(1, λ) | λ 0} (right-hand side of Figure 4).

Tropical Fourier-Motzkin Elimination

In this section, we first present a tropical Fourier-Motzkin elimination method, which allows to eliminate a variable in a finite system of mixed inequalities. Then we apply this method to establish relationships between tropical polyhedra with mixed constraints, zones and tropical hemispaces.

The algorithm

We first illustrate the algorithm on an example.

Example 3.1. Consider the system given in (2.3), and assume we want to eliminate the variable x 1 . From the last (rightmost) two inequalities of (2.3), we know that:

x 1 G 3 -x 2 x 1 G 2 -⊕ 1x 2 (3.1)
In each inequality involving the variable x 1 on the right-hand side (i.e. the leftmost three inequalities of (2.3)), we propose to replace x 1 by the two upper bounds provided by (3.1). This produces the following six inequalities:

(-2)x 2 G 0 -⊕ 3 -x 2 (-2)x 2 G 2 -⊕ 1 -x 2 -3 G 3 -x 2 -3 G 2 -⊕ 1x 2 0 G 4 -x 2 0 G 3 -⊕ 2x 2 (3.2)
Besides, in each inequality not involving x 1 on the right-hand side, we remove the term in x 1 from the left-hand side, if any. From the rightmost inequalities of (2.3), we obtain the following three inequalities:

-2 G x 2 -∞ G 3 -x 2 -∞ G 0 -⊕ (-1)x 2 . (3.3)
We claim that the inequalities in (3.2) and (3.3) precisely describe the projection on the x 2 axis of the polyhedron with mixed constraints defined by (2.3). Note that the collection of inequalities obtained in this way is redundant: one inequality, -2 G x 2 , suffices.

We now formalize the approach sketched in Example 3.1. Under some assumptions (which are specified in Theorem 3.3 below), it applies more generally to systems of constraints over a totally ordered idempotent semiring.

Recall that a semiring (S, ⊕, ⊗, 0, 1) is said to be totally ordered if there exists a total order S on S such that:

(i) 0 S a for all a ∈ S, (ii) for all a, b, c ∈ S, a S b implies a ⊕ c S b ⊕ c, a ⊗ c S b ⊗ c, and c ⊗ a S c ⊗ b.
The semiring S is said to be idempotent if a ⊕ a = a for all a ∈ S. The next lemma shows that such a semiring is naturally ordered, meaning that a ⊕ b is equal to the maximal element among a and b.

Now we explain how to eliminate

x n in a linear system of inequalities over S in the variables x 1 , . . . , x n . For the sake of simplicity, we extend the operations of S to matrices and vectors in the usual way and represent the multiplication ⊗ by concatenation.

Theorem 3.3 (Fourier-Motzkin elimination for systems over totally ordered idempotent semirings). Let (S, ⊕, ⊗, 0, 1, S ) be a totally ordered idempotent semiring and P ⊂ S n be the solution set of the system Ax ⊕ c S Bx ⊕ d, where A, B ∈ S p×n and c, d ∈ S p satisfy the following conditions:

(i) A in is (left-)invertible with respect to ⊗ if A in = 0 (we denote its inverse by A -1 in ), a (ii) for any α ∈ S there exists β ∈ S such that α S B in β if B in = 0, (iii) either A ij = 0 or B ij = 0 for i ∈ [p] and j ∈ [n].
Let Q ⊂ S n-1 be the set defined by the following inequalities in the variables x 1 , . . . , x n-1 :

(⊕ j =n A ij x j ) ⊕ c i S (⊕ j =n B ij x j ) ⊕ d i , (3.4)
a Here and below, M in denotes the (i, n)-entry of matrix M , and should not be confused with any abbreviation.

for all i ∈ [p] such that B in = 0, and

(⊕ j =n A ij x j ) ⊕ c i S (⊕ j =n (B ij ⊕ B in A -1 kn B kj )x j ) ⊕ d i ⊕ B in A -1 kn d k , (3.5)
for all i, k ∈ [p] such that B in = 0 and A kn = 0. Then x ∈ Q if, and only if, there exists λ ∈ S such that (x, λ) ∈ P.

Proof. Assume that (x, λ) ∈ P for some λ ∈ S. Then for all i ∈ [p] such that B in = 0, we have:

(⊕ j =n A ij x j ) ⊕ c i S (⊕ j =n A ij x j ) ⊕ A in λ ⊕ c i S (⊕ j =n B ij x j ) ⊕ d i ,
which proves that x satisfies the inequalities of the form (3.4). Now consider i, k ∈ [p] such that B in = 0 and A kn = 0. Then, A in = B kn = 0 by Condition (iii), and A kn is left-invertible by Condition (i). Since A kn λ S (⊕ j =n B kj x j ) ⊕ d k , we know that

λ S A -1 kn (⊕ j =n B kj x j ) ⊕ A -1 kn d k .
Replacing λ by the latter upper bound in the inequality

(⊕ j =n A ij x j ) ⊕ c i = (⊕ j =n A ij x j ) ⊕ A in λ ⊕ c i S (⊕ j =n B ij x j ) ⊕ B in λ ⊕ d i
precisely yields inequality (3.5), using distributivity of ⊗ and commutativity of ⊕. Thus, we conclude that x ∈ Q.

Conversely, let x ∈ Q. In the first place, assume that A in = 0 for all i ∈ [p]. Define

λ := ⊕ i∈I β i ,
where

I := {i ∈ [p] | B in = 0} and β i ∈ S is such that (⊕ j =n A ij x j ) ⊕ c i S B in β i for i ∈ I (β i exists thanks to Condition (ii)). Then, if B in = 0, we have (⊕ j =n A ij x j )⊕A in λ⊕c i = (⊕ j =n A ij x j )⊕c i S B in λ S (⊕ j =n B ij x j )⊕B in λ⊕d i .
The same inequality is trivially satisfied if B in = 0 due to (3.4). It follows that (x, λ) ∈ P. Now assume that A kn = 0 for some k ∈ [p]. Define

λ := min k∈[p] A kn =0 A -1 kn (⊕ j =n B kj x j ) ⊕ A -1 kn d k , (3.6)
where the operator min is understood as providing the minimum of its operands with respect to the order S . As a consequence, for all i such that A in = 0, we have

A in λ S (⊕ j =n B ij x j ) ⊕ d i .
The fact that B in = 0 (by Condition (iii)) and the conjunction with (3.4) yield:

(⊕ j =n A ij x j ) ⊕ A in λ ⊕ c i S (⊕ j =n B ij x j ) ⊕ d i = (⊕ j =n B ij x j ) ⊕ B in λ ⊕ d i .
Note that the latter inequality also holds for all i ∈ [p] such that A in and B in are both equal to 0. Now suppose that i ∈ [p] satisfies B in = 0 and k ∈ [p] attains the minimum in (3.6). Since x satisfies (3.5), i.e.

(⊕ j =n A ij x j ) ⊕ c i S (⊕ j =n B ij x j ) ⊕ d i ⊕ B in A -1 kn (⊕ j =n B kj x j ⊕ d k ) it follows that (⊕ j =n A ij x j ) ⊕ A in λ ⊕ c i = (⊕ j =n A ij x j ) ⊕ c i S (⊕ j =n B ij x j ) ⊕ B in λ ⊕ d i , because B in = 0 implies A in = 0 by Condition (iii)
. This shows that (x, λ) belongs to P.

The case of tropical polyhedra with mixed constraints is obtained by setting S = G. Note that the conditions of Theorem 3.3 are satisfied when S = G, due in particular to Lemma 2.5 and the fact that any non-zero coefficient on the left-hand side of a mixed inequality is invertible (as an element of R). However, a tropical polyhedron with mixed constraints consists of the solutions belonging to R n max , while Theorem 3.3 applies to the solutions in G n . The following result shows that the projection algorithm is still valid when restricted to R n max .

Theorem 3.4 (Fourier-Motzkin elimination for systems of mixed inequalities). Assume P and Q are defined as in Theorem 3.3 with S = G. Then, for all x ∈ R n-1 max , x ∈ Q if, and only if, there exists λ ∈ R max such that (x, λ) ∈ P.

Proof. Observe that to prove the theorem, it is enough to show that if y := (x, λ) ∈ P for some x ∈ R n-1 max and λ ∈ G, then there exists λ ′ ∈ R max such that (x, λ ′ ) ∈ P. If λ ∈ R max , there is nothing to prove, so assume λ ∈ R -∪ {+∞}. We will show that for a certain choice of λ ′ ∈ R verifying λ ′ G λ, the vector y ′ := (x, λ ′ ) ∈ R n max belongs to P. Note that for any such choice of λ ′ , the vector y ′ satisfies the inequalities in Ax ⊕ c G Bx ⊕ d indexed by i ∈ [p] such that B in = ±∞. Indeed, in this case, we have

(⊕ j A ij y ′ j ) ⊕ c i G (⊕ j A ij y j ) ⊕ c i G (⊕ j B ij y j ) ⊕ d i = (⊕ j B ij y ′ j ) ⊕ d i . (3.7)
Thus, we next focus on the inequalities indexed by elements of the set

I := {i ∈ [p] | B in ∈ R ∪ R -}. In consequence, A in = -∞ for all i ∈ I.
It is convenient to split the rest of the proof into two cases.

In the first place, assume λ = +∞. Define λ ′ := δǫ ∈ R, where ǫ > 0 and

δ = ⊕ i∈I |B in | -1 (⊕ j =n A ij x j ⊕ c i ) if I = ∅ , 0 otherwise. Obviously, λ ′ G λ.
Besides, for all i ∈ I we have

(⊕ j =n A ij x j ) ⊕ A in λ ′ ⊕ c i G (⊕ j =n B ij x j ) ⊕ B in λ ′ ⊕ d i , since ⊕ j =n A ij x j ⊕ c i < |B in |λ ′ and A in = -∞. Now assume λ ∈ R -. Let I ′ be the set of indices i ∈ I such that B in λ > G ⊕ j =n B ij x j ⊕ d i . Then, (⊕ j A ij y j ) ⊕ c i = (⊕ j =n A ij x j ) ⊕ c i G B in λ for all i ∈ I ′ . For i ∈ I ′ , let ν i = ⊕ j =n A ij x j ⊕ c i . Since ν i belongs to R max (A ij , x j and c i belong to R max ) and B in λ belongs to R -, we necessarily have ν i < |B in λ|. Define λ ′ := κ|λ| ∈ R, where κ = max i∈I ′ (ν i -|B in λ|)/2 if {i ∈ I ′ | ν i ∈ R} = ∅ , -1 otherwise. As κ < 0, we have λ ′ G λ. Moreover, if i ∈ I ′ , then ν i < κ|B in λ| and so (⊕ j A ij y ′ j ) ⊕ c i G (⊕ j A ij y j ) ⊕ c i = (⊕ j =n A ij x j ) ⊕ c i = = ν i G κB in λ G κB in |λ| = B in λ ′ G (⊕ j B ij y ′ j ) ⊕ d i . Finally, note that for i ∈ I \ I ′ the relations in (3.7) are still valid because in that case we have ⊕ j =n B ij x j ⊕ d i G B in λ G B in λ ′ .
This completes the proof.

Characterization of tropical polyhedra with mixed constraints in terms of zones and tropical hemispaces

In this subsection we discuss some consequences of tropical Fourier-Motzkin elimination. In the first place, we establish that the tropical convex hull of the union of two tropical polyhedra with mixed constraints is a tropical polyhedron with mixed constraints. Recall that the tropical convex hull tconv(G) of a set G ⊂ R n max is defined as the set of the vectors of the form

λ 1 x 1 ⊕ • • • ⊕ λ m x m
where m is a positive integer,

x i ∈ G, λ i ∈ R max (i ∈ [m]), and ⊕ i∈[m] λ i = 0.
Proposition 3.5. Let P, P ′ ⊂ R n max be polyhedra with mixed constraints, respectively defined by the systems

Ax ⊕ c G Bx ⊕ d and A ′ x ⊕ c ′ G B ′ x ⊕ d ′
, and let Q be the polyhedron defined by the inequalities which are obtained eliminating y 1 , . . . , y n , y ′ 1 , . . . , y ′ n , λ and µ in the following system:

x = y ⊕ y ′ λ ⊕ µ = 0 Ay ⊕ λc G By ⊕ λd y 1 ⊕ • • • ⊕ y n G (+∞)λ (3.8) A ′ y ′ ⊕ µc ′ G B ′ y ′ ⊕ µd ′ y ′ 1 ⊕ • • • ⊕ y ′ n G (+∞)µ
Then, we have tconv(P ∪ P ′ ) = Q.

Proof. In the first place, note that P ⊂ Q. Indeed, given x ∈ P, let λ = 0, µ = -∞, y = x and y

′ i = -∞ for i ∈ [n].
Then, (3.8) is clearly satisfied, and so from Theorem 3.4 we deduce that x ∈ Q. Similarly, P ′ ⊂ Q. Since Q is tropically convex, we deduce that tconv(P ∪ P ′ ) ⊂ Q.

Conversely, let x ∈ Q, and consider y, y ′ , λ, µ as in (3.8). If both λ, µ are distinct from -∞, then λ -1 y ∈ P, µ -1 y ′ ∈ P ′ , and x = λ(λ -1 y) ⊕ µ(µ -1 y ′ ), which ensures that x ∈ tconv(P ∪ P ′ ). Otherwise, if for instance µ = -∞, then we necessarily have λ = 0, and so y ∈ P. Moreover, from

y ′ 1 ⊕ • • • ⊕ y ′ n G (+∞)µ we deduce that y ′ i = -∞ for all i ∈ [n]
, and in consequence x = y. This completes the proof, because again we have x = y ∈ P ⊂ tconv(P ∪ P ′ ), and so Q ⊂ tconv(P ∪ P ′ ).

In order to characterize tropical polyhedra with mixed constraints in terms of zones, we first need to extend the definition of zones to R max : a zone (of R n max ) is a set of vectors x ∈ R n max defined by inequalities of the form

m i ⊳ x i x i ⊳ M i x i ⊳ k ij x j (3.9)
where ⊳ ∈ { , <} and m i , M i , k ij ∈ R max .

Theorem 3.6. A subset P of R n max is a tropical polyhedron with mixed constraints if, and only if, it is a tropically convex union of finitely many zones.

Proof. Observe that when ⊳ is equal to in (3.9), these inequalities are equivalent to the ones obtained replacing ⊳ by G . Moreover, we have

m i < x i ⇐⇒ m i G 0 -x i if m i ∈ R 0 G (+∞)x i if m i = -∞ x i < M i ⇐⇒ x i G 0 -M i if M i ∈ R x i < k ij x j ⇐⇒ (x i G (0 -)k ij x j and 0 G (+∞)x j ) if k ij ∈ R
In consequence, any zone is a tropical polyhedron with mixed constraints. Then, by Proposition 3.5, so is the tropical convex hull of the union of finitely many zones.

The "if" part of the theorem follows from the fact that if the union of finitely many zones is tropically convex, then it coincides with its tropical convex hull. Suppose now that Q is a polyhedron defined by mixed inequalities of the form (2.1), in which only one of the coefficients b j is distinct from -∞. If this coefficient is b 0 , as we can assume that b 0 = +∞, it follows that (2.1) can be rewritten as a system of inequalities of the form x i G βM i , with β ∈ {0, 0 -} and M i ∈ R. If the considered coefficient is b j for j ∈ [n], then (2.1) can be rewritten as a system of inequalities of the form m j G βx j and x i G βk ij x j , with β ∈ {0, 0 -, +∞} and m j , k ij ∈ R. Since

x i G βk ij x j ⇐⇒        x i k ij x j if β = 0 x i < k ij x j or (x i -∞ and x j -∞) if β = 0 - -∞ < x j or (x i -∞ and x j -∞) if β = +∞ x i G βM i ⇐⇒ x i M i if β = 0 x i < M i if β = 0 - m j G βx j ⇐⇒        m j x j if β = 0 m j < x j if β = 0 - -∞ < x j if β = +∞
it follows that Q is a finite union of zones.

The "only if" part of the theorem follows from the fact that any polyhedron with mixed constraints can be written as a finite union of polyhedra of the form considered in the previous paragraph (it suffices to choose, in each inequality, one term in the right-hand side to be the maximizing one). Theorem 3.6 raises the problem, of independent interest, of determining whether a given union of finitely many zones is tropically convex. To our knowledge, this problem has not been studied so far, even in the case of closed zones. A naive solution consists in computing the tropical convex hull of the union of zones (using Proposition 3.5), and checking whether it intersects the complement of the union of zones (the latter can be expanded into a union of zones, and the intersection test requires the techniques developed in Section 4, see Theorem 4.7). This approach would be particularly expensive. Yet, it is similar to the technique implemented in the UPPAAL DBM library [START_REF] David | UPPAAL DBM library[END_REF] to test if a union of zones is a zone. Whether there exists a more efficient method is left for future work. Now we study the relationship between tropical polyhedra with mixed constraints and tropical hemispaces. Recall that a tropical hemispace is a tropically convex set whose complement is also tropically convex. Tropical hemispaces and mixed half-spaces share the property that their closure is a closed half-space (in the case of hemispaces, this is proved in [START_REF] Briec | Halfspaces and Hahn-Banach like properties in B-convexity and max-plus convexity[END_REF]). In fact, Proposition 3.7 and Example 3.8 below show that mixed half-spaces are a proper subclass of hemispaces. Proposition 3.7. Mixed half-spaces are tropical hemispaces.

Proof. We already proved in Proposition 2.3 that mixed half-spaces are tropically convex.

The complement of the mixed half-space defined by (2.1) consists of the vectors x ∈ R n max such that

a 0 ⊕ a 1 x 1 ⊕ • • • ⊕ a n x n > G b 0 ⊕ b 1 x 1 ⊕ • • • ⊕ b n x n . (3.10)
Let x, y ∈ R n max be in this complement, and λ, µ ∈ R max be such that λ ⊕ µ = 0. Without loss of generality, assume that λ = 0. If µ = -∞, then λx ⊕ µy = x trivially satisfies (3.10). Otherwise, i.e. if µ ∈ R and µ 0, then by Property (iv) of Lemma 2.1 we have µ(a 0 ⊕ a

1 y 1 ⊕ • • • ⊕ a n y n ) > G µ(b 0 ⊕ b 1 y 1 ⊕ • • • ⊕ b n y n ). It readily follows that a 0 ⊕ a 1 (λx 1 ⊕ µy 1 ) ⊕ • • • ⊕ a n (λx n ⊕ µy n ) > G b 0 ⊕ b 1 (λx 1 ⊕ µy 1 ) ⊕ • • • ⊕ b n (λx n ⊕ µy n )
. This shows that the complement of a mixed half-space is tropically convex. We claim that H is not a mixed half-space. Its closure is the tropical half-space defined by the inequality

x 3 ⊕ x 4 0x 1 ⊕ 0x 2 . (3.11)
Any mixed half-space whose closure is given by (3.11) is defined by a mixed inequality obtained from (3.11) by replacing some of the coefficients 0 on the right-hand side by 0 -. However, it can be easily verified that none of these mixed half-spaces is equal to H.

Similarly, it can be checked that the complement of H, which is given by the set of vectors x ∈ R 4 max such that

x 1 < x 3 ⊕ x 4 and (x 2 < x 3 or x 2 x 4 ) ,
is not a mixed half-space either.

To prove the following proposition, we shall use the characterization of tropical hemispaces in terms of (P, R)-decompositions established in [START_REF] Katz | Characterization of tropical hemispaces by (P, R)-decompositions[END_REF]. Proposition 3.9. Tropical hemispaces are tropical polyhedra with mixed constraints.

Proof. In the first place, let us recall that the tropical conic hull of a subset G of R n max is defined as

tcone(G) := {µ 1 x 1 ⊕ • • • ⊕ µ m x m | m ∈ N, x i ∈ G, µ i ∈ R max } .
Moreover, given two subsets G and

G ′ of R n max , their tropical Minkowski sum G⊕G ′ is defined as {x ⊕ x ′ | x ∈ G, x ′ ∈ G ′ }.
In this proof, we denote by u i ∈ R n max , for i ∈ [n], the vector defined by u i j := 0 if j = i and u i j := -∞ otherwise. Let H 1 , H 2 be two complementary hemispaces. Suppose that the vector all of whose entries are equal to -∞ belongs to H 1 . Then, by [START_REF] Katz | Characterization of tropical hemispaces by (P, R)-decompositions[END_REF]Theorem 4.22] there exist a partition I, J of [n] and interval sets

Λ 1 ij , Λ 2 ij ⊂ R max for i ∈ I ∪ {0} and j ∈ J such that H 1 = tconv({λu j | j ∈ J, λ ∈ Λ 1 0j }) ⊕ tcone({u i ⊕ λu j | i ∈ I, j ∈ J, λ ∈ Λ 1 ij }) H 2 = tconv({λu j | j ∈ J, λ = +∞, λ ∈ Λ 2 0j }) ⊕ tcone({λu i ⊕ u j | i ∈ I, j ∈ J, λ ∈ -Λ 2 ij })
where each couple of intervals Λ 1 ij , Λ 2 ij has one of the following forms:

(Λ 1 ij , Λ 2 ij ) = ([-∞, β], ]β, +∞]), β ∈ R ∪ {-∞} ([-∞, α[, [α, +∞]), α ∈ R ∪ {+∞} (3.12)
Thus, note that x ∈ H 1 if, and only if, there exist λ ij and µ ij in R max for i ∈ I ∪{0} and j ∈ J such that

x i = ⊕ j∈J µ ij for i ∈ I x j = ⊕ i∈I∪{0} λ ij µ ij for j ∈ J ⊕ j∈J µ 0j = 0 λ ij ∈ Λ 1 ij for i ∈ I ∪ {0} and j ∈ J
Equivalently, x ∈ H 1 if, and only if, there exist µ ij and ν ij in R max for i ∈ I ∪ {0} and j ∈ J such that

x i = ⊕ j∈J µ ij for i ∈ I x j = ⊕ i∈I∪{0} ν ij for j ∈ J ⊕ j∈J µ 0j = 0 ν ij G        βµ ij if Λ 1 ij = [-∞, β], β ∈ R max α -µ ij if Λ 1 ij = [-∞, α[, α ∈ R (+∞)µ ij if Λ 1 ij = [-∞, +∞[
for i ∈ I ∪ {0} and j ∈ J (3.13) By Theorem 3.4, we conclude that H 1 is a tropical polyhedron with mixed constraints, since it is defined by the system of mixed inequalities obtained by eliminating µ ij and ν ij for i ∈ I ∪ {0} and j ∈ J in (3.13).

The same result can be obtained for H 2 using a symmetric argument.

The following result is a straightforward consequence of Propositions 3.7 and 3.9.

Corollary 3.10. Tropical polyhedra with mixed constraints are precisely the intersections of finitely many tropical hemispaces.

Remark 3.11. We have previously defined a closed tropical polyhedron as the solution set of inequalities of the form (1.1), i.e. mixed inequalities with coefficients in R max . We point out that this definition is consistent with the fact that such polyhedra are precisely the tropical polyhedra with mixed constraints which are closed. Indeed, by Theorem 3.6 a tropical polyhedron with mixed constraints P can be written as a finite union of zones. If P is closed, then it is equal to the union of the closure of these zones (i.e. closed zones, which can be generated by finitely many points and rays by the tropical Minkowski-Weyl Theorem, see [START_REF] Gaubert | Minimal half-spaces and external representation of tropical polyhedra[END_REF]Theorem 2]). Since P is tropically convex, it is even equal to the tropical convex hull of this union. It follows that it is generated by finitely many points and rays. By the tropical Minkowski-Weyl Theorem, we deduce that it is the solution set of finitely many inequalities of the form (1.1).

Eliminating Redundant Mixed Inequalities

Like in the classical setting, Fourier-Motzkin elimination generates a system of O(p 2 ) inequalities from an input with p constraints. Consequently, the number of inequalities may grow in O(p 2 k ) after k successive applications. To avoid the explosion of the size of the constraint system, superfluous inequalities must be eliminated. With this aim, we present a decision procedure for implications of the form:

Ax ⊕ c G Bx ⊕ d =⇒ ex ⊕ g G f x ⊕ h for all x ∈ R n max , (4.1)
where

A ∈ R p×n max , B ∈ G p×n , c ∈ R p max , d ∈ G p , g ∈ R max , h ∈ G
, and e and f are n-dimensional row vectors with entries in R max and G respectively. We assume that e and g are not identically null (in the tropical sense) and that h = +∞, because otherwise deciding implication (4.1) is trivial.

Equivalence with mean payoff games

We first show that deciding an implication of the form (4.1) is equivalent to an emptiness problem for tropical polyhedra with mixed constraints. Proposition 4.1. Let Q be the tropical polyhedron with mixed constraints defined by the system Ax ⊕ c G Bx ⊕ d and the following inequalities:

       f i x i G (0 -e)x ⊕ 0 -g if f i ∈ R max |f i |x i G ex ⊕ g if f i ∈ R - x i G -∞ if f i = +∞ (4.2)
for all i ∈ [n], h G (0 -e)x ⊕ 0 -g if h ∈ R max |h| G ex ⊕ g if h ∈ R - (4.3)
and

0 G ⊕ ei =-∞ (+∞)x i if g = -∞.
Then

if, ex ⊕ g > G h and ex ⊕ g > G f i x i for all i ∈ [n]. This implies ex ⊕ g > -∞, i.e. 0 G (+∞)(ex ⊕ g). The latter inequality is trivially satisfied if g = -∞. When g = -∞, it is equivalent to 0 G ⊕ ei =-∞ (+∞)x i . Finally, assuming ex ⊕ g > -∞, note that ex ⊕ g > G f i x i is equivalent to (4.
2), and ex ⊕ g > G h is equivalent to (4.3). This completes the proof.

In light of Proposition 4.1, it is enough to develop a decision procedure to determine whether a tropical polyhedron with mixed constraints is empty. Our approach relies on parametric mean payoff games, following the lines of [START_REF] Akian | Tropical polyhedra are equivalent to mean payoff games[END_REF][START_REF] Allamigeon | Tropical polar cones, hypergraph transversals, and mean payoff games[END_REF].

Let R be a tropical polyhedron with mixed constraints defined by the system

M x ⊕ p G N x ⊕ q , (4.4)
where M ∈ R r×n max , N ∈ G r×n , p ∈ R r max and q ∈ G r . It is convenient to consider two different cases, depending on whether +∞ coefficients appear or not in (4.4).

Polyhedra defined by systems with no +∞ coefficients.

In the first place, we restrict to the following case: Assumption A. No coefficient is equal to +∞ on the right-hand side of mixed inequalities.

In other words, in this subsection we assume N ∈ (G \ {+∞}) r×n and q ∈ (G \ {+∞}) r .

In this case, with each ε 0 we associate a closed tropical polyhedron R ε , given by the system M x ⊕ p G N (ε)x ⊕ q(ε), and a mean payoff game involving two players, "Max" and "Min", playing on a weighted bipartite digraph G ε composed of two kinds of nodes: row nodes i ∈ [r], and column nodes j ∈ [n + 1]. This digraph contains an arc from row node i to column node j with weight N ij (ε) when N ij = -∞, and an arc from j to i with weight -M ij when M ij = -∞. Similarly, it contains an arc from row node i to column node n + 1 with weight q i (ε) if q i = -∞, and an arc from column node n + 1 to row node i with weight -p i when p i = -∞.

Example 4.2. Figure 5 provides an illustration of the digraph G ε corresponding to the tropical polyhedron with mixed constraints defined by the system:

1 : -3 G x 1 2 : 0 G 1x 1 ⊕ 0 -x 2 3 : -2 G x 2 4 : (-2)x 1 G 0 -⊕ (-1)x 2
The principle of the game is the following. Players Min and Max alternatively move a pawn over the nodes of G ε . When it is placed on a column node, Player Min selects an outgoing arc, moves the pawn to the corresponding row node, and pays to Player Max the weight of the selected arc. Once the pawn is on a row node, Player Max similarly selects an outgoing arc, moves the pawn along it, and receives from Player Min a payment equal to the weight of the selected arc.

In the sequel, we suppose that Players Max and Min always have at least one possible action in each node: Assumption B. Each node of G ε has at least one outgoing arc. This technical property can be assumed without loss of generality, up to adding trivial inequalities or removing non-relevant unknowns in the system. We refer to the discussion of Assumptions 2.1 and 2.2 in [START_REF] Akian | Tropical polyhedra are equivalent to mean payoff games[END_REF] for further details.

We consider infinite runs of the game, in which case the payoff is defined as the mean of the payments of Player Min to Player Max. Player Min wants to minimize this mean of payments while Player Max wants to maximize it. We denote by v(ε) the value of the game associated with G ε when it starts at column node n + 1. It is shown in [START_REF] Akian | Tropical polyhedra are equivalent to mean payoff games[END_REF]Theorem 3.5] that the tropical polyhedron R ε is non-empty if, and only if, v(ε) 0, i.e. column node n + 1 is a winning initial node (for Player Max). Then, the following result immediately follows from Lemma 2.2.

Proposition 4.3. The tropical polyhedron with mixed constraints R is non-empty if, and only if, there exists ε > 0 such that v(ε) 0.

Let M (resp. Ñ ) be the matrix of size r × (n + 1) obtained by concatenating matrix M and column vector p (resp. N and q). The dynamic programming operator g ε associated with the game over G ε is the function from R n+1 max to itself defined by

(g ε (x)) j := min i∈[r] Mij =-∞ -Mij + max k∈[n+1] Ñik =-∞ Ñik (ε) + x k , (4.5)
for j ∈ [n + 1]. This function satisfies the following properties:

(i) it is order preserving, i.e. x y implies g ε (x) g ε (y) for all x, y ∈ R n+1 max , (ii) it is additively homogeneous, i.e. g ε (λx) = λg ε (x) for all λ ∈ R max and

x ∈ R n+1 max , (iii) it preserves R n+1 , thanks to Assumption B above. Such a function can be shown to be non-expansive for the sup-norm. Since it is also piecewise affine, a theorem due to Kohlberg [START_REF] Kohlberg | Invariant half-lines of nonexpansive piecewise-linear transformations[END_REF] implies the following vector χ(g ε ), referred to as the cycle-time vector of g ε , exists and has finite entries:

χ(g ε ) := lim h→+∞ g h ε (0)/h .
Kohlberg's theorem also implies the j-th entry of χ(g ε ), which we denote by χ j (g ε ), corresponds to the value of the game when it starts at column node j. We refer to [START_REF] Akian | Tropical polyhedra are equivalent to mean payoff games[END_REF] for further details. Following the notation above, we consequently have

v(ε) = χ n+1 (g ε )
for ε 0. The cycle-time vector χ(g ε ) can be expressed in terms of the cycle-time vectors of dynamic programming operators associated with certain one-player games. More precisely, a (positional) strategy for Player Min is a function σ : [n + 1] → [r] associating with each column node j a row node σ(j) such that Mσ(j)j = -∞. Such a strategy defines a one-player game (played by Player Max) over the digraph G σ ε obtained from G ε by deleting the arcs connecting column nodes j with row nodes i such that i = σ(j). Its dynamic programming operator g σ ε is given by:

(g σ ε (x)) j = -Mσ(j)j + max k∈[n+1] Ñσ(j)k =-∞ Ñσ(j)k (ε) + x k , for j ∈ [n + 1].
Observe that this operator is linear in the tropical semiring R max . If we denote by Σ the (finite) set of strategies for Player Min, then as another consequence of Kohlberg's theorem, it can be shown that

χ(g ε ) = min σ∈Σ χ(g σ ε ) . ( 4

.6)

A dual result based on strategies for Player Max can also be established. Given σ ∈ Σ, the (n+1)-th entry of the vector χ(g σ ε ) can be similarly interpreted as the value of the one-player game associated with the digraph G σ ε when it starts at column node n + 1. As the function g σ ε is linear in the tropical semiring, it is known [START_REF] Cochet-Terrasson | A constructive fixed point theorem for min-max functions[END_REF] that χ n+1 (g σ ε ) is equal to the maximal weight-to-length ratio of the elementary circuits of G σ ε reachable from column node n+1. A circuit in this digraph is referred to as a sequence of column nodes j 0 , . . . , j l-1 , j l = j 0 , where l 1, and so l is considered to be its length. Note that the reachability relation in G σ ε does not depend on ε. Let C σ be the set of the elementary circuits of G σ 0 reachable from column node n + 1. By (4.6), we readily obtain

v(ε) = χ n+1 (g ε ) = min σ∈Σ max (j 0 ,...,j l-1 ,j l )∈Cσ 1 l 0 s l-1
-Mσ(js)js + Ñσ(js)js+1 (ε) (4.7) for ε 0. We deduce that:

Lemma 4.4. The function ε → v(ε) is non-increasing and piecewise affine.

Proof. The fact that ε → v(ε) is piecewise affine straightforwardly follows from (4.7).

We next prove by induction on h that the function ε → (g h ε (x)) j is non-increasing for any x ∈ R n and j ∈ [n]. In the first place, observe that ε appears only negatively in the coefficients Ñik (ε) of (4.5), so the function ε → (g ε (x)) j is non-increasing. Now consider h ∈ N and ε ε ′ . By induction, we know that

g h ε ′ (x) g h ε (x) for any x ∈ R n . Since the function x → g ε (x) is order preserving, we have g ε (g h ε ′ (x)) g h+1 ε (x). Besides, g ε (g h ε ′ (x)) g ε ′ (g h ε ′ (x))) = g h+1 ε ′ (x). It follows that (g h+1 ε ′ (x)) j (g h+1 ε (x)) j for all j ∈ [n].
We conclude that ε → v(ε) is non-increasing as the limit of non-increasing functions.

If we assume that the numerical parts of the non-zero entries of M , N , p and q are integers (this assumption is obviously satisfied in the application to timed automata in Section 5), the criterion of Proposition 4.3 can be determined by evaluating v(ε) at ε = 0 and at a small positive value.

Proposition 4.5. The tropical polyhedron with mixed constraints R is non-empty if, and only if, v(0) 1/(n + 1) or v(1/(n + 1) 2 ) 0.

Proof. Each linear piece of the function ε → v(ε) corresponds to an affine map given by the weight-to-length ratio of an elementary circuit of G σ ε for some strategy σ for Player Min. In consequence, this affine map is of the form λ-kε l , where: (i) l is the length of the circuit (l n + 1), (ii) λ is the sum of 2l integers given by the modulus, or their opposite, of some entries of the matrices M and N and of the vectors p and q, (iii) k is the number of occurrences of -ε in the weight N ij (ε) or q i (ε) of some arcs of the circuit (so k l).

Therefore, any non-differentiability point ε of the map ε → v(ε) satisfies (λ-kε)/l = (λ ′k ′ ε)/l ′ , where l ′ , λ ′ , and k ′ have the same properties as l, λ, and k above respectively. It follows that any positive non-differentiability point (if any) is of the form:

ε = λ ′ l -λl ′ k ′ l -l ′ k .
Assume, without loss of generality, that k/l < k ′ /l ′ . Since ε > 0, the numerator λ ′ lλl ′ is a positive integer. This implies that ε ε * , where ε * = 1/(n + 1) 2 . Consequently, the function ε → v(ε) is affine on the interval [0, ǫ * ]. Since it is non-increasing by Lemma 4.4, we have v(ε) < 0 for all ε > 0 if, and only if, v(0) 0 (by continuity) and v(ε * ) < 0. The application of Proposition 4.3 shows that R is non-empty if, and only if, v(0) > 0 or v(ε * ) 0. Since v(0) is equal to the weightto-length ratio of an elementary circuit of G σ 0 , for some σ ∈ Σ, it can be written as λ ′′ /l ′′ , where λ ′′ and l ′′ have the same properties as λ and l above. It follows that v(0) is positive if, and only if, it is greater than or equal to 1/(n + 1). This completes the proof.

Let G ′ 0 be the digraph obtained from G 0 by subtracting 1/(n+1) from the weight of each arc connecting a row node with a column node. Then, v(0)-(1/(n+1)) is the value of the mean payoff game associated with G ′ 0 when it starts from column node n + 1. It follows that the condition of Proposition 4.5 holds if, and only if, column node n + 1 is winning (for Player Max) in one of the two games associated with G ′ 0 and G 1/(n+1) 2 . Let G ⋆ be the digraph obtained as the disjoint union of G ′ 0 and G 1/(n+1) 2 , adding a special row node 0 and two arcs, with zero weight, connecting it with column nodes n + 1 of G ′ 0 and G 1/(n+1) 2 . The criterion of Proposition 4.5 can be restated as follows:

Proposition 4.6. The tropical polyhedron with mixed constraints R is non-empty if, and only if, row node 0 is a winning initial node (for Player Max) in the mean payoff game associated with G ⋆ .

As an immediate consequence, we obtain the following complexity result, in which the equivalence (ii) ⇔ (iii) extends Theorem 3.2 of [START_REF] Akian | Tropical polyhedra are equivalent to mean payoff games[END_REF], whereas the equivalence (i) ⇔ (iii) extends Theorem 18 of [START_REF] Allamigeon | Tropical polar cones, hypergraph transversals, and mean payoff games[END_REF] (only non-strict constraints are considered there). Theorem 4.7. Under Assumption A, the following problems are (Karp) polynomial-time equivalent:

(i) deciding whether a mixed tropical affine inequality is implied by a system of such inequalities; (ii) deciding whether a tropical polyhedron with mixed constraints is empty; (iii) determining whether a given initial node in a mean payoff game is winning.

Problem (iii) is known to be in NP ∩ coNP, see [START_REF] Zwick | The complexity of mean payoff games on graphs[END_REF]. We deduce from Theorem 4.7 that Problems (i) and (ii) both belong to the same complexity class (NP and coNP are closed under Karp reductions). Whether Problem (iii) can be solved in polynomial time has been an open question since the first combinatorial algorithm [START_REF] Gurvich | Cyclic games and an algorithm to find minimax cycle means in directed graphs[END_REF]. Value iteration leads to a pseudo-polynomial algorithm [START_REF] Zwick | The complexity of mean payoff games on graphs[END_REF]. Several algorithms rely on the idea of strategy iteration [START_REF] Howard | Dynamic Programming and Markov Processes[END_REF], applying various strategy improvement rules, see in particular [START_REF] Björklund | A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games[END_REF][START_REF] Cochet-Terrasson | A constructive fixed point theorem for min-max functions[END_REF][START_REF] Dhingra | How to solve large scale deterministic games with mean payoff by policy iteration[END_REF][START_REF] Jurdziński | A deterministic subexponential algorithm for solving parity games[END_REF]. A remarkable example has recently been constructed [START_REF] Friedmann | An exponential lower bound for the parity game strategy improvement algorithm as we know it[END_REF] in which some common rules lead to an exponential number of iterations. However, many algorithms, including the one of [START_REF] Cochet-Terrasson | A constructive fixed point theorem for min-max functions[END_REF][START_REF] Dhingra | How to solve large scale deterministic games with mean payoff by policy iteration[END_REF], are known to have experimentally a small average case number of iterations (growing sublinearly with the dimension), see the benchmarks in [START_REF] Chaloupka | Parallel algorithms for mean-payoff games: An experimental evaluation[END_REF].

The support of a tropically convex set C ⊂ R n max is defined as the set supp(C) of indices j ∈ [n] such that there exists x ∈ C verifying

x j = -∞. Note that supp(C) is the greatest subset J ⊂ [n] such that J = {j ∈ [n] | x j = -∞} for a certain x ∈ C.
Mean payoff games can be used to compute the support of the tropical polyhedron with mixed constraints R. Indeed, j belongs to the support of R if, and only if, j ∈ supp(R ε ) for some ε > 0. By [1, Theorem 3.2], the fact that j ∈ supp(R ε ) is equivalent to χ j (g ε ) 0 and χ n+1 (g ε ) 0, i.e. to the fact that column nodes j and n + 1 are both winning initial nodes for Player Max in the game associated with G ε . Using the same arguments as above, it can be shown that there exists ε > 0 such that χ j (g ε ) 0 if, and only if, χ j (g 0 ) 1/(n + 1) or χ j (g 1/(n+1) 2 ) 0.

In consequence, the support of R can be computed by determining the winning initial nodes in the games associated with G ′ 0 and G 1/(n+1) 2 . We point out that some policy iteration based algorithms, such as the one of [START_REF] Cochet-Terrasson | A constructive fixed point theorem for min-max functions[END_REF][START_REF] Dhingra | How to solve large scale deterministic games with mean payoff by policy iteration[END_REF], directly provide the cycle-time vector χ(g) of the dynamic programming operator g of a mean payoff game (and so all the winning initial nodes).

Remark 4.8. Positional strategies for Player Max are defined symmetrically to the ones for Player Min, i.e. as functions τ from row nodes to column nodes, such that for each row node i there is an arc in G ε connecting it with column node τ (i). Such a strategy τ induces a one-player game (now played by Player Min) whose associated digraph G τ ε is obtained by removing from G ε the arcs connecting row nodes i with columns nodes j such that j = τ (i).

Positional strategies can be used as certificates to ensure that a mean payoff game is winning for one of the players, and these certificates can be checked in polynomial time. For instance, given a column node j ∈ [n + 1], a strategy σ for Player Min satisfying χ j (g σ ε ) 0 ensures that χ j (g ε ) 0 by (4.6). In other words, column node j is a winning initial node for Player Min in the game associated with G ε . Since as explained above χ j (g σ ε ) is given by the maximal weight-to-length ratio of the circuits reachable from column node j in G σ ε , it can be checked that χ j (g σ ε ) is less than or equal to 0 in polynomial time using Karp's algorithm.

Polyhedra defined by systems with +∞ coefficients.

We now deal with the case in which Assumption A is not satisfied. Suppose that the tropical polyhedron with mixed constraints R is defined by (4.4), where now N ∈ G r×n . Observe that we can still assume that q ∈ (G \ {+∞}) r , because any inequality in which q i is equal to +∞ is trivial.

Given I ⊂ [r], we denote by R I the polyhedron defined by the inequalities

M i1 x 1 ⊕ • • • ⊕ M in x n ⊕ p i G (⊕ Nij =+∞ N ij x j ) ⊕ q i for i ∈ I.
The algorithm in Figure 6 determines whether R is empty by evaluating the emptiness of polyhedra of the form R I . To prove the correctness of this algorithm, we shall use the following lemma.

Lemma 4.9. At each iteration of the loop at Line 4, we have R ⊂ R I∪I ′ .

Proof. We prove the lemma by induction on the number of iterations of the loop. Before the first iteration, we have J = [n] and so

I ∪ I ′ = {i ∈ [r] | N ij =
+∞ for all j ∈ [n]}. Thus, the polyhedron R I∪I ′ is defined by a subsystem of M x ⊕ p G N x ⊕ q, and the inclusion R ⊂ R I∪I ′ is immediate.

Input: polyhedron with mixed constraints R defined by the system

M x ⊕ p G N x ⊕ q Output: true if R is empty, false otherwise 1: J := [n] 2: I := ∅ 3: I ′ := {i ∈ [r] | N ij = +∞
for all j ∈ J} 4: while I ′ = ∅ do 5:

I := I ∪ I ′ 6:
if R I is empty then

7:
return true

J := supp(R I )

10:

I ′ := {i ∈ I | N ij = +∞ for all j ∈ J} 11:
end if 12: end while 13: return false Fig. 6. Determining whether a polyhedron with mixed constraints is empty in the general case.

Now suppose that at iteration k we have R ⊂ R I k ∪I ′ k , and let x ∈ R. If the loop is iterated again, then the sets J, I and I ′ are respectively given by

J k+1 = supp(R I k ∪I ′ k ) I k+1 = I k ∪ I ′ k I ′ k+1 = {i ∈ I k+1 | N ij = +∞ for all j ∈ J k+1 }
In consequence, we have supp(R) ⊂ J k+1 , and so x j = -∞ for j ∈ [n] \ J k+1 . Then, we deduce that x satisfies the inequality

M i1 x 1 ⊕ • • • ⊕ M in x n ⊕ p i G (⊕ j∈J k+1 N ij x j ) ⊕ q i G (⊕ Nij =+∞ N ij x j ) ⊕ q i for any i ∈ I ′ k+1 . Thus, we have x ∈ R I ′ k+1 . Since x ∈ R ⊂ R I k ∪I ′ k = R I k+1 , we readily obtain x ∈ R I k+1 ∪I ′
k+1 , which completes the proof.

Proposition 4.10. The algorithm of Figure 6 is correct, and the number of iterations of the loop at Line 4 is bounded by min(n, r).

Proof. Suppose that the algorithm returns true. Then R I = ∅, and by Lemma 4.9 we have R = ∅. Now assume that false is returned. Let x ∈ R I be such that {j ∈ [n] | x j = -∞} = supp(R I ) = J. We claim that x ∈ R. Indeed, since I ′ = ∅ (which is the condition to reach Line 13 and return false), we know that for all i ∈ I there exists j ∈ J such that N ij = +∞. As x j = -∞ for j ∈ J, this means that the i-th inequality of the system M x ⊕ p G N x ⊕ q is satisfied (the right-hand side is equal to +∞). As x also satisfies the inequalities of the system indexed by i ∈ I, the claim is proved.

Finally, observe that at each iteration of the loop, the set I is strictly increased at Line 5. Similarly, if at Line 10 the set I ′ is not empty, then necessarily the set J has been strictly decreased at Line 9. We deduce that the number of iterations is indeed bounded by min(n, r).

The idea behind the algorithm of Figure 6 can be used to build certificates.

Proposition 4.11. The problem of determining whether a polyhedron with mixed constraints is empty belongs to NP ∩ coNP.

Proof. A certificate that R = ∅ can be provided by two sets J ⊂ [n] and I ⊂ [r] such that {i ∈ I | N ij = +∞ for all j ∈ J} = ∅, together with positional strategies ensuring that R I = ∅ and supp(R I ) = J (see Remark 4.8 and the discussion on supports which precedes it). The first property of the sets I and J can be checked in polynomial time, the same as the properties R I = ∅ and supp(R I ) = J thanks to the positional strategies for the players. As shown in the proof of Proposition 4.10, this ensures that R is not empty. In consequence, the problem is in coNP.

To certify that R = ∅, we use a decreasing sequence J 1 = [n], J 2 , . . . , J k of subsets of [n] and an increasing sequence I 1 , . . . , I k of subsets of [r] such that

I l = {i ∈ [r] | N ij = +∞ for all j ∈ J l } ,
for all l ∈ [k], together with positional strategies ensuring that R I l = ∅ and J l+1 = supp(R I l ) for l ∈ [k -1], and that R I k = ∅. Since I l+1 = I l ∪ {i ∈ I l | N ij = +∞ for all j ∈ J l+1 } for l ∈ [k -1], it can be shown by induction on l ∈ [k] that R ⊂ R I l , using the same technique as in the proof of Lemma 4.9. Thus, these certificates allow to prove that R = ∅, and they can be checked in polynomial time. This completes the proof.

Polynomial-time weak redundancy elimination

Since no polynomial-time algorithm is known to evaluate the criteria given in Section 4.1, we also develop a sufficient criterion for which a potentially faster algorithm exists. It consists in checking whether ex ⊕ g G f x ⊕ h is a linear combination of the inequalities in Ax ⊕ c G Bx ⊕ d. Note that in general, this condition is not necessary for (4.1) to hold (the tropical analogue of Farkas' lemma given in [START_REF] Allamigeon | Tropical polar cones, hypergraph transversals, and mean payoff games[END_REF] shows that taking tropical linear combinations does not suffice to deduce all valid inequalities). Now we see the constraint ex ⊕ g G f x ⊕ h as the (2n + 2)-dimensional row vector v := (e, g, f , h). Similarly, we introduce the matrix R ∈ G p×(2n+2) , whose rows are given by the vectors (A i , c i , B i , d i ), for i ∈ [p], where A i and B i denote the i-th rows of A and B respectively. We are reduced to the problem of determining whether there exists a p-dimensional row vector w (with entries in G) such that v = wR. Without loss of generality, we assume that no row of R is identically zero. We propose a method based on residuation theory (see e.g. [START_REF] Gaubert | Methods and applications of (max, +) linear algebra[END_REF]). Given x ∈ G, the self-map z → zx on G can be shown to be residuated, meaning that for each y ∈ G there exists a maximal element of the set {z ∈ G | zx G y}, denoted by y/x. Indeed, the later element is given by:

y → y/x := (|y| -|x|) -if x ∈ R, y ∈ R -, |y| -|x| otherwise,
where it is used the conventions α -

(-∞) = +∞ for α ∈ R max , α -(+∞) = -∞ for α ∈ R max ,
(v j /R ij ) for i ∈ [p].
Then, the inequality ex ⊕ g G f x ⊕ h is a linear combination of the inequalities in the system Ax ⊕ c G Bx ⊕ d if, and only if, v = w * R.

The principle of Proposition 4.12 is that w * can be shown to be the greatest solution of wR G v. Thus, there exists a solution to v = wR if, and only if, the equality is satisfied for w = w * . It follows that the criterion of Proposition 4.12 can be checked efficiently, in time O(n × p).

Complexity of successive Fourier-Motzkin eliminations

As discussed in the beginning of Section 4, propagating redundant inequalities may produce O(p 2 k ) constraints after k calls to Fourier-Motzkin elimination method (recall that p refers to the number of constraints defining the initial polyhedron). We claim that, in the case of closed tropical polyhedra, the number of constraints remains simply exponential at every Fourier-Motzkin elimination when the weak redundancy criterion is used. To see this, let P 0 = P, P 1 , . . . , P k be the closed tropical polyhedra arising during a sequence of k calls to Fourier-Motzkin elimination followed by the weak inequality redundancy elimination of Proposition 4.12. Proposition 4.13. There exists a constant K (independent from k, n, and p) such that for all l ∈ [k], the number of inequalities describing P l obtained using the weak inequality redundancy elimination is bounded by

K(n -l + 1)p ⌊n/2⌋⌊(n-l)/2⌋ . (4.8)
Proof. By the tropical analogue of McMullen's upper bound theorem [START_REF] Allamigeon | The number of extreme points of tropical polyhedra[END_REF], we know that the number q of extreme generators (points and rays) of P is bounded by U (p + n + 1, n), where U (p, n) is the number of facets of (classical) cyclic polytopes with p extreme points in dimension n. In particular, q is bounded by p ⌊n/2⌋ when n and p are sufficiently large (see Appendix Appendix A).

It is straightforward to see that the extreme generators of every polyhedron P l (l ∈ [k]) arise as the projection of some of the extreme generators of P. In consequence, the number of extreme generators of each P l is bounded by q.

Dually, the set of inequalities satisfied by all the points of a tropical polyhedron Q forms a tropical polyhedral cone called the polar cone of Q, see [START_REF] Allamigeon | Tropical polar cones, hypergraph transversals, and mean payoff games[END_REF]. As proved in [START_REF] Allamigeon | The number of extreme points of tropical polyhedra[END_REF], if Q is generated by q points and rays in dimension n-l, the number of (non-trivial) extreme rays of its polar is bounded by (n-l +1)(U (q +n-l +1, n-l)-n+l +2). In particular, this also bounds the size of any description of Q by linearly independent inequalities. It can be shown that there exists a constant K ′ > 0 such that the latter quantity is bounded by K ′ (nl + 1)q ⌊(n-l)/2⌋ for all values of q and nl (see Appendix Appendix A). It follows that the representation by inequalities obtained after the application of the weak redundancy criterion is bounded by a quantity of the form (4.8).

As a consequence, after the (l + 1)-th call to Fourier-Moztkin elimination, the number of inequalities (defining P l+1 ) is bounded by the square of (4.8), and the weak redundancy criterion can be applied in time O((nl) 3 p n(n-l)/2 ). It follows that the complexity of k successive calls to tropical Fourier-Motzkin elimination using the weak redundancy criterion can be bounded by

O(kn 3 p n 2 /2 ) .
Therefore, the time complexity is only exponential in the worst case.

Since the criterion provided by Theorem 4.7 may eliminate further inequalities, the number of inequalities describing P l obtained using this criterion instead of the weak one is also bounded by (4.8). However, this has to be balanced with the potentially greater cost of the associated algorithm for solving mean payoff games.

Tropical Forward Exploration for Timed Automata

Timed automata is one of the formalisms used for modelling and verification of realtime systems. As an application of the methods developed in this paper, we show how the forward exploration algorithm for timed automata [START_REF] Alur | A theory of timed automata[END_REF] can be implemented using tropical polyhedra with mixed constraints as symbolic states. This algorithm is used to solve the reachability problem, to which most verification problems for timed automata can be reduced, see [START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF][START_REF] Alur | Model-checking in dense real-time[END_REF].

We first recall some notions concerning timed automata, and illustrate with an example the drawbacks (mentioned in the introduction) of using zones or closed tropical polyhedra as symbolic states. Note that zones are also used as symbolic states in the verification of other real-time models such as e.g. timed Petri nets [START_REF] Bowden | Modelling time in Petri nets[END_REF][START_REF] Lime | Romeo: A parametric modelchecker for Petri nets with stopwatches[END_REF], hence the corresponding algorithms can potentially benefit from our results too.

We consider a timed automaton over the set of clocks C = {x 1 , . . . , x n }. It is represented by a directed graph whose nodes correspond to locations (l 0 , l 1 , . . . ). We denote by l 0 the initial location and by L the set of locations. An edge from location l to l ′ is denoted by l φ,r -→ l ′ , where φ represents a clock constraint and r a set of reset operations. More precisely, φ is a (possibly empty) conjunction of atomic clock constraints of the form x i ⊲⊳ k and x i ⊲⊳ k + x j , where x i , x j ∈ C, k ∈ Z, and ⊲⊳ ∈ {<, , =, , >}. Besides, r is defined as a partial function from C to N, meaning that x i is mapped to k when the clock x i is reset to the value k.

l 0 l 1 l 2 l 3 l f x 1 := 0 x 2 := 0 x 2 > 1 x 1 > 1 x 1 1 ∧ x 2 1 l 0 : l 1 : l 2 : l 3 : = ∪ l f :
The set of edges is denoted by E. Each location l can be additionally labeled by a clock constraint θ(l). Then, the states of the automaton are of the form (l, v), where l ∈ L and v : C → R ≥0 is such that (v(x 1 ), . . . , v(x n )) satisfies the constraint θ(l).

The evolution of the system (i.e. the semantics of the automaton) is expressed as a transition relation on these states, denoted by . Transitions can be of two kinds:

Delays: where clock values increase synchronously at a given location. More precisely, (l, v) (l, v ′ ) if there exists t 0 such that v ′ (x i ) := v(x i ) + t for all i ∈ [n], and (v(x 1 ) + t ′ , . . . , v(x n ) + t ′ ) satisfies θ(l) for all t ′ ∈ [0, t].

Switches: which are governed by the edges l φ,r -→ l ′ . In this case, we have (l, v) (l ′ , v ′ ) if (v(x 1 ), . . . , v(x n )) satisfies the constraints φ, and v

′ (x i ) := r(x i ) if r is defined on x i , v ′ (x i ) := v(x i ) otherwise.
The basic problem in the verification of timed automata is (untimed) reachability: is a final location l f of the automaton reachable? More precisely, the reachability problem consists in determining whether there exist clock values v f : C → R ≥0 and a finite path (l 0 , v 0 ) * (l f , v f ) of transitions in the automata, where v 0 is the function which maps every x i to 0.

Example 5.1. Consider the timed-automaton fragment depicted in Figure 7, which involves two clocks x 1 and x 2 . Its edges are labeled by the reset operations (for instance, x 1 := 0) and/or the constraints on clocks (for instance, x 2 > 1). As mentioned above, the initial location is l 0 , and the two clocks are initialized to 0.

The diagrams on the right-hand side of Figure 7 depict the symbolic states of this automaton, i.e. the sets of states (clock values) which can arise at each location. For instance, at location l 0 we recover the initial state x 1 = x 2 = 0, and all the other states x 1 = x 2 = t > 0 arise as time goes by while staying at the same location. Similarly, the states at location l 1 are obtained from the ones at location l 0 by resetting clock x 1 , i.e. setting x 1 = 0, while x 2 0 is not affected. Then, as time goes by, we get all the states satisfying 0

x 1 x 2 . Note that the final location l f is not reachable in this example.

The symbolic states at locations l 0 , l 1 and l 2 can be represented exactly by zones, but the one at location l 3 cannot. Hence, the symbolic state at l 3 has to be split, potentially doubling the number of symbolic states to be visited after. If several such timed-automaton fragments are concatenated, it is easy to see that this splitting of symbolic states may lead to a situation where an exponential number of zones have to be used to determine that the final location is not reachable. Alternatively, the symbolic state at location l 3 could be over-approximated by a single zone , but in this case we cannot certify anymore that the final location l f is not reachable. On the other hand, the use of closed tropical polyhedra to over-approximate the union of the sets of states arising from l 1 and l 2 provides the closure of this union, which contains the point (1, 1). Then, the final location l f becomes reachable, while it should not if strict constraints were correctly handled.

The reachability problem can be solved using a symbolic forward exploration algorithm, first given in [START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF], which is still used in state-of-the-art tools. This algorithm, shown in Figure 8, is usually implemented using zones (or DBMs). The algorithm explores sets of reachable states, representing them as symbolic states using zones, and performing symbolic delay and switch operations on them. We do not discuss this algorithm further, but we point out that any class of symbolic states can be used, provided that it supports the operations is empty, is included, intersect, reset, and delay used in the above algorithm. We now detail the definition of these operations, and show how to implement them over tropical polyhedra with mixed constraints.

The operation is empty(P) determines whether the polyhedron P is empty. It is implemented using the methods described in Section 4.1, i.e. through a reduction to mean payoff games. The operation is included(P 1 , P 2 ) checks if P 1 ⊂ P 2 . This can be performed using the procedure for deciding implications of Section 4.1, by determining whether the system of inequalities defining P 1 implies each defining inequality of the polyhedron P 2 . The operation intersect ψ (P) computes the intersection of P with the constraints in ψ. It is simply defined by appending the inequalities in ψ to the system defining P, where any strict constraint in ψ is encoded as an inequality over G using elements of the form λ -. The operation reset xi:=k (P) consists in computing the polyhedron {y ∈ R n max | x ∈ P, y j = x j if j = i, y i = k} .

It can be obtained by eliminating x i in the system of constraints defining P using Fourier-Motzkin elimination, and then intersecting the resulting polyhedron with the constraint x i = k (encoded as two inequalities x i G k and k G x i ). Finally, the operation delay(P) consists in converting the polyhedron P into the set {λx | Choose and remove (l, V ) from Waiting if (not is included(V, V ′ )) for all (l, V ′ ) ∈ Passed then for all l φ,r -→ l ′ do 10:

V ′ := intersect θ(l ′ ) (delay(resetr(intersect φ (V ))

11:

if not is empty(V ′ ) then 12:

Waiting := Waiting ∪ {(l ′ , V ′ )} x ∈ P, λ 0} (recall that λx corresponds to the vector with entries λ + x i ). Assuming that P is given by the system Ax ⊕ c G Bx ⊕ d, we first let Q be the polyhedron defined by Ax ⊕ λc G Bx ⊕ λd and 0 G λ, and then apply Fourier-Motzkin elimination on λ to get delay(P). To prove this algorithm is correct, observe that:

delay(P) = {λx ∈ R n max | 0 G λ, Ax ⊕ c G Bx ⊕ d} = {x ∈ R n max | 0 G λ, A(λ -1 x) ⊕ c G B(λ -1 x) ⊕ d} = {x ∈ R n max | 0 G λ, Ax ⊕ λc G Bx ⊕ λd} .
To combat state space explosion, symbolic states are also equipped with an over-approximating union operator. In this way, symbolic states which are reached through different paths may be recombined, leading to a significant reduction in the number of symbolic states the forward exploration algorithm has to consider. Given two polyhedra with mixed constraints P, P ′ ⊂ R n max , the over-approximation union operator over approx(P, P ′ ) is defined as the tropical convex hull of P ∪ P ′ . Note that given systems of mixed inequalities describing P and P ′ , a system describing over approx(P, P ′ ) can be computed by means of Proposition 3.5. As this involves 2n + 2 calls to tropical Fourier-Motzkin elimination, it is crucial to implement some redundancy elimination.

Observe that the error introduced using the operation over approx over polyhedra with mixed constraints is smaller than using zone-based over-approximation. Indeed, zones are tropically convex, and thus any zone containing P ∪ P ′ also contains the tropical convex hull of P ∪ P ′ . In the example of Figure 7, the over-approximating union by polyhedra with mixed constraints of the two sets of states arising at l 3 is exact, and given by the polyhedron defined by x 1 , x 2 G 0 and 1 G 0 -x 1 ⊕ 0 -x 2 , or equivalently, 1 < max(x 1 , x 2 ).

We have implemented a prototype of the forward exploration algorithm based on tropical polyhedra with mixed constraints. The algorithms of Section 3 and the operations described above have been implemented within the OCaml library TPLib [START_REF] Allamigeon | TPLib: Tropical polyhedra library in OCaml[END_REF], whose purpose is to provide algorithms for tropical polyhedra. It relies on the library MPGLib [START_REF] Allamigeon | MPGLib: Mean payoff games library[END_REF], which implements the algorithm in [START_REF] Dhingra | How to solve large scale deterministic games with mean payoff by policy iteration[END_REF] for solving mean payoff games by policy iteration. Our prototype successfully checks that location l f is not reachable in the timed automaton of Figure 7. In future works, we plan to apply our method on more representative examples taken from real case studies, and to compare it in terms of performance/precision with state-of-the-art tools such as Uppaal [START_REF] Behrmann | UPPAAL 4.0[END_REF]. and if n is odd,

U (p + n + 1, n) = 2
p + 1 + ⌊n/2⌋ ⌊n/2⌋ .

In both cases, it can be easily checked that Using the same arguments, we obtain that:

U (p + n +
U (q + nl + 1, nl) q ⌊(n-l)/2⌋

as soon as q 6 and nl 12. In any case, we can find a constant K ′ > 0 such that for all values of q and nl, U (q + nl + 1, nl) K ′ q ⌊(n-l)/2⌋

Assuming that q U (p + n + 1, n), it follows that for a certain constant K ′′ > 0,

(nl + 1)(U (q + nl + 1, nl)n + l + 2) K ′′ (nl + 1)p ⌊n/2⌋⌊(n-l)/2⌋ if p 6 and n 12. This allows to show that there exists K > 0 such that for all p, n, and l ∈ [n -1],

(nl + 1)(U (q + nl + 1, nl)n + l + 2) K(nl + 1)p ⌊n/2⌋⌊(n-l)/2⌋ .

2 Fig. 1 .

 21 Fig.1. Left: a tropical polyhedron (including the black border). Right: a (non-closed) zone defined by the inequalities 1 x 1 < 7, 1 < x 2 5, -2 < x 1x 2 3.

Fig. 2 .

 2 Fig. 2. Hasse diagram of the order G over the elements of G with modulus in Z ∪ {±∞}.

  and x, y = ±∞ ; -∞ if x = -∞ or y = -∞ ; +∞ if x, y = -∞, and x = +∞ or y = +∞ .

(

  ii) Straightforward from Property (i). (iii) This property readily follows from the definition of the multiplication. (iv) If z = ±∞, the first property is straightforward, so assume |z| ∈ R. Let x < G y (the implication is trivial when x = y). If |x| < |y|, we have |xz| < |yz| because z = ±∞. Moreover, if |x| = |y| =: α, then α = ±∞ (as x and y are distinct), and thus necessarily x = α -and y = α (because x < G y). Hence xz ∈ R - and |xz| = |yz|. In both cases, we conclude that xz G yz. Conversely, assume that z ∈ R. Using the first part of the proof, xz G yz implies x G y by multiplying both sides of the inequality xz G yz by z -1 .

Lemma 2 . 5 .

 25 Let a, b ∈ R max and c, d ∈ G. The set of solutions in R max of the mixed tropical affine inequality ax⊕b G cx⊕d is given by {x ∈ R max | b G cx⊕d} if a G c, and by {x ∈ R max | ax ⊕ b G d} otherwise.

2 Fig. 3 .

 23 Fig. 3. Tropical polyhedra with mixed constraints (the ends of the black segments marked by points are included in the polyhedra).

Fig. 4 .

 4 Fig. 4. Left: a tropical polyhedron with mixed constraints, together with an open mixed halfspace (in blue) defining it. Right: the closed polyhedron defined by the corresponding non-strict inequalities.

Lemma 3 . 2 .

 32 Let (S, ⊕, ⊗, 0, 1, S ) be a totally ordered idempotent semiring. Then, for all a, b ∈ S, a ⊕ b = a if a S b, and a ⊕ b = b otherwise. Proof. First, observe that b S 0 implies a⊕b S a. Analogously, we have a⊕b S b. Now suppose that a S b. Then, a = a ⊕ b since a = a ⊕ a S a ⊕ b.

Example 3 . 8 .

 38 Consider the tropical hemispace H defined as the set of vectors x ∈ R 4 max such that (x 3 x 1 and x 4 x 1 ) or (x 3 x 2 and x 4 < x 2 ) .

Fig. 5 .

 5 Fig. 5. The digraph associated with a parametric mean payoff game (column and row nodes are respectively represented by circles and squares).

Proposition 4 . 12 .

 412 and (+∞) -(+∞) = +∞. Define the p-dimensional row vector w * by w * i := min j∈[2n+2]

Fig. 7 .

 7 Fig. 7. Left: Timed automaton. Right: Symbolic states accumulated during forward exploration, shown after delays (black borders are included in the depicted gray regions).

Input:

  timed automaton (L, l 0 , C, θ, E), l f ∈ L Output: true if ∃v f : C → R ≥0 : (l 0 , v 0 ) * (l f , v f ),false otherwise 1: Waiting := {(l 0 , intersect θ(l0) (delay({v 0 })))}; Passed := ∅ 2: while Waiting = ∅ do 3:

8 :

 8 Passed := Passed ∪ {(l, V )} 9:

Fig. 8 .

 8 Fig. 8. The symbolic forward reachability algorithm for timed automata.

1 m

 1 ln 1 + p + 1 m + m = m ln e(p + 1 + m) m m ln p as soon as e(p + m + 1) pm. The latter condition is satisfied if p 6 and m 6. This shows that (A.1) holds when p 6 and n 12.

  , implication (4.1) holds if, and only if, Q is empty. Bx⊕d and ex⊕g > G f x⊕h. Observe that ex⊕g > G f x⊕h holds if, and only

	max such that Proof. Implication (4.1) is false if, and only if, there exists x ∈ R n Ax⊕c G

  We claim that for p and n sufficiently large,U (p + n + 1, n) p ⌊n/2⌋ . (A.1)Let m := ⌊n/2⌋. By Stirling approximation formulas, we know that for all positive

				1, n) 2	p + 1 + ⌊n/2⌋ ⌊n/2⌋	.
	integer h,	√	2πh(h/e) h h! e	√	h(h/e) h
	As a result,
	p + 1 + m m	e 2π	p + 1 + m (p + 1)m	1 +	p + 1 m	m	1 +	m p + 1

Xavier Allamigeon, Uli Fahrenberg, Stéphane Gaubert, Ricardo D. Katz, Axel Legay

Xavier Allamigeon, Uli Fahrenberg, Stéphane Gaubert, Ricardo D. Katz, Axel Legay

Xavier Allamigeon, Uli Fahrenberg, Stéphane Gaubert, Ricardo D. Katz, Axel Legay

Acknowledgments

The authors warmly thank Alexandre David for helpful discussions on the algorithms involved in the verification of timed automata. The authors are also grateful to the anonymous referee for his comments and suggestions which helped to improve the paper.

* The five authors were partially supported by the programme "Ingénierie Numérique & Sécurité" of the French National Agency of Research (ANR), project "MALTHY", number ANR-13-INSE-0003. Xavier Allamigeon was partially supported by the same programme, project "CAFEIN", number ANR-12-INSE-0007. Ricardo D. Katz was partially supported by CONICET Grant PIP 112-201101-01026. Xavier Allamigeon, Ricardo D. Katz and Stéphane Gaubert were partially supported by the PGMO program of EDF and Fondation Mathématique Jacques Hadamard. Uli Fahrenberg and Axel Legay were partially supported by the EU IP project DANSE and by the regional CREATE Estase initiative.

Appendix A. Additional Details for the Proof of Proposition 4.13

We first recall that:

for n even,

for n odd.

Thus, if n is even,