TY - GEN
T1 - Finite abstractions of stochastic Max-Plus-Linear systems
AU - Adzkiya, Dieky
AU - Esmaeil Zadeh Soudjani, Sadegh
AU - Abate, Alessandro
N1 - Funding Information:
The first two authors have equally contributed to this work. This work has been supported by the European Commission via STREP project MoVeS 257005, Marie Curie grant MANTRAS 249295, and IAPP project AMBI 324432.
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
KW - Abstractions
KW - Approximate probabilistic bisimulations
KW - Continuous state spaces
KW - Discrete-time stochastic processes
KW - Max-plus algebra
KW - Max-plus-linear systems
UR - http://www.scopus.com/inward/record.url?scp=84907375968&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-10696-0_7
DO - 10.1007/978-3-319-10696-0_7
M3 - Conference contribution
AN - SCOPUS:84907375968
SN - 9783319106953
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 74
EP - 89
BT - Quantitative Evaluation of Systems - 11th International Conference, QEST 2014, Proceedings
PB - Springer Verlag
T2 - 11th International Conference on Quantitative Evaluation of Systems, QEST 2014
Y2 - 8 September 2014 through 10 September 2014
ER -