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

翻译：我们提出了一种通用方法论，用于构造在具有一般状态空间的时间齐次马尔可夫链上，关于反应性性质的几乎必然和定量接受的可靠且完备的证明规则。反应性捕获了 $ω$-正则性质并包含线性时序逻辑。我们的核心技术结果证明了：每个反应性性质都可以分解为多个关于进入吸收区域的几乎必然终止的义务，并且在一般状态空间上始终存在合适的吸收区域。这使得每个关于几乎必然终止的完备证明规则都能扩展为反应性的证明规则，在几乎必然情形下保持完备性，并在定量情形下达到任意小 $\varepsilon$-近似的完备性。我们将这一新方法论应用于最近关于可数无限状态空间特殊情形下几乎必然终止的可靠且完备超鞅证书结果，并结合了标准定量安全性结果。由此，我们首次获得了可数无限状态空间时间齐次马尔可夫链上关于几乎必然 $ω$-正则性质的可靠且完备超鞅证书，以及关于定量 $ω$-正则性质的可靠且 $\varepsilon$-完备超鞅证书。