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

TL;DR

This paper introduces a generalized tropical Fourier-Motzkin elimination method for tropical polyhedra, enabling analysis of strict and non-strict inequalities with applications to real-time system verification.

Contribution

It develops a tropical analogue of Fourier-Motzkin elimination, characterizes tropical polyhedra, and proposes efficient algorithms for inequality reduction with applications to timed automata.

Findings

Tropical polyhedra coincide with tropically convex unions of cells.

Redundant inequalities can be dynamically eliminated via mean payoff game reduction.

Polynomial-time deletion procedures lead to exponential bounds on total execution time.

Abstract

We introduce a generalization of tropical polyhedra able to express both strict and non-strict inequalities. Such inequalities are handled by means of a semiring of germs (encoding infinitesimal perturbations). We develop a tropical analogue of Fourier-Motzkin elimination from which we derive geometrical properties of these polyhedra. In particular, we show that they coincide with the tropically convex union of (non-necessarily closed) cells that are convex both classically and tropically. We also prove that the redundant inequalities produced when performing successive elimination steps can be dynamically deleted by reduction to mean payoff game problems. As a complement, we provide a coarser (polynomial time) deletion procedure which is enough to arrive at a simply exponential bound for the total execution time. These algorithms are illustrated by an application to real-time systems (reachability analysis of timed automata).