On the Computation of Backward Reachable Sets for Max-Plus Linear Systems with Disturbances

TL;DR

This paper presents a tropical polyhedra-based computational framework for backward reachability analysis in uncertain max-plus linear systems, enabling efficient safety verification.

Contribution

It introduces a novel approach that preserves tropical-polyhedral structure for computing backward reachable sets under disturbances.

Findings

Operators preserve tropical-polyhedral structure

Framework enables constructive computation of reachable sets

Illustrative examples demonstrate effectiveness

Abstract

This paper investigates one-step backward reachability for uncertain max-plus linear systems with additive disturbances. Given a target set, the problem is to compute the set of states from which there exists an admissible control input such that, for all admissible disturbances, the successor state remains in the target set. This problem is closely related to safety analysis and is challenging due to the high computational complexity of existing approaches. To address this issue, we develop a computational framework based on tropical polyhedra. We assume that the target set, the control set, and the disturbance set are all represented as tropical polyhedra, and study the structural properties of the associated backward operators. In particular, we show that these operators preserve the tropical-polyhedral structure, which enables the constructive computation of reachable sets within the same framework. The proposed approach provides an effective geometric and algebraic tool for reachability analysis of uncertain max-plus linear systems. Illustrative examples are included to demonstrate the proposed method.