VeriSiMPL 2: An open-source software for the verification of max-plus-linear systems

Dieky Adzkiya*, Yining Zhang, Alessandro Abate

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

5 Citations (Scopus)


This work presents a technique to generate finite abstractions of autonomous Max-Plus-Linear (MPL) systems, a class of discrete-event systems employed to characterize the dynamics of the timing related to the synchronization of successive events. Abstractions of MPL systems are derived as finite-state transition systems. A transition system is obtained first by partitioning the state space of the MPL system into finitely many regions and then by associating a unique state of the transition system to each partitioning region. Relations among the states of the transition system are then set up based on the underlying dynamical transitions between the corresponding partitioning regions of the MPL state space. In order to establish formal equivalences, the obtained finite abstractions are proven either to simulate or to bisimulate the original MPL system. The approach enables the study of general properties of the original MPL system formalized as logical specifications, by verifying them over the finite abstraction via model checking. The article presents a new, extended and improved implementation of a software tool (available online) for the discussed formal abstraction of MPL systems, and is tested on a numerical benchmark against a previous version.

Original languageEnglish
Pages (from-to)109-145
Number of pages37
JournalDiscrete Event Dynamic Systems: Theory and Applications
Issue number1
Publication statusPublished - 1 Mar 2016


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


Dive into the research topics of 'VeriSiMPL 2: An open-source software for the verification of max-plus-linear systems'. Together they form a unique fingerprint.

Cite this