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
(368 KB)
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}
}
This page is maintained by Bart De Schutter.
Last update: February 21, 2026.