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.
Publisher page
Downloads
BibTeX
@article{AdzDeS:13-018,
author = {Adzkiya, Dieky and De Schutter, Bart and Abate, Alessandro},
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}
}