Algorithmics of tropical polyhedra, and applications

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.