Complete Supermartingale Certificates for $\omega$-Regular Properties
Alessandro Abate, Mirco Giacobbe, Sergey Ichtchenko, Diptarko Roy

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 -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 -approximation in the quantitative case. We apply our new methodology to recent results on sound and complete supermartingale…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
