# The Complexity of Second-order HyperLTL

Martin Zimmermann (Aalborg University, Aalborg, Denmark)

###### Abstract

We determine the complexity of second-order HyperLTL satisfiability and model-
checking: Both are as hard as truth in third-order arithmetic.

##  1 Introduction

The introduction of hyperlogics [2] for the specification and verification of
hyperproperties [3], properties that relate multiple system executions, has
been one of the major success stories of formal verification during the last
decade. Logics like HyperLTL, the extension of LTL with trace quantification,
and HyperCTL∗, the extension of CTL∗ with trace quantification, are natural
specification languages for information-flow properties, have a decidable
model-checking problem [5], and hence found many applications.

However, while expressive enough to express common information-flow
properties, they are unable to express other important hyperproperties, e.g.,
common knowledge in multi-agent systems and asynchronous properties (witnessed
by a plethora of asynchronous extensions of HyperLTL). These examples all have
in common that they are _second-order_ properties, i.e., they naturally
require quantification over sets of traces while HyperLTL only allows
quantification over traces.

In light of this situation, Beutner et al. [1] introduced Hyper2LTL, HyperLTL
extended with second-order quantification of traces. They show that the logic
is indeed able to capture common knowledge, asynchronous extensions of
HyperLTL, and many other applications. However, they also note that this
expressiveness comes at a steep price: model-checking Hyper2LTL is highly
undecidable, i.e., $\Sigma_{1}^{1}$-hard. Thus, their main result is a partial
model-checking algorithm for a fragment of Hyper2LTL where second-order
quantification is replaced by inflationary (deflationary) fixedpoints of
HyperLTL definable operators. The algorithm over- and underapproximates these
fixedpoints and then invokes a HyperLTL model-checking algorithm on these
approximations. A prototype implementation of the algorithm is able to model-
check properties capturing common knowledge, asynchronous hyperproperties, and
distributed computing.

However, one question has been left open: Just how complex is Hyper2LTL
verification?

#### Complexity Classes for Undecidable Problems

The complexity of undecidable problems is typically captured in terms of the
arithmetical and analytical hierarchy, where decision problems (encoded as
subsets of $\mathbb{N}$) are classified based on their definability by
formulas of higher-order arithmetic, namely by the type of objects one can
quantify over and by the number of alternations of such quantifiers. We refer
to Roger’s textbook [9] for fully formal definitions and refer to Figure 1 for
a visualization. We recall the following classes: $\Sigma_{1}^{0}$ contains
the sets of natural numbers of the form

$\\{x\in\mathbb{N}\mid\exists x_{0}.\ \cdots\exists x_{k}.\
\psi(x,x_{0},\ldots,x_{k})\\}$

where quantifiers range over natural numbers and $\psi$ is a quantifier-free
arithmetic formula. Note that this is exactly the class of recursively
enumerable sets. The notation $\Sigma_{1}^{0}$ signifies that there is a
single block of existential quantifiers (the subscript $1$) ranging over
natural numbers (type $0$ objects, explaining the superscript $0$).
Analogously, $\Sigma_{1}^{1}$ is induced by arithmetic formulas with
existential quantification of type $1$ objects (sets of natural numbers) and
arbitrary (universal and existential) quantification of type $0$ objects. So,
$\Sigma_{1}^{0}$ is part of the first level of the arithmetical hierarchy
while $\Sigma_{1}^{1}$ is part of the first level of the analytical hierarchy.
In general, level $\Sigma_{n}^{0}$ (level $\Pi_{n}^{0}$) of the arithmetical
hierarchy is induced by formulas with at most $n$ alternations between
existential and universal type $0$ quantifiers, starting with an existential
(universal) quantifier. Similar hierarchies can be defined for arithmetic of
any fixed order by limiting the alternations of the highest-order quantifiers
and allowing arbitrary lower-order quantification. In this work, the highest
order we are concerned with is three, i.e., quantification over sets of sets
of natural numbers.

HyperLTL satisfiability is $\Sigma_{1}^{1}$-complete [7], HyperLTL finite-
state satisfiability is $\Sigma_{1}^{0}$-complete [4], and, as mentioned
above, Hyper2LTL model-checking is $\Sigma_{1}^{1}$-hard [1], but no upper
bounds are known.

$\cdots$$\Sigma^{0}_{0}$$=$$\Pi^{0}_{0}$$\Sigma^{0}_{1}$$\Pi^{0}_{1}$$\Sigma^{0}_{2}$$\Pi^{0}_{2}$$\Sigma^{0}_{2}$$\Pi^{0}_{2}$$\cdots$$\cdots$$\Sigma^{1}_{0}$$=$$\Pi^{1}_{0}$$\Sigma^{1}_{1}$$\Pi^{1}_{1}$$\Sigma^{1}_{2}$$\Pi^{1}_{2}$$\Sigma^{1}_{2}$$\Pi^{1}_{2}$$\cdots$$\cdots$$\Sigma^{2}_{0}$$=$$\Pi^{2}_{0}$$\Sigma^{2}_{1}$$\Pi^{2}_{1}$$\Sigma^{2}_{2}$$\Pi^{2}_{2}$$\Sigma^{2}_{2}$$\Pi^{2}_{2}$$\cdots$$\cdots$DecidableUndecidableRecursivelyenumerable
arithmetical hierarchy $\equiv$ first-order arithmetic analytical hierarchy
$\equiv$ second-order arithmetic analytical hierarchy $\equiv$ third-order
arithmetic

Figure 1: The arithmetical hierarchy, the analytical hierarchy, and beyond.

Another yardstick is truth for order $k$ arithmetic, i.e., the question
whether a given sentence of order $k$ arithmetic evaluates to true. In the
following, we are in particular interested in the case $k=3$, i.e., we
consider formulas with arbitrary quantification over type $0$ objects, type
$1$ objects, and type $2$ objects (sets of sets of natural numbers). Note that
these formulas span the whole third hierarchy, as we allow arbitrary nesting
of existential and universal third-order quantification.

#### Our Contribution

In this work, we determine the exact complexity of Hyper2LTL satisfiability
and model-checking, as well as some variants of satisfiability.

An important stepping stone is the investigation of the cardinality of models
of Hyper2LTL. It is known that every satisfiable HyperLTL sentence has a
countable model, and that some have no finite models [6]. This restricts the
order of arithmetic that can be simulated in HyperLTL and explains in
particular the $\Sigma_{1}^{1}$-completeness of HyperLTL satisfiability [7].
We show that (unsurprisingly) second-order quantification allows to write
formulas that only have uncountable models by generalizing the lower bound
construction of HyperLTL to Hyper2LTL. Note that the cardinality of the
continuum is a trivial upper bound on the size of models, as they are sets of
traces.

With this tool at hand, we are able to show that Hyper2LTL satisfiability is
as hard as truth in third-order arithmetic, i.e., much harder than HyperLTL
satisfiability. This in itself is not surprising, as second-order
quantification is expected to increase the complexity considerably. But what
might be surprising is that the problem is not $\Sigma_{1}^{2}$-complete,
i.e., at the same position of the third hierarchy that HyperLTL satisfiability
occupies in one full hierarchy below (see Figure 1).

Furthermore, we also show that Hyper2LTL finite-state satisfiability is as
hard as truth in third-order arithmetic, and therefore as hard as general
satisfiability. This should be contrasted with the situation for HyperLTL
described above, where finite-state satisfiability is
$\Sigma_{1}^{0}$-complete (i.e., recursively enumerable) and thus much simpler
than general satisfiability, which is $\Sigma_{1}^{1}$-complete.

Finally, our techniques for Hyper2LTL satisfiability also shed light on the
complexity of Hyper2LTL model-checking, which we show to be as hard as truth
in third-order arithmetic as well, i.e., all three problems we consider have
the same complexity. Again, this has be contrasted with the situation for
HyperLTL, where model-checking is decidable, albeit Tower-complete.

One could rightfully expect that quantification over arbitrary sets of traces
is the culprit behind the formidable complexity of Hyper2LTL. In fact, Beutner
et al. noticed that many of the applications of Hyper2LTL described above only
require limited forms of set quantification. However, we show that two natural
fragments of Hyper2LTL obtained by restricting the range of second-order
quantifiers do retain the same complexity for all three decision problems.

Table 1 lists our results and compares them to the corresponding results for
LTL and HyperLTL.

Table 1: List of our results (in gray) and comparison to other logics. “T3OA-complete” stands for “as hard as truth in third-order arithmetic”. | satisfiability | finite-state satisfiability | model-checking
---|---|---|---
LTL |  PSpace-complete |  PSpace-complete |  PSpace-complete
HyperLTL |  $\Sigma_{1}^{1}$-complete |  $\Sigma_{1}^{0}$-complete |  Tower-complete
Hyper2LTL | T3OA-complete | T3OA-complete | T3OA-complete

##  2 Preliminaries

We denote the nonnegative integers by $\mathbb{N}$. An alphabet is a nonempty
finite set. The set of infinite words over an alphabet $\Sigma$ is denoted by
$\Sigma^{\omega}$. Throughout this paper, we fix a finite set $\mathrm{AP}$ of
atomic propositions. A trace over $\mathrm{AP}$ is an infinite word over the
alphabet $2^{\mathrm{AP}}$. Given $\mathrm{AP}^{\prime}\subseteq\mathrm{AP}$,
the $\mathrm{AP}^{\prime}$-projection of a trace $t(0)t(1)t(2)\cdots$ over
$\mathrm{AP}$ 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 transition system $\mathfrak{T}=(V,E,I,\lambda)$ consists of a finite set
$V$ of vertices, a set $E\subseteq V\times V$ of (directed) edges, a set
$I\subseteq V$ of initial vertices, and a labeling $\lambda\colon V\rightarrow
2^{\mathrm{AP}}$ of the vertices by sets of atomic propositions. We assume
that every vertex has at least one outgoing edge. A path $\rho$ through
$\mathfrak{T}$ is an infinite sequence $\rho(0)\rho(1)\rho(2)\cdots$ of
vertices with $\rho(0)\in I$ and $(\rho(n),\rho(n+1))\in E$ for every $n\geq
0$. The trace of $\rho$ is defined as
$\lambda(\rho)=\lambda(\rho(0))\lambda(\rho(1))\lambda(\rho(2))\cdots$. The
set of traces of $\mathfrak{T}$ is
$\mathrm{Tr}(\mathfrak{T})=\\{\lambda(\rho)\mid\rho\text{ is a path through
$\mathfrak{T}$}\\}$.

###  2.1 Hyper2LTL

Let $\mathcal{V}_{1}$ be a set of first-order trace variables (i.e., ranging
over traces) and $\mathcal{V}_{2}$ be a set of second-order trace variables
(i.e., ranging over sets of traces) such that
$\mathcal{V}_{1}\cap\mathcal{V}_{2}=\emptyset$. We typically use $\pi$
(possibly with decorations) to denote first-order variables and $X$ (possibly
with decorations) to denote second-order variables. Also, we assume the
existence of two distinguished second-order variables $X_{a}$ and $X_{d}$ that
refer to the set $(2^{\mathrm{AP}})^{\omega}$ of all traces and the universe
of discourse (a fixed set of traces, often that of a given transition system
over which the formula is evaluated, e.g., in model-checking), respectively.

Then, the formulas of Hyper2LTL are given by the grammar

$\displaystyle\varphi{}$ $\displaystyle\mathop{::=}{}\exists X.\
\varphi\mid\forall X.\ \varphi\mid\exists\pi\in X.\ \varphi\mid\forall\pi\in
X.\ \varphi\mid\psi$ $\displaystyle\psi{}$
$\displaystyle\mathop{::=}{}\texttt{p}_{\pi}\mid\neg\psi\mid\psi\vee\psi\mid\mathop{\mathbf{X}\vphantom{a}}\nolimits\psi\mid\psi\operatorname{\mathbf{U}}\psi$

where p ranges over $\mathrm{AP}$, $\pi$ ranges over $\mathcal{V}_{1}$, and
$X$ ranges over $\mathcal{V}_{2}$. Conjunction, implication, and equivalence
are defined as usual, and the temporal operators eventually
$\mathop{\mathbf{F}\vphantom{a}}\nolimits$ and always
$\mathop{\mathbf{G}\vphantom{a}}\nolimits$ are derived as
$\mathop{\mathbf{F}\vphantom{a}}\nolimits\psi=\neg\psi\operatorname{\mathbf{U}}\psi$
and
$\mathop{\mathbf{G}\vphantom{a}}\nolimits\psi=\neg\mathop{\mathbf{F}\vphantom{a}}\nolimits\neg\psi$.
A _sentence_ is a formula without free (first- and second-order) variables,
which are defined as usual. We measure the size of a formula by its number of
distinct subformulas.

The semantics of Hyper2LTL is defined with respect to a _variable assignment_
, a partial mapping
$\Pi\colon\mathcal{V}_{1}\cup\mathcal{V}_{2}\rightarrow(2^{\mathrm{AP}})^{\omega}\cup
2^{(2^{\mathrm{AP}})^{\omega}}$ such that

  * •

if $\Pi(\pi)$ for $\pi\in\mathcal{V}_{1}$ is defined, then
$\Pi(\pi)\in(2^{\mathrm{AP}})^{\omega}$ and

  * •

if $\Pi(X)$ for $X\in\mathcal{V}_{2}$ is defined, then $\Pi(X)\in
2^{(2^{\mathrm{AP}})^{\omega}}$.

Given a variable assignment $\Pi$, a variable $\pi\in\mathcal{V}_{1}$, and a
trace $t$, we denote by $\Pi[\pi\mapsto t]$ the assignment that coincides with
$\Pi$ everywhere but at $\pi$, which is mapped to $t$. Similarly, given a
variable assignment $\Pi$, a variable $X\in\mathcal{V}_{2}$, and a set $T$ of
traces we denote by $\Pi[X\mapsto T]$ the assignment that coincides with $\Pi$
everywhere but at $X$, which is mapped to $T$. Furthermore, $\Pi[j,\infty)$
denotes the variable assignment mapping every $\pi\in\mathcal{V}_{1}$ in
$\Pi$’s domain to $\Pi(\pi)(j)\Pi(\pi)(j+1)\Pi(\pi)(j+2)\cdots$, the suffix of
$\Pi(\pi)$ starting at position $j$ (note that the assignment of variables
$X\in\mathcal{V}_{2}$ is not updated, as this is not necessary for our
application).

For a variable assignment $\Pi$ we define

  * •

$\Pi\models\texttt{p}_{\pi}$ if $\texttt{p}\in\Pi(\pi)(0)$,

  * •

$\Pi\models\neg\psi$ if $\Pi\not\models\psi$,

  * •

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

  * •

$\Pi\models\mathop{\mathbf{X}\vphantom{a}}\nolimits\psi$ if
$\Pi[1,\infty)\models\psi$,

  * •

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

  * •

$\Pi\models\exists\pi\in X.\ \varphi$ if there exists a trace $t\in\Pi(X)$
such that $\Pi[\pi\mapsto t]\models\varphi$,

  * •

$\Pi\models\forall\pi\in X.\ \varphi$ if for all traces $t\in\Pi(X)$ we have
$\Pi[\pi\mapsto t]\models\varphi$,

  * •

$\Pi\models\exists X.\ \varphi$ if there exists a set
$T\subseteq(2^{\mathrm{AP}})^{\omega}$ such that $\Pi[X\mapsto
T]\models\varphi$, and

  * •

$\Pi\models\forall X.\ \varphi$ if for all sets
$T\subseteq(2^{\mathrm{AP}})^{\omega}$ we have $\Pi[X\mapsto
T]\models\varphi$.

The variable assignment with empty domain is denoted by $\Pi_{\emptyset}$. We
say that a set $T$ of traces satisfies a Hyper2LTL sentence $\varphi$, written
$T\models\varphi$, if
$\Pi_{\emptyset}[X_{a}\mapsto(2^{\mathrm{AP}})^{\omega},X_{d}\mapsto
T]\models\varphi$, i.e., if we assign the set of all traces to $X_{a}$ and the
set $T$ to the universe of discourse $X_{d}$. In this case, we say that $T$ is
a model of $\varphi$. A transition system $\mathfrak{T}$ satisfies $\varphi$,
written $\mathfrak{T}\models\varphi$, if
$\mathrm{Tr}(\mathfrak{T})\models\varphi$. Slightly sloppily, we again say
that $\mathfrak{T}$ satisfies $\varphi$ in this case. Although Hyper2LTL
sentences are required to be in prenex normal form, they are closed under
Boolean combinations, which can easily be seen by transforming such a formula
into an equivalent formula in prenex normal form. Thus, in examples and proofs
we will often use Boolean combinations of Hyper2LTL formulas.

######  Remark 1.

HyperLTL is the fragment of Hyper2LTL obtained by disallowing second-order
quantification and only allowing first-order quantification of the form
$\exists\pi\in X_{d}$ and $\forall\pi\in X_{d}$, i.e., one can only quantify
over traces from the universe of discourse. Hence, we typically simplify our
notation to $\exists\pi$ and $\forall\pi$ in HyperLTL formulas.

To conclude, we highlight that second-order quantification in Hyper2LTL ranges
over arbitrary sets of traces (not necessarily from the universe of discourse)
and that first-order quantification ranges over elements in such sets, i.e.,
(possibly) again over arbitrary traces. To disallow this, we introduce
_closed-world_ semantics for Hyper2LTL. Here, we only consider formulas that
do not use the variable $X_{a}$ and change the semantics of the set
quantifiers as follows:

  * •

$\Pi\models\exists X.\ \varphi$ if there exists a set $T\subseteq\Pi(X_{d})$
such that $\Pi[X\mapsto T]\models\varphi$, and

  * •

$\Pi\models\forall X.\ \varphi$ if for all sets $T\subseteq\Pi(X_{d})$ we have
$\Pi[X\mapsto T]\models\varphi$.

We say that $T\subseteq(2^{\mathrm{AP}})^{\omega}$ satisfies $\varphi$ under
closed-world semantics, if $\Pi_{\emptyset}[X_{d}\mapsto T]\models\varphi$.
Hence, under closed-world semantics, second-order quantifiers only range over
subsets of the universe of discourse. Consequently, first-order quantifiers
also range over traces from the universe of discourse.

######  Lemma 1.

Every Hyper2LTL formula $\varphi$ can in polynomial time be translated into a
Hyper2LTL formula $\varphi^{\prime}$ such that for all sets $T$ of traces we
have $T\models\varphi$ under closed-world semantics if and only if
$T\models\varphi^{\prime}$ (under standard semantics).

###### Proof.

Second-order quantification over subsets of the universe of discourse can
easily be mimicked by guarding classical quantifiers ranging over arbitrary
sets. Here, we rely on the formula $\forall\pi\in X.\ \exists\pi^{\prime}\in
X_{d}.\
\mathop{\mathbf{G}\vphantom{a}}\nolimits\bigwedge_{\texttt{p}\in\mathrm{AP}}\texttt{p}_{\pi}\leftrightarrow\texttt{p}_{\pi^{\prime}}$,
which expresses that every trace in $X$ is also in $X_{d}$.

Now, given a Hyper2LTL sentence $\varphi$, let $\varphi^{\prime}$ be the
Hyper2LTL sentence obtained by recursively replacing

  * •

each existential second-order quantifier $\exists X.\ \psi$ in $\varphi$ by
$\exists X.\ (\forall\pi\in X.\ \exists\pi^{\prime}\in X_{d}.\
\mathop{\mathbf{G}\vphantom{a}}\nolimits\bigwedge_{\texttt{p}\in\mathrm{AP}}\texttt{p}_{\pi}\leftrightarrow\texttt{p}_{\pi^{\prime}})\wedge\psi$
and

  * •

each universal second-order quantifier $\forall X.\ \psi$ in $\varphi$ by
$\forall X.\ (\forall\pi\in X.\ \exists\pi^{\prime}\in X_{d}.\
\mathop{\mathbf{G}\vphantom{a}}\nolimits\bigwedge_{\texttt{p}\in\mathrm{AP}}\texttt{p}_{\pi}\leftrightarrow\texttt{p}_{\pi^{\prime}})\rightarrow\psi$,

and then bringing the resulting sentence into prenex normal form, which can be
done as no quantifier is under the scope of a temporal operator. ∎

Thus, all complexity upper bounds for standard semantics also hold for closed-
world semantics and all lower bounds for closed-world semantics also hold for
standard semantics.

###  2.2 Arithmetic

We consider formulas of arithmetic, i.e., predicate logic with signature
$(+,\cdot,<,\in)$, evaluated over the structure $(\mathbb{N},+,\cdot,<,\in)$.
A type $0$ object is a natural number $n\in\mathbb{N}$, a type $1$ object is a
subset of $\mathbb{N}$, and a type $2$ object is a set of subsets of
$\mathbb{N}$. Our benchmark is third-order arithmetic, i.e., predicate logic
with quantification over type $0$, type $1$, and type $2$ objects. In the
following, we use lower-case roman letters (possibly with decorations) for
first-order variables, upper-case roman letters (possibly with decorations)
for second-order variables, and upper-case calligraphic roman letters
(possibly with decorations) for third-order variables. Note that every fixed
natural number is definable in first-order arithmetic, so we freely us them as
syntactic sugar.

Truth of third-order arithmetic is the following decision problem: given a
sentence $\varphi$ of third-order arithmetic, does
$(\mathbb{N},+,\cdot,<,\in)$ satisfy $\varphi$?

##  3 The Cardinality of Hyper2LTL Models

A Hyper2LTL sentence is satisfiable if it has a model. In this section, we
investigate the cardinality of models of satisfiable Hyper2LTL sentences. We
begin by stating a (trivial) upper bound, which follows from the fact that
models are sets of traces. Here, $\mathfrak{c}$ denotes the cardinality of the
continuum (equivalently, the cardinality of $(2^{\mathrm{AP}})^{\omega}$ for
every finite $\mathrm{AP}$).

######  Proposition 1.

Every satisfiable Hyper2LTL sentence has a model of cardinality
$\mathfrak{c}$.

Next, we show that this trivial upper bound is tight.

######  Remark 2.

There is a very simple, albeit equally unsatisfactory, way to obtain the
desired lower bound: Consider $\forall\pi\in X_{a}.\ \exists\pi^{\prime}\in
X_{d}.\
\mathop{\mathbf{G}\vphantom{a}}\nolimits\bigwedge_{\texttt{p}\in\mathrm{AP}}\texttt{p}_{\pi}\leftrightarrow\texttt{p}_{\pi^{\prime}}$
expressing that every trace in the set of all traces is also in the universe
of discourse, i.e., $(2^{\mathrm{AP}})^{\omega}$ is its only model. However,
this crucially relies on the fact that $X_{a}$ is, by definition, interpreted
as the set of all traces. In fact the formula does not even use second-order
quantification.

In the following, we construct a sentence that has only uncountable models,
and which retains that property under closed-world semantics (which in
particular means it cannot use $X_{a}$). This should be compared with
HyperLTL, where every satisfiable sentence has a countable model [6].
Unsurprisingly, the addition of (even restricted) second-order quantification
increases the cardinality of minimal models, even without cheating.

######  Example 1.

We begin by recalling a construction of Finkbeiner and Zimmermann giving a
satisfiable HyperLTL sentence $\psi$ that has no finite models [6]. The
sentence intuitively posits the existence of a unique trace for every natural
number $n$. Our lower bound for Hyper2LTL builds upon that construction.

Fix $\mathrm{AP}=\\{\texttt{x}\\}$ and consider the conjunction
$\psi=\psi_{1}\wedge\psi_{2}\wedge\psi_{3}$ of the following three formulas:

  1. 1.

$\psi_{1}=\forall\pi.\
\neg\texttt{x}_{\pi}\operatorname{\mathbf{U}}(\texttt{x}_{\pi}\wedge\mathop{\mathbf{X}\vphantom{a}}\nolimits\mathop{\mathbf{G}\vphantom{a}}\nolimits\neg\texttt{x}_{\pi})$:
every trace in a model is of the form
$\emptyset^{n}\\{\texttt{x}\\}\emptyset^{\omega}$ for some $n\in\mathbb{N}$,
i.e., every model is a subset of
$\\{\emptyset^{n}\\{\texttt{x}\\}\emptyset^{\omega}\mid n\in\mathbb{N}\\}$.

  2. 2.

$\psi_{2}=\exists\pi.\ \texttt{x}_{\pi}$: the trace
$\emptyset^{0}\\{\texttt{x}\\}\emptyset^{\omega}$ is in every model.

  3. 3.

$\psi_{3}=\forall\pi.\ \exists\pi^{\prime}.\
\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{x}_{\pi}\wedge\mathop{\mathbf{X}\vphantom{a}}\nolimits\texttt{x}_{\pi^{\prime}})$:
if $\emptyset^{n}\\{\texttt{x}\\}\emptyset^{\omega}$ is in a model for some
$n\in\mathbb{N}$, then also
$\emptyset^{n+1}\\{\texttt{x}\\}\emptyset^{\omega}$.

Then, $\psi$ has exactly one model (over $\mathrm{AP}$), namely
$\\{\emptyset^{n}\\{\texttt{x}\\}\emptyset^{\omega}\mid n\in\mathbb{N}\\}$.

Traces of the form $\emptyset^{n}\\{\texttt{x}\\}\emptyset^{\omega}$ indeed
encode natural numbers and $\psi$ expresses that every model contains the
encodings of all natural numbers and nothing else. But we can of course also
encode sets of natural numbers with traces as follows: a trace $t$ over a set
of atomic propositions containing x encodes the set
$\\{n\in\mathbb{N}\mid\texttt{x}\in t(n)\\}$. In the following, we show that
second-order quantification allows us to express the existence of the
encodings of all subsets of natural numbers by requiring that for every subset
$S\subseteq\mathbb{N}$ (encoded by the set
$\\{\emptyset^{n}\\{\texttt{x}\\}\emptyset^{\omega}\mid n\in S\\}$ of traces)
there is a trace $t$ encoding $S$, which means x is in $t(n)$ if and only if
$S$ contains a trace in which x holds at position $n$. This equivalence can be
expressed in Hyper2LTL. For technical reasons, we do not capture the
equivalence directly but instead use encodings of both the natural numbers
that are in $S$ and the natural numbers that are not in $S$.

######  Theorem 1.

There is a satisfiable Hyper2LTL sentence that only has models of cardinality
$\mathfrak{c}$.

###### Proof.

We prove that there is a satisfiable Hyper2LTL sentence
$\varphi_{\mathit{allSets}}$ whose unique model has cardinality
$\mathfrak{c}$. To this end, we fix
$\mathrm{AP}=\\{\texttt{+},\texttt{-},\texttt{s},\texttt{x}\\}$ and consider
the conjunction
$\varphi_{\mathit{allSets}}=\varphi_{0}\wedge\cdots\wedge\varphi_{4}$ of the
following formulas:

  * •

$\varphi_{0}=\forall\pi\in X_{d}.\
\bigvee_{\texttt{p}\in\\{\texttt{+},\texttt{-},\texttt{s}\\}}\mathop{\mathbf{G}\vphantom{a}}\nolimits(\texttt{p}_{\pi}\wedge\bigwedge_{\texttt{p}^{\prime}\in\\{\texttt{+},\texttt{-},\texttt{s}\\}\setminus\\{\texttt{p}\\}}\neg\texttt{p}^{\prime}_{\pi})$:
In each trace of a model, either one of the propositions in
$\\{\texttt{+},\texttt{-},\texttt{s}\\}$ holds at every position and the other
two propositions in $\\{\texttt{+},\texttt{-},\texttt{s}\\}$ hold at none of
the positions. Consequently, we speak in the following about type p traces for
$\texttt{p}\in\\{\texttt{+},\texttt{-},\texttt{s}\\}$.

  * •

$\varphi_{1}=\forall\pi\in X_{d}.\
(\texttt{+}_{\pi}\vee\texttt{-}_{\pi})\rightarrow\neg\texttt{x}_{\pi}\operatorname{\mathbf{U}}(\texttt{x}_{\pi}\wedge\mathop{\mathbf{X}\vphantom{a}}\nolimits\mathop{\mathbf{G}\vphantom{a}}\nolimits\neg\texttt{x}_{\pi})$:
Type p traces for $\texttt{p}\in\\{\texttt{+},\texttt{-}\\}$ in the model have
the form
$\\{\texttt{p}\\}^{n}\\{\texttt{x},\texttt{p}\\}\\{\texttt{p}\\}^{\omega}$.

  * •

$\varphi_{2}=\bigwedge_{\texttt{p}\in\\{\texttt{+},\texttt{-}\\}}\exists\pi\in
X_{d}.\ \texttt{p}_{\pi}\wedge\texttt{x}_{\pi}$: for both
$\texttt{p}\in\\{\texttt{+},\texttt{-}\\}$, the type p trace
$\\{\texttt{p}\\}^{0}\\{\texttt{x},\texttt{p}\\}\\{\texttt{p}\\}^{\omega}$ is
in every model.

  * •

$\varphi_{3}=\bigwedge_{\texttt{p}\in\\{\texttt{+},\texttt{-}\\}}\forall\pi\in
X_{d}.\ \exists\pi^{\prime}\in X_{d}.\
\texttt{p}_{\pi}\rightarrow(\texttt{p}_{\pi^{\prime}}\wedge\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{x}_{\pi}\wedge\mathop{\mathbf{X}\vphantom{a}}\nolimits\texttt{x}_{\pi^{\prime}}))$:
for both $\texttt{p}\in\\{\texttt{+},\texttt{-}\\}$, if the type p trace
$\\{\texttt{p}\\}^{n}\\{\texttt{x},\texttt{p}\\}\\{\texttt{p}\\}^{\omega}$ is
in a model for some $n\in\mathbb{N}$, then also
$\\{\texttt{p}\\}^{n+1}\\{\texttt{x},\texttt{p}\\}\\{\texttt{p}\\}^{\omega}$.

Note that the formulas $\varphi_{1},\varphi_{2},\varphi_{3}$ are similar to
the formulas $\psi_{1},\psi_{2},\psi_{3}$ from Example 1. Hence, every model
of the first four conjuncts contains
$\\{\\{\texttt{+}\\}^{n}\\{\texttt{x},\texttt{+}\\}\\{\texttt{+}\\}^{\omega}\mid
n\in\mathbb{N}\\}$ and
$\\{\\{\texttt{-}\\}^{n}\\{\texttt{x},\texttt{-}\\}\\{\texttt{-}\\}^{\omega}\mid
n\in\mathbb{N}\\}$ as subsets, and no other type + or type - traces.

Now, consider an arbitrary set $T$ of traces over $\mathrm{AP}$ (recall that
second-order quantification ranges over arbitrary sets, not only over subsets
of the universe of discourse). We say that $T$ is contradiction-free if there
is no $n\in\mathbb{N}$ such that
$\\{\texttt{+}\\}^{n}\\{\texttt{x},\texttt{+}\\}\\{\texttt{+}\\}^{\omega}\in
T$ and
$\\{\texttt{-}\\}^{n}\\{\texttt{x},\texttt{-}\\}\\{\texttt{-}\\}^{\omega}\in
T$. Furthermore, a trace $t$ over $\mathrm{AP}$ is consistent with a
contradiction-free $T$ if

    1. (C1)

$\\{\texttt{+}\\}^{n}\\{\texttt{x},\texttt{+}\\}\\{\texttt{+}\\}^{\omega}\in
T$ implies $\texttt{x}\in t(n)$ and

    2. (C2)

$\\{\texttt{-}\\}^{n}\\{\texttt{x},\texttt{-}\\}\\{\texttt{-}\\}^{\omega}\in
T$ implies $\texttt{x}\notin t(n)$.

Note that $T$ does not necessarily specify the truth value of x in every
position of $t$, i.e., in those positions $n\in\mathbb{N}$ where neither
$\\{\texttt{+}\\}^{n}\\{\texttt{x},\texttt{+}\\}\\{\texttt{+}\\}^{\omega}$ nor
$\\{\texttt{-}\\}^{n}\\{\texttt{x},\texttt{-}\\}\\{\texttt{-}\\}^{\omega}$ are
in $T$. Nevertheless, for every trace $t$ over $\\{\texttt{x}\\}$ there is a
contradiction-free $T$ such that the $\\{\texttt{x}\\}$-projection of every
trace $t^{\prime}$ over $\mathrm{AP}$ that is consistent with $T$ is equal to
$t$.

  * •

Hence, we define $\varphi_{4}$ as the formula

$\displaystyle\forall X.\ {}$ $\displaystyle{}\overbrace{[\forall\pi\in X.\
\forall\pi^{\prime}\in X.\
(\texttt{+}_{\pi}\wedge\texttt{-}_{\pi^{\prime}})\rightarrow\neg\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{x}_{\pi}\wedge\texttt{x}_{\pi^{\prime}})]}^{\text{$X$
is contradiction-free}}\rightarrow$
$\displaystyle{}\exists\pi^{\prime\prime}\in X_{d}.\
\forall\pi^{\prime\prime\prime}\in X.\
\texttt{s}_{\pi^{\prime\prime}}\wedge\underbrace{(\texttt{+}_{\pi^{\prime\prime\prime}}\rightarrow\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{x}_{\pi^{\prime\prime\prime}}\wedge\texttt{x}_{\pi^{\prime\prime}}))}_{\text{(C1)}}\wedge\underbrace{(\texttt{-}_{\pi^{\prime\prime\prime}}\rightarrow\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{x}_{\pi^{\prime\prime\prime}}\wedge\neg\texttt{x}_{\pi^{\prime\prime}}))}_{\text{(C2)}},$

expressing that for every contradiction-free set of traces $T$, there is a
type s trace $t^{\prime\prime}$ in the model (note that $\pi^{\prime\prime}$
is required to be in $X_{d}$) that is consistent with $T$.

While $\varphi_{\mathit{allSets}}$ is not in prenex normal form, it can easily
be turned into an equivalent formula in prenex normal form (at the cost of
readability). Now, the set

$\displaystyle T_{\mathit{allSets}}={}$
$\displaystyle{}\\{\\{\texttt{+}\\}^{n}\\{\texttt{x},\texttt{+}\\}\\{\texttt{+}\\}^{\omega}\mid
n\in\mathbb{N}\\}\cup\\{\\{\texttt{-}\\}^{n}\\{\texttt{x},\texttt{-}\\}\\{\texttt{-}\\}^{\omega}\mid
n\in\mathbb{N}\\}\cup$
$\displaystyle{}\\{(t(0)\cup\\{\texttt{s}\\})(t(1)\cup\\{\texttt{s}\\})(t(2)\cup\\{\texttt{s}\\})\cdots\mid
t\in(2^{\\{\texttt{x}\\}})^{\omega}\\}$

of traces satisfies $\varphi_{\mathit{allSets}}$. On the other hand, every
model of $\varphi_{\mathit{allSets}}$ must indeed contain
$T_{\mathit{allSets}}$ as a subset, as $\varphi_{\mathit{allSets}}$ requires
the existence of all of its traces in the model. Finally, due to $\varphi_{0}$
and $\varphi_{1}$, a model cannot contain any traces that are not in
$T_{\mathit{allSets}}$, i.e., $T_{\mathit{allSets}}$ is the unique model of
$\varphi_{\mathit{allSets}}$.

To conclude, we just remark that

$\\{(t(0)\cup\\{\texttt{s}\\})(t(1)\cup\\{\texttt{s}\\})(t(2)\cup\\{\texttt{s}\\})\cdots\mid
t\in(2^{\\{\texttt{x}\\}})^{\omega}\\}\subseteq T_{\mathit{allSets}}$

has indeed cardinality $\mathfrak{c}$, as $(2^{\\{\texttt{x}\\}})^{\omega}$
has cardinality $\mathfrak{c}$. ∎

As alluded to above, we could restrict the second-order quantifier in
$\varphi_{4}$ (the only one in $\varphi_{\mathit{allSets}}$) to subsets of the
universe of discourse, as the set
$T=\\{\\{\texttt{+}\\}^{n}\\{\texttt{x},\texttt{+}\\}\\{\texttt{+}\\}^{\omega}\mid
n\in\mathbb{N}\\}\cup\\{\\{\texttt{-}\\}^{n}\\{\texttt{x},\texttt{-}\\}\\{\texttt{-}\\}^{\omega}\mid
n\in\mathbb{N}\\}$ of traces (which is a subset of every model) is already
_rich_ enough to encode every subset of $\mathbb{N}$ by an appropriate
contradiction-free subset of $T$. Thus, $\varphi_{\mathit{allSets}}$ has the
unique model $T_{\mathit{allSets}}$ even under closed-world semantics.

######  Corollary 1.

There is a satisfiable Hyper2LTL sentence that only has models of cardinality
$\mathfrak{c}$ under closed-world semantics.

##  4 The Complexity of Hyper2LTL Satisfiability

The Hyper2LTL satisfiability problem asks, given a Hyper2LTL sentence
$\varphi$, whether $\varphi$ is satisfiable. In this section, we determine
tight bounds on the complexity of the Hyper2LTL satisfiability problem and
some of its variants.

Recall that in Section 3 we encoded sets of natural numbers as traces over a
set of propositions containing x and encoded natural numbers as singleton
sets. Hence, sets of traces can encode sets of sets of natural numbers, i.e.,
type $2$ objects. Using these encodings, we show that Hyper2LTL and truth in
third-order arithmetic have the same complexity.

An important ingredient in our proof is the implementation of addition and
multiplication in temporal logic following Fortin et al. [8]: Let
$\mathrm{AP}_{\mathit{arith}}=\\{\texttt{arg1},\texttt{arg2},\texttt{res},\texttt{add},\texttt{mult}\\}$
and let $T_{(+,\cdot)}$ be the set of all traces
$t\in(2^{\mathrm{AP}_{\mathit{arith}}})^{\omega}$ such that

  * •

there are unique $n_{1},n_{2},n_{3}\in\mathbb{N}$ with $\texttt{arg1}\in
t(n_{1})$, $\texttt{arg2}\in t(n_{2})$, and $\texttt{res}\in t(n_{3})$, and

  * •

either $\texttt{add}\in t(n)$, $\texttt{mult}\notin t(n)$ for all $n$, and
$n_{1}+n_{2}=n_{3}$, or $\texttt{mult}\in t(n)$, $\texttt{add}\notin t(n)$ for
all $n$, and $n_{1}\cdot n_{2}=n_{3}$.

######  Proposition 2 (Theorem 5.5 of [8]).

There is a satisfiable HyperLTL sentence $\varphi_{(+,\cdot)}$ such that the
$\mathrm{AP}_{\mathit{arith}}$-projection of every model of
$\varphi_{(+,\cdot)}$ is $T_{(+,\cdot)}$.

Now, we are able to settle the complexity of the Hyper2LTL satisfiability
problem.

######  Theorem 2.

The Hyper2LTL satisfiability problem is polynomial-time equivalent to truth in
third-order arithmetic.

###### Proof.

We begin with the lower bound by reducing truth in third-order arithmetic to
Hyper2LTL satisfiability: we present a polynomial-time translation from
sentences $\varphi$ of third-order arithmetic to Hyper2LTL sentences
$\varphi^{\prime}$ such that $(\mathbb{N},+,\cdot,<,\in)\models\varphi$ if and
only if $\varphi^{\prime}$ is satisfiable.

Given a third-order sentence $\varphi$, we define

$\varphi^{\prime}=\varphi_{\mathit{allSets}}\wedge\exists X_{\mathit{arith}}.\
(\varphi^{\prime}_{(+,\cdot)}\wedge{\mathit{hyp}}(\varphi))$

where $\varphi_{\mathit{allSets}}$ is the Hyper2LTL sentence from the proof of
Theorem 1 enforcing every subset of $\mathbb{N}$ to be encoded in a model,
$\varphi^{\prime}_{(+,\cdot)}$ is the Hyper2LTL formula obtained from the
HyperLTL formula $\varphi_{(+,\cdot)}$ by replacing each quantifier
$\exists\pi$ ($\forall\pi$, respectively) by $\exists\pi\in
X_{\mathit{arith}}$ ($\forall\pi\in X_{\mathit{arith}}$, respectively), and
where ${\mathit{hyp}}(\varphi)$ is defined inductively as follows:

  * •

For third-order variables $\mathcal{Y}$, ${\mathit{hyp}}(\exists\mathcal{Y}.\
\psi)=\exists X_{\mathcal{Y}}.\ (\forall\pi\in X_{\mathcal{Y}}.\
\texttt{s}_{\pi})\wedge{\mathit{hyp}}(\psi)$.

  * •

For third-order variables $\mathcal{Y}$, ${\mathit{hyp}}(\forall\mathcal{Y}.\
\psi)=\forall X_{\mathcal{Y}}.\ (\forall\pi\in X_{\mathcal{Y}}.\
\texttt{s}_{\pi})\rightarrow{\mathit{hyp}}(\psi)$.

  * •

For second-order variables $Y$, ${\mathit{hyp}}(\exists Y.\
\psi)=\exists\pi_{Y}\in X_{d}.\
\texttt{s}_{\pi_{Y}}\wedge{\mathit{hyp}}(\psi)$.

  * •

For second-order variables $Y$, ${\mathit{hyp}}(\forall Y.\
\psi)=\forall\pi_{Y}\in X_{d}.\
\texttt{s}_{\pi_{Y}}\rightarrow{\mathit{hyp}}(\psi)$.

  * •

For first-order variables $y$, ${\mathit{hyp}}(\exists y.\
\psi)=\exists\pi_{y}\in X_{d}.\
\texttt{s}_{\pi_{y}}\wedge[(\neg\texttt{x}_{\pi_{y}})\operatorname{\mathbf{U}}(\texttt{x}_{\pi_{y}}\wedge\mathop{\mathbf{X}\vphantom{a}}\nolimits\mathop{\mathbf{G}\vphantom{a}}\nolimits\neg\texttt{x}_{\pi_{y}})]\wedge{\mathit{hyp}}(\psi)$.

  * •

For first-order variables $y$, ${\mathit{hyp}}(\forall y.\
\psi)=\forall\pi_{y}\in X_{d}.\
(\texttt{s}_{\pi_{y}}\wedge[(\neg\texttt{x}_{\pi_{y}})\operatorname{\mathbf{U}}(\texttt{x}_{\pi_{y}}\wedge\mathop{\mathbf{X}\vphantom{a}}\nolimits\mathop{\mathbf{G}\vphantom{a}}\nolimits\neg\texttt{x}_{\pi_{y}})])\rightarrow{\mathit{hyp}}(\psi)$.

  * •

${\mathit{hyp}}(\psi_{1}\vee\psi_{2})={\mathit{hyp}}(\psi_{1})\vee{\mathit{hyp}}(\psi_{2})$.

  * •

${\mathit{hyp}}(\neg\psi)=\neg{\mathit{hyp}}(\psi)$.

  * •

For second-order variables $Y$ and third-order variables $\mathcal{Y}$,
${\mathit{hyp}}(Y\in\mathcal{Y})=\exists\pi\in X_{\mathcal{Y}}.\
\mathop{\mathbf{G}\vphantom{a}}\nolimits(\texttt{x}_{\pi_{Y}}\leftrightarrow\texttt{x}_{\pi})$.

  * •

For first-order variables $y$ and second-order variables $Y$,
${\mathit{hyp}}(y\in
Y)=\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{x}_{\pi_{y}}\wedge\texttt{x}_{\pi_{Y}})$.

  * •

For first-order variables $y,y^{\prime}$,
${\mathit{hyp}}(y<y^{\prime})=\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{x}_{\pi_{y}}\wedge\mathop{\mathbf{X}\vphantom{a}}\nolimits\mathop{\mathbf{F}\vphantom{a}}\nolimits\texttt{x}_{\pi_{y^{\prime}}})$.

  * •

For first-order variables $y_{1},y_{2},y$,
${\mathit{hyp}}(y_{1}+y_{2}=y)=\exists\pi\in X_{\mathit{arith}}.\
\texttt{add}_{\pi}\wedge\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{arg1}_{\pi}\wedge\texttt{x}_{\pi_{y_{1}}})\wedge\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{arg2}_{\pi}\wedge\texttt{x}_{\pi_{y_{2}}})\wedge\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{res}_{\pi}\wedge\texttt{x}_{\pi_{y}})$.

  * •

For first-order variables $y_{1},y_{2},y$, ${\mathit{hyp}}(y_{1}\cdot
y_{2}=y)=\exists\pi\in X_{\mathit{arith}}.\
\texttt{mult}_{\pi}\wedge\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{arg1}_{\pi}\wedge\texttt{x}_{\pi_{y_{1}}})\wedge\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{arg2}_{\pi}\wedge\texttt{x}_{\pi_{y_{2}}})\wedge\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{res}_{\pi}\wedge\texttt{x}_{\pi_{y}})$.

Note that $\varphi^{\prime}$ is not in prenex normal form, but can easily be
brought into prenex normal form, as there are no quantifiers under the scope
of a temporal operator.

Now, an induction shows that $(\mathbb{N},+,\cdot,<,\in)$ satisfies $\varphi$
if and only if $T_{\mathit{allSets}}$ satisfies $\varphi^{\prime}$. As
$T_{\mathit{allSets}}$ is the unique model of $\varphi_{\mathit{allSets}}$, it
is also the unique model of $\varphi$, i.e., $\varphi^{\prime}$ is satisfiable
if and only if $T_{\mathit{allSets}}$ satisfies $\varphi^{\prime}$. Altogether
we obtain the desired equivalence between
$(\mathbb{N},+,\cdot,<,\in)\models\varphi$ and $\varphi^{\prime}$ being
satisfiable.

For the upper bound, we conversely reduce Hyper2LTL satisfiability to truth in
third-order arithmetic: we present a polynomial-time translation from
Hyper2LTL sentences $\varphi$ to sentences $\varphi^{\prime}$ of third-order
arithmetic such that $\varphi$ is satisfiable if and only if
$(\mathbb{N},+,\cdot,<,\in)\models\varphi^{\prime}$.

Let $\mathit{pair}\colon\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$
denote Cantor’s pairing function defined as
$\mathit{pair}(i,j)=\frac{1}{2}(i+j)(i+j+1)+j$, which is a bijection.
Furthermore, fix some bijection
$e\colon\mathrm{AP}\rightarrow\\{0,1,\ldots,|\mathrm{AP}|-1\\}$. Then, we
encode a trace $t\in(2^{\mathrm{AP}})^{\omega}$ by the set
$S_{t}=\\{\mathit{pair}(j,e(\texttt{p}))\mid j\in\mathbb{N}\text{ and
}\texttt{p}\in t(j)\\}\subseteq\mathbb{N}$. As $\mathit{pair}$ is a bijection,
we have that $t\neq t^{\prime}$ implies $S_{t}\neq S_{t^{\prime}}$. While not
every subset of $\mathbb{N}$ encodes some trace $t$, the first-order formula

$\varphi_{\mathit{isTrace}}(Y)=\forall x.\ \forall y.\
y\geq|\mathrm{AP}|\rightarrow\mathit{pair}(x,y)\notin Y$

checks if a set does encode a trace. Here, we use $\mathit{pair}$ as syntactic
sugar, which is possible as the definition of $\mathit{pair}$ only uses
addition and multiplication.

As (certain) sets of natural numbers encode traces, sets of (certain) sets of
natural numbers encode sets of traces. This is sufficient to reduce Hyper2LTL
to third-order arithmetic, which allows the quantification over sets of sets
of natural numbers. Before we present the translation, we need to introduce
some more auxiliary formulas:

  * •

Let $\mathcal{Y}$ be a third-order variable (i.e., $\mathcal{Y}$ ranges over
sets of sets of natural numbers). Then, the formula

$\varphi_{\mathit{onlyTraces}}(\mathcal{Y})=\forall Y.\
Y\in\mathcal{Y}\rightarrow\varphi_{\mathit{isTrace}}(Y)$

checks if a set of sets of natural numbers only contains sets encoding a
trace.

  * •

Further, the formula

$\varphi_{\mathit{allTraces}}(\mathcal{Y})=\varphi_{\mathit{onlyTraces}}(\mathcal{Y})\wedge\forall
Y.\ \pi_{\mathit{isTrace}}(Y)\rightarrow Y\in\mathcal{Y}$

checks if a set of sets of natural numbers contains exactly the sets encoding
a trace.

Now, we are ready to define our encoding of Hyper2LTL in third-order
arithmetic. Given a Hyper2LTL sentence $\varphi$, let

$\varphi^{\prime}=\exists\mathcal{Y}_{a}.\ \exists\mathcal{Y}_{d}.\
\varphi_{\mathit{allTraces}}(\mathcal{Y}_{a})\wedge\varphi_{\mathit{onlyTraces}}(\mathcal{Y}_{d})\wedge{\mathit{ar}}(\varphi)(0)$

where ${\mathit{ar}}(\varphi)$ is defined inductively as presented below. Note
that $\varphi^{\prime}$ requires $\mathcal{Y}_{a}$ to contain exactly the
encodings of all traces (i.e., it corresponds to the distinguished Hyper2LTL
variable $X_{a}$ in the following translation) and $\mathcal{Y}_{d}$ is an
existentially quantified set of trace encodings (i.e., it corresponds to the
distinguished Hyper2LTL variable $X_{d}$ in the following translation).

In the inductive definition of ${\mathit{ar}}(\varphi)$, we will employ a free
first-order variable $i$ to denote the position at which the formula is to be
evaluated to capture the semantics of the temporal operators. As seen above,
in $\varphi^{\prime}$, this free variable is set to zero in correspondence
with the Hyper2LTL semantics.

  * •

${\mathit{ar}}(\exists X.\ \psi)=\exists\mathcal{Y}_{X}.\
\varphi_{\mathit{onlyTraces}}(\mathcal{Y}_{X})\wedge{\mathit{ar}}(\psi)$.
Here, the free variable of ${\mathit{ar}}(\exists X.\ \psi)$ is the free
variable of ${\mathit{ar}}(\psi)$.

  * •

${\mathit{ar}}(\forall X.\ \psi)=\forall\mathcal{Y}_{X}.\
\varphi_{\mathit{onlyTraces}}(\mathcal{Y}_{X})\rightarrow{\mathit{ar}}(\psi)$.
Here, the free variable of ${\mathit{ar}}(\forall X.\ \psi)$ is the free
variable of ${\mathit{ar}}(\psi)$.

  * •

${\mathit{ar}}(\exists\pi\in X.\ \psi)=\exists Y_{\pi}.\
Y_{\pi}\in\mathcal{Y}_{X}\wedge{\mathit{ar}}(\psi)$. Here, the free variable
of ${\mathit{ar}}(\exists\pi\in X.\ \psi)$ is the free variable of
${\mathit{ar}}(\psi)$.

  * •

${\mathit{ar}}(\forall\pi\in X.\ \psi)=\forall Y_{\pi}.\
Y_{\pi}\in\mathcal{Y}_{X}\rightarrow{\mathit{ar}}(\psi)$. Here, the free
variable of ${\mathit{ar}}(\forall\pi\in X.\ \psi)$ is the free variable of
${\mathit{ar}}(\psi)$.

  * •

${\mathit{ar}}(\psi_{1}\vee\psi_{2})={\mathit{ar}}(\psi_{1})\vee{\mathit{ar}}(\psi_{2})$.
Here, we require the free variables of ${\mathit{ar}}(\psi_{1})$ and
${\mathit{ar}}(\psi_{2})$ are the same (which can always be achieved by
variable renaming), which is then also the free variable of
${\mathit{ar}}(\psi_{1}\vee\psi_{2})$.

  * •

${\mathit{ar}}(\neg\psi)=\neg{\mathit{ar}}(\psi)$. Here, the free variable of
${\mathit{ar}}(\neg\psi)$ is the free variable of $\neg{\mathit{ar}}(\psi)$.

  * •

${\mathit{ar}}(\mathop{\mathbf{X}\vphantom{a}}\nolimits\psi)=(i^{\prime}=i+1)\wedge{\mathit{ar}}(\psi)$,
where $i^{\prime}$ is the free variable of ${\mathit{ar}}(\psi)$ and $i$ is
the free variable of
${\mathit{ar}}(\mathop{\mathbf{X}\vphantom{a}}\nolimits\psi)$.

  * •

${\mathit{ar}}(\psi_{1}\operatorname{\mathbf{U}}\psi)=\exists i_{1}.\
i_{1}\geq i\wedge{\mathit{ar}}(\psi_{1})\wedge\forall i_{2}.\ (i\leq
i_{2}\wedge i_{2}<i_{1})\rightarrow{\mathit{ar}}(\psi_{2})$, where $i_{1}$ is
the free variable of ${\mathit{ar}}(\psi_{1})$, $i_{2}$ is the free variable
of ${\mathit{ar}}(\psi_{2})$, and $i$ is the free variable of
${\mathit{ar}}(\psi_{1}\operatorname{\mathbf{U}}\psi_{2})$.

  * •

${\mathit{ar}}(\texttt{p}_{\pi})=\mathit{pair}(i,e(\texttt{p}))\in Y_{\pi}$,
where $e\colon\mathrm{AP}\rightarrow\\{0,1,\ldots,|\mathrm{AP}|-1\\}$ is the
encoding of propositions by natural numbers introduced above. Note that $i$ is
the free variable of ${\mathit{ar}}(a_{\pi})$.

Now, an induction shows that
$\Pi_{\emptyset}[X_{a}\rightarrow(2^{\mathrm{AP}})^{\omega},X_{d}\mapsto
T]\models\varphi$ if and only if $(\mathbb{N},+,\cdot,<,\in)$ satisfies
${\mathit{ar}}(\varphi)$ when the variable $\mathcal{Y}_{a}$ is interpreted by
the encoding of $(2^{\mathrm{AP}})^{\omega}$ and $\mathcal{Y}_{d}$ is
interpreted by the encoding of $T$. Hence, $\varphi$ is indeed satisfiable if
and only if $(\mathbb{N},+,\cdot,<,\in)$ satisfies $\varphi^{\prime}$. ∎

Again, let us also consider the lower bound under closed-world semantics.
Recall that we have constructed from a sentence $\varphi$ of third-order
arithmetic a Hyper2LTL sentence $\varphi^{\prime}$ such that
$(\mathbb{N},+,\cdot,<,\in)\models\varphi$ if and only if $\varphi^{\prime}$
is satisfiable. Furthermore, if $\varphi^{\prime}$ is satisfiable, then it has
the unique model $T_{\mathit{allSets}}$. The unique model $T_{(+,\cdot)}$ of
the conjunct $\varphi_{(+,\cdot)}$ of $\varphi^{\prime}$, is not a subset of
$T_{\mathit{allSets}}$, i.e., the construction presented above is not correct
under closed-world semantics. However, by slightly modifying the construction
of $\varphi_{\mathit{allSets}}$ so that it also allows for the traces in
$T_{(+,\cdot)}$ in the model, we obtain from $\varphi^{\prime}$ a formula that
is satisfied by $T_{\mathit{allSets}}\cup T_{(+,\cdot)}$ if and only if
$(\mathbb{N},+,\cdot,<,\in)\models\varphi$. We leave the details to the
reader.

Thus, the lower bound holds even under closed-world semantics. Together with
Lemma 1 we obtain the following corollary.

######  Corollary 2.

The Hyper2LTL satisfiability problem under closed-world semantics is
polynomial-time equivalent to truth in third-order arithmetic.

The Hyper2LTL finite-state satisfiability problem asks, given a Hyper2LTL
sentence $\varphi$, whether there is a finite transition system satisfying
$\varphi$. Note that we do not ask for a finite set $T$ of traces satisfying
$\varphi$, and that the set of traces of the finite transition system may
still be infinite or even uncountable. Nevertheless, the problem is
potentially simpler, as there are only countably many finite transition
systems (and their sets of traces are much simpler). Nevertheless, we show
that the finite-state satisfiability problem is as hard as the general
satisfiability problem, as Hyper2LTL allows the quantification over arbitrary
(sets of) traces, i.e., restricting the universe of discourse to the traces of
a finite transition system does not restrict second-order quantification at
all. This has to be contrasted with the finite-state satisfiability problem
for HyperLTL (defined analogously), which is recursively enumerable, as
HyperLTL model-checking of finite transition systems is decidable [2].

######  Theorem 3.

The Hyper2LTL finite-state satisfiability problem is polynomial-time
equivalent to truth in third-order arithmetic.

###### Proof.

For the lower bound, we reduce truth in third-order arithmetic to Hyper2LTL
finite-state satisfiability: we present a polynomial-time translation from
sentences $\varphi$ of third-order arithmetic to Hyper2LTL sentences
$\varphi^{\prime}$ such that $(\mathbb{N},+,\cdot,<,\in)\models\varphi$ if and
only if $\varphi^{\prime}$ is satisfied by a finite transition system.

So, let $\varphi$ be a sentence of third-order arithmetic. Recall that in the
proof of Theorem 2, we have shown how to construct from $\varphi$ the
Hyper2LTL sentence $\varphi^{\prime}$ such that the following three statements
are equivalent:

  * •

$(\mathbb{N},+,\cdot,<,\in)\models\varphi$.

  * •

$\varphi^{\prime}$ is satisfiable.

  * •

$\varphi^{\prime}$ is satisfied by $T_{\mathit{allSets}}$.

As there is a finite transition system $\mathfrak{T}_{\mathit{allSets}}$ with
$\mathrm{Tr}(\mathfrak{T}_{\mathit{allSets}})=T_{\mathit{allSets}}$, the lower
bound follows from Theorem 2.

For the upper bound, we conversely reduce Hyper2LTL finite-state
satisfiability to truth in third-order arithmetic: we present a polynomial-
time translation from Hyper2LTL sentences $\varphi$ to sentences
$\varphi^{\prime\prime}$ of third-order arithmetic such that $\varphi$ is
satisfied by a finite transition system if and only if
$(\mathbb{N},+,\cdot,<,\in)\models\varphi^{\prime\prime}$.

Recall that in the proof of Theorem 2, we have constructed a Hyper2LTL
sentence

$\varphi^{\prime}=\exists\mathcal{Y}_{a}.\ \exists\mathcal{Y}_{d}.\
\varphi_{\mathit{allTraces}}(\mathcal{Y}_{a})\wedge\varphi_{\mathit{onlyTraces}}(\mathcal{Y}_{d})\wedge{\mathit{ar}}(\varphi)(0)$

where $\mathcal{Y}_{a}$ represents the distinguished Hyper2LTL variable
$X_{a}$, $\mathcal{Y}_{d}$ represents the distinguished Hyper2LTL variable
$X_{d}$, and where ${\mathit{ar}}(\varphi)$ is the encoding of $\varphi$ in
Hyper2LTL.

To encode the general satisfiability problem it was sufficient to express that
$\mathcal{Y}_{d}$ only contains traces. Here, we now require that
$\mathcal{Y}_{d}$ contains exactly the traces of some finite transition
system, which can easily be expressed in second-order arithmetic111With a
little more effort, and a little less readability, first-order suffices for
this task, as finite transition systems can be encoded by natural numbers. as
follows.

We begin with a formula $\varphi_{\mathit{isTS}}(n,E,I,\ell)$ expressing that
the second-order variables $E$, $I$, and $\ell$ encode a transition system
with set $\\{0,1,\ldots,n-1\\}$ of vertices. Our encoding will make extensive
use of the pairing function introduced in the proof of Theorem 2. Formally, we
define $\varphi_{\mathit{isTS}}(n,E,I,\ell)$ as the conjunction of the
following formulas (where all quantifiers are first-order and we use
$\mathit{pair}$ as syntactic sugar):

  * •

$\forall y.\ y\in E\rightarrow\exists v.\ \exists v^{\prime}.\ (v<n\wedge
v^{\prime}<n\wedge y=\mathit{pair}(v,v^{\prime}))$: edges are pairs of
vertices.

  * •

$\forall v.\ v<n\rightarrow\exists v^{\prime}.\
(v^{\prime}<n\wedge\mathit{pair}(v,v^{\prime})\in E)$: every vertex has a
successor.

  * •

$\forall v.\ v\in I\rightarrow v<n$: the set of initial vertices is a subset
of the set of all vertices.

  * •

$\forall y.\ y\in\ell\rightarrow\exists v.\ \exists p.\ (v<n\wedge
p<|\mathrm{AP}|\wedge y=\mathit{pair}(v,p))$: the labeling of $v$ by $p$ is
encoded by the pair $(v,p)$.

Next, we define $\varphi_{\mathit{isPath}}(P,n,E,I)$, expressing that the
second-order variable $P$ encodes a path through the transition system encoded
by $n$, $E$, and $I$, as the conjunction of the following formulas:

  * •

$\forall j.\ \exists v.\ (v<n\wedge\mathit{pair}(j,v)\in P\wedge\neg\exists
v^{\prime}.\ (v^{\prime}\neq v\wedge\mathit{pair}(j,v^{\prime})\in P))$: the
fact that at position $j$ the path visits vertex $v$ is encoded by the pair
$(j,v)$. Exactly one vertex is visited at each position.

  * •

$\exists v.\ v\in I\wedge\mathit{pair}(0,v)\in P$: the path starts in an
initial vertex.

  * •

$\forall j.\ \exists v.\ \exists v^{\prime}.\ \mathit{pair}(j,v)\in
P\wedge\mathit{pair}(j+1,v^{\prime})\in P\wedge\mathit{pair}(v,v^{\prime})\in
E$: successive vertices in the path are indeed connected by an edge.

Finally, we define $\varphi_{\mathit{traceOf}}(T,P,\ell)$, expressing that the
second-order variable $T$ encodes the trace (using the encoding from the proof
of Theorem 2) of the path encoded by the second-order variable $P$, as the
following formula:

  * •

$\forall j.\ \forall p.\ \mathit{pair}(j,p)\in T\leftrightarrow(\exists v.\
(j,v)\in P\wedge(v,p)\in\ell)$: a proposition holds in the trace at position
$j$ if and only if it is in the labeling of the $j$-th vertex of the path.

Now, we define the sentence $\varphi^{\prime\prime}$ as

$\displaystyle\exists\mathcal{Y}_{a}.\ \exists\mathcal{Y}_{d}.\ {}$
$\displaystyle{}\varphi_{\mathit{allTraces}}(\mathcal{Y}_{a})\wedge\varphi_{\mathit{onlyTraces}}(\mathcal{Y}_{d})\wedge$
$\displaystyle{}[\underbrace{\exists n.\ \exists E.\ \exists I.\ \exists\ell.\
\varphi_{\mathit{isTS}}(n,E,I,\ell)}_{\text{there exists a transition
system~{}$\mathfrak{T}$}}\wedge\overbrace{(\forall T.\
T\in\mathcal{Y}_{d}\rightarrow\exists P.\
(\varphi_{\mathit{isPath}}(P,n,E,I)\wedge\varphi_{\mathit{traceOf}}(T,P,\ell)))}^{\text{$\mathcal{Y}_{d}$
contains only traces of paths through $\mathfrak{T}$}}$
$\displaystyle{}\phantom{(\exists n.\ \exists E.\ \exists I.\ \exists\ell.\
\varphi_{\mathit{isTS}}(n,E,I,\ell)}\wedge\underbrace{(\forall P.\
(\varphi_{\mathit{isPath}}(P,n,E,I)\rightarrow\exists T.\
T\in\mathcal{Y}_{d}\wedge\varphi_{\mathit{traceOf}}(T,P,\ell)))}_{\text{$\mathcal{Y}_{d}$
contains all traces of paths through $\mathfrak{T}$.}}]$
$\displaystyle{}\wedge{\mathit{ar}}(\varphi)(0)$

holds in $(\mathbb{N},+,\cdot,<,\in)$ if and only if $\varphi$ is satisfied by
a finite transition system. ∎

Again, let us also consider the case of closed-world semantics. There is no
finite transition system $\mathfrak{T}$ with
$\mathrm{Tr}(\mathfrak{T})=T_{(+,\cdot)}$. But the topological closure
$\overline{T_{(+,\cdot)}}$ of $T_{(+,\cdot)}$, which contains all traces of
$T_{(+,\cdot)}$, is also the unique model of some HyperLTL sentence [8]. Using
these facts, we can show that the lower bound also works for closed-world
semantics. To this end, we again need to modify $\varphi_{\mathit{allSets}}$
to allow the traces in $\overline{T_{(+,\cdot)}}$, modify
${\mathit{ar}}(\varphi)$ to ignore the traces in
$\overline{T_{(+,\cdot)}}\setminus T_{(+,\cdot)}$, and then consider the model
$T_{\mathit{allSets}}\cup\overline{T_{(+,\cdot)}}$, which can be represented
by a finite transition system. We leave the details to the reader.

With Lemma 1, we obtain the following corollary.

######  Corollary 3.

The Hyper2LTL finite-state satisfiability problem under closed-world semantics
is polynomial-time equivalent to truth in third-order arithmetic.

Let us also just remark that the proof of Theorem 3 can easily be adapted to
show that other natural variations of the satisfiability problem are also
polynomial-time equivalent to truth in third-order arithmetic, e.g.,
satisfiability by countable transition systems, satisfiability by finitely
branching transition systems, etc. In fact, as long as a class $\mathcal{C}$
of transition systems is definable in third-order arithmetic, the Hyper2LTL
satisfiability problem restricted to transition systems in $\mathcal{C}$ is
reducible to truth in third-order arithmetic. On the other hand, Hyper2LTL
satisfiability restricted to transition systems in $\mathcal{C}$ is
polynomial-time reducible to truth in third-order arithmetic, for any nonempty
class $\mathcal{C}$ of transition systems, as $T_{\mathit{allSets}}$ is
definable in Hyper2LTL: one can just posit the existence of all traces in
$T_{\mathit{allSets}}$ and does not need to have them contained in the models
of the formula (in standard semantics).

##  5 The Complexity of Hyper2LTL Model-Checking

The Hyper2LTL model-checking problem asks, given a finite transition system
$\mathfrak{T}$ and a Hyper2LTL sentence $\varphi$, whether
$\mathfrak{T}\models\varphi$. Beutner et al. [1] have shown that Hyper2LTL
model-checking is $\Sigma_{1}^{1}$-hard, but there is no known upper bound in
the literature. We improve the lower bound considerably, i.e., also to truth
in third-order arithmetic, and then show that this bound is tight. This is the
first upper bound on the problem’s complexity.

######  Theorem 4.

The Hyper2LTL model-checking problem is polynomial-time equivalent to truth in
third-order arithmetic.

###### Proof.

For the lower bound, we reduce truth in third-order arithmetic to the
Hyper2LTL model-checking problem: we present a polynomial-time translation
from sentences $\varphi$ of third-order arithmetic to pairs
$(\mathfrak{T},\varphi^{\prime})$ of a finite transition system $\mathfrak{T}$
and a Hyper2LTL sentence $\varphi^{\prime}$ such that
$(\mathbb{N},+,\cdot,<,\in)\models\varphi$ if and only if
$\mathfrak{T}\models\varphi^{\prime}$.

In the proof of Theorem 3 we have, given a sentence $\varphi$ of third-order
arithmetic, constructed a Hyper2LTL sentence $\varphi^{\prime}$ such that
$(\mathbb{N},+,\cdot,<,\in)\models\varphi$ if and only if
$\mathfrak{T}_{\mathit{allSets}}$ satisfies $\varphi^{\prime}$, where
$\mathfrak{T}_{\mathit{allSets}}$ is a finite transition system that is
independent of $\varphi$. Thus, we obtain the lower bound by mapping $\varphi$
to $\varphi^{\prime}$ and $\mathfrak{T}_{\mathit{allSets}}$.

For the upper bound, we reduce the Hyper2LTL model-checking problem to truth
in third-order arithmetic: we present a polynomial-time translation from pairs
$(\mathfrak{T},\varphi)$ of a finite transition system and a Hyper2LTL
sentence $\varphi$ to sentences $\varphi^{\prime}$ of third-order arithmetic
such that $\mathfrak{T}\models\varphi$ if and only if
$(\mathbb{N},+,\cdot,<,\in)\models\varphi^{\prime}$.

In the proof of Theorem 3, we have constructed, from a Hyper2LTL sentence
$\varphi$, a sentence $\varphi^{\prime}$ of third-order arithmetic that
expresses the existence of a finite transition system that satisfies
$\varphi$. We obtain the desired upper bound by modifying $\varphi^{\prime}$
to replace the existential quantification of the transition system by
hardcoding $\mathfrak{T}$ instead. ∎

Again, the lower bound proof can easily be extended to closed-world semantics,
as argued in the proof of Theorem 3.

######  Corollary 4.

The Hyper2LTL model-checking problem under closed-world semantics is
polynomial-time equivalent to truth in third-order arithmetic.

##  6 Hyper2LTLfp

As we have seen, unrestricted second-order quantification makes Hyper2LTL very
expressive and therefore algorithmically infeasible. But restricted forms of
second-order quantification are sufficient for many application areas. Hence,
Beutner et al. [1] introduced Hyper2LTLfp, a fragment of Hyper2LTL in which
second-order quantification ranges over smallest/largest sets that satisfy a
given guard. For example, the formula $\exists(X,\curlyvee,\varphi_{1}).\
\varphi_{2}$ expresses that there is a set $T$ of traces that satisfies both
$\varphi_{1}$ and $\varphi_{2}$, and $T$ is _a_ smallest set that satisfies
$\varphi_{1}$ (i.e., $\varphi_{1}$ is the guard). This fragment is expressive
enough to express common knowledge, asynchronous hyperproperties, and
causality in reactive systems [1].

The formulas of Hyper2LTLfp are given by the grammar

$\displaystyle\varphi{}$
$\displaystyle\mathop{::=}{}\exists(X,\mathrlap{\curlyvee}\curlywedge,\varphi).\
\varphi\mid\forall(X,\mathrlap{\curlyvee}\curlywedge,\varphi).\
\varphi\mid\exists\pi\in X.\ \varphi\mid\forall\pi\in X.\ \varphi\mid\psi$
$\displaystyle\psi{}$
$\displaystyle\mathop{::=}{}\texttt{p}_{\pi}\mid\neg\psi\mid\psi\vee\psi\mid\mathop{\mathbf{X}\vphantom{a}}\nolimits\psi\mid\psi\operatorname{\mathbf{U}}\psi$

where p ranges over $\mathrm{AP}$, $\pi$ ranges over $\mathcal{V}_{1}$, $X$
ranges over $\mathcal{V}_{2}$, and
$\mathrlap{\curlyvee}\curlywedge\in\\{\curlyvee,\curlywedge\\}$, i.e., the
only modification concerns the syntax of second-order quantification.

Accordingly, the semantics of Hyper2LTLfp is similar to that of Hyper2LTL but
for the second-order quantifiers, for which we define (for
$\mathrlap{\curlyvee}\curlywedge\in\\{\curlyvee,\curlywedge\\}$)

  * •

$\Pi\models\exists(X,\mathrlap{\curlyvee}\curlywedge,\varphi_{1}).\
\varphi_{2}$ if there exists a set
$T\in\mathrm{sol}(\Pi,(X,\mathrlap{\curlyvee}\curlywedge,\varphi_{1}))$ such
that $\Pi[X\mapsto T]\models\varphi_{2}$, and

  * •

$\Pi\models\forall(X,\mathrlap{\curlyvee}\curlywedge,\varphi_{1}).\
\varphi_{2}$ if for all sets
$T\in\mathrm{sol}(\Pi,(X,\mathrlap{\curlyvee}\curlywedge,\varphi_{1}))$ we
have $\Pi[X\mapsto T]\models\varphi_{2}$,

where $\mathrm{sol}(\Pi,(X,\mathrlap{\curlyvee}\curlywedge,\varphi_{1}))$ is
the set of all minimal/maximal models of the formula $\varphi_{1}$, which is
defined as follows:

$\displaystyle\mathrm{sol}(\Pi,(X,\curlyvee,\varphi_{1}))$
$\displaystyle{}=\\{T\subseteq(2^{\mathrm{AP}})^{\omega}\mid\Pi[X\mapsto
T]\models\varphi_{1}\text{ and for all }T^{\prime}\subsetneq T\text{ we have
}\Pi[X\mapsto T^{\prime}]\not\models\varphi_{1}\\}$
$\displaystyle\mathrm{sol}(\Pi,(X,\curlywedge,\varphi_{1}))$
$\displaystyle{}=\\{T\subseteq(2^{\mathrm{AP}})^{\omega}\mid\Pi[X\mapsto
T]\models\varphi_{1}\text{ and for all }T^{\prime}\supsetneq T\text{ we have
}\Pi[X\mapsto T^{\prime}]\not\models\varphi_{1}\\}$

Note that $\mathrm{sol}(\Pi,(X,\curlyvee,\varphi_{1}))$ may be empty or may
contain multiple sets, which then have to be pairwise incomparable.

The notions of satisfaction and models are defined as for Hyper2LTL.

######  Proposition 3 (Proposition 1 of [1]).

Every Hyper2LTLfp formula $\varphi$ can in polynomial-time222The polynomial-
time claim is not made in [1], but follows from the construction when using
appropriate data structures for formulas. be translated into a Hyper2LTL
formula $\varphi^{\prime}$ such that for all sets $T$ of traces we have
$T\models\varphi$ if and only if $T\models\varphi^{\prime}$.

Thus, every complexity upper bound for Hyper2LTL also holds for Hyper2LTLfp
and every lower bound for Hyper2LTLfp also holds for Hyper2LTL. In the
following, we show that lower bounds can also be transferred in the other
direction, i.e., from Hyper2LTL to Hyper2LTLfp. Thus, contrary to the design
goal of Hyper2LTLfp, it is in general not more feasible than full Hyper2LTL.

We begin again by studying the cardinality of models of Hyper2LTLfp sentences,
which will be the key technical tool for our complexity results. Again, as
such formulas are evaluated over sets of traces, whose cardinality is bounded
by $\mathfrak{c}$, there is a trivial upper bound. Our main result is that
this bound is tight even for the restricted setting of Hyper2LTLfp.

######  Theorem 5.

There is a satisfiable Hyper2LTLfp sentence that only has models of
cardinality $\mathfrak{c}$.

###### Proof.

We adapt the proof of Theorem 1 to Hyper2LTLfp. Recall that we have
constructed the formula
$\varphi_{\mathit{allSets}}=\varphi_{0}\wedge\cdots\wedge\varphi_{4}$ whose
unique model is uncountable. The subformulas $\varphi_{0},\ldots,\varphi_{3}$
of $\varphi_{\mathit{allSets}}$ are first-order, so let us consider
$\varphi_{4}$. Recall that $\varphi_{4}$ has the form

$\displaystyle\forall X.\ {}$ $\displaystyle{}[\forall\pi\in X.\
\forall\pi^{\prime}\in X.\
(\texttt{+}_{\pi}\wedge\texttt{-}_{\pi^{\prime}})\rightarrow\neg\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{x}_{\pi}\wedge\texttt{x}_{\pi^{\prime}})]\rightarrow$
$\displaystyle{}\exists\pi^{\prime\prime}\in X_{d}.\
\forall\pi^{\prime\prime\prime}\in X.\
\texttt{s}_{\pi^{\prime\prime}}\wedge(\texttt{+}_{\pi^{\prime\prime\prime}}\rightarrow\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{x}_{\pi^{\prime\prime\prime}}\wedge\texttt{x}_{\pi^{\prime\prime}}))\wedge(\texttt{-}_{\pi^{\prime\prime\prime}}\rightarrow\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{x}_{\pi^{\prime\prime\prime}}\wedge\neg\texttt{x}_{\pi^{\prime\prime}})),$

expressing that for every contradiction-free set of traces $T$, there is a
type s trace $t^{\prime\prime}$ in the model that is consistent with $T$.
Here, $X$ ranges over arbitrary sets $T$ of traces. However, this is not
necessary. Consider the formula

$\varphi_{4}^{\prime}=\forall(X,\curlywedge,\varphi_{\mathit{conFree}}).\
\exists\pi^{\prime\prime}\in X_{d}.\ \forall\pi^{\prime\prime\prime}\in X.\
\texttt{s}_{\pi^{\prime\prime}}\wedge(\texttt{+}_{\pi^{\prime\prime\prime}}\rightarrow\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{x}_{\pi^{\prime\prime\prime}}\wedge\texttt{x}_{\pi^{\prime\prime}}))\wedge(\texttt{-}_{\pi^{\prime\prime\prime}}\rightarrow\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{x}_{\pi^{\prime\prime\prime}}\wedge\neg\texttt{x}_{\pi^{\prime\prime}})),$

with

$\varphi_{\mathit{conFree}}=\forall\pi\in X.\ \forall\pi^{\prime}\in X.\
(\texttt{+}_{\pi}\wedge\texttt{-}_{\pi^{\prime}})\rightarrow\neg\mathop{\mathbf{F}\vphantom{a}}\nolimits(\texttt{x}_{\pi}\wedge\texttt{x}_{\pi^{\prime}})$

expressing that $X$ is contradiction-free. In $\varphi_{4}^{\prime}$ the set
variable $X$ only ranges over _maximal_ contradiction-free sets of traces,
i.e., those that contain for each $n$ either
$\\{\texttt{+}\\}^{n}\\{\texttt{x},\texttt{+}\\}\\{\texttt{+}\\}^{\omega}$ or
$\\{\texttt{-}\\}^{n}\\{\texttt{x},\texttt{-}\\}\\{\texttt{-}\\}^{\omega}$.

But even with the restriction to such maximal sets, $\varphi_{4}^{\prime}$
still requires that a model of
$\varphi_{\mathit{allSets}}^{\prime}=\varphi_{0}\wedge\cdots\varphi_{3}\wedge\varphi_{4}^{\prime}$
contains the encoding of every subset of $\mathbb{N}$ by a type s trace, as
every subset of $\mathbb{N}$ is captured by a maximal contradiction-free set
of traces. ∎

Now, let us describe how we settle the complexity of Hyper2LTLfp
satisfiability and model-checking: Recall that Hyper2LTL allows set
quantification over arbitrary sets of traces while Hyper2LTLfp restricts
quantification to minimal/maximal sets of traces that satisfy a guard formula.
By using the guard $\varphi_{\mathit{allSets}}^{\prime}$ (using fresh
propositions) the minimal sets satisfying the guard are uncountable. Thus, we
can obtain every possible set over a set $\mathrm{AP}^{\prime}$ as a minimal
set satisfying the guard.

Formally, let us fix some set $\mathrm{AP}^{\prime}$ not containing the
propositions $\texttt{+},\texttt{-},\texttt{s},\texttt{x}$ used to construct
$\varphi_{\mathit{allSets}}^{\prime}$ and let
$\mathrm{AP}\subseteq\mathrm{AP}^{\prime}\cup\\{\texttt{+},\texttt{-},\texttt{s},\texttt{x}\\}$.
Then, due to Theorem 5, we have

$\\{T\mid T\text{ is the $\mathrm{AP}^{\prime}$-projection of
some~{}$T\in\mathrm{sol}(\Pi,(X,\curlyvee,\varphi_{\mathit{allSets}}^{\prime}))$}\\}$

is equal to $(2^{\mathrm{AP}^{\prime}})^{\omega}$. Hence, we can use guarded
quantification to simulate general quantification. This allows us to easily
transfer all lower bounds for Hyper2LTL to Hyper2LTLfp.

######  Theorem 6.

Hyper2LTLfp satisfiability, finite-state satisfiability, and model-checking
are polynomial-time equivalent to truth in third-order arithmetic.

###### Proof.

The upper bounds follow immediately from the analogous upper bounds for
Hyper2LTL and Proposition 3, while the lower bounds are obtained by adapting
the reductions presented in the proofs of Theorem 2, Theorem 3, and Theorem 4
by replacing

  * •

each existential second-order quantifier $\exists X$ by
$\exists(X,\curlyvee,\varphi_{\mathit{allSets}}^{\prime})$ and

  * •

each universal second-order quantifier $\forall X$ by
$\forall(X,\curlyvee,\varphi_{\mathit{allSets}}^{\prime})$.

Here, we just have to assume that the propositions in
$\varphi_{\mathit{allSets}}^{\prime}$ do not appear in the formula we are
modifying, which can always be achieved by renaming propositions, if
necessary. As explained above, the modified formulas with restricted
quantification are equivalent to the original Hyper2LTL formulas constructed
in the proofs of Theorem 2, Theorem 3, and Theorem 4, which implies the
desired lower bounds. ∎

Let us conclude by mentioning without proof (and even without definition, for
that matter) that these results can also be generalized to Hyper2LTLfp under
closed-world semantics.

##  7 Conclusion

We have investigated and settled the complexity of satisfiability and model-
checking for Hyper2LTL. All are as hard as truth in third-order arithmetic,
and therefore (not surprisingly) much harder than the corresponding problems
for HyperLTL, which are “only” $\Sigma_{1}^{1}$-complete and Tower-complete,
respectively. This shows that the addition of second-order quantification
increases the already high complexity significantly.

All our results already hold for restricted forms of second-order
quantification, i.e., for closed-world semantics and for Hyper2LTLfp, a
fragment of Hyper2LTL proposed by Beutner et al. to make model-checking more
feasible. Our results show that Hyper2LTLfp does (in general) not achieve this
goal. However, Beutner et al. presented a further syntactic restriction of
Hyper2LTLfp that guarantees quantification over unique sets. In fact, in this
fragment, quantification degenerates to a fixed-point computation of a set of
traces. They show that this fixed-point can be approximated to obtain a
partial model-checking algorithm. In future work, we investigate the
complexity and expressiveness of this fragment.

Another interesting question for future work is the addition of second-order
quantification to HyperCTL∗.

#### Acknowledgements

This work was initiated by a discussion at Dagstuhl Seminar 23391 ”The Futures
of Reactive Synthesis” and supported by DIREC – Digital Research Centre
Denmark.

## References

  * [1] Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, and Niklas Metzger.  Second-order hyperproperties.  In Constantin Enea and Akash Lal, editors, CAV 2023, Part II, volume 13965 of LNCS, pages 309–332. Springer, 2023.
  * [2] Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez.  Temporal logics for hyperproperties.  In Martín Abadi and Steve Kremer, editors, POST 2014, volume 8414 of LNCS, pages 265–284. Springer, 2014.
  * [3] Michael R. Clarkson and Fred B. Schneider.  Hyperproperties.  J. Comput. Secur., 18(6):1157–1210, 2010.
  * [4] Bernd Finkbeiner and Christopher Hahn.  Deciding hyperproperties.  In Josée Desharnais and Radha Jagadeesan, editors, CONCUR 2016, volume 59 of LIPIcs, pages 13:1–13:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
  * [5] Bernd Finkbeiner, Markus N. Rabe, and César Sánchez.  Algorithms for Model Checking HyperLTL and HyperCTL∗.  In Daniel Kroening and Corina S. Pasareanu, editors, CAV 2015, Part I, volume 9206 of LNCS, pages 30–48. Springer, 2015.
  * [6] Bernd Finkbeiner and Martin Zimmermann.  The First-Order Logic of Hyperproperties.  In STACS 2017, volume 66 of LIPIcs, pages 30:1–30:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
  * [7] Marie Fortin, Louwe B. Kuijer, Patrick Totzke, and Martin Zimmermann.  HyperLTL satisfiability is $\Sigma_{1}^{1}$-complete, HyperCTL* satisfiability is $\Sigma_{1}^{2}$-complete.  In Filippo Bonchi and Simon J. Puglisi, editors, MFCS 2021, volume 202 of LIPIcs, pages 47:1–47:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
  * [8] Marie Fortin, Louwe B. Kuijer, Patrick Totzke, and Martin Zimmermann.  HyperLTL satisfiability is highly undecidable, HyperCTL* is even harder.  arXiv, 2303.16699, 2023.  Journal version of [7]. Under submission.
  * [9] Hartley Rogers.  Theory of Recursive Functions and Effective Computability.  MIT Press, Cambridge, MA, USA, 1987.