Skip to Main content Skip to Navigation
Journal articles

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

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).
Complete list of metadata

Cited literature [47 references]  Display  Hide  Download

https://hal.inria.fr/hal-01087367
Contributor : Uli Fahrenberg <>
Submitted on : Wednesday, November 26, 2014 - 3:23:53 PM
Last modification on : Tuesday, June 15, 2021 - 4:27:49 PM
Long-term archiving on: : Friday, February 27, 2015 - 10:56:32 AM

File

main-IJAC-hal.pdf
Files produced by the author(s)

Identifiers

Citation

Xavier Allamigeon, Axel Legay, Uli Fahrenberg, Ricardo Katz, Stéphane Gaubert. Tropical Fourier–Motzkin elimination, with an application to real-time verification. International Journal of Algebra and Computation, World Scientific Publishing, 2014, 24 (5), pp.569 - 607. ⟨10.1142/S0218196714500258⟩. ⟨hal-01087367⟩

Share

Metrics

Record views

1032

Files downloads

462