ω-正则超性质的可实现性

我们研究了超逻辑 HyperQPTL，它结合了迹关系与 $\omega$-正则性的概念。我们证明了 HyperQPTL 极具表达力，能够表达如及时性、有界等待授权、认知性质，特别是任意 $\omega$-正则性质等属性。这些性质在先前研究的如 HyperLTL 等超逻辑中无法表达。同时，我们论证了 HyperQPTL 的表达力是最优的，在某种意义上，一个更具表达力的 $\omega$-正则超性质逻辑将具有不可判定的模型检测问题。我们进一步研究了 HyperQPTL 的可实现性问题。我们证明了对于包含如及时性等性质的 HyperQPTL 片段，可实现性是可判定的。但尽管如此，与可满足性问题相反，命题量化确实使超逻辑的可实现性问题变得更难。更具体地说，具有全称-存在命题量词交替后接单个迹量词的 HyperQPTL 公式片段在一般情形下是不可判定的，尽管该片段投影到 HyperLTL 具有可判定的可实现性问题。最后，我们在原型工具 BoSy 中实现了 HyperQPTL 的有界综合问题。使用 BoSy 与 HyperQPTL 规约，我们已能够综合出多个资源仲裁器。非线性时间超逻辑的综合问题仍然开放。例如，尚不知如何从分支时间超逻辑（如 HyperCTL$^*$）给出的规约综合系统。