Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
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…
cs.LO2025
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…
cs.LO2024
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…