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.