HyperQPTL and HyperQPTL$^+$ are expressive specification languages for hyperproperties, properties that relate multiple executions of a system. Tight complexity bounds are known for HyperQPTL finite-state satisfiability and model-checking. Here, we settle the complexity of satisfiability for HyperQPTL as well as satisfiability, finite-state satisfiability, and model-checking for HyperQPTL$^+$: the former is $Σ^2_1$-complete, the latter are all equivalent to truth in third-order arithmetic, i.e., all four are very undecidable.

翻译：HyperQPTL与HyperQPTL⁺是用于表达超性质（即涉及系统多个执行轨迹间关系的性质）的强表达能力规约语言。对于HyperQPTL的有限状态可满足性与模型检测，其紧致复杂性界限已为人所知。本文中，我们确定了HyperQPTL的可满足性复杂性，以及HyperQPTL⁺的可满足性、有限状态可满足性与模型检测的复杂性：前者为Σ¹₂-完全问题，而后者均等价于三阶算术的真值判定问题，即这四类问题均具有极高的不可判定性。