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.