Computational techniques for reachability analysis of Max-Plus-Linear systems

被引:27
|
作者
Adzkiya, Dieky [1 ]
De Schutter, Bart [1 ]
Abate, Alessandro [1 ,2 ]
机构
[1] Delft Univ Technol, Delft Ctr Syst & Control, NL-2628 CD Delft, Netherlands
[2] Univ Oxford, Dept Comp Sci, Oxford OX1 3QD, England
关键词
Max-Plus-Linear systems; Forward and backward reachability analysis; Reach tube and reach set; Piecewise affine systems; Difference-bound matrices; TIMED AUTOMATA; HYBRID SYSTEMS; PETRI NETS; VERIFICATION; ALGEBRA; THEOREM; SETS;
D O I
10.1016/j.automatica.2015.01.002
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
This work discusses a computational approach to reachability analysis of Max-Plus-Linear (MPL) systems, a class of discrete-event systems widely used in synchronization and scheduling applications. Given a set of initial states, we characterize and compute its "reach tube," namely the collection of set of reachable states (regarded step-wise as "reach sets"). By an alternative characterization of the MPL dynamics, we show that the exact computation of the reach sets can be performed quickly and compactly by manipulations of difference-bound matrices, and further derive worst-case bounds on the complexity of these operations. The approach is also extended to backward reachability analysis. The concepts and results are elucidated by a running example, and we further illustrate the performance of the approach by a numerical benchmark: the technique comfortably handles twenty-dimensional MPL systems (i.e. with twenty continuous state variables), and as such it outperforms the state-of-the-art alternative approaches in the literature. (C) 2015 Elsevier Ltd. All rights reserved.
引用
收藏
页码:293 / 302
页数:10
相关论文
共 50 条