MnLargeSymbols’164 MnLargeSymbols’171 0

11institutetext: CISPA Helmholtz Center for Information Security,
Saarbrücken, Germany
11email: {raven.beutner,finkbeiner,hadar.frenkel,
niklas.metzger} @cispa.de

# Second-Order Hyperproperties

Raven Beutner  0000-0001-6234-5651 Bernd Finkbeiner  0000-0002-4280-8441 Hadar
Frenkel  0000-0002-3566-0338 Niklas Metzger  0000-0003-3184-6335

###### Abstract

We introduce Hyper2LTL, a temporal logic for the specification of
hyperproperties that allows for second-order quantification over sets of
traces. Unlike first-order temporal logics for hyperproperties, such as
HyperLTL, Hyper2LTL can express complex epistemic properties like common
knowledge, Mazurkiewicz trace theory, and asynchronous hyperproperties. The
model checking problem of Hyper2LTL is, in general, undecidable. For the
expressive fragment where second-order quantification is restricted to
smallest and largest sets, we present an approximate model-checking algorithm
that computes increasingly precise under- and overapproximations of the
quantified sets, based on fixpoint iteration and automata learning. We report
on encouraging experimental results with our model-checking algorithm, which
we implemented in the tool HySO.

##  1 Introduction

About a decade ago, Clarkson and Schneider coined the term _hyperproperties_
[20] for the rich class of system requirements that relate multiple
computations. In their definition, hyperproperties generalize trace
properties, which are sets of traces, to _sets of_ sets of traces. This covers
a wide range of requirements, from information-flow security policies to
epistemic properties describing the knowledge of agents in a distributed
system. Missing from Clarkson and Schneider’s original theory was, however, a
concrete specification language that could express customized hyperproperties
for specific applications and serve as the common semantic foundation for
different verification methods.

A first milestone towards such a language was the introduction of the temporal
logic HyperLTL [19]. HyperLTL extends linear-time temporal logic (LTL) with
quantification over traces. Suppose, for example, that an agent $i$ in a
distributed system observes only a subset of the system variables. The agent
_knows_ that some LTL formula $\varphi$ is true on some trace $\pi$ iff
$\varphi$ holds on _all_ traces $\pi^{\prime}$ that agent $i$ cannot
distinguish from $\pi$. If we denote the indistinguishability of $\pi$ and
$\pi^{\prime}$ by $\pi\sim_{i}\pi^{\prime}$, then the property that _there
exists a trace $\pi$ where agent $i$ knows $\varphi$_ can be expressed as the
HyperLTL formula

$\displaystyle\exists\pi.\forall\pi^{\prime}\mathpunct{.}\pi\sim_{i}\pi^{\prime}\rightarrow\varphi(\pi^{\prime}),$

where we write $\varphi(\pi^{\prime})$ to denote that the trace property
$\varphi$ holds on trace $\pi^{\prime}$.

While HyperLTL and its variations have found many applications [30, 42, 27],
the expressiveness of these logics is limited, leaving many widely used
hyperproperties out of reach. A prominent example is _common knowledge_ ,
which is used in distributed applications to ensure simultaneous action [29,
38]. Common knowledge in a group of agents means that the agents not only know
_individually_ that some condition $\varphi$ is true, but that this knowledge
is “common” to the group in the sense that each agent _knows_ that every agent
_knows_ that $\varphi$ is true; on top of that, each agent in the group
_knows_ that every agent _knows_ that every agent _knows_ that $\varphi$ is
true; and so on, forming an infinite chain of knowledge.

The fundamental limitation of HyperLTL that makes it impossible to express
properties like common knowledge is that the logic is restricted to _first-
order quantification_. HyperLTL, then, cannot reason about sets of traces
directly, but must always do so by referring to individual traces that are
chosen existentially or universally from the full set of traces. For the
specification of an agent’s individual knowledge, where we are only interested
in the (non-)existence of a single trace that is indistinguishable and that
violates $\varphi$, this is sufficient; however, expressing an infinite chain,
as needed for common knowledge, is impossible.

In this paper, we introduce Hyper2LTL, a temporal logic for hyperproperties
with _second-order quantification_ over traces. In Hyper2LTL, the existence of
a trace $\pi$ where the condition $\varphi$ is common knowledge can be
expressed as the following formula (using slightly simplified syntax):

$\displaystyle\exists\pi.\,\exists X\mathpunct{.}\ \pi\in
X\land\Big{(}\forall\pi^{\prime}\in X.\,\forall\pi^{\prime\prime}.\
\big{(}\bigvee_{i=1}^{n}\pi^{\prime}\sim_{i}\pi^{\prime\prime}\big{)}\rightarrow\pi^{\prime\prime}\in
X\Big{)}\,\land\,\forall\pi^{\prime}\in
X\mathpunct{.}\varphi({\pi^{\prime}}).$

The second-order quantifier $\exists X$ postulates the existence of a set $X$
of traces that (1) contains $\pi$; that (2) is closed under the observations
of each agent, i.e., for every trace $\pi^{\prime}$ already in $X$, all other
traces $\pi^{\prime\prime}$ that some agent $i$ cannot distinguish from
$\pi^{\prime}$ are also in $X$; and that (3) only contains traces that satisfy
$\varphi$. The existence of $X$ is a necessary and sufficient condition for
$\varphi$ being common knowledge on $\pi$. In the paper, we show that
Hyper2LTL is an elegant specification language for many hyperproperties of
interest that cannot be expressed in HyperLTL, including, in addition to
epistemic properties like common knowledge, also Mazurkiewicz trace theory and
asynchronous hyperproperties.

The model checking problem for Hyper2LTL is much more difficult than for
HyperLTL. A HyperLTL formula can be checked by translating the LTL subformula
into an automaton and then applying a series of automata transformations, such
as self-composition to generate multiple traces, projection for existential
quantification, and complementation for negation [30, 8]. For Hyper2LTL, the
model checking problem is, in general, undecidable. We introduce a method that
nevertheless obtains sound results by over- and underapproximating the
quantified sets of traces. For this purpose, we study Hyper2LTLfp, a fragment
of Hyper2LTL, in which we restrict second-order quantification to the smallest
or largest set satisfying some property. For example, to check common
knowledge, it suffices to consider the _smallest_ set $X$ that is closed under
the observations of all agents. This smallest set $X$ is defined by the
(monotone) fixpoint operation that adds, in each step, all traces that are
indistinguishable to some trace already in $X$.

We develop an approximate model checking algorithm for Hyper2LTLfp that uses
bidirectional inference to deduce lower and upper bounds on second-order
variables, interposed with first-order model checking in the style of
HyperLTL. Our procedure is parametric in an oracle that provides (increasingly
precise) lower and upper bounds. In the paper, we realize the oracles with
_fixpoint iteration_ for underapproximations of the sets of traces assigned to
the second-order variables, and _automata learning_ for overapproximations. We
report on encouraging experimental results with our model-checking algorithm,
which has been implemented in a tool called HySO.

##  2 Preliminaries

For $n\in\mathbb{N}$ we define $[n]:=\\{1,\ldots,n\\}$. We assume that AP is a
finite set of atomic propositions and define $\Sigma:=2^{\text{AP}}$. For
$t\in\Sigma^{\omega}$ and $i\in\mathbb{N}$ define $t(i)\in\Sigma$ as the $i$th
element in $t$ (starting with the $0$th); and $t[i,\infty]$ for the infinite
suffix starting at position $i$. For traces
$t_{1},\ldots,t_{n}\in\Sigma^{\omega}$ we write
$\mathit{zip}(t_{1},\ldots,t_{n})\in(\Sigma^{n})^{\omega}$ for the pointwise
zipping of the traces, i.e.,
$\mathit{zip}(t_{1},\ldots,t_{n})(i):=(t_{1}(i),\ldots,t_{n}(i))$.

##### Transition systems.

A _transition system_ is a tuple $\mathcal{T}=(S,S_{0},\kappa,L)$ where $S$ is
a set of states, $S_{0}\subseteq S$ is a set of initial states,
$\kappa\subseteq S\times S$ is a transition relation, and $L:S\to\Sigma$ is a
labeling function. A path in $\mathcal{T}$ is an infinite state sequence
$s_{0}s_{1}s_{2}\cdots\in S^{\omega}$, s.t., $s_{0}\in S_{0}$, and
$(s_{i},s_{i+1})\in\kappa$ for all $i$. The associated trace is given by
$L(s_{0})L(s_{1})L(s_{2})\cdots\in\Sigma^{\omega}$ and
$\mathit{Traces}(\mathcal{T})\subseteq\Sigma^{\omega}$ denotes all traces of
$\mathcal{T}$.

##### Automata.

A _non-deterministic Büchi automaton_ (NBA) [17] is a tuple
$\mathcal{A}=(\Sigma,Q,q_{0},\delta,F)$ where $\Sigma$ is a finite alphabet,
$Q$ is a finite set of states, $Q_{0}\subseteq Q$ is the set of initial
states, $F\subseteq Q$ is a set of accepting states, and
$\delta:Q\times\Sigma\to 2^{Q}$ is the transition function. A run on a word
$u\in\Sigma^{\omega}$ is an infinite sequence of states
$q_{0}q_{1}q_{2}\cdots\in Q^{\omega}$ such that $q_{0}\in Q_{0}$ and for every
$i\in\mathbb{N}$, $q_{i+1}\in\delta(q_{i},u(i))$. The run is accepting if it
visits states in $F$ infinitely many times, and we define the language of
$\mathcal{A}$, denoted $\mathcal{L}(\mathcal{A})\subseteq\Sigma^{\omega}$, as
all infinite words on which $\mathcal{A}$ has an accepting run.

##### HyperLTL.

HyperLTL [19] is one of the most studied temporal logics for the specification
of hyperproperties. We assume that $\mathcal{V}$ is a fixed set of trace
variables. For the most part, we use variations of $\pi$ (e.g.,
$\pi,\pi^{\prime},\pi_{1},\ldots$) to denote trace variables. HyperLTL
formulas are then generated by the grammar

$\displaystyle\varphi$
$\displaystyle:=\mathbb{Q}\pi\mathpunct{.}\varphi\mid\psi$ $\displaystyle\psi$
$\displaystyle:=a_{\pi}\mid\neg\psi\mid\psi\land\psi\mid\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\psi\mid\psi\operatorname{\mathcal{U}}\psi$

where $a\in\text{AP}$ is an atomic proposition, $\pi\in\mathcal{V}{}$ is a
trace variable, $\mathbb{Q}\in\\{\forall,\exists\\}$ is a quantifier, and
$\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ and
$\operatorname{\mathcal{U}}$ are the temporal operators _next_ and _until_.

The semantics of HyperLTL is given with respect to a _trace assignment_ $\Pi$,
which is a partial mapping $\Pi:\mathcal{V}\rightharpoonup\Sigma^{\omega}$
that maps trace variables to traces. Given $\pi\in\mathcal{V}$ and
$t\in\Sigma^{\omega}$ we define $\Pi[\pi\mapsto t]$ as the updated assignment
that maps $\pi$ to $t$. For $i\in\mathbb{N}$ we define $\Pi[i,\infty]$ as the
trace assignment defined by $\Pi[i,\infty](\pi):=\Pi(\pi)[i,\infty]$, i.e., we
(synchronously) progress all traces by $i$ steps. For quantifier-free formulas
$\psi$ we follow the LTL semantics and define

$\displaystyle\Pi$ $\displaystyle\vDash a_{\pi}$ iff $\displaystyle
a\in\Pi(\pi)(0)$ $\displaystyle\Pi$ $\displaystyle\vDash\neg\psi$ iff
$\displaystyle\Pi\not\vDash\psi$ $\displaystyle\Pi$
$\displaystyle\vDash\psi_{1}\land\psi_{2}$ iff
$\displaystyle\Pi\vDash\psi_{1}\text{ and }\Pi\vDash\psi_{2}$
$\displaystyle\Pi$ $\displaystyle\vDash\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\psi$ iff
$\displaystyle\Pi[1,\infty]\vDash\psi$ $\displaystyle\Pi$
$\displaystyle\vDash\psi_{1}\operatorname{\mathcal{U}}\psi_{2}$ iff
$\displaystyle\exists
i\in\mathbb{N}\mathpunct{.}\Pi[i,\infty]\vDash\psi_{2}\text{ and }\forall
j<i\mathpunct{.}\Pi[j,\infty]\vDash\psi_{1}\,.$

The indexed atomic propositions refer to a specific path in $\Pi$, i.e.,
$a_{\pi}$ holds iff $a$ holds on the trace bound to $\pi$. Quantifiers range
over system traces:

$\displaystyle\Pi\vDash_{\mathcal{T}}\psi\text{ iff
}\Pi\vDash\psi\quad\quad\text{and}\quad\quad\Pi\vDash_{\mathcal{T}}\mathbb{Q}\pi\mathpunct{.}\varphi\text{
iff }\mathbb{Q}t\in\mathit{Traces}(\mathcal{T})\mathpunct{.}\Pi[\pi\mapsto
t]\vDash\varphi\,.$

We write $\mathcal{T}\vDash\varphi$ if $\emptyset\vDash_{\mathcal{T}}\varphi$
where $\emptyset$ denotes the empty trace assignment.

##### HyperQPTL.

HyperQPTL [43] adds – on top of the trace quantification of HyperLTL – also
propositional quantification (analogous to the propositional quantification
that QPTL [44] adds on top of LTL). For example, HyperQPTL can express a
promptness property which states that there must exist a bound (which is
common among all traces), up to which an event must have happened. We can
express this as $\exists
q.\forall\pi\mathpunct{.}\operatorname{\leavevmode\hbox to8.7pt{\vbox
to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}q\land(\neg
q)\operatorname{\mathcal{U}}a_{\pi}$ which states that there exists an
evaluation of proposition $q$ such that (1) $q$ holds at least once, and (2)
for all traces $\pi$, $a$ holds on $\pi$ before the first occurrence of $q$.
See [8] for details.

##  3 Second-Order HyperLTL

The (first-order) trace quantification in HyperLTL ranges over the set of all
system traces; we thus cannot reason about arbitrary sets of traces as
required for, e.g., common knowledge. We introduce a second-order extension of
HyperLTL by introducing second-order variables (ranging over sets of traces)
and allowing quantification over traces from any such set. We present two
variants of our logic that differ in the way quantification is resolved. In
Hyper2LTL, we quantify over arbitrary sets of traces. While this yields a
powerful and intuitive logic, second-order quantification is inherently non-
constructive. During model checking, there thus does not exist an efficient
way to even approximate possible witnesses for the sets of traces. To solve
this quandary, we restrict Hyper2LTL to Hyper2LTLfp, where we instead quantify
over sets of traces that satisfy some minimality or maximality constraint.
This allows for large fragments of Hyper2LTLfp that admit algorithmic
approximations to its model checking (by, e.g., using known techniques from
fixpoint computations [45, 46]).

###  3.1 $\text{Hyper}^{2}\text{LTL}$

Alongside the set $\mathcal{V}{}$ of trace variables, we use a set
$\mathfrak{V}{}$ of second-order variables (which we, for the most part,
denote with capital letters $X,Y,...$). We assume that there is a special
variable $\mathfrak{S}\in\mathfrak{V}{}$ that refers to the set of traces of
the given system at hand, and a variable $\mathfrak{A}\in\mathfrak{V}{}$ that
refers to the set of all traces. We define the Hyper2LTL syntax by the
following grammar:

$\displaystyle\varphi$ $\displaystyle:=\mathbb{Q}\pi\in
X\mathpunct{.}\varphi\mid\mathbb{Q}X\mathpunct{.}\varphi\mid\psi$
$\displaystyle\psi$
$\displaystyle:=a_{\pi}\mid\neg\psi\mid\psi\land\psi\mid\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\psi\mid\psi\operatorname{\mathcal{U}}\psi$

where $a\in\text{AP}{}$ is an atomic proposition, $\pi\in\mathcal{V}{}$ is a
trace variable, $X\in\mathfrak{V}{}$ is a second-order variable, and
$\mathbb{Q}\in\\{\forall,\exists\\}$ is a quantifier. We also consider the
usual derived Boolean constants ($\mathit{true}$, $\mathit{false}$) and
connectives ($\lor$, $\rightarrow$, $\leftrightarrow$) as well as the temporal
operators _eventually_ ($\operatorname{\leavevmode\hbox to8.7pt{\vbox
to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\psi:=\mathit{true}\operatorname{\mathcal{U}}\psi$)
and _globally_ ($\operatorname{\leavevmode\hbox to6.97pt{\vbox
to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\psi:=\neg\operatorname{\leavevmode\hbox
to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neg\psi$). Given a
set of atomic propositions $P\subseteq\text{AP}$ and two trace variables
$\pi,\pi^{\prime}$, we abbreviate $\pi=_{P}\pi^{\prime}:=\bigwedge_{a\in
P}(a_{\pi}\leftrightarrow a_{\pi^{\prime}})$.

#### Semantics.

Apart from a trace assignment $\Pi$ (as in the semantics of HyperLTL), we
maintain a second-order assignment $\Delta:\mathfrak{V}{}\rightharpoonup
2^{\Sigma^{\omega}}$ mapping second-order variables to _sets of traces_. Given
$X\in\mathfrak{V}$ and $A\subseteq\Sigma^{\omega}$ we define the updated
assignment $\Delta[X\mapsto A]$ as expected. Quantifier-free formulas $\psi$
are then evaluated in a fixed trace assignment as for HyperLTL (cf. Section
2). For the quantifier prefix we define:

$\displaystyle\Pi,\Delta$ $\displaystyle\vDash\psi$ iff
$\displaystyle\Pi\vDash\psi$ $\displaystyle\Pi,\Delta$
$\displaystyle\vDash\mathbb{Q}\pi\in X\mathpunct{.}\varphi$ iff
$\displaystyle\mathbb{Q}t\in\Delta(X)\mathpunct{.}\Pi[\pi\mapsto
t],\Delta\vDash\varphi$ $\displaystyle\Pi,\Delta$
$\displaystyle\vDash\mathbb{Q}X\mathpunct{.}\varphi$ iff
$\displaystyle\mathbb{Q}A\subseteq\Sigma^{\omega}\mathpunct{.}\Pi,\Delta[X\mapsto
A]\vDash\varphi$

Second-order quantification updates $\Delta$ with a set of traces, and first-
order quantification updates $\Pi$ by quantifying over traces within the set
defined by $\Delta$.

Initially, we evaluate a formula in the empty trace assignment and fix the
valuation of the special second-order variable $\mathfrak{S}$ to be the set of
all system traces and $\mathfrak{A}$ to be the set of all traces. That is,
given a system $\mathcal{T}$ and Hyper2LTL formula $\varphi$, we say that
$\mathcal{T}$ satisfies $\varphi$, written $\mathcal{T}\vDash\varphi$, if
$\emptyset,[\mathfrak{S}\mapsto\mathit{Traces}(\mathcal{T}),\mathfrak{A}\mapsto\Sigma^{\omega}]\vDash\varphi$,
where we write $\emptyset$ for the empty trace assignment. The model-checking
problem for Hyper2LTL is checking whether $\mathcal{T}\vDash\varphi$ holds.

Hyper2LTL naturally generalizes HyperLTL by adding second-order
quantification. As sets range over _arbitrary_ traces, Hyper2LTL also subsumes
the more powerful logic HyperQPTL. The proof of Lemma 1 is given in Section
0.A.1.

######  Lemma 1 ()

Hyper2LTL subsumes HyperQPTL (and thus also HyperLTL).

#### Syntactic Sugar.

In Hyper2LTL, we can quantify over traces within a second-order variable, but
we cannot state, within the body of the formula, that some path is a member of
some second-order variable. For that, we define $\pi\triangleright X$ (as an
atom within the body) as syntactic sugar for $\exists\pi^{\prime}\in
X.\operatorname{\leavevmode\hbox to6.97pt{\vbox
to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(\pi^{\prime}=_{\text{AP}}\pi)$,
i.e., $\pi$ is in $X$ if there exists some trace in $X$ that agrees with $\pi$
on all propositions. Note that we can only use $\pi\triangleright X$ _outside_
of the scope of any temporal operators; this ensures that we can bring the
resulting formula into a form that conforms to the Hyper2LTL syntax.

###  3.2 $\text{Hyper}^{2}\text{LTL}_{fp}$

The semantics of Hyper2LTL quantifies over arbitrary sets of traces, making
even approximations to its semantics challenging. We propose Hyper2LTLfp as a
restriction that only quantifies over sets that are subject to an additional
minimality or maximality constraint. For large classes of formulas, we show
that this admits effective model-checking approximations. We define
Hyper2LTLfp by the following grammar:

$\displaystyle\varphi$ $\displaystyle:=\mathbb{Q}\,\pi\in
X\mathpunct{.}\varphi\mid\mathbb{Q}\,(X,\mathbin{\mathchoice{{\ooalign{\hfil$\displaystyle\curlywedge$\hfil\cr\hfil$\displaystyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\curlywedge$\hfil\cr\hfil$\textstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\curlywedge$\hfil\cr\hfil$\scriptstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\curlywedge$\hfil\cr\hfil$\scriptscriptstyle\curlyvee$\hfil\cr}}}}{},\varphi)\mathpunct{.}\varphi\mid\psi$
$\displaystyle\psi$
$\displaystyle:=a_{\pi}\mid\neg\psi\mid\psi\land\psi\mid\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\psi\mid\psi\operatorname{\mathcal{U}}\psi$

where $a\in\text{AP}$, $\pi\in\mathcal{V}{}$, $X\in\mathfrak{V}$,
$\mathbb{Q}\in\\{\forall,\exists\\}$, and
$\mathbin{\mathchoice{{\ooalign{\hfil$\displaystyle\curlywedge$\hfil\cr\hfil$\displaystyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\curlywedge$\hfil\cr\hfil$\textstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\curlywedge$\hfil\cr\hfil$\scriptstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\curlywedge$\hfil\cr\hfil$\scriptscriptstyle\curlyvee$\hfil\cr}}}}{}\in\\{\curlywedge,\curlyvee\\}$
determines if we consider smallest ($\curlyvee$) or largest ($\curlywedge$)
sets. For example, the formula
$\exists\,(X,\curlyvee,\varphi_{1})\mathpunct{.}\varphi_{2}$ holds if there
exists some set of traces $X$, that satisfies both $\varphi_{1}$ and
$\varphi_{2}$, and is _a_ smallest set that satisfies $\varphi_{1}$. Such
minimality and maximality constraints with respect to a (hyper)property arise
naturally in many properties. Examples include common knowledge (cf. Section
3.3), asynchronous hyperproperties (cf. Section 4.2), and causality in
reactive systems [22, 21].

#### Semantics.

For path formulas, the semantics of Hyper2LTLfp is defined analogously to that
of Hyper2LTL and HyperLTL. For the quantifier prefix we define:

$\displaystyle\Pi,\Delta$ $\displaystyle\vDash\psi$ iff
$\displaystyle\Pi\vDash\psi$ $\displaystyle\Pi,\Delta$
$\displaystyle\vDash\mathbb{Q}\pi\in X\mathpunct{.}\varphi$ iff
$\displaystyle\mathbb{Q}t\in\Delta(X)\mathpunct{.}\Pi[\pi\mapsto
t],\Delta\vDash\varphi$ $\displaystyle\Pi,\Delta$
$\displaystyle\vDash\mathbb{Q}(X,\mathbin{\mathchoice{{\ooalign{\hfil$\displaystyle\curlywedge$\hfil\cr\hfil$\displaystyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\curlywedge$\hfil\cr\hfil$\textstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\curlywedge$\hfil\cr\hfil$\scriptstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\curlywedge$\hfil\cr\hfil$\scriptscriptstyle\curlyvee$\hfil\cr}}}}{},\varphi_{1})\mathpunct{.}\varphi_{2}$
iff
$\displaystyle\mathbb{Q}A\in\mathit{sol}(\Pi,\Delta,(X,\mathbin{\mathchoice{{\ooalign{\hfil$\displaystyle\curlywedge$\hfil\cr\hfil$\displaystyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\curlywedge$\hfil\cr\hfil$\textstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\curlywedge$\hfil\cr\hfil$\scriptstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\curlywedge$\hfil\cr\hfil$\scriptscriptstyle\curlyvee$\hfil\cr}}}}{},\varphi_{1}))\mathpunct{.}\Pi,\Delta[X\mapsto
A]\vDash\varphi_{2}$

where
$\mathit{sol}(\Pi,\Delta,(X,\mathbin{\mathchoice{{\ooalign{\hfil$\displaystyle\curlywedge$\hfil\cr\hfil$\displaystyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\curlywedge$\hfil\cr\hfil$\textstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\curlywedge$\hfil\cr\hfil$\scriptstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\curlywedge$\hfil\cr\hfil$\scriptscriptstyle\curlyvee$\hfil\cr}}}}{},\varphi_{1}))$
denotes all solutions to the minimality/maximality condition given by
$\varphi_{1}$, which we define by mutual recursion as follows:
$\displaystyle\mathit{sol}(\Pi,\Delta,(X,\curlyvee,\varphi))$
$\displaystyle:=\\{A\subseteq\Sigma^{\omega}\mid\Pi,\Delta[X\mapsto
A]\vDash\varphi\land\forall A^{\prime}\subsetneq
A\mathpunct{.}\Pi,\Delta[X\mapsto A^{\prime}]\not\vDash\varphi\\}$
$\displaystyle\mathit{sol}(\Pi,\Delta,(X,\curlywedge,\varphi))$
$\displaystyle:=\\{A\subseteq\Sigma^{\omega}\mid\Pi,\Delta[X\mapsto
A]\vDash\varphi\land\forall A^{\prime}\supsetneq
A\mathpunct{.}\Pi,\Delta[X\mapsto A^{\prime}]\not\vDash\varphi\\}$
A set $A$ satisfies the minimality/maximality constraint if it satisfies
$\varphi$ and is a least (in case
$\mathbin{\mathchoice{{\ooalign{\hfil$\displaystyle\curlywedge$\hfil\cr\hfil$\displaystyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\curlywedge$\hfil\cr\hfil$\textstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\curlywedge$\hfil\cr\hfil$\scriptstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\curlywedge$\hfil\cr\hfil$\scriptscriptstyle\curlyvee$\hfil\cr}}}}{}=\curlyvee$)
or greatest (in case
$\mathbin{\mathchoice{{\ooalign{\hfil$\displaystyle\curlywedge$\hfil\cr\hfil$\displaystyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\curlywedge$\hfil\cr\hfil$\textstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\curlywedge$\hfil\cr\hfil$\scriptstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\curlywedge$\hfil\cr\hfil$\scriptscriptstyle\curlyvee$\hfil\cr}}}}{}=\curlywedge$)
set that satisfies $\varphi$.

Note that
$\mathit{sol}(\Pi,\Delta,(X,\mathbin{\mathchoice{{\ooalign{\hfil$\displaystyle\curlywedge$\hfil\cr\hfil$\displaystyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\curlywedge$\hfil\cr\hfil$\textstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\curlywedge$\hfil\cr\hfil$\scriptstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\curlywedge$\hfil\cr\hfil$\scriptscriptstyle\curlyvee$\hfil\cr}}}}{},\varphi))$
can contain multiple sets or no set at all, i.e., there may not exists a
unique least or greatest set that satisfies $\varphi$. In Hyper2LTLfp, we
therefore add an additional quantification over the set of all solutions to
the minimality/maximality constraint. When discussing our model checking
approximation algorithm, we present a (syntactic) restriction on $\varphi$
which guarantees that
$\mathit{sol}(\Pi,\Delta,(X,\mathbin{\mathchoice{{\ooalign{\hfil$\displaystyle\curlywedge$\hfil\cr\hfil$\displaystyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\curlywedge$\hfil\cr\hfil$\textstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\curlywedge$\hfil\cr\hfil$\scriptstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\curlywedge$\hfil\cr\hfil$\scriptscriptstyle\curlyvee$\hfil\cr}}}}{},\varphi))$
contains a unique element (i.e., is a singleton set). Moreover, our
restriction allows us to employ fixpoint techniques to find approximations to
this unique solution. In case the solution for
$(X,\mathbin{\mathchoice{{\ooalign{\hfil$\displaystyle\curlywedge$\hfil\cr\hfil$\displaystyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\curlywedge$\hfil\cr\hfil$\textstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\curlywedge$\hfil\cr\hfil$\scriptstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\curlywedge$\hfil\cr\hfil$\scriptscriptstyle\curlyvee$\hfil\cr}}}}{},\varphi)$
is unique, we often omit the leading quantifier and simply write
$(X,\mathbin{\mathchoice{{\ooalign{\hfil$\displaystyle\curlywedge$\hfil\cr\hfil$\displaystyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\curlywedge$\hfil\cr\hfil$\textstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\curlywedge$\hfil\cr\hfil$\scriptstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\curlywedge$\hfil\cr\hfil$\scriptscriptstyle\curlyvee$\hfil\cr}}}}{},\varphi)$
instead of
$\mathbb{Q}(X,\mathbin{\mathchoice{{\ooalign{\hfil$\displaystyle\curlywedge$\hfil\cr\hfil$\displaystyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\curlywedge$\hfil\cr\hfil$\textstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\curlywedge$\hfil\cr\hfil$\scriptstyle\curlyvee$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\curlywedge$\hfil\cr\hfil$\scriptscriptstyle\curlyvee$\hfil\cr}}}}{},\varphi)$.

As we can encode the minimality/maximality constraints of Hyper2LTLfp in
Hyper2LTL (see Section 0.A.2), we have the following:

######  Proposition 1 ()

Any Hyper2LTLfp formula $\varphi$ can be effectively translated into an
Hyper2LTL formula $\varphi^{\prime}$ such that for all transition systems
$\mathcal{T}$ we have $\mathcal{T}\vDash\varphi$ iff
$\mathcal{T}\vDash\varphi^{\prime}$.

$b$ $a$ $d$ $c$ ptptpt

$\displaystyle\pi=$ $\displaystyle\ a^{n}d^{\omega}$ $\displaystyle
K_{2}(\pi)=$ $\displaystyle\ a^{n-1}bd^{\omega}$ $\displaystyle
K_{1}K_{2}(\pi)=$ $\displaystyle\ a^{n-1}cd^{\omega}$ $\displaystyle
K_{2}K_{1}K_{2}(\pi)=$ $\displaystyle\ a^{n-2}bcd^{\omega}$
$\displaystyle\ldots$ $\displaystyle K_{1}K_{2}\ldots K_{2}(\pi)=$
$\displaystyle\ ac^{n-1}d^{\omega}$

Figure 1: Left: An example for a multi-agent system with two agents, where
agent 1 observes $a$ and $d$, and agent 2 observes $c$ and $d$. Right: The
iterative construction of the traces to be considered for common knowledge
starting with $a^{n}d^{\omega}$.

###  3.3 Common Knowledge in Multi-Agent Systems

To explain common knowledge, we use a variation of an example from [41], and
encode it in Hyper2LTLfp. Figure 1(left) shows a transition system of a
distributed system with two agents, agent $1$ and agent $2$. Agent $1$
observes variables $a$ and $d$, whereas agent $2$ observes $c$ and $d$. The
property of interest is _starting from the trace $\pi=a^{n}d^{\omega}$ for
some fixed $n>1$, is it common knowledge for the two agents that $a$ holds in
the second step_. It is trivial to see that $\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}a$ holds on $\pi$.
However, for common knowledge, we consider the (possibly) infinite chain of
observationally equivalent traces. For example, agent $2$ cannot distinguish
the traces $a^{n}d^{\omega}$ and $a^{n-1}bd^{\omega}$. Therefore, agent $2$
only knows that $\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}a$ holds on $\pi$ if
it also holds on $\pi^{\prime}=a^{n-1}bd^{\omega}$. For common knowledge,
agent $1$ also has to know that agent $2$ knows
$\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}a$, which means that
for all traces that are indistinguishable from $\pi$ or $\pi^{\prime}$ for
agent $1$, $\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}a$ has to hold. This
adds $\pi^{\prime\prime}=a^{n-1}cd^{\omega}$ to the set of traces to verify
$\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}a$ against. This
chain of reasoning continues as shown in Figure 1(right). In the last step we
add $ac^{n-1}d^{\omega}$ to the set of indistinguishable traces, concluding
that $\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}a$ is not common
knowledge.

The following Hyper2LTLfp formula specifies the property stated above. The
abbreviation $\mathit{obs}(\pi_{1},\pi_{2}):=\operatorname{\leavevmode\hbox
to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(\pi_{1}=_{\\{a,d\\}}\pi_{2})\vee\operatorname{\leavevmode\hbox
to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(\pi_{1}=_{\\{c,d\\}}\pi_{2})$
denotes that $\pi_{1}$ and $\pi_{2}$ are observationally equivalent for either
agent 1 or agent 2.

$\displaystyle\forall\pi\in\mathfrak{S}.\big{(}\bigwedge_{i=0}^{n-1}\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{i}a_{\pi}\land\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{n}\operatorname{\leavevmode\hbox
to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}d_{\pi}\big{)}\to$
$\displaystyle\quad\Big{(}X,\curlyvee,\pi\triangleright
X\land\big{(}\forall\pi_{1}\in
X.\forall\pi_{2}\in\mathfrak{S}{}\mathpunct{.}\mathit{obs}(\pi_{1},\pi_{2})\rightarrow\pi_{2}\triangleright
X\big{)}\Big{)}\mathpunct{.}\forall\pi^{\prime}\in
X.\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}a_{\pi^{\prime}}$

For a trace $\pi$ of the form $\pi=a^{n}d^{\omega}$, the set $X$ represents
the _common knowledge set_ on $\pi$. This set $X$ is the smallest set that (1)
contains $\pi$ (expressed using our syntactic sugar $\triangleright$); and (2)
is closed under observations by either agent, i.e., if we find some
$\pi_{1}\in X$ and some system trace $\pi_{2}$ that are observationally
equivalent, $\pi_{2}$ should also be in $X$. Note that this set is unique (due
to the minimality restriction), so we do not quantify it explicitly. Lastly,
we require that all traces in $X$ satisfy the property
$\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}a$. All sets that
satisfy this formula would also include the trace $ac^{n-1}d^{\omega}$, and
therefore no such $X$ exists; thus, we can conclude that starting from trace
$a^{n}d^{\omega}$, it is _not_ common knowledge that
$\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}a$ holds.

On the other hand, it _is_ common knowledge that $a$ holds in the _first_ step
(cf. Section 6).

###  3.4 $\text{Hyper}^{2}\text{LTL}$ Model Checking

As Hyper2LTL and Hyper2LTLfp allow quantification over arbitrary sets of
traces, we can encode the satisfiability of HyperQPTL (i.e., the question of
whether some set of traces satisfies a formula) within their model-checking
problem; rendering the model-checking problem highly undecidable [32], even
for very simple formulas [4].

######  Proposition 2 ()

For any HyperQPTL formula $\varphi$ there exists a Hyper2LTL formula
$\varphi^{\prime}$ such that $\varphi$ is satisfiable iff $\varphi^{\prime}$
holds on some arbitrary transition system. The model-checking problem of
Hyper2LTL is thus highly undecidable ($\Sigma_{1}^{1}$-hard).

###### Proof

Let $\varphi^{\prime}$ be the Hyper2LTL formula obtained from $\varphi$ by
replacing each HyperQPTL trace quantifier $\mathbb{Q}\pi$ with the Hyper2LTL
quantifier $\mathbb{Q}\pi\in X$, and each propositional quantifier
$\mathbb{Q}q$ with $\mathbb{Q}\pi_{q}\in\mathfrak{A}$ for some fresh trace
variable $\pi_{q}$. In the body, we replace each propositional variable $q$
with $a_{\pi_{q}}$ for some fixed proposition $a\in\text{AP}$. Then, $\varphi$
is satisfiable iff the Hyper2LTL formula $\exists X.\varphi^{\prime}$ holds in
some arbitrary system. ∎

Hyper2LTLfp cannot express HyperQPTL satisfiability directly. If there exists
a model of a HyperQPTL formula, there may not exist a least one. However,
model checking of Hyper2LTLfp is also highly undecidable.

######  Proposition 3 ()

The model-checking problem of Hyper2LTLfp is $\Sigma_{1}^{1}$-hard.

######  Proof (Sketch)

We can encode the existence of a _recurrent_ computation of a Turing machine,
which is known to be $\Sigma_{1}^{1}$-hard [1].∎

Conversely, the _existential_ fragment of Hyper2LTL can be encoded back into
HyperQPTL satisfiability:

######  Proposition 4 ()

Let $\varphi$ be a Hyper2LTL formula that uses only existential second-order
quantification and $\mathcal{T}$ be any system. We can effectively construct a
formula $\varphi^{\prime}$ in HyperQPTL such that $\mathcal{T}\vDash\varphi$
iff $\varphi^{\prime}$ is satisfiable.

Lastly, we present some easy fragments of Hyper2LTL for which the model-
checking problem is decidable. Here we write $\exists^{*}X$ (resp.
$\forall^{*}X$) for some sequence of existentially (resp. universally)
quantified _second-order_ variables and $\exists^{*}\pi$ (resp.
$\forall^{*}\pi$) for some sequence of existentially (resp. universally)
quantified _first-order_ variables. For example, $\exists^{*}X\forall^{*}\pi$
captures all formulas of the form $\exists X_{1},\ldots
X_{n}.\forall\pi_{1},\ldots,\pi_{m}.\psi$ where $\psi$ is quantifier-free.

######  Proposition 5 ()

The model-checking problem of Hyper2LTL is decidable for the fragments:
$\exists^{*}X\forall^{*}\pi$, $\forall^{*}X\forall^{*}\pi$,
$\exists^{*}X\exists^{*}\pi$, $\forall^{*}X\exists^{*}\pi$, $\exists
X.\exists^{*}\pi\in X\forall^{*}\pi^{\prime}\in X$.

See Section 0.A.3 for the full proofs of the propositions above.

##  4 Expressiveness of $\text{Hyper}^{2}\text{LTL}$

In this section, we point to existing logics that can naturally be encoded
within our second-order hyperlogics Hyper2LTL and Hyper2LTLfp.

###  4.1 $\text{Hyper}^{2}\text{LTL}$ and LTLK,C

LTLK extends LTL with the knowledge operator $\mathsf{K}$. For some subset of
agents $A$, the formula $\mathsf{K}_{A}\psi$ holds in timestep $i$, if $\psi$
holds on all traces equivalent to some agent in $A$ up to timestep $i$. See
Section 0.B.1 for detailed semantics. LTLK and HyperCTL∗ have incomparable
expressiveness [15] but the knowledge operator $\mathsf{K}$ can be encoded by
either adding a linear past operator [15] or by adding propositional
quantification (as in HyperQPTL) [43].

Using Hyper2LTLfp we can encode LTLK,C, featuring the knowledge operator
$\mathsf{K}$ _and_ the common knowledge operator $\mathsf{C}$ (which requires
that $\psi$ holds on the closure set of equivalent traces, up to the current
timepoint) [39]. Note that LTLK,C is not encodable by only adding
propositional quantification or the linear past operator.

######  Proposition 6 ()

For every _LTL K,C_ formula $\varphi$ there exists an Hyper2LTLfp formula
$\varphi^{\prime}$ such that for any system $\mathcal{T}$ we have
$\mathcal{T}\vDash_{\text{LTL${}_{\mathsf{K},\mathsf{C}}$}}\varphi$ iff
$\mathcal{T}\vDash\varphi^{\prime}$.

######  Proof (Sketch)

We follow the intuition discussed in Section 3.3. For each occurrence of a
knowledge operator in $\\{\mathsf{K},\mathsf{C}\\}$, we introduce a second-
order set that collects all equivalent traces, and a fresh trace variable that
keeps track on the points in time with respect to which we need to compare. We
then inductively construct a Hyper2LTLfp formula that captures all the
knowledge and common-knowledge sets. For more details see Section 0.B.1. ∎

###  4.2 $\text{Hyper}^{2}\text{LTL}$ and Asynchronous Hyperproperties

Most existing hyperlogics (including Hyper2LTL) traverse the traces of a
system _synchronously_. However, in many cases such a synchronous traversal is
too restricting and we need to compare traces asynchronously. As an example,
consider _observational determinism_ (OD), which we can express in HyperLTL as
$\varphi_{\mathit{OD}}:=\forall\pi_{1}.\forall\pi_{2}.\operatorname{\leavevmode\hbox
to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(o_{\pi_{1}}\leftrightarrow
o_{\pi_{2}})$. The formula states that the output of a system is identical
across all traces and so (trivially) no information about high-security inputs
is leaked. In most systems encountered in practice, this synchronous formula
is violated, as the exact timing between updates to $o$ might differ by a few
steps (see Section 0.B.2 for some examples). However, assuming that an
attacker only has access to the memory footprint and not a timing channel, we
would only like to check that all traces are _stutter_ equivalent (with
respect to $o$).

A range of extensions to existing hyperlogics has been proposed to reason
about such asynchronous hyperproperties [3, 16, 37, 5, 9]. We consider AHLTL
[3]. An AHLTL formula has the form
$\mathbb{Q}_{1}\pi_{1},\ldots,\mathbb{Q}_{n}\pi_{m}.\mathbf{E}\mathpunct{.}\psi$
where $\psi$ is a qunatifier-free HyperLTL formula. The initial trace
quantifier prefix is handled as in HyperLTL. However, different from HyperLTL,
a trace assignment $[\pi_{1}\mapsto t_{1},\ldots,\pi_{n}\mapsto t_{n}]$
satisfies $\mathbf{E}\mathpunct{.}\psi$ if there exist stuttered traces
$t_{1}^{\prime},\ldots,t_{n}^{\prime}$ of $t_{1},\ldots,t_{n}$ such that
$[\pi_{1}\mapsto t_{1}^{\prime},\ldots,\pi_{n}\mapsto
t_{n}^{\prime}]\vDash\psi$. We write
$\mathcal{T}\vDash_{\mathit{AHLTL}}\varphi$ if a system $\mathcal{T}$
satisfies the AHLTL formula $\varphi$. Using this quantification over
stutterings we can, for example, express an asynchronous version of
observational determinism as
$\forall\pi_{1}.\forall\pi_{2}.\mathbf{E}\mathpunct{.}\operatorname{\leavevmode\hbox
to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(o_{\pi_{1}}\leftrightarrow
o_{\pi_{2}})$ stating that every two traces can be aligned such that they
(globally) agree on $o$. Despite the fact that Hyper2LTLfp is itself
synchronous, we can use second-order quantification to encode asynchronous
hyperproperties, as we state in the following proposition.

###### Proposition 7

For any AHLTL formula $\varphi$ there exists a Hyper2LTLfp formula
$\varphi^{\prime}$ such that for any system $\mathcal{T}$ we have
$\mathcal{T}\vDash_{\mathit{AHLTL}}\varphi$ iff
$\mathcal{T}\vDash\varphi^{\prime}$.

###### Proof

Assume that
$\varphi=\mathbb{Q}_{1}\pi_{1},\ldots,\mathbb{Q}_{n}\pi_{n}.\mathbf{E}\mathpunct{.}\psi$
is the given AHLTL formula. For each $i\in[n]$ we define a formula
$\varphi_{i}$ as follows

$\displaystyle\forall\pi_{1}\in
X_{i}.\forall\pi_{2}\in\mathfrak{A}{}\mathpunct{.}\Big{(}\big{(}\pi_{1}=_{\text{AP}}\pi_{2}\big{)}\operatorname{\mathcal{U}}\big{(}\operatorname{\leavevmode\hbox
to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\bigwedge_{a\in\text{AP}}a_{\pi_{1}}\leftrightarrow\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}a_{\pi_{2}}\big{)}\Big{)}\rightarrow\pi_{2}\triangleright
X_{i}$

The formula asserts that the set of traces bound to $X_{i}$ is closed under
stuttering, i.e., if we start from any trace in $X_{i}$ and stutter it once
(at some arbitrary position) we again end up in $X_{i}$. Using the formulas
$\varphi_{i}$, we then construct a Hyper2LTLfp formula that is equivalent to
$\varphi$ as follows

$\displaystyle\varphi^{\prime}:=\,$
$\displaystyle\mathbb{Q}_{1}\pi_{1}\in\mathfrak{S}{},\ldots,\mathbb{Q}_{n}\pi_{n}\in\mathfrak{S}{}.(X_{1},\curlyvee,\pi_{1}\triangleright
X_{1}\land\varphi_{1})\cdots(X_{n},\curlyvee,\pi_{n}\triangleright
X_{n}\land\varphi_{n})$ $\displaystyle\quad\quad\exists\pi_{1}^{\prime}\in
X_{1},\ldots,\exists\pi_{n}^{\prime}\in
X_{n}.\psi[\pi_{1}^{\prime}/\pi_{1},\ldots,\pi_{n}^{\prime}/\pi_{n}]$

We first mimic the quantification in $\varphi$ and, for each trace $\pi_{i}$,
construct a least set $X_{i}$ that contains $\pi_{i}$ and is closed under
stuttering (thus describing exactly the set of all stuttering of $\pi_{i}$).
Finally, we assert that there are traces
$\pi_{1}^{\prime},\ldots,\pi_{n}^{\prime}$ with $\pi_{i}^{\prime}\in X_{i}$
(so $\pi_{i}^{\prime}$ is a stuttering of $\pi_{i}$) such that
$\pi_{1}^{\prime},\ldots,\pi_{n}^{\prime}$ satisfy $\psi$. It is easy to see
that $\mathcal{T}\vDash_{\mathit{AHLTL}}\varphi$ iff
$\mathcal{T}\vDash\varphi^{\prime}$ holds for all systems. ∎

Hyper2LTLfp captures all properties expressible in AHLTL. In particular, our
approximate model-checking algorithm for Hyper2LTLfp (cf. Section 5) is
applicable to AHLTL; even for instances where no approximate solutions were
previously known. In Section 6, we show that our prototype model checker for
Hyper2LTLfp can verify asynchronous properties in practice.

##  5 Model-Checking $\text{Hyper}^{2}\text{LTL}_{fp}$

In general, finite-state model checking of Hyper2LTLfp is highly undecidable
(cf. Proposition 2). In this section, we outline a partial algorithm that
computes approximations on the concrete values of second-order variables for a
fragment of Hyper2LTLfp. At a very high-level, our algorithm (Algorithm 1)
iteratively computes under- and overapproximations for second-order variables.
It then turns to resolve first-order quantification, using techniques from
HyperLTL model checking [30, 8], and resolves existential and universal trace
quantification on the under- and overapproximation of the second-order
variables, respectively. If the verification fails, it goes back to refine
second-order approximations.

In this section, we focus on the setting where we are interested in the least
sets (using $\curlyvee$), and use techniques to approximate the _least_
fixpoint. A similar (dual) treatment is possible for Hyper2LTLfp formulas that
use the largest set. Every Hyper2LTLfp which uses only minimal sets has the
following form:

$\displaystyle\varphi=\gamma_{1}.(Y_{1},\curlyvee,\varphi^{\mathit{con}}_{1}).\gamma_{2}\ldots.(Y_{k},\curlyvee{},\varphi^{\mathit{con}}_{k})\mathpunct{.}\gamma_{k+1}\mathpunct{.}\psi$
(1)

We quantify second-order variables $Y_{1},\ldots,Y_{k}$, where, for each
$j\in[k]$, $Y_{j}$ is the least set that satisfies
$\varphi^{\mathit{con}}_{j}$. Finally, for each $j\in[k+1]$,

$\displaystyle\gamma_{j}=\mathbb{Q}_{l_{j}+1}\pi_{l_{j}+1}\in
X_{l_{j}+1}\ldots\mathbb{Q}_{l_{j+1}}\pi_{l_{j+1}}\in X_{l_{j+1}}$

is the block of first-order quantifiers that sits between the quantification
of $Y_{j-1}$ and $Y_{j}$. Here
$X_{l_{j}+1},\ldots,X_{l_{j+1}}\in\\{\mathfrak{S},\mathfrak{A},Y_{1},\ldots,Y_{j-1}\\}$
are second-order variables that are quantified before $\gamma_{j}$. In
particular, $\pi_{1},\ldots,\pi_{l_{j}}$ are the first-order variables
quantified before $Y_{j}$.

###  5.1 Fixpoints in $\text{Hyper}^{2}\text{LTL}_{fp}$

We consider a fragment of Hyper2LTLfp which we call the _least fixpoint
fragment_. Within this fragment, we restrict the formulas
$\varphi^{\mathit{con}}_{1},\ldots,\varphi^{\mathit{con}}_{k}$ such that
$Y_{1},\ldots,Y_{k}$ can be approximated as (least) fixpoints. Concretely, we
say that $\varphi$ is in the _least fixpoint fragment_ of Hyper2LTLfp if for
all $j\in[k]$, $\varphi^{\mathit{con}}_{j}$ is a conjunction of formulas of
the form

$\displaystyle\forall\dot{\pi}_{1}\in X_{1}.\ldots\forall\dot{\pi}_{n}\in
X_{n}\mathpunct{.}\psi_{\mathit{step}}\rightarrow\dot{\pi}_{M}\triangleright
Y_{j}$ (2)

where each $X_{i}\in\\{\mathfrak{S},\mathfrak{A},Y_{1},\ldots,Y_{j}\\}$,
$\psi_{\mathit{step}}$ is quantifier-free formula over trace variables
$\dot{\pi}_{1},\ldots,\dot{\pi}_{n},\pi_{1},\ldots,\pi_{l_{j}}$, and
$M\in[n]$. Intuitively, Equation 2 states a requirement on traces that should
be included in $Y_{j}$. If we find traces $\dot{t}_{1}\in
X_{1},\ldots,\dot{t}_{n}\in X_{n}$ that, together with the traces
$t_{1},\ldots,t_{l_{j}}$ quantified before $Y_{j}$, satisfy
$\psi_{\mathit{step}}$, then $\dot{t}_{M}$ should be included in $Y_{j}$.

Together with the minimality constraint on $Y_{j}$ (stemming from the
semantics of Hyper2LTLfp), this effectively defines a (monotone) least
fixpoint computation, as $\psi_{\mathit{step}}$ defines exactly the traces to
be added to the set. This will allow us to use results from fixpoint theory to
compute approximations for the sets $Y_{j}$.

Our least fixpoint fragment captures most properties of interest, in
particular, common knowledge (Section 3.3) and asynchronous hyperproperties
(Section 4.2). We observe that formulas of the above form ensure that the
solution $Y_{j}$ is unique, i.e., for any trace assignment $\Pi$ to
$\pi_{1},\ldots,\pi_{l_{j}}$ and second-order assignment $\Delta$ to
$\mathfrak{S},\mathfrak{A},Y_{1},\ldots,Y_{j-1}$, there is only one element in
$\mathit{sol}(\Pi,\Delta,(Y_{j},\curlyvee,\varphi_{j}^{\mathit{con}}))$.

###  5.2 Functions as Automata

In our (approximate) model-checking algorithm, we represent a concrete
assignment to the second-order variables $Y_{1},\ldots,Y_{k}$ using automata
$\mathcal{B}_{Y_{1}},\ldots,\mathcal{B}_{Y_{k}}$. The concrete assignment of
$Y_{j}$ can depend on traces assigned to $\pi_{1},\ldots,\pi_{l_{j}}$, i.e.,
the first-order variables quantified before $Y_{j}$. To capture these
dependencies, we view each $Y_{j}$ not as a set of traces but as a function
mapping traces of all preceding first-order variables to a set of traces. We
represent such a function $f:(\Sigma^{\omega})^{l_{j}}\to
2^{(\Sigma^{\omega})}$ mapping the $l_{j}$ traces to a set of traces as an
automaton $\mathcal{A}$ over $\Sigma^{l_{j}+1}$. For traces
$t_{1},\ldots,t_{l_{j}}$, the set $f(t_{1},\ldots,t_{l_{j}})$ is represented
in the automaton by the set
$\\{t\in\Sigma^{\omega}\mid\mathit{zip}(t_{1},\ldots,t_{l_{j}},t)\in\mathcal{L}(\mathcal{A})\\}$.
For example, the function $f(t_{1}):=\\{t_{1}\\}$ can be defined by the
automaton that accepts the zipping of a pair of traces exactly if both traces
agree on all propositions. This representation of functions as automata allows
us to maintain an assignment to $Y_{j}$ that is parametric in
$\pi_{1},\ldots,\pi_{l_{j}}$ and still allows first-order model checking on
$Y_{1},\ldots,Y_{k}$.

###  5.3 Model Checking for First-Order Quantification

First, we focus on first-order quantification, and assume that we are given a
concrete assignment for each second-order variable as fixed automata
$\mathcal{B}_{Y_{1}},\ldots,\mathcal{B}_{Y_{k}}$ (where $\mathcal{B}_{Y_{j}}$
is an automaton over $\Sigma^{l_{j}+1}$). Our construction for resolving
first-order quantification is based on HyperLTL model checking [30], but needs
to work on sets of traces that, themselves, are based on traces quantified
before (cf. Section 5.2). Recall that the first-order quantifier prefix is
$\gamma_{1}\cdots\gamma_{k+1}=\mathbb{Q}_{1}\pi_{1}\in
X_{1}\cdots\mathbb{Q}_{l_{k+1}}\pi_{l_{k+1}}\in X_{l_{k+1}}$. For each $1\leq
i\leq l_{k+1}$ we inductively construct an automaton $\mathcal{A}_{i}$ over
$\Sigma^{i-1}$ that summarizes all trace assignments to
$\pi_{1},\ldots,\pi_{i-1}$ that satisfy the subformula starting with the
quantification of $\pi_{i}$. That is, for all traces $t_{1},\ldots,t_{i-1}$ we
have

$\displaystyle[\pi_{1}\mapsto t_{1},\ldots,\pi_{i-1}\mapsto
t_{i-1}]\vDash\mathbb{Q}_{i}\pi_{i}\in
X_{i}\cdots\mathbb{Q}_{l_{k+1}}\pi_{l_{k+1}}\in X_{l_{k+1}}\mathpunct{.}\psi$

(under the fixed second-order assignment for $Y_{1},\ldots,Y_{k}$ given by
$\mathcal{B}_{Y_{1}},\ldots,\mathcal{B}_{Y_{k}}$) if and only if
$\mathit{zip}(t_{1},\ldots,t_{i-1})\in\mathcal{L}(\mathcal{A}_{i})$. In the
context of HyperLTL model checking we say $\mathcal{A}_{i}$ is _equivalent_ to
$\mathbb{Q}_{i}\pi_{i}\in X_{i}\cdots\mathbb{Q}_{l_{k+1}}\pi_{l_{k+1}}\in
X_{l_{k+1}}\mathpunct{.}\psi$ [30, 8]. In particular, $\mathcal{A}_{1}$ is an
automaton over singleton alphabet $\Sigma^{0}$.

We construct $\mathcal{A}_{1},\ldots,\mathcal{A}_{l_{k+1}+1}$ inductively,
starting with $\mathcal{A}_{l_{k+1}+1}$. Initially, we construct
$\mathcal{A}_{l_{k+1}+1}$ (over $\Sigma^{l_{k+1}}$) using a standard LTL-to-
NBA construction on the (quantifier-free) body $\psi$ (see [30] for details).
Now assume that we are given an (inductively constructed) automaton
$\mathcal{A}_{i+1}$ over $\Sigma^{i}$ and want to construct $\mathcal{A}_{i}$.
We first consider the case where $\mathbb{Q}_{i}=\exists$, i.e., the $i$th
trace quantification is existential. Now $X_{i}$ (the set where $\pi_{i}$ is
resolved on) either equals $\mathfrak{S}$, $\mathfrak{A}$ or $Y_{j}$ for some
$j\in[k]$. In either case, we represent the current assignment to $X_{i}$ as
an automaton $\mathcal{C}$ over $\Sigma^{T+1}$ for some $T<i$ that defines the
model of $X_{i}$ based on traces $\pi_{1},\ldots,\pi_{T}$: In case
$X_{i}=\mathfrak{S}$, we set $\mathcal{C}$ to be the automaton over
$\Sigma^{0+1}$ that accepts exactly the traces in the given system
$\mathcal{T}$; in case $X_{i}=\mathfrak{A}$, we set $\mathcal{C}$ to be the
automaton over $\Sigma^{0+1}$ that accepts all traces; If $X_{i}=Y_{j}$ for
some $j\in[k]$ we set $\mathcal{C}$ to be $\mathcal{B}_{Y_{j}}$ (which is an
automaton over $\Sigma^{l_{j}+1}$).111Note that in this case $l_{j}<i$: if
trace $\pi_{i}$ is resolved on $Y_{j}$ (i.e, $X_{i}=Y_{j}$), then $Y_{j}$ must
be quantified _before_ $\pi_{i}$ so there are at most $i-1$ traces quantified
before $Y_{j}$.  Given $\mathcal{C}$, we can now modify the construction from
[30], to resolve first-order quantification: The desired automaton
$\mathcal{A}_{i}$ should accept the zipping of traces $t_{1},\ldots,t_{i-1}$
if there exists a trace $t$ such that (1)
$\mathit{zip}(t_{1},\ldots,t_{i-1},t)\in\mathcal{L}(\mathcal{A}_{i+1})$, _and_
(2) the trace $t$ is contained in the set of traces assigned to $X_{i}$ as
given by $\mathcal{C}$, i.e.,
$\mathit{zip}(t_{1},\ldots,t_{T},t)\in\mathcal{L}(\mathcal{C})$. The
construction of this automaton is straightforward by taking a product of
$\mathcal{A}_{i+1}$ and $\mathcal{C}$. We denote this automaton with
eProduct($\mathcal{A}_{i+1}$,$\mathcal{C}$). In case $\mathbb{Q}_{i}=\forall$
we exploit the duality that $\forall\pi.\psi$ = $\neg\exists\pi.\neg\psi$,
combining the above construction with automata complementation. We denote this
universal product of $\mathcal{A}_{i+1}$ and $\mathcal{C}$ with
uProduct($\mathcal{A}_{i+1}$,$\mathcal{C}$).

The final automaton $\mathcal{A}_{1}$ is an automaton over singleton alphabet
$\Sigma^{0}$ that is equivalent to $\gamma_{1}\cdots\gamma_{k+1}.\psi$, i.e.,
the entire first-order quantifier prefix. Automaton $\mathcal{A}_{1}$ thus
satisfies $\mathcal{L}(\mathcal{A}_{1})\neq\emptyset$ (which we can decide)
iff the empty trace assignment satisfies the first-order formula
$\gamma_{1}\cdots\gamma_{k+1}\mathpunct{.}\psi$, iff $\varphi$ (of Equation 1)
holds within the fixed model for $Y_{1},\ldots,Y_{k}$. For a given fixed
second-order assignment (given as automata
$\mathcal{B}_{Y_{1}},\ldots,\mathcal{B}_{Y_{k}}$), we can thus decide if the
system satisfies the first-order part.

During the first-order model-checking phase, each quantifier alternations in
the formula require complex automata complementation. For the first-order
phase, we could also use cheaper approximate methods by, e.g., instantiating
the existential trace using a strategy [24, 7, 6].

###  5.4 Bidirectional Model Checking

So far, we have discussed the verification of the first-order quantifiers
assuming we have a fixed model for all second-order variables
$Y_{1},\ldots,Y_{k}$. In our actual model-checking algorithm, we instead
maintain under- and overapproximations on each of the $Y_{1},\ldots,Y_{k}$.

Algorithm 1

⬇

let $\varphi$ = $\big[\gamma_j \; (Y_j, \smallestSet ,
\varphi_j^\mathit{con})\big]_{j=1}^k \; \gamma_{k+1}\ldot \psi$ where
$\gamma_i$ = $\big[\quant_m \pi_m \in X_m \big]_{m=l_i+1}^{l_{i+1}} $

let N = 0

let $\calA_\calT$ = systemToNBA($\calT$)

repeat

// Start outside-in traversal on second-order variables

let $\flat$ = $\big[\systemvar \mapsto (\calA_\calT,\calA_\calT), \allvar
\mapsto (\calA_\top, \calA_\top)\big]$

for $j$ from $1$ to $k$ do

$\calB_j^l$ := underApprox($(Y_j,\smallestSet,
\varphi_j^\mathit{con})$,$\flat$,$N$)

$\calB_j^u$ := overApprox($(Y_j,\smallestSet,
\varphi_j^\mathit{con})$,$\flat$,$N$)

$\flat(Y_j)$ := $(\calB_j^l,\calB_j^u)$

// Start inside-out traversal on first-order variables

let $\calA_{l_{k+1} + 1}$ = LTLtoNBA($\psi$)

for $i$ from $l_{k+1}$ to $1$ do

let $(\calC^l, \calC^u)$ = $\flat(X_i)$

if $\quant_i = \exists$ then

$\calA_i$ := eProduct($\calA_{i+1}$, $\calC^l$)

else

$\calA_i$ := uProduct($\calA_{i+1}$, $\calC^u$)

if $\calL(\calA_1) \neq \emptyset$ then

return SAT

else

$N$ = $N$ + 1

In each iteration, we first traverse the second-order quantifiers in an
_outside-in_ direction and compute lower- and upper-bounds on each $Y_{j}$.
Given the bounds, we then traverse the first-order prefix in an _inside-out_
direction using the current approximations to $Y_{1},\ldots,Y_{k}$. If the
current approximations are not precise enough to witness the satisfaction (or
violation) of a property, we repeat and try to compute better bounds on
$Y_{1},\ldots,Y_{k}$. Due to the different directions of traversal, we refer
to our model-checking approach as _bidirectional_. Algorithm 1 provides an
overview. Initially, we convert the system $\mathcal{T}$ to an NBA
$\mathcal{A}_{\mathcal{T}}$ accepting exactly the traces of the system. In
each round, we compute under- and overapproximations for each $Y_{j}$ in a
mapping $\flat$. We initialize $\flat$ by mapping $\mathfrak{S}$ to
$(\mathcal{A}_{\mathcal{T}},\mathcal{A}_{\mathcal{T}})$ (i.e., the value
assigned to the system variable is precisely $\mathcal{A}_{\mathcal{T}}$ for
both under- and overapproximation), and $\mathfrak{A}$ to
$(\mathcal{A}_{\top},\mathcal{A}_{\top})$ where $\mathcal{A}_{\top}$ is an
automaton over $\Sigma^{1}$ accepting all traces. We then traverse the second-
order quantifiers outside-in (from $Y_{1}$ to $Y_{k}$) and for each $Y_{j}$
compute a pair $(\mathcal{B}_{j}^{l},\mathcal{B}_{j}^{u})$ of automata over
$\Sigma^{l_{j}+1}$ that under- and overapproximate the actual (unique) model
of $Y_{j}$. We compute these approximations using functions underApprox and
overApprox, which can be instantiated with any procedure that computes sound
lower and upper bounds (see Section 5.5). During verification, we further
maintain a precision bound $N$ (initially set to $0$) that tracks the current
precision of the second-order approximations.

When $\flat$ contains an under- and overapproximation for each second-order
variable, we traverse the first-order variables in an inside-out direction
(from $\pi_{l_{k+1}}$ to $\pi_{1}$) and, following the construction outlined
in Section 5.3, construct automata
$\mathcal{A}_{l_{k}+1},\ldots,\mathcal{A}_{1}$. Different from the simplified
setting in Section 5.3 (where we assume a fixed automaton
$\mathcal{B}_{Y_{j}}$ providing a model for each $Y_{j}$), the mapping $\flat$
contains only approximations of the concrete solution. We choose which
approximation to use according to the corresponding set quantification: In
case we construct $\mathcal{A}_{i}$ and $\mathbb{Q}_{i}=\exists$, we use the
_underapproximation_ (thus making sure that any witness trace we pick is
indeed contained in the actual model of the second-order variable); and if
$\mathbb{Q}_{i}=\forall$, we use the _overapproximation_ (making sure that we
consider at least those traces that are in the actual solution). If
$\mathcal{L}(\mathcal{A}_{1})$ is non-empty, i.e., accepts the empty trace
assignment, the formula holds (assuming the approximations returned by
underApprox and overApprox are sound). If not, we increase the precision bound
$N$ and repeat.

In Algorithm 1, we only check for the satisfaction of a formula (to keep the
notation succinct). Using the second-order approximations in $\flat$ we can
also check the negation of a formula (by considering the negated body and
dualizing all trace quantifiers). Our tool (Section 6) makes use of this and
thus simultaneously tries to show satisfaction and violation of a formula.

###  5.5 Computing Under- and Overapproximations

In this section we provide concrete instantiations for underApprox and
overApprox.

#### Computing Underapproximations.

As we consider the fixpoint fragment, each formula
$\varphi_{j}^{\mathit{con}}$ (defining $Y_{j}$) is a conjunction of formulas
of the form in Equation 2, thus defining $Y_{j}$ via a least fixpoint
computation. For simplicity, we assume that $Y_{j}$ is defined by the single
conjunct, given by Equation 2 (our construction generalizes easily to a
conjunction of such formulas). Assuming fixed models for $\mathfrak{S}$,
$\mathfrak{A}$ and $Y_{1},\ldots,Y_{j-1}$, the fixpoint operation defining
$Y_{j}$ is monotone, i.e., the larger the current model for $Y_{j}$ is, the
more traces we need to add according to Equation 2. Monotonicity allows us to
apply the Knaster–Tarski theorem [45] and compute underapproximations to the
fixpoint by iteration.

In our construction of an approximation for $Y_{j}$, we are given a mapping
$\flat$ that fixes a pair of automata for $\mathfrak{S}$, $\mathfrak{A}$, and
$Y_{1},\ldots,Y_{j-1}$ (due to the outside-in traversal in Algorithm 1). As we
are computing an underapproximation, we use the underapproximation for each of
the second-order variables in $\flat$. So $\flat(\mathfrak{S})$ and
$\flat(\mathfrak{A})$ are automata over $\Sigma^{1}$ and for each
$j^{\prime}\in[j-1]$, $\flat(Y_{j^{\prime}})$ is an automaton over
$\Sigma^{l_{j^{\prime}}+1}$. Given this fixed mapping $\flat$, we iteratively
construct automata $\hat{\mathcal{C}}_{0},\hat{\mathcal{C}}_{1},\ldots$ over
$\Sigma^{l_{j}+1}$ that capture (increasingly precise) underapproximations on
the solution for $Y_{j}$. We set $\hat{\mathcal{C}}_{0}$ to be the automaton
with the empty language. We then recursively define $\hat{\mathcal{C}}_{N+1}$
based on $\hat{\mathcal{C}}_{N}$ as follows: For each second-order variable
$X_{i}$ for $i\in[n]$ used in Equation 2 we can assume a concrete assignment
in the form of an automaton $\mathcal{D}_{i}$ over $\Sigma^{T_{i}+1}$ for some
$T_{i}\leq l_{j}$: In case $X_{i}\neq Y_{j}$ (so
$X_{i}\in\\{\mathfrak{S},\mathfrak{A},Y_{1},\ldots,Y_{j-1}\\}$), we set
$\mathcal{D}_{i}:=\flat(X_{i})$. In case $X_{i}=Y_{j}$, we set
$\mathcal{D}_{i}:=\hat{\mathcal{C}}_{N}$, i.e., we use the current
approximation of $Y_{j}$ in iteration $N$. After we have set
$\mathcal{D}_{1},\ldots,\mathcal{D}_{n}$, we compute an automaton
$\dot{\mathcal{C}}$ over $\Sigma^{l_{j}+1}$ that accepts
$\mathit{zip}(t_{1},\ldots,t_{l_{j}},t)$ iff there exists traces
$\dot{t}_{1},\ldots,\dot{t}_{n}$ such that (1)
$\mathit{zip}(t_{1},\ldots,t_{T_{i}},\dot{t}_{i})\in\mathcal{L}(\mathcal{D}_{i})$
for all $i\in[n]$, (2) $[\pi_{1}\mapsto t_{1},\ldots,\pi_{l_{j}}\mapsto
t_{l_{j}},\dot{\pi}_{1}\mapsto\dot{t}_{1},\ldots,\dot{\pi}_{n}\mapsto\dot{t}_{n}]\vDash\psi_{\mathit{step}}$,
and (3) trace $t$ equals $\dot{t}_{M}$ (of Equation 2). The intuition is that
$\dot{\mathcal{C}}$ captures all traces that should be added to $Y_{j}$: Given
$t_{1},\ldots,t_{l_{j}}$ we check if there are traces
$\dot{t}_{1},\ldots,\dot{t}_{n}$ for trace variables
$\dot{\pi}_{1},\ldots,\dot{\pi}_{n}$ in Equation 2 where (1) each
$\dot{t}_{i}$ is in the assignment for $X_{i}$, which is captured by the
automaton $\mathcal{D}_{i}$ over $\Sigma^{T_{i}+1}$, and (2) the traces
$\dot{t}_{1},\ldots,\dot{t}_{n}$ satisfy $\varphi_{\mathit{step}}$. If this is
the case, we want to add $\dot{t}_{M}$ (as stated in Equation 2). We then
define $\hat{\mathcal{C}}_{N+1}$ as the union of $\hat{\mathcal{C}}_{N}$ and
$\dot{\mathcal{C}}$, i.e. extend the previous model with all (potentially new)
traces that need to be added.

#### Computing Overapproximations.

As we noted above, conditions of the form of Equation 2 always define fixpoint
constraints. To compute upper bounds on such fixpoint constructions we make
use of Park’s theorem, [46] stating that if we find some set (or automaton)
$\mathcal{B}$ that is inductive (i.e., when computing all traces that we would
need to add assuming the current model of $Y_{j}$ is $\mathcal{B}$, we end up
with traces that are already in $\mathcal{B}$), then $\mathcal{B}$
overapproximates the unique solution (aka. least fixpoint) of $Y_{j}$. To
derive such an inductive invariant, we employ techniques developed in the
context of regular model checking [14] (see Section 7). Concretely, we employ
the approach from [18] that uses automata learning [2] to find suitable
invariants. While the approach from [18] is limited to finite words, we extend
it to an $\omega$-setting by interpreting an automaton accepting finite words
as one that accepts an $\omega$-word $u$ iff every prefix of $u$ is
accepted.222This effectively poses the assumption that the step formula
specifies a safety property, which seems to be the case for almost all
examples. As an example, common knowledge infers a safety property: In each
step, we add all traces for which there exists some trace that agrees on all
propositions observed by that agent. As soon as the learner provides a
candidate for an equivalence check, we check that it is inductive and, if not,
provide some finite counterexample (see [18] for details). If the automaton is
inductive, we return it as a potential overapproximation. Should this
approximation not be precise enough, the first-order model checking (Section
5.3) returns some concrete counterexample, i.e., some trace contained in the
invariant but violating the property, which we use to provide more
counterexamples to the learner.

##  6 Implementation and Experiments

We have implemented our model-checking algorithm in a prototype tool we call
HySO (Hyperproperties with Second Order).333Our tool is publicly available at
https://zenodo.org/record/7878311. Our tool uses spot [28] for basic automata
operations (such as LTL-to-NBA translations and complementations). To compute
under- and overapproximations, we use the techniques described in Section 5.5.
We evaluate the algorithm on the following benchmarks.

#### Muddy Children.

The muddy children puzzle [29] is one of the classic examples in common
knowledge literature. The puzzle consists of $n$ children standing such that
each child can see all other children’s faces. From the $n$ children, an
unknown number $k\geq 1$ have a muddy forehead, and in incremental rounds, the
children should step forward if they know if their face is muddy or not.
Consider the scenario of $n=2$ and $k=1$, so child $a$ sees that child $b$ has
a muddy forehead and child $b$ sees that $a$ is clean. In this case, $b$
immediately steps forward, as it knows that its forehead is muddy since $k\geq
1$. In the next step, $a$ knows that its face is clean since $b$ stepped
forward in round 1. In general, one can prove that all children step forward
in round $k$, deriving common knowledge.

For each $n$ we construct a transition system $\mathcal{T}_{n}$ that encodes
the muddy children scenario with $n$ children. For every $m$ we design a
Hyper2LTLfp formula $\varphi_{m}$ that adds to the common knowledge set $X$
all traces that appear indistinguishable in the first $m$ steps for some
child. We then specify that all traces in $X$ should agree on all inputs,
asserting that all inputs are common knowledge.444This property is not
expressible in non-hyper logics such as LTLK,C, where we can only check _trace
properties_ on the common knowledge set $X$. In contrast, Hyper2LTLfp allows
us to check _hyperproperties_ on $X$. That way, we can express that some value
is common knowledge (i.e., equal across all traces in the set) and not only
that a property is common knowledge (i.e., holds on all traces in the set). We
used HySO to _fully automatically_ check $\mathcal{T}_{n}$ against
$\varphi_{m}$ for varying values of $n$ and $m$, i.e., we checked if, after
the first $m$ steps, the inputs of all children are common knowledge. As
expected, the above property holds only if $m\geq n$ (in the worst case, where
all children are dirty $(k=n)$, the inputs of all children only become common
knowledge after $n$ steps). We depict the results in Table 1(a).

|  | m
---|---|---
|  | 1 | 2 | 3 | 4
n | 2 |  ✗ 0.64 |  ✓ 0.59 |  |
3 |  ✗ 0.79 |  ✗ 0.75 |  ✓ 0.54 |
4 |  ✗ 2.72 |  ✗ 2.21 |  ✗ 1.67 |  ✓ 1.19
(a)

Instance | Method | Res | $\boldsymbol{t}$
---|---|---|---
$\mathcal{T}_{\mathit{syn}}$, $\varphi_{\mathit{OD}}$ | - | ✓ | 0.26
$\mathcal{T}_{\mathit{asyn}}$, $\varphi_{\mathit{OD}}$ | - | ✗ | 0.31
$\mathcal{T}_{\mathit{syn}}$, $\varphi^{\mathit{asyn}}_{\mathit{OD}}$ | Iter (0) | ✓ | 0.50
$\mathcal{T}_{\mathit{syn}}$, $\varphi^{\mathit{asyn}}_{\mathit{OD}}$ | Iter (1) | ✓ | 0.78
Q1, $\varphi_{\mathit{OD}}$ | - | ✗ | 0.34
Q1, $\varphi^{\mathit{asyn}}_{\mathit{OD}}$ | Iter (1) | ✓ | 0.86
(b)

Table 1:  In Table 1(a), we check common knowledge in the muddy children
puzzle for $n$ children and $m$ rounds. We give the result (✓ if common
knowledge holds and ✗ if it does not), and the running time. In Table 1(b), we
check synchronous and asynchronous versions of observational determinism. We
depict the number of iterations needed and running time. Times are given in
seconds.

#### Asynchronous Hyperproperties.

As we have shown in Section 4.2, we can encode arbitrary AHLTL properties into
Hyper2LTLfp. We verified synchronous and asynchronous version of observational
determinism (cf. Section 4.2) on programs taken from [3, 5, 9]. We depict the
verification results in Table 1(b). Recall that Hyper2LTLfp properties without
any second-order variables correspond to HyperQPTL formulas. HySO can check
such properties precisely, i.e., it constitutes a sound-and-complete model
checker for HyperQPTL properties with an arbitrary quantifier prefix. The
synchronous version of observational determinism is a HyperLTL property and
thus needs no second-order approximation (we set the method column to “-” in
these cases).

#### Common Knowledge in Multi-agent Systems.

We used HySO for an automatic analysis of the system in Figure 1. Here, we
verify that on initial trace $\\{a\\}^{n}\\{d\\}^{\omega}$ it is CK that $a$
holds in the first step. We use a similar formula as the one of Section 3.3,
with the change that we are interested in whether $a$ is CK (whereas we used
$\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}a$ in Section 3.3).
As expected, HySO requires $2n-1$ iterations to converge. We depict the
results in Table 2(a).

$\boldsymbol{n}$ | Method | Res | $\boldsymbol{t}$
---|---|---|---
1 | Iter (1) | ✓ | 0.51
2 | Iter (3) | ✓ | 0.83
3 | Iter (5) | ✓ | 1.20
10 | Iter (19) | ✓ | 3.81
100 | Iter (199) | ✓ | 102.8
(a)

Instance | Method | Res | $\boldsymbol{t}$
---|---|---|---
SwapA | Learn | ✓ | 1.07
SwapATwice | Learn | ✓ | 2.13
SwapA5 | Iter (5) | ✓ | 1.15
SwapA15 | Iter (15) | ✓ | 3.04
SwapAViolation5 | Iter (5) | ✗ | 2.35
SwapAViolation15 | Iter (15) | ✗ | 4.21
(b)

Table 2:  In Table 1(a), we check common knowledge in the example from Figure
1 when starting with $a^{n}d^{\omega}$ for varying values of $n$. We depict
the number of refinement iterations, the result, and the running time. In
Table 2(b), we verify various properties on Mazurkiewicz traces. We depict
whether the property could be verified or refuted by iteration or automata
learning, the result, and the time. Times are given in seconds.

#### Mazurkiewicz Traces.

Mazurkiewicz traces are an important concept in the theory of distributed
computing [26]. Let $I\subseteq\Sigma\times\Sigma$ be an independence relation
that determines when two consecutive letters can be switched (think of two
actions in disjoint processes in a distributed system). Any
$t\in\Sigma^{\omega}$ then defines the set of all traces that are equivalent
to $t$ by flipping consecutive independent actions an arbitrary number of
times (the equivalence class of all these traces is called the Mazurkiewicz
Trace). See [26] for details. The verification problem for Mazurkiewicz traces
now asks if, given some $t\in\Sigma^{\omega}$, all traces in the Mazurkiewicz
trace of $t$ satisfy some property $\psi$. Using Hyper2LTLfp we can directly
reason about the Mazurkiewicz Trace of any given trace, by requiring that all
traces that are equal up to one swap of independent letters are also in a
given set (which is easily expressed in Hyper2LTLfp).

Using HySO we verify a selection of such trace properties that often require
non-trivial reasoning by coming up with a suitable invariant. We depict the
results in Table 2(b). In our preliminary experiments, we model a situation
where we start with $\\{a\\}^{1}\\{\\}^{\omega}$ and can swap letters
$\\{a\\}$ and $\\{\\}$. We then, e.g., ask if on any trace in the resulting
Mazurkiewicz trace, $a$ holds at most once, which requires inductive
invariants and cannot be established by iteration.

##  7 Related Work

In recent years, many logics for the formal specification of hyperproperties
have been developed, extending temporal logics with explicit path
quantification (examples include HyperLTL, HyperCTL∗ [19], HyperQPTL [43, 10],
HyperPDL [36], and HyperATL∗ [5, 9]); extending first and second-order logics
with an equal level predicate [24, 31]; or extending ($\omega$)-regular
hyperproperties [35, 13] to context-free hyperproperties [33]. Hyper2LTL is
the first temporal logic that reasons about second-order hyperproperties which
allows is to capture many existing (epistemic, asynchronous, etc.) hyperlogics
while at the same time taking advantage of model-checking solutions that have
been proven successful in first-order settings.

##### Asynchronous Hyperproperties.

For asynchronous hyperproperties, Gutfeld et al. [37] present an asynchronous
extension of the polyadic $\mu$-calculus. Bozelli et al. [16] extend HyperLTL
with temporal operators that are only evaluated if the truth value of some
temporal formula changes. Baumeister et al. present AHLTL [3], that extends
HyperLTL with a explicit quantification over trajectories and can be directly
encoded within Hyper2LTLfp.

##### Regular Model Checking.

Regular model checking [14] is a general verification method for (possibly
infinite state) systems, in which each state of the system is interpreted as a
finite word. The transitions of the system are given as a finite-state
(regular) transducer, and the model checking problem asks if, from some
initial set of states (given as a regular language), some bad state is
eventually reachable. Many methods for automated regular model checking have
been developed [11, 25, 12, 18]. Hyper2LTL can be seen as a logical foundation
for $\omega$-regular model checking: Assume the set of initial states is given
as a QPTL formula $\varphi_{\mathit{init}}$, the set of bad states is given as
a QPTL formula $\varphi_{\mathit{bad}}$, and the transition relation is given
as a QPTL formula $\varphi_{\mathit{step}}$ over trace variables $\pi$ and
$\pi^{\prime}$. The set of bad states is reachable from a trace (state) in
$\varphi_{\mathit{init}}$ iff the following Hyper2LTLfp formula holds on the
system that generates all traces:

$\displaystyle\big{(}X,\curlyvee,\forall\pi\in\mathfrak{S}\mathpunct{.}\varphi_{\mathit{init}}(\pi)\rightarrow\pi\triangleright
X\land$ $\displaystyle\quad\quad\quad\forall\pi\in
X.\forall\pi^{\prime}\in\mathfrak{S}\mathpunct{.}\varphi_{\mathit{step}}(\pi,\pi^{\prime})\rightarrow\pi^{\prime}\triangleright
X\big{)}\mathpunct{.}\forall\pi\in X.\neg\varphi_{\mathit{bad}}(\pi)$

Conversely, Hyper2LTLfp can express more complex properties, beyond the
reachability checks possible in the framework of ($\omega$-)regular model
checking.

##### Model Checking Knowledge.

Model checking of knowledge properties in multi-agent systems was developed in
the tools MCK [34] and MCMAS [40], which can exactly express LTLK. Bozzelli et
al. [15] have shown that HyperCTL∗ and LTLK have incomparable expressiveness,
and present HyperCTL${}^{*}_{lp}$ – an extension of HyperCTL∗ that can reason
about past – to unify HyperCTL∗ and LTLK. While HyperCTL${}^{*}_{lp}$ can
express the knowledge operator, it cannot capture common knowledge. LTLK,C
[39] captures both knowledge and common knowledge, but the suggested model-
checking algorithm only handles a decidable fragment that is reducible to LTL
model checking.

##  8 Conclusion

Hyperproperties play an increasingly important role in many areas of computer
science. There is a strong need for specification languages and verification
methods that reason about hyperproperties in a uniform and general manner,
similar to what is standard for more traditional notions of safety and
reliability. In this paper, we have ventured forward from the first-order
reasoning of logics like HyperLTL into the realm of second-order
hyperproperties, i.e., properties that not only compare individual traces but
reason comprehensively about _sets_ of such traces. With Hyper2LTL, we have
introduced a natural specification language and a general model-checking
approach for second-order hyperproperties. Hyper2LTL provides a general
framework for a wide range of relevant hyperproperties, including common
knowledge and asynchronous hyperproperties, which could previously only be
studied with specialized logics and algorithms. Hyper2LTL also provides a
starting point for future work on second-order hyperproperties in areas such
as cyber-physical [42] and probabilistic systems [27].

#### Acknowledgements.

We thank Jana Hofmann for the fruitful discussions. This work was supported by
the European Research Council (ERC) Grant HYPER (No. 101055412), by DFG grant
389792660 as part of TRR 248, and by the German Israeli Foundation (GIF) Grant
No. I-1513-407.2019.

## References

  * [1] Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1) (1994). https://doi.org/10.1145/174644.174651
  * [2] Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2) (1987). https://doi.org/10.1016/0890-5401(87)90052-6
  * [3] Baumeister, J., Coenen, N., Bonakdarpour, B., Finkbeiner, B., Sánchez, C.: A temporal logic for asynchronous hyperproperties. In: International Conference on Computer Aided Verification, CAV 2021. Lecture Notes in Computer Science, vol. 12759. Springer (2021). https://doi.org/10.1007/978-3-030-81685-8_33
  * [4] Beutner, R., Carral, D., Finkbeiner, B., Hofmann, J., Krötzsch, M.: Deciding hyperproperties combined with functional specifications. In: Annual ACM/IEEE Symposium on Logic in Computer, LICS 2022. ACM (2022). https://doi.org/10.1145/3531130.3533369
  * [5] Beutner, R., Finkbeiner, B.: A temporal logic for strategic hyperproperties. In: International Conference on Concurrency Theory, CONCUR 2021. LIPIcs, vol. 203. Schloss Dagstuhl (2021). https://doi.org/10.4230/LIPIcs.CONCUR.2021.24
  * [6] Beutner, R., Finkbeiner, B.: Prophecy variables for hyperproperty verification. In: IEEE Computer Security Foundations Symposium, CSF 2022. IEEE (2022). https://doi.org/10.1109/CSF54842.2022.9919658
  * [7] Beutner, R., Finkbeiner, B.: Software verification of hyperproperties beyond k-safety. In: International Conference on Computer Aided Verification, CAV 2022\. Lecture Notes in Computer Science, vol. 13371. Springer (2022). https://doi.org/10.1007/978-3-031-13185-1_17
  * [8] Beutner, R., Finkbeiner, B.: AutoHyper: Explicit-state model checking for HyperLTL. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023. vol. 13993. Springer (2023). https://doi.org/10.1007/978-3-031-30823-9_8
  * [9] Beutner, R., Finkbeiner, B.: HyperATL∗: A logic for hyperproperties in multi-agent systems. Log. Methods Comput. Sci. (2023)
  * [10] Beutner, R., Finkbeiner, B.: Model checking omega-regular hyperproperties with AutoHyperQ. In: International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2023. EPiC Series in Computing, EasyChair (2023)
  * [11] Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: International Conference on Computer Aided Verification, CAV 2003. Lecture Notes in Computer Science, vol. 2725. Springer (2003). https://doi.org/10.1007/978-3-540-45069-6_24
  * [12] Boigelot, B., Legay, A., Wolper, P.: Omega-regular model checking. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004. Lecture Notes in Computer Science, vol. 2988. Springer (2004). https://doi.org/10.1007/978-3-540-24730-2_41
  * [13] Bonakdarpour, B., Sheinvald, S.: Finite-word hyperlanguages. In: Leporati, A., Martín-Vide, C., Shapira, D., Zandron, C. (eds.) Language and Automata Theory and Applications - 15th International Conference, LATA 2021, Milan, Italy, March 1-5, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12638, pp. 173–186. Springer (2021). https://doi.org/10.1007/978-3-030-68195-1_17, https://doi.org/10.1007/978-3-030-68195-1_17
  * [14] Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: International Conference on Computer Aided Verification, CAV 2000. Lecture Notes in Computer Science, vol. 1855. Springer (2000). https://doi.org/10.1007/10722167_31
  * [15] Bozzelli, L., Maubert, B., Pinchinat, S.: Unifying hyper and epistemic temporal logics. In: International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2015. Lecture Notes in Computer Science, vol. 9034. Springer (2015). https://doi.org/10.1007/978-3-662-46678-0_11
  * [16] Bozzelli, L., Peron, A., Sánchez, C.: Asynchronous extensions of HyperLTL. In: Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021. IEEE (2021). https://doi.org/10.1109/LICS52264.2021.9470583
  * [17] Büchi, J.R.: On a decision method in restricted second-order arithmetic. In: Studies in Logic and the Foundations of Mathematics. vol. 44. Elsevier (1966)
  * [18] Chen, Y., Hong, C., Lin, A.W., Rümmer, P.: Learning to prove safety over parameterised concurrent systems. In: Formal Methods in Computer Aided Design, FMCAD 2017. IEEE (2017). https://doi.org/10.23919/FMCAD.2017.8102244
  * [19] Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: International Conference on Principles of Security and Trust, POST 2014. Lecture Notes in Computer Science, vol. 8414. Springer (2014). https://doi.org/10.1007/978-3-642-54792-8_15
  * [20] Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6) (2010). https://doi.org/10.3233/JCS-2009-0393
  * [21] Coenen, N., Dachselt, R., Finkbeiner, B., Frenkel, H., Hahn, C., Horak, T., Metzger, N., Siber, J.: Explaining hyperproperty violations. In: International Conference on Computer Aided Verification, CAV 2022. Lecture Notes in Computer Science, vol. 13371. Springer (2022). https://doi.org/10.1007/978-3-031-13185-1_20
  * [22] Coenen, N., Finkbeiner, B., Frenkel, H., Hahn, C., Metzger, N., Siber, J.: Temporal causality in reactive systems. In: International Symposium on Automated Technology for Verification and Analysis, ATVA 2022. Lecture Notes in Computer Science, vol. 13505. Springer (2022). https://doi.org/10.1007/978-3-031-19992-9_13
  * [23] Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J.: The hierarchy of hyperlogics. In: Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. IEEE (2019). https://doi.org/10.1109/LICS.2019.8785713
  * [24] Coenen, N., Finkbeiner, B., Sánchez, C., Tentrup, L.: Verifying hyperliveness. In: International Conference on Computer Aided Verification, CAV 2019. Lecture Notes in Computer Science, vol. 11561. Springer (2019). https://doi.org/10.1007/978-3-030-25540-4_7
  * [25] Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. In: International Conference on Computer Aided Verification, CAV 2001. Lecture Notes in Computer Science, vol. 2102. Springer (2001). https://doi.org/10.1007/3-540-44585-4_27
  * [26] Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific (1995). https://doi.org/10.1142/2563
  * [27] Dimitrova, R., Finkbeiner, B., Torfah, H.: Probabilistic hyperproperties of markov decision processes. In: International Symposium on Automated Technology for Verification and Analysis, ATVA 2020. Lecture Notes in Computer Science, vol. 12302. Springer (2020). https://doi.org/10.1007/978-3-030-59152-6_27
  * [28] Duret-Lutz, A., Renault, E., Colange, M., Renkin, F., Aisse, A.G., Schlehuber-Caissier, P., Medioni, T., Martin, A., Dubois, J., Gillard, C., Lauko, H.: From spot 2.0 to spot 2.10: What’s new? In: International Conference on Computer Aided Verification, CAV 2022. Lecture Notes in Computer Science, vol. 13372. Springer (2022). https://doi.org/10.1007/978-3-031-13188-2_9
  * [29] Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press (1995). https://doi.org/10.7551/mitpress/5803.001.0001
  * [30] Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for model checking HyperLTL and HyperCTL*. In: International Conference on Computer Aided Verification, CAV 2015. Lecture Notes in Computer Science, vol. 9206. Springer (2015). https://doi.org/10.1007/978-3-319-21690-4_3
  * [31] Finkbeiner, B., Zimmermann, M.: The first-order logic of hyperproperties. In: Symposium on Theoretical Aspects of Computer Science, STACS 2017. LIPIcs, vol. 66. Schloss Dagstuhl (2017). https://doi.org/10.4230/LIPIcs.STACS.2017.30
  * [32] Fortin, M., Kuijer, L.B., Totzke, P., Zimmermann, M.: HyperLTL satisfiability is $\Sigma_{1}^{1}$-complete, HyperCTL* satisfiability is $\Sigma_{1}^{2}$-complete. In: International Symposium on Mathematical Foundations of Computer Science, MFCS 2021. LIPIcs, vol. 202. Schloss Dagstuhl (2021). https://doi.org/10.4230/LIPIcs.MFCS.2021.47
  * [33] Frenkel, H., Sheinvald, S.: Realizable and context-free hyperlanguages. In: Ganty, P., Monica, D.D. (eds.) Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2022, Madrid, Spain, September 21-23, 2022. EPTCS, vol. 370, pp. 114–130 (2022). https://doi.org/10.4204/EPTCS.370.8, https://doi.org/10.4204/EPTCS.370.8
  * [34] Gammie, P., van der Meyden, R.: MCK: model checking the logic of knowledge. In: International Conference on Computer Aided Verification, CAV 2004. Lecture Notes in Computer Science, vol. 3114. Springer (2004). https://doi.org/10.1007/978-3-540-27813-9_41
  * [35] Goudsmid, O., Grumberg, O., Sheinvald, S.: Compositional model checking for multi-properties. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12597, pp. 55–80. Springer (2021). https://doi.org/10.1007/978-3-030-67067-2_4, https://doi.org/10.1007/978-3-030-67067-2_4
  * [36] Gutsfeld, J.O., Müller-Olm, M., Ohrem, C.: Propositional dynamic logic for hyperproperties. In: International Conference on Concurrency Theory, CONCUR 2020. LIPIcs, vol. 171. Schloss Dagstuhl (2020). https://doi.org/10.4230/LIPIcs.CONCUR.2020.50
  * [37] Gutsfeld, J.O., Müller-Olm, M., Ohrem, C.: Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang. 5(POPL) (2021). https://doi.org/10.1145/3434319
  * [38] Halpern, J.Y., Moses, Y.: Knowledge and common knowledge in a distributed environment. J. ACM 37(3), 549–587 (1990)
  * [39] van der Hoek, W., Wooldridge, M.J.: Model checking knowledge and time. In: International Workshop on Model Checking of Software, SPIN 2002. Lecture Notes in Computer Science, vol. 2318. Springer (2002). https://doi.org/10.1007/3-540-46017-9_9
  * [40] Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. 19(1) (2017). https://doi.org/10.1007/s10009-015-0378-x
  * [41] van der Meyden, R.: Common knowledge and update in finite environments. Inf. Comput. 140(2) (1998). https://doi.org/10.1006/inco.1997.2679
  * [42] Nguyen, L.V., Kapinski, J., Jin, X., Deshmukh, J.V., Johnson, T.T.: Hyperproperties of real-valued signals. In: ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017. ACM (2017). https://doi.org/10.1145/3127041.3127058
  * [43] Rabe, M.N.: A temporal logic approach to information-flow control. Ph.D. thesis, Saarland University (2016)
  * [44] Sistla, A.P.: Theoretical issues in the design and verification of distributed systems. Ph.D. thesis, Harvard University (1983)
  * [45] Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. (1955)
  * [46] Winskel, G.: The formal semantics of programming languages - an introduction. Foundation of computing series, MIT Press (1993)

##  Appendix 0.A Additional Material for Section 3

###  0.A.1 Additional Material for Section 3.1

See 1

###### Proof

HyperQPTL extends HyperLTL with quantification over atomic propositions.
However, HyperQPTL can also be expressed using quantification over arbitrary
traces, that are not necessarily system traces, capturing exactly the same
semantics. Then, we can translate every HyperLTL trace quantification
$\mathbb{Q}\pi.\varphi$ to $\mathbb{Q}\pi\in\mathfrak{S}.\varphi$, and every
HyperQPTL trace quantification $\mathbb{Q}\tau.\varphi$ to
$\mathbb{Q}\tau\in\mathfrak{A}.\varphi$, to obtain a Hyper2LTL formula. ∎

###  0.A.2 Additional Material for Section 3.2

See 1

###### Proof

We translate the Hyper2LTLfp formula $\varphi$ into a Hyper2LTL formula
$\llbracket\varphi\rrbracket$:

$\displaystyle\llbracket\psi\rrbracket$ $\displaystyle:=\psi$
$\displaystyle\llbracket\mathbb{Q}\pi\in X\mathpunct{.}\varphi\rrbracket$
$\displaystyle:=\mathbb{Q}\pi\in X\mathpunct{.}\llbracket\varphi\rrbracket$
$\displaystyle\llbracket\exists(X,\curlyvee,\varphi_{1})\mathpunct{.}\varphi_{2}\rrbracket$
$\displaystyle:=\exists
X\mathpunct{.}\llbracket\varphi_{1}\rrbracket\land\big{(}\forall
Y\mathpunct{.}Y\subsetneq
X\Rightarrow\neg\llbracket\varphi_{1}[Y/X]\rrbracket\big{)}\land\llbracket\varphi_{2}\rrbracket$
$\displaystyle\llbracket\forall(X,\curlyvee,\varphi_{1})\mathpunct{.}\varphi_{2}\rrbracket$
$\displaystyle:=\forall
X\mathpunct{.}\Big{(}\llbracket\varphi_{1}\rrbracket\land\big{(}\forall
Y\mathpunct{.}Y\subsetneq
X\Rightarrow\neg\llbracket\varphi_{1}[Y/X]\rrbracket\big{)}\Big{)}\Rightarrow\llbracket\varphi_{2}\rrbracket$
$\displaystyle\llbracket\exists(X,\curlywedge,\varphi_{1})\mathpunct{.}\varphi_{2}\rrbracket$
$\displaystyle:=\exists
X\mathpunct{.}\llbracket\varphi_{1}\rrbracket\land\big{(}\forall
Y\mathpunct{.}Y\supsetneq
X\Rightarrow\neg\llbracket\varphi_{1}[Y/X]\rrbracket\big{)}\land\llbracket\varphi_{2}\rrbracket$
$\displaystyle\llbracket\forall(X,\curlywedge,\varphi_{1})\mathpunct{.}\varphi_{2}\rrbracket$
$\displaystyle:=\forall
X\mathpunct{.}\Big{(}\llbracket\varphi_{1}\rrbracket\land\big{(}\forall
Y\mathpunct{.}Y\supsetneq
X\Rightarrow\neg\llbracket\varphi_{1}[Y/X]\rrbracket\big{)}\Big{)}\Rightarrow\llbracket\varphi_{2}\rrbracket$

Path formulas and first-order quantification can be translated verbatim. To
translate (fixpoint-based) second-order quantification we use additional
second order quantification to express the fact that a set should be a least
or greatest. We write $Y\subsetneq X$ as a shorthand for

$\displaystyle\big{(}\forall\pi\in Y.\pi\triangleright
X\big{)}\land\big{(}\exists\pi\in Y.\forall\pi^{\prime}\in
Y\mathpunct{.}\operatorname{\leavevmode\hbox to8.7pt{\vbox
to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neg(\pi=_{\text{AP}}\pi^{\prime})\big{)}$

$\varphi_{1}[Y/X]$ denotes the formula where all free occurrences of $X$ are
replaced by $Y$.

Note that above formula is no Hyper2LTL formula as it is not in prenex normal
form. However, no (first or second-order) quantification occurs under temporal
operators, so we can easiliy bring it into prenex normal form. It is easy to
see that any system satisfies $\varphi$ in the Hyper2LTLfp semantics iff it
satisfies $\llbracket\varphi\rrbracket$ in the Hyper2LTL semantics. ∎

###  0.A.3 Additional Proofs for Section 3.4

See 3

###### Proof

Instead of working with Turing machines, we consider two counter machines as
they are simpler to handle. A two-counter machine (2CM) maintains two counters
$c_{1},c_{2}$ and has a finite set of instructions $l_{1},\ldots,l_{n}$. Each
instruction $l_{i}$ is of one of the following forms, where $x\in\\{1,2\\}$
and $1\leq j,k\leq n$.

  * •

$l_{i}:\big{[}c_{x}\coloneqq c_{x}+1;\texttt{ goto }\\{l_{j},l_{k}\\}\big{]}$

  * •

$l_{i}:\big{[}c_{x}\coloneqq c_{x}-1;\texttt{ goto }\\{l_{j},l_{k}\\}\big{]}$

  * •

$l_{i}:\big{[}\texttt{if }c_{x}=0\texttt{ then goto }l_{j}\texttt{ else goto
}l_{k}\big{]}$

Here, goto $\\{l_{j},l_{k}\\}$ indicates that the machine nondeterministically
chooses between instructions $l_{j}$ and $l_{k}$. A configuration of a 2CM is
a tuple $(l_{i},v_{1},v_{2})$, where $l_{i}$ is the next instruction to be
executed, and $v_{1},v_{2}\in\mathbb{N}$ denote the values of the counters.
The initial configuration of a 2CM is $(l_{1},0,0)$. The transition relation
between configurations is defined as expected. Decrementing a counter that is
already $0$ leaves the counter unchanged. An infinite computation is
_recurring_ if it visits instruction $l_{1}$ infinitely many times. Deciding
if a machine has a recurring computation is $\Sigma_{1}^{1}$-hard [1].

For our proof, we encode each configuration of the 2CM as an infinite trace.
We use to atomic propositions $c_{1},c_{2}$, which we ensure to hold exactly
once and use this unique position to represent the counter value. The current
instruction can be encoded in the first position using APs
$l_{1},\ldots,l_{n}$. We further use a fresh AP $\dagger$ – which also holds
exactly once – to mark the step of this configuration. We are interested in a
set of traces $X$ that satisfies all of the following requirements:

  1. 1.

The set $X$ contains the initial configuration. Note that in this
configuration, $\dagger$ holds in the _first_ step.

  2. 2.

For every configuration, there exists a successor configuration. Note that in
the successor configuration, $\dagger$ is shifted by one position.

  3. 3.

All pairs of traces where $\dagger$ holds at the same position are equal. $X$
thus assigns a unique configuration to each step.

  4. 4.

The computation is recurrent. As already done in [4], we can ensure this by
adding a fresh counter that counts down to the next visit of instruction
$l_{1}$.

It is easy to see that we can encode all the above as a Hyper2LTL (or
Hyper2LTLfp) formula using only first-order quantification over traces in $X$.
Let $\varphi$ be such a formula. It is easy to see that the Hyper2LTL formula
$\exists X.\varphi$ holds on any system, iff there exists a set $X$ with the
above properties iff the 2CM has a recurring computation. The reproves
Proposition 2.

For the present proof, we do, however, want to show $\Sigma^{1}_{1}$-hardness
for the less powerful Hyper2LTLfp. The key point to extend this is to ensure
that iff there exists a set $X$ that satisfies the above requirements, then
there also exists a minimal one. The key observation is that – by the
construction of $X$ – any set $X$ that satisfies the above _is already
minimal_ : The AP $\dagger$ ensures that, for each step, there exists exactly
one configuration (Item 3), and, when removing any number of traces from $X$,
we will inevitably violate Item 4.

We thus get that the 2CM has a recurring computation iff there exists
_mininmal_ $X$ that satisfies $\varphi$ iff the Hyper2LTLfp formula
$\exists(X,\curlyvee,\varphi)\mathpunct{.}\mathit{true}$ holds on an arbitrary
system. ∎

See 4

###### Proof

Assume that we have $m$ second-order quantifiers, and for each $k\in[m]$,
$\pi_{1},\ldots,\pi_{l_{k}}$ are the first-order variables occurring before
$X_{k}$ is quantified:

$\displaystyle\varphi=\mathbb{Q}\pi_{1},\ldots,\mathbb{Q}\pi_{l_{1}}\exists
X_{1}\mathbb{Q}\pi_{l_{1}+1},\ldots,\mathbb{Q}\pi_{l_{2}}\exists
X_{2}\cdots\exists
X_{m}\mathbb{Q}\pi_{l_{m}+1},\ldots,\mathbb{Q}\pi_{l_{m+1}}\psi\ ,$

The second-order variables we use thus are
$\mathfrak{V}=\\{\mathfrak{S},\mathfrak{A},X_{1},\ldots,X_{m}\\}$. Each
$X\in\mathfrak{V}$ can depend on some of the traces quantified before it. In
particular, each $X_{k}$ depends on traces $\pi_{1},\ldots,\pi_{l_{k}}$,
$\mathfrak{S}$ depends on none of the traces (as it is fixed) and neither does
$\mathfrak{A}$. We define a function $c:\mathfrak{V}{}\to\mathbb{N}$ that
denotes on how many traces the set can depend, i.e.,
$c(\mathfrak{S})=c(\mathfrak{A})=0$, and $c(X_{k})=l_{k}$.

We then encode this functional dependence into a model by using traces. For
each $X\in\mathfrak{V}$, we define atomic propositions

$\displaystyle\text{AP}_{X}:=\\{[a,j]_{X}\mid a\in\text{AP}\land
j\in[c(X)]\cup\\{\dagger\\}\\}$

and then define

$\displaystyle\text{AP}^{\prime}:=\text{AP}\uplus\bigcup_{X\in\mathfrak{V}{}}\text{AP}_{X}$

We will use the original APs to describe traces. The additional propositions
are used to encode functions which map the $c(X)$ traces quantified before $X$
to some set of traces. Given traces $\pi_{1},\ldots,\pi_{C(X)}$, we say a
trace $t$ is in the model of $X$ if there exists some trace $\dot{t}$ (in the
model of our final formula) such that

$\displaystyle\begin{split}\forall
z\in\mathbb{N}\mathpunct{.}\Big{(}\bigwedge_{j\in[C(X)]}\bigwedge_{a\in\text{AP}}\big{(}a\in
t_{j}(z)\leftrightarrow[a,j]_{X}\in\dot{t}(z)\big{)}\Big{)}\land\\\ \forall
z\in\mathbb{N}\mathpunct{.}\Big{(}\bigwedge_{a\in\text{AP}}\big{(}a\in
t(z)\leftrightarrow[a,\dagger]_{X}\in\dot{t}(z)\big{)}\Big{)}\end{split}$ (3)

holds. That is, the trace $\dot{t}$ defines the functional mapping from
$t_{1},\ldots,t_{c(X)}$ to $t$.

We use this idea of encoding functions to translate $\varphi$ as follows:

$\displaystyle\llbracket\psi\rrbracket$ $\displaystyle:=\psi$
$\displaystyle\llbracket\mathbb{Q}X.\varphi\rrbracket$
$\displaystyle:=\llbracket\varphi\rrbracket$
$\displaystyle\llbracket\exists\pi_{i}\in X\mathpunct{.}\varphi\rrbracket$
$\displaystyle:=\exists\pi_{i}\mathpunct{.}\langle\pi_{i}\in
X\rangle\land\llbracket\varphi\rrbracket$
$\displaystyle\llbracket\forall\pi_{i}\in X\mathpunct{.}\varphi\rrbracket$
$\displaystyle:=\forall\pi_{i}\mathpunct{.}\langle\pi_{i}\in
X\rangle\rightarrow\llbracket\varphi\rrbracket$

We leave path formulas unchanged and fully ignore second-order quantification
(which is always existential). We define $\langle\pi\in X\rangle$ as an
abbreviation for

$\displaystyle\exists\dot{\pi}\mathpunct{.}\Big{(}\bigwedge_{j\in[c(X)]}\operatorname{\leavevmode\hbox
to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{