Abstraction and verification of autonomous Max-Plus-Linear systems

Dieky Adzkiya*, Bart De Schutter, Alessandro Abate

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

4 Citations (Scopus)


This work investigates the use of finite abstractions for the verification of autonomous Max-Plus-Linear (MPL) models. Abstractions are characterized as finite-state labeled transition systems (LTS) and are obtained by first partitioning the state space of the MPL and associating states of the LTS to the partitions, then by defining relations among the vertices of the LTS, corresponding to dynamical transitions between the MPL state partitions, and finally by labeling the LTS edges according to one-step time properties of the events of the MPL model. In order to establish formal equivalences, the finite LTS abstraction is proven to either simulate or to bisimulate the original MPL model, the difference depending on its determinism. The computational performance of the abstraction procedure is tested on a benchmark. The work then studies properties of the original MPL model by verifying equivalent specifications on the finite LTS abstraction.

Original languageEnglish
Title of host publication2012 American Control Conference, ACC 2012
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages6
ISBN (Print)9781457710957
Publication statusPublished - 2012
Externally publishedYes
Event2012 American Control Conference, ACC 2012 - Montreal, QC, Canada
Duration: 27 Jun 201229 Jun 2012

Publication series

NameProceedings of the American Control Conference
ISSN (Print)0743-1619


Conference2012 American Control Conference, ACC 2012
CityMontreal, QC


Dive into the research topics of 'Abstraction and verification of autonomous Max-Plus-Linear systems'. Together they form a unique fingerprint.

Cite this