Paper: Complete ω-Regular Supermartingale Certificates (at LICS 2026)

Authors: Alessandro Abate Mirco Giacobbe Sergey Ichtchenko Diptarko Roy

Open access: https://doi.org/10.4230/LIPIcs.LICS.2026.3

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 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 ω-regular properties and the first sound and ε-complete supermartingale certificates for quantitative ω-regular properties on time-homogeneous Markov chains with countably infinite state spaces.

BibTeX

  @InProceedings{AbateGiacobbeIchtch-CompleteRegularSupe,
    author = 	 {Alessandro Abate and Mirco Giacobbe and Sergey Ichtchenko and Diptarko Roy},
    title = 	 {Complete ω-Regular Supermartingale Certificates},
    booktitle =  {Proceedings of the Forty-First Annual Symposium on Logic in Computer Science (LICS 2026)},
    year =	 {2026},
    month =	 {July}, 
    pages =      {3:1--3:28},
    location =   {Lisbon, Portugal}, 
    publisher =	 {Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
    doi =        {10.4230/LIPIcs.LICS.2026.3}
  }