Xavier Allamigeon

We study the tropical analogue of the notion of polar of a cone, working over the semiring of tropical numbers with signs. We characterize the cones which arise as polars of sets of tropically nonnegative vectors by an invariance property with respect to a tropical analogue of Fourier–Motzkin elimination. We also relate tropical polars with images by the nonarchimedean valuation of classical polars over real closed nonarchimedean fields and show, in particular, that for semi-algebraic sets over such fields, the operation of taking the polar commutes with the operation of signed valuation (keeping track both of the nonarchimedean valuation and sign). We apply these results to characterize images by the signed valuation of classical cones of matrices, including the cones of positive semidefinite matrices, completely positive matrices, completely positive semidefinite matrices, and their polars, including the cone of co-positive matrices, showing that hierarchies of classical cones collapse under tropicalization. We finally discuss an application of these ideas to optimization with signed tropical numbers.

The purpose of this paper is the formal verification of a counterexample of Santos et al. to the so-called Hirsch Conjecture on the diameter of polytopes (bounded convex polyhedra). In contrast with the pen-and-paper proof, our approach is entirely computational: we implement in Coq and prove correct an algorithm that explicitly computes, within the proof assistant, vertex-edge graphs of polytopes as well as their diameter. The originality of this certificate-based algorithm is to achieve a tradeoff between simplicity and efficiency. Simplicity is crucial in obtaining the proof of correctness of the algorithm. This proof splits into the correctness of an abstract algorithm stated over proof-oriented data types and the correspondence with a low-level implementation over computation-oriented data types. A special effort has been made to reduce the algorithm to a small sequence of elementary operations (e.g., matrix multiplications, basic routines on sets and graphs), in order to make the derivation of the correctness of the low-level implementation more transparent. Efficiency allows us to scale up to polytopes with a challenging combinatorics. For instance, we formally check the two counterexamples of Matschke, Santos and Weibel to the Hirsch conjecture, respectively 20- and 23-dimensional polytopes with 36 425 and 73 224 vertices involving rational coefficients with up to 40 digits in their numerator and denominator. We also illustrate the performance of the method by computing the list of vertices or the diameter of well-known classes of polytopes, such as (polars of) cyclic polytopes involved in McMullen's Upper Bound Theorem.

Linear complementarity programming is a generalization of linear programming which encompasses the computation of Nash equilibria for bimatrix games. While the latter problem is PPAD-complete, we show that the tropical analogue of the complementarity problem associated with Nash equilibria can be solved in polynomial time. Moreover, we prove that the Lemke--Howson algorithm carries over the tropical setting and performs a linear number of pivots in the worst case. A consequence of this result is a new class of (classical) bimatrix games for which Nash equilibria computation can be done in polynomial time.

We study timed Petri nets, with preselection and priority routing. We represent the behavior of these systems by piecewise affine dynamical systems. We use tools from the theory of nonexpansive mappings to analyze these systems. We establish an equivalence theorem between priority-free fluid timed Petri nets and semi-Markov decision processes, from which we derive the convergence to a periodic regime and the polynomial-time computability of the throughput. More generally, we develop an approach inspired by tropical geometry, characterizing the congestion phases as the cells of a polyhedral complex. We illustrate these results by a current application to the performance evaluation of emergency call centers in the Paris area.

Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistant Coq. This builds on the formalization of a library providing the basic constructions and operations over polyhedra, including projections, convex hulls and images under linear maps. Moreover, we design a special mechanism which automatically introduces an appropriate representation of a polyhedron or a face, depending on the context of the proof. We demonstrate the usability of this approach by establishing some of the most important combinatorial properties of faces, namely that they constitute a family of graded atomistic and coatomistic lattices closed under sublattices.

We exhibit a class of classical or tropical posynomial systems which can be solved by reduction to linear or convex programming problems. This relies on a notion of colorful vectors with respect to a collection of Newton polytopes. This extends the convex programming approach of one player stochastic games.