Hyperproperties express, e.g., information-flow properties of systems, which involves the simultaneous reasoning about multiple execution traces of a system. Consequently, HyperLTL, the most important specification logic for hyperproperties, extends LTL with quantification over traces. However, HyperLTL can only express synchronous hyperproperties. Recently, several logics for asynchronous hyperproperties have been proposed. Here, we focus on AHLTL, asynchronous HyperLTL, which extends HyperLTL with quantification over trajectories that control the relative speed at which time progresses on the quantified traces. Model-checking AHLTL is known to be undecidable while satisfiability is known to be $Σ_1^1$-hard, but the precise complexity of both problems is open. Here, we close these gaps and show that model-checking is equivalent to truth in second-order arithmetic while satisfiability is $Σ_1^1$-complete if the trajectory is existentially quantified and $Σ_1^1$-hard and in $Σ_2^1$ if the trajectory is universally quantified.

翻译：超属性描述了系统的信息流属性等，这需要同时推理系统的多条执行迹。因此，作为超属性最重要的规格说明逻辑，HyperLTL通过在迹上进行量化扩展了LTL。然而，HyperLTL只能表达同步超属性。近年来，已有若干针对异步超属性的逻辑被提出。本文聚焦于AHLTL（异步HyperLTL），它通过在控制量化迹上时间进展相对速度的轨迹上进行量化，扩展了HyperLTL。已知AHLTL的模型检验是不可判定的，而可满足性是$Σ_1^1$-难的，但这两个问题的精确复杂度尚待确定。本文填补了这些空白，证明了模型检验等价于二阶算术中的真值判定，而当轨迹为存在量化时可满足性是$Σ_1^1$-完全的，当轨迹为全称量化时可满足性为$Σ_1^1$-难且属于$Σ_2^1$。