Gaëtan Regaud

Gaëtan Regaud, Martin Zimmermann

We settle the complexity of satisfiability, finite-state satisfiability, and model-checking for generalized HyperLTL with stuttering and contexts, an expressive logic for the specification of asynchronous hyperproperties. Such properties cannot be specified in HyperLTL, as it is restricted to synchronous hyperproperties. Nevertheless, we prove that satisfiability is $Σ_1^1$-complete and thus not harder than for HyperLTL. On the other hand, we prove that model-checking and finite-state satisfiability are equivalent to truth in second-order arithmetic, and thus much harder than the decidable HyperLTL model-checking problem and the $Σ_0^1$-complete HyperLTL finite-state satisfiability problem. The lower bounds for the model-checking and finite-state satisfiability problems hold even when only allowing stuttering or only allowing contexts.

Gaëtan Regaud, Martin Zimmermann

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.