The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas

TL;DR

This paper explores the boundaries of decidability in HyperLTL satisfiability by examining small model sizes and simple formulas, providing new decidability results and complexity bounds.

Contribution

It identifies decidability conditions for HyperLTL satisfiability based on model size restrictions and formula simplicity, extending understanding of its computational limits.

Findings

Decidability achieved for models of bounded size

Decidability for formulas with nesting depth one

Tight complexity bounds established for various cases

Abstract

HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information flow policies by relating multiple traces of a security-critical system. HyperLTL has been successfully applied to express fundamental security policies like noninterference and observational determinism, but has also found applications beyond security, e.g., distributed protocols and coding theory. However, HyperLTL satisfiability is undecidable as soon as there are existential quantifiers in the scope of a universal one. To overcome this severe limitation to applicability, we investigate here restricted variants of the satisfiability problem to pinpoint the decidability border. First, we restrict the space of admissible models and show decidability when restricting the search space to models of bounded size or to finitely representable ones. Second, we consider formulas with restricted nesting of temporal operators and show that nesting depth one yields decidability for a slightly larger class of quantifier prefixes. We provide tight complexity bounds in almost all cases.

Tables

Table 1. Table 1: Complexity of HyperLTL satisfiability in terms of quantifier prefixes and temporal depth. An asterisk  ∗ superscript ∗ \mbox{}^{\ast} denotes that the upper bound only holds for until-free formulas. All lower bounds in the second column already hold for temporal depth two.

	temporal depth one	arbitrary temporal depth
${\exists }^{\ast }$ / ${\forall }^{\ast }$	NP-complete ([7]+[8])	PSpace-complete ([8]+[26])
${\exists }^{\ast }{\forall }^{\ast }$	NExpTime-complete (Thm. 4.4)	ExpSpace-complete ([8])
${\exists }^{\ast }\forall {\exists }^{\ast }$	in N2ExpTime∗ (Thm. 4.3)	undecidable ([8])
${\forall }^2{\exists }^{\ast }$	undecidable (Thm. 4.2)	undecidable

Equations

$$\forall \pi .\forall {\pi }^{\prime }.\left(\mathbf{G}{\bigwedge }_{i\in I\setminus \{h\}}(i_{\pi }\iff i_{{\pi }^{\prime }})\right)\Rightarrow \mathbf{G}(o_{\pi }\iff o_{{\pi }^{\prime }}).$$

$$\phi$$

$$\psi$$

$$\phi$$

$$\psi$$

$${\psi }^{\prime }$$

$${\#}_j(u_m)=\#(u_m)(0)\cdots \#(u_m)(j-1)\overline{\#(u_m)(j)}\#(u_m)(j+1)\cdots \#(u_m)(\ell -1)$$

$$T_1=\{\#(u_{s(r)})\#(u_{s(r)}^{\prime })b_r{\$}^{\omega }\mid 0\le r<|s|\}$$

$$T_2=\{t_i\mid 0\le i<|h(s)|=|h^{\prime }(s)|\}$$

$$t_i=({\#}_j(u_{s(r)}))({\#}_{j^{\prime }}(u_{s(r^{\prime })}^{\prime }))[b_r,b_{r^{\prime }}]{\$}^{\omega }$$

$$\sum _{r_0<r}|h(s(r_0))|+j=i$$

$$\sum _{r_0<r^{\prime }}|h^{\prime }(s(r_0))|+j^{\prime }=i.$$

$$e::=a\mid b\mid \epsilon \mid \varnothing \mid e+e\mid ee\mid \neg e$$

$$T(\mathcal{K})=l^{\omega }+l^{\ast }(a+b{)}^{\omega }+l^{\ast }(a+b{)}^{\ast }{r}^{\omega }+l^{\ast }\#r^{\omega }.$$

$$\psi =\mathbf{F}{r}_{{\pi }_1}\wedge \mathbf{F}{r}_{{\pi }_2}\wedge \mathbf{G}(\neg {\#}_{{\pi }_1}\wedge \neg {\#}_{{\pi }_2})\wedge {\psi }_{e_1,{\pi }_1}\wedge {\psi }_{e_2,{\pi }_2}$$

$${\psi }^{\prime }=\mathbf{G}(l_{{\pi }_2}\iff \neg r_{{\pi }_1})\wedge \mathbf{G}(a_{\pi }\iff (a_{{\pi }_1}\vee a_{{\pi }_2})\wedge b_{\pi }\iff (b_{{\pi }_1}\vee b_{{\pi }_2}))$$

$${\phi }^{\prime }=Q_1{\pi }_1\dots Q_n{\pi }_n.\exists \tau .m_{\tau }^{\psi }\wedge \underset{{\psi }^{\prime }⊑\psi }{\bigwedge }\overline{{\psi }^{\prime }}.$$

$$(T^{\prime },{\Pi }^{\prime })\models \exists \tau .m_{\tau }^{\psi }\wedge \underset{{\psi }^{\prime }⊑\psi }{\bigwedge }\overline{{\psi }^{\prime }}$$

$$(T^{\prime },{\Pi }^{\prime })\models Q_{n-i}{\pi }_{n-i}\dots Q_n{\pi }_n.\exists \tau .m_{\tau }^{\psi }\wedge \underset{{\psi }^{\prime }⊑\psi }{\bigwedge }\overline{{\psi }^{\prime }}$$

$$\forall {\pi }_1\dots \forall {\pi }_n.\exists {\pi }_{n+1}{Q}_1{\tau }_1\dots Q_p{\tau }_p.\psi$$

$$\varphi_{1}=\forall\pi_{1}\ldots\forall\pi_{n}.\exists\pi_{n+1}.{\mathbf{F\,}}\big{(}\bigwedge_{i=1}^{n+1}m^{i}_{\pi_{i}}\big{)},$$

$$\varphi_{2}=\forall\pi_{1}\ldots\forall\pi_{n}.\forall\pi_{n+1}.Q_{1}\tau_{1}\ldots Q_{p}\tau_{p}.{\mathbf{F\,}}\big{(}\bigwedge_{i=1}^{n+1}m^{i}_{\pi_{i}}\big{)}\Rightarrow\psi,$$

$$\forall\pi^{\prime}_{1}\ldots\forall\pi^{\prime}_{n}.\forall\pi_{1}\ldots\forall\pi_{n}.\forall\pi_{n+1}.Q_{1}\tau_{1}\ldots Q_{p}\tau_{p}.\exists\pi^{\prime}_{n+1}.{\mathbf{F\,}}\big{(}\bigwedge_{i=1}^{n+1}m^{i}_{\pi^{\prime}_{i}}\big{)}\land\big{[}{\mathbf{F\,}}\big{(}\bigwedge_{i=1}^{n+1}m^{i}_{\pi_{i}}\big{)}\Rightarrow\psi\big{]}.$$

$${\phi }^{\prime }=\forall \pi .\forall {\pi }^{\prime }.\exists {\pi }_{n+1}\dots \exists {\pi }_{n+n^{\prime }}.\exists {\tau }_{(1,1)}\exists {\tau }_{(1,2)}\dots \exists {\tau }_{(n-1,n)}\exists {\tau }_{(n,n)}.{\psi }_1\wedge {\psi }_2$$

$$\psi_{1}=\bigwedge_{i_{1}=1}^{n}\bigwedge_{i_{2}=1}^{n}\bigwedge_{a\in\mathrm{AP}}{\mathbf{G\,}}\Big{[}\big{(}(a,i_{1})_{\tau_{(i_{1},i_{2})}}\Leftrightarrow(a,i_{2})_{\pi^{\prime}}\big{)}\land\bigwedge_{j\neq i_{1}}\big{(}(a,j)_{\tau_{(i_{1},i_{2})}}\Leftrightarrow(a,j)_{\pi}\big{)}\Big{]}$$

$${\phi }^{\prime }=\exists {\tau }_0.\exists {\tau }_1\dots \exists {\tau }_n.\forall \pi .\exists {\tau }_{n+1}\dots \exists {\tau }_{n+n^{\prime }}.{\psi }^{\prime }$$

$$\psi^{\prime}=\bigwedge_{k=0}^{d}\Big{(}{\mathbf{F\,}}m^{k}_{\tau_{0}}\Big{)}\land\Big{(}{\mathbf{F\,}}\big{(}\bigvee_{a\in\mathrm{AP}\cup\{m^{0},\ldots,m^{d}\}}a_{\pi}\oplus a_{\tau_{0}}\big{)}\Rightarrow\psi^{\prime\prime}\Big{)}$$

$$\exists {\tau }_1\dots \exists {\tau }_m.\forall \pi .\exists {\tau }_{n+1}\dots \exists {\tau }_{n+n^{\prime }}.{\psi }^{\prime }.$$

$$\begin{gathered} \exists \pi .\exists {\pi }_0.\exists {\pi }_1.\forall {\tau }_1\dots \forall {\tau }_n.\forall {\tau }_1^{\prime }\dots \forall {\tau }_n^{\prime }.\forall {\sigma }_1\dots \forall {\sigma }_n.\forall {\sigma }_1^{\prime }\dots {\sigma }_n^{\prime }. \\ {\psi }_{0/1}\wedge [{\psi }_{assign}\Rightarrow ({\psi }_{halt}\wedge {\psi }_{init}\wedge {\psi }_{cons}\wedge {\psi }_{complete}\wedge \underset{(q,q^{\prime },a,d)\in \Delta }{\bigvee }{\psi }_{trans}(q,q^{\prime },a,a^{\prime },d))]. \end{gathered}$$

$$\mathrm{AP}=\Sigma \cup Q\cup \{{\mathrm{rk}}_0,\dots ,{\mathrm{rk}}_n\}\cup \{h,0,1,2,in,ni,m_t,m_s,lt,gt\}$$

$${\psi }_{in}(\pi ,{\pi }^{\prime })=1_{\pi }\wedge 1_{{\pi }^{\prime }}\wedge \mathbf{F}({ni}_{{\pi }^{\prime }}\wedge {in}_{\pi })\wedge \underset{r=0}{\overset{n-1}{\bigvee }}({\mathrm{rk}}_r{)}_{{\pi }^{\prime }}\wedge ({\mathrm{rk}}_{r+1}{)}_{\pi }.$$

$$\forall \pi .\forall {\pi }^{\prime }.(1_{\pi }\wedge 1_{{\pi }^{\prime }})\Rightarrow [\mathbf{F}(l{t}_{\pi }\wedge g{t}_{{\pi }^{\prime }})\iff {\psi }_{0,1}\vee ({\psi }_{equalrank}\wedge {\psi }_{order})],$$

Full text

First, we restrict the space of admissible models and show decidability when restricting the search space to models of bounded size or to finitely representable ones. Second, we consider formulas with restricted nesting of temporal operators and show that nesting depth one yields decidability for a slightly larger class of quantifier prefixes. We provide tight complexity bounds in almost all cases.

1 Introduction

The introduction of temporal logics for the specification of information flow policies [3] was a significant milestone in the long and successful history of applying logics in computer science [16]. Probably the most important representative of these logics is HyperLTL [3], which extends Linear Temporal Logic (LTL) [24] by trace quantifiers. This addition allows to express properties that relate multiple execution traces, which is typically necessary to capture the flow of information [4]. In contrast, LTL, currently the most influential specification language for reactive systems, is only able to express properties of single traces.

HyperLTL provides a uniform framework for expressing information flow policies in a formalism with intuitive syntax and semantics, and for the automated verification of these policies: A wide range of policies from the literature [15, 20, 21, 22, 23, 28] with specialized verification algorithms is expressible in HyperLTL, i.e., universal HyperLTL verification algorithms are applicable to all of them.

As an example, consider a system with a set $I$ of inputs, which contains a hidden input $h\in I$, and an output $o$. Now, noninterference [15] between $h$ and $o$ requires that no information about $h$ is leaked via $o$, i.e., for all execution traces $\pi$ and $\pi^{\prime}$, if the inputs in $\pi$ and $\pi^{\prime}$ only differ in $h$, then they have the same output at all times. Formally, this is captured by the HyperLTL formula

[TABLE]

Today, there are tools for model checking HyperLTL properties [6, 13], for checking satisfiability of HyperLTL properties [9, 11], for synthesizing reactive systems from HyperLTL properties [10], and for runtime monitoring of HyperLTL properties [1, 2, 12]. Furthermore, the extraordinary expressiveness of HyperLTL has been exhibited [14] and connections to first and second-order predicate logics have been established [5, 14].

The major drawback of HyperLTL is the usual price one has to pay for great expressiveness: prohibitively high worst-case complexity. In particular, model checking finite Kripke structures against HyperLTL formulas is nonelementary [3] and satisfiability is even undecidable [8]. These results have to be contrasted with model checking and satisfiability being PSpace-complete for LTL [26], problems routinely solved in real-life applications [19].

Due to the sobering state of affairs, it is imperative to find fragments of the logic with (more) tractable complexity. In this work, we focus on the satisfiability problem, the most fundamental decision problem for a logic. Nevertheless, it has many applications in verification, e.g., checking the equivalence and implication of specifications can be reduced to satisfiability. Finally, the question whether a property given by some HyperLTL formula is realizable by some system is also a satisfiability problem.

A classical attempt to overcome the undecidability of the satisfiability problem is to restrict the number of quantifier alternations of the formulas under consideration. In fact, the alternation depth is the measure underlying the nonelementary complexity of the HyperLTL model checking problem [3]. However, the situation is different for the satisfiability problem: It is undecidable even when restricted to $\forall\exists^{*}$ formulas, i.e., formulas starting with one universal quantifier followed by existential ones [8]. All remaining prefix classes are decidable by reductions to the LTL satisfiability problem, e.g., the satisfiability problem is PSpace-complete for the alternation-free prefix classes $\exists^{*}$ and $\forall^{*}$ and ExpSpace-complete for the class $\exists^{*}\forall^{*}$ [8].

However, there are more complexity measures beyond the alternation depth that can be restricted in order to obtain tractable satisfiability problems, both on formulas and on models. The latter case is of particular interest, since it is known that not every satisfiable HyperLTL has a “simple” model, for various formalizations of “simple” [14]. Thus, for those formulas, such a restriction could make a significant difference. Furthermore, from a more practical point of view, one is often interested in whether there is a, say, finite model while the existence of an intricate infinite model may not be useful.

We study the satisfiability problem for formulas with restricted quantifier prefixes and restricted temporal depth [7], which measures the nesting of temporal operators. Our main result here shows that satisfiability is even undecidable for formulas of the form $\forall^{2}\exists^{*}\varphi$, where $\varphi$ has temporal depth one and only uses eventually ${\mathbf{F\,}}$ and always ${\mathbf{G\,}}$, i.e., it is a Boolean combination of formulas ${\mathbf{F\,}}\varphi^{\prime}$ with propositional $\varphi^{\prime}$. Thereby, we strengthen the previous undecidability result for $\forall\exists^{*}$ by bounding the temporal depth to one, but at the price of a second universal quantifier. Moreover, we clarify the border between decidability and undecidability at temporal depth two: Using only one universally quantified variable, temporal depth one, and only ${\mathbf{F\,}}$, ${\mathbf{G\,}}$, and nested applications of next ${\mathbf{X\,}}$ leads to decidability. Finally, we show that every HyperLTL formula can be transformed into an equisatisfiable $\forall^{2}\exists^{*}$ formula of temporal depth two, i.e., this fragment already captures the full complexity of the satisfiability problem.

Thus, the overall picture is still rather bleak: if one only restricts the formula then the islands of decidability are very small. Phrased differently, even very simple formulas are extremely expressive and allow to encode computations of Turing-complete devices in their models. However, note that such models are necessarily complex, as they need to be able to encode an unbounded amount of information.

Thus, we also consider satisfiability problems for arbitrary formulas, but with respect to restricted models which do not allow to encode such computations. In particular, we consider three variants of increasing complexity: Checking whether a given HyperLTL formula has a model of a given cardinality $k$ is ExpSpace-complete, whether it has a model containing only ultimately periodic traces of length at most $k$ is N2ExpTime-complete, and checking whether it has a model induced by a Kripke structure with $k$ states is Tower-complete. The last result is even true for a fixed Kripke structure, which therefore has implications for the complexity of the model checking problem as well. Thus, the situation is more encouraging when checking for the existence of small models: satisfiability becomes decidable, even with (relatively) moderate complexity in the first two cases.

However, as argued above, all three approaches are (necessarily) incomplete: There are satisfiable formulas that have only infinite models, satisfiable formulas that have only non-ultimately periodic models, and satisfiable formulas that have no $\omega$-regular models [14], a class of models that includes all those that are induced by a finite Kripke structure.

All in all, our work shows that HyperLTL satisfiability remains a challenging problem, but we have provided a complete classification of the tractable cases in terms of alternation depth, temporal depth, and representation of the model (for formulas without until).

All proofs omitted due to space restrictions can be found in the appendix.

2 Definitions

Fix a finite set $\mathrm{AP}$ of atomic propositions. A valuation is a subset of $\mathrm{AP}$. A trace over $\mathrm{AP}$ is a map $t\colon\mathbb{N}\rightarrow 2^{\mathrm{AP}}$, denoted by $t(0)t(1)t(2)\cdots$, i.e., an infinite sequence of valuations. The set of all traces over $\mathrm{AP}$ is denoted by $(2^{\mathrm{AP}})^{\omega}$. The projection of $t$ to $\mathrm{AP}^{\prime}$ is the trace $(t(0)\cap\mathrm{AP}^{\prime})(t(1)\cap\mathrm{AP}^{\prime})(t(2)\cap\mathrm{AP}^{\prime})\cdots$ over $\mathrm{AP}^{\prime}$. A trace $t$ is ultimately periodic, if $t=x\cdot y^{\omega}$ for some $x,y\in(2^{\mathrm{AP}})^{+}$, i.e., there are $s,p>0$ with $t(n)=t(n+p)$ for all $n\geq s$.

The formulas of HyperLTL are given by the grammar

[TABLE]

where $a$ ranges over atomic propositions in $\mathrm{AP}$ and where $\pi$ ranges over a fixed countable set $\mathcal{V}$ of trace variables. Conjunction, implication, equivalence, and exclusive disjunction $\oplus$, as well as the temporal operators eventually ${\mathbf{F\,}}$ and always ${\mathbf{G\,}}$ are derived as usual. A sentence is a closed formula, i.e., a formula without free trace variables. The size of a formula $\varphi$, denoted by $|\varphi|$, is its number of distinct subformulas.

The semantics of HyperLTL is defined with respect to a trace assignment, a partial mapping $\Pi\colon\mathcal{V}\rightarrow(2^{\mathrm{AP}})^{\omega}$. The assignment with empty domain is denoted by $\Pi_{\emptyset}$. Given a trace assignment $\Pi$, a trace variable $\pi$, and a trace $t$ we denote by $\Pi[\pi\rightarrow t]$ the assignment that coincides with $\Pi$ everywhere but at $\pi$, which is mapped to $t$. We also use shorthand notation like $[\pi_{1}\rightarrow t_{1},\ldots,\pi_{n}\rightarrow t_{n}]$ and $[(\pi_{i}\rightarrow t_{i})_{1\leq i\leq n}]$ for $\Pi_{\emptyset}[\pi_{1}\rightarrow t_{1}]\ldots[\pi_{n}\rightarrow t_{n}]$, if the $\pi_{i}$ are pairwise different. Furthermore, $\Pi[j,\infty)$ denotes the trace assignment mapping every $\pi$ in $\Pi$’s domain to $\Pi(\pi)(j)\Pi(\pi)(j+1)\Pi(\pi)(j+2)\cdots$.

For sets $T$ of traces and trace assignments $\Pi$ we define

• •

$(T,\Pi)\models a_{\pi}$, if $a\in\Pi(\pi)(0)$,

• •

$(T,\Pi)\models\neg\psi$, if $(T,\Pi)\not\models\psi$,

• •

$(T,\Pi)\models\psi_{1}\vee\psi_{2}$, if $(T,\Pi)\models\psi_{1}$ or $(T,\Pi)\models\psi_{2}$,

• •

$(T,\Pi)\models{\mathbf{X\,}}\psi$, if $(T,\Pi[1,\infty))\models\psi$,

• •

$(T,\Pi)\models\psi_{1}{\mathbf{\,U\,}}\psi_{2}$, if there is a $j\geq 0$ such that $(T,\Pi[j,\infty))\models\psi_{2}$ and for all $0\leq j^{\prime}<j$: $(T,\Pi[j^{\prime},\infty))\models\psi_{1}$,

• •

$(T,\Pi)\models\exists\pi.\varphi$, if there is a trace $t\in T$ such that $(T,\Pi[\pi\rightarrow t])\models\varphi$, and

• •

$(T,\Pi)\models\forall\pi.\varphi$, if for all traces $t\in T$: $(T,\Pi[\pi\rightarrow t])\models\varphi$.

We say that $T$ satisfies a sentence $\varphi$ if $(T,\Pi_{\emptyset})\models\varphi$. In this case, we write $T\models\varphi$ and say that $T$ is a model of $\varphi$. Conversely, satisfaction of quantifier-free formulas does not depend on $T$. Hence, we say that $\Pi$ satisfies a quantifier-free $\psi$ if $(\emptyset,\Pi)\models\psi$ and write $\Pi\models\psi$ (assuming $\Pi$ is defined on all trace variables that appear in $\psi$).

The alternation depth of a HyperLTL formula $\varphi$, denoted by $\mathrm{ad}(\varphi)$, is defined as its number of quantifier alternations. Its temporal depth, denoted by $\mathrm{td}(\varphi)$, is defined as the maximal depth of the nesting of temporal operators in the formula. Formally, $\mathrm{td}$ and $\mathrm{ad}$ are defined as follows :

• •

$\mathrm{td}(a_{\pi})=0$

• •

$\mathrm{td}(\neg\psi)=\mathrm{td}(\psi)$

• •

$\mathrm{td}(\psi_{1}\vee\psi_{2})=\max(\mathrm{td}(\psi_{1}),\mathrm{td}(\psi_{2}))$,

• •

$\mathrm{td}({\mathbf{X\,}}\psi)=1+\mathrm{td}(\psi)$,

• •

$\mathrm{td}(\psi_{1}{\mathbf{\,U\,}}\psi_{2})=1+\max(\mathrm{td}(\psi_{1}),\mathrm{td}(\psi_{2}))$,

• •

$\mathrm{td}(\exists\pi.\varphi)=\mathrm{td}(\varphi)$

• •

$\mathrm{td}(\forall\pi.\varphi)=\mathrm{td}(\varphi)$.

• •

$\mathrm{ad}(\exists\pi_{1}\ldots\exists\pi_{n}.\varphi)=0$ for quantifier-free $\varphi$

• •

$\mathrm{ad}(\forall\pi_{1}\ldots\forall\pi_{n}.\varphi)=0$ for quantifier-free $\varphi$

• •

$\mathrm{ad}(\exists\pi_{1}\ldots\exists\pi_{n}.\forall\tau.\varphi)=1+\mathrm{ad}(\forall\tau.\varphi)$

• •

$\mathrm{ad}(\forall\pi_{1}\ldots\forall\pi_{n}.\exists\tau.\varphi)=1+\mathrm{ad}(\exists\tau.\varphi)$

Although HyperLTL sentences are required to be in prenex normal form, they are closed under Boolean combinations, which can easily be seen by transforming such formulas into prenex normal form. Note that this transformation can be implemented such that it changes neither the temporal nor alternation depth, and can be performed in polynomial time.

The fragment HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$ contains formulas of temporal depth one using only ${\mathbf{F\,}}$ and ${\mathbf{G\,}}$ as temporal operators, and HyperLTL${}^{1}(\mathbf{F},\mathbf{G},\mathbf{X}^{*})$ contains formulas using only ${\mathbf{F\,}}$, ${\mathbf{G\,}}$, and ${\mathbf{X\,}}$ as temporal operators and of temporal depth one, however we allow iterations of the ${\mathbf{X\,}}$ operator. Formally, HyperLTL${}^{1}(\mathbf{F},\mathbf{G},\mathbf{X}^{*})$ formulas are generated by the grammar

[TABLE]

where $n$ ranges over the natural numbers. The grammar for HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$ is obtained by removing ${\mathbf{X\,}}^{n}\psi^{\prime}$ from the grammar above.

Also, we use standard notation for classes of formulas with restricted quantifier prefixes, e.g., $\forall^{2}\exists^{*}$ denotes the set of HyperLTL formulas in prenex normal form with two universal quantifiers followed by an arbitrary number of existential quantifiers, but no other quantifiers.

Finally, we encounter various complexity classes, classical ones from NP to N2ExpTime, as well as Tower (see, e.g., [25]). Intuitively, Tower is the set of problems that can be solved by a Turing machine that, on an input of size $n$, stops in time 2^{2^{\rotatebox[origin={l}]{29.0}{\scriptscriptstyle\ldots\mathstrut}^{2}}}, with the height of the tower of exponents bounded by $b(n)$, where $b$ is a fixed elementary function. The reductions presented in this work are polynomial time reductions unless otherwise stated.

3 Satisfiability for Restricted Classes of Models

As the satisfiability problem “Given a HyperLTL sentence $\varphi$, does $\varphi$ have a nonempty model?” is undecidable, even when restricted to finite models [8]. Hence, one has to consider simpler problems to regain decidability. In this section, we simplify the problem by checking only for the existence of simple models, for the following three formalizations of simplicity, where the bound $k$ is always part of the input:

• •

Models of cardinality at most $k$ (Theorem 3.1).

• •

Models containing only ultimately periodic traces $xy^{\omega}$ with $|x|+|y|\leq k$ (Theorem 3.2).

• •

Models induced by a finite-state system with at most $k$ states (Theorem 3.3).

In every case, we allow arbitrary HyperLTL formulas as input and encode $k$ in binary.

With the following result, we determine the complexity of checking satisfiability with respect to models of bounded size. The algorithm uses a technique introduced by Finkbeiner and Hahn [8, Theorem 3] that allows us to replace existential and universal quantification by disjunctions and conjunctions, if the model is finite. Similarly, the lower bound also follows from Finkbeiner and Hahn.

Theorem 3.1

The following problem is ExpSpace-complete: Given a HyperLTL sentence $\varphi$ and $k\in\mathbb{N}$ (in binary), does $\varphi$ have a model with at most $k$ traces?

Proof

For the ExpSpace upper bound, one can check, given $\varphi$ and $k$, satisfiability of the sentence $\exists\pi_{1}\ldots\exists\pi_{k}.\overline{\varphi}$ where $\overline{\varphi}$ is defined inductively as follows:

• •

$\overline{\varphi}=\varphi$ if $\varphi$ is quantifier-free.

• •

$\overline{\forall\pi.\varphi}=\bigwedge_{i=1}^{k}\overline{\varphi}[\pi\leftarrow\pi_{i}]$.

• •

$\overline{\exists\pi.\varphi}=\bigvee_{i=1}^{k}\overline{\varphi}[\pi\leftarrow\pi_{i}]$.

Here, $\overline{\varphi}[\pi\leftarrow\pi_{i}]$ is obtained from $\overline{\varphi}$ by replacing every occurrence of $\pi$ by $\pi_{i}$. This sentence states the existence of at most $k$ traces satisfying $\varphi$ by replacing every quantifier by an explicit conjunction or disjunction over the possible assignments.

The resulting sentence is of size at most $|\varphi|k^{|\varphi|}+k$, which is exponential in the size of the input and its satisfiability can be checked in polynomial space in the size of the resulting formula [8]. As a result, the problem is in ExpSpace as well.

Finkbeiner and Hahn showed that satisfiability is ExpSpace-complete for sentences of the form $\exists^{*}\forall^{*}$ [8]. This implies ExpSpace-hardness of our problem, as if such a sentence, say with $k$ existential quantifiers, is satisfiable then it has a model with at most $k$ traces. ∎

As the algorithm proceeds by a reduction to the satisfiability problem for $\exists^{*}$ formulas, which in turn is reduced to LTL satisfiability, one can show that a HyperLTL sentence $\varphi$ has a model with $k$ traces if and only if it has a model with $k$ ultimately periodic traces.

Next, we consider another variant of the satisfiability problem, where we directly restrict the space of possible models to ultimately periodic ones of the form $xy^{\omega}$ with $|x|+|y|\leq k$. As we encode $k$ in binary, the length of those traces is exponential in the input and the cardinality of the model is bounded doubly-exponentially. This explains the increase in complexity in the following theorem in comparison to Theorem 3.1.

Theorem 3.2

The following problem is N2ExpTime-complete: Given a HyperLTL sentence $\varphi$ and $k\in\mathbb{N}$ (in binary), does $\varphi$ have a model whose elements are of the form $xy^{\omega}$ with $|x|+|y|\leq k$?

Proof

For the upper bound, given a HyperLTL sentence $\varphi$ and $k\in\mathbb{N}$ in binary we start by guessing a model $T\subseteq\{xy^{\omega}\mid|x|+|y|\leq k\}$. Let $n=\lceil\log_{2}(k)\rceil+|\varphi|$ be the size of the input. We have $|T|\leq(2^{|\mathrm{AP}|}+1)^{k+1}\leq(2^{n}+1)^{2^{n}+1}$ (as we can assume all atomic propositions appear in the formula, $|\mathrm{AP}|\leq|\varphi|\leq n$), i.e., $|T|$ is doubly-exponential in $n$.

Then, we apply to $\varphi$ a similar transformation as the one used in the proof of Theorem 3.1, i.e., we create a variable $\pi_{u,v}$ for each trace $uv^{\omega}\in T$, and we replace in the sentence every universal (existential) quantifier by a conjunction (disjunction) over every possible trace assignment of the quantified variable over $T$. Formally, we define $\overline{\varphi}$ as follows:

• •

$\overline{\varphi}=\varphi$ if $\varphi$ is quantifier-free

• •

$\overline{\forall\pi.\varphi}=\bigwedge_{uv^{\omega}\in T}\overline{\varphi}[\pi\leftarrow\pi_{u,v}]$

• •

$\overline{\exists\pi.\varphi}=\bigvee_{uv^{\omega}\in T}\overline{\varphi}[\pi\leftarrow\pi_{u,v}]$

The size of the formula is multiplied by $|T|$ at each new quantifier. In the end, the size of $\overline{\varphi}$ is at most $|T|^{|\varphi|}|\varphi|\leq n((2^{n}+1)^{2^{n}+1})^{n}=2^{2^{O(n)}}$. Define $\Pi_{T}=[(\pi_{u,v}\rightarrow uv^{\omega})_{uv^{\omega}\in T}]$.

Observe that as $T\subseteq\{xy^{\omega}\mid|x|+|y|\leq k\}$, for all $j>k$, $w(j+k!)=w(j)$ for every $w\in T$. Thus, every quantifier-free formula evaluated over $\Pi_{T}$ is satisfied at some index if and only if it is satisfied at some index less than $k!+k$. Therefore, one can evaluate $\overline{\varphi}$ over $\Pi_{T}$ by recursively computing for each subformula the set of indices $0\leq j<k+k!$ such that this subformula is satisfied by $\Pi_{T}[j,\infty)$. This procedure is polynomial in the size of $\overline{\varphi}$, $T$ and $k!$, all three being doubly-exponential in $n$, i.e., it is doubly-exponential in the size of the input.

To prove the lower bound, we reduce from the following bounded variant of Post’s correspondence problem (PCP): Given two lists $u_{1},\ldots,u_{n}$ and $u_{1}^{\prime},\ldots,u_{n}^{\prime}$ of words, does there exist a word $s\in\{1,\ldots,n\}^{+}$ with $|s|\leq 2^{2^{n}}$ and $h(s)=h^{\prime}(s)$? Here $h$ is the homomorphism induced by $m\mapsto u_{m}$ for every $m$ and $h^{\prime}$ is defined analogously. We refer to such a word $s$ as a solution. This variant is N2ExpTime-hard, which can be shown by adapting the proof of undecidability of PCP as presented by Hopcroft and Ullman [18]. The same construction allows to reduce from the problem of deciding, given a nondeterministic Turing machine $\mathcal{M}$ and a word $w$, if $\mathcal{M}$ halts on $w$ in at most $2^{2^{|w|}}$ steps.

Now, given an instance $u_{1},\ldots,u_{n},u_{1}^{\prime},\ldots,u_{n}^{\prime}$ of this problem over an alphabet $\Sigma$, we construct a sentence $\varphi$ and a $k\in\mathbb{N}$ in polynomial time in $\sum_{m}|u_{m}|+|u_{m}^{\prime}|$ such that $\varphi$ has a model $T\subseteq\{xy^{\omega}\mid|x|+|y|\leq k\}$ if and only if the instance has a solution.

Let $\ell$ be the maximal length of a word of the instance. For all $1\leq m\leq n$, let $\#(u_{m})=u_{m}\#^{\ell-|u_{m}|}$ and $\#(u_{m}^{\prime})=u_{m}^{\prime}\#^{l-|u_{m}^{\prime}|}$, i.e., $|\#(u_{m})|=|\#(u_{m}^{\prime})|=\ell$ for all $m$. For every $a\in\Sigma$, let $\overline{a}$ be a fresh letter and let $\overline{\Sigma}=\{\overline{a}\mid a\in\Sigma\}$. For all $1\leq m\leq n$ and $0\leq j<|u_{m}|$ let

[TABLE]

be the word $\#(u_{m})$ where the letter at position $j$ is replaced by its associated letter in $\overline{\Sigma}$. Analogously, we define $\#_{j}(u_{m}^{\prime})$.

Further, for all $r\in\mathbb{N}$, let $b_{r}\in\{0,1\}^{*}$ be the binary representation of $r$, with the least significant bit at the beginning and without trailing zeros. Finally, for all $b_{r},b_{r^{\prime}}$ let $[b_{r},b_{r^{\prime}}]$ be the unique word over $\{0,1\}^{2}$ such that $[b_{r},b_{r^{\prime}}](i)=(b_{r}(i),b_{r^{\prime}}(i))$ for all $i$. If $b_{r}$ and $b_{r^{\prime}}$ are not of the same length, then we pad the shorter one with [math]’s at the end.

In the following, we work with the set \mathrm{AP}=\Sigma\cup\overline{\Sigma}\cup\{\#,\,0,1}\cup{0,1}^{2}$of atomic propositions. In the construction, we ensure that on every trace of the model exactly one proposition is satisfied at any moment in time. Thus, we treat traces as words over$\mathrm{AP}$without making a distinction between a proposition$a$and the singleton${a}$.

We define two types of traces:

• •

Traces of type one are of the form \#(u_{m})\#(u^{\prime}_{m})b_{r}\^{\omega}$for some$1\leq m\leq n$and some$r\in\mathbb{N}$, which is called the rank of the trace.

• •

Traces of type two are of the form (\#_{j}(u_{m}))(\#_{j^{\prime}}(u_{m^{\prime}}^{\prime}))[b_{r},b_{r^{\prime}}]\^{\omega}$with$1\leq m,m^{\prime}\leq n$,$0\leq j<|u_{m}|$,$0\leq j^{\prime}<|u_{m^{\prime}}^{\prime}|$and$r,r^{\prime}\in\mathbb{N}$. Note that we allow$m\neq m^{\prime}$.

A trace t_{1}=\#(u_{m_{1}})\#(u^{\prime}_{m_{1}})b_{r_{1}}\^{\omega}$of type one and a trace$t_{2}=(#{j}(u{m_{2}}))(#{j^{\prime}}(u{m^{\prime}{2}}^{\prime}))[b{r_{2}},b_{r^{\prime}{2}}]$^{\omega}$of type two are *$u$-compatible* if$u{m_{1}}=u_{m_{2}}$and$r_{1}=r_{2}$and *$u^{\prime}$-compatible* if$u^{\prime}{m{1}}=u^{\prime}{m^{\prime}{2}}$and$r_{1}=r^{\prime}_{2}$.

Fix a trace t_{0}=(\#_{j}(u_{m}))(\#_{j^{\prime}}(u_{m^{\prime}}^{\prime}))[b_{r},b_{r^{\prime}}]\^{\omega}$of type two. It is *final* if$j=|u_{m}|-1$,$j^{\prime}=|u_{m^{\prime}}^{\prime}|-1$and$b_{r}=b_{r^{\prime}}$. If it is not final, then a trace$t_{1}$of type two is a *successor* of$t_{0}$, if one of the following holds:

• •

$j<|u_{m}|-1$ and $j^{\prime}<|u_{m^{\prime}}^{\prime}|-1$ and t_{1}=(\#_{j+1}(u_{m}))(\#_{j^{\prime}+1}(u_{m^{\prime}}^{\prime}))[b_{r},b_{r^{\prime}}]\^{\omega}$.

• •

$j=|u_{m}|-1$ and $j^{\prime}<|u_{m^{\prime}}^{\prime}|-1$ and t_{1}=(\#_{0}(u_{m^{*}}))(\#_{j^{\prime}+1}(u_{m^{\prime}}^{\prime}))[b_{r+1},b_{r^{\prime}}]\^{\omega}$for some$1\leq m^{*}\leq n$.

• •

$j<|u_{m}|-1$ and $j^{\prime}=|u_{m^{\prime}}^{\prime}|-1$ and t_{1}=(\#_{j+1}(u_{m}))(\#_{0}(u_{m^{*}}^{\prime}))[b_{r},b_{r^{\prime}+1}]\^{\omega}$for some$1\leq m^{*}\leq n$.

• •

$j=|u_{m}|-1$ and $j^{\prime}=|u_{m^{\prime}}^{\prime}|-1$ (which implies $r\neq r^{\prime}$, as $t_{0}$ is not final) and t_{1}=(\#_{0}(u_{m^{*}}))(\#_{0}(u_{{m^{*}}^{\prime}}^{\prime}))[b_{r+1},b_{r^{\prime}+1}]\^{\omega}$for some$1\leq m^{},{m^{}}^{\prime}\leq n$.

Now, we construct $\varphi$. It is the conjunction of sentences expressing the following statements, which can be brought into prenex normal form. In order to improve readability, the construction of the sentences expressing each requirement is left to the reader.

Exactly one atomic proposition is satisfied at each position of each trace. 2. 2.

Every trace is either of type one or of type two. 3. 3.

No two distinct type one traces have the same rank. 4. 4.

For every type one trace $t$ of positive rank $r$ there exists a type one trace $t^{\prime}$ of rank $r-1$. 5. 5.

There exists a type two trace of the form (\#_{0}(u_{m}))(\#_{0}(u_{m}^{\prime}))[b_{0},b_{0}]\^{\omega}$for some$m$. 6. 6.

For every type two trace $t_{0}$ there exists a type two trace $t_{1}$ such that either $t_{0}$ is final or $t_{1}$ is a successor of $t_{0}$. 7. 7.

For every type two trace $t_{2}$ there exist two type one traces $t_{1}$ and $t_{1}^{\prime}$ such that $t_{2}$ and $t_{1}$ are $u$-compatible and $t_{2}$ and $t_{1}^{\prime}$ are $u^{\prime}$-compatible. 8. 8.

In every trace t=(\#_{j}(u_{m}))(\#_{j^{\prime}}(u_{m^{\prime}}^{\prime}))[b_{r},b_{r^{\prime}}]\^{\omega}$of type two, the letters from$\overline{\Sigma}$in$u_{m}$and$u_{m^{\prime}}^{\prime}$ are equal.

As an example, consider the following instance of PCP

[TABLE]

with solution $212$. We encode the solution by the set $T_{1}\cup T_{2}$ depicted below (where we drop the suffixes \^{\omega}$ for readability).

$T_{1}$:$T_{2}$:aa\#a\#\#0$$b\#\#aba1$$aa\#a\#\#01$$\overline{a}a\#\overline{a}\#\#(0,0)$$a\overline{a}\#\overline{a}ba(0,1)$$\overline{b}\#a\overline{b}a(1,1) $\overline{a}a\#ab\overline{a}(0,1)(1,0)$ $a\overline{a}\#\overline{a}\#\#(0,0)(1,1)$

Note that $T_{1}$ contains type one traces while $T_{2}$ contains type two traces. We claim that $T_{1}\cup T_{2}$ satisfies all eight requirement listed above. Requirements 1, 2, 3, and 8 are straightforward to verify. The relation between type one traces specified by Requirement 4 is given by the arrows between the type one traces in $T_{1}$. The initial trace as in Requirement 5 is the left most type two trace in $T_{2}$ and the successor relation on type two traces as in Requirement 6 is indicated by the arrows between the type two traces. The compatible type one traces as in Requirement 7 are given by the arrows from $T_{2}$ to $T_{1}$ with the solid arrows denoting the $u$-compatible type one traces and the dashed arrows denoting the $u^{\prime}$-compatible ones.

After this example, we prove that $\varphi$ has the desired properties in general. To this end, fix $k=2^{n}+2m+1$, which can be encoded in binary with polynomially many bits in $n+m$.

First, assume there is a solution $s\in\{1,\ldots,n\}^{+}$, i.e., we have $h(s)=h^{\prime}(s)$, where $h$ and $h^{\prime}$ are the homomorphisms induced by mapping $m$ to $u_{m}$ and $u_{m}^{\prime}$, respectively. We define

[TABLE]

and

[TABLE]

where

[TABLE]

where $r,j$ are the unique indices such that $r<|s|$, $j<|u_{s(r)}|$, and

[TABLE]

and, similarly, $r^{\prime},j^{\prime}$ are the unique indices such that $r^{\prime}<|s|$, $j^{\prime}<|u^{\prime}_{s(r^{\prime})}|$, and

[TABLE]

Intuitively, for every $i$, we pick the pair $(u_{s(r)},u^{\prime}_{s(r^{\prime})})$ of words of the instance the $i$-th letter of $h(s)$ is in, and mark its position correctly in those words.

Traces of $T_{1}$ are of type one and traces of $T_{2}$ are of type two. It is then easy to check that Requirements 1 to 8 are satisfied by $T=T_{1}\cup T_{2}$. Furthermore, as $|s|\leq 2^{2^{n}}$, the size of the $b_{r}$ is at most $2^{n}$. Thus, all words of $T$ are of the form x\^{\omega}$with$|x|\leq 2^{n}+2m=k-1$, as required.

Conversely, assume $\varphi$ is satisfied by a set $T\subseteq\{xy^{\omega}\mid|x|+|y|\leq k\}$ of traces. Then, by Requirement 2, we have $T=T_{1}\cup T_{2}$ where $T_{1}$ is a set of type one traces and $T_{2}$ is a set of type two traces. Let $r^{*}$ be the maximal rank of a trace in $T_{1}$ (which is well-defined as $T_{1}$ is finite). Then, by Requirements 3 and 4, there exists exactly one trace $t^{1}_{r}\in T_{1}$ such that $t^{1}_{r}$ is of rank $r$, for all $0\leq r\leq r^{*}$. Let $s^{*}\in\{1,...,n\}^{r^{*}+1}$ be such that for all $r\leq r^{*}$, t^{1}_{r}=\#(u_{s^{*}(r)})\#(u^{\prime}_{s^{*}(r)})b_{r}\^{\omega}$. Note that as$t^{1}{r^{*}}=#(u{s({r^{}})})#(u^{\prime}_{s({r^{}})})b_{r^{}}$^{\omega}\in T$, we must have$2m+|b_{r^{}}|+1\leq k$. Thus,$|b_{r^{}}|\leq 2^{n}$, and$r^{}<2^{2^{n}}$.

By Requirements 5 and 6, there exists a sequence of traces $t^{2}_{0},t^{2}_{1},\ldots,t^{2}_{p}\in T_{2}$ such that $t^{2}_{i+1}$ is a successor of $t^{2}_{i}$ for all $0\leq i\leq p$, such that t^{2}_{0}=(\#_{0}(u_{m}))(\#_{0}(u^{\prime}_{m}))[b_{0},b_{0}]\^{\omega}$for some$m$, and such that$t^{2}_{p}$ is final.

An induction over $i$, using Requirements 6 and 7, shows that the first letter with a bar in $t^{2}_{i}$ is the $i$-th letter of $u_{s^{*}(0)}\cdots u_{s^{*}(r^{*})}$ and the second one is the $i$-th letter of $u^{\prime}_{s^{*}(0)}\cdots u^{\prime}_{s^{*}(r^{*})}$. Requirement 8 ensures that those two letters are always equal. As $t^{2}_{p}$ is final, there exists a prefix $s$ of $s^{*}$ such that $|u_{s(0)}\cdots u_{s(|s|-1)}|=|u^{\prime}_{s(0)}\cdots u^{\prime}_{s(|s|-1)}|=p+1$ and $u_{s(0)}\cdots u_{s(|s|-1)}(i)=u^{\prime}_{s(0)}\cdots u^{\prime}_{s(|s|-1)}(i)$ for all $i$, i.e., the two words are equal. As $|s|\leq|s^{*}|\leq 2^{2^{n}}$, we therefore obtain a solution to the PCP instance. ∎

As expected, the complexity of the satisfiability problem increases the more traces one has at hand to encode computations. In Theorem 3.1, we have exponentially many; in Theorem 3.2, we have doubly-exponentially many. In our last theorem, we consider infinite sets of traces that are finitely representable by finite-state systems. Here, satisfiability becomes intractable, yet still decidable, even when restricted to formulas of temporal depth one.

Formally, a Kripke structure ${\mathcal{K}}=(Q,\delta,q_{0},\lambda)$ consists of a finite set $Q$ of states, an initial state $q_{0}\in Q$, a transition function $\delta\colon Q\rightarrow 2^{Q}\setminus\{\emptyset\}$ for all $q$, and a labelling function $\lambda\colon Q\rightarrow 2^{\mathrm{AP}}$. A run of ${\mathcal{K}}$ is an infinite sequence $q_{0}q_{1}q_{2}\cdots$ of states starting with $q_{0}$ and such that $q_{j+1}\in\delta(q_{j})$ for all $j\in\mathbb{N}$. A trace of ${\mathcal{K}}$ is the sequence of labels $\lambda(q_{0})\lambda(q_{1})\lambda(q_{2})\cdots$ associated to a run $q_{0}q_{1}q_{2}\cdots$ of ${\mathcal{K}}$. The set of traces of ${\mathcal{K}}$ is denoted by $\mathrm{T}({\mathcal{K}})$.

Theorem 3.3

The following problem is Tower-complete: Given a HyperLTL sentence $\varphi$ and $k\in\mathbb{N}$ (in binary), does $\varphi$ have a model $T({\mathcal{K}})$ for some Kripke structure ${\mathcal{K}}$ with at most $k$ states?

Proof

Clarkson et al. presented a model-checking algorithm for HyperCTL∗ (and thus for HyperLTL, which is a fragment of HyperCTL∗), and showed that its complexity is a tower of exponentials whose height is the alternation depth of the input sentence [3]. Thus, one can enumerate all Kripke structures with at most $k$ states (up to isomorphism) and model-check them one by one in Tower. This yields the desired upper bound, as there are “only” exponentially many (in $k$) Kripke structures with $k$ states.

The lower bound is obtained by a reduction from the universality problem for star-free regular expressions with complementation. The equivalence problem for those expressions is Tower-complete (under elementary reductions, which is standard for Tower-complete problems), even for two-letter alphabets [25, 27]. As those expressions are closed by complementation and union, the universality problem is Tower-complete as well.

Star-free expressions with complementation over $\{a,b\}$ are generated by the grammar

[TABLE]

and have the obvious semantics inducing a language over $\{a,b\}^{*}$, denoted by $e$ as well.

Let $e$ be such an expression. We construct a HyperLTL sentence $\varphi_{e}$ and a Kripke structure ${\mathcal{K}}$ such that $T({\mathcal{K}})$ is a model of $\varphi_{e}$ if and only if $e$ is universal. ${\mathcal{K}}$ does not depend on $e$ and is shown in Figure 1. As all sets of variables in ${\mathcal{K}}$ are singletons, we indifferently use the notation $a$ for the letter $a$ and the singleton $\{a\}$. The set of traces induced by this Kripke structure is

[TABLE]

Given an expression $e$ and a trace variable $\pi$, we inductively define a formula $\psi_{e,\pi}$ which expresses that when $\pi$ is mapped by a trace assignment $\Pi$ to a trace of ${\mathcal{K}}$ of the form $l^{n}wr^{\omega}$ with $w\in\{a,b\}^{*}$, then $w\in e$ if and only if $(T({\mathcal{K}}),\Pi)\models\psi_{e,\pi}$.

• •

$\psi_{\emptyset,\pi}=a_{\pi}\land\neg a_{\pi}$: No trace assignment satisfies $\psi_{\emptyset,\pi}$, just as the language of $\emptyset$ does not contain any word.

• •

$\psi_{\varepsilon,\pi}={\mathbf{G\,}}(l_{\pi}\lor r_{\pi})$: $(T({\mathcal{K}}),\Pi)$ with $\Pi(\pi)=l^{n}wr^{\omega}$ satisfies $\psi_{\varepsilon,\pi}$ if and only if $w=\varepsilon$.

• •

$\psi_{a,\pi}=\exists\tau.({\mathbf{F\,}}\#_{\tau})\land{\mathbf{F\,}}(a_{\pi})\land{\mathbf{G\,}}(l_{\tau}\Leftrightarrow l_{\pi}\land r_{\tau}\Leftrightarrow r_{\pi})$ : The traces of ${\mathcal{K}}$ with an occurrence of $\#$ are the traces of the form $l^{*}\#r^{\omega}$. Thus, $(T({\mathcal{K}}),\Pi)$ with $\Pi(\pi)=l^{n}wr^{\omega}$ satisfies $\psi_{a,\pi}$ if and only if $l^{n}wr^{\omega}$ is a copy of such a trace with $\#$ replaced by $a$, i.e., if and only if $w=a$.

• •

$\psi_{b,\pi}=\exists\tau.({\mathbf{F\,}}\#_{\tau})\land{\mathbf{F\,}}(b_{\pi})\land{\mathbf{G\,}}(l_{\tau}\Leftrightarrow l_{\pi}\land r_{\tau}\Leftrightarrow r_{\pi})$: Similarly to $\psi_{a,\pi}$.

• •

$\psi_{e_{1}+e_{2},\pi}=\psi_{e_{1},\pi}\lor\psi_{e_{2},\pi}$.

• •

$\psi_{e_{1}e_{2},\pi}=\exists\pi_{1}.\exists\pi_{2}.\psi\wedge\psi^{\prime}$ with

[TABLE]

expressing that $\pi_{1}$ and $\pi_{2}$ are of the form $l^{n_{1}}w_{1}r^{\omega}$ and $l^{n_{2}}w_{2}r^{\omega}$ with $w_{1}\in e_{1}$ and $w_{2}\in e_{2}$, and with

[TABLE]

expressing that $n_{2}=n_{1}+|w_{1}|$ and that $w=w_{1}w_{2}$, where $\Pi(\pi)=l^{n}wr^{\omega}$. Thus, $(T({\mathcal{K}}),\Pi)$ satisfies $\psi_{e_{1}e_{2},\pi}$ if and only if there exist $w_{1}\in e_{1},w_{2}\in e_{2}$ such that $w=w_{1}w_{2}$.

• •

$\psi_{\neg e,\pi}=\neg\psi_{e,\pi}$.

Although this inductive definition does not necessarily give a formula in prenex normal form, one can easily check that no quantifier is in the scope of a temporal operator, thus the resulting formula can be turned into a HyperLTL formula.

To conclude, consider the sentence $\varphi_{e}=\forall\pi.{\mathbf{G\,}}\neg r_{\pi}\lor{\mathbf{F\,}}\#_{\pi}\lor\psi_{e,\pi}$, which can again be brought into prenex normal form. Further, note that no temporal operator is in the scope of another one, thus $\varphi_{e}$ has temporal depth one. The set $T({\mathcal{K}})$ is a model of $\varphi_{e}$ if and only if all its traces are in $\{a,b,l\}^{\omega}$, in $l^{*}\#r^{\omega}$, or of the form $l^{*}wr^{\omega}$ with $w\in e$. This is the case if and only if all words $w\in\{a,b\}^{*}$ are in the language of $e$, i.e., if and only if $e$ is universal. ∎

As the Kripke structure ${\mathcal{K}}$ in the lower bound proof above is fixed, we also obtain a novel hardness result for model-checking.

Corollary 1

HyperLTL model-checking a fixed Kripke structure with five states is Tower-complete, even for sentences of temporal depth one.

Note that one could already infer the Tower-completeness of the model-checking problem by carefully examining the proof of Theorem 5 of [3] concerning HyperCTL∗ model-checking. The reduction from the satisfiability problem for QPTL presented there also works for HyperLTL, albeit with temporal depth larger than one. Interestingly, both reductions use a fixed Kripke structure, meaning in particular that the encoding of $k$ has no impact on the asymptotic complexity.

4 Satisfiability for Restricted Classes of Formulas

After studying the HyperLTL satisfiability problem for classes of restricted models, but arbitrary formulas, we now consider restrictions on formulas, but arbitrary models. Recall that Finkbeiner and Hahn presented a complete picture in terms of quantifier prefixes: Satisfiability is PSpace-complete for the alternation-free fragments $\exists^{*}$ and $\forall^{*}$ as well as ExpSpace-complete for $\exists^{*}\forall^{*}$. In all other cases, the problem is undecidable, i.e., as soon as there is a single universal quantifier in front of existential ones.

In a sense, the decidable fragments are variants of LTL: Both alternation-free fragments can easily be reduced to LTL satisfiability while the $\exists^{*}\forall^{*}$ one is easily reducible to the $\exists^{*}$ fragment, with an exponential blowup. Thus, the decidable fragments barely exceed the realm of LTL.

In this section, we consider another dimension to measure the complexity of formulas, temporal depth, i.e., we restrict the nesting of temporal operators. The hope is that in this setting, we can obtain decidability for larger quantifier prefix classes. However, a slight adaptation of Finkbeiner and Hahn’s undecidability result for $\forall\exists^{*}$, along with an application of Lemma 1 proven below, already shows undecidability for $\forall\exists^{*}$ formulas of temporal depth two and without untils.

Thus, we have to restrict our search to fragments of temporal depth one, which contain most of the information flow policies expressible in HyperLTL [3]. And indeed, we prove satisfiability decidable for $\exists^{*}\forall\exists^{*}$ HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$ formulas. Thus, if the temporal depth is one and untils are excluded, then one can allow a universal quantifier in front of existential ones without losing decidability. This fragment includes, for example, the noninference property [22].

However, even allowing the smallest possible extension, i.e., adding a second universal quantifier, leads again to undecidability: HyperLTL satisfiability is undecidable for $\forall^{2}\exists^{*}$ formulas of temporal depth one using only ${\mathbf{F\,}}$ as temporal operator. Thus, satisfiability remains hard, even when severely restricting the temporal depth of formulas. Our results for temporal depth one are summarized in Table 1.

We begin this section by showing that every HyperLTL formula can be transformed in polynomial time into an equisatisfiable one with quantifier prefix $\forall^{2}\exists^{*}$ with temporal depth two. Thus, this fragment already captures the full complexity of the satisfiability problem. This transformation is later used in several proofs.

Theorem 4.1

For every HyperLTL sentence one can compute in polynomial time an equisatisfiable sentence of the form $\forall^{2}\exists^{*}$ with temporal depth at most two.

We decompose the proof into three steps, formalized by the following three lemmas. We begin by reducing the temporal depth to at most two by adapting a construction of Demri and Schnoebelen, which associates to every LTL formula an equisatisfiable formula with temporal depth at most two [7].

The idea is to add atomic propositions to witness the satisfaction of subformulas $\psi^{\prime}$ of $\psi$. We express the existence, for every $n$-tuple of traces $(t_{1},\ldots,t_{n})$ of the model, of a witness trace. For all $j\in\mathbb{N}$, for all subformulas $\psi^{\prime}$ of $\psi$, the valuation $[(\pi_{i}\rightarrow t_{i}[j,\infty))_{1\leq i\leq n}]$ satisfies $\psi^{\prime}$ if and only if the associated atomic proposition is satisfied at position $j$ of the witness trace.

Lemma 1

For every HyperLTL sentence $Q_{1}\pi_{1}\ldots Q_{n}\pi_{n}.\psi$ with quantifier-free $\psi$, one can compute in polynomial time an equisatisfiable sentence $Q_{1}\pi_{1}\ldots Q_{n}\pi_{n}.\exists\pi.\psi^{\prime}$ with quantifier-free $\psi^{\prime}$ and temporal depth at most two.

Proof

Let $\varphi=Q_{1}\pi_{1}\ldots Q_{n}\pi_{n}.\psi$ with quantifier-free $\psi$ and $Q_{i}\in\{\exists,\forall\}$ for all $i$. We denote by $\psi^{\prime}\sqsubseteq\psi$ the fact that $\psi^{\prime}$ is a subformula of $\psi$ and introduce a fresh atomic proposition $m^{\psi^{\prime}}$ for every $\psi^{\prime}\sqsubseteq\psi$. To every trace assignment $\Pi=[(\pi_{i}\rightarrow t_{i})_{1\leq i\leq n}]$ we associate a witness trace $\mathrm{wtns}(t_{1},\ldots,t_{n})$ such that:

• •

For all $a\in\mathrm{AP}$ and all $j\in\mathbb{N}$, $a\in\mathrm{wtns}(t_{1},\ldots,t_{n})(j)$ if and only if $a\in t_{1}(j)$, i.e., the projection of $\mathrm{wtns}(t_{1},\ldots,t_{n})$ to $\mathrm{AP}$ is equal to $t_{1}$.

• •

For all $\psi^{\prime}\sqsubseteq\psi$ and all $j\in\mathbb{N}$, $m^{\psi^{\prime}}\in\mathrm{wtns}(t_{1},\ldots,t_{n})(j)$ if and only if $(T,\Pi[j,\infty))\models\psi^{\prime}$.

Thus, $\mathrm{wtns}(t_{1},\ldots,t_{n})$ is a copy of $t_{1}$ on which we use the $m^{\psi^{\prime}}$ to mark the positions at which $\psi^{\prime}$ is satisfied. Now, define

[TABLE]

Intuitively, $\varphi^{\prime}$ has an additional existentially quantified variable $\tau$ that acts as a witness and we ensure that its marking is consistent with the semantics of HyperLTL using a formula $\overline{\psi^{\prime}}$ for each $\psi^{\prime}\sqsubseteq\psi$, which is defined as follows:

• •

$\overline{a_{\pi}}={\mathbf{G\,}}(m^{a_{\pi}}_{\tau}\Leftrightarrow a_{\pi})$

• •

$\overline{\psi_{1}\lor\psi_{2}}={\mathbf{G\,}}(m^{\psi_{1}\lor\psi_{2}}_{\tau}\Leftrightarrow(m^{\psi_{1}}_{\tau}\lor m^{\psi_{2}}_{\tau}))$

• •

$\overline{\neg\psi_{1}}={\mathbf{G\,}}(m^{\neg\psi_{1}}_{\tau}\Leftrightarrow\neg m^{\psi_{1}}_{\tau})$

• •

$\overline{{\mathbf{X\,}}\psi_{1}}={\mathbf{G\,}}(m^{{\mathbf{X\,}}\psi_{1}}_{\tau}\Leftrightarrow{\mathbf{X\,}}m^{\psi_{1}}_{\tau})$

• •

$\overline{\psi_{1}{\mathbf{\,U\,}}\psi_{2}}={\mathbf{G\,}}(m^{\psi_{1}{\mathbf{\,U\,}}\psi_{2}}_{\tau}\Leftrightarrow m^{\psi_{1}}_{\tau}{\mathbf{\,U\,}}m^{\psi_{2}}_{\tau})$

We claim that $\varphi^{\prime}$ has the desired properties.

Suppose $\varphi^{\prime}$ is satisfied by a model $T^{\prime}$. Then, for all $t^{\prime}\in T^{\prime}$ let $t$ be the projection of $t^{\prime}$ to $\mathrm{AP}$, and let $T$ be the set of those traces $t$. An induction on $\psi$ allows one to prove that if

[TABLE]

for some trace assignment $\Pi^{\prime}$ over $T^{\prime}$, then $(T^{\prime},\Pi^{\prime})\models\psi$. As $\psi$ only contains propositions from $\mathrm{AP}$, this implies $(T,\Pi)\models\psi$, where for all $\pi$, $\Pi(\pi)$ is the projection of $\Pi^{\prime}(\pi)$ to $\mathrm{AP}$.

Then, an induction on the number of quantifiers allows to generalize this: For all $0\leq i\leq n-1$, for all $\Pi^{\prime}$, if

[TABLE]

then $(T,\Pi)\models Q_{n-i}\pi_{n-i}\ldots Q_{n}\pi_{n}.\psi$ where $\Pi(\pi)$ is again the projection of $\Pi^{\prime}(\pi)$ to $\mathrm{AP}$. Thus, as $T^{\prime}$ satisfies $\varphi^{\prime}$, $T$ satisfies $\varphi$.

Now suppose $\varphi$ is satisfied by a model $T$. Let $T^{\prime}=\{\mathrm{wtns}(t_{1},\ldots,t_{n})\mid t_{1},\ldots,t_{n}\in T\}$. As the projection of $\mathrm{wtns}(t_{1},\ldots,t_{n})$ to $\mathrm{AP}$ is $t_{1}$, $T$ is the set of projections of traces of $T^{\prime}$ to $\mathrm{AP}$. Furthermore, $T^{\prime}$ contains a witness for all the tuples of traces of $T$, allowing us to prove that $T^{\prime}$ satisfies $\varphi^{\prime}$ as follows.

For all $\Pi$, if $(T,\Pi)\models\psi$, then let $\Pi^{\prime}$ be such that $\Pi^{\prime}(\pi_{i})=\mathrm{wtns}(\Pi(\pi_{i}),\ldots,\Pi(\pi_{i}))$ (whose projection to $\mathrm{AP}$ is $\Pi(\pi_{i})$) for all $i$ and $\Pi^{\prime}(\tau)=\mathrm{wtns}(\Pi(\pi_{1}),\ldots,\Pi(\pi_{n}))$. An induction on $\psi$ shows that $(T^{\prime},\Pi^{\prime})\models m^{\psi}_{\tau}\land\bigwedge_{\psi^{\prime}\sqsubseteq\psi}\overline{\psi^{\prime}}$. Hence, $(T^{\prime},\Pi^{\prime})\models\exists\tau.m^{\psi}_{\tau}\bigwedge_{\psi^{\prime}\sqsubseteq\psi}\overline{\psi^{\prime}}$.

Another induction on the number of quantifiers yields that, as $T$ satisfies $\varphi$, $T^{\prime}$ satisfies $\varphi^{\prime}$. Therefore, $\varphi$ and $\varphi^{\prime}$ are equisatisfiable. ∎

Next, we turn the quantifier prefix into the form $\forall^{*}\exists^{*}$ without increasing the temporal depth.

Here the key idea is to move existential quantifiers in the scope of universal ones after marking them with fresh atomic propositions: We can replace an $\exists\forall$ by a $\forall\exists$ if we require that the existentially quantified variable is now uniquely marked by a proposition (and therefore cannot depend on the universally quantified variable).

Lemma 2

For every HyperLTL sentence $\varphi$, one can compute in polynomial time an equisatisfiable sentence $\varphi^{\prime}$ of the form $\forall^{*}\exists^{*}$ with $\mathrm{td}(\varphi^{\prime})=\max(\mathrm{td}(\varphi),1)$.

Proof

We call an existential quantifier in a HyperLTL formula critical if there is a universal quantifier in its scope. Formulas without critical existential quantifiers are exactly formulas of the form $\forall^{*}\exists^{*}$. In what follows, we describe a polynomial time transformation to decrease the number of critical existential quantifiers of a formula. By iterating this procedure, we obtain a formula of the desired form.

Let $\varphi$ be a HyperLTL formula with at least one critical existential quantifier, i.e., $\varphi$ is of the form

[TABLE]

with $n\geq 0$, $p>0$, quantifier-free $\psi$, $Q_{i}\in\{\exists,\forall\}$, and $Q_{i}=\forall$ for some $i$.

If $\varphi$ has a model $T$, then the quantifier prefix $\forall\pi_{1}\ldots\forall\pi_{n}.\exists\pi_{n+1}$ of $\varphi$ induces a Skolem function $f$ associating to every $n$-tuple $(t_{1},\ldots,t_{n})$ of traces in $T$ a trace $f(t_{1},\ldots,t_{n})=t_{n+1}$ in $T$ such that $(T,\Pi)\models Q_{1}\tau_{1}\ldots Q_{p}\tau_{p}.\psi$, where $\Pi$ is the trace assignment with $\Pi(\pi_{i})=t_{i}$ for all $1\leq i\leq n+1$.

We introduce $n+1$ fresh propositions $m^{1},\ldots,m^{n+1}$ to mark the traces $t_{1},\ldots,t_{n+1}$ such that $f(t_{1},\ldots,t_{n})=t_{n+1}$. Let $\varphi^{\prime\prime}$ be the conjunction of the sentences

[TABLE]

which states the existence of the Skolem function, and

[TABLE]

which ensures that the Skolem function is correct. Note that we replaced the existential quantifier on $\pi{n+1}$ by a universal one. Note that the conjunction of those sentences can be turned into a HyperLTL sentence by renaming the trace variables $\pi_{i}$ in the first one into $\pi^{\prime}_{i}$ and then merging them in the following way:

[TABLE]

This formula has one less critical existential quantifier than $\varphi$. Hence, it only remains to prove that $\varphi$ and $\varphi^{\prime\prime}$ are equisatisfiable.

Suppose $\varphi$ is satisfiable. Then, it has a countable (possibly finite) model $T$ [14]. Thus, for all $t_{1},\ldots,t_{n}\in T$, there exists $t_{n+1}\in T$ with $(T,[(\pi_{i}\rightarrow t_{i})_{1\leq i\leq n+1}])\models Q_{1}\tau_{1},\ldots,Q_{p}\tau_{p},\psi$. Thus, for all $t_{1},\ldots,t_{n}\in T$ there exists a trace assignment $\Pi_{t_{1},\ldots,t_{n}}$ over $T$ with domain $\{\pi_{1},\ldots,\pi_{n},\pi_{n+1}\}$ such that

• •

$(T,\Pi_{t_{1},\ldots,t_{n}})\models Q_{1}\tau_{1},\ldots,Q_{p}\tau_{p},\psi$, and

• •

$\Pi_{t_{1},\ldots,t_{n}}(\pi_{i})=t_{i}$ for all $1\leq i\leq n$.

Also, fix an injection $g\colon T^{n+1}\rightarrow\mathbb{N}$ (which exists as $T$ is countable). Now, let $T^{\prime\prime}=\{t^{\prime\prime}\mid t\in T\}\subseteq(2^{\mathrm{AP}\cup\{m^{i}\mid 1\leq i\leq n+1\}})^{\omega}$ where $t^{\prime\prime}$ is obtained from $t$ as follows:

• •

The projection of $t^{\prime\prime}$ to $\mathrm{AP}$ is $t$, and

• •

for all $1\leq i\leq n+1$: $m^{i}\in t^{\prime\prime}(j)$ if and only if there exist $t_{1},\ldots,t_{n+1}$ such that $t=t_{i}$, $j=g(t_{1},...,t_{n+1})$, and $t_{n+1}=\Pi_{t_{1},\ldots,t_{n}}(\pi_{n+1})$, i.e., we encode the Skolem function using the marks $m^{i}$ at the position given by the injection $g$ to each $(n+1)$-tuple of traces.

We now prove that $T^{\prime\prime}$ is a model of $\varphi^{\prime\prime}$. To this end, fix some $t^{\prime\prime}_{1},\ldots,t^{\prime\prime}_{n+1}\in T^{\prime\prime}$, and let $\Pi^{\prime\prime}=[(\pi_{i}\rightarrow t_{i}^{\prime\prime})_{1\leq i\leq n+1}]$. There exist $t_{1},\ldots,t_{n+1}\in T$ such that $t_{i}$ is the projection of $t^{\prime\prime}_{i}$ to $\mathrm{AP}$ for all $i$. We denote $\Pi_{t_{1},\ldots,t_{n}}$ by $\Pi$. If $\Pi(\pi_{n+1})\neq t_{n+1}$ then $m^{i}\notin t^{\prime\prime}_{i}(g(t_{1},...,t_{n},t_{n+1}))$ for some $i$. By injectivity of $g$ and by definition of $T^{\prime\prime}$, there does not exist any other $j\in\mathbb{N}$ such that $m^{i}\in t^{\prime\prime}_{i}(j)$ for all $1\leq i\leq n+1$. Thus, $(T^{\prime\prime},\Pi^{\prime\prime})\not\models{\mathbf{F\,}}(\bigwedge_{i=1}^{n+1}m^{i}_{\pi_{i}})$ i.e., $(T^{\prime\prime},\Pi^{\prime\prime})\models Q_{1}\tau_{1}\ldots Q_{p}\tau_{p}.{\mathbf{F\,}}(\bigwedge_{i=1}^{n+1}m^{i}_{\pi_{i}})\Rightarrow\psi$.

If $\Pi(\pi_{n+1})=t_{n+1}$, i.e., $\Pi(\pi_{i})=t_{i}$ for all $i$, then by definition of $\Pi=\Pi_{t_{1},\ldots,t_{n}}$, $(T,\Pi)\models Q_{1}\tau_{1}\ldots Q_{p}\tau_{p}.\psi$. As $\psi$ only contains propositions from $\mathrm{AP}$ and as $t_{i}$ is the projection of $t^{\prime\prime}_{i}$ to $\mathrm{AP}$ for all $i$, $(T^{\prime\prime},\Pi^{\prime\prime})\models Q_{1}\tau_{1}\ldots Q_{p}\tau_{p}.\psi$. Thus, $(T^{\prime\prime},\Pi^{\prime\prime})\models Q_{1}\tau_{1}\ldots Q_{p}\tau_{p}.{\mathbf{F\,}}(\bigwedge_{i=1}^{n+1}m^{i}_{\pi_{i}})\Rightarrow\psi$ as well. As we have picked $t_{0},\ldots,t_{n+1}$ arbitrarily, we have shown $T^{\prime\prime}\models\varphi_{2}$.

Hence, it remains to consider $\varphi_{1}$. Recall that in this formula, $\pi_{n+1}$ is quantified existentially. Thus, fix some $t^{\prime\prime}_{1},\ldots,t^{\prime\prime}_{n}$ in $T^{\prime\prime}$ and let $t_{1},\ldots,t_{n}$ be their projections to $\mathrm{AP}$. As argued above, there is a trace $t_{n+1}$ in $T$ such that $\Pi_{t_{1},\ldots,t_{n}}(\pi_{n+1})=t_{n+1}$. By definition of $g$ and $T^{\prime\prime}$, $m^{i}\in t^{\prime\prime}_{i}(g(t_{1},\ldots,t_{n+1}))$ for all $i$. Therefore, $(T^{\prime\prime},[(\pi_{i}\rightarrow t^{\prime\prime}_{i})_{1\leq i\leq n+1}])\models{\mathbf{F\,}}(\bigwedge_{i=1}^{n+1}m^{i}_{\pi_{i}})$. Thus, $T^{\prime\prime}$ is also a model of $\varphi_{1}$. Altogether, $T^{\prime\prime}$ is a model of $\varphi^{\prime\prime}$.

Conversely, suppose $\varphi^{\prime\prime}$ has a model $T^{\prime\prime}$. For all $t^{\prime\prime}\in T^{\prime\prime}$, let $t$ be its projection to $\mathrm{AP}$. Further, let $T=\{t\mid t^{\prime\prime}\in T^{\prime\prime}\}$. Fix some $t_{1},\ldots,t_{n}\in T$. Let $t^{\prime\prime}_{i}\in T^{\prime\prime}$ be such that $t_{i}$ is the projection of $t^{\prime\prime}_{i}$ to $\mathrm{AP}$ for all $i$. As $T^{\prime\prime}$ models $\varphi^{\prime\prime}$, there exists $t^{\prime\prime}_{n+1}\in T^{\prime\prime}$ such that $(T^{\prime\prime},[(\pi_{i}\rightarrow t^{\prime\prime}_{i})_{1\leq i\leq n+1}])\models{\mathbf{F\,}}(\bigwedge_{i=1}^{n+1}m^{i}_{\pi_{i}})$.

Also, as $T^{\prime\prime}$ models $\varphi^{\prime\prime}$, $(T^{\prime\prime},[(\pi_{i}\rightarrow t^{\prime}_{i})_{1\leq i\leq n+1}])\models Q_{1}\tau_{1}\ldots Q_{p}\tau_{p}.{\mathbf{F\,}}(\bigwedge_{i=1}^{n+1}m^{i}_{\pi_{i}})\Rightarrow\psi$. Now, as $\psi$ only contains variables of $\mathrm{AP}$, $(T,[(\pi_{i}\rightarrow t_{i})_{1\leq i\leq n+1}])\models Q_{1}\tau_{1}\ldots Q_{p}\tau_{p}.\psi$.

As we have picked $t_{1},\ldots,t_{n}$ arbitrarily, we have shown that $T$ is a model of $\varphi$. ∎

The construction presented in the proof of Lemma 2 may increase the number of universally quantified variables, but we can decrease that number to two without increasing the temporal or alternation depth. This step also completes the proof of Theorem 4.1

This transformation can be achieved by merging several traces into one. To this end, we increase the set of atomic propositions by considering as new atomic propositions tuples of the previous atomic propositions, i.e., one trace now encodes a tuple of traces. However we cannot decrease the number of universal quantifiers below two this way, as we need two universal quantifiers to ensure that every possible combination of traces is represented in the model, i.e., any model of the resulting formula is the set of mergings of traces of another model.

Lemma 3

For every HyperLTL sentence $\varphi$ of the form $\forall^{*}\exists^{*}\psi$ with quantifier-free $\psi$, one can compute in polynomial time an equisatisfiable sentence $\varphi^{\prime}$ of the form $\forall^{2}\exists^{*}\psi^{\prime}$ where $\psi^{\prime}$ is quantifier-free and $\mathrm{td}(\varphi^{\prime})=\max(\mathrm{td}(\varphi),1)$.

Proof

Let $\varphi=\forall\pi_{1}\ldots\forall\pi_{n}\exists\pi_{n+1}\ldots\exists\pi_{n+n^{\prime}}\psi$ with quantifier-free $\psi$, i.e., $\varphi$ starts with $n$ universal quantifiers. We only consider the case $n>2$, as otherwise we can just choose $\varphi^{\prime}=\varphi$.

We construct a sentence $\varphi^{\prime}$ over $\mathrm{AP}\times\{1,\ldots,n\}$, i.e., a single trace represents a tuple of $n$ traces over $\mathrm{AP}$. The two universally quantified variables are employed to ensure that every possible tuple is represented by a trace: Given two traces, we state the existence of $n^{2}$ other traces that are shufflings of those two. We also simulate the universal quantifiers of $\varphi$ using the first of the two universal quantifiers in $\varphi^{\prime}$: instead of quantifying $n$ times a single trace, we quantify an $n$-tuple of traces once.

Formally, we define

[TABLE]

where

[TABLE]

expresses that $\pi$ takes all the tuples of traces of the model as values: For any two tuples $(t_{1},\ldots,t_{n})$, $(t^{\prime}_{1},\ldots,t^{\prime}_{n})$ and for all $1\leq i_{1},i_{2}\leq n$ we make sure that the trace $(t_{1},\ldots,t_{i_{1}-1},t^{\prime}_{i_{2}},t_{i_{1}+1},\ldots,t_{n})$ also appears. This property implies that all tuples of traces are taken into account when $\pi$ is ranging over them.

Furthermore, $\psi_{2}$ is obtained from $\psi$ by replacing each atomic formula $a_{\pi_{j}}$ for $1\leq j\leq n$ with $(a,j)_{\pi}$ and every $a_{\pi_{j}}$ for $n+1\leq j\leq n+n^{\prime}$ by $(a,1)_{\pi_{j}}$, i.e., we identify the universally quantified traces with the components of a tuple of traces assigned to $\pi$ in $\psi_{2}$ and the existentially ones with the first components of the tuples assigned to the $\pi_{i}$ in $\psi_{2}$.

Suppose $\varphi$ has a model $T$. Then, for all $t_{1},\ldots,t_{n}\in T$ let $\mathrm{mrg}(t_{1},\ldots,t_{n})$ be the trace over $\mathrm{AP}\times\{1,\ldots,n\}$ such that $\mathrm{mrg}(t_{1},\ldots,t_{n})(j)=\bigcup_{i=1}^{n}t_{i}(j)\times\{i\}$ for all $j\in\mathbb{N}$. Let $\mathrm{mrg}(T)=\{\mathrm{mrg}(t_{1},\ldots,t_{n})\mid t_{1},\ldots,t_{n}\in T\}$. Note that there is a bijection between $n$-tuples over traces from $T$ and traces in $\mathrm{mrg}(T)$.

Let $t^{\prime}\in\mathrm{mrg}(T)$, there exist $t_{1},\ldots,t_{n}\in T$ such that $t^{\prime}=\mathrm{mrg}(t_{1},\ldots,t_{n})$. As $T$ is a model of $\varphi$, there exist $t_{n+1},\ldots,t_{n+n^{\prime}}$ such that $(T,[(\pi_{i}\rightarrow t_{i})_{1\leq i\leq n+n^{\prime}}])\models\psi$. Further, let $t^{\prime}_{1},\ldots,t^{\prime}_{n}\in T$ be arbitrary. Then, one can check that the trace assignment associating

• •

$\mathrm{mrg}(t_{1},\ldots,t_{n})$ to $\pi$,

• •

$\mathrm{mrg}(t^{\prime}_{1},\ldots,t^{\prime}_{n})$ to $\pi^{\prime}$,

• •

$\mathrm{mrg}(t_{i},\ldots,t_{i})$ to $\pi_{i}$ with $n+1\leq i\leq n+n^{\prime}$, and

• •

$\mathrm{mrg}(t_{1},\ldots,t_{i_{1}-1},t^{\prime}_{i_{2}},t_{i_{1}+1},\ldots,t_{n})$ to $\tau_{(i_{1},i_{2})}$

satisfies both $\psi_{1}$ and $\psi_{2}$. Thus, as we have picked the $t_{i}$ and $t_{i}^{\prime}$ for $1\leq i\leq n$ arbitrarily, we conclude that $\mathrm{mrg}(T)$ is a model of $\varphi^{\prime}$.

Conversely, suppose $\varphi^{\prime}$ has a model $T^{\prime}$. For all $t^{\prime}\in T^{\prime}$, let $t$ be the trace over $\mathrm{AP}$ such that $t(j)=\{a\mid(a,1)\in t^{\prime}(j)\}$ for all $j\in\mathbb{N}$, and let $T=\{t\mid t^{\prime}\in T^{\prime}\}$. As $T^{\prime}$ satisfies $\varphi^{\prime}$, for all $t^{\prime}_{1},t^{\prime}_{2}\in T$, for all $1\leq i_{1},i_{2}\leq n$ there exist $t^{\prime}_{i_{1},i_{2}}$ which is identical to $t^{\prime}_{1}$ on all $\mathrm{AP}\times\{i\}$ except for $\mathrm{AP}\times\{i_{1}\}$, for which it is identical to $t^{\prime}_{2}$ on $\mathrm{AP}\times\{i_{2}\}$. Because of this property, one can see that $T^{\prime}$ is equal to $\{\mathrm{mrg}(t_{1},\ldots,t_{n})\mid t_{1},\ldots,t_{n}\in T\}$.

Now, an induction on the construction of $\psi_{2}$ shows that, as $T^{\prime}$ satisfies $\varphi^{\prime}$, $T$ satisfies $\varphi$. ∎

Thus, $\forall^{2}\exists^{*}$ formulas with temporal depth two capture the complete complexity of the satisfiability problem for HyperLTL. As the latter problem is undecidable and as all reduction presented above are effective, we immediately obtain that satisfiability for $\forall^{2}\exists^{*}$ formulas with temporal depth two is also undecidable.

As alluded to above, an even stronger result can be obtained by strengthening the proof of Hahn and Finkbeiner for $\forall\exists^{*}$ formulas to only use temporal depth two. 111Alternatively, one can also obtain a direct reduction from the Turing machine immortality problem [17] to satisfiability of $\forall\exists$ sentences of temporal depth two. Thus, only formulas of temporal depth one remain to consider.

Before we start investigating this class let us quickly comment on why we disregard temporal depth zero: every such sentence can easily be turned to an equisatisfiable instance of QBF, which is known to be solvable in polynomial space.

Thus, it only remains to consider formulas with arbitrary quantifier prefixes, but temporal depth one. Our main result of this section shows that even this problem is undecidable, even for HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$ formulas with alternation depth one. Due to the restriction on the temporal depth, our encoding of a Minsky machine is more complicated than it would be with arbitrary temporal depth.

Theorem 4.2

The following problem is undecidable: Given a $\forall^{2}\exists^{*}$ HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$ sentence $\varphi$, is $\varphi$ satisfiable?

Proof

We reduce from the (non)-halting problem for 2-counter Minsky machines. Recall that such a machine can be seen as a tuple $\mathcal{M}=(Q,\Delta,q_{0})$ where $Q$ is a finite set of states, $q_{0}\in Q$ an initial state, and $\Delta\subseteq Q\times\{1,2\}\times OP\times Q$ a set of transition rules, where $OP=\{\texttt{++},\texttt{--},\texttt{=0?}\}$. A configuration of $\mathcal{M}$ is an element of $Q\times\mathbb{N}\times\mathbb{N}$. For all $n,n^{\prime}\in\mathbb{N}$, $op\in OP$ we write $n\xrightarrow{op}n^{\prime}$ if:

• •

$op$ is ++ and $n^{\prime}=n+1$.

• •

$op$ is -- and $n^{\prime}=n-1$ (note that this operation is only applicable if $n>0$).

• •

$op$ is =0? and $n^{\prime}=n=0$.

There is a transition from $(q,n_{1},n_{2})$ to $(q^{\prime},n^{\prime}_{1},n^{\prime}_{2})$ if and only if there exists $i\in\{1,2\}$ and $op\in OP$ such that $(q,i,op,q^{\prime})\in\Delta$, $n_{3-i}=n_{3-i}^{\prime}$ and $n_{i}\xrightarrow{op}n^{\prime}_{i}$. Given such a machine, it is undecidable whether it has an infinite computation $(q_{0},0,0)\rightarrow(q_{1},n_{1}^{1},n_{2}^{1})\rightarrow(q_{2},n_{1}^{2},n_{2}^{2})\rightarrow\cdots$.

Let $\mathcal{M}=(Q,\Delta,q_{0})$ be a 2-counter Minsky machine. We use $\mathrm{AP}=Q\cup\{1,2\}$ as atomic propositions. Given $i\in\{1,2\}$, we denote by $\overline{i}$ the other proposition. Consider the formula $\psi_{1}=\forall\pi.\forall\pi^{\prime}.{\mathbf{G\,}}(1_{\pi}\Rightarrow 1_{\pi^{\prime}})\lor{\mathbf{G\,}}(1_{\pi^{\prime}}\Rightarrow 1_{\pi})$. We define $\psi_{2}$ with $2\in\mathrm{AP}$ analogously. In the following, we only consider sets of traces that satisfy $\psi_{1}\wedge\psi_{2}$.

For each trace $t\in(2^{\mathrm{AP}})^{\omega}$ and $i\in\{1,2\}$, we define the $i$-set of $t$ as $S_{i}(t)=\{j\in\mathbb{N}\mid i\in t(j)\}$. Now fix $T\subseteq(2^{\mathrm{AP}})^{\omega}$ that satisfies $\psi_{1}\wedge\psi_{2}$. We define the order $\leq_{i}$ on $T$ as follows: for all $t,t^{\prime}\in T$, $t\leq_{i}t^{\prime}$ if and only if $S_{i}(t)\subseteq S_{i}(t^{\prime})$. We write $t<_{i}t^{\prime}$ if $S_{i}(t)\subsetneq S_{i}(t^{\prime})$. As $T$ satisfies $\psi_{1}\wedge\psi_{2}$, the $\leq_{i}$ are total orders on $T$. We also define for all $t\in T$ and $i\in\{1,2\}$, the rank of $t$ with respect to $i$ as $\mathrm{rk}_{i}(t)=|\{S_{i}(t^{\prime})\mid t^{\prime}\in T\text{ and }t^{\prime}<_{i}t\}|$, which may be infinite. Note that if $S_{i}(t)=\emptyset$ then $\mathrm{rk}_{i}(t)=0$, and that if $S_{i}(t)=S_{i}(t^{\prime})$ then $\mathrm{rk}_{i}(t)=\mathrm{rk}_{i}(t^{\prime})$. Finally, as $\leq_{i}$ is a total order, if we have $t<_{i}t^{\prime}$, but there is no $t^{\prime\prime}$ with $t<_{i}t^{\prime\prime}<_{i}t^{\prime}$, then $\mathrm{rk}_{i}(t^{\prime})=\mathrm{rk}_{i}(t)+1$. Note that this holds even when $\mathrm{rk}_{i}(t)$ is infinite, assuming $\infty+1=\infty$.

We construct a HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$ formula $\varphi$ that encodes the existence of an infinite computation $(q_{0},0,0)\rightarrow(q_{1},n_{1}^{1},n_{2}^{1})\rightarrow(q_{2},n_{1}^{2},n_{2}^{2})\rightarrow\cdots$ of $\mathcal{M}$. In a model $T$ of $\varphi$, a configuration $(q,n_{1},n_{2})$ is encoded by a trace $t$ with $t(0)\cap Q=\{q\}$ and for $i\in\{1,2\}$, $rk_{i}(t)=n_{i}$. Then, $\varphi$ states the existence of an initial trace $t_{0}$, representing the configuration $(q_{0},0,0)$, as well as the existence of a successor $t^{\prime}$ encoding $(q^{\prime},n_{1}^{\prime},n_{2}^{\prime})$ for each trace $t$ encoding $(q,n_{1},n_{2})$, i.e., we require $(q,n_{1},n_{2})\rightarrow(q^{\prime},n_{1}^{\prime},n_{2}^{\prime})$. The latter is witnessed by the existence of a transition $(q,i,op,q^{\prime})$ such that:

$t(0)\cap Q=\{q\}$ and $t^{\prime}(0)\cap Q=\{q^{\prime}\}$, i.e., $t$ and $t^{\prime}$ indeed encode the states of their respective configurations correctly. 2. 2.

For all $j\in\mathbb{N}$, $\overline{i}\in t(j)$ if and only if $\overline{i}\in t^{\prime}(j)$, i.e. $S_{\overline{i}}(t)=S_{\overline{i}}(t^{\prime})$. Thus, as argued above, $\mathrm{rk}_{\overline{i}}(t)=\mathrm{rk}_{\overline{i}}(t^{\prime})$, which implies $n_{\overline{i}}=n^{\prime}_{\overline{i}}$. 3. 3.

If $op$ is ++ then $t<_{i}t^{\prime}$ and there does not exist any $t^{\prime\prime}$ such that $t<_{i}t^{\prime\prime}<_{i}t^{\prime}$, i.e., $\mathrm{rk}_{i}(t^{\prime})=\mathrm{rk}_{i}(t)+1$, as $\leq_{i}$ is a total order. Then, we have $n_{i}^{\prime}=n_{i}+1$. 4. 4.

If $op$ is -- then $t>_{i}t^{\prime}$ and there does not exist any $t^{\prime\prime}$ such that $t>_{i}t^{\prime\prime}>_{i}t^{\prime}$, i.e., $\mathrm{rk}_{i}(t^{\prime})=\mathrm{rk}_{i}(t)-1$, as $\leq_{i}$ is a total order. Then, we have $n_{i}^{\prime}=n_{i}-1$. 5. 5.

If $op$ is =0? then for all $j\in\mathbb{N}$, $i\notin t(j)$ and $i\notin t^{\prime}(j)$. Hence, $S_{i}(t)=S_{i}(t^{\prime})=\emptyset$, i.e., $\mathrm{rk}_{i}(t)=\mathrm{rk}_{i}(t^{\prime})=0$, which implies $n_{i}=n_{i}^{\prime}=0$.

We encode those conditions in $\varphi$, which is the conjunction of the following three sentences and of $\psi_{1}\wedge\psi_{2}$:

• •

$\varphi_{1}=\forall\pi.\bigwedge_{q\neq q^{\prime}\in Q}q_{\pi}\Rightarrow\neg q^{\prime}_{\pi}$ expresses that a trace is associated to at most one state.

• •

$\varphi_{2}=\exists\pi_{0}.{(q_{0})}_{\pi_{0}}\land{\mathbf{G\,}}(\neg 1_{\pi_{0}}\land\neg 2_{\pi_{0}})$ expresses the existence of a trace representing the initial configuration $(q_{0},0,0)$.

• •

$\varphi_{3}=\forall\pi.\exists\pi^{\prime}.\bigvee_{(q,i,op,q^{\prime})\in\Delta}q_{\pi}\land q^{\prime}_{\pi^{\prime}}\land\varphi_{i,op}\land{\mathbf{G\,}}(\overline{i}_{\pi}\Leftrightarrow\overline{i}_{\pi^{\prime}})$ expresses that all traces have a successor obtained by faithfully simulating a transition of the machine.

Here, we use the formulas

• •

$\varphi_{1,\texttt{++}}=\forall\pi^{\prime\prime}.\pi<_{1}\pi^{\prime}\land(\pi^{\prime\prime}\leq_{1}\pi\lor\pi^{\prime}\leq_{1}\pi^{\prime\prime})$,

• •

$\varphi_{1,\texttt{--}}=\forall\pi^{\prime\prime}.\pi>_{1}\pi^{\prime}\land(\pi^{\prime\prime}\geq_{1}\pi\lor\pi^{\prime}\geq_{1}\pi^{\prime\prime})$, and

• •

$\varphi_{1,\texttt{=0?}}={\mathbf{G\,}}(\neg 1_{\pi}\land\neg 1_{\pi^{\prime}})$,

where $\pi\leq_{1}\pi^{\prime}={\mathbf{G\,}}(1_{\pi}\Rightarrow 1_{\pi^{\prime}})$ and $\pi<_{1}\pi^{\prime}=\pi\leq_{1}\pi^{\prime}\land{\mathbf{F\,}}(\neg 1_{\pi}\land 1_{\pi^{\prime}})$. Finally, we define the formulas $\leq_{2}$, $<_{2}$, and $\varphi_{2,op}$ analogously.

The sentence $\varphi$ is not in prenex normal form. However, as no quantifier appears in the scope of a temporal operator, it can be put in that form. Further, it is not of the form $\forall^{2}\exists^{*}$, but we can apply Lemmas 2 and 3 to bring it into this form while preserving the temporal depth, which is already one. We claim that $\varphi$ is satisfiable if and only if $\mathcal{M}$ has an infinite computation starting in $(q_{0},0,0)$.

Suppose $\varphi$ is satisfied by a model $T$. The subformulas $\varphi_{1}$ and $\varphi_{2}$ enforce that $T$ contains a trace $t_{0}$ encoding the initial configuration $(q_{0},0,0)$ of $\mathcal{M}$. Further, $\varphi_{3}$ expresses that every trace $t$ encoding a configuration $(q,n_{1},n_{2})$ has a successor $t^{\prime}$ encoding a configuration $(q^{\prime},n_{1}^{\prime},n_{2}^{\prime})$ with $(q,n_{1},n_{2})\rightarrow(q^{\prime},n_{1}^{\prime},n_{2}^{\prime})$. Thus, there exists an infinite sequence $t_{0},t_{1},t_{2},\ldots$ of traces encoding an infinite run of $\mathcal{M}$.

Conversely, suppose $\mathcal{M}$ has an infinite run $(q_{0},0,0)\rightarrow(q_{1},n_{1}^{1},n_{2}^{1})\rightarrow(q_{2},n_{1}^{2},n_{2}^{2})\cdots$, then for all $j$ let $t_{j}$ be the trace whose projection to $Q$ is $\{q_{j}\}\emptyset^{\omega}$, and whose projection to $\{i\}$ is $\{i\}^{n_{i}^{j}}\emptyset^{\omega}$ for $i\in\{1,2\}$. One can then easily check that $\{t_{j}\mid j\in\mathbb{N}\}$ is a model of $\varphi$. ∎

Thus, two universal quantifiers before some existential ones and using only ${\mathbf{F\,}}$ and ${\mathbf{G\,}}$ without nesting yields undecidable satisfiability. Our next result shows that removing one of the two universal quantifiers allows us to recover decidability, even when allowing nested next operators and leading existential quantifiers.

As a first step in the proof, we show that the nested next operators can be eliminated without introducing additional universal quantifiers. This is true, as we are only interested in satisfiability.

Lemma 4

For every $\exists^{*}\forall\exists^{*}$ HyperLTL${}^{1}(\mathbf{F},\mathbf{G},\mathbf{X}^{*})$ sentence, one can construct in polynomial time an equisatisfiable $\exists^{*}\forall\exists^{*}$ HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$ sentence.

Proof

Let $\varphi=\exists\tau_{1}\ldots\exists\tau_{n}.\forall\pi.\exists\tau_{n+1}\ldots\exists\tau_{n+n^{\prime}}.\psi$ be a HyperLTL${}^{1}(\mathbf{F},\mathbf{G},\mathbf{X}^{*})$ sentence. We assume w.l.o.g., that $\psi$ is a Boolean combination of formulas of the form ${\mathbf{F\,}}\beta$ and ${\mathbf{X\,}}^{k}\beta$ where $\beta$ is a Boolean combination of atomic propositions. Let $d$ be the maximal integer such that $\psi$ contains a subformula of the form ${\mathbf{X\,}}^{d}\beta$ (which is [math], if there is no ${\mathbf{X\,}}$ in $\psi$).

We extend the set of atomic propositions with fresh ones $m^{0},\ldots,m^{d}$ and define

[TABLE]

(i.e., we just add one existentially quantified variable $\tau_{0}$) with

[TABLE]

where $\psi^{\prime\prime}$ is $\psi$ where every maximal subformula of the form ${\mathbf{X\,}}^{k}\beta$ has been replaced with ${\mathbf{G\,}}({m^{k}}_{\tau_{0}}\Rightarrow\beta)$. Intuitively, we state the existence of a special trace on which the atomic propositions $m^{0},\ldots,m^{d}$ mark some positions which will simulate the positions from [math] up to $d$ in any order with any multiplicity. As we are dealing with satisfiability, and as the order of the valuations at these positions is irrelevant for the satisfaction of a HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$ formula, we obtain an equisatisfiable formula.

If $\varphi$ has a model $T$, then let $T^{\prime}=T\cup\{t_{0}\}$, with $t_{0}=\{m^{0}\}\ldots\{m^{d}\}\emptyset^{\omega}$. Here every $m^{k}$ appears once, at position $k$, thus, ${\mathbf{X\,}}^{k}\beta$ is satisfied by some assignment over $T$ if and only ${\mathbf{G\,}}(m^{k}\Rightarrow\beta)$ is satisfied by the same assignment over $T^{\prime}$. Then, one can show by a simple induction over the construction of $\psi^{\prime}$ that for all $t_{1},\ldots,t_{n+n^{\prime}},t$, $(T,[(\tau_{i}\rightarrow t_{i})_{1\leq i\leq n+n^{\prime}},\pi\rightarrow t])$ satisfies $\psi$ if and only if $(T^{\prime},[(\tau_{i}\rightarrow t_{i})_{0\leq i\leq n+n^{\prime}},\pi\rightarrow t])$ satisfies $\psi^{\prime}$. Since $\varphi$ and $\varphi^{\prime}$ have the same quantifier prefix (but for the quantification of $\tau_{0}$), and as $T$ satisfies $\varphi$, $T^{\prime}$ satisfies $\varphi^{\prime}$.

Conversely, if $\varphi^{\prime}$ has a model $T^{\prime}$, then let $t^{\prime}_{0}\in T^{\prime}$ be such that $(T^{\prime},[\tau_{0}\rightarrow t^{\prime}_{0}])$ satisfies

[TABLE]

In particular $(T^{\prime},[\tau_{0}\rightarrow t^{\prime}_{0}])$ satisfies $\bigwedge_{k=0}^{d}{\mathbf{F\,}}m^{k}_{\tau_{0}}$. Thus, there exist $j_{0},\ldots,j_{k}\in\mathbb{N}$ such that $m^{k}\in t^{\prime}_{0}(j_{k})$ for all $k$. For all $t^{\prime}\in T^{\prime}\setminus\{t^{\prime}_{0}\}$ let $t$ be the projection to $\mathrm{AP}$ of $t^{\prime}(j_{0})\cdots t^{\prime}(j_{d})t^{\prime}$, and let $T=\{t\mid t^{\prime}\in T^{\prime}\setminus\{t^{\prime}_{0}\}\}$. Thus, if a trace assignment over $T^{\prime}$ satisfies ${\mathbf{G\,}}(m^{k}_{\tau_{0}}\Rightarrow\beta)$ then the associated trace assignment over $T$ satisfies ${\mathbf{X\,}}^{k}\beta$. Furthermore, if a trace assignment over $T^{\prime}$ satisfies ${\mathbf{F\,}}\beta$ (respectively ${\mathbf{G\,}}\beta$) then so does the associated trace assignment over $T$ (we have not modified the set of combinations of valuations that eventually appear, just their order). Hence, as $\psi$ can be seen as a positive Boolean combination of such formulas, an induction over $\varphi$ shows that, as $\varphi^{\prime}$ is satisfiable, so is $\varphi$. ∎

Now, we are ready to prove our main decidability result in this section. Note that we do not claim a matching lower bound here. We comment on this gap in the conclusion.

Theorem 4.3

The following problem is in N2ExpTime: Given a HyperLTL${}^{1}(\mathbf{F},\mathbf{G},\mathbf{X}^{*})$ sentence $\varphi$ of the form $\exists^{*}\forall\exists^{*}$, is $\varphi$ satisfiable?

Proof

Let $\varphi=\exists\tau_{1}\ldots\tau_{n}.\forall\pi.\exists\tau_{n+1}\ldots\exists\tau_{n+n^{\prime}}.\psi$ be a HyperLTL${}^{1}(\mathbf{F},\mathbf{G},\mathbf{X}^{*})$ sentence with quantifier-free $\psi$. Due to Lemma 4, it is enough to consider the case where $\psi$ is a Boolean combination of formulas of the form ${\mathbf{F\,}}\beta$ for a Boolean combination $\beta$ of atomic propositions.

To every tuple $(t_{1},\ldots,t_{k})$ of traces $t_{i}\in(2^{\mathrm{AP}})^{\omega}$, we associate a finite set of tuples of valuations $V(t_{1},\ldots,t_{k})=\{(t_{1}(j),\ldots,t_{k}(j))\mid j\in\mathbb{N}\}\subseteq(2^{\mathrm{AP}})^{k}$, i.e., the set all the tuples of valuations that appear eventually. The cardinality of $V(t_{1},\ldots,t_{k})$ is at most $2^{k|\mathrm{AP}|}$.

Let $\beta$ be a Boolean combination of atomic propositions over trace variables $\pi_{1},\ldots,\pi_{k}$. Then, a trace assignment $[(\pi_{i}\rightarrow t_{i})_{1\leq i\leq k}]$ satisfies ${\mathbf{F\,}}\beta$ if and only if there exists $j\in\mathbb{N}$ such that $\beta$ is satisfied at position $j$ of $(t_{1},\ldots,t_{k})$, i.e., there exists $(v_{1},\ldots,v_{k})\in V(t_{1},\ldots,t_{k})$ such that $(v_{1},\ldots,v_{k})$ satisfies $\beta$ (in the sense that any trace assignment $\Pi$ such that $\Pi(\pi_{i})(0)=v_{i}$ for all $i$ satisfies $\beta$). Intuitively, we abstract a tuple of traces into a finite set of tuples of valuations, and then abstract a model as a set of such finite representations. Then, we show that satisfiability can be decided using such abstractions.

As a consequence, whether a given trace assignment $[(\pi_{i}\rightarrow t_{i})_{1\leq i\leq k}]$ satisfies a given Boolean combination $\psi$ of formulas ${\mathbf{F\,}}\beta$ only depends on $V(t_{1},\ldots,t_{k})$, and given $V\subseteq(2^{\mathrm{AP}})^{k}$, one can check in polynomial time whether a trace assignment yielding $V$ satisfies $\psi$. If it is the case, we say that $V$ satisfies $\psi$.

To check the satisfiability of $\varphi$, we start by nondeterministically guessing a set $S\subseteq 2^{(2^{\mathrm{AP}})^{n+n^{\prime}+1}}$ of sets of $(n+n^{\prime}+1)$-tuples of valuations. This set is supposed to represent a model of $\varphi$. The $n$ first valuations represent the fixed values assigned to $\tau_{1},\ldots,\tau_{n}$. The $(n+1)$-th represents the valuation of the universally quantified variable. Thus, for every trace of the model there must exist a tuple in which that trace is represented at position $n+1$. The valuations of positions $n+2$ to $n+n^{\prime}$ have to be such that $\varphi$ is satisfied by all tuples.

Thus, we check the following requirements:

For all $V_{1},V_{2}\in S$, $\{(v_{1},\ldots,v_{n})\mid(v_{1},\ldots,v_{n+n^{\prime}+1})\in V_{1}\}$ is equal to $\{(v_{1},\ldots,v_{n})\mid(v_{1},\ldots,v_{n+n^{\prime}+1})\in V_{2}\}$: The set of values taken by the traces assigned to $\tau_{1},\ldots,\tau_{n}$ cannot depend on the values of the other variables. Thus, we ensure that these values are fixed in the guessed model. 2. 2.

For all $V\in S$ and $1\leq i\leq n+n^{\prime}+1$, there exists $V^{\prime}\in S$ such that $\{(v_{1},\ldots,v_{n},v_{i})\mid(v_{1},\ldots,v_{n+n^{\prime}+1})\in V\}=\{(v_{1},\ldots,v_{n+1})\mid(v_{1},\ldots,v_{n+n^{\prime}+1})\in V^{\prime}\}$. All the values taken by the existentially quantified variables have to be taken by the universally quantified one as well. 3. 3.

For all $V\in S$, $V$ satisfies $\psi$.

If all requirements are satisfied, we accept, otherwise we reject. This procedure requires nondeterministic doubly-exponential time as $|S|\leq 2^{2^{|\mathrm{AP}|+n+n^{\prime}+1}}$.

Suppose $\varphi$ is satisfiable and fix a model $T$. There exist $t_{1},\ldots,t_{n}\in T$ such that $(T,[(\tau_{i}\rightarrow t_{i})_{1\leq i\leq n}])\models\forall\pi\exists\tau_{n+1}\ldots\exists\tau_{n+n^{\prime}}.\psi$. Furthermore, for a fixed $t\in T$ there exist $t_{n+1},\ldots,t_{n+n^{\prime}}\in T$ such that $(T,[(\tau_{i}\rightarrow t_{i})_{1\leq i\leq n+n^{\prime}},\pi\rightarrow t])\models\psi$. Let $V^{*}(t)=\{(t_{1}(j),\ldots,t_{n}(j),t(j),t_{n+1}(j),\ldots,t_{n+n^{\prime}}(j))\mid j\in\mathbb{N}\}$.

Now, one can easily check that Requirements 1, 2, and 3 are satisfied by $\{V^{*}(t)\mid t\in T\}$. Thus, the algorithm accepts $\varphi$.

Conversely, suppose the algorithm accepts $\varphi$. Then, there exists some $S$ satisfying all three requirements above. We construct from $S$ a model $T$ of $\varphi$.

Let $t_{1},\ldots,t_{n}$ be traces such that for all $V\in S$, $\{(v_{1},\ldots,v_{n})\mid(v_{1},\ldots,v_{n+n^{\prime}+1})\in V\}=V(t_{1},\ldots,t_{n})$, and for all $(v_{1},\ldots,v_{n+n^{\prime}+1})\in V$, $(v_{1},\ldots,v_{n})=(t_{1}(j),\ldots,t_{n}(j))$ for infinitely many $j$, i.e., each of the valuations appears infinitely often in the traces. Those traces can be constructed due to Requirement 1.

Let $T_{0}=\{t_{1},\ldots,t_{n}\}$. For all $\ell\in\mathbb{N}$ we construct $T_{\ell}$ by induction on $\ell\in\mathbb{N}$, while maintaining the following two invariants:

For all $t\in T_{\ell}$ there exists $V\in S$ such that $V(t_{1},\ldots,t_{n},t)$ is equal to $\{(v_{1},\ldots,v_{n+1})\mid(v_{1},\ldots,v_{n+n^{\prime}+1})\in V\}$, and for all $(v_{1},\ldots,v_{n+n^{\prime}+1})\in V$, $(v_{1},\ldots,v_{n+1})$ is equal to $(t_{1}(j),\ldots,t_{n}(j),t(j))$ for infinitely many $j$, where the $t_{i}$ are the traces in $T_{0}$. 2. 2.

If $\ell>0$ then for every $t\in T_{\ell-1}$, there exist traces $t_{n+1},\ldots,t_{n+n^{\prime}}\in T_{\ell}$ such that $[(\tau_{i}\rightarrow t_{i})_{1\leq i\leq n+n^{\prime}},\pi\rightarrow t]\models\psi$.

By Requirement 2 and by construction, $T_{0}$ satisfies Invariant 1, and it clearly satisfies Invariant 2. Let $\ell\in\mathbb{N}$, suppose $T_{\ell}$ has been constructed, and that it satisfies Invariants 1 and 2. By Invariant 1, for all $t\in T_{\ell}$ we can construct traces $t_{n+1},\ldots,t_{n+n^{\prime}}$ such that $V(t_{1},\ldots,t_{n},t,t_{n+1},\ldots,t_{n+n^{\prime}})\in S$ and for all $(v_{1},\ldots,v_{n},v,v_{n+1},\ldots,v_{n+n^{\prime}})\in V(t_{1},\ldots,t_{n},t,t_{n+1},\ldots,t_{n+n^{\prime}})$, it is the case that $(v_{1},\ldots,v_{n},v,v_{n+1},\ldots,v_{n+n^{\prime}})$ is equal to

$(t_{1}(j),\ldots,t_{n}(j),t(j),t_{n+1}(j),\ldots,t_{n+n^{\prime}}(j))$ for infinitely many $j$ (as all the $(v_{1},\ldots,v_{n},v)$ appear infinitely many times in $(t_{1},\ldots,t_{n},t)$ by Invariant 1). Let $I(t)=\{t_{n+1},\ldots,t_{n+n^{\prime}}\}$. Let $T_{\ell+1}=\bigcup_{t\in T}I(t)$, which satisfies Invariant 1 by Requirement 2. It also satisfies Invariant 2 by definition. Furthermore, by Requirement 3, $V(t_{1},\ldots,t_{n},t,t_{n+1},\ldots,t_{n+n^{\prime}})$ satisfies $\psi$.

Finally, let $T=\bigcup_{\ell\in\mathbb{N}}T_{\ell}$ and let $t\in T$. Then, there exists an $\ell$ such that $t\in T_{\ell}$. Thus, there also exist $t_{n+1},\ldots,t_{n+n^{\prime}}\in T_{\ell+1}$ such that $[(\tau_{i}\rightarrow t_{i})_{1\leq i\leq n+n^{\prime}},\pi\rightarrow t]$ satisfies $\psi$. Therefore, $T$ satisfies $\varphi$. ∎

Recall that satisfiability of $\exists^{*}\forall^{*}$ formulas is ExpSpace-complete [8]. The proof of Finkbeiner and Hahn can be slightly adapted to produce a formula of temporal depth two: their approach states the existence of a trace representing a sequence of configurations of an exponential-space bounded Turing machine. The only difficulty that can arise in expressing the correctness of the run described by that trace is relating a position of one of the configurations to the neighbouring positions in the next configuration (in order to simulate the movement of the head). One may then require to combine an until and a next in order to express this requirement, in the scope of an always expressing that it holds for every position. This nesting can be removed by adding a fresh proposition $p$ that is satisfied on all positions of the first configuration, on none of the second one, and so on, i.e., its truth value alternates between the configurations. One can then express the previous requirement with a single until in the scope of an always, yielding temporal depth two.

Our next result shows that one obtains slightly better complexity when restricting the temporal depth of formulas to one.

Theorem 4.4

The following problem is NExpTime-complete: Given an $\exists^{*}\forall^{*}$ HyperLTL sentence $\varphi$ with temporal depth one, is $\varphi$ satisfiable?

Proof

This proof is an adaptation of the proof by Finkbeiner and Hahn showing that the problem is ExpSpace-complete for sentences of arbitrary temporal depth [8]. For the upper bound, we use the transformation of Finkbeiner and Hahn to turn the initial sentence into an equisatisfiable exponentially larger one of the form $\exists^{*}\psi^{\prime}$ without increasing the temporal depth, by replacing universal quantifiers with conjunctions. Then, we turn that sentence into an equisatisfiable LTL formula of the same size and the same temporal depth by merging traces, again due to Finkbeiner and Hahn. Finally, we apply a result of Demri and Schnoebelen stating that satisfiability of LTL formulas of temporal depth one is in NP [7]. Altogether, we obtain the desired algorithm.

For the lower bound, we again adapt ideas of Finkbeiner and Hahn. We reduce from the following NExpTime-complete problem: Given a nondeterministic Turing machine $\mathcal{M}$ and an integer $n$ (in unary), does $\mathcal{M}$ accept the empty word in time at most $2^{n}$? Given such a machine $\mathcal{M}=(Q,\Sigma,\Delta,q_{0},q_{f})$, we construct a HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$ formula $\varphi$ of the form $\exists^{*}\forall^{*}\psi$ such that $\varphi$ is satisfiable if and only if $\mathcal{M}$ accepts the empty word in less than $2^{n}$ steps. We can assume that there is a loop on the final state, i.e., the machine accepts in at most $2^{n}$ steps if and only if it accepts in exactly $2^{n}$ steps. We also assume $\Sigma$ to contain a blank letter $B$ meaning that nothing has been written at that position yet. In particular, the initial tape contains only $B$.

In our encoding of a run of $\mathcal{M}$, the valuation at some position encodes the content of one cell at one moment in time. Thus, we use the set $Q\cup\Sigma\cup\{\mathrm{spc}_{1},\ldots,\mathrm{spc}_{n}\}\cup\{\mathrm{tm}_{1},\ldots,\mathrm{tm}_{n}\}\cup\{h\}\cup\{0,1\}$ of atomic propositions, where $h$, $\mathrm{spc}_{i}$, and $\mathrm{tm}_{i}$ are fresh atomic propositions representing respectively whether the head is at the encoded cell, the position on the tape and time (the two latter in binary). For all $0\leq j<2^{n}$ let $time(j)$ and $space(j)$ be the valuations over the $\mathrm{tm}_{i}$ and $\mathrm{spc}_{i}$ representing $j$.

To encode the existence of an accepting run of $\mathcal{M}$, we require the existence of a trace $t$ encoding such a run in the following sense:

• •

Every valuation of $\mathrm{tm}_{1},\ldots,\mathrm{tm}_{k},\mathrm{spc}_{1},\ldots,\mathrm{spc}_{k}$ appears eventually on $t$.

• •

Two positions with the same valuation of the $\mathrm{tm}_{i}$ and $\mathrm{spc}_{i}$ also have the same valuation of the other atomic propositions.

• •

For all $j\in\mathbb{N}$, $t(j)$ contains exactly one letter from $\Sigma$ and one state from $Q$.

• •

There exists a run of $\mathcal{M}$ such that for all $j_{t},j_{s}$, if at the $j_{t}$-th step the machine is in state $q$ and has an $a$ at position $j_{s}$, then for all $m\in\mathbb{N}$, if $t(m)\cap\{\mathrm{tm}_{i}\mid 1\leq i\leq n\}=time(j_{t})$ and $t(m)\cap\{\mathrm{spc}_{i}\mid 1\leq i\leq n\}=space(j_{s})$ then $a,q\in t(m)$ and $h\in t(m)$ if and only if the head is at position $j_{s}$ at the $j_{t}$-th step of the run, i.e., every trace faithfully represents the content of the cell at the step of the run and the position on the tape it is assigned to.

Now, we define $\varphi$ as

[TABLE]

We explain the role of $\varphi$’s subformulas below, but leave the construction of the formulas to the reader in order to improve readability. We just remark that all can be constructed with temporal depth one.

• •

$\psi_{0/1}$ expresses that $\pi_{0}$ takes value $\{0\}^{\omega}$ and that $\pi_{1}$ takes value $\{1\}^{\omega}$.

• •

$\psi_{assign}$ ensures that all the traces assigned to the $\tau_{i},\tau^{\prime}_{i},\sigma_{i},\sigma^{\prime}_{i}$ are equal to either the trace assigned to $\pi_{0}$ or the one assigned to $\pi_{1}$. The values of those traces represent two valuations of the $\mathrm{tm}_{i}$ ($\tau_{i}$ and $\tau^{\prime}_{i}$) and two of the $\mathrm{spc}_{i}$ ($\sigma_{i}$ and $\sigma^{\prime}_{i}$).

• •

$\psi_{halt}$ ensures that there exists a position in the trace assigned to $\pi$ containing $q_{f}$.

• •

$\psi_{init}$ ensures that all the positions having the $\mathrm{tm}_{i}$ representing [math] contain a $B$ and a $q_{0}$, and that positions having the $\mathrm{tm}_{i}$ and $\mathrm{spc}_{i}$ representing [math] contain an $h$, i.e., the initial configuration is encoded correctly.

• •

$\psi_{cons}$ checks that all positions of the trace assigned to $\pi$ in which the valuation of the time and space propositions is the one represented by the traces assigned to the $\tau_{i}$ and $\sigma_{i}$ have the same valuation over the other variables. It also checks that there is exactly one letter and one state at each position of the trace assigned to $\pi$, and that if two positions in the trace assigned to $\pi$ have the same time valuations (represented by the trace assigned to $\tau_{i}$) but not the same space valuations, then at most one of the two satisfies the head proposition $h$, and they have the same state.

• •

$\psi_{complete}$ expresses that there exists a position in $\pi$ matching the $\mathrm{tm}_{i}$ and $\mathrm{spc}_{i}$ with the $\tau_{i}$ and $\sigma_{i}$, i.e., that the complete computation tableau is encoded.

• •

$\psi_{trans}(q,q^{\prime},a,a^{\prime},d)$ checks that the position of the head, the state and the change in the letters are consistent with that transition. For instance, if the $\sigma_{i}$ and $\sigma_{i}^{\prime}$ represent the same valuation and the $\tau^{\prime}_{i}$ represent the successor of the $\tau_{i}$ and the positions in $\pi$ matching the $\tau_{i}$ and $\sigma_{i}$ contain $h$, then $\psi_{trans}$ ensures that the positions matching $\tau_{i}$ and $\sigma_{i}$ contain $a$ and $q$ and the ones matching $\tau^{\prime}_{i}$ and $\sigma^{\prime}_{i}$ contain $a^{\prime}$ and $q^{\prime}$.

One can then see that this formula is satisfiable if and only if $\mathcal{M}$ accepts in time at most $2^{n}$, as it explicitly describes the existence of an accepting run of $\mathcal{M}$. ∎

We conclude by considering the satisfiability problem for HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$ with arbitrary quantifier prefixes, but restricted to models induced by finite-state systems. The undecidability of satisfiability for arbitrary formulas over finite-state systems can be easily inferred from the proof of undecidability of satisfiability of Finkbeiner and Hahn, as the formulas they construct, if satisfiable, have a finite and ultimately periodic model, which is therefore representable by a finite-state system. For formulas of HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$, we leave decidability open, but prove intractability.

Theorem 4.5

The following problem is Tower-hard: Given a HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$ sentence $\varphi$, does $\varphi$ have a model $T({\mathcal{K}})$ for some Kripke structure ${\mathcal{K}}$?

Proof

Let $\mathcal{M}$ be a deterministic Turing machine $(Q,\Sigma,\delta,q_{0},q_{f})$, let $w\in\Sigma^{*}$, and let $n=|w|$. We construct a sentence $\varphi$ that is satisfiable by a Kripke structure if and only if $\mathcal{M}$ accepts $w$ in time $\mathrm{twr}(n)$, where $\mathrm{twr}(0)=2$ and $\mathrm{twr}(k+1)=2^{\mathrm{twr}(k)}$ for all $k\in\mathbb{N}$. This problem can easily be shown Tower-complete under elementary reductions.

To this end, we use the set

[TABLE]

of propositions. There are two types of traces: Type one traces, marked by the atomic proposition $1$, allow us to count up to $\mathrm{twr}(n)$, while type two traces simulate an accepting run of $\mathcal{M}$ on $w$. Each type two trace encodes one cell of the tape of $\mathcal{M}$ at one step of the computation. We use the formula $\psi_{type}=\forall\pi.1_{\pi}\oplus 2_{\pi}$ to ensure that the traces are split between the two types.

Each type one trace is assigned a rank between [math] and $n$, which is indicated by the propositions $\mathrm{rk}_{0},\ldots,\mathrm{rk}_{n}$. A trace of rank $r+1$ encodes a set of traces of rank $r$. There are two traces of rank zero, which represent zero and one. Thus, we are able to generate $\mathrm{twr}(r)$ traces of rank $r$ for all $0\leq r\leq n$. For instance, at rank one we have four traces, representing all possible subsets of the two rank zero traces.

Then, we construct an order on those traces and use traces of rank $n$ to simulate the Turing machine. More precisely, each trace of type two is associated to two traces of type one, one for space and one for time, which encode its position on the tape and the step of the computation it describes.

We require that for all type one traces $t$ there is exactly one $r$ such that $\mathrm{rk}_{r}\in t(0)$, and we then say that $t$ is of rank $r$. If $t$ is of rank zero then it is either $t_{0}=\{1,r_{0},0\}^{\omega}$ or $t_{1}=\{1,r_{0}\}^{\omega}$. These properties can easily be expressed in HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$.

A type one trace $t$ of rank $r+1$ is said to contain a type one trace $t^{\prime}$ of rank $r$ (denoted by $t^{\prime}\in t$) if and only if there exists $j\in\mathbb{N}$ such that $in\in t^{\prime}(j)$ and $ni\in t(j)$. To every trace $t$ of rank $r$ we associate a set $S(t)$, which is an element of the set obtained by iterating the power set operator on $\{\{0\},\{1\}\}$ $r$ times:

• •

$S(t_{0})=\{0\}$ and $S(t_{1})=\{1\}$.

• •

Else, $S(t)=\{S(t^{\prime})\mid t^{\prime}\in t\}$.

The following formula is satisfied by $[\pi\rightarrow t,\pi^{\prime}\rightarrow t^{\prime}]$ if and only if $t\in t^{\prime}$:

[TABLE]

Furthermore, we define a strict order $<$ over traces of equal rank: $t_{0}<t_{1}$ for the only two traces $t_{0},t_{1}$ of rank [math], and for all traces $t,t^{\prime}$ of rank $r+1$, $t<t^{\prime}$ if and only if there exists $t^{\prime\prime}$ of rank $r$ such that $S(t^{\prime\prime})\in S(t^{\prime})\setminus S(t)$ and for all $t^{*}$ of rank $r$ such that $t^{\prime\prime}<t^{*}$, $S(t^{*})\in S(t)$ if and only if $S(t^{*})\in S(t^{\prime})$. This is defined by analogy with the comparison of two numbers based on their binary representations (assumed to be of the same size). One is larger than the other if there is a position at which it has a $1$, the other has a [math], and they are equal on every bit of higher weight. Using this intuition, one can indeed show that $<$ is a strict order.

To express the order $<$ in HyperLTL, we use atomic propositions $lt$ and $gt$ and the following formula to ensure that for all traces $t,t^{\prime}$ in the model, $t<t^{\prime}$ if and only if there exists $j\in\mathbb{N}$ such that $lt\in t(j)$ and $gt\in t^{\prime}(j)$:

[TABLE]

where $\psi_{0,1}$ expresses that the value taken by $\pi$ is $t_{0}$ and the one taken by $\pi^{\prime}$ is $t_{1}$, $\psi_{equalrank}$ expresses that the values of $\pi$ and $\pi^{\prime}$ have the same rank, and

[TABLE]

We also require that two traces $t,t^{\prime}$ of equal rank but incomparable for $<$ (i.e. $S(t)=S(t^{\prime})$) must be equal. This is expressed by the formula

[TABLE]

We then define a successor relation $sc$ on traces of equal rank. We have $sc(t_{0},t_{1})$ and not $sc(t_{1},t_{0})$, $sc(t_{1},t_{1})$, or $sc(t_{1},t_{1})$. For all traces $t,t^{\prime}$ of rank $r>0$, $sc(t,t^{\prime})$ expresses that there exists a trace $t^{\prime\prime}$ of rank $r-1$ such that, $S(t^{\prime\prime})\in S(t^{\prime})\setminus S(t)$ and for all $t^{*}<t^{\prime\prime}$, $S(t^{*})\in S(t)\setminus S(t^{\prime})$. Intuitively, this is analogous to the definition of the successor in binary: In order to add one to a binary number, one has to find the bit of least weight such that this bit is [math] and all the bits of lower weights are $1$. Then one has to turn this bit to one and all the lower ones to [math]. The following formula is satisfied by $[\pi\rightarrow t,\pi^{\prime}\rightarrow t^{\prime}]$ if and only if $sc(t,t^{\prime})$ holds:

[TABLE]

We then ensure that all possible $S(t)$ are generated: We state the existence of a trace $t_{0}^{r}$ for each $1\leq r\leq n$ such that for all $j\in\mathbb{N}$, $ni\notin t_{0}^{r}(j)$. The trace $t_{0}^{r}$ represents the empty set at rank $r$. The following formula expresses the existence of those traces:

[TABLE]

We also state that for all $r$ and for all traces $t$ of rank $r$, if $t$ is not maximal for $<$ (i.e., if it does not contain every trace of rank $r-1$), then there exists a trace $t^{\prime}$ such that $sc(t,t^{\prime})$:

[TABLE]

where

[TABLE]

As a result, we have ensured that all the $S(t)$ were generated. In particular, we have $\mathrm{twr}(n)$ traces of rank $n$, and we have a successor relation $sc$. We can use these traces as a counter from [math] to $\mathrm{twr}(n)-1$.

Finally, for convenience, we ensure that $S$ is injective, i.e., for all traces $t,t^{\prime}$ of type one, if $S(t)=S(t^{\prime})$ (i.e., if $t$ and $t^{\prime}$ have the same rank but are incomparable for $<$) then $t=t^{\prime}$. The following formula expresses it:

[TABLE]

We associate to every pair $(t,t^{\prime})$ of traces of type one and rank $n$ ($t$ for time and $t^{\prime}$ for space) a unique type two trace representing the content of the tape at the position represented by $t_{s}$ at the time represented by $t_{t}$. We use the atomic propositions ${m_{t}}$ and ${m_{s}}$ to encode this relation. The following formulas express it:

[TABLE]

expresses that to each pair $(t,t^{\prime})$ of rank $n$ traces we associate a type two trace as explained above, and

[TABLE]

expresses that this type two trace is unique.

We can now define a formula $\psi_{sametime}(\tau,\tau^{\prime})$ satisfied in the model by $[\tau\rightarrow t,\tau^{\prime}\rightarrow t^{\prime}]$ if and only if $t$ and $t^{\prime}$ are of type two and are associated to the same step of the computation:

[TABLE]

We also define a formula $\psi_{nexttime}(\tau,\tau^{\prime})$ satisfied in the model by $[\tau\rightarrow t,\tau^{\prime}\rightarrow t^{\prime}]$ if and only if $t$ and $t^{\prime}$ are of type two and the time associated to $t^{\prime}$ is the successor of the time associated to $t$:

[TABLE]

We define $\psi_{nextspace}$ similarly.

With these formulas at hand, we can now simulate the run of $\mathcal{M}$: The consistency and the transitions of the machine can easily be implemented using the $sc$ and $<$ relations. For instance, the following formula expresses that if at some step of the run the head does not point to a position, then the letter at that position should not change between this step and the next one:

[TABLE]

If the final formula has a model, then $\mathcal{M}$ accepts $w$ , and then we can construct a model satisfying the formula which is finite (as there are finitely many type one and type two traces) and in which all traces are ultimately periodic (as there are finitely many of them, we only need finitely many positions to encode all the relations). Thus, this model can be represented by a Kripke structure of nonelementary size.

Conversely, if the formula has a model represented by a Kripke structure, then in particular it is satisfiable. Thus, $\mathcal{M}$ accepts $w$ (one can construct an accepting run of $\mathcal{M}$ from a model of the formula).

Furthermore, even though the construction described in this proof may yield formulas of alternation depth greater than one, we can reduce the depth to one using Lemma 2: If the final formula has a model, then it has a finite and ultimately periodic one. The construction of Lemma 2 encodes a finite number of new relations over the traces. Hence, the resulting $\forall^{*}\exists^{*}$ formula also has a finite and ultimately periodic model, which is therefore also the set of traces of a Kripke structure. ∎

Let us conclude by remarking that the satisfiability problem for HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$ over Kripke structures is different from the general one, i.e., there are satisfiable formulas which are not satisfied by the set of traces of any Kripke structure. Consider for instance the sentence $\forall\pi.\exists\pi^{\prime}.{\mathbf{G\,}}(a_{\pi}\Rightarrow a_{\pi^{\prime}})\land{\mathbf{F\,}}(\neg a_{\pi}\land a_{\pi^{\prime}})$. It is satisfied by $\{a\}^{*}\emptyset^{\omega}$.

Suppose there exists a Kripke structure ${\mathcal{K}}$ with a set of traces satisfying this sentence. We define inductively an increasing sequence of finite trace prefixes $p_{n}$ for $n\in\mathbb{N}$ as $p_{0}=\varepsilon$ and $p_{n+1}=p_{n}\{a\}$ if $p_{n}\{a\}$ is a prefix of a trace of ${\mathcal{K}}$, and $p_{n+1}=p_{n}\emptyset$ otherwise. As the set of traces of a Kripke structure is closed, the limit $t$ of this sequence is a trace of ${\mathcal{K}}$. As ${\mathcal{K}}$ satisfies the sentence, there exists $t^{\prime}$ such that for all $j$ if $a\in t(j)$ then $a\in t^{\prime}(j)$ and there exists $j^{*}$ such that $a\in t^{\prime}(j^{*})$ and $a\notin t(j^{*})$. In particular, there exists a minimal such $j^{*}$. Then $p_{j^{*}+1}=p_{j^{*}}\emptyset$, but $p_{j^{*}}\{a\}$ is a prefix of $t^{\prime}$, thereby contradicting the choice of $p_{j^{*}+1}$, as we prefer to extend by $\{a\}$ instead of $\emptyset$. Thus, this satisfiable sentence is not satisfiable by the set of traces of a finite Kripke structure.

5 Conclusion

We have shown that HyperLTL satisfiability can be decidable, either if one restricts the space of models one is interested in to sufficiently simple ones, or if one restricts the alternation and temporal depth of the formulas under consideration. In particular, we have investigated the formulas of temporal depth one without untils. An interesting open problem is to extend the decidability result presented in Theorem 4.3 to formulas with untils. Also, we claimed no lower bound on the problem solved in Theorem 4.3. We claim there is an ExpSpace lower bound obtained by encoding exponential space Turing machines, but the exact complexity of the problem is left open. Another interesting problem left open is the decidability of HyperLTL${}^{1}(\mathbf{F},\mathbf{G})$ over Kripke structures. We have presented a Tower lower bound in Theorem 4.5, but it is open whether the problem is indeed decidable.

In general, restricting the space of models turns out to be more fruitful than to restrict the formulas under consideration, as satisfiability is undecidable for extremely simple formulas (simplicity being measured in alternation depth and temporal depth). An interesting challenge pertains to finding other measures of simplicity that yield larger decidable fragments.