实现Omega正则超性质
Realizing Omega-regular Hyperproperties
摘要：
研究了超逻辑HyperQPTL，它结合了迹关系和$ω$ -正则性的概念.我们证明了HyperQPTL是非常有表现力的，它可以表达诸如不确定性，有界等待授权，认知属性，特别是任何$ω$ -正则属性等属性。这些属性在以前研究过的超逻辑（如HyperLTL）中无法表达。与此同时，我们认为，HyperQPTL的表现力是最佳的，在某种意义上，一个更有表现力的逻辑$ω$ -正则超属性将有一个不可判定的模型检验问题。我们进一步研究了HyperQPTL的可实现性问题。我们证明了可实现性对于包含像不确定性这样的属性的HyperQPTL片段是可判定的。但是，与可满足性问题相比，命题量化确实使超逻辑的可实现性问题更难。更具体地说，具有泛存在命题量词交替后跟单个迹量词的HyperQPTL公式片段通常是不可判定的，即使片段到HyperLTL的投影具有可判定的可实现性问题。最后，我们在原型工具BoSy中实现了HyperQPTL的有界综合问题。使用带有HyperQPTL规范的BoSy，我们已经能够合成几个资源仲裁器。非线性时间超逻辑的综合问题仍然是一个未解决的问题。例如，还不知道如何从分支时间超逻辑（如HyperCTL $^*$）中给出的规范合成系统。
英文摘要：
We studied the hyperlogic HyperQPTL, which combines the concepts of trace relations and $ω$-regularity. We showed that HyperQPTL is very expressive, it can express properties like promptness, bounded waiting for a grant, epistemic properties, and, in particular, any $ω$-regular property. Those properties are not expressible in previously studied hyperlogics like HyperLTL. At the same time, we argued that the expressiveness of HyperQPTL is optimal in a sense that a more expressive logic for $ω$-regular hyperproperties would have an undecidable model checking problem. We furthermore studied the realizability problem of HyperQPTL. We showed that realizability is decidable for HyperQPTL fragments that contain properties like promptness. But still, in contrast to the satisfiability problem, propositional quantification does make the realizability problem of hyperlogics harder. More specifically, the HyperQPTL fragment of formulas with a universal-existential propositional quantifier alternation followed by a single trace quantifier is undecidable in general, even though the projection of the fragment to HyperLTL has a decidable realizability problem. Lastly, we implemented the bounded synthesis problem for HyperQPTL in the prototype tool BoSy. Using BoSy with HyperQPTL specifications, we have been able to synthesize several resource arbiters. The synthesis problem of non-linear-time hyperlogics is still open. For example, it is not yet known how to synthesize systems from specifications given in branching-time hyperlogics like HyperCTL$^*$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
