Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Stochastic Omega-Regular Verification and Control with Supermartingales

Alessandro Abate, Mirco Giacobbe, Diptarko Roy

TL;DR

The paper addresses the challenge of verifying and controlling $\omega$-regular specifications for stochastic processes with infinite state spaces. It introduces Streett supermartingales, a new certificate based on the Robbins–Siegmund convergence theorem, to characterize almost-sure Streett acceptance and enables joint synthesis of per-pair certificates, supporting invariants, and control policies. The authors show that, under piecewise polynomial or linear templates, the synthesis reduces to decision procedures in NRA, QF_NRA, QCP, or LP, and they provide a prototype demonstrating effectiveness on continuous-state systems across safety, persistence, recurrence, and reactivity properties. This approach preserves the probabilistic dynamics and unifies and extends prior martingale-based methods, offering a scalable, certificate-based path to automated $\omega$-regular verification and control for infinite-state models.

Abstract

We present for the first time a supermartingale certificate for $ω$-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 $ω$-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 $ω$-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 $ω$-regular verification and control synthesis problems.

Stochastic Omega-Regular Verification and Control with Supermartingales

TL;DR

The paper addresses the challenge of verifying and controlling -regular specifications for stochastic processes with infinite state spaces. It introduces Streett supermartingales, a new certificate based on the Robbins–Siegmund convergence theorem, to characterize almost-sure Streett acceptance and enables joint synthesis of per-pair certificates, supporting invariants, and control policies. The authors show that, under piecewise polynomial or linear templates, the synthesis reduces to decision procedures in NRA, QF_NRA, QCP, or LP, and they provide a prototype demonstrating effectiveness on continuous-state systems across safety, persistence, recurrence, and reactivity properties. This approach preserves the probabilistic dynamics and unifies and extends prior martingale-based methods, offering a scalable, certificate-based path to automated -regular verification and control for infinite-state models.

Abstract

We present for the first time a supermartingale certificate for -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 -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 -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 -regular verification and control synthesis problems.
Paper Structure (2 sections, 2 theorems, 4 equations, 2 figures)

This paper contains 2 sections, 2 theorems, 4 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Streett Supermartingales

Key Result

theorem thmcountertheorem

Let $\{{\cal F}_t \}$ be a filtration and let $\{V_t \}$, $\{U_t \}$, and $\{W_t \}$ be three real-valued nonnegative stochastic processes adapted to $\{ {\cal F}_t \}$. Suppose that, for all $t \in \mathbb{N}$, the following statement holds almost surely: Then,

Figures (2)

  • Figure 1: A simple infinite-state stochastic process over variable $x \in \mathbb{Z}$. Above, the value of a Streett supermartingale for the reactivity property ${\sf GF}(x \text{ is even}) \lor {\sf FG} (x < 0)$.
  • Figure 2: Intuition for \ref{['thm:streett-supermartingale']} on exemplar trajectories.

Theorems & Definitions (2)

  • theorem thmcountertheorem: Robbins & Siegmund Convergence Theorem RobbinsSiegmund1971
  • theorem thmcountertheorem: Streett Supermartingales