Multiplicative Barrier Certificates for Probabilistic Safety of Markov Jump Systems

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.