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

• 成果类型: Article
• 署名作者: Mufid, Muhammad Syifa'ul; Adzkiya, Dieky; Abate, Alessandro
• 署名单位: University of Oxford; Institut Teknologi Sepuluh Nopember
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2021.3090525
• 发表日期: 2022
• 页码: 2700-2714
• 关键词: Multiprotocol label switching; Algebra; reachability analysis; Analytical models; uncertainty; trajectory; Linear systems; Difference-bound matrices (DBMs); linear real arithmetic (LRA); max-plus linear (MPL) systems; piecewise-affine (PWA) systems; reachability analysis (RA); satisfiability modulo theory (SMT)

摘要

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.