The Complexity of Generalized HyperLTL with Stuttering and Contexts
Abstract
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 -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 -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.
Cite
@article{arxiv.2504.08509,
title = {The Complexity of Generalized HyperLTL with Stuttering and Contexts},
author = {Gaëtan Regaud and Martin Zimmermann},
journal= {arXiv preprint arXiv:2504.08509},
year = {2025}
}