HyperQPTL and HyperQPTL$^+$ are expressive specification languages for hyperproperties, i.e., 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 equivalent to truth in second-order arithmetic, the latter are all equivalent to truth in third-order arithmetic, i.e., they are all four very undecidable.

翻译：HyperQPTL与HyperQPTL$^+$是用于超属性（即涉及系统多个执行轨迹之间关系的性质）的两种表达力较强的规约语言。对于HyperQPTL的有限状态可满足性与模型检测问题，其精确计算复杂度已知。本文中，我们确定了HyperQPTL的可满足性问题，以及HyperQPTL$^+$的可满足性、有限状态可满足性与模型检测问题的复杂度：前者等价于二阶算术的真值判定问题，后者三者均等价于三阶算术的真值判定问题，即这四类问题均具有极高的不可判定性。