Forward reachability computation for autonomous max-plus-linear systems


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:
 * Corresponding technical report: pdf file (223 KB)
      Note: More information on the pdf file format mentioned above can be found here.


Bibtex entry:

@inproceedings{AdzDeS:14-010,
        author={D. Adzkiya and B. {D}e Schutter and A. Abate},
        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}
        }



Go to the publications overview page.


This page is maintained by Bart De Schutter. Last update: July 3, 2018.