Computation of the Transient in Max-Plus Linear Systems via SMT-Solving
Systems and Control
2020-07-09 v2 Logic in Computer Science
Systems and Control
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.
Cite
@article{arxiv.2007.00505,
title = {Computation of the Transient in Max-Plus Linear Systems via SMT-Solving},
author = {Alessandro Abate and Alessandro Cimatti and Andrea Micheli and Muhammad Syifa'ul Mufid},
journal= {arXiv preprint arXiv:2007.00505},
year = {2020}
}
Comments
The paper consists of 22 pages (including references and Appendix). It is accepted in FORMATS 2020 First revision