Finite abstractions of max-plus-linear systems


Reference:
D. Adzkiya, B. De Schutter, and A. Abate, "Finite abstractions of max-plus-linear systems," IEEE Transactions on Automatic Control, vol. 58, no. 12, pp. 3039-3053, Dec. 2013.

Abstract:
This work puts forward a novel technique to generate finite abstractions of autonomous and nonautonomous Max-Plus-Linear (MPL) models, a class of discrete-event systems used to characterize the dynamics of the timing related to successive events that synchronize autonomously. Nonautonomous versions of MPL models embed within their dynamics nondeterminism, namely a signal choice that is usually regarded as an exogenous control or schedule. In this paper, abstractions of MPL models are characterized as finite-state Labeled Transition Systems (LTS). LTS are obtained first by partitioning the state space (and, for the nonautonomous model, by covering the input space) of the MPL model and by associating states of the LTS to the introduced partitions, then by defining relations among the states of the LTS based on dynamical transitions between the corresponding partitions of the MPL state space, and finally by labeling the LTS edges according to the one-step timing properties of the events of the original MPL model. In order to establish formal equivalences, the finite abstractions are proven to either simulate or to bisimulate the original MPL model. This approach enables the study of general properties of the original MPL model by verifying (via model checking) equivalent logical specifications over the finite LTS abstraction. The computational aspects related to the abstraction procedure are thoroughly discussed and its performance is tested on a numerical benchmark.


Downloads:
 * Online version of the paper
 * Corresponding technical report: pdf file (328 KB)
      Note: More information on the pdf file format mentioned above can be found here.


Bibtex entry:

@article{AdzDeS:13-018,
        author={D. Adzkiya and B. {D}e Schutter and A. Abate},
        title={Finite abstractions of max-plus-linear systems},
        journal={IEEE Transactions on Automatic Control},
        volume={58},
        number={12},
        pages={3039--3053},
        month=dec,
        year={2013},
        doi={10.1109/TAC.2013.2273299}
        }



Go to the publications overview page.


This page is maintained by Bart De Schutter. Last update: August 15, 2017.