On the Computation and Approximation of Backward Reachable Sets for Max-Plus Linear Systems using Polyhedras

TL;DR

This paper introduces a novel approximation framework for backward reachability analysis in max-plus linear systems, leveraging tropical polyhedra to efficiently compute reachable sets despite non-convexities.

Contribution

It proposes a systematic algorithm that constructs outer and inner representations of backward reachable sets using tropical polyhedra, improving scalability over traditional methods.

Findings

Efficient approximation of backward reachable sets using tropical polyhedra.

Scalable algorithm for constructing outer and inner set representations.

Reliable analysis for general target regions in max-plus linear systems.

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.