论文标题
通过SMT解决的最大线性系统中的瞬态计算
Computation of the Transient in Max-Plus Linear Systems via SMT-Solving
论文作者
论文摘要
本文提出了一种基于满意度模型理论（SMT）的新方法，以研究最大值线性（MPL）系统的瞬态，即导致其周期性制度的步骤数。与最先进的技术不同，我们的方法允许分析初始状态子集的周期性行为，以及表现出相同特定周期性行为和瞬态的初始状态集的表征。我们的实验表明，该技术基于对大维系统系统的最大代数计算的最高代数计算，大大优于最先进的方法。
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.
