Stochastic Omega-Regular Verification and Control with Supermartingales
<|reference_start|>Stochastic Omega-Regular Verification and Control with Supermartingales: We present for the first time a supermartingale certificate for $\omega$-regular specifications. We leverage the Robbins & Siegmund convergence theorem to characterize supermartingale certificates for the almost-sure acceptance of Streett conditions on general stochastic processes, which we call Streett supermartingales. This enables effective verification and control of discrete-time stochastic dynamical models with infinite state space under $\omega$-regular and linear temporal logic specifications. Our result generalises reachability, safety, reach-avoid, persistence and recurrence specifications; our contribution applies to discrete-time stochastic dynamical models and probabilistic programs with discrete and continuous state spaces and distributions, and carries over to deterministic models and programs. We provide a synthesis algorithm for control policies and Streett supermartingales as proof certificates for $\omega$-regular objectives, which is sound and complete for supermartingales and control policies with polynomial templates and any stochastic dynamical model whose post-expectation is expressible as a polynomial. We additionally provide an optimisation of our algorithm that reduces the problem to satisfiability modulo theories, under the assumption that templates and post-expectation are in piecewise linear form. We have built a prototype and have demonstrated the efficacy of our approach on several exemplar $\omega$-regular verification and control synthesis problems.<|reference_end|>
@article{abate2024stochastic,
    title={Stochastic Omega-Regular Verification and Control with Supermartingales},
    author={Alessandro Abate, Mirco Giacobbe, Diptarko Roy},
    journal={arXiv preprint arXiv:2405.17304},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.17304},
    primaryClass={cs.LO cs.SY eess.SY}
}