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 -re…
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 Verification with Neural Networks
Alessandro Abate, Alec Edwards, Mirco Giacobbe +2
We present a data-driven approach to the quantitative verification of probabilistic programs and stochastic dynamical models. Our approach leverages neural networks to compute tigh…
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…