# A Logic for Hyperproperties in Multi-Agent Systems

Raven Beutner  CISPA Helmholtz Center for Information Security, Germany  and
Bernd Finkbeiner  CISPA Helmholtz Center for Information Security, Germany

###### Abstract.

Hyperproperties are commonly used in computer security to define information-
flow policies and other requirements that reason about the relationship
between multiple computations. In this paper, we study a novel class of
hyperproperties where the individual computation paths are chosen by the
strategic choices of a coalition of agents in a multi-agent system. We
introduce HyperATL∗, an extension of computation tree logic with path
variables and strategy quantifiers. Our logic can express strategic
hyperproperties, such as that the scheduler in a concurrent system has a
_strategy_ to avoid information leakage. HyperATL∗ is particularly useful to
specify _asynchronous_ hyperproperties, i.e., hyperproperties where the speed
of the execution on the different computation paths depends on the choices of
the scheduler. Unlike other recent logics for the specification of
asynchronous hyperproperties, our logic is the first to admit decidable model
checking for the full logic. We present a model checking algorithm for
HyperATL∗ based on alternating automata, and show that our algorithm is
asymptotically optimal by providing a matching lower bound. We have
implemented a prototype model checker for a fragment of HyperATL∗, able to
check various security properties on small programs.

###### Key words and phrases:

hyperproperties, multi-agent systems, alternating-time temporal logic,
HyperATL∗, information-flow control, asynchronous hyperproperties, model
checking

This work was partially supported by the German Research Foundation (DFG) as
part of the Collaborative Research Center “Foundations of Perspicuous Software
Systems” (TRR 248, 389792660), by the ERC Grant OSARES (No. 683300) and by the
Saarbrücken Graduate School of Computer Science.

##  1\. Introduction

Hyperproperties [CS10] are system properties that relate multiple paths of a
system. Such properties are of increasing importance as they can, for example,
characterize the information-flow in a system. A prominent logic to express
hyperproperties is HyperLTL, which extends linear-time temporal logic (LTL)
with explicit path quantification [CFK+14]. HyperLTL can, for instance,
express generalized non-interference (GNI) [McC88] stating that the high-
security input of a system does not influence the observable output.

$\displaystyle\forall\pi\mathpunct{.}\forall\pi^{\prime}\mathpunct{.}\exists\pi^{\prime\prime}\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}}}\big{(}\bigwedge_{a\in
H}a_{\pi}\leftrightarrow
a_{\pi^{\prime\prime}}\big{)}\land\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}}}\big{(}\bigwedge_{a\in
O}a_{\pi^{\prime}}\leftrightarrow a_{\pi^{\prime\prime}}\big{)}$ (GNI)

Here $H$ is a set of high-security input propositions and $O$ a set of outputs
(for simplicity we assume that there are no low-security inputs). The formula
states that for any paths $\pi,\pi^{\prime}$ there exists a third path
$\pi^{\prime\prime}$ that agrees with the high-security inputs of $\pi$ and
with the outputs of $\pi^{\prime}$. The existence of $\pi^{\prime\prime}$
guarantees that any observation on the outputs is compatible with every
possible sequence of high-security inputs; non-determinism is the sole
explanation for the output.

Existing hyperlogics (including HyperLTL) consider a system as a set of paths
and quantify (universally or existentially) over those paths. In this paper,
we introduce a novel class of hyperproperties that reason about _strategic
behavior_ in a multi-agent system where the paths of the system are outcomes
of games played on a game structure. We introduce HyperATL∗, a temporal logic
to express hyperproperties in multi-agent systems. Our logic builds on the
foundation laid by alternating-time temporal logic (ATL∗) [AHK02]111ATL∗ is
branching-time logic that extends CTL∗ by offering selective quantification
over paths that are possible outcomes of games [AHK02]. The ATL∗ quantifier
$\llangle A\rrangle\varphi$ states that the players in $A$ have a joint
strategy such that every outcome under that strategy satisfies $\varphi$..
While strategy quantifiers in ATL∗ can be nested (similar to CTL∗), the logic
is unable to express hyperproperties, as the scope of each quantifier is
limited to the current path (see [Fin17]).

HyperATL∗ HyperCTL∗ATL∗HyperLTLCTL∗ATLHyperpropertiesStrategic
PropertiesLTLCTL Figure 1. Hierarchy of expressiveness of temporal logics. An
arrow $A\to B$ indicates that $A$ is a (syntactic) fragment of $B$. Logics
surrounded in the blue, dashed area can express hyperproperties. Logics in the
red, dotted area can express strategic properties on multi-agent systems.

HyperATL∗ combines quantification over strategic behavior with the ability to
express hyperproperties. Syntactically, our logic combines the strategic
quantifier of ATL∗ but binds the outcome to a path variable (similar to
HyperLTL). For example, the HyperATL∗ formula $\llangle A\rrangle\pi.\varphi$
to specifies that the agents in $A$ have a strategy such that all outcomes
under that strategy, when bound to the path variable $\pi$, satisfy $\varphi$.
Similar to HyperLTL, quantification is resolved incrementally. For example,
$\llangle A\rrangle\pi.\llangle A^{\prime}\rrangle\pi^{\prime}.\varphi$
requires the existence of strategy for the agents in $A$ such that for all
possible outcomes under that strategy, when bound to $\pi$, the agents in
$A^{\prime}$ have a strategy such that all possible outcomes, when bounds to
$\pi^{\prime}$, satisfy $\varphi$. In particular, the quantification over
strategies for $A^{\prime}$ takes place after $\pi$ is fixed222This
incremental elimination of quantification ensures that HyperATL∗ is a proper
extension of HyperCTL∗ but is also crucial for decidable model checking. In
fact, model checking for any logic that could express the existence of a
strategy such that the set of plays of that strategy satisfies a
hyperproperty, would already subsume the realizability of hyperproperties
which is known to be undecidable already for very simple fragments [FHL+18]..
We endow our logic with an explicit construct to resolve multiple games
simultaneously (syntactically, we surround quantifiers by $[\cdot]$ brackets).
The formula $[\llangle A\rrangle\pi\mathpunct{.}\llangle
A^{\prime}\rrangle\pi^{\prime}.]~{}\varphi$ requires winning strategies for
the agents in $A$ (for the first copy) and for $A^{\prime}$ (for the second
copy) in a game that progresses simultaneously; the players can observe the
current state of both copies.

The resulting logic is very expressive and subsumes both the existing
hyperlogic HyperCTL∗ [CFK+14] (the branching-time extension of HyperLTL) and
ATL∗ [AHK02]. The situation is depicted in Figure 1. Reasoning about strategic
hyperproperties in multi-agent systems (expressed in HyperATL∗) is useful in
various settings, including information-flow control and asynchronous
hyperproperties. Consider the following two examples.

#### Application 1: Information-flow Control

We consider a strategic information-flow control property in the context of
GNI. Imagine a system where the non-determinism arises from a scheduling
decision between two subprograms $P_{1},P_{2}$. Each subprogram reads the next
high-security input $h$ of the system. Suppose that $P_{1}$ assumes that $h$
is even and otherwise leaks information, while $P_{2}$ assumes that $h$ is odd
and otherwise leaks information. In HyperLTL, quantification is resolved
incrementally so the witness path $\pi^{\prime\prime}$ in GNI is chosen after
$\pi$ and $\pi^{\prime}$ are already fixed. In particular, all future high-
security input $h$ are already determined, so a leakage disproving path
$\pi^{\prime\prime}$ can be constructed (by always scheduling the copy that
does not leak information on the _next_ input); the system satisfies GNI. By
contrast, an _actual_ scheduler, who determines which subprogram handles the
next input cannot avoid information leakage. HyperATL∗ can express a more
strict information-flow policy. As a first step, we consider a system as a
game structure with two players. Player $\xi_{H}$ chooses the high-security
inputs (in each step) and player $\xi_{N}$ resolves the non-determinism of the
system (we give a concrete semantics into such a game structure in Section
8.1). Consider the following HyperATL∗ specification.

$\displaystyle\forall\pi\mathpunct{.}\llangle\xi_{N}\rrangle\pi^{\prime}\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}}}\big{(}\bigwedge_{a\in
O}a_{\pi}\leftrightarrow a_{\pi^{\prime}}\big{)}$

This formula requires that for every possible path $\pi$, the non-determinism
player $\xi_{N}$ has a _strategy_ to produce identical outputs on
$\pi^{\prime}$ against all possible moves by $\xi_{H}$. Any possible output of
the system is thus achievable by a strategy only knowing the finite input-
history, but oblivious to the future high-security inputs. The system sketched
above does not satisfy this property.

A particular strength of this formulation is that we can encode additional
requirements on the strategy for the scheduler. For example, if the internal
non-determinism arises from the scheduling decisions between multiple
components, we can require fairness of the scheduling strategy.
$\vartriangleleft$

$o$ $\leftarrow$ truewhile( true) $h$$\leftarrow$ReadHif $h$then
$o$$\leftarrow$$\neg$ $o$else $temp$$\leftarrow$$\neg$ $o$ $o$$\leftarrow$
$temp$ Figure 2. Example program that violates (synchronous) observational
determinism.

#### Application 2: Asynchronous Hyperproperties

Most existing hyperlogics traverse the paths of a system synchronously.
However, in many applications (for example, when reasoning about software) we
require an asynchronous traversal to, e.g., account for the unknown speed of
execution of software that runs on some unknown platform or to abstract away
from intermediate (non-observable) program steps. Strategic hyperproperties
enable reasoning over asynchronous hyperproperties by considering the
execution speed of a system as being controlled by a dedicated scheduling
player, which we add via a system transformation. Instead of reasoning about
asynchronicity directly, we then reason about strategies for the scheduling
player.

As an example, consider the program in Figure 2. It continuously reads a high-
security input $h$ and, depending on $h$, flips the output $o$ either
directly, or via a temporary variable. Consider the HyperLTL specification
$\forall\pi.\forall\pi^{\prime}\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}}}\big{(}o_{\pi}\leftrightarrow
o_{\pi^{\prime}}\big{)}$. It expresses _observational-determinism_ (OD), i.e.,
the output should be identical across all paths [HWS06]. In Figure 2, the
exact timepoint of the change in $o$ differs and so the program does not
satisfy OD. However, on a fast enough hardware, an observer might be unable to
detect the timing offset and only observe the value of $o$ whenever a change
occurs. To express this, we require a property that allows the paths of the
program to be executed at different speeds to realign the output. We extend
the system with a scheduling agent $\mathit{sched}$ that can stutter the
system (we give a concrete construction in Section 5) and express the
following HyperATL∗ property.

$\displaystyle[\llangle\mathit{sched}\rrangle\pi\mathpunct{.}\llangle\mathit{sched}\rrangle\pi^{\prime}.]~{}\mathit{fair}_{\pi}\land\mathit{fair}_{\pi^{\prime}}\land\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}}}\big{(}o_{\pi}\leftrightarrow
o_{\pi^{\prime}}\big{)}$

This formula requires that the scheduler has a strategy to align any two
program paths such that the output agrees.
$\mathit{fair}_{\pi}\land\mathit{fair}_{\pi^{\prime}}$ ensures that both
copies are scheduled infinitely many times (see Section 5 for details). By
surrounding the quantifier with $[\cdot]$, both games are resolved
simultaneously (opposed to incrementally), so the strategies in both copies
can collaborate. The program in Figure 2 (with an added asynchronous
scheduler) satisfies this HyperATL∗ property.

This general style of asynchronous reasoning turns out to be remarkably
effective: Verification is possible (decidable) for the full logic and the
approach subsumes the largest known decidable fragment of a recent
asynchronous extension of HyperLTL [BCB+21].  $\vartriangleleft$

#### Model Checking

We show that model checking of HyperATL∗ on concurrent game structures is
decidable and present an automata-based algorithm. Our algorithm incrementally
reduces model checking to the emptiness of an automaton. By using alternating
automata we encode the strategic behavior of a game structure within the
transition function of the automaton. To characterize its complexity, we
partition HyperATL∗ formulas based on the number of complex quantifiers
(quantifiers where the set of agents is non-trivial) and simple quantifiers
(quantifiers that are $\exists$ or $\forall$). For each fragment, we derive
upper bounds on the model checking complexity, both in the size of the system
and specification. Different from HyperLTL – where each alternation results in
an exponential blowup [FRS15, Rab16] – the strategic quantification in
HyperATL∗ results in a _double_ exponential blowup with each complex
quantifier. Using a novel counter construction we prove matching lower bounds
on the HyperATL∗ model checking problem (in the size of both specification and
system).

#### Prototype Model Checker

On the practical side, we present hyperatlmc, a prototype model checker for an
efficient fragment of HyperATL∗. The fragment supported by our tool does, in
particular, include all alternation free HyperLTL formulas [FRS15], the model
checking approach from [CFST19], and the formulas arising when expressing
asynchronous hyperproperties in HyperATL∗.

#### Contributions

In summary, our contributions include the following:

  * •

We introduce HyperATL∗, a novel logic to express strategic hyperproperties in
multi-agent systems. We demonstrate that HyperATL∗ can express many existing
information-flow policies and offers a natural formalism to express
asynchronous hyperproperties (subsuming the largest known decidable fragment
of the logic presented in [BCB+21]).

  * •

We give an automata-based model checking algorithm for HyperATL∗ and analyze
its complexity (both in system and specification size) based on the number and
type of quantifiers.

  * •

We prove matching lower bounds on the HyperATL∗ model checking problem via a
novel counter construction.

  * •

We present hyperatlmc, a prototype-model checker for an efficient fragment of
HyperATL∗, and apply it to verify information-flow policies and asynchronous
hyperproperties on small finite-state programs.

This paper is an extended version of a preliminary conference version [BF21].
Compared to the conference paper, this version contains detailed and
streamlined proofs of the theoretical results. Moreover, we extend our earlier
complexity bounds by also analyzing HyperATL∗ model-checking in the size of
the system (in [BF21] we only consider the complexity in the size of the
specification) and derive uniform lower and upper bounds that are stated
purely in the number and type of the quantifiers (without side conditions
needed in [BF21]).

#### Structure

The remainder of this paper is structured as follows. In Section 2 we
introduce basic preliminaries and in Section 3 we develop HyperATL∗.
Afterward, in Section 4 and Section 5, we present examples (ranging from
information-flow control to asynchronous hyperproperties) expressible in
HyperATL∗ and connect to existing asynchronous logics. We discuss model
checking on finite-state game structures in Section 6. In Section 7 we show
matching lower bounds on the model checking problem. Finally, in Section 8 we
report on our prototype model checker and discuss related work in Section 9.

##  2\. Preliminaries

In this section, we introduce basic preliminaries on transition systems, game
structures and alternating automata. We fix a finite set of atomic
propositions $\mathit{AP}$ and define $\Sigma:=2^{\mathit{AP}}$. For an
infinite sequence $u\in X^{\omega}$ for some set $X$ and $i\in{\rm Nature}$,
we write $u(i)\in X$ for the $i$th element (starting at the $0$th) and
$u[i,\infty]\in X^{\omega}$ for the infinite-suffix starting at position $i$.
For $u_{1},\cdots,u_{n}\in X^{\omega}$, we define
$\otimes(u_{1},\cdots,u_{n})\in(X^{n})^{\omega}$ as the pointwise product,
i.e., $\otimes(u_{1},\cdots,u_{n})(i):=(u_{1}(i),\cdots,u_{n}(i))$. For two
sequences we write $u_{1}\otimes u_{2}$ instead of $\otimes(u_{1},u_{2})$. The
pointwise product extends to finite sequences of the same length.

#### Transition Systems

A _transition system_ is a tuple $\mathcal{T}=(S,s_{0},\delta,L)$ where $S$ is
a finite set of states, $s_{0}\in S$ an initial state, $\delta\subseteq
S\times S$ a transition relation and $L:S\to\Sigma$ a labeling function. We
assume that for every $s\in S$ there is at least one $s^{\prime}$ such that
$(s,s^{\prime})\in\delta$. A path in $\mathcal{T}$ is an infinite sequence
$p\in S^{\omega}$ such that for every $i\in{\rm Nature}$,
$(p(i),p(i+1))\in\delta$.

#### Concurrent Game Structures

As the basic model of multi-agent systems we use game structures. A
_concurrent game structure_ (CGS) [AHK02] is an extension of a transition
system in which the transition relation is composed of the moves of individual
agents (also called players). Formally, a CGS is a tuple
$\mathcal{G}=(S,s_{0},\Xi,\mathcal{M},\delta,L)$. The finite set of states
$S$, the initial state $s_{0}\in S$ and the labeling $L:S\to\Sigma$ are as in
a transition system. Additionally, $\Xi$ is a finite and non-empty set of
agents (or players), $\mathcal{M}$ a finite and non-empty set of moves and
$\delta:S\times(\Xi\to\mathcal{M})\to S$ a transition function. We call a
mapping $\sigma:\Xi\to\mathcal{M}$ a global move vector. Given a state and
global move vector, the transition function $\delta$ determines a successor
state. For a set of agent $A\subseteq\Xi$ a function $\sigma:A\to\mathcal{M}$
a partial move vector. For disjoint sets of agents $A_{1},A_{2}\subseteq\Xi$
and partial move vectors $\sigma_{i}:A_{i}\to\mathcal{M}$ for $i\in\\{1,2\\}$
we define $\sigma_{1}+\sigma_{2}:A_{1}\cupdot A_{2}\to\mathcal{M}$ as the move
vector obtained as the combination of the individual choices. For
$\sigma:A\to\mathcal{M}$ and $A^{\prime}\subseteq A$, we define $\sigma_{\mid
A^{\prime}}:A^{\prime}\to\mathcal{M}$ by restricting the domain of $\sigma$ to
$A^{\prime}$. Note that every transition system $\mathcal{T}$ can be seen as a
$1$-player CGS in which the move of the unique player determines the successor
state.

#### Multi Stage Concurrent Game Structures

In a concurrent game structure (as the name suggests) all agents choose their
next move concurrently, i.e., without knowing what moves the other players
have chosen. We introduce the concept of _multi-stage game structure_ (MSCGS),
in which the move selection proceeds in stages and agents can base their
decision on the already fixed moves of (some of the) other agents. This is
particularly useful when we, e.g., want to base a scheduling decision on the
moves selected by the other agents. Formally, a MSCGS is a CGS equipped with a
function $d:\Xi\to\mathbb{N}$, that orders the agents according to
informedness. Whenever $d(\xi_{1})<d(\xi_{2})$, $\xi_{2}$ can base its next
move on the move selected by $\xi_{1}$. A CGS thus naturally corresponds to a
MSCGS with $d=\mathbf{0}$, where $\mathbf{0}$ is the constant $0$ function.

#### Strategies in Game Structures

A strategy in a game structure is a function that maps finite histories of
plays in the game to a move in $\mathcal{M}$. As the plays in an MSCGS
progress in stages, each decision is based on the past sequence of states
_and_ the fixed moves of all agents in previous stages. Formally, a strategy
for an agent $\xi\in\Xi$ is a function

$\displaystyle f_{\xi}:S^{+}\times(\\{\xi^{\prime}\mid
d(\xi^{\prime})<d(\xi)\\}\to\mathcal{M})\to\mathcal{M}$

Note that in case where $d=\mathbf{0}$, a strategy is just a function
$S^{+}\to\mathcal{M}$.

Given a set of agents $A$, a set of strategies $F_{A}=\\{f_{\xi}\mid\xi\in
A\\}$ and a state $s\in S$, we define
$\mathit{out}(\mathcal{G},s,F_{A})\subseteq S^{\omega}$ as the set of all runs
$u\in S^{\omega}$ such that 1) $u(0)=s$ and 2) for every $i\in\mathbb{N}$
there exists a global move vector $\sigma:\Xi\to\mathcal{M}$ with
$\delta(u(i),\sigma)=u(i+1)$ and for all $\xi\in A$ we have
$\sigma(\xi)=f_{\xi}(u[0,i],\sigma_{\mid\\{\xi^{\prime}\mid
d(\xi^{\prime})<d(\xi)\\}})$.  $\vartriangleleft$

#### Alternating Automata

For a set $X$, we write $\mathbb{B}^{+}(X)$ for the set of positive boolean
formulas over $X$ with the standard propositional semantics. Given
$\Psi\in\mathbb{B}^{+}(X)$ and $B\subseteq X$ we write $B\models\Psi$ if the
assignment obtained from $B$ by mapping all $x\in B$ to true and all $x\not\in
B$ to false satisfies $\Psi$. An _alternating parity automaton_ (APA) is a
tuple $\mathcal{A}=(Q,q_{0},\Sigma,\rho,c)$ where $Q$ is a finite set of
states, $q_{0}\in Q$ an initial state, $\Sigma$ a finite alphabet,
$\rho:Q\times\Sigma\to\mathbb{B}^{+}(Q)$ a transition function and
$c:Q\to\mathbb{N}$ a coloring. A tree is a set $T\subseteq\mathbb{N}^{*}$ that
is prefixed closed, i.e., $\tau\cdot n\in T$ implies $\tau\in T$. We refer to
elements in $\tau\in T$ as nodes and denote with $|\tau|$ the length of $\tau$
(or equivalently the depth of the node). For a node $\tau\in T$, we define
$\mathit{children}(\tau)$ as the set of immediate children of $\tau$, i.e.,
$\mathit{children}(\tau):=\\{\tau\cdot n\in T\mid n\in\mathbb{N}\\}$. A
$X$-labeled tree is a pair $(T,r)$ where $T$ is a tree and $r:T\to X$ a
labeling with $X$. A run of an APA $\mathcal{A}=(Q,q_{0},\Sigma,\rho,c)$ on a
word $u\in\Sigma^{\omega}$ is a $Q$-labeled tree $(T,r)$ such that 1)
$r(\epsilon)=q_{0}$, and 2) for all $\tau\in T$,
$\\{r(\tau^{\prime})\mid\tau^{\prime}\in\mathit{children}(\tau)\\}\models\rho(r(\tau),u(|\tau|))$.
A run $(T,r)$ is accepting if for every infinite path in $T$ the minimal color
(as given by $c$) that occurs infinitely many times is even. We denote with
$\mathcal{L}(\mathcal{A})$ the set of words for which $\mathcal{A}$ has an
accepting run. We call an alternating automaton $\mathcal{A}$ non-
deterministic (resp. universal) if the codomain of the transition function
$\rho$ consists of disjunctions (resp. conjunction) of states. If the codomain
of $\rho$ consists of atomic formulas (i.e., formulas without boolean
connectives), we call $\mathcal{A}$ deterministic333In a non-deterministic or
universal automaton we consider $\rho$ as a function $Q\times\Sigma\to 2^{Q}$.
For a deterministic automaton we consider $\rho$ as a function
$Q\times\Sigma\to Q$. . Alternating, non-deterministic, universal and
deterministic parity automata all recognize the same class of languages
(namely $\omega$-regular ones) although they can be (double) exponentially
more succinct.

######  Theorem 1 ([MH84, DH94]).

For every alternating parity automaton $\mathcal{A}$ with $n$ states, there
exists a non-deterministic parity automaton $\mathcal{A}^{\prime}$ with
$2^{\mathcal{O}(n\log n)}$ states that accepts the same language. For every
non-deterministic or universal parity automaton $\mathcal{A}$ with $n$ states,
there exists a deterministic parity automaton $\mathcal{A}^{\prime}$ with
$2^{\mathcal{O}(n\log n)}$ states that accepts the same language.

######  Theorem 2 ([KV01]).

For every alternating parity automaton $\mathcal{A}$ with $n$ states, there
exists an alternating parity automaton $\overline{\mathcal{A}}$ with
$\mathcal{O}(n^{2})$ states that accepts the complemented language. If
$\mathcal{A}$ is non-deterministic (resp. universal), $\overline{\mathcal{A}}$
is universal (resp. non-deterministic).

##  3\. HyperATL*

In this section, we introduce HyperATL∗. Our logic extends CTL∗ [EH86] by
introducing path variables (similar to HyperCTL∗ [CFK+14]) and strategic
quantification (similar to ATL∗ [AHK02]). Assume a fixed set of agents $\Xi$
and let $\mathcal{V}$ be a finite set of path variables. HyperATL∗ formulas
are generated by the following grammar

$\displaystyle\varphi,\psi:=\llangle A\rrangle\pi.\varphi\mid
a_{\pi}\mid\varphi\land\psi\mid\neg\varphi\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}}}\varphi\mid\varphi\operatorname{\mathcal{U}}\psi$

where $\pi\in\mathcal{V}$ is a path variable, $a\in\mathit{AP}$ an atomic
proposition, and $A\subseteq\Xi$ a set of agents. Quantification of the form
$\llangle A\rrangle\pi.\varphi$ binds a path to path variable $\pi$ and
$a_{\pi}$ refers to the truth value of $a$ on the path bound to variable
$\pi$. A formula is closed if all sub-formulas $a_{\pi}$ occur in the scope of
a quantifier that binds $\pi$; throughout the paper we assume all formulas to
be closed. We use the usual derived boolean connectives
$\lor,\to,\leftrightarrow$, the boolean constants true ($\top$) and false
($\bot$) and 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}}}\varphi:=\top\operatorname{\mathcal{U}}\varphi$),
_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}}}\varphi:=\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\varphi$),
_release_
($\varphi\operatorname{\mathcal{R}}\psi:=\neg(\neg\psi\operatorname{\mathcal{U}}\neg\varphi)$)
and _weak until_
($\varphi\operatorname{\mathcal{W}}\psi:=(\varphi\operatorname{\mathcal{U}}\psi)\lor\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}}}\varphi$)

The strategic quantifier $\llangle A\rrangle\pi.\varphi$ states that the
agents in $A$ have a joint strategy such that every outcome under that
strategy, when bound to path variable $\pi$, satisfies $\varphi$. Trivial
agent sets, i.e., $A=\emptyset$ or $A=\Xi$, correspond to classical
existential or universal quantification. We therefore write
$\forall\pi.\varphi$ instead of $\llangle\emptyset\rrangle\pi.\varphi$ and
$\exists\pi.\varphi$ instead of $\llangle\Xi\rrangle\pi.\varphi$. For a single
agent $\xi$, we write $\llangle\xi\rrangle\pi.\varphi$ instead of
$\llangle\\{\xi\\}\rrangle\pi.\varphi$. We define $\llbracket
A\rrbracket\pi.\varphi:=\neg\llangle A\rrangle\pi.\neg\varphi$ which states
that the agents in $A$ have _no_ strategy such that every outcome, when bound
to $\pi$, avoids $\varphi$ (see [AHK02]). We call a quantifier $\llangle
A\rrangle\pi$ _simple_ if the agent-set $A$ is trivial ($\emptyset$ or $\Xi$)
and otherwise _complex_.

A HyperATL∗ formula is _linear_ if it consists of an initial quantifier prefix
followed by a quantifier-free formula, i.e., has the form
$\mathbb{Q}_{1}\pi_{1}.\cdots\mathbb{Q}_{n}\pi_{n}.\psi$ where $\psi$ is
quantifier-free and each $\mathbb{Q}_{i}$ is either $\llangle A\rrangle$ or
$\llbracket A\rrbracket$ for some $A$. Linear-HyperATL∗ is thus the syntactic
subfragment of HyperATL∗ that is analogous to the definition of HyperLTL as a
syntactic fragment of HyperCTL∗.

#### Semantics

The semantics of HyperATL∗ is defined with respect to a game structure
$\mathcal{G}=(S,s_{0},\Xi,\mathcal{M},\delta,d,L)$ and a path assignment
$\Pi$, which is a partial mapping $\Pi:\mathcal{V}\rightharpoonup S^{\omega}$.
For $\pi\in\mathcal{V}$ and path $p\in S^{\omega}$ we write $\Pi[\pi\mapsto
p]$ for the assignment obtained by updating the value of $\pi$ to $p$. We
write $\Pi[i,\infty]$ to denote the path assignment defined by
$\Pi[i,\infty](\pi):=\Pi(\pi)[i,\infty]$.

$\displaystyle\Pi$ $\displaystyle\models_{\mathcal{G}}a_{\pi}$ iff
$\displaystyle a\in L(\Pi(\pi)(0))$ $\displaystyle\Pi$
$\displaystyle\models_{\mathcal{G}}\neg\varphi$ iff
$\displaystyle\Pi\not\models_{\mathcal{G}}\varphi$ $\displaystyle\Pi$
$\displaystyle\models_{\mathcal{G}}\varphi\land\psi$ iff
$\displaystyle\Pi\models_{\mathcal{G}}\varphi\text{ and
}\Pi\models_{\mathcal{G}}\psi$ $\displaystyle\Pi$
$\displaystyle\models_{\mathcal{G}}\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}}}\varphi$ iff
$\displaystyle\Pi[1,\infty]\models_{\mathcal{G}}\varphi$ $\displaystyle\Pi$
$\displaystyle\models_{\mathcal{G}}\varphi\operatorname{\mathcal{U}}\psi$ iff
$\displaystyle\exists i\geq
0\mathpunct{.}\Pi[i,\infty]\models_{\mathcal{G}}\psi\text{ and }\forall 0\leq
j<i\mathpunct{.}\Pi[j,\infty]\models_{\mathcal{G}}\varphi$ $\displaystyle\Pi$
$\displaystyle\models_{\mathcal{G}}\llangle A\rrangle\pi\mathpunct{.}\varphi$
iff $\displaystyle\exists F_{A}\mathpunct{.}\forall
p\in\mathit{out}(\mathcal{G},\Pi(\epsilon)(0),F_{A})\mathpunct{.}\Pi[\pi\mapsto
p]\models_{\mathcal{G}}\varphi$

Here $\Pi(\epsilon)$ refers to the path that was last added to the assignment
(similar to the HyperCTL∗ semantics [CFK+14])444If we assume the path
variables quantified in a formula are distinct (which we can always ensure by
$\alpha$-renaming), we can view a path assignment $\Pi$ as a finite list of
pairs in $\mathcal{V}\times S^{\omega}$, interpret $\Pi[\pi\mapsto p]$ as
appending the pair $(\pi,p)$ to the list and interpret $\Pi(\epsilon)$ as the
path of the last pair in the list.. If $\Pi$ is the empty assignment, we
define $\Pi(\epsilon)(0)$ as the initial state $s_{0}$ of $\mathcal{G}$. We
say that $\mathcal{G}$ satisfies $\varphi$, written
$\mathcal{G}\models\varphi$, if $\emptyset\models_{\mathcal{G}}\varphi$ where
$\emptyset$ is the empty path assignment.

######  Remark 3.

Note that the games used to produce paths in a strategy quantification
$\llangle A\rrangle\pi\mathpunct{.}\varphi$ are _local_ , i.e., the outcome of
the game is fixed (and bound to $\pi$) before $\varphi$ is evaluated further.
The strategy for agents in $A$ is quantified after the outer paths (bounds to
the path variables that are free in $\llangle
A\rrangle\pi\mathpunct{.}\varphi$) are fixed. For example, in a formula of the
form $\forall\pi.\llangle A\rrangle\pi^{\prime}.\varphi$ the agents in $A$
know the already fixed path bound to $\pi$ but behave as a strategy w.r.t.
$\pi^{\prime}$. In particular, $\forall\pi.\exists\pi^{\prime}.\varphi$
corresponds directly to the (syntactically identical) HyperCTL∗ property.
$\vartriangleleft$

######  Proposition 4.

HyperATL∗ subsumes HyperCTL∗ (and thus HyperLTL) and ATL∗.

The resulting hierarchy is depicted in Figure 1.

#### Extension 1: Extended Path Quantification

Oftentimes, it is convenient to compare different game structures with respect
to a hyperproperty. For _linear_ HyperATL∗ properties, we consider formulas
with extended path quantification. We write $\llangle
A\rrangle_{\mathcal{G}}\,\pi.\varphi$ to quantify path $\pi$ via a game played
in $\mathcal{G}$555Note that this is possible for linear formulas, as each
play starts in the initial state of $\mathcal{G}$ irrespective of the current
path assignment. Syntactically, we use names (variables) for the game
structures and evaluate the formula in an environment that maps names to
concrete structures. See, e.g., [Rab16, §5.4] for details in the context of
HyperCTL∗. . For example, $\forall_{\mathcal{G}}\,\pi.~{}\llangle
A\rrangle_{\mathcal{G}^{\prime}}\,\pi^{\prime}.~{}\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
o_{\pi^{\prime}})$ states that for each path $\pi$ in $\mathcal{G}$ the agents
in $A$ have a strategy in $\mathcal{G}^{\prime}$ that produces only paths
$\pi^{\prime}$ which agrees with $\pi$ on $o$ (where $o$ is a shared
proposition between $\mathcal{G}$ and $\mathcal{G}^{\prime}$).

#### Extension 2: Parallel Composition

We extend HyperATL∗ with a syntactic construct that allows multiple paths to
be resolved in a single bigger game, where individual copies of the system
progress in parallel. Consider the following modification to the HyperATL∗
syntax, where $k\geq 1$:

$\displaystyle\varphi,\psi:=[\llangle
A_{1}\rrangle\pi_{1}.~{}\cdots~{}\llangle A_{k}\rrangle\pi_{k}.]~{}\varphi\mid
a_{\pi}\mid\neg\varphi\mid\varphi\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}}}\varphi\mid\varphi\operatorname{\mathcal{U}}\psi$

When surrounding strategy quantifiers by $[\cdot]$ the resulting paths are the
outcome of a game played on a bigger, parallel game of the structure.
Consequently, the agents in each copy can base their decisions not only on the
current state of their copy but on the combined state of all $k$ copies (which
allows for a coordinated behavior among the copies). For a player $\xi$ and
CGS $\mathcal{G}=(S,s_{0},\Xi,\mathcal{M},\delta,L)$, a $k$-strategy for $\xi$
is a function $f_{\xi}:(S^{k})^{+}\to\mathcal{M}$.

For a system $\mathcal{G}$, sets of $k$-strategies strategies
$F_{A_{1}},\cdots,F_{A_{k}}$ and states $s_{1},\cdots,s_{k}$, we define
$\mathit{out}(\mathcal{G},(s_{1},\cdots,s_{k}),F_{A_{1}},\cdots,F_{A_{k}})$ as
all plays $u\in(S^{k})^{\omega}$ such that 1) $u(0)=(s_{1},\cdots,s_{k})$, and
2) for every $i\in\mathbb{N}$ there exist global move vectors
$\sigma_{1},\cdots,\sigma_{k}$ such that
$u(i+1)=\left(\delta(t_{1},\sigma_{1}),\cdots,\delta(t_{k},\sigma_{k})\right)$
where $u(i)=(t_{1},\cdots,t_{k})$ and for every $j\in\\{1,\cdots,k\\}$, agent
$\xi\in A_{j}$ and strategy $f_{\xi}\in F_{A_{j}}$ ,
$\sigma_{j}(\xi)=f_{\xi}(u[0,i])$.  $\vartriangleleft$

The definition of $k$-strategy and
$\mathit{out}(\mathcal{G},(s_{1},\cdots,s_{k}),F_{A_{1}},\cdots,F_{A_{k}})$
extends naturally if we consider MSCGSs instead of CGSs. We extend our
semantics by the following judgment:

$\displaystyle\Pi$ $\displaystyle\models_{\mathcal{G}}[\llangle
A_{1}\rrangle\pi_{1}.~{}\cdots~{}\llangle
A_{k}\rrangle\pi_{k}.]~{}\varphi\;\text{iff }$ $\displaystyle\exists
F_{A_{1}},\cdots,F_{A_{k}}.\forall(p_{1},\cdots,p_{k})\in\mathit{out}(\mathcal{G},(\Pi(\epsilon)(0),\cdots,\Pi(\epsilon)(0)),F_{A_{1}},\cdots,F_{A_{k}}).\Pi[\pi_{i}\mapsto
p_{i}]_{i=1}^{k}\models_{\mathcal{G}}\varphi$

Here we consider
$\mathit{out}(\mathcal{G},(s_{1},\cdots,s_{k}),F_{A_{1}},\cdots,F_{A_{k}})$ as
a set of elements in $(S^{\omega})^{k}$ instead of $(S^{k})^{\omega}$ using
the natural correspondence (given by $\otimes^{-1}$). Note that $[\llangle
A\rrangle\pi.]~{}\varphi$ is equivalent to $\llangle A\rrangle\pi.\varphi$.

##  4\. Strategic Hyperproperties and Information-Flow Control

Before discussing the automated verification of HyperATL∗ properties, we
consider example properties expressed in HyperATL∗. We organize our examples
into two categories. We begin with examples from information-flow control and
highlight the correspondence with existing properties and security paradigms
(this is done in this section). Afterward (in Section 5), we show that
strategic hyperproperties are naturally suited to express asynchronous
hyperproperties.

######  Remark 5.

In our discussion of information-flow policies, we focus on game structures
that result from reactive systems. Let $H,L$ and $O$ be pairwise disjoint sets
of atomic propositions denoting high-security inputs, low-security inputs, and
outputs. We consider a system as a 3-payer game structure comprising agents
$\xi_{N},\xi_{H}$ and $\xi_{L}$ responsible for resolving non-determinism and
selecting high-security and low-security inputs. In particular, the move from
$\xi_{H}$ (resp. $\xi_{L}$) determines the values of the propositions in $H$
(resp. $L$) in the next step and $\xi_{N}$ resolves the remaining non-
determines in the system. We call a CGS of the above form a _progCGS_
(program-CGS). We will see a concrete transformation of finite-state programs
into progCGSs in Section 8.1. For now, we rely on the reader’s intuition. We
call a progCGS _input-total_ if, in each step, $\xi_{H}$ and $\xi_{L}$ can
choose _all_ possible valuations for the input propositions in $H$ and $L$
respectively; we assume all progCGSs in this section to be input total.
$\vartriangleleft$

###  4.1. Strategic Non-Interference

In the introduction, we already saw that, in some cases, generalized non-
interference [McC88] is a too relaxed notion of security, as the witness path
is fixed knowing the entire future input/output sequence. Recall the
definition of GNI (compared to the introduction, we now assume the presence of
low-security inputs).

$\displaystyle\forall\pi\mathpunct{.}\forall\pi^{\prime}\mathpunct{.}\exists\pi^{\prime\prime}\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}}}\big{(}\bigwedge_{a\in
H}a_{\pi}\leftrightarrow
a_{\pi^{\prime\prime}}\big{)}\land\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}}}\big{(}\bigwedge_{a\in
L\cup O}a_{\pi^{\prime}}\leftrightarrow a_{\pi^{\prime\prime}}\big{)}$ (GNI)

In HyperATL∗, we express.

$\displaystyle\forall\pi\mathpunct{.}\llangle\\{\xi_{N},\xi_{L}\\}\rrangle\pi^{\prime}\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}}}\big{(}\bigwedge_{a\in
L\cup O}a_{\pi}\leftrightarrow a_{\pi^{\prime}}\big{)}$ (stratNI)

In this formula, a strategy for the $\xi_{N}$ and $\xi_{L}$ should construct a
path $\pi^{\prime}$ that agrees with the low-security inputs and outputs of
$\pi$. Note that $\xi_{L}$ only determines the value of the propositions in
$L$ so any winning strategy for $\xi_{L}$ is “deterministic” in the sense that
it needs to copy the low-security inputs from $\pi$. Agent $\xi_{N}$ needs to
resolve the non-determinism, but does not know the future high-security inputs
on $\pi^{\prime}$ (as those are chosen by $\xi_{H}$). If there exists a
winning _strategy_ for $\xi_{N}$ that avoids information leakage, there also
exists a path (in the sense of GNI) that disproves leakage.

######  Lemma 6.

For any progCGS $\mathcal{G}$, if $\mathcal{G}\models\ref{prop:stratNI}$ then
$\mathcal{G}\models\ref{prop:GNI}$.

######  Proof 4.1.

We show the contraposition and assume that
$\mathcal{G}\not\models\ref{prop:GNI}$. There thus exists paths $p_{H}$ and
$p_{L,O}$ such that no path in $\mathcal{G}$ agrees with the high inputs of
$p_{H}$ and low-security inputs and outputs of $p_{L,O}$. We show that
$\mathcal{G}\not\models\ref{prop:stratNI}$. For the universally quantified
path bound to $\pi$ we choose $p_{L,O}$ and argue that $\xi_{N},\xi_{L}$ have
no winning strategy to construct $\pi^{\prime}$. A spoiling strategy for
$\xi_{H}$ is the one that, in each step, chooses the high-security inputs in
accordance with $p_{H}$ (which is possible as the system is input-total). A
winning strategy for $\xi_{N}$ and $\xi_{L}$ would then need to construct a
path that agrees with $p_{H}$ on $H$ and with $p_{L,O}$ on $L\cup O$ which, by
assumption, does not exist.

###  4.2. Parallel Composition and $\forall\exists$-verification

Our next examples make use of the parallel composition in form of the
$[\llangle A_{1}\rrangle\pi_{1}.~{}\cdots~{}\llangle A_{k}\rrangle\pi_{k}.]$
quantifier. We consider the model checking algorithm for
$\forall^{*}\exists^{*}$-HyperLTL formulas introduced by Coenen et al.
[CFST19]. The idea is to consider the verification of HyperLTL-formula
$\forall\pi\mathpunct{.}\exists\pi^{\prime}\mathpunct{.}\varphi$ as a game
between the $\forall$-player and $\exists$-player. The $\forall$-player moves
through a copy of the state space (thereby producing a path $\pi$) and the
$\exists$-player reacts with moves in a separate copy (thereby producing a
path $\pi^{\prime}$). The $\exists$-player wins if $\pi^{\prime}$ combined
with $\pi$ satisfies $\varphi$, in which case the property holds (the reveres
of this implication does not hold in general). This game-based verification is
expressible as a logical statement in HyperATL∗: Formula
$[\forall\pi.\exists\pi^{\prime}].\varphi$ requires a strategy that constructs
$\pi^{\prime}$ when played in parallel with a game that constructs $\pi$. A
system thus satisfies $[\forall\pi.\exists\pi^{\prime}].\varphi$ exactly if
the property can be verified in the game-based approach from [CFST19].

While [CFST19] derives a verification _method_ , HyperATL∗ can express both
the original HyperLTL-property and the game-based property as _formulas_ ; the
correctness of the algorithm from [CFST19] becomes a logical implication in
HyperATL∗. Lemma 7 states a more general implication (by considering a
property $\forall\pi.\llangle A\rrangle\pi^{\prime}.\varphi$ instead of
$\forall\pi.\exists\pi^{\prime}.\varphi$).

######  Lemma 7.

Let $\mathcal{G}$ be any game structure and $\varphi$ be any HyperATL∗
formula. If $\mathcal{G}\models[\forall\pi.\llangle
A\rrangle\pi^{\prime}.]\varphi$ then $\mathcal{G}\models\forall\pi.\llangle
A\rrangle\pi^{\prime}.\varphi$.

######  Proof 4.2.

Assume that $\mathcal{G}\models[\forall\pi.\llangle
A\rrangle\pi^{\prime}.]\varphi$. Let $F_{A}=\\{f_{\xi}:(S\times
S)^{+}\to\mathcal{M}\mid\xi\in A\\}$ be the set of strategies for the agents
in $A$ that is wining, i.e., for every
$(p,p^{\prime})\in\mathit{out}(\mathcal{G},(s_{0},s_{0}),\emptyset,F_{A})$ we
have $[\pi\mapsto p,\pi^{\prime}\mapsto p^{\prime}]\models\varphi$. We show
that $\mathcal{G}\models\forall\pi.\llangle A\rrangle\pi^{\prime}.\varphi$.
Let $\Pi=[\pi\mapsto p]$ be any path assignment for $\pi$ (which is
universally quantified). We construct a winning strategy
$f_{\xi}^{\prime}:S^{+}\to\mathcal{M}$ for each $\xi\in A$. For $u\in S^{+}$
define

$\displaystyle f_{\xi}^{\prime}(u):=f_{\xi}(u\otimes p[0,|u|-1])$

Strategy $f_{\xi}^{\prime}$ disregards most of the already fixed path $p$ and
queries $f_{\xi}$ on prefixes of $p$. Let
$F_{A}^{\prime}=\\{f_{\xi}^{\prime}\mid\xi\in A\\}$. It is easy to see that
for each $p^{\prime}\in\mathit{out}(\mathcal{G},s_{0},F_{A}^{\prime})$ we have
$p\otimes
p^{\prime}\in\mathit{out}(\mathcal{G},(s_{0},s_{0}),\emptyset,F_{A})$ and so
$\mathcal{G}\models\forall\pi_{1}.\llangle A\rrangle\pi_{2}.\varphi$ as
required.

Using Lemma 7 (which generalizes easily to formulas of the form
$\forall\pi_{1}.\cdots\forall\pi_{k}.\llangle A\rrangle\pi^{\prime}.\varphi$),
we obtain a stronger HyperATL∗ formula by placing the quantifier prefix of GNI
under a $[\cdot]$. We can manually increase the lookahead to enable the
strategy that is constructing path $\pi^{\prime\prime}$ to peek at future
events on $\pi$ and $\pi^{\prime}$ by shifting the system.

For a game structure
$\mathcal{G}=(S,s_{\mathit{init}},\Xi,\mathcal{M},\delta,L)$ and $n\in{\rm
Nature}_{\geq 1}$ we define

$\displaystyle\mathit{shift}(\mathcal{G},n):=(S\cupdot\\{s_{0},\cdots,s_{n-1}\\},s_{0},\Xi,\mathcal{M},\delta^{\prime},L^{\prime})$

where $s_{0},\cdots,s_{n-1}$ are fresh states not already in $S$,
$\delta^{\prime}$ is defined by $\delta^{\prime}(s,\sigma):=\delta(s,\sigma)$
for $s\in S$, $\delta^{\prime}(s_{i},\sigma):=s_{i+1}$ if $i<n-1$ and
$\delta^{\prime}(s_{n-1},\sigma):=s_{\mathit{init}}$. Labeling $L^{\prime}$ is
defined by $L^{\prime}(s)=L(s)$ if $s\in S$ and $L^{\prime}(s_{i})=\emptyset$.
We define $\mathit{shift}(\mathcal{G},0):=\mathcal{G}$.  $\vartriangleleft$

System $\mathit{shift}(\mathcal{G},n)$ shifts the behavior of $\mathcal{G}$ by
adding $n$ initial steps before continuing as in $\mathcal{G}$. We express a
shifted approximation of GNI as follows.

$\displaystyle\big{[}\forall_{\mathcal{G}}\pi\mathpunct{.}\forall_{\mathcal{G}}\pi^{\prime}\mathpunct{.}\exists_{\mathit{shift}(\mathcal{G},n)}\pi^{\prime\prime}\mathpunct{.}\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}}}\big{(}\bigwedge_{a\in
H}a_{\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}}}^{n}a_{\pi^{\prime\prime}}\big{)}\land\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}}}\big{(}\bigwedge_{a\in
L\cup O}a_{\pi^{\prime}}\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}}}^{n}a_{\pi^{\prime\prime}}\big{)}$
(aproxGNIn)

We shift the behavior of the copy on which $\pi^{\prime\prime}$ is constructed
by $n$ positions which we correct using $n$ $\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}}}$s in the body of the
formula. It is easy to see that if $\mathcal{G}\models\textit{aproxGNI}_{n}$
for some $n$, then $\mathcal{G}\models\ref{prop:GNI}$666This implication is of
practical relevance as aproxGNIn sits at a fragment of HyperATL∗ checkable in
polynomial time (in the size of the system) whereas the
$\forall^{*}\exists^{*}$-fragment of HyperLTL (and thus HyperATL∗) is already
PSPACE-hard [Rab16]. .

###  4.3. Simulation-based Non-Interference

The previously discussed information-flow policies are path-based. By
contrast, _simulation_ -based definitions of non-interference, require a lock-
step security simulation that disproves leakage (see, e.g., [SS00, Sab03,
MS10]). Let
$\mathcal{G}=(S,s_{0},\\{\xi_{N},\xi_{L},\xi_{H}\\},\mathcal{M},\delta,L)$ be
a progCGS. For states $s,s^{\prime}\in S$ and evaluations $i_{L}\in 2^{L}$ and
$i_{H}\in 2^{H}$, we write $s\Rightarrow^{i_{L}}_{i_{H}}s^{\prime}$ if
$L(s^{\prime})\cap L=i_{L}$ and $L(s^{\prime})\cap H=i_{H}$ and $s^{\prime}$
is a possible successor of $s$ in $\mathcal{G}$ (i.e., there exists a move
vector $\sigma$ such that $\delta(s,\sigma)=s^{\prime}$).

A _security simulation_ is a relation $R\subseteq S\times S$ such that
whenever $(s,t)\in R$, we have 1) $s$ and $t$ agree on the output
propositions, i.e., $L(s)\cap O=L(t)\cap O$, and 2) for any $i_{L}\in 2^{L}$
and $i_{H},i^{\prime}_{H}\in 2^{H}$ if
$s\Rightarrow^{i_{L}}_{i_{H}}s^{\prime}$ then there exists a $t^{\prime}$ with
$t\Rightarrow^{i_{L}}_{i^{\prime}_{H}}t^{\prime}$ and
$(s^{\prime},t^{\prime})\in R$.  $\vartriangleleft$

Note that this is not equivalent to the fact that $R$ is a simulation in the
standard sense [Mil80] as the second condition is asymmetric in the high-
security inputs. We call $\mathcal{G}$ _simulation secure_ if there exists a
security simulation $R$ with $(s_{0},s_{0})\in R$ [Sab03, SS00]. It is easy to
see that every input-total system that is _simulation secure_ satisfies GNI.
The converse does, in general, not hold. HyperATL∗ can express _simulation
security_.

$\displaystyle[\forall_{\mathcal{G}}\,\pi\mathpunct{.}\llangle\\{\xi_{N}\\}\rrangle_{\mathit{shift}(\mathcal{G},1)}\,\pi^{\prime}.]~{}\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}}}\big{(}\bigwedge_{a\in
L}a_{\pi}\leftrightarrow\bigcirc
a_{\pi^{\prime}}\big{)}\to\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}}}\big{(}\bigwedge_{a\in
O}a_{\pi}\leftrightarrow\bigcirc a_{\pi^{\prime}}\big{)}$ (simNI)

Here we shift the path $\pi^{\prime}$ by one position
($\mathit{shift}(\mathcal{G},1)$) which we correct using the
$\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}}}$. The shifting
allows the strategy for $\xi_{N}$ in the second copy to base its decision on
an already fixed step in the first copy, i.e., it corresponds to a strategy
with a fixed lookahead of $1$ step.

######  Lemma 8.

A progCGS $\mathcal{G}$ is _simulation secure_ if and only if
$\mathcal{G}\models\ref{prop:simNI}$.

######  Proof 4.3.

We only sketch the high-level idea as the proof is similar to the well-known
characterization of simulations and bisimulations as two-player games [Sti95]
. For the first direction, we assume that $\mathcal{G}$ is _simulation secure_
and let $R$ be a security simulation witnessing this. The idea of the strategy
for $\xi_{N}$ is to choose successors such that the parallel game between both
copies is always in $R$-related states (after shifting). This is possible as
long as the premise of simNI is not violated. By the definition of security
simulations, this already implies $\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
O}a_{\pi}\leftrightarrow\bigcirc a_{\pi^{\prime}})$. Note that the shifting is
key, so the strategy for $\xi_{N}$ fixes a move _after_ the universality
quantified path chooses a successor (as in the definition of security
simulation). For the second direction assume $\xi_{N}$ has a winning strategy.
We construct the relation $R$ by defining $(s,t)\in R$ whenever the pair
$(s,t)$ occurs in the (shifted) parallel composition in any play for which the
premise of simNI holds.

###  4.4. Non-Deducibility of Strategies

As the last example in this section, we consider _non-deducibility of
strategies_ ($\mathit{NDS}$) [WJ90]. $\mathit{NDS}$ requires that every
possible output is compatible with every possible input-_strategy_ (whereas
GNI requires it to be compatible with every possible input-_sequence_). The
subtle difference between sequences and strategies is important when a high-
security input player can observe the internal state of a system. As a
motivating example, consider the following (first introduced in [WJ90]):

Suppose we have a system that reads a binary input $h$ from a high-security
source and outputs $o$. The system maintains a bit $b$ of information in its
state, initially chosen non-deterministically. In each step, the system reads
the input $h$, outputs $h\oplus b$ (where $\oplus$ is the xor-operation), non-
deterministically picks a new value for $b$ and then repeats. As $\oplus$
encodes an one-time pad, it is not hard to see that this system satisfies GNI:
Given any input, any output is possible by resolving the non-deterministic
choice of $b$ appropriately.

If the input player is, however, able to observe the system (in the context of
[WJ90] the system shares the internal bit on a private channel), she can
communicate an arbitrary sequence of bits to the low-security environment.
Whenever she wants to send bit $c$, she inputs $h=c\oplus b$ where $b$ is the
value of the internal bit (note that $(c\oplus b)\oplus b=c$).
$\vartriangleleft$

Instead of requiring that every output sequence is compatible with all
possible high-security input sequences, we require it to be compatible with
all possible high-security input strategies. Phrased differently, there should
_not_ be an output sequence such that a strategy for the input-player can
_avoid_ this output.

$\displaystyle\neg\exists\pi.~{}\llangle\xi_{H}\rrangle\pi^{\prime}.~{}\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
L}a_{\pi}\leftrightarrow a_{\pi^{\prime}})\to\lozenge(\bigvee_{a\in
O}a_{\pi}\not\leftrightarrow a_{\pi^{\prime}})$ (NDS)

This formula states that there does not exist a path $\pi$ such that $\xi_{H}$
has a strategy to avoid the output of $\pi$ (provided with the same low-
security inputs). The system sketched in Example 4.4 does not satisfy NDS
(there, e.g., exists a strategy for $\xi_{H}$ that ensures that the output $o$
is always set to true). Note that, due to determinacy of parity games, NDS is
equivalent to stratNI on turn-based game structures.

##  5\. Strategic and Asynchronous Hyperproperties

Most existing hyperlogics traverse the paths of a system synchronously.
Especially when reasoning about software systems, one requires an asynchronous
traversal to account, for example, for the unknown execution speed or to
abstract way from intermediate (non-observable) program steps. In this
section, we outline how strategic hyperproperties are useful to express such
asynchronous hyperproperties.

The idea is to express asynchronous hyperproperties by viewing the stuttering
of a system (i.e., whether a system progresses or remains in its current
state) as being resolved by a dedicated player (which we call scheduling
player). Quantification over strategies of the scheduling player then
naturally corresponds asynchronous reasoning. That is, instead of reasoning
about the (asynchronous) scheduling of a system directly, we reason about
strategies for the scheduling agent. This style of asynchronous reasoning can
express many properties while remaining fully decidable (as model checking of
HyperATL∗ is decidable, see Section 6) and yields formulas that are
efficiently checkable (see Section 8).

###  5.1. Scheduling Player and Stuttering Transformation

We call a player $\mathit{sched}$ an asynchronous scheduler if it can decide
whether the system progresses (as decided by the other agents) or stutters.
Note that this differs from the asynchronous turn-based games as defined in
[AHK02]. In our setting, the scheduler does not control which of the player
controls the next move, but rather decides if the system as a whole progresses
or stutters. In cases where the system does not already include an
asynchronous scheduler, we can include a scheduler via a simple system
transformation.

Given a game structure $\mathcal{G}=(Q,q_{0},\Xi,\mathcal{M},\delta,d,L)$ over
$\mathit{AP}$ and a fresh agent _sched_ not already included in $\Xi$. Define
the stutter version of $\mathcal{G}$, denoted $\mathcal{G}_{\mathit{stut}}$,
as the game structure over $\mathit{AP}\cupdot\\{\mathit{stut}\\}$ by
$\mathcal{G}_{\mathit{stut}}:=(Q\times\\{0,1\\},(q_{0},0),\Xi\cupdot\\{\mathit{sched}\\},\mathcal{M}\times\\{\rightarrowtail,\downarrowtail\\},\delta^{\prime},d^{\prime},L^{\prime})$
where

$\displaystyle\delta^{\prime}((s,\\_),\sigma):=\begin{cases}\begin{aligned}
&(\delta(s,\mathit{proj}_{1}\circ\sigma_{\mid\Xi}),0)\quad&&\text{if
}(\mathit{proj}_{2}\circ\sigma)(\mathit{sched})=\rightarrowtail\\\
&(s,1)\quad&&\text{if
}(\mathit{proj}_{2}\circ\sigma)(\mathit{sched})=\downarrowtail\end{aligned}\end{cases}$

$L^{\prime}((s,0)):=L(s)$ and $L^{\prime}(s,1)"=L(s)\cup\\{\mathit{stut}\\}$.
Finally $d^{\prime}(\xi)"=d(\xi)$ for $\xi\in\Xi$ and
$d^{\prime}(\mathit{sched}):=m+1$ where $m$ is the maximal element in the
codomain of $d$.  $\vartriangleleft$

Here $\mathit{proj}_{i}$ is the projection of the $i$th element in a tuple,
$\circ$ denotes function composition, and $\\_$ represents an arbitrary value
in that position. In $\mathcal{G}_{\mathit{stut}}$, the agents of the original
game structure $\mathcal{G}$, fix moves in $\mathcal{M}$ and thereby determine
the next state of the system. In addition, the
$\\{\rightarrowtail,\downarrowtail\\}$-decision of scheduling player
determines if the move is actually made ($\rightarrowtail$) or if the system
remains in its current state ($\downarrowtail$). As $\mathit{sched}$ sits in
the last stage of the MSCGS, the scheduling decision is based on the already
fixed moves of the agents in $\Xi$. The extended state-space
$Q\times\\{0,1\\}$ is used to keep track of the stuttering which becomes
visible via the new atomic proposition $\mathit{stut}$.

###  5.2. Observational Determinism

As a warm-up, we again consider the property of observational-determinism
which states that the output along all paths is identical, i.e.,
$\forall\pi\mathpunct{.}\forall\pi^{\prime}\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}}}\big{(}\bigwedge_{a\in
O}a_{\pi}\leftrightarrow a_{\pi^{\prime}}\big{)}$. We already argued that the
example program in the introduction (in Figure 2) does not satisfy this
property (if interpreted as a transition system in the natural way), as the
output changes at different time points. To express an asynchronous version of
OD, we reason about (a strategy for) the scheduling player on the transformed
system.

$\displaystyle[\llangle\mathit{sched}\rrangle\pi.\llangle\mathit{sched}\rrangle\pi^{\prime}.]\;\mathit{fair}_{\pi}\land\mathit{fair}_{\pi^{\prime}}\land\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}}}\Big{(}\bigwedge_{a\in
O}a_{\pi}\leftrightarrow a_{\pi^{\prime}}\Big{)}$ (ODasynch)

where $\mathit{fair}_{\pi}:=\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}}}\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\mathit{stut}_{\pi}$,
asserts that the system may not be stuttered forever. Note that we
encapsulated the quantifiers by $[\cdot]$ thus resolving the games in
parallel. Note that $\mathit{sched}$ only controls the stuttering and not the
path of the underlying system. The example from Figure 2, after the stuttering
transformation, satisfies this formula, as the output can be aligned by the
scheduling player.

###  5.3. One-Sided Stuttering

By resolving the stuttered paths incrementally (i.e., omitting the
$[\cdot]$-brackets) we can also express _one-sided stuttering_ , i.e., allow
only the second copy to be stuttered. As an example, assume $P^{h}$ is a
program written in a higher-level programming language and $P^{l}$ the
complied program into a low-level language (e.g., assembly code). Let
$\mathcal{T}^{\mathit{h}}$ and $\mathcal{T}^{\mathit{l}}$ be transition
systems of both programs, and consider the property that the low-level program
program exhibits the same output as the original program. As the compiler
breaks each program statement into multiple low-level instructions, the
outputs will not match in a synchronous manner. Instead, the system
$\mathcal{T}^{h}$ should be stuttered for the low-level program to “catch up”.
Using Definition 5.1 we can express this as follows.

$\displaystyle\forall_{\mathcal{T}^{\mathit{l}}}\,\pi.\;\llangle\mathit{sched}\rrangle_{\mathcal{T}^{\mathit{h}}_{\mathit{stut}}}\,\pi^{\prime}\mathpunct{.}\mathit{fair}_{\pi^{\prime}}\land\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}}}\Big{(}\bigwedge_{a\in
O}a_{\pi}\leftrightarrow a_{\pi^{\prime}}\Big{)}$

I.e., for every execution $\pi$ of the assembly code we can stutter the
program such that the observations align.

###  5.4. Asynchronous HyperLTL

We compare the strategic approach on asynchronicity of HyperATL∗ (in Section
5.2) with _asynchronous HyperLTL_ (AHLTL for short) [BCB+21], a recent
extension of HyperLTL specifically designed to express asynchronous
properties. AHLTL is centered around the stuttering of a path. A path
$p^{\prime}$ is a stuttering of $p$, written $p\trianglelefteq p^{\prime}$, if
it is obtained by stuttering each step in $p$ finitely often. Formulas in
AHLTL quantify universally or existentially over stuttering of paths. For
example, the AHLTL formula
$\forall\pi_{1}.\cdots\forall\pi_{n}.\mathbf{E}.\varphi$ holds on a transition
system $\mathcal{T}$ (written
$\mathcal{T}\models_{\texttt{AHLTL}}\forall\pi_{1}.\cdots\forall\pi_{n}.\mathbf{E}.\varphi$)
if for all path $p_{1},\cdots,p_{n}$ in the $\mathcal{T}$, there exists
stutterings $p^{\prime}_{1},\cdots,p^{\prime}_{n}$ that (when bound to
$\pi_{1},\cdots,\pi_{n}$) satisfy $\varphi$. Different from the asynchronous
treatment in HyperATL∗, the stuttering in AHLTL is quantified after all paths
are fixed. Finite-state model checking of AHLTL is undecidable, already for
formulas of the form $\forall\pi_{1}.\forall\pi_{2}.\mathbf{E}.\varphi$
[BCB+21].

The largest known fragment of AHLTL with decidable model-checking are formulas
of the form $\forall\pi_{1}.\cdots\forall\pi_{n}.\mathbf{E}.\varphi$ where
$\varphi$ is an _admissible formula_. An admissible formula has the form

$\displaystyle\varphi=\varphi_{\mathit{state}}\land\big{(}\bigwedge_{i=1}^{n}\varphi_{\mathit{stut}}^{i}\big{)}\land\varphi_{\mathit{phase}}$

where $\varphi_{\mathit{state}}$ is a state-formula, i.e., uses no temporal
operators, each $\varphi_{\mathit{stut}}^{i}$ is a stutter invariant formula
that only refers to a single path variable and $\varphi_{\mathit{phase}}$ is a
phase formula which is a conjunction of formulas of the form
$\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
P}(a_{\pi_{i}}\leftrightarrow a_{\pi_{j}})$. The phase formula requires the
two paths $\pi_{i}$ and $\pi_{j}$ two traverse the same sequence (phases) of
“colors” defined by $P$. See [BCB+21, §4.1] for a more detailed discussion.

By replacing the stuttering quantifier $\mathbf{E}$ in AHLTL with strategy
quantification in HyperATL∗ we obtain a sound approximation.

######  Theorem 9.

Assume a transition system $\mathcal{T}$ and AHLTL formula
$\forall\pi_{1}.\cdots\forall\pi_{n}.\mathbf{E}.\varphi$. If

$\displaystyle\mathcal{T}_{\mathit{stut}}\models[\llangle\mathit{sched}\rrangle\pi_{1}.\cdots\llangle\mathit{sched}\rrangle\pi_{n}]~{}\varphi\land\bigwedge_{i\in\\{1,\cdots,n\\}}\mathit{fair}_{\pi_{i}}$
(1)

then

$\displaystyle\mathcal{T}\models_{\texttt{AHLTL}}\forall\pi_{1}.\cdots\forall\pi_{n}.\mathbf{E}.\varphi$
(2)

If $n=2$ and $\varphi$ is an admissible formula, 1 and 2 are equivalent.

######  Proof 5.1.

Let $\mathcal{T}=(S,s_{0},\delta,L)$. We first show that 1 implies 2. Assume 1
and let
$f_{\mathit{sched}}^{i}:(S^{n})^{+}\to\mathcal{M}\times\\{\rightarrowtail,\downarrowtail\\}$
for $1\leq i\leq n$ be a winning strategy for the scheduler. To show 2 let
$p_{1},\cdots,p_{n}$ be any paths in $\mathcal{T}$. For each $1\leq i\leq n$
we define a stuttered version $p_{i}^{\prime}$ such that $p_{i}\trianglelefteq
p_{i}^{\prime}$. As intermediate steps we define $p_{1,m},\cdots,p_{n,m}\in
S^{m}$ and $c_{1,m},\cdots,c_{n,m}\in{\rm Nature}$ for each $m\in{\rm
Nature}_{\geq 1}$ by recursion on $m$. For $m=1$, we set $p_{i,1}=p_{i}(0)$,
i.e., a path of length $1$ and $c_{i,1}=1$ for each $1\leq i\leq n$. For
$m>1$, define $b_{i,m}:=\mathit{proj}_{2}\circ
f^{i}_{\mathit{sched}}(\otimes(p_{1,m-1},\cdots,p_{n,m-1}))$ for each $1\leq
i\leq n$. If $b_{i,m}=\rightarrowtail$, we define $c_{i,m}:=c_{i,m-1}+1$ and
if $b_{i,m}=\downarrowtail$ we define $c_{i,m}:=c_{i,m-1}$. We then set
$p_{i,m}:=p_{i,m}\cdot p_{i}(c_{i,m})$ (where $\cdot$ denotes sequence
concatenation). Define $p_{i}^{\prime}\in S^{\omega}$ as the limit of
$\\{p_{i,m}\\}_{m\in{\rm Nature}_{\geq 1}}$ (which exists as $p_{i,m}$ is a
prefix of $p_{i,m+1}$ for every $m$). It is easy to see that
$p_{i}\trianglelefteq p_{i}^{\prime}$ (the fairness assumption in 1 ensures
that that a path is not stuttered forever). Moreover $[\pi_{1}\mapsto
p^{\prime}_{1},\cdots,\pi_{n}\mapsto p^{\prime}_{n}]\models\varphi$ holds as
$\\{f_{\mathit{sched}}^{i}\\}_{i=1}^{n}$ is winning and so $[\pi_{1}\mapsto
p_{1},\cdots,\pi_{n}\mapsto p_{n}]\models_{\texttt{AHLTL}}\mathbf{E}.\varphi$
as required.

For the second direction assume 2 and that $\varphi$ is admissible. Let
$\varphi=\varphi_{\mathit{state}}\land\big{(}\bigwedge_{i=1}^{l}\varphi_{\mathit{stut}}^{i}\big{)}\land\varphi_{\mathit{phase}}$.
State formula $\varphi_{\mathit{state}}$ only refers to the initial states (as
it is free of temporal operators) and $\varphi_{\mathit{stut}}^{i}$ is, by
assumption, stutter invariant, so any fair scheduling chosen by
$\mathit{sched}$ satisfies both $\varphi_{\mathit{state}}$ and
$\bigwedge_{i=1}^{l}\varphi_{\mathit{stut}}^{i}$. Let
$\varphi_{\mathit{phase}}=\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
P}(a_{\pi_{1}}\leftrightarrow a_{\pi_{2}})$ be the phase formula. We say two
states $s,s^{\prime}\in S$ are _about to change phase_ if for some $a\in P$ we
have $a\in L(s)\not\leftrightarrow a\in L(s^{\prime})$. In this case we write
$\mathit{change}(s,s^{\prime})$. The strategy for the scheduler has access to
both the current state $s_{1},s_{2}$ of both copies and the next state
$s^{\prime}_{1},s^{\prime}_{2}$ in both copies (as the scheduler sits at the
last stage of $\mathcal{T}_{\mathit{stut}}$). The joint strategy for the
scheduler in both copies behaves as follows: If
$\mathit{change}(s_{1},s_{1}^{\prime})\leftrightarrow\mathit{change}(s_{2},s_{2}^{\prime})$
holds, i.e., either both or none of the copies are about to change phase, it
schedules _both_ copies. Otherwise, it only schedules the copy that is _not_
about to change phase. This ensures that phase changes occur synchronized in
both copies. As we assumed 2, there is a stuttering for all paths in the
system such that $\varphi_{\mathit{phase}}$ holds, i.e., all paths traverse
the same phases, albeit at possibly different speeds. It is easy to see that
the strategy defined above, creates an alignment into identical phases for any
two paths of the system. Consequently, any play compatible with this strategy
satisfies $\varphi_{\mathit{phase}}$ (and therefore also $\varphi$) and so 1
holds as required.

Theorem 9 gives a sound approximation of the (undecidable) AHLTL model
checking that is exact for admissible formulas. As HyperATL∗ model checking is
decidable (see Section 6) and the stuttering construction
$\mathcal{T}_{\mathit{stut}}$ is effectively computable, we derive an
alternative proof of the decidability result from [BCB+21]. In summary,
HyperATL∗ subsumes the largest (known) decidable fragment of AHLTL, while
enjoying decidable model checking for the full logic. The HyperATL∗ formula
constructed in Theorem 9 falls in the fragment supported by our model checker
(Section 8).

##  6\. Automata-Based Model Checking

In this section, we present an automata-based model checking algorithm for
HyperATL∗, i.e., given formula $\dot{\varphi}$ (we use the dot to refer to the
original formula and use $\varphi,\psi$ to refer to sub-formulas of
$\dot{\varphi}$) and game structure
$\mathcal{G}=(S,s_{0},\Xi,\mathcal{M},\delta,d,L)$ decide if
$\mathcal{G}\models\dot{\varphi}$. Before discussing our verification
approach, let us briefly recall ATL∗ model checking [AHK02] and why the
approach is not applicable to HyperATL∗. In ATL∗, checking if $\llangle
A\rrangle\varphi$ holds in some state $s$, can be reduced to the non-emptiness
check of the intersection of two tree automata. One accepting all possible
trees that can be achieved via a strategy for players in $A$ starting in $s$,
and one accepting all trees whose paths satisfy the path formula $\varphi$
[AHK02]. In our hyperlogic this is not possible. When checking $\llangle
A\rrangle\pi.\varphi$ we can not construct an automaton accepting all trees
that satisfy $\varphi$, as the satisfaction of $\varphi$ depends on the paths
assigned to the outer path-quantifiers (which are not yet fixed).

Instead, we construct an automaton that accepts all _path assignments_ for the
outer quantifiers for which there exists a winning strategy for the agents in
$A$ (similar to the model checking approach for HyperCTL∗ [FRS15]). Different
from the approach for HyperCTL∗, we can not resolve path quantification via
existential or universal projection and instead encode the strategic behavior
of $\mathcal{G}$ within the transition function of an _alternating_ automaton.

In the following we 1) define a notion of equivalence between formulas and
automata and discuss the overall model checking algorithm (in Section 6.1), 2)
give an inductive construction of an equivalent automaton (in Section 6.2), 3)
prove the construction correct (in Section 6.3) and 4) discuss the complexity
of our algorithm (in Section 6.4).

###  6.1. $\mathcal{G}$-Equivalence and Model Checking Algorithm

Recall that for paths $p_{1},\cdots,p_{n}\in S^{\omega}$,
$\otimes(p_{1},\cdots,p_{n})\in(S^{n})^{\omega}$ denotes the pointwise product
(also called the zipping). Assume that some HyperATL∗ formula $\psi$ contains
free path variables $\pi_{1},\cdots,\pi_{n}$ (in our algorithm $\psi$ is a
sub-formula of $\dot{\varphi}$ that occurs under path quantifiers that bind
$\pi_{1},\cdots,\pi_{n}$). We say that an automaton $\mathcal{A}$ over
alphabet $\Sigma_{\psi}:=S^{n}$ is _$\mathcal{G}$ -equivalent_ to $\psi$, if
for any paths $p_{1},\cdots,p_{n}$ it holds that

$\displaystyle[\pi_{i}\mapsto
p_{i}]_{i=1}^{n}\models_{\mathcal{G}}\psi\quad\text{iff}\quad\otimes(p_{1},\cdots,p_{n})\in\mathcal{L}(\mathcal{A})$

That is, $\mathcal{A}$ accepts a zipping of paths exactly if the path
assignment constructed from those paths satisfies the formula; $\mathcal{A}$
summarizes all path assignments for the free variables that satisfy a formula.

Now let $\dot{\varphi}$ be the formula to be checked. Our model checking
algorithm progresses in an (inductive) bottom-up manner and constructs an
automaton $\mathcal{A}_{\psi}$ that is $\mathcal{G}$-equivalent for each
subformula $\psi$ of $\dot{\varphi}$ (we give the construction in the next
section). Consequently, we obtain an automaton $\mathcal{A}_{\dot{\varphi}}$
over alphabet $\Sigma_{\dot{\varphi}}=S^{0}$ that is $\mathcal{G}$-equivalent
to $\dot{\varphi}$. By definition of $\mathcal{G}$-equivalence,
$\mathcal{A}_{\dot{\varphi}}$ is non-empty iff
$\emptyset\models_{\mathcal{G}}\dot{\varphi}$ iff
$\mathcal{G}\models\dot{\varphi}$. As emptiness of an alternating parity
automaton is decidable [KV98] we obtain a model-checking algorithm for
HyperATL∗.

###  6.2. Construction of $\mathcal{G}$-Equivalent Automata

We give an inductive construction of a $\mathcal{G}$-equivalent automaton. We
include disjunction ($\lor$) and release ($\operatorname{\mathcal{R}}$) as
first-class operators and $\llbracket A\rrbracket$ as a first-class quantifier
(opposed to derived operators and quantifier) as this later allows us to
consider formulas in negation normal form. In the following, we give a
construction of a $\mathcal{G}$-equivalent automaton for each syntactic
construct of HyperATL∗. The most interesting case is the construction for a
formula $\varphi=\llangle A\rrangle\pi.\psi$ where we construct an automaton
$\mathcal{A}_{\varphi}$ over $\Sigma_{\varphi}=S^{n}$ from an automaton
$\mathcal{A}_{\psi}$ over $\Sigma_{\psi}=S^{n+1}$ by a suitable projection
that takes the strategic behavior in $\mathcal{G}$ into account. We split the
construction into the cases of logical and temporal operators (in Figure 3),
simple quantification (in Figure 4), and complex quantification (in Figure 5).

$\varphi=a_{\pi_{i}}$
$\mathcal{A}_{\varphi}:=(\\{q_{\mathit{init}}\\},q_{\mathit{init}},\Sigma_{\varphi},\rho,\mathbf{0})$,
where
$\displaystyle\rho(q_{\mathit{init}},[s_{1},\cdots,s_{n}]):=\begin{cases}\begin{aligned}
\;&\top\quad&&\text{if }a\in L(s_{i})\\\ &\bot\quad&&\text{if }a\not\in
L(s_{i})\end{aligned}\end{cases}$

$\varphi=\neg\psi_{1}$
$\mathcal{A}_{\varphi}:=\overline{\mathcal{A}}_{\psi_{1}}$ where
$\overline{\mathcal{A}}_{\psi_{1}}$ is obtained by Theorem 2.

$\varphi=\psi_{1}\lor\psi_{2}$ $\mathcal{A}_{\varphi}:=(Q_{1}\cupdot
Q_{2}\cupdot\\{q_{\mathit{init}}\\},q_{\mathit{init}},\Sigma_{\varphi},\rho,c_{1}\cupdot
c_{2}\cupdot[q_{\mathit{init}}\mapsto 0])$, where
$\displaystyle\rho(q,[s_{1},\cdots,s_{n}]):=\begin{cases}\begin{aligned}
\;&\rho_{1}(q_{0,1},[s_{1},\cdots,s_{n}])\lor\rho_{2}(q_{0,2},[s_{1},\cdots,s_{n}])\quad&&\text{if
}q=q_{\mathit{init}}\\\ &\rho_{i}(q,[s_{1},\cdots,s_{n}])\quad&&\text{if }q\in
Q_{i}\end{aligned}\end{cases}$

$\varphi=\psi_{1}\land\psi_{2}$ $\mathcal{A}_{\varphi}:=(Q_{1}\cupdot
Q_{2}\cupdot\\{q_{\mathit{init}}\\},q_{\mathit{init}},\Sigma_{\varphi},\rho,c_{1}\cupdot
c_{2}\cupdot[q_{\mathit{init}}\mapsto 0])$, where
$\displaystyle\rho(q,[s_{1},\cdots,s_{n}]):=\begin{cases}\begin{aligned}
\;&\rho_{1}(q_{0,1},[s_{1},\cdots,s_{n}])\land\rho_{2}(q_{0,2},[s_{1},\cdots,s_{n}])\quad&&\text{if
}q=q_{\mathit{init}}\\\ &\rho_{i}(q,[s_{1},\cdots,s_{n}])\quad&&\text{if }q\in
Q_{i}\end{aligned}\end{cases}$

$\varphi=\operatorname{\leavevmode\hbox to8.89pt{\vbox
to8.89pt{\pgfpicture\makeatletter\hbox{\hskip 4.44333pt\lower-1.34334pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.62pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{3.09999pt}\pgfsys@moveto{4.13333pt}{3.09999pt}\pgfsys@curveto{4.13333pt}{5.38278pt}{2.28279pt}{7.23332pt}{0.0pt}{7.23332pt}\pgfsys@curveto{-2.28279pt}{7.23332pt}{-4.13333pt}{5.38278pt}{-4.13333pt}{3.09999pt}\pgfsys@curveto{-4.13333pt}{0.8172pt}{-2.28279pt}{-1.03334pt}{0.0pt}{-1.03334pt}\pgfsys@curveto{2.28279pt}{-1.03334pt}{4.13333pt}{0.8172pt}{4.13333pt}{3.09999pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{3.09999pt}\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_{1}$
$\mathcal{A}_{\varphi}:=(Q_{1}\cup\\{q_{\mathit{init}}\\},q_{\mathit{init}},\Sigma_{\varphi},\rho,c_{1}\cupdot[q_{\mathit{init}}\mapsto
0])$, where
$\displaystyle\rho(q,[s_{1},\cdots,s_{n}]):=\begin{cases}\begin{aligned}
\;&q_{0,1}\quad&&\text{if }q=q_{\mathit{init}}\\\
&\rho_{1}(q,[s_{1},\cdots,s_{n}])\quad&&\text{if }q\in
Q_{1}\end{aligned}\end{cases}$

$\varphi=\psi_{1}\operatorname{\mathcal{U}}\psi_{2}$
$\mathcal{A}_{\varphi}:=(Q_{1}\cupdot
Q_{2}\cupdot\\{q_{\mathit{init}}\\},q_{\mathit{init}},\Sigma_{\varphi},\rho,c_{1}\cupdot
c_{2}\cupdot[q_{\mathit{init}}\mapsto 1])$, where
$\displaystyle\rho(q,[s_{1},\cdots,s_{n}]):=\begin{cases}\begin{aligned}
\;&\rho_{2}(q_{0,2},[s_{1},\cdots,s_{n}])\lor\big{(}\rho_{1}(q_{0,1},[s_{1},\cdots,s_{n}])\land
q_{\mathit{init}}\big{)}\quad&&\text{if }q=q_{\mathit{init}}\\\
&\rho_{i}(q,[s_{1},\cdots,s_{n}])\quad&&\text{if }q\in
Q_{i}\end{aligned}\end{cases}$

$\varphi=\psi_{1}\operatorname{\mathcal{R}}\psi_{2}$
$\mathcal{A}_{\varphi}:=(Q_{1}\cupdot
Q_{2}\cupdot\\{q_{\mathit{init}}\\},q_{\mathit{init}},\Sigma_{\varphi},\rho,c_{1}\cupdot
c_{2}\cupdot[q_{\mathit{init}}\mapsto 0])$, where
$\displaystyle\rho(q,[s_{1},\cdots,s_{n}]):=\begin{cases}\begin{aligned}
\;&\rho_{2}(q_{0,2},[s_{1},\cdots,s_{n}])\land\big{(}\rho_{1}(q_{0,1},[s_{1},\cdots,s_{n}])\lor
q_{\mathit{init}}\big{)}\quad&&\text{if }q=q_{\mathit{init}}\\\
&\rho_{i}(q,[s_{1},\cdots,s_{n}])\quad&&\text{if }q\in
Q_{i}\end{aligned}\end{cases}$

Figure 3. Automaton construction for boolean and temporal operators. Here,
$\mathcal{A}_{\psi_{i}}=(Q_{i},q_{0,i},\Sigma_{\psi_{i}},\rho_{i},c_{i})$ is
the inductively constructed alternating automaton for sub-formula $\psi_{i}$.
We assume that $Q_{1}$ and $Q_{2}$ are disjoint sets of states and
$q_{\mathit{init}}$ is a fresh state. For two colorings $c_{1}:Q_{1}\to{\rm
Nature}$ and $c_{2}:Q_{2}\to{\rm Nature}$, $c_{1}\cupdot c_{2}:Q_{1}\cupdot
Q_{2}\to{\rm Nature}$ denotes the combined coloring. We write $[q\mapsto n]$
for the function $\\{q\\}\to{\rm Nature}$ that maps $q$ to $n$.

#### Boolean And Temporal Operators

For the boolean combinators and temporal operators, our construction follows
the standard translation from LTL to alternating automata (see, e.g., [MSS88,
Var95] or [FRS15] for details). We give the construction in Figure 3. Here
$\mathcal{A}_{\psi_{i}}=(Q_{i},q_{0,i},\Sigma_{\psi_{i}},\rho_{i},c_{i})$ is
an inductively constructed APA for the subformulas $\psi_{i}$.

$\varphi=\exists\pi.\psi$ $\displaystyle\mathcal{A}_{\varphi}:=(S\times
Q\cupdot\\{q_{\mathit{init}}\\},q_{\mathit{init}},\Sigma_{\varphi},\rho^{\prime},c^{\prime})$
where $c^{\prime}(s,q):=c(q)$ and $c^{\prime}(q_{\mathit{init}})$ can be
chosen arbitrarily. The nondeterministic transition function
$\rho^{\prime}:\big{(}S\times
Q\cupdot\\{q_{\mathit{init}}\\}\big{)}\times\Sigma_{\varphi}\to 2^{S\times
Q\cupdot\\{q_{\mathit{init}}\\}}$ is defined via
$\displaystyle\rho^{\prime}(q_{\mathit{init}},[s_{1},\cdots,s_{n}]):=$
$\displaystyle\quad\quad\quad\\{(s^{\prime},q^{\prime})\mid
q^{\prime}\in\rho(q_{0},[s_{1},\cdots,s_{n},s_{n}^{\circ}])\land\exists\sigma:\Xi\to\mathcal{M}\mathpunct{.}\delta(s_{n}^{\circ},\sigma)=s^{\prime}\\}$
$\displaystyle\rho^{\prime}((s,q),[s_{1},\cdots,s_{n}]):=$
$\displaystyle\quad\quad\quad\\{(s^{\prime},q^{\prime})\mid
q^{\prime}\in\rho(q,[s_{1},\cdots,s_{n},s])\land\exists\sigma:\Xi\to\mathcal{M}\mathpunct{.}\delta(s,\sigma)=s^{\prime}\\}$
where we define $s_{n}^{\circ}:=s_{n}$ if $n\geq 1$ and otherwise
$s_{n}^{\circ}:=s_{0}$ (where $s_{0}$ is the initial state of $\mathcal{G}$).
Figure 4. Construction of a $\mathcal{G}$-equivalent automaton for
$\varphi=\exists.\psi$. Here,
$\mathcal{A}_{\psi}^{\mathit{ndet}}=(Q,q_{0},\Sigma_{\psi},\rho,c)$ with
$\rho:Q\times\Sigma_{\psi}\to 2^{Q}$ is a non-deterministic automaton
equivalent of the inductively constructed alternating automaton
$\mathcal{A}_{\psi}$ for $\psi$.

#### Simple Quantification

We now consider the case where $\varphi=\llangle A\rrangle\pi.\psi$ and focus
on the case where the quantifier is _simple_. Assume that $A=\Xi$, i.e.,
$\varphi=\exists\pi.\psi$. The construction of $\mathcal{A}_{\varphi}$ is
similar to the one in [FRS15] by building the existential product of
$\mathcal{A}_{\psi}$ and $\mathcal{G}$. We give the construction in Figure 4.
Here $\mathcal{A}_{\psi}^{\mathit{ndet}}$ is a _non-deterministic_ automaton
equivalent to $\mathcal{A}_{\psi}$ which we can obtain (with an exponential
blowup) via Theorem 1. Automaton $\mathcal{A}_{\varphi}$ guesses a path in
$\mathcal{G}$ and tracks the acceptance of $\mathcal{A}_{\psi}$ on this path
combined with the input word over $S^{n}$, i.e., every accepting run of
$\mathcal{A}_{\varphi}$ on $\otimes(p_{1},\cdots,p_{n})$ guesses a path $p$ in
$\mathcal{G}$ such that $\mathcal{A}_{\psi}$ accepts
$\otimes(p_{1},\cdots,p_{n},p)$. Note that if $\varphi=\exists\pi.\psi$,
$\mathcal{A}_{\varphi}$ is a non-deterministic automaton. The case where
$\varphi=\forall\pi.\psi$ is analogous by converting $\mathcal{A}_{\psi}$ to a
_universal_ automaton $\mathcal{A}_{\psi}^{\mathit{univ}}$ and constructing
the universal product with $\mathcal{G}$. Alternatively, as
$\forall\pi.\varphi\equiv\neg\exists\pi.\neg\varphi$ we can also use the
construction for existential quantification combined with Theorem 2. If
$\varphi=\forall\pi\mathpunct{.}\psi$, $\mathcal{A}_{\varphi}$ is an universal
automaton.

$\varphi=\llangle A\rrangle\pi.\psi$
$\displaystyle\mathcal{A}_{\varphi}:=(S\times
Q\cupdot\\{q_{\mathit{init}}\\},q_{\mathit{init}},\Sigma_{\varphi},\rho^{\prime},c^{\prime})$
where $c^{\prime}(s,q):=c(q)$ and $c^{\prime}(q_{\mathit{init}})$ can be
chosen arbitrarily. Th transition function $\rho^{\prime}:\big{(}S\times
Q\cupdot\\{q_{\mathit{init}}\\}\big{)}\times\Sigma_{\varphi}\to\mathbb{B}^{+}\big{(}S\times
Q\cupdot\\{q_{\mathit{init}}\\}\big{)}$ is defined via
$\displaystyle\rho^{\prime}\big{(}q_{\mathit{init}},[s_{1},\cdots,s_{n}]\big{)}:=$
$\displaystyle\quad\quad\bigvee\limits_{\sigma_{0}:A_{0}\to\mathcal{M}}\bigwedge\limits_{\sigma^{\prime}_{0}:\overline{A}_{0}\to\mathcal{M}}\cdots\bigvee\limits_{\sigma_{m}:A_{m}\to\mathcal{M}}\bigwedge\limits_{\sigma^{\prime}_{m}:\overline{A}_{m}\to\mathcal{M}}\bigg{(}\delta\Big{(}s^{\circ}_{n},\sum_{i=0}^{m}(\sigma_{i}+\sigma^{\prime}_{i})\Big{)},\rho\big{(}q_{0},[s_{1},\cdots,s_{n},s^{\circ}_{n}]\big{)}\bigg{)}$
$\displaystyle\rho^{\prime}\big{(}(s,q),[s_{1},\cdots,s_{n}]\big{)}:=$
$\displaystyle\quad\quad\bigvee\limits_{\sigma_{0}:A_{0}\to\mathcal{M}}\bigwedge\limits_{\sigma^{\prime}_{0}:\overline{A}_{0}\to\mathcal{M}}\cdots\bigvee\limits_{\sigma_{m}:A_{m}\to\mathcal{M}}\bigwedge\limits_{\sigma^{\prime}_{m}:\overline{A}_{m}\to\mathcal{M}}\bigg{(}\delta\Big{(}s,\sum_{i=0}^{m}(\sigma_{i}+\sigma^{\prime}_{i})\Big{)},\rho\big{(}q,[s_{1},\cdots,s_{n},s]\big{)}\bigg{)}$
where we define $s_{n}^{\circ}:=s_{n}$ if $n\geq 1$ and otherwise
$s_{n}^{\circ}:=s_{0}$ (where $s_{0}$ is the initial state of $\mathcal{G}$).
The sets $A_{i}$ and $\overline{A}_{i}$ are defined as $A_{i}:=A\cap
d^{-1}(i)$ and $\overline{A}_{i}:=(\Xi\setminus A)\cap d^{-1}(i)$ and $m$ is
the maximal element in the codomain of $d$. Figure 5. Construction of a
$\mathcal{G}$-equivalent automaton for $\varphi=\llangle A\rrangle.\psi$.
Here, $\mathcal{A}^{\mathit{det}}_{\psi}=(Q,q_{0},\Sigma_{\psi},\rho,c)$ with
$\rho:Q\times\Sigma_{\psi}\to Q$ is a deterministic automaton equivalent to
the inductive constructed alternating automaton $\mathcal{A}_{\psi}$ for
$\psi$.

#### Strategic Quantification

Lastly, we consider the general case where $\varphi=\llangle
A\rrangle\pi.\psi$ (without the restriction that the quantifier is
simple)777Note that the construction in Figure 5 subsumes the construction in
Figure 4. We give an explicit construction for the case of simple
quantification (in Figure 4) as the resulting automaton is exponentially
smaller, giving tight complexity results (see Section 6.4). . In our
construction, $\mathcal{A}_{\varphi}$ encodes the strategic behavior of the
agents in $A$. We achieve this, by encoding the strategic play of the game
structure within the transition function of $\mathcal{A}_{\varphi}$. We give
the construction in Figure 5. Here $\mathcal{A}^{\mathit{det}}_{\psi}$ is a
_deterministic_ automaton equivalent to $\mathcal{A}_{\psi}$ which we obtain
(with a double exponential blowup) via Theorem 1. The transition function
encodes the strategic behavior by disjunctively choosing moves for players in
$A$, followed by a conjunctive treatment of all adversarial players. The
stages of $\mathcal{G}$, naturally correspond to the order of the move
selection (as captured in the sets $A_{i}$ and $\overline{A}_{i}$), giving an
alternating sequence of disjunctions and conjunctions. In the case where the
MSCGS $\mathcal{G}$ is a CGS, i.e., $d=\mathbf{0}$, the transition function
has the form of a (positive) DNF (a boolean formula of the form
$\bigvee\bigwedge$), where the moves of agents in $A$ are considered
disjunctively and the moves by all other agents conjunctively. Our
construction can be extended to handle the self composition $[\llangle
A_{1}\rrangle\pi_{1}.~{}\cdots~{}\llangle A_{k}\rrangle\pi_{k}]$ by joining
the stage across $k$ copies of the game structure. For formulas
$\varphi=\llbracket A\rrbracket\pi.\psi\equiv\neg\llangle
A\rrangle\mathpunct{.}\psi$ we use the above construction combined with
Theorem 2.

###  6.3. Correctness

The correctness of our construction in Section 6.2 is stated by the following
proposition.

######  Proposition 10.

For any HyperATL∗ formula $\varphi$, $\mathcal{A}_{\varphi}$ is
$\mathcal{G}$-equivalent to $\varphi$.

The proof of Proposition 10 goes by induction on $\varphi$ following the
construction of $\mathcal{A}_{\varphi}$. For the logical and temporal
connectives (in Figure 3) and pure existential quantification (in Figure 4),
the statement is obvious (see, e.g., [MSS88, Var95] for the logical and
temporal connectives and [FRS15] for the case of simple existential
quantification). A proof for the case where $\varphi=\llangle
A\rrangle\pi.\psi$ (in Figure 5) can be found in LABEL:app:proofEquiv.

###  6.4. Complexity Upper Bounds

The complexity of our model checking algorithm hinges on the size of the
automaton $\mathcal{A}_{\dot{\varphi}}$. The constructions in Figure 3 only
increases the size of the automaton by a polynomial amount, but the
constructions for path quantification in Figure 4 and Figure 5 increase the
number of states exponentially. We observe a difference in blowup between
simple quantification and complex quantification. The former requires (in
general) a conversion of the alternating automaton $\mathcal{A}_{\psi}$ to a
non-deterministic automaton ($\mathcal{A}_{\psi}^{\mathit{ndet}}$ in Figure 4)
causing an exponential blowup whereas the latter requires a full
determinization ($\mathcal{A}_{\psi}^{\mathit{det}}$ in Figure 5) causing a
_double_ exponential blowup.

To capture the size of the automaton and the resulting complexity of our
algorithm, we define $\mathit{Tower}_{c}(k,n)$ as a tower of $k$ exponents
(with base $c$) , i.e.,

$\displaystyle\mathit{Tower}_{c}(0,n)$ $\displaystyle:=n$
$\displaystyle\mathit{Tower}_{c}(k+1,n)$
$\displaystyle:=c^{\mathit{Tower}_{c}(k,n)}$

For $k\geq 1$ we define $k$-EXPSPACE as the class of languages recognized by a
deterministic (or non-deterministic [Sav70]) Turing machine (TM) with space
$\mathit{Tower}_{c}(k,n)$ for some fixed $c\in{\rm Nature}$. Analogously, we
define $k$-EXPTIME as the class of languages recognizable by a _deterministic_
TM in time $\mathit{Tower}_{c}(k,n)$ for some fixed $c$. We define $0$-EXPTIME
:= PTIME, $0$-EXPSPACE := PSPACE. For $k<0$ we define $k$-EXPSPACE :=
NLOGSPACE.

#### Complexity based on Prefix-Cost

$\displaystyle d_{\mathit{spec}}(\mathbb{Q}\,\pi\mathpunct{.}\psi)$
$\displaystyle:=0$ $\displaystyle
d_{\mathit{spec}}(\mathbb{Q}_{1}\,\pi\mathpunct{.}\mathbb{Q}_{2}\,\pi^{\prime}\mathpunct{.}\varphi)$
$\displaystyle:=d_{\mathit{spec}}(\mathbb{Q}_{2}\,\pi^{\prime}\mathpunct{.}\varphi)+q(\mathbb{Q}_{1},\mathbb{Q}_{2})$
(a) Prefix-costs measured for the _formula_ size. $\psi$ is the quantifier-
free body of the formula. The definition of the cost function $q$ is in Figure
6(c).

$\displaystyle d_{\mathit{sys}}(\exists\pi\mathpunct{.}\psi)$
$\displaystyle:=1$ $\displaystyle
d_{\mathit{sys}}(\forall\pi\mathpunct{.}\psi)$ $\displaystyle:=1$
$\displaystyle d_{\mathit{sys}}(\llangle A\rrangle\pi\mathpunct{.}\psi)$
$\displaystyle:=2$ $\displaystyle d_{\mathit{sys}}(\llbracket
A\rrbracket\pi\mathpunct{.}\psi)$ $\displaystyle:=2$ $\displaystyle
d_{\mathit{sys}}(\mathbb{Q}_{1}\,\pi\mathpunct{.}\mathbb{Q}_{2}\,\pi^{\prime}\mathpunct{.}\varphi)$
$\displaystyle:=d_{\mathit{sys}}(\mathbb{Q}_{2}\,\pi^{\prime}\mathpunct{.}\varphi)+q(\mathbb{Q}_{1},\mathbb{Q}_{2})$
(b) Prefix-costs measured for the _system_ size. $\psi$ is the quantifier-free
body of the formula. The definition of the cost function $q$ is in Figure
6(c).

| $\exists$ | $\forall$ | $\llangle A\rrangle$ | $\llbracket A\rrbracket$
---|---|---|---|---
$\exists$ | $0$ | $1$ | $1$ | $1$
$\forall$ | $1$ | $0$ | $1$ | $1$
$\llangle A\rrangle$ | $1$ | $1$ | $2$ | $2$
$\llbracket A\rrbracket$ | $1$ | $1$ | $2$ | $2$
(c) Cost associated with each quantifier alteration. Given
$\mathbb{Q}_{1},\mathbb{Q}_{2}\in\\{\exists,\forall,\llangle
A\rrangle,\llbracket A\rrbracket\\}$, the cost
$q(\mathbb{Q}_{1},\mathbb{Q}_{2})$ is given in column $\mathbb{Q}_{1}$, row
$\mathbb{Q}_{2}$ (Note that the matrix symmetric).

Figure 6. Definition of prefix-costs in the size of the formula and size of
the system. Here $\llangle A\rrangle$ and $\llbracket A\rrbracket$ represent a
complex quantifier. i.e, $A\neq\emptyset$ and $A\neq\Xi$.

.

We can characterize the cost of our algorithm on a linear HyperATL∗ based on
the structure of the quantifier888Our bounds in this section are stated for
_linear_ HyperATL∗ formulas as this allows for a simpler characterization. For
general HyperATL∗ formulas, we can easily derive that a formula with $k$
complex and $l$ simple quantifiers can be checked in $(2k+l)$-EXPTIME (in the
size of the formula), c.f., Proposition 13. Here we transform the formula into
a negation normal form, where negation only occurs directly in front of atomic
propositions (which is possible as we included release, disjunction and
$\llbracket A\rrbracket$). All construction in Figure 3 are then linear (as we
avoided negation of complex automata) and so the exponent ($c$ in the
definition of $\mathit{Tower}_{c}(\cdot,\cdot)$) is bounded by some function
of $k$ and $l$. . We distinguish between the complexity in the size of the
specification and the size of the system. For a linear formula $\varphi$, we
define the specification-prefix-costs $d_{\mathit{spec}}(\varphi)$ and system-
prefix-costs $d_{\mathit{sys}}(\varphi)$ via the inductive definitions in
Figure 6(a) and Figure 6(b). Our definitions generalize the _alternation-
depth_ used to characterize the HyperLTL model checking complexity [FRS15].

######  Theorem 11.

Model checking a linear HyperATL∗ formula $\varphi$ is

  1. (1)

in $d_{\mathit{spec}}(\varphi)$-EXPTIME in the size of the specification, and

  2. (2)

in $d_{\mathit{sys}}(\varphi)$-EXPTIME in the size of the system

######  Proof 6.1.

Let formula $\varphi$ and system $\mathcal{G}$ be given. Define
$d_{\mathit{spec}}:=d_{\mathit{spec}}(\varphi)$ and
$d_{\mathit{sys}}:=d_{\mathit{sys}}(\varphi)$. Using the constructions in
Figure 4 and Figure 5 we observe that the size of $\mathcal{A}_{\varphi}$ is
at most $\mathit{Tower}_{c}(d_{\mathit{spec}},|\varphi|)$ and
$\mathit{Tower}_{c}(d_{\mathit{sys}},|\mathcal{G}|)$ for some $c$ that depends
only on $d_{\mathit{spec}}$ and $d_{\mathit{sys}}$. To argue this, we consider
all cases in Figure 6(c). For example, for a formula $\exists\pi.\llangle
A\rrangle\pi^{\prime}.\varphi$, the alternating automaton
$\mathcal{A}_{\llangle A\rrangle\pi^{\prime}.\varphi}$ needs to be translated
to a non-deterministic automaton in the construction in Figure 4, which incurs
a single exponential blowup. For a formula $\llangle A\rrangle\pi.\llangle
A^{\prime}\rrangle\pi^{\prime}.\varphi$, automaton $\mathcal{A}_{\llangle
A^{\prime}\rrangle\pi^{\prime}.\varphi}$ needs to be determinized, causing a
double exponential blowup. For a formula $\llangle
A\rrangle\pi.\exists\pi^{\prime}.\varphi$, the automaton
$\mathcal{A}_{\exists\pi^{\prime}.\varphi}$ is already nondeterministic, so we
can perform a determinization with a single exponential blowup. As we can
decide emptiness of alternating automata in polynomial time (for a fixed
number of colors) [KV98], the bounds follow. Note that
$d_{\mathit{spec}}(\varphi)$ and $d_{\mathit{sys}}(\varphi)$ only differ in
the cost associated with the innermost quantifier. The automaton construction
for this last quantifier is linear in the size of the system but exponential
(in case the innermost quantifier is simple) or double exponential (in case
the innermost quantifier is complex) in the size of the formula.

######  Remark 12.

As complex quantification requires a full determinization, simple
quantification between complex quantifiers may have no impact on the
complexity. For example, checking a formula of the form $\llangle
A\rrangle\pi.\exists\pi^{\prime}.\llangle
A^{\prime}\rrangle\pi^{\prime\prime}.\psi$ and a formula of the form $\llangle
A\rrangle\pi.\llangle A^{\prime}\rrangle\pi^{\prime}.\psi$ have, in general,
identical model checking complexity.

#### Complexity based on Quantifier Count

We obtain a simpler complexity characterization if we only consider the number
and type of each quantifier. We consider the complexity in the size of the
formula (in Proposition 13) and the size of the system (in Proposition 14).

######  Proposition 13.

Model checking of a linear HyperATL∗ formula with $k$ complex and $l$ simple
quantifiers is

  1. (1)

in $(2k+l)$-EXPTIME, and

  2. (2)

in $(2k+l-1)$-EXPSPACE if $l\geq 1$

when measured in the size of the specification.

######  Proof 6.2.

Let $\varphi$ be any formula $k$ complex and $l$ simple quantifiers and
$\mathcal{G}$ the game structure. Point (1) follows directly from Theorem 11,
as $2k+l\geq d_{\mathit{spec}}(\varphi)$.

For point (2) let
$\varphi=\mathbb{Q}_{1}\;\pi_{1}.\cdots\mathbb{Q}_{k+l}\;\pi_{k+l}.\varphi$
where $\psi$ is quantifier-free. Let $i$ be the smallest index such that
$\mathbb{Q}_{i}$ is simple (which exists as $l\geq 1$). In case $i=1$ (i.e.,
the outermost quantifier is simple) we may assume w.l.o.g that
$\mathbb{Q}_{1}=\exists$ (as otherwise we simply check the negated formula).
So $\mathcal{A}_{\varphi}$ is a non-deterministic automaton and the
$(2k+l-1)$-EXPSPACE bound follows, as we can check the emptiness of non-
deterministic automata in NLOGSPACE [VW94]. If $i>1$ it is easy to see that
$2k+l-1\geq d_{\mathit{spec}}(\varphi)$, so we get a bound of
$(2k+l-1)$-EXPTIME using Theorem 11 and thereby also the desired
$(2k+l-1)$-EXPSPACE bound.

######  Proposition 14.

Model checking of a linear HyperATL∗ formula with $k$ complex and $l$ simple
quantifiers is

  1. (1)

in $(2k+l-2)$-EXPSPACE, and

  2. (2)

in $(2k+l-2)$-EXPTIME if $k\geq 1$, and

  3. (3)

in $(2k+l-3)$-EXPSPACE if $k\geq 1$ and the outermost quantifier is simple (so
$l\geq 1$)

when measured in the size of the system.

######  Proof 6.3.

Let $\varphi$ be any formula $k$ complex and $l$ simple quantifiers and
$\mathcal{G}$ the game structure. We begin with point (2). It is easy to see
that if $k\geq 1$, then $2k+l-2\geq d_{\mathit{sys}}(\varphi)$, so (2) follows
from Theorem 11.

For point (3) we may assume that the outer quantifier is existential
(otherwise we check the negated formula). We observe that if $k\geq 1$, the
size of $\mathcal{A}_{\varphi}$ is at most
$\mathit{Tower}_{c}(2k+l-2,|\mathcal{G}|)$ and $\mathcal{A}_{\varphi}$ is non-
deterministic, so emptiness can be checked in NLOGSPACE, giving the desired
$(2k+l-3)$-EXPSPACE bound.

It remains to show point (1). If $k\geq 1$, we get the even better bound of
$(2k+l-2)$-EXPTIME from point (2). In case $k=0$ (so all quantifiers are
simple) we again assume that the outermost quantifier is existential. It is
easy to see that the size of $\mathcal{A}_{\varphi}$ is at most
$\mathit{Tower}_{c}(2k+l-1,|\mathcal{G}|)$ and non-deterministic so the bound
follows from the NLOGSPACE emptiness check. Note that the case where $k=0$
corresponds directly to HyperLTL model checking.

##  7\. Lower Bounds for Model Checking

In this section, we establish lower bounds on the HyperATL∗ model checking.
Our lower bounds show that strategic quantification in the context of
hyperproperties results in a logic that is strictly harder (w.r.t. model
checking) than both a hyperlogic without strategic quantification (such as
HyperLTL) and a non-hyper logic with strategic quantification (such as ATL∗).

######  Theorem 15.

Model checking of a linear HyperATL∗ formula with $k$ complex and $l$ simple
quantifiers is $(2k+l-1)$-EXPSPACE-hard in the size of the formula.

######  Theorem 16.

Model checking of a linear HyperATL∗ formula with $k$ complex and $l$ simple
quantifiers is $(2k+l-3)$-EXPSPACE-hard in the size of the system.

$k=0$$k=1$$k\geq 2$$2$-EXPTIME-completein $(2k+l)$-EXPTIME$(2k+l-1)$-EXPSPACE-
hard$(2k+l-1)$-EXPSPACE-complete$l=0$$l\geq 1$ (a) Complexity in the size of
the specification. $(2k+l)$-EXPTIME containment and $(2k+l-1)$-EXPSPACE-
hardness hold for the entire fragment (the blue, striped area).

PTIME-completein $(2k+l-2)$-EXPTIME$(2k+l-3)$-EXPSPACE-hard$(l-2)$-EXPSPACE-
complete(Outermost quantifier is simple) $(2k+l-3)$-EXPSPACE-
complete$k=0$$k=1$$k\geq 2$$l=0$$l\geq 1$ (b) Complexity in the size of the
system. $(2k+l-2)$-EXPTIME containment and $(2k+l-3)$-EXPSPACE-hardness hold
for the blue, striped area. $(2k+l-3)$-EXPSPACE-completeness only holds for
formulas where the outermost quantifier is simple (the red dotted area).

Figure 7. Upper and lower bounds on the complexity of model checking a linear
HyperATL∗ formulas with $k$ complex and $l$ simple quantifiers. The bounds are
given in the size of the specification (Figure 7(a)) and size of the system
(Figure 7(b)).

#### Complexity in Specification Size

If we consider the HyperATL∗ model checking complexity in terms of the
specification size, Proposition 13 together with Theorem 15 span the landscape
depicted in Figure 7(a). For all formulas, we get an upper bound of
$(2k+l)$-EXPTIME and a lower bound of $(2k+l-1)$-EXPSPACE-hardness. In two
cases we can improve the upper or lower bounds further and get tightness. If
$k=1$ and $l=0$ we get a better $2$-EXPTIME lower bound from the ATL∗ model
checking [AHK02] and thus $2$-EXPTIME-completeness. In case $l\geq 1$, we get
a matching $(2k+l-1)$-EXPSPACE upper bound and thus $(2k+l-1)$-EXPSPACE-
completeness (note that this subsumes the HyperLTL bounds in case $k=0$).

#### Complexity in System Size

If we consider the complexity in the size of the system, Proposition 14
together with Theorem 16 span the landscape depicted in Figure 7(b). We get a
general lower bound of $(2k+l-3)$-EXPSPACE-hardness. In cases where $k\geq 1$,
we get an upper bound of $(2k+l-2)$-EXPTIME. In three cases we can tighten the
results: In case $k=0$ (where the formula is a HyperLTL formula), we get
$(l-2)$-EXPSPACE-completeness [Rab16]. In cases where $k=1$ and $l=0$, we get
a better lower bound from the ATL∗ model checking and thus PTIME-completeness
[AHK02]. And lastly, in case where $l\geq 1$ and the outermost quantifier is
simple, we get an improved upper bound resulting in $(2k+l-3)$-EXPSPACE-
completeness.

###  7.1. Proof Preliminaries

The remainder of this section is devoted to a proof of Theorem 15 and Theorem
16. Readers less interested in a formal (and rather lengthy) proof can skip to
Section 8.

Our proof encodes the acceptance of space-bounded Turing machines (TM). It
builds on ideas used for the HyperLTL lower bounds shown by Rabe [Rab16]
(adopting earlier ideas from Stockmeyer [Sto74]) but uses a novel construction
to achieve a doubly exponential increase using complex quantification. The
main idea of our construction is to design a HyperATL∗ formula that requires a