面向 $\omega$-正则验证的超鞅Martingale 层次结构

我们提出了新的基于超鞅Martingale 的证书，用于验证 $\omega$-正则属性的几乎必然满足：(1)广义Streett 超鞅Martingale（GSSMs）及其 lexicographic 扩展（LexGSSMs）、(2)分布值Streett 超鞅Martingale（DVSSMs）、(3)进度测度超鞅Martingale（PMSMs）及其 lexicographic 扩展（LexPMSMs）。GSSMs、LexGSSMs 和 DVSSMs 来源于Markov链关于给定Streett条件正 recur 与 null recur 的最小固定点特征；PMSMs 和 LexPMSMs 则是Parity 进度测度的概率扩展。我们研究这些证书与现有证书（即Streett 超鞅Martingale）之间的层次关系，比较每种证书类型可验证的問題类别。值得注意的是，我们证明这些证书的严格优于Streett 超鞅Martingale。我们还证明GSSMs 对正 recur 的完备，DVSSMs 对 null recur 的完备：DVSSMs 在理论上是最强大的证书，因为对于几乎必然满足给定 $\omega$-正则属性的任意Markov链，都存在DVSSM 对其进行认证。我们提供了一个sound且相对完备的算法，用于合成LexPMSMs，这是该层次结构中第二强的证书。我们实现了一个基于该算法的原型工具，实验表明，该工具能够成功为包括那些无法被现有超鞅Martingale 认证的各种示例生成证书。