Reference
D. Adzkiya, B. De Schutter, and A. Abate, "Abstraction and verification of
autonomous max-plus-linear systems,"
Proceedings of the 2012
American Control Conference, Montréal, Canada, pp. 721-726, June
2012.
Abstract
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.
Downloads
BibTeX
@inproceedings{AdzDeS:12-010,
author = {Adzkiya, Dieky and De Schutter, Bart and Abate, Alessandro},
title = {Abstraction and Verification of Autonomous Max-Plus-Linear
Systems},
booktitle = {Proceedings of the 2012 American Control Conference},
address = {Montr\'eal, Canada},
pages = {721--726},
month = jun,
year = {2012}
}