Stochastic Omega-Regular Verification and Control with Supermartingales

TL;DR

This paper introduces supermartingale certificates for verifying and controlling stochastic systems against omega-regular specifications, enabling effective analysis of complex probabilistic models with infinite states.

Contribution

It develops a novel supermartingale-based framework for omega-regular verification and control, including a synthesis algorithm and optimization techniques for polynomial and linear templates.

Findings

Effective verification of omega-regular properties on stochastic models.

Control synthesis with sound and complete algorithms.

Prototype implementation demonstrates practical applicability.

Abstract

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.