User menu

Accès à distance ? S'identifier sur le proxy UCLouvain

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

Primary tabs

Allamigeon, Xavier Legay, Axel [UCL] Fahrenberg, Uli Katz, Ricardo Gaubert, Stéphane

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).

Document type Article de périodique (Journal article) – Article de recherche
Publication date 2014
Language Anglais
Journal information "International Journal of Algebra and Computation (IJAC)" - Vol. 24, no. 5, p. 569-607 (2014)
Publisher World Scientific Pub Co Pte Lt
Publication status Publié
Affiliation UCL - SST/ICTM/INGI - Pôle en ingénierie informatique
Links
  1. AKIAN MARIANNE, GAUBERT STÉPHANE, GUTERMAN ALEXANDER, TROPICAL POLYHEDRA ARE EQUIVALENT TO MEAN PAYOFF GAMES, 10.1142/s0218196711006674
  2. Allamigeon Xavier, Gaubert Stéphane, Goubault Éric, Computing the Vertices of Tropical Polyhedra Using Directed Hypergraphs, 10.1007/s00454-012-9469-6
  3. Allamigeon Xavier, Gaubert Stéphane, Katz Ricardo D., The number of extreme points of tropical polyhedra, 10.1016/j.jcta.2010.04.003
  4. Allamigeon Xavier, Gaubert Stéphane, Katz Ricardo D., Tropical polar cones, hypergraph transversals, and mean payoff games, 10.1016/j.laa.2011.02.004
  5. Alur R., Courcoubetis C., Dill D., Model-Checking in Dense Real-Time, 10.1006/inco.1993.1024
  6. Alur Rajeev, Dill David L., A theory of timed automata, 10.1016/0304-3975(94)90010-8
  7. Bezem Marc, Nieuwenhuis Robert, Rodríguez-Carbonell Enric, The Max-Atom Problem and Its Relevance, Logic for Programming, Artificial Intelligence, and Reasoning (2008) ISBN:9783540894384 p.47-61, 10.1007/978-3-540-89439-1_4
  8. Björklund Henrik, Vorobyov Sergei, A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games, 10.1016/j.dam.2006.04.029
  9. Briec Walter, Horvath Charles, -convexity, 10.1080/02331930410001695283
  10. Briec W., Pacific J. Optim., 4, 293 (2008)
  11. Butkovič Peter, Schneider Hans, Sergeev Sergei˘, Generators, extremals and bases of max cones, 10.1016/j.laa.2006.10.004
  12. Butkovič P., Ekon.-Mat., 20, 203 (1984)
  13. Cochet-Terrasson Jean, Gaubert Stephane, Gunawardena Jeremy, A constructive fixed point theorem for min-max functions, 10.1080/026811199281967
  14. Cohen Guy, Gaubert Stéphane, Quadrat Jean-Pierre, Max-plus algebra and system theory: Where we are and where to go now, 10.1016/s1367-5788(99)90091-3
  15. Cohen Guy, Gaubert Stéphane, Quadrat Jean-Pierre, Singer Ivan, Max-plus convex sets and functions, 10.1090/conm/377/06987
  16. A. David, Model-Based Design for Embedded Systems, eds. G. Nicolescu and P. J. Mosterman (CRC Press, 2010) pp. 93–119.
  17. Develin M., Doc. Math., 9, 1 (2004)
  18. Develin Mike, Yu Josephine, Tropical Polytopes and Cellular Resolutions, 10.1080/10586458.2007.10129009
  19. Gaubert Séphane, Gunawardena Jeremy, The duality theorem for min-max functions, 10.1016/s0764-4442(97)82710-3
  20. Gaubert S., Kybernetika, 40, 153 (2004)
  21. Gaubert Stéphane, Katz Ricardo D., The Minkowski theorem for max-plus convex sets, 10.1016/j.laa.2006.09.019
  22. Gaubert Stéphane, Katz Ricardo D., Minimal half-spaces and external representation of tropical polyhedra, 10.1007/s10801-010-0246-4
  23. Gaubert Stéphane, Katz Ricardo D., Sergeev Sergeĭ, Tropical linear-fractional programming and parametric mean payoff games, 10.1016/j.jsc.2011.12.049
  24. Gaubert Stéphane, Meunier Frédéric, Carathéodory, Helly and the Others in the Max-Plus World, 10.1007/s00454-009-9207-x
  25. Gaubert S., Sergeev S., Cyclic projectors and separation theorems in idempotent convex geometry, 10.1007/s10958-008-9243-8
  26. Gaubert Stéphane, Sergeev Sergeĭ, The level set method for the two-sided max-plus eigenproblem, 10.1007/s10626-012-0137-z
  27. Gurvich V.A., Karzanov A.V., Khachivan L.G., Cyclic games and an algorithm to find minimax cycle means in directed graphs, 10.1016/0041-5553(88)90012-2
  28. Henzinger T.A., Nicollin X., Sifakis J., Yovine S., Symbolic Model Checking for Real-Time Systems, 10.1006/inco.1994.1045
  29. Howard R. A., Dynamic Programming and Markov Processes (1960)
  30. M. Joswig, Combinatorial and computational geometry, Mathematical Science Research Institute Publications 52 (Cambridge University Press, Cambridge, 2005) pp. 409–431.
  31. Katz Ricardo D., Nitica Viorel, Sergeev Sergeĭ, Characterization of tropical hemispaces by (P,R)-decompositions, 10.1016/j.laa.2013.10.029
  32. Kohlberg Elon, Invariant Half-Lines of Nonexpansive Piecewise-Linear Transformations, 10.1287/moor.5.3.366
  33. Kot Martin, Modeling selected real-time database concurrency control protocols in Uppaal, 10.1007/s11334-009-0086-3
  34. Lime Didier, Roux Olivier H., Seidner Charlotte, Traonouez Louis-Marie, Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches, Tools and Algorithms for the Construction and Analysis of Systems (2009) ISBN:9783642007675 p.54-57, 10.1007/978-3-642-00768-2_6
  35. Litvinov G. L., Maslov V. P., Shpiz G. B., 10.1023/a:1010266012029
  36. Lu Qi, Madsen Michael, Milata Martin, Ravn Søren, Fahrenberg Uli, Larsen Kim G., Reachability analysis for timed automata using max-plus algebra, 10.1016/j.jlap.2011.10.004
  37. Möhring Rolf H., Skutella Martin, Stork Frederik, Scheduling with AND/OR Precedence Constraints, 10.1137/s009753970037727x
  38. Zimmermann K., Ekon.-Mat., 13, 179 (1977)
  39. Zwick Uri, Paterson Mike, The complexity of mean payoff games on graphs, 10.1016/0304-3975(95)00188-3
Bibliographic reference Allamigeon, Xavier ; Legay, Axel ; Fahrenberg, Uli ; Katz, Ricardo ; Gaubert, Stéphane. Tropical Fourier–Motzkin elimination, with an application to real-time verification. In: International Journal of Algebra and Computation (IJAC), Vol. 24, no. 5, p. 569-607 (2014)
Permanent URL https://hdl.handle.net/2078.1/210467