HyperLTL is an extension of LTL which allows quantification over traces. HyperLTL formulas are generated by the grammar: $$\phi::=\forall\pi.\phi\mid\exists\pi.\phi\mid\psi$$ $$\psi::=a_\pi\mid\neg\psi\mid\psi\lor\psi\mid X\psi\mid\psi U\psi$$ with the intuitive semantics. For example the formula \[\forall\pi.\exists\pi'.F(a_{\pi'}\land\neg a_\pi)\land G(a_\pi\Rightarrow a_{\pi'})\] expresses that for all traces there exists another trace satisfying $a$ at strictly more positions; $\{a\}^*\emptyset^\omega$ is a model of this formula. There are two main versions of the satisfiability problem for this logics: Given a formula $\phi$, one can ask if there exists any set of traces satisfying $\phi$, or if there exists a finite Kripke structure whose runs induce a set of traces satisfying $\phi$. Unfortunately, both problems are undecidable in general.
This motivates us to look for restrictions on parameters such as temporal depth, number of quantifier alternations or of universal quantifiers which would allow us to reach decidability. For the general problem, only very small fragments are decidable. However there is some hope in the other case. In particular, we do not know if it is decidable, given a HyperLTL formula $\phi$ of temporal depth one, whether $\phi$ is satisfied by the set of traces of some Kripke structure (the problem is TOWER-hard). If it is not, then which other restrictions would make it decidable?