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

Xavier Allamigeon 1, 2 Axel Legay 3 Uli Fahrenberg 3 Ricardo Katz 4 Stéphane Gaubert 1, 2
1 MAXPLUS - Max-plus algebras and mathematics of decision
CMAP - Centre de Mathématiques Appliquées - Ecole Polytechnique, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
3 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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).
Type de document :
Article dans une revue
International Journal of Algebra and Computation (IJAC), 2014, 24 (5), pp.569 - 607. 〈10.1142/S0218196714500258〉
Liste complète des métadonnées

Littérature citée [47 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01087367
Contributeur : Uli Fahrenberg <>
Soumis le : mercredi 26 novembre 2014 - 15:23:53
Dernière modification le : mercredi 16 mai 2018 - 11:24:07
Document(s) archivé(s) le : vendredi 27 février 2015 - 10:56:32

Fichier

main-IJAC-hal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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 (IJAC), 2014, 24 (5), pp.569 - 607. 〈10.1142/S0218196714500258〉. 〈hal-01087367〉

Partager

Métriques

Consultations de la notice

665

Téléchargements de fichiers

192