4 papers
Value Functions as Supermartingale Certificates
Alessandro Abate, Daniel Contro, Mirco Giacobbe +2
Certification methods for stochastic systems provide sufficient proof rules, based on real-valued supermartingale certificates, to determine the almost-sure satisfaction of -reg…
Complete -Regular Supermartingale Certificates
Alessandro Abate, Mirco Giacobbe, Sergey Ichtchenko +1
We introduce a general methodology for the construction of sound and complete proof rules for the almost-sure and quantitative acceptance of reactivity properties on time-homogeneo…
Quantitative Supermartingale Certificates
Alessandro Abate, Mirco Giacobbe, Diptarko Roy
We introduce a general methodology for quantitative model checking and control synthesis with supermartingale certificates. We show that every specification that is invariant to ti…
Stochastic Omega-Regular Verification and Control with Supermartingales
Alessandro Abate, Mirco Giacobbe, Diptarko Roy
We present for the first time a supermartingale certificate for -regular specifications. We leverage the Robbins & Siegmund convergence theorem to characterize supermartingale c…