Abstraction and verification of autonomous Max-Plus-Linear systems

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.