Reference
D. Adzkiya, B. De Schutter, and A. Abate, "Forward reachability computation for
autonomous max-plus-linear systems,"
Proceedings of the 20th
International Conference on Tools and Algorithms for the Construction and
Analysis of Systems (TACAS 2014), Grenoble, France, pp. 248-262, Apr.
2014.
Abstract
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.
Downloads
BibTeX
@inproceedings{AdzDeS:14-010,
author = {Adzkiya, Dieky and De Schutter, Bart and Abate, Alessandro},
title = {Forward Reachability Computation for Autonomous Max-Plus-Linear
Systems},
booktitle = {Proceedings of the 20th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS
2014)},
address = {Grenoble, France},
pages = {248--262},
month = apr,
year = {2014}
}