Stochastic Omega-Regular Verification and Control with Supermartingales

Alessandro Abate, Mirco Giacobbe, Diptarko Roy

We present for the first time a supermartingale certificate for $\omega$-regular specifications. We leverage the Robbins & Siegmund convergence theorem to characterize supermartingale c…