Computation of Transient in Max-Plus Linear Systems via SMT-Solving

Alessandro Abate, Alessandro Cimatti, Andrea Micheli and Syifa'ul Mufid

This paper proposes a new approach, grounded in Satisfiability Modulo Theories (SMT), to study the transient of a Max-Plus Linear (MPL) system, that is the number of steps leading to the periodic regime. Differently from state-of-the-art techniques, our approach allows the analysis of periodic behaviors for subsets of initial states, and the characterization of initial states exhibiting a specific periodic behavior and transient. Our experiments show that the proposed technique dramatically outperforms state-of-the-art methods based on max-plus algebra computations for systems of large dimensions.