Complete Supermartingale Certificates for $\omega$-Regular Properties

TL;DR

This paper develops a comprehensive methodology for constructing sound and complete proof rules for reactivity properties, including $$-regular properties, on Markov chains with general state spaces, extending previous results to countably infinite states.

Contribution

It introduces a general approach to decompose reactivity properties into obligations, enabling complete proof rules for almost-sure and quantitative acceptance on general state spaces.

Findings

First sound and complete supermartingale certificates for almost-sure $$-regular properties.

First sound and $$-complete supermartingale certificates for quantitative $$-regular properties.

Extension of proof rules from almost-sure termination to reactivity properties.

Abstract

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-homogeneous Markov chains with general state spaces. Reactivity captures $\omega$-regular properties and subsumes linear temporal logic. Our core technical result establishes that every reactivity property admits decomposition into multiple obligations of almost-sure termination into absorbing regions, and that appropriate absorbing regions always exist on general state spaces. This enables the extension of every complete proof rule for almost-sure termination into a proof rule for reactivity that is complete in the almost-sure case, and complete up to an arbitrarily small $\varepsilon$-approximation in the quantitative case. We apply our new methodology to recent results on sound and complete supermartingale certificates for almost-sure termination in the special case of countably infinite state spaces, alongside standard results on quantitative safety. As a result, we obtain the first sound and complete supermartingale certificates for almost-sure $\omega$-regular properties and the first sound and $\varepsilon$-complete supermartingale certificates for quantitative $\omega$-regular properties on time-homogeneous Markov chains with countably infinite state spaces.