Tropical polyhedra have been recently used to represent disjunctive
invariants in static analysis. To handle larger instances, tropical analogues
of classical linear programming results need to be developed. This motivation
leads us to study a general tropical linear programming problem. We construct
an associated parametric mean payoff game problem, and show that the optimality
of a given point, or the unboundedness of the problem, can be certified by
exhibiting a strategy for one of the players having certain infinitesimal
properties (involving the value of the game and its derivative) that we
characterize combinatorially. In other words, strategies play in tropical
linear programming the role of Lagrange multipliers in classical linear
programming. We use this idea to design a Newton-like algorithm to solve
tropical linear programming problems, by reduction to a sequence of auxiliary
mean payoff game problems.