  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 its periodic regime. Differently from
state-of-the-art techniques, our approach allows the analysis of periodic
behaviors for subsets of initial states, as well as the characterization of
sets of initial states exhibiting the same 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.
