Skip to main navigation Skip to search Skip to main content

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

  • University of Oxford
  • Fondazione Bruno Kessler

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

5 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationFormal Modeling and Analysis of Timed Systems - 18th International Conference, FORMATS 2020, Proceedings
EditorsNathalie Bertrand, Nils Jansen
PublisherSpringer
Pages161-177
Number of pages17
ISBN (Print)9783030576271
DOIs
Publication statusPublished - 2020
Externally publishedYes
Event18th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2020 - Vienna, Austria
Duration: 1 Sept 20203 Sept 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12288 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2020
Country/TerritoryAustria
CityVienna
Period1/09/203/09/20

Fingerprint

Dive into the research topics of 'Computation of the Transient in Max-Plus Linear Systems via SMT-Solving'. Together they form a unique fingerprint.

Cite this