# Algorithmics of tropical polyhedra, and applications

Xavier Allamigeon (INRIA Saclay)Tropical polyhedra are the analogues of convex polyhedra in tropical algebra.
Tropical algebra refers to the set **R** ∪ {-∞} endowed with max as addition
and + as multiplication.

We develop a tropical analogue of the classical double description method,
allowing one to compute an internal representation (in terms of vertices) of a
polyhedron defined externally (by inequalities). The heart of the method is a
characterization of the extreme points of a tropical polyhedron in terms of a
system of constraints which define it. We show that a point of a tropical
polyhedron is extreme if and only if a directed hypergraph which we construct
from the subdifferentials of the active constraints at this point admits a
unique terminal strongly connected component. The latter property can be
checked in almost linear time, which allows us to eliminate quickly redundant
generators. We provide theoretical worst case complexity bounds and report
extensive experimental tests performed using an *OCaml* implementation called
*TPLib* , showing that this method outperforms the previous ones. We also
discuss some extensions and applications to software verification.