Finite abstractions of max-plus-linear systems

Dieky Adzkiya, Bart De Schutter, Alessandro Abate

Research output: Contribution to journalArticlepeer-review

26 Citations (Scopus)


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.

Original languageEnglish
Article number6558835
Pages (from-to)3039-3053
Number of pages15
JournalIEEE Transactions on Automatic Control
Issue number12
Publication statusPublished - Dec 2013
Externally publishedYes


  • Bisimulations
  • Difference-bound matrices
  • Discrete-event systems
  • Labeled transition systems
  • Max-plus algebra
  • Model abstractions
  • Model checking
  • Piece-wise affine models


Dive into the research topics of 'Finite abstractions of max-plus-linear systems'. Together they form a unique fingerprint.

Cite this