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

TL;DR

This paper introduces an SMT-based method to analyze the transient behavior of Max-Plus Linear systems, enabling the study of initial state subsets and outperforming existing algebraic techniques for large systems.

Contribution

It presents a novel SMT-based approach for transient analysis in MPL systems, allowing analysis of specific initial state subsets and their periodic behaviors.

Findings

Significantly faster analysis for large systems

Ability to characterize initial state sets with identical transients

Outperforms algebraic methods in efficiency

Abstract

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.