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

DOI10.1142/S0218196714500258zbMath1301.90069arXiv1308.2122OpenAlexW3104719736MaRDI QIDQ2923336

Axel Legay, Uli Fahrenberg, Stéphane Gaubert, Ricardo D. Katz, Xavier Allamigeon

Publication date: 15 October 2014

Published in: International Journal of Algebra and Computation (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1308.2122

zbMATH Keywords

timed automatamean payoff gamesstrict inequalitiesFourier-Motzkin eliminationreal-time verificationtropical polyhedra

Mathematics Subject Classification ID

Convex programming (90C25) Computational aspects related to convexity (52B55) Fractional programming (90C32) Axiomatic and generalized convexity (52A01) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Combinatorial games (91A46) Max-plus and related algebras (15A80)

Related Items

The Tropical Nullstellensatz and Positivstellensatz for Sparse Polynomial Systems ⋮ Reachability of eigenspaces for interval circulant matrices in max-algebra ⋮ Approximating the volume of tropical polytopes is difficult ⋮ Interval robustness of (interval) max-plus matrices ⋮ Max-plus steady states in discrete event dynamic systems with inexact data ⋮ Conditional independence in max-linear Bayesian networks

Uses Software

• Uppaal
• TPLib

Cites Work

• Unnamed Item
• Tropical linear-fractional programming and parametric mean payoff games
• Reachability analysis for timed automata using max-plus algebra
• Tropical polar cones, hypergraph transversals, and mean payoff games
• The number of extreme points of tropical polyhedra
• Minimal half-spaces and external representation of tropical polyhedra
• Model-checking in dense real-time
• A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games
• The Minkowski theorem for max-plus convex sets
• Generators, extremals and bases of max cones
• A theory of timed automata
• Symbolic model checking for real-time systems
• The complexity of mean payoff games on graphs
• Computing the vertices of tropical polyhedra using directed hypergraphs
• Carathéodory, Helly and the others in the max-plus world
• The level set method for the two-sided max-plus eigenproblem
• Characterization of tropical hemispaces by \((P, R)\)-decompositions
• Cyclic projectors and separation theorems in idempotent convex geometry
• TROPICAL POLYHEDRA ARE EQUIVALENT TO MEAN PAYOFF GAMES
• Cyclic games and an algorithm to find minimax cycle means in directed graphs
• Invariant Half-Lines of Nonexpansive Piecewise-Linear Transformations
• The duality theorem for min-max functions
• Scheduling with AND/OR Precedence Constraints
• -convexity
• A constructive fixed point theorem for min-max functions
• Tropical Polytopes and Cellular Resolutions
• The Max-Atom Problem and Its Relevance
• Idempotent functional analysis: An algebraic approach