On the Computation and Approximation of Backward Reachable Sets for Max-Plus Linear Systems using Polyhedras
Yuda Li, Shaoyuan Li, Xiang Yin
TL;DR
This work tackles backward reachability in max-plus linear systems (MPLS) for general, potentially non-convex targets by introducing a tropical-polyhedra based approximation framework. It replaces the exponential complexity of Difference Bounds Matrix (DBM) methods with a symbolic propagation approach that leverages closure- and projection-based techniques, representing sets via outer (M-form) and inner (V-form) tropical polyhedra. The method includes extremal filtering to keep the generating sets compact and provides both one-step and finite-horizon (N-step) backward reachability analyses. The resulting framework enables scalable approximate backward reachability, supporting safety verification and controller synthesis for broader target geometries within MPLS.
Abstract
This paper investigates reachability analysis for max-plus linear systems (MPLS), an important class of dynamical systems that model synchronization and delay phenomena in timed discrete-event systems. We specifically focus on backward reachability analysis, i.e., determining the set of states that can reach a given target set within a certain number of steps. Computing backward reachable sets presents significant challenges due to the non-convexity of max-plus dynamics and the complexity of set complement operations. To address these challenges, we propose a novel approximation framework that efficiently computes backward reachable sets by exploiting the structure of tropical polyhedra. Our approach reformulates the problem as a sequence of symbolic operations and approximates non-convex target sets through closure operations on unions of tropical polyhedra. We develop a systematic algorithm that constructs both outer (M-form) and inner (V-form) representations of the resulting sets, incorporating extremal filtering to reduce computational complexity. The proposed method offers a scalable alternative to traditional DBM-based approaches, enabling reliable approximate backward reachability analysis for general target regions in MPLS.