k-Inductive Barrier Certificates for Stochastic Systems
Mahathi Anand, Vishnu Murali, Ashutosh Trivedi, Majid Zamani · 2022
Barrier certificates are inductive invariants that provide guarantees on the safety and reachability behaviors of continuous dynamical systems. For stochastic dynamical systems, barrier certificates take the form of inductive “expectation” invariants. In this context, a barrier certificate is a non-negative real-valued function over the state space of the system satisfying a strong supermartingale condition: it decreases in expectation as the system evolves The existence of barrier certificates, then, provides lower bounds on the probability of satisfaction of safety or reachability specifications over unbounded-time horizons. Unfortunately, establishing supermartingale conditions on barrier certificates can often be restrictive. In practice, we strive to overcome this challenge by utilizing a weaker condition called c-martingale that permits a bounded increment in expectation at every time step; unfortunately this only guarantees the property of interest for a bounded time horizon.