SMT-Based Reachability Analysis of High Dimensional Interval Max-Plus Linear Systems

Muhammad Syifaaul Mufid*, Dieky Adzkiya, Alessandro Abate

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)

Abstract

This article discusses the reachability analysis (RA) of interval max-plus linear (IMPL) systems, a subclass of continuous-space, discrete-event systems defined over the max-plus algebra. Unlike standard max-plus linear systems, where the transition matrix is fixed at each discrete step, IMPL systems allow for uncertainty on state matrices. Given an initial and a target set, we develop algorithms to verify the existence of IMPL system trajectories that, starting from the initial set, eventually reach the target set. We show that RA can be solved by encoding the IMPL system, as well as initial and target sets, into linear real arithmetic expressions, and then checking the satisfaction of a resulting logical formula via a satisfiability modulo theory (SMT) solver. The performance and scalability of the developed SMT-based algorithms are shown to drastically outperform state-of-the-art RA algorithms applied to IMPL systems, which promises to usher their use in practical, industrial-sized IMPL models.

Original languageEnglish
Pages (from-to)2700-2714
Number of pages15
JournalIEEE Transactions on Automatic Control
Volume67
Issue number6
DOIs
Publication statusPublished - 1 Jun 2022

Keywords

  • Difference-bound matrices (DBMs)
  • linear real arithmetic (LRA)
  • max-plus linear (MPL) systems
  • piecewise-affine (PWA) systems
  • reachability analysis (RA)
  • satisfiability modulo theory (SMT)

Fingerprint

Dive into the research topics of 'SMT-Based Reachability Analysis of High Dimensional Interval Max-Plus Linear Systems'. Together they form a unique fingerprint.

Cite this