The Complexity of Generalized HyperLTL with Stuttering and Contexts
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916954860683264 |
|---|---|
| author | Regaud, Gaëtan Zimmermann, Martin |
| author_facet | Regaud, Gaëtan Zimmermann, Martin |
| contents | We settle the complexity of 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 is equivalent to truth in second-order arithmetic, and thus much harder than the decidable HyperLTL model-checking problem. The lower bounds for the model-checking problem hold even when only allowing stuttering or only allowing contexts. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_14095 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Complexity of Generalized HyperLTL with Stuttering and Contexts Regaud, Gaëtan Zimmermann, Martin Logic in Computer Science Formal Languages and Automata Theory We settle the complexity of 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 is equivalent to truth in second-order arithmetic, and thus much harder than the decidable HyperLTL model-checking problem. The lower bounds for the model-checking problem hold even when only allowing stuttering or only allowing contexts. |
| title | The Complexity of Generalized HyperLTL with Stuttering and Contexts |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2509.14095 |