Paper Info
Title
SMT-Based Reachability Analysis of High Dimensional Interval Max-Plus Linear Systems
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.
Year
DOI
Venue
2022
10.1109/TAC.2021.3090525
IEEE Transactions on Automatic Control
Keywords
DocType
Volume
Difference-bound matrices (DBMs),linear real arithmetic (LRA),max-plus linear (MPL) systems,piecewise-affine (PWA) systems,reachability analysis (RA),satisfiability modulo theory (SMT)
Journal
67
Issue
ISSN
Citations 
6
0018-9286
0
PageRank 
References 
Authors
0.34
20
3
Name
Order
Citations
PageRank
Muhammad Syifa'ul Mufid101.35
Dieky Adzkiya2358.29
Alessandro Abate300.34