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

被引:28
作者
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
相关论文
共 48 条
[31]   Transience bounds for long walks [J].
Hartmann, M ;
Arguelles, C .
MATHEMATICS OF OPERATIONS RESEARCH, 1999, 24 (02) :414-439
[32]   Equivalence of hybrid dynamical models [J].
Heemels, WPMH ;
De Schutter, B ;
Bemporad, A .
AUTOMATICA, 2001, 37 (07) :1085-1091
[33]  
Heidergott B., 2006, Max Plus at work: modeling and analysis of synchronized systems: a course on Max -Plus algebra and its applications
[34]  
Henzinger TA, 1998, LECT NOTES COMPUT SC, V1386, P190
[35]   PERFORMANCE EVALUATION OF JOB-SHOP SYSTEMS USING TIMED EVENT-GRAPHS [J].
HILLION, HP ;
PROTH, JM .
IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 1989, 34 (01) :3-9
[36]   An Automated Framework for Formal Verification of Timed Continuous Petri Nets [J].
Kloetzer, Marius ;
Mahulea, Cristian ;
Belta, Calin ;
Silva, Manuel .
IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS, 2010, 6 (03) :460-471
[37]  
Kurzhanskiy A.A., 2006, TECHNICAL REPORT
[38]   Ellipsoidal techniques for reachability analysis of discrete-time linear systems [J].
Kurzhanskiy, Alex A. ;
Varaiya, Pravin .
IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2007, 52 (01) :26-38
[39]  
Le Guernic C, 2009, LECT NOTES COMPUT SC, V5643, P540, DOI 10.1007/978-3-642-02658-4_40
[40]   Reachability analysis for timed automata using max-plus algebra [J].
Lu, Qi ;
Madsen, Michael ;
Milata, Martin ;
Ravn, Soren ;
Fahrenberg, Uli ;
Larsen, Kim G. .
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2012, 81 (03) :298-313