Multiplicative Barrier Certificates for Probabilistic Safety of Markov Jump Systems
(2024) IFAC-PapersOnLine — Vol. 58, n° 11, p. 63-68 (2024)
Files
1-s20-S2405896324005251-main.pdf
Open Access - Adobe PDF
- 1.64 MB
Details
- Authors
- Abstract
- This work offers a formal framework for providing safety certificates over discrete-time Markov jump systems (MJSs). Our proposed scheme centers around a new concept of multiplicative barrier certificates (MBCs), enabling us to establish a probabilistic lower bound for the safety property in infinite time horizons within this class of models. In particular, while a summative barrier certificate, as commonly proposed in the relevant literature, may not be available to ensure the safety of MJS models, we introduce an alternative approach in a multiplicative form, as opposed to the conventional “decreasing in mean” formulation. We demonstrate that in scenarios where a summative barrier does not exist, there is potential for the existence of a multiplicative counterpart. We also provide a systematic methodology grounded on the counterexample-guided inductive synthesis (CEGIS) scheme to systematically construct the proposed multiplicative certificates. We showcase the efficacy of our approach through its application in an air traffic management system.
- Affiliations
Citations
Samari, B., Rossa, M. D., Lavaei, A., Soudjani, S., & Jungers, R. (2024). Multiplicative Barrier Certificates for Probabilistic Safety of Markov Jump Systems. IFAC-PapersOnLine, 58(11), 63-68. https://doi.org/10.1016/j.ifacol.2024.07.426 (Original work published 2024)