-A A +A

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

TitleComputation of the Transient in Max-Plus Linear Systems via SMT-Solving
Publication TypeConference Paper
Year of Publication2020
AuthorsAbate A, Cimatti A, Micheli A, Mufid MSyifa'Ul
Conference NameFORMATS 2020
Date Published09/2020

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.


Oxford Control and Verification (OXCAV) Group

C/O Department of Computer Science

Wolfson Building, Parks Rd, Oxford OX1 3QD

T: +44 (0) 18656 10767

Education - This is a contributing Drupal Theme
Design by WeebPal.