TY - GEN
T1 - Forward reachability computation for autonomous max-plus-linear systems
AU - Adzkiya, Dieky
AU - De Schutter, Bart
AU - Abate, Alessandro
N1 - Funding Information:
This work has been supported by the European Commission STREP project MoVeS 257005, by the European Commission Marie Curie grant MANTRAS 249295, by the European Commission IAPP project AMBI 324432, by the European Commission NoE Hycon2 257462, and by the NWO VENI grant 016.103.020.
PY - 2014
Y1 - 2014
N2 - This work discusses the computation of forward reachability for autonomous (that is, deterministic) Max-Plus-Linear (MPL) systems, a class of continuous-space discrete-event models that are relevant for applications dealing with synchronization and scheduling. Given an MPL model and a set of initial states, we characterize and compute its "reach tube," namely the sequential collection of the sets of reachable states (these sets are regarded step-wise as "reach sets"). We show that the exact computation of the reach sets can be quickly and compactly performed by manipulations of difference-bound matrices, and derive explicit worst-case bounds for the complexity of these operations. The concepts and techniques are implemented within the toolbox VeriSiMPL, and are practically elucidated by a running example. We further display the computational performance of the approach by two concluding numerical benchmarks: the technique comfortably handles reachability computations over twenty-dimensional MPL models (i.e., models with twenty continuous variables), and it clearly outperforms an alternative state-of-the-art approach in the literature.
AB - This work discusses the computation of forward reachability for autonomous (that is, deterministic) Max-Plus-Linear (MPL) systems, a class of continuous-space discrete-event models that are relevant for applications dealing with synchronization and scheduling. Given an MPL model and a set of initial states, we characterize and compute its "reach tube," namely the sequential collection of the sets of reachable states (these sets are regarded step-wise as "reach sets"). We show that the exact computation of the reach sets can be quickly and compactly performed by manipulations of difference-bound matrices, and derive explicit worst-case bounds for the complexity of these operations. The concepts and techniques are implemented within the toolbox VeriSiMPL, and are practically elucidated by a running example. We further display the computational performance of the approach by two concluding numerical benchmarks: the technique comfortably handles reachability computations over twenty-dimensional MPL models (i.e., models with twenty continuous variables), and it clearly outperforms an alternative state-of-the-art approach in the literature.
UR - http://www.scopus.com/inward/record.url?scp=84900557249&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-54862-8_17
DO - 10.1007/978-3-642-54862-8_17
M3 - Conference contribution
AN - SCOPUS:84900557249
SN - 9783642548611
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 248
EP - 262
BT - Tools and Algorithms for the Construction and Analysis of Systems - 20th Int. Conf., TACAS 2014, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2014, Proc.
PB - Springer Verlag
T2 - 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
Y2 - 5 April 2014 through 13 April 2014
ER -