SMT-Based Reachability Analysis of High Dimensional Interval Max-Plus Linear Systems

This article discusses the reachability analysis (RA) of interval max-plus linear (IMPL) systems, a subclass of continuous-space, discrete-event systems defined over the max-plus algebra. Unlike standard max-plus linear systems, where the transition matrix is fixed at each discrete step, IMPL systems allow for uncertainty on state matrices. Given an initial and a target set, we develop algorithms to verify the existence of IMPL system trajectories that, starting from the initial set, eventually reach the target set. We show that RA can be solved by encoding the IMPL system, as well as initial and target sets, into linear real arithmetic expressions, and then checking the satisfaction of a resulting logical formula via a satisfiability modulo theory (SMT) solver. The performance and scalability of the developed SMT-based algorithms are shown to drastically outperform state-of-the-art RA algorithms applied to IMPL systems, which promises to usher their use in practical, industrial-sized IMPL models.