}{}\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}}\big{(}a_{\pi_{j}}\leftrightarrow([a,j]_{X})_{\dot{\pi}}\big{)}\Big{)}\land\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}}\big{(}a_{\pi}\leftrightarrow([a,\dagger]_{X})_{\dot{\pi}}\big{)}\Big{)}$

which encodes Equation 3.

The last thing we need to ensure is that $\mathfrak{S}$ and $\mathfrak{A}$ are
encoded correctly. That is for any trace $t$ we have
$t\in\mathit{Traces}(\mathcal{T})$ iff there exists a $\dot{t}$ (in the model)
such that for any $z\in\mathbb{N}$ and $a\in\text{AP}$, we have $a\in t(z)$
iff $[a,\dagger]_{\mathfrak{S}}\in\dot{t}(z)$. Similarly, there should exists
a trace $\dot{t}$ (in the model) such that for any $z\in\mathbb{N}$ and
$a\in\text{AP}$, $[a,\dagger]_{\mathfrak{A}}\in\dot{t}(z)$. Both requirement
can be easily expressed as HyperQPTL formulas $\varphi_{\mathfrak{S}}$ and
$\varphi_{\mathfrak{A}}$ (Note that expressing these requirement in HyperLTL
is not possible as we cannot quantify over traces that are not within the
current model).

It is easy to see that $\mathcal{T}\vDash\varphi$ iff
$\llbracket\varphi\rrbracket\land\varphi_{\mathfrak{S}}\land\varphi_{\mathfrak{A}}$
is satisfiable. ∎

See 5

###### Proof

$\forall^{*}X\forall^{*}\pi.\varphi$, $\exists^{*}X\exists^{*}\pi.\varphi$: As
universal properties are downwards closed and existential properties are
upwards closed, removing second order quantification does not change the
semantics of the formula.

$\exists^{*}X\forall^{*}\pi.\varphi$: for every variable $X$ we introduce a
trace variable $\pi_{x}$ which is existentially bounded, and for every
occurrence of $\pi$ in $\varphi$ such that $\pi\in X$, we replace $\pi$ with
$\pi_{x}$. If $\varphi$ holds for all traces in $X$, it holds also when
replacing $X$ with the singleton $\pi_{x}$. The other direction of implication
is trivial as we found a set $X=\\{\pi_{X}\\}$ for which $\varphi$ holds. For
similar reasons, for $\forall^{*}X\exists^{*}\pi.\varphi$ we can remove the
second order quantification and replace every existentially trace
quantification with a universal trace quantification.

As a conclusion of all of the above, we have that the model-checking of
Hyper2LTLformulas of the following type is decidable:
$\mathbb{Q}_{1}X_{1}\cdots\mathbb{Q}_{k}X_{k}.\mathbb{Q}^{\prime}_{1}\pi_{1}\in
X_{1}\cdots\mathbb{Q}^{\prime}_{k}\pi_{k}\in X_{k}.\varphi$ where we have
$\mathbb{Q}_{i},\mathbb{Q}^{\prime}_{i}\in\\{\exists,\forall\\}$ and in
$\varphi$ only traces from the same set $X_{i}$ are compared to each other
(that is, $\varphi$ does not bind traces from different sets to each other).

Lastly, for $\psi=\exists X.\exists^{*}\pi\in X.\forall^{*}\pi^{\prime}\in
X.\varphi$, we use a reduction to the satisfiability problem of HyperQPTL
[23]. Let $\varphi_{\mathcal{T}}$ a QPTL formula that models the system. Then,
$\mathcal{T}\vDash\psi$ iff the HyperQPTL formula $\hat{\psi}$ is satisfiable,
where
$\hat{\psi}=\exists^{*}\pi.\forall^{*}\pi^{\prime}.\forall\tau.\varphi_{\mathcal{T}}(\tau)\wedge\psi(\pi,\pi^{\prime})$.
Since $\hat{\psi}$ is a $\exists^{*}\forall^{*}$ HyperQPTL formula, its
satisfiability problem is decidable [23]. ∎

##  Appendix 0.B Appendix for Section 4

###  0.B.1 Additional Material for Section 4.1

LTLK,C is defined by the following grammar:

$\displaystyle\psi:=a\mid\neg\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_{1}\operatorname{\mathcal{U}}\psi_{2}\mid\mathsf{K}_{A}\psi\mid\mathsf{E}\psi\mid\mathsf{C}\psi$

where $A$ is a set of agents. Given two traces $t,t^{\prime}$ we write
$t[0,i]=_{A_{i}}t^{\prime}[0,i]$ if $t$ and $t^{\prime}$ appear
indistinguishable for agent $A_{i}$ in the first $i$ steps. Given a set of
traces $T$ and a trace $t$ we define

$\displaystyle t,i$ $\displaystyle\vDash_{T}a$ iff $\displaystyle a\in t(i)$
$\displaystyle t,i$ $\displaystyle\vDash_{T}\neg\psi$ iff $\displaystyle
t,i\not\vDash_{T}\psi$ $\displaystyle t,i$
$\displaystyle\vDash_{T}\psi_{1}\land\psi_{2}$ iff $\displaystyle
t,i\vDash_{T}\psi_{1}\text{ and }t,t\vDash_{T}\psi_{2}$ $\displaystyle t,i$
$\displaystyle\vDash_{T}\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 t,i+1\vDash_{T}\psi$ $\displaystyle t,i$
$\displaystyle\vDash_{T}\psi_{1}\operatorname{\mathcal{U}}\psi_{2}$ iff
$\displaystyle\exists j\geq i\mathpunct{.}t,j\vDash_{T}\psi_{2}\text{ and
}\forall i\leq k<j\mathpunct{.}t,k\vDash_{T}\psi_{1}$ $\displaystyle t,i$
$\displaystyle\vDash_{T}\mathsf{K}_{A_{i}}\psi$ iff $\displaystyle\forall
t^{\prime}\in T\mathpunct{.}t[0,i]=_{A_{i}}t^{\prime}[0,i]\to
t^{\prime},i\vDash\psi$ $\displaystyle t,i$
$\displaystyle\vDash_{T}\mathsf{E}\psi$ iff $\displaystyle
t,i\vDash_{T}\bigwedge_{A_{i}\in A}\mathsf{K}_{A_{i}}\psi$ $\displaystyle t,i$
$\displaystyle\vDash_{T}\mathsf{C}\psi$ iff $\displaystyle
t,i\vDash_{T}\mathsf{E}^{\infty}\psi$

The _everyone knows_ operator $\mathsf{E}$ states that every agents knows that
$\psi$ holds. The semantics of the common knowledge operator $\mathsf{C}$ is
then the infinite chain, or transitive closure, of _everyone knows that
everyone knows that …_ $\psi$.

See 6

###### Proof

Let $\\{A_{1},\ldots,A_{n}\\}$ be the set of agents. For the $j$th occurrence
of a knowledge operator $\mathbb{K}\in\\{\mathsf{K},\mathsf{C}\\}$ we
introduce a new trace variable $\tau_{j}$ and a second order variable $Y_{j}$.
In addition, we introduce a new atomic proposition $k$. We then replace the
$j$th occurrence of $\mathbb{K}$ in $\varphi$ with $k_{\tau_{j}}$, resulting
in the HyperLTL formula $\psi^{\tau}$. Denote by $\psi_{j}$ the subformula of
$\psi^{\tau}$ that directly follows $k_{\tau_{j}}$.

We define by induction on the nested knowledge operators the corresponding
Hyper2LTLfp formula $\varphi_{j}$. For the first (inner-most) operator, we
define $\varphi_{0}$ to be the LTL formula nested under this operator. Now,
assume we have defined $\varphi_{j-1}$, and let
$\mathbb{K}\in\\{\mathsf{K},\mathsf{C}\\}$ be the $j$th inner-most knowledge
operator. Then, $\varphi_{j}$ is defined as follows.

$\displaystyle\forall\tau_{j}\in\mathfrak{A}.\Big{(}Y_{j},\curlyvee,(\pi\in
Y_{j}\wedge\forall\pi_{1}\in Y_{j}.\forall\pi_{2}\in\mathfrak{S}.\left(\neg
k_{\tau_{j}}\operatorname{\mathcal{U}}(k_{\tau_{j}}\wedge\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}}}\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}}}\neg
k_{\tau_{j}})\right)\rightarrow$
$\displaystyle\left(\mathit{equiv}^{j}_{\mathbb{K}}(\pi_{1},\pi_{2})\operatorname{\mathcal{U}}k_{\tau_{j}}\rightarrow\pi_{2}\triangleright
Y_{j}\right)\Big{)}.\forall\pi_{1}\in
Y_{j}.\varphi_{j-1}\wedge\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}}}\left(k_{\tau_{j}}\rightarrow\psi_{j}\right)$

Where

$\displaystyle\mathit{equiv}^{j}_{\mathsf{K}_{A_{i}}}:=\pi_{1}\leftrightarrow_{A_{i}}\pi_{2}\quad\quad\quad\mathit{equiv}^{j}_{\mathsf{C}}:=\bigvee_{i\in[n]}\pi_{1}\leftrightarrow_{A_{i}}\pi_{2}$

Each instantiation of the universally quantified variable $\tau_{j}$
corresponds to one timepoint in which we want to check knowledge on.
Therefore, we verify that $k$ appears exactly once on the trace (first line of
the formula). Then, we add to the knowledge set all traces that are equivalent
(by the knowledge if this agent, or by the common knowledge of all agents)
until this timepoint. The formula outside the minimality condition verifies
that for all traces in the set $Y_{j}$, the subformula $\varphi_{j-1}$ holds
thus enforcing the knowledge requirement on all traces in $Y_{j}$. In
addition, it uses the property $\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}}}\left(k_{\tau_{j}}\rightarrow\psi_{j}\right)$
to make sure that the temporal (non-knowledge) requirements hold at the same
time for all traces in $Y_{j}$. Finally, we define
$\varphi^{\prime}=\forall\pi.\varphi_{n}$ where $n$ is the number of knowledge
operators in $\varphi$. Note that in general, the formula above can yield
infinitely many sets of traces. In practical examples, e.g. the examples
appear in this paper, we can write simplified formulas that reason about the
specific problem at hand and only require a finite (usually $1$) number of
such sets. Also note that as the sets $Y_{j}$ are unique, we do not need the
quantification over least sets. ∎

###  0.B.2 Additional Material To Section 4.2

Consider the system in Figure 2(a) (taken from [3]). The synchronous version
of observational determinism ($\varphi_{\mathit{OD}}$) holds on this system:
While we branch on the secret input $h$, the value of $o$ is the same across
all traces. In contrast, $\varphi_{\mathit{OD}}$ does not hold on the system
in Figure 2(b) as, in the second branch, the update occurs one step later.
This, however, is not an accurate interpretation of $\varphi_{\mathit{OD}}$
(assuming that an attacker only has access to the memory footprint and not the
CPU registers or a timing channel), as any two traces are _stutter_ equivalent
(with respect to $o$). In AHLTL we can express an asynchronous version of OD
as $\forall\pi_{1}.\forall\pi_{2}.\mathbf{E}\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 all two traces can be aligned such they (globally)
agree on $o$. This formula now holds on both Figure 2(a) and Figure 2(b).

⬇

if $h$ then

$o$ <- 1

else

$o$ <- $o$ + 1

(a)

⬇

if $h$ then

$o$ $\leftarrow$ 1

else

$reg$ $\leftarrow$ $o$ + 1

$o$ $\leftarrow$ $reg$

(b)

Figure 2: Example Programs.

##  Appendix 0.C Additional Material for Section 6

###  0.C.1 Muddy Children

We consider the following Hyper2LTLfp formula which captures the common
knowledge set after $m$ steps.

$\displaystyle\forall\pi\in\mathfrak{S}{}.$
$\displaystyle\quad\Big{(}X,\curlyvee,\pi\triangleright
X\land\forall\pi_{1}\in
X.\forall\pi_{2}\in\mathfrak{S}{}.\big{(}\bigvee_{i\in[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}}}^{\leq
m}\pi_{1}=_{\text{AP}_{i}}\pi_{2}\big{)}\Rightarrow\pi_{2}\triangleright
X\Big{)}.$ $\displaystyle\quad\quad\quad\quad\forall\pi_{1}\in
X.\forall\pi_{2}\in
X.\bigwedge_{i\in[n]}{i_{c}}_{\pi_{1}}\leftrightarrow{i_{c}}_{\pi_{2}}$

where we write $\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}}}^{\leq m}\psi$ to
assert that $\psi$ holds in the first $m$ steps. Here, $\text{AP}_{i}$ are all
propositions observable by child $i$, i.e., all variables expect the one that
determines if $i$ is muddy. Note that this formula falls within our fixpoint
fragment of Hyper2LTLfp.

Further note that we express a hyperproperty on the knowledge set, i.e.,
compare pairs of traces in the knowledge set. This is not possible in logic’s
such as LTLK,C in which we can only check if a trace property holds on the
knowledge set.

###  0.C.2 Asynchronous Hyperproperties

We verify

$\displaystyle\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}})$ (4)

and the asynchronous version of it. In AHLTL [3] we can define this as
follows:

$\displaystyle\varphi_{\mathit{OD}}:=\forall\pi_{1}.\forall\pi_{2}.\mathbf{E}\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}})$

In Hyper2LTLfp we can express the above AHLTL formula as the following
formula:

$\displaystyle\begin{split}&\forall\pi_{1}\in\mathfrak{S}.\forall\pi_{2}\in\mathfrak{S}.\\\
&\quad\big{(}X_{1},\curlyvee,\pi_{1}\triangleright X_{1}\land\forall\pi\in
X.\forall\pi\in\mathfrak{A}.((o_{\pi}\leftrightarrow
o_{\pi^{\prime}})\operatorname{\mathcal{U}}\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}\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}}}o_{\pi^{\prime}})\rightarrow\pi^{\prime}\triangleright
X_{1}\big{)}\\\ &\quad\big{(}X_{2},\curlyvee,\pi_{2}\triangleright
X_{2}\land\forall\pi\in
X.\forall\pi^{\prime}\in\mathfrak{A}.((o_{\pi}\leftrightarrow
o_{\pi^{\prime}})\operatorname{\mathcal{U}}\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}\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}}}o_{\pi^{\prime}})\rightarrow\pi^{\prime}\triangleright
X_{2}\big{)}\\\ &\quad\quad\exists\pi_{1}\in X_{1},\exists\pi_{2}\in
X_{2}\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}})\end{split}$ (5)

Note that this formula falls within our fixpoint fragment of Hyper2LTLfp.

In Table 1(b), we check Equation 4 and Equation 5 on the two example programs
from the introduction in [3] and the asynchronous program Q1 from [5, 9].

###  0.C.3 Mazurkiewicz Trace

Using our logic, we can also express many properties that reason about the
class of (Mazurkiewicz) traces. The idea of trace is to abstract away from the
concrete order of independent actions (letters). Let
$I\subseteq\Sigma\times\Sigma$ be an independence relation on letters. That
is, $(a,b)\in I$ iff interchanging the order of $a$ and $b$ has no effect
(e.g., local actions for two concurrent processes). We say two traces
$t_{1},t_{2}$ are equivalent (written $t_{1}\equiv_{I}t_{2})$ if we can
rewrite $t_{1}$ into $t_{2}$ by flipping consecutive letters that are in $I$.
For example if $(a,b)\in I$ then $xaby\equiv_{I}xbay$ for all
$x\in\Sigma^{*},y\in\Sigma^{\omega}$. The Mazurkiewicz trace of a concrete
trace $t$ is then defined as $[t]_{I}:=\\{t^{\prime}\mid t\equiv_{i}t\\}$.

Using Hyper2LTLfp we can directly reason about the equivalence classes of
$\equiv_{I}$. Consider the following (quantifier-free) formula
$\varphi_{I}(\pi,\pi^{\prime})$, stating that $\pi$ and $\pi^{\prime}$ are
identical up to one flip of consecutive independent actions.

$\displaystyle(\pi=_{\text{AP}}\pi^{\prime})\operatorname{\mathcal{W}}\Big{(}\bigvee_{(x,y)\in
I}x_{\pi}\land y_{\pi^{\prime}}\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}}}(y_{\pi}\land
x_{\pi^{\prime}})\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}}}\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}}}\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=_{\text{AP}}\pi^{\prime})\Big{)}$

Here we write $x_{\pi}$ for $x\in\Sigma=2^{\text{AP}}$ for the formula
$\bigwedge_{a\in X}a_{\pi}\land\bigwedge_{a\not\in X}\neg a_{\pi}$. The
formula asserts that both traces are equal, until one pair of independent
actions is flipped, followed by, again, identical suffixes.

Using $\varphi_{I}$ we can directly reason about Mazurkiewicz traces. Assume
we are interested if for every (concrete) trace $t$ that satisfies LTL
property $\phi$, all its equivalent traces satisfy $\psi$. We can express this
in Hyper2LTLfp as follows:

$\displaystyle\begin{split}&\forall\pi\in\mathfrak{S}{}.(X,\curlyvee,\pi\triangleright
X\land\forall{\pi_{1}}\in
X\mathpunct{.}\forall{\pi_{2}}\in\mathfrak{A}\mathpunct{.}\varphi_{I}(\pi_{1},\pi_{2})\rightarrow\pi_{2}\triangleright
X)\mathpunct{.}\\\ &\quad\quad\forall\pi^{\prime}\in
X\mathpunct{.}\phi(\pi)\rightarrow\psi(\pi^{\prime})\end{split}$ (6)

That is, for all traces $\pi$, we compute the set $X$ which contains all
equivalent traces. This set should contain $\pi$, must be closed under
$\varphi_{I}$, and is minimal w.r.t. those two properties. Note that this
formula falls within our fixpoint fragment of Hyper2LTLfp.

#### Preliminary Experiments.

The above formula is applicable to arbitrary independec relation, so our tool
can be used to automatically check arbitrary properties on Mazurkiewicz
traces. In our preliminary experiments, we focus on very simple Mazurkiewicz
trace. We model a situation where we start with $\\{a\\}^{1}\\{\\}^{\omega}$
and can swap letters $\\{a\\}$ and $\\{\\}$. We acknowledge that the example
is very simple, but nevertheless emphasize the complex trace-based reasoning
possible with HySO. We then ask the following problems: We ask if, from every
trace, $a$ holds at most once on all traces in $X$. If we apply only
iteration, HySO will move the unique $a$ one step to the right in each
iteration, i.e., after $n$ steps the current under-approximation contains
traces $\\{a\\}\\{\\}^{\omega}$, $\\{\\}^{1}\\{a\\}\\{\\}^{\omega}$,
$\\{\\}^{2}\\{a\\}\\{\\}^{\omega}$, $\ldots$,
$\\{\\}^{n}\\{a\\}\\{\\}^{\omega}$. This fixpoint will never converge, so HySO
would iterate forever. Instead, if we also enable learning of
overapproximations, HySO automatically learns an invariant that proves the
above property (which is instance SwapA in Table 2(b)). We can relax this
requirement to only consider a fixed, finite prefix. SwapAn states that $a$
_can_ hold in any position in the first $n$ steps (by using existential
quantification over $X$). As expected, HySO can prove this property by
iteration $n$ times. Lastly, the violation SwapAViolationn states that any
trace satisfies $a$ within the first $n$ steps. This obviously does not hold,
but HySO requires $n$ iterations to find a counterexample, i.e., a trace where
$a$ does not hold within the first $n$ steps.