Finite abstractions of stochastic Max-Plus-Linear systems

Dieky Adzkiya, Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate

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

5 Citations (Scopus)


This work investigates the use of finite abstractions to study the finite-horizon probabilistic invariance problem over Stochastic Max-Plus-Linear (SMPL) systems. SMPL systems are probabilistic extensions of discrete-event MPL systems that are widely employed in the engineering practice for timing and synchronisation studies. We construct finite abstractions by re-formulating the SMPL system as a discrete-time Markov process, then tailoring formal abstraction techniques in the literature to generate a finite-state Markov Chain (MC), together with precise guarantees on the level of the introduced approximation. This finally allows to probabilistically model check the obtained MC against the finite-horizon probabilistic invariance specification. The approach is practically implemented via a dedicated software, and elucidated in this work over numerical examples.

Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems - 11th International Conference, QEST 2014, Proceedings
PublisherSpringer Verlag
Number of pages16
ISBN (Print)9783319106953
Publication statusPublished - 2014
Externally publishedYes
Event11th International Conference on Quantitative Evaluation of Systems, QEST 2014 - Florence, Italy
Duration: 8 Sept 201410 Sept 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8657 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference11th International Conference on Quantitative Evaluation of Systems, QEST 2014


  • Abstractions
  • Approximate probabilistic bisimulations
  • Continuous state spaces
  • Discrete-time stochastic processes
  • Max-plus algebra
  • Max-plus-linear systems


Dive into the research topics of 'Finite abstractions of stochastic Max-Plus-Linear systems'. Together they form a unique fingerprint.

Cite this