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:


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: March 1, 2025.