Formal verification of stochastic max-plus-linear systems

Sadegh Esmaeil Zadeh Soudjani, Dieky Adzkiya, Alessandro Abate

Research output: Contribution to journalArticlepeer-review

13 Citations (Scopus)


This work investigates the computation of finite abstractions of Stochastic Max-Plus-Linear (SMPL) systems and their formal verification against general bounded-time linear temporal specifications. SMPL systems are probabilistic extensions of discrete-event MPL systems, which are widely employed for modeling engineering systems dealing with practical timing and synchronization issues. Departing from the standard existing approaches for the analysis of SMPL systems, we newly propose to construct formal, finite abstractions of a given SMPL system: the SMPL system is first re-formulated as a discrete-time Markov process, then abstracted as a finite-stateMarkov Chain (MC). The derivation of precise guarantees on the level of the introduced formal approximation allows us to probabilistically model check the obtained MC against bounded-time linear temporal specifications (which are of rather general applicability), and to reliably export the obtained results over the original SMPL system. The approach is practically implemented on a dedicated software and is elucidated and run over numerical examples.

Original languageEnglish
Article number7335578
Pages (from-to)2861-2876
Number of pages16
JournalIEEE Transactions on Automatic Control
Issue number10
Publication statusPublished - 2016


  • Continuous-state processes
  • Discrete-time stochastic processes
  • Finite abstractions
  • Linear-time logic max-plus algebra
  • Max-plus-linear (MPL) systems
  • Probabilisticmodel checking


Dive into the research topics of 'Formal verification of stochastic max-plus-linear systems'. Together they form a unique fingerprint.

Cite this