MnLargeSymbols’164 MnLargeSymbols’171 ifaamas [AAMAS ’24]Proc. of the 23rd
International Conference on Autonomous Agents and Multiagent Systems (AAMAS
2024)May 6 – 10, 2024 Auckland, New ZealandN. Alechina, V. Dignum, M. Dastani,
J.S. Sichman (eds.) 2024 2024 88 0000-0001-6234-5651 CISPA Helmholtz Center
for
Information Security Germany 0000-0002-4280-8441 CISPA Helmholtz Center for
Information Security Germany

# Hyper Strategy Logic

Raven Beutner  and  Bernd Finkbeiner

###### Abstract.

Strategy logic (SL) is a powerful temporal logic that enables strategic
reasoning in multi-agent systems. SL supports explicit (first-order)
quantification over strategies and provides a logical framework to express
many important properties such as Nash equilibria, dominant strategies, etc.
While in SL the same strategy can be used in multiple strategy profiles, each
such profile is evaluated w.r.t. a path-property, i.e., a property that
considers the _single_ path resulting from a particular strategic interaction.
In this paper, we present Hyper Strategy Logic (HyperSL), a strategy logic
where the outcome of multiple strategy profiles can be compared w.r.t. a
_hyperproperty_ , i.e., a property that relates _multiple_ paths. We show that
HyperSL can capture important properties that cannot be expressed in SL,
including non-interference, quantitative Nash equilibria, optimal adversarial
planning, and reasoning under imperfect information. On the algorithmic side,
we identify an expressive fragment of HyperSL with decidable model checking
and present a model-checking algorithm. We contribute a prototype
implementation of our algorithm and report on encouraging experimental
results.

###### Key words and phrases:

Strategy Logic, Hyperproperties, Model Checking, Imperfect Information, Nash
Equilibrium, Information-Flow Cotrol

##  1\. Introduction

Two important developments in the area of reactive systems concern the study
of strategic properties in multi-agent systems (MAS) and the study of
hyperproperties. _Strategic properties_ analyze the ability of agents to
achieve a goal against (or in cooperation) with other agents. Logics such as
alternating-time temporal logic (ATL∗) Alur et al. (2002) and strategy logic
(SL) Chatterjee et al. (2010); Mogavero et al. (2014b) reason about the
temporal interaction of such agents and allow for rigorous correctness
guarantees using techniques such as model-checking. _Hyperproperties_ Clarkson
and Schneider (2008) are properties that relate _multiple_ executions within a
system. Hyperproperties occur in many situations in computer science where
traditional path properties (that refer to _individual_ system execution) are
not sufficient. Typical examples include (1) _optimality_ , e.g., one path
reaching a goal faster than all other paths; (2) _information-flow policies_ ,
e.g., requiring that any two paths with identical low-security input should
produce the same low-security output McCullough (1988); and (3) _robustness_ ,
i.e., stating that similar inputs should lead to similar outputs Chaudhuri et
al. (2012).

Such hyperproperties are also of vital importance in MASs. For example, we
might ask if some agent has a strategy to achieve a goal without leaking
information (an information-flow property) or can achieve a goal faster than
some other agent (an optimality requirement). Yet existing logics for
strategic reasoning (such as variants of SL Mogavero et al. (2014b);
Chatterjee et al. (2010)) cannot express such hyper-requirements (we discuss
related approaches in Section 2). We illustrate this on the example of Nash
equilibria:

Assume we are given a MAS with agents
$\\{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}1},\ldots,{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}n}\\}$
and LTL properties
$\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}1},\ldots,\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}n}$
that describe the objectives of the agents. Agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
wants to make sure that
$\operatorname{\textsf{F}}\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
holds, i.e., formula
$\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
_eventually_ holds. We want to check whether the system admits a Nash
equilibrium, i.e., there exists a strategy for each agent such that no agent
has an incentive to deviate in order to fulfill her objective Nash Jr (1950).
In SL, we can express the existence of a Nash equilibrium as follows:

$\displaystyle\exists x_{1},\ldots,x_{n}\mathpunct{.}\forall
y\mathpunct{.}\bigwedge_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}=1}^{n}$
$\displaystyle\Big{(}(\operatorname{\textsf{F}}\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})(\@vec{x}[{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mapsto
y])\rightarrow(\operatorname{\textsf{F}}\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})(\@vec{x})\Big{)}$

where we abbreviate the strategy profiles $\@vec{x}=(x_{1},\ldots,x_{n})$ and
$\@vec{x}[{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mapsto
y]=(x_{1},\ldots,x_{i-1},y,x_{i+1},\ldots,x_{n})$. In the variant SL we
consider here (similar to the SL by Chatterjee et al. Chatterjee et al.
(2010)), atomic formulas have the form $\psi({\@vec{x}})$ where $\psi$ is an
LTL formula, and ${\@vec{x}}$ is a strategy profile that assigns a strategy to
each agent. Formula $\psi(\@vec{x})$ holds if the unique path that results
from the interaction of the strategies in $\@vec{x}$ satisfies $\psi$. The
above formula thus states that if some agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
can achieve $\operatorname{\textsf{F}}\psi_{i}$ by playing some deviating
strategy $y$ instead of $x_{i}$, i.e., the unique play that results from
strategy profile
$\@vec{x}[{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mapsto
y]$ satisfies $\operatorname{\textsf{F}}\psi_{i}$, then
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
could stick with strategy $x_{i}$, i.e., $\operatorname{\textsf{F}}\psi_{i}$
also holds under strategy profile $\@vec{x}$.

In the formula, we effectively compare two plays under strategy profiles
$\@vec{x}$ and
$\@vec{x}[{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mapsto
y]$. However, SL limits the comparison between multiple interactions to a
boolean combination of LTL properties on their outcomes (paths). In game-
theoretic terms, the above formula assumes that the reward for each agent is
binary; the reward of agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
is maximal if
$\operatorname{\textsf{F}}\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
holds and minimal if it does not. This fails to capture quantitative reward,
for example, in a setting where agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
receives a higher reward (and thus deviates) by fulfilling
$\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
_sooner_. To express the existence of such a quantitative equilibrium, a
boolean formula over individual temporal properties on strategy profiles
$\@vec{x}$ and
$\@vec{x}[{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mapsto
y]$ is not sufficient. We need a more powerful mechanism that can compare the
temporal behavior of _multiple_ paths: a _hyperproperty_.

##### HyperSL

In this paper, we propose HyperSL – a new temporal logic that combines first-
order strategic reasoning (as in SL) with the ability to compare _multiple_
paths w.r.t. a hyperproperty. Syntactically, we use path variables to refer to
multiple paths at the same time (similar to existing hyperlogics such as
HyperCTL∗ Clarkson et al. (2014) and HyperATL∗ Beutner and Finkbeiner (2021,
2023b)). In HyperSL, atomic formulas have the form
$\psi[\pi_{1}:{\@vec{x}}_{1},\ldots,\pi_{m}:{\@vec{x}}_{m}]$ where
$\pi_{1},\ldots,\pi_{m}$ are path variables,
${\@vec{x}}_{1},\ldots,{\@vec{x}}_{m}$ are strategy profiles (assigning a
strategy to each agent), and $\psi$ is an LTL formula where atomic
propositions are indexed by path variables from $\pi_{1},\ldots,\pi_{m}$. The
formula states that the plays resulting from strategy profiles
${\@vec{x}}_{1},\ldots,{\@vec{x}}_{m}$, when bound to
$\pi_{1},\ldots,\pi_{m}$, (together) satisfy the hyperproperty expressed by
$\psi$.

Coming back to the Nash equilibrium example from before, we can use HyperSL to
express the existence of a Nash equilibrium in a quantitative reward setting
as follows:

$\displaystyle\exists x_{1},\ldots,x_{n}\mathpunct{.}\forall
y\mathpunct{.}\bigwedge_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}=1}^{n}$
$\displaystyle\Big{(}\big{(}\neg{\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}}_{\pi_{1}}\operatorname{\textsf{W}}{\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}}_{\pi_{2}}\big{)}\left[\begin{aligned}
\pi_{1}&:{\@vec{x}}[{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mapsto
y]\\\\[-2.84526pt] \pi_{2}&:{\@vec{x}}\end{aligned}\right]\Big{)}$

Here, we write
${\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}}_{\pi_{1}}$
(resp.
${\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}}_{\pi_{2}}$)
to state that
$\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
holds on path $\pi_{1}$ (resp. $\pi_{2}$). In the formula, we again quantify
over a deviating strategy $y$, but can compare the two paths resulting from
strategy profiles
${\@vec{x}}[{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mapsto
y]$ and ${\@vec{x}}$ within the _same_ temporal formula. This formula states
that path $\pi_{1}$ (constructed using strategy profile
${\@vec{x}}[{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mapsto
y]$) does not satisfy
$\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
strictly before
$\psi_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
holds on path $\pi_{2}$ (constructed using strategy profile
${\@vec{x}}$).111We make use of LTL’s weak until operator
$\operatorname{\textsf{W}}$. Formula
$\psi_{1}\operatorname{\textsf{W}}\psi_{2}$ holds if $\psi_{1}$ holds until
$\psi_{2}$ holds eventually _or_ $\psi_{1}$ holds at all times.  If the above
formula holds, ${\@vec{x}}$ thus constitutes a strategy profile such that no
agent could achieve its goal strictly sooner (if at all).

Note that we can express any Nash equilibrium as long as “agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
(strictly) prefers the outcome on path $\pi_{1}$ over that on path $\pi_{2}$”
is expressible using an LTL formula over $\pi_{1},\pi_{2}$. Likewise, HyperSL
can, e.g., express that some strategy (1) reaches a goal without leaking
information, (2) is at least as fast as any other strategy, or (3) is robust
w.r.t. the behavior of other agents.

##### Expressiveness of HyperSL

After we introduce HyperSL (in Section 4), we study its relation to existing
logics (in Section 5). We show that HyperSL subsumes many non-hyper strategy
logics as well as hyperlogics such as HyperCTL∗ Clarkson et al. (2014),
HyperATL∗ Beutner and Finkbeiner (2021, 2023b), and HyperATL${}^{*}_{S}$
Beutner and Finkbeiner (2024) (see Section 2). Moreover, HyperSL also admits
reasoning under imperfect information despite having a semantics defined under
complete information. The key observation here is that “acting under imperfect
information” _is a hyperproperty_ : a strategy acts under imperfect
information if, on any _pair_ of paths with the same observation, the strategy
chooses the same action. Formally, we show that HyperSL subsumes SLii Berthon
et al. (2017b, 2021), a strategy logic centered around imperfect information.

##### Model Checking

HyperSL’s ability to compare multiple strategic interactions renders model-
checking (MC) undecidable. In Section 6, we identify a fragment of our logic –
called HyperSL[SPE] – for which MC is possible. Intuitively, in HyperSL[SPE],
the quantifier prefix should be such that we can group it into individual
“blocks” where the strategy variables from each block are used on independent
path variables. HyperSL[SPE] subsumes SL[1G] (the single-goal fragment of SL)
Mogavero et al. (2013), HyperLTL Clarkson et al. (2014), HyperATL∗ Beutner and
Finkbeiner (2021, 2023b), and HyperATL${}^{*}_{S}$ Beutner and Finkbeiner
(2024), but also captures properties that cannot be expressed in existing
logics. We argue that HyperSL[SPE] is the largest fragment with a decidable
model-checking problem that is defined purely in terms of the quantification
structure.

##### Implementation and Experiments

We implement our MC algorithm for HyperSL[SPE] in the HyMASMC tool Beutner and
Finkbeiner (2024) and experiment with various MAS models (in Section 7). Our
experiments show that HyMASMC performs well on many _non_ -hyper strategy
logic specifications and can verify complex hyperproperties that cannot be
expressed in any existing logic.

##  2\. Related Work

SL has been extended along multiple dimensions, including agent-unbinding
Laroussinie and Markey (2015), reasoning about probabilities Aminof et al.
(2019), epistemic properties Belardinelli et al. (2021); Maubert and Murano
(2018); Belardinelli et al. (2017), and quantitative properties Bouyer et al.
(2019). We refer to Mogavero et al. (2014b); Pauly and Parikh (2003) for a
more in-depth discussion. The common thread in all the previous extensions is
a focus on the temporal behavior on _individual_ paths. HyperSL generalizes SL
and is the first to compare _multiple_ paths. Even quantitative extensions
like SL[$\mathcal{F}$] Bouyer et al. (2019) evaluate an
LTL[$\mathcal{F}$]-formula on a _per-path_ basis. In contrast, HyperSL can
express complex relationships _between_ paths.

Studying logics that can express strategic properties under _imperfect
information_ has attracted much attention and led to various extensions of
ATL∗ Dima and Tiplea (2011); Bulling and Jamroga (2014); Laroussinie et al.
(2015); Belardinelli et al. (2017); Berthon et al. (2017a) and SL Berthon et
al. (2017b); Knight and Maubert (2019). Berthon et al. Berthon et al. (2017b)
showed that their logic, SLii, subsumes most existing approaches. We show that
HyperSL can also reason about imperfect information (and subsumes SLii)
despite having a semantics that is defined under full information.

Logics for expressing hyperproperties in non-agent-based systems (e.g.,
labeled transition systems) have been obtained by extending existing temporal
or first-order logics with explicit path quantification over path/trace
variables or an equal-level predicate Clarkson et al. (2014); Finkbeiner and
Zimmermann (2017); Gutsfeld et al. (2020); Coenen et al. (2019); Beutner and
Finkbeiner (2022). As strategic reasoning is significantly more powerful than
pure path quantification, HyperSL subsumes HyperCTL∗ (when interpreting
transition systems as single-agent MASs). HyperATL∗ Beutner and Finkbeiner
(2021, 2023b) and HyperATL${}^{*}_{S}$ Beutner and Finkbeiner (2024) extend
alternating-time temporal logic (ATL∗) Alur et al. (2002) with path variables
and strategy-sharing constraints, leading to a strategic hyperlogic that can
express important security properties such as non-deducibility of strategies
Wittbold and Johnson (1990) and simulation security Sabelfeld (2003). Similar
to ATL∗, the strategic reasoning in HyperATL∗ and HyperATL${}^{*}_{S}$ is
limited to _implicit_ reasoning about the strategic ability of coalitions of
agents and cannot explicitly reason about strategies as, e.g., needed to
express the existence of a Nash equilibrium.

Our model-checking algorithm for HyperSL[SPE] is based on an iterative
elimination of path (variables) in an automaton, similar to existing
algorithms for HyperCTL∗ Finkbeiner et al. (2015) and HyperATL∗ Beutner and
Finkbeiner (2023b, 2024). Compared to HyperATL∗, we need to eliminate paths by
simulating an _arbitrary_ prefix of strategy quantifiers, leading to a more
involved construction and more complex correctness proof.

##  3\. Preliminaries

We let $\mathit{AP}$ be a fixed finite set of atomic propositions and fix a
fixed finite set of agents
$\mathit{{Agts}}=\\{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}1},\ldots,{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}n}\\}$.
Given a set $X$, we write $X^{+}$ (resp. $X^{\omega}$) for the set of non-
empty finite (resp. infinite) sequences over $X$. For $u\in X^{\omega}$ and
$j\in Nature$, we write $x(j)$ for the $i$th element, $u[0,j]$ for the finite
prefix up to position $j$ (of length $j+1$), and $u[j,\infty]$ for the
infinite suffix starting at position $j$.

##### Concurrent Game Structures

As the underlying model of MASs, we use concurrent game structures (CGS) Alur
et al. (2002). A CGS is a tuple $\mathcal{G}=(S,s_{0},\mathbb{A},\kappa,L)$
where $S$ is a finite set of states, $s_{0}\in S$ is an initial state,
$\mathbb{A}$ is a finite set of actions,
$\kappa:S\times(\mathit{{Agts}}\to\mathbb{A})\to S$ is a transition function,
and $L:S\to 2^{\mathit{AP}}$ is a labeling function. The transition function
takes a state $s$ and an _action profile_
$\@vec{a}:\mathit{{Agts}}\to\mathbb{A}$ (mapping each agent an action) and
returns a unique successor state $\kappa(s,\@vec{a})$. We write
$\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}a_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
for the action profile where each agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
is assigned action
$a_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$.

A strategy in $\mathcal{G}$ is a function $f:S^{+}\to\mathbb{A}$, mapping
finite plays to actions. We denote the set of all strategies in $\mathcal{G}$
with $\mathit{Str}(\mathcal{G})$. A _strategy profile_
$\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
assigns each agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
a strategy
$f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{Str}(\mathcal{G})$.
Given strategy profile
$\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
and state $s\in S$, we can define the unique path resulting from the
interaction between the agents: We define
$\mathit{Play}_{\mathcal{G}}(s,\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})$
as the unique path $p\in S^{\omega}$ such that $p(0)=s$ and for every $j\in
Nature$ we have
$p(j+1)=\kappa\big{(}p(j),\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}(p[0,j])\big{)}$.
That is, in every step, we construct the action profile
$\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}(p[0,j])$
in which each agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
plays the action determined by
$f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
on the current prefix $p[0,j]$.

##### Alternating Automata

Our model-checking algorithm is based on alternating automata over infinite
words. These automata generalize nondeterministic automata by alternating
between nondeterministic and universal transitions Vardi (1995). For
transitions of the former kind, we can choose _some_ successor state; for
transitions of the latter type, we need to consider _all_ possible successor
states. Formally, an _alternating parity automaton (APA)_ over alphabet
$\Sigma$ is a tuple $\mathcal{A}=(Q,q_{0},\delta,c)$ where $Q$ is a finite set
of states, $q_{0}\in Q$ is an initial state, $c:Q\to Nature$ is a color
assignment, and $\delta:Q\times\Sigma\to\mathbb{B}^{+}(Q)$ is a transition
function that maps each state-letter pair to a positive boolean formula over
$Q$ (denoted with $\mathbb{B}^{+}(Q)$). For example, if
$\delta(q,l)=q_{1}\lor(q_{2}\land q_{3})$, we can – from state $q\in Q$ and
upon reading letter $l\in\Sigma$ – either move to state $q_{1}$ or move to
_both_ $q_{2}$ and $q_{3}$ (i.e., we spawn two copies of our automaton, one
starting in state $q_{2}$ and one in $q_{3}$). We write
$\mathcal{L}(\mathcal{A})\subseteq\Sigma^{\omega}$ for the set of all infinite
words for which we can construct a run tree that respects the transition
formulas such that the _minimal_ color that occurs infinitely many times (as
given by $c$) is _even_. For space reasons, we cannot give a formal semantics
of APA runs and instead refer the reader to Appendix A. No specific knowledge
about APAs is required to understand the high-level idea of our algorithm.

A special kind of APAs are _deterministic parity automata (DPA)_ in which
$\delta$ is a function $Q\times\Sigma\to Q$ assigning a unique successor state
to each state-letter pair. We can always determinize APAs:

######  Proposition 0 (Miyano and Hayashi (1984); Piterman (2007)).

For any APA $\mathcal{A}$ with $n$ states, we can effectively compute a DPA
$\mathcal{A}^{\prime}$ with at most $2^{2^{\mathcal{O}(n)}}$ states such that
$\mathcal{L}(\mathcal{A})=\mathcal{L}(\mathcal{A}^{\prime})$.

##  4\. Hyper Strategy Logic

Our new logic HyperSL is centered around the idea of combining strategic
reasoning (as possible in strategy logic Chatterjee et al. (2010); Mogavero et
al. (2014b)) with the ability to express hyperproperties (as possible in
logics such as HyperCTL∗ Clarkson et al. (2014)). To accomplish this, we
combine the ideas from both disciples. On the strategy-logic-side, we use
strategy variables to quantify over strategies. On the hyper-side, we use path
variables to compare multiple paths within a temporal formula.

Let $\mathcal{X}$ be a set of _strategy variables_ and $\mathcal{V}$ a set of
_path variables_. We typically use lowercase letters ($x,y,z,x_{1},\ldots$)
for strategy variables and variations of $\pi$
($\pi,\pi^{\prime},\pi_{1},\ldots$) for path variables. Path and state
formulas in HyperSL are generated by the following grammar:

$\displaystyle\psi$
$\displaystyle:=a_{\pi}\mid\varphi_{\pi}\mid\psi\land\psi\mid\neg\psi\mid\operatorname{\textsf{X}}\psi\mid\psi\operatorname{\textsf{U}}\psi$
$\displaystyle\varphi$ $\displaystyle:=\forall x.\varphi\mid\exists
x.\varphi\mid\psi\big{[}\pi_{1}:{\@vec{x}}_{1},\ldots,\pi_{m}:{\@vec{x}}_{m}\big{]}$

where $a\in\mathit{AP}$ is an atomic proposition,
$\pi,\pi_{1},\ldots,\pi_{m}\in\mathcal{V}$ are path variables,
$x\in\mathcal{X}$ is a strategy variable, and
${\@vec{x}}_{1},\ldots,{\@vec{x}}_{m}:\mathit{{Agts}}\to\mathcal{X}$ are
_strategy profiles_ that assign a strategy variable to each agent. We often
write $\psi[\pi_{k}:{\@vec{x}}_{k}]_{k=1}^{m}$ as a shorthand for
$\psi[\pi_{1}:{\@vec{x}}_{1},\ldots,\pi_{m}:{\@vec{x}}_{m}]$. We use
$\mathds{Q}$ as a placeholder for either $\forall$ or $\exists$. We use the
standard Boolean connectives $\lor,\to,\leftrightarrow$, and constants
$\top,\bot$, as well as the derived LTL operators _eventually_
$\operatorname{\textsf{F}}\psi:=\top\operatorname{\textsf{U}}\psi$ and
_globally_
$\operatorname{\textsf{G}}\psi:=\neg\operatorname{\textsf{F}}\neg\psi$. For
each formula $\psi[\pi_{k}:{\@vec{x}}_{k}]_{k=1}^{m}$, we assume that all path
variables that are free in $\psi$ belong to $\\{\pi_{1},\ldots,\pi_{m}\\}$,
i.e., all used path variables are bound to some strategy profile. We further
assume that all nested state formulas are closed.

Note that our syntax does not support boolean combinations of state formulas
as is usual in SL Mogavero et al. (2014b). As we can evaluate a path formula
on multiple paths, we can move boolean combinations within the path formulas.

######  Example 0.

Consider the SL formula $\exists x\mathpunct{.}(\exists
y.(\operatorname{\textsf{F}}a)(x,y))\land(\forall
z.\allowbreak(\operatorname{\textsf{G}}b)(z,x))$, which can be expressed in
HyperSL as follows: $\exists x\mathpunct{.}\exists y\mathpunct{.}\forall
y\mathpunct{.}\allowbreak(\operatorname{\textsf{F}}a_{\pi_{1}}\land\operatorname{\textsf{G}}b_{\pi_{2}})[\pi_{1}:(x,y),\pi_{2}:(z,x)]$.
$\triangle$

#### Semantics

We fix a game structure $\mathcal{G}=(S,s_{0},\mathbb{A},\kappa,L)$. A
_strategy assignment_ is a partial mapping
$\Delta:\mathcal{X}\rightharpoonup\mathit{Str}(\mathcal{G})$. We write
$\\{\\}$ for the unique strategy assignment with an empty domain. In HyperSL,
a path formula $\psi$ refers to propositions on multiple path variables. We
evaluate it in the context of a _path assignment_
$\Pi:\mathcal{V}\rightharpoonup S^{\omega}$ mapping path variables to paths
(similar to the semantics of HyperCTL∗ Clarkson et al. (2014)). Given $j\in
Nature$, we define $\Pi[j,\infty]$ as the shifted assignment defined by
$\Pi[j,\infty](\pi):=\Pi(\pi)[j,\infty]$. For a path formula $\psi$, we then
define the semantics in the context of path assignment $\Pi$:

$\displaystyle\Pi$ $\displaystyle\models_{\mathcal{G}}a_{\pi}$ iff
$\displaystyle a\in L\big{(}\Pi(\pi)(0)\big{)}$ $\displaystyle\Pi$
$\displaystyle\models_{\mathcal{G}}\varphi_{\pi}$ iff
$\displaystyle\Pi(\pi)(0),\\{\\}\models_{\mathcal{G}}\varphi$
$\displaystyle\Pi$ $\displaystyle\models_{\mathcal{G}}\psi_{1}\land\psi_{2}$
iff $\displaystyle\Pi\models_{\mathcal{G}}\psi_{1}\text{ and
}\Pi\models_{\mathcal{G}}\psi_{2}$ $\displaystyle\Pi$
$\displaystyle\models_{\mathcal{G}}\neg\psi$ iff
$\displaystyle\Pi\not\models_{\mathcal{G}}\psi$ $\displaystyle\Pi$
$\displaystyle\models_{\mathcal{G}}\operatorname{\textsf{X}}\psi$ iff
$\displaystyle\Pi[1,\infty]\models_{\mathcal{G}}\psi$ $\displaystyle\Pi$
$\displaystyle\models_{\mathcal{G}}\psi_{1}\operatorname{\textsf{U}}\psi_{2}$
iff $\displaystyle\exists j\in
Nature\mathpunct{.}\Pi[j,\infty]\models_{\mathcal{G}}\psi_{2}\text{ and }$
$\displaystyle\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\forall 0\leq
k<j\mathpunct{.}\Pi[k,\infty]\models_{\mathcal{G}}\psi_{1}$

The semantics for path formulas synchronously steps through all paths in $\Pi$
and evaluate $a_{\pi}$ on the path bound to $\pi$. State formulas are
evaluated in a state $s\in S$ and strategy assignment $\Delta$ as follows:

$\displaystyle s,\Delta\models_{\mathcal{G}}\forall x\mathpunct{.}\varphi$ iff
$\displaystyle\forall
f\in\mathit{Str}(\mathcal{G})\mathpunct{.}s,\Delta[x\mapsto
f]\models_{\mathcal{G}}\varphi$ $\displaystyle
s,\Delta\models_{\mathcal{G}}\exists x\mathpunct{.}\varphi$ iff
$\displaystyle\exists
f\in\mathit{Str}(\mathcal{G})\mathpunct{.}s,\Delta[x\mapsto
f]\models_{\mathcal{G}}\varphi$ $\displaystyle
s,\Delta\models_{\mathcal{G}}\psi\big{[}\pi_{k}:{\@vec{x}}_{k}\big{]}_{k=1}^{m}$
iff
$\displaystyle\Big{[}\pi_{k}\\!\mapsto\\!\mathit{Play}_{\mathcal{G}}\Big{(}s,\\!\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}\\!\\!\Delta({\@vec{x}}_{k}({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}))\Big{)}\Big{]}_{k=1}^{m}\models_{\mathcal{G}}\psi$

To resolve a formula $\psi\big{[}\pi_{k}:{\@vec{x}}_{k}\big{]}_{k=1}^{m}$, we
construct $m$ paths (bound to $\pi_{1},\ldots,\pi_{m}$), and evaluate $\psi$
in the resulting path assignment. The $k$th path (bound to $\pi_{k}$) is the
play where each agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
plays strategy
$\Delta({\@vec{x}}_{k}({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}))$,
i.e., the strategy currently bound to the strategy variable
${\@vec{x}}_{k}({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})$.
We write $\mathcal{G}\models\varphi$ if
$s_{0},\\{\\}\models_{\mathcal{G}}\varphi$, i.e., the initial state satisfies
state formula $\varphi$.

##  5\. Expressiveness of HyperSL

The ability to compare multiple paths within a temporal formula makes HyperSL
a powerful formalism that subsumes many existing logics. We only briefly
mention some connections to existing logics. More details can be found in
Appendix B.

###  5.1. SL and HyperSL

HyperSL naturally subsumes many (non-hyper) strategy logics Mogavero et al.
(2014b); Chatterjee et al. (2010), which evaluate temporal properties on
_individual_ paths. We consider SL formulas defined by the following grammar:

$\displaystyle{\psi}$
$\displaystyle:=a\mid\varphi\mid\neg{\psi}\mid{\psi}\land{\psi}\mid\operatorname{\textsf{X}}{\psi}\mid{\psi}\operatorname{\textsf{U}}{\psi}$
$\displaystyle{\varphi}$
$\displaystyle:={\psi}\mid{\varphi}\land{\varphi}\mid{\varphi}\lor{\varphi}\mid\forall
x\mathpunct{.}{\varphi}\mid\exists
x\mathpunct{.}{\varphi}\mid({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},x){\varphi}$

where $a\in\mathit{AP}$, $x\in\mathcal{X}$, and
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}$.
We assume that nested state formulas are closed. In this SL, we can quantify
over strategies and _bind_ a strategy $x$ to agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
using
$({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},x)$;
see Section B.1 for the full semantics. We can show the following:

lemmareSlToHyper For any SL formula $\varphi$ there exists a HyperSL formula
$\varphi^{\prime}$ such that for any CGS $\mathcal{G}$,
$\mathcal{G}\models_{\text{SL}}\varphi$ iff
$\mathcal{G}\models\varphi^{\prime}$.

###### Proof Sketch.

We use a unique path variable $\dot{\pi}$. During translation, we track the
current strategy (variable) for each agent and construct $\dot{\pi}$ using the
resulting strategy profile. ∎

######  Example 0.

Consider the formula $\exists x\mathpunct{.}\forall
y\mathpunct{.}({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}1},x)({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}2},y)({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}3},y)\operatorname{\textsf{G}}\operatorname{\textsf{F}}a$.
We can express this formula in HyperSL as $\exists x\mathpunct{.}\exists
y\mathpunct{.}\big{(}\operatorname{\textsf{G}}\operatorname{\textsf{F}}a_{\dot{\pi}}\big{)}[\dot{\pi}:(x,y,y)]$
where $(x,y,y)$ denotes the strategy profile mapping agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}1}$
to $x$, and agents
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}2}$
and
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}3}$
to $y$.  $\triangle$

###  5.2. HyperATL∗ and HyperSL

Compared to SL, ATL∗ Alur et al. (2002) offers a weaker (implicit) form of
strategic reasoning. The ATL∗ formula $\llangle A\rrangle\psi$ expresses that
the agents in $A\subseteq\mathit{{Agts}}$ have a joint strategy to ensure path
formula $\psi$ Alur et al. (2002). HyperATL∗ Beutner and Finkbeiner (2021,
2023b) is an extension of ATL∗ that can express hyperproperties, generated by
the following grammar:

$\displaystyle{\psi}$
$\displaystyle:=a_{\pi}\mid\neg{\psi}\mid{\psi}\land{\psi}\mid\operatorname{\textsf{X}}{\psi}\mid{\psi}\operatorname{\textsf{U}}{\psi}$
$\displaystyle{\varphi}$ $\displaystyle:=\llangle
A\rrangle\pi\mathpunct{.}{\varphi}\mid\llbracket
A\rrbracket\pi\mathpunct{.}{\varphi}\mid{\psi}$

where $a\in\mathit{AP}$, $\pi\in\mathcal{V}$, and $A\subseteq\mathit{{Agts}}$.
Formula $\llangle A\rrangle\pi\mathpunct{.}{\varphi}$ states that the agents
in $A$ have a strategy such that any path under that strategy, when bound to
path variable $\pi$, satisfies the remaining formula ${\varphi}$. Likewise,
$\llbracket A\rrbracket\pi\mathpunct{.}{\varphi}$ states that, no matter what
strategy the agents in $A$ play, some compatible path, when bound to $\pi$,
satisfies ${\varphi}$. See Section B.2 for the full HyperATL∗ semantics. We
can show the following:

lemmahyperatlsToHyper For any HyperATL∗ formula $\varphi$ there exists a
HyperSL formula $\varphi^{\prime}$ such that for any CGS $\mathcal{G}$,
$\mathcal{G}\models_{\text{HyperATL${}^{*}${}}}\varphi$ iff
$\mathcal{G}\models\varphi^{\prime}$.

###### Proof Sketch.

Similar to the translation of ATL∗ to SL Mogavero et al. (2014b); Chatterjee
et al. (2010), we translate each HyperATL∗ quantifier $\llangle A\rrangle\pi$
(resp. $\llbracket A\rrbracket\pi$) using existential (resp. universal)
quantification over fresh strategies for all agents in $A$, followed by
universal (resp. existential) quantification over strategies for agents in
$\mathit{{Agts}}\setminus A$ and use these strategies to construct path $\pi$.
∎

######  Example 0.

Consider the HyperATL∗ formula
$\llangle\\{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}1},{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}2}\\}\rrangle\pi_{1}\mathpunct{.}\allowbreak\llangle\\{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}3}\\}\rrangle\allowbreak\pi_{2}\mathpunct{.}(a_{\pi_{1}}\operatorname{\textsf{U}}b_{\pi_{2}})$.
We can express this in HyperSL as $\exists
x_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}1},x_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}2}}\mathpunct{.}\forall
x_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}3}}\mathpunct{.}\exists
y_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}3}}\mathpunct{.}\allowbreak\forall
y_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}1}},y_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}2}}\mathpunct{.}\allowbreak(a_{\pi_{1}}\operatorname{\textsf{U}}b_{\pi_{2}})\big{[}\pi_{1}:(x_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}1}},x_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}2}},x_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}3}}),\pi_{2}:(y_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}1}},y_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}2}},y_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}3}})\big{]}$.
$\triangle$

By Section 5.2, HyperSL thus captures the various security hyperproperties
(such as non-deducibility of strategies Wittbold and Johnson (1990) and
simulation security Sabelfeld (2003)) that can be expressed in HyperATL∗
Beutner and Finkbeiner (2021). We can extend Section 5.2 further to also
capture the strategy sharing constraints found in HyperATL${}^{*}_{S}$ Beutner
and Finkbeiner (2024).

lemmahyperatlssToHyper For any HyperATL${}^{*}_{S}$ formula $\varphi$ there
exists a HyperSL formula $\varphi^{\prime}$ such that for any CGS
$\mathcal{G}$, $\mathcal{G}\models_{\text{HyperATL${}^{*}_{S}${}}}\varphi$ iff
$\mathcal{G}\models\varphi^{\prime}$.

Moreover, HyperSL can express properties that go well beyond the strict
$\exists\forall$ and $\forall\exists$ quantifier alternation found in
HyperATL∗ and HyperATL${}^{*}_{S}$ (as, e.g., needed for Nash equilibria).

###  5.3. Imperfect Information and HyperSL

In recent years, much effort has been made to study strategic behavior under
_imperfect information_ Belardinelli et al. (2019); Berthon et al. (2017b);
Knight and Maubert (2019); Belardinelli et al. (2017); Berthon et al. (2017a);
Dima and Tiplea (2011). In such a setting, an agent acts strategically (i.e.,
decides on an action based on its past experience) but only observes parts of
the overall system. Perhaps surprisingly, HyperSL is expressive enough to
allow reasoning under imperfect information despite having a semantics with
complete information (cf. Section 4). Concretely, we consider strategy logic
under imperfect information (SLii), an extension of SL with imperfect
information Berthon et al. (2017b, 2021) defined as follows:

$\displaystyle{\psi}$
$\displaystyle:=a\mid{\varphi}\mid\neg{\psi}\mid{\psi}\land{\psi}\mid\operatorname{\textsf{X}}{\psi}\mid{\psi}\operatorname{\textsf{U}}{\psi}$
$\displaystyle{\varphi}$
$\displaystyle:={\psi}\mid{\varphi}\land{\varphi}\mid{\varphi}\lor{\varphi}\mid\forall
x^{o}\mathpunct{.}{\varphi}\mid\exists
x^{o}\mathpunct{.}{\varphi}\mid({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},x){\varphi}$

where $a\in\mathit{AP}$, $x\in\mathcal{X}$,
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}$,
and $o\in\mathit{Obs}$ is an _observation_ that gets attached to each
strategy. SLii is evaluated on _CGSs under partial observation_ , which are
pairs $(\mathcal{G},\\{\sim_{o}\\}_{o\in\mathit{Obs}})$ consisting of a CGS
$\mathcal{G}=(S,s_{0},\mathbb{A},\kappa,L)$ and an observation relation
$\sim_{o}\subseteq S\times S$ for each observation $o\in\mathit{Obs}$. If
$s\sim_{o}s^{\prime}$, then $s$ and $s^{\prime}$ appear indistinguishable for
a strategy with observation $o$. See Section B.3 for the full semantics.

We can effectively encode each MC instance of SLii into an equisatisfiable
HyperSL instance (Note that the MAS models of SLii and HyperSL are different,
so we cannot translate the formula directly but translate both the formula and
the model).

theoremsliToHyper For any SLii MC instance
$\big{(}(\mathcal{G},\\{\sim_{o}\\}_{o\in\mathit{Obs}}),\varphi\big{)}$, we
can effectively compute a HyperSL MC instance
$\big{(}\mathcal{G}^{\prime},\varphi^{\prime}\big{)}$, such that
$(\mathcal{G},\\{\sim_{o}\\}_{o\in\mathit{Obs}})\models_{\text{SL}_{\text{ii}}}\varphi$
iff $\mathcal{G}^{\prime}\models\varphi^{\prime}$.

###### Proof Sketch.

The key observation is that a strategy acting under imperfect information _is_
a hyperproperty Bozzelli et al. (2015); Beutner et al. (2023): A strategy $f$
acts under observation $o\in\mathit{Obs}$ iff on any two finite paths under
$f$ the action chosen by $f$ is the same, provided the two paths are
indistinguishable w.r.t. $\sim_{o}$. We can extend the CGS $\mathcal{G}$ so
that the above is easily expressible in HyperSL. We can then restrict
quantification to strategies under an arbitrary observation and use a similar
translation to the one used in Section 5.1. ∎

As model checking of SLii is undecidable Berthon et al. (2017b), we get:

######  Corollary 0.

Model checking of HyperSL is undecidable.

##  6\. Model Checking of HyperSL

While HyperSL MC is undecidable in general (cf. Corollary 5), we can identify
fragments for which MC is possible. For this, we cannot follow the approach of
existing MC algorithms for (variants of) non-hyper SL, which use tree automata
to summarize strategies Chatterjee et al. (2010); Mogavero et al. (2014b). For
example, given an atomic state formula
$\psi[\pi_{k}:{\@vec{x}}_{k}]_{k=1}^{m}$, we cannot construct a tree automaton
that accepts all strategies that fulfill $\psi$. This automaton would need to
_compare_ (and thus traverse) multiple paths in a tree at the same time.
Instead – given the “hyper” origins of our logic – we approach the MC problem
by focusing on the interactions of its path variables and use _word_ automata
to summarize satisfying path assignments.

Throughout this section, we assume that all strategy variables are
$\alpha$-renamed such that no variable is quantified more than once.

###  6.1. HyperSL[SPE]

We call the fragment of HyperSL we study in this section HyperSL[SPE] – short
for HyperSL with Single Path Elimination.

######  Definition 0.

A HyperSL[SPE] formula has the form

$\displaystyle\varphi=\flat_{1}\ldots\flat_{m}\mathpunct{.}\psi\big{[}\pi_{k}:{\@vec{x}}_{k}\big{]}_{k=1}^{m},$

where $\flat_{1},\ldots,\flat_{m}$ are blocks of strategy quantifiers and for
each $1\leq k\leq m$ and
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}$,
strategy variable
${\@vec{x}}_{k}({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})$
is quantified in $\flat_{k}$. We refer to $m$ as the _block-rank_ of
$\varphi$.

Intuitively, the definition states that we can partition the quantifier prefix
into smaller blocks where the variables quantified in each block $\flat_{k}$
can be used to eliminate (construct) the (unique) path variable $\pi_{k}$. We
will exploit this restriction during model-checking: we can eliminate each
block of quantifiers incrementally: as all strategies quantified in block
$\flat_{k}$ are only needed for path $\pi_{k}$, we can “construct” $\pi_{k}$,
and afterward forget about the strategies we have used. Note that the
definition of HyperSL[SPE] only depends on the quantifier prefix and the path
each strategy variable is used on; it does not make any assumption on the
structure of $\psi$.

######  Example 0.

Consider the following (abstract) HyperSL formula, where $\psi$ is an
arbitrary LTL formula over $\pi_{1},\pi_{2}$.

$\displaystyle\underbrace{\exists
c\mathpunct{.}}_{\flat_{1}}\underbrace{\exists z\mathpunct{.}\forall
w\mathpunct{.}\exists v\mathpunct{.}}_{\flat_{2}}\psi\left[\begin{aligned}
\pi_{1}&:(c,c,c,c)\\\ \pi_{2}&:(w,z,v,v)\end{aligned}\right]$

This formula is a HyperSL[SPE] formula: The first block $\flat_{1}$ consists
of strategy variable $c$ and constructs $\pi_{1}$, and the second block
$\flat_{2}$ constructs $\pi_{2}$. The block-rank of this formula is $2$.
$\triangle$

###  6.2. Expressiveness Of HyperSL[SPE]

Before we outline our model-checking algorithm for HyperSL[SPE] formulas, we
point to some (fragments of) other logics that fall within HyperSL[SPE].

##### HyperATL∗ and HyperSL[SPE]

When translating HyperATL∗ (or HyperATL${}^{*}_{S}$) formulas into HyperSL
(cf. Sections 5.2 and 4), each quantifier $\llangle A\rrangle\pi$ (resp.
$\llbracket A\rrbracket\pi$) is replaced by a $\exists^{*}\forall^{*}$ (resp.
$\forall^{*}\exists^{*}$) block of strategy quantifiers that are used to
construct $\pi$ (and only $\pi$). The resulting formula is thus a HyperSL[SPE]
formula.

##### SL[1G] and HyperSL[SPE]

SL[1G] is a fragment of SL that allows a prefix of strategy quantifier and
agent bindings followed by a single path formula (with no nested agent
binding) Mogavero et al. (2014b, 2013, a); Cermák et al. (2015). When
translating SL[1G] into HyperSL, we obtain a formula of the form
$\mathds{Q}_{1}x_{1}\ldots\mathds{Q}_{m}x_{m}\mathpunct{.}\psi[\pi:{\@vec{x}}]$
(cf. Section 5.1), which is trivially HyperSL[SPE] as there is a single path
variable (with block-rank $1$).

##### Beyond HyperATL${}^{*}_{S}$ and SL[1G]

Additionally, HyperSL[SPE] captures interesting hyperproperties that could not
be captured in existing logics:

######  Example 0.

Assume a MAS with
$\mathit{{Agts}}=\\{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}r},{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}a},{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}\mathit{ndet}}\\}$
describing a planning task between a robot
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}r}$
that wants to reach a state where AP $\mathit{goal}\in\mathit{AP}$ holds, and
an adversary
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}a}$
that wants to prevent the robot from reaching the goal. In each step, agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}r}$
can select a direction to move in, and
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}a}$
can choose a direction it wants to push the robot to. Each combination of
actions of
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}r}$
and
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}a}$
results in a set of potential successor locations, and the nondeterminism
agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}\mathit{ndet}}$
decides which of those locations the robot actually moves to. We want to check
if agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}r}$
has a winning strategy that _can_ reach the goal against all possible
behaviors of agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}a}$,
i.e.,
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}r}$
needs to reach the goal under favorable non-deterministic outcomes. We can
express this (non-hyper) property in HyperSL[SPE] as

$\displaystyle\exists x\mathpunct{.}\forall y\mathpunct{.}\exists
z\mathpunct{.}\big{(}\operatorname{\textsf{F}}\mathit{goal}_{\pi}\big{)}\big{[}\pi:(x,y,z)\big{]},$

where we write $(x,y,z)$ for the strategy profile that assigns agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}r}$
to $x$, agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}a}$
to $y$, and agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}\mathit{ndet}}$
to $z$. In HyperSL[SPE], we can additionally state that
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}r}$
should reach the goal _as fast as possible_ , i.e., at least as fast as any
path in the MAS:

$\displaystyle\exists x\mathpunct{.}\forall y\mathpunct{.}\exists
z\mathpunct{.}\forall a\mathpunct{.}\forall b\mathpunct{.}\forall
c\mathpunct{.}(\neg\mathit{goal}_{\pi^{\prime}})\operatorname{\textsf{U}}\mathit{goal}_{\pi}\left[\begin{aligned}
&\pi:(x,y,z)\\\ &\pi^{\prime}:(a,b,c)\end{aligned}\right]$

Here, we quantify over any potential different path $\pi^{\prime}$ and state
that $\pi$ is at least as fast as $\pi^{\prime}$. Such requirements cannot be
expressed in SL (even in quantitative versions like SL[$\mathcal{F}$]), nor
can they be expressed in HyperATL∗ or HyperATL${}^{*}_{S}$.  $\triangle$

###  6.3. Summarizing Path Assignments

In the remainder of this section, we prove the following:

######  Theorem 9.

Model checking for HyperSL[SPE] is decidable.

We fix a CGS $\mathcal{G}=(S,s_{0},\mathbb{A},\kappa,L)$ and state $\dot{s}\in
S$, and let
$\varphi=\flat_{1}\ldots\flat_{m}\mathpunct{.}\psi\big{[}\pi_{k}:{\@vec{x}}_{k}\big{]}_{k=1}^{m}$
be a HyperSL[SPE] formula. We want to check if
$\dot{s},\\{\\}\models_{\mathcal{G}}\varphi$, i.e., $\varphi$ holds in state
$\dot{s}$.

##### Zipping Path Assignments

The main idea of our algorithm is to summarize path assignments that satisfy
subformulas of $\varphi$, similar to MC algorithms for HyperLTL, HyperCTL∗,
and HyperATL∗ Finkbeiner et al. (2015); Beutner and Finkbeiner (2023a, b,
2024). To enable automata-based reasoning about path assignments, i.e.,
mappings $\Pi:V\to S^{\omega}$ for some $V\subseteq\mathcal{V}$, we _zip_ such
an assignment into an infinite word. Concretely, given $\Pi:V\to S^{\omega}$
we define $\mathit{zip}(\Pi)\in(V\to S)^{\omega}$ as the infinite word of
functions where $\mathit{zip}(\Pi)(j)(\pi):=\Pi(\pi)(j)$ for every $j\in
Nature$, i.e., the function in the $j$th step maps each path variable $\pi\in
V$ to the $j$th state on the path bound to $\pi$.

##### Summary Automaton

Given a quantifier block $\flat=\mathds{Q}_{1}x_{1}\ldots\mathds{Q}_{n}x_{n}$
over strategy variables $x_{1},\ldots,x_{n}$, we define $\widetilde{\flat}$ as
the analogous block of quantification of strategies
$f_{x_{1}},\ldots,f_{x_{n}}$, i.e.,
$\widetilde{\flat}:=\mathds{Q}_{1}f_{x_{1}}\in\mathit{Str}(\mathcal{G})\ldots\mathds{Q}_{n}f_{x_{n}}\in\mathit{Str}(\mathcal{G})$.
At the core of our model-checking algorithm, we construct automata that accept
(zippings of) partial satisfying path assignments. Formally:

######  Definition 0.

For $1\leq k\leq m+1$, we say an automaton $\mathcal{A}$ over alphabet
$(\\{\pi_{1},\ldots,\pi_{k-1}\\}\to S)$ is a _$(\mathcal{G},\dot{s},k)$
-summary_ if for every path assignment $\Pi:\\{\pi_{1},\ldots,\pi_{k-1}\\}\to
S^{\omega}$ we have $\mathit{zip}(\Pi)\in\mathcal{L}(\mathcal{A})$ if and only
if

$\displaystyle\widetilde{\flat_{k}}\cdots\widetilde{\flat_{m}}\mathpunct{.}\Pi\Big{[}\pi_{j}\mapsto\mathit{Play}_{\mathcal{G}}(\dot{s},\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}f_{{\@vec{x}}_{j}({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})})\Big{]}_{j=k}^{m}\models_{\mathcal{G}}\psi.$

That is, a $(\mathcal{G},\dot{s},k)$-summary accepts (the zipping of) a path
assignment $\Pi$ over paths $\pi_{1},\ldots,\pi_{k-1}$ if – when simulating
the quantification over strategies needed to construct paths
$\pi_{k},\ldots,\pi_{m}$ and adding them to $\Pi$ – the body $\psi$ of the
formula is satisfied.

######  Example 0.

We illustrate the concept using the abstract formula from Example 7. A
$(\mathcal{G},\dot{s},3)$-summary is an automaton $\mathcal{A}_{3}$ over
alphabet $(\\{\pi_{1},\pi_{2}\\}\to S)$ such that for every
$\Pi:\\{\pi_{1},\pi_{2}\\}\to S^{\omega}$ we have
$\mathit{zip}(\Pi)\in\mathcal{L}(\mathcal{A}_{3})$ iff
$\Pi\models_{\mathcal{G}}\psi$. A $(\mathcal{G},\dot{s},2)$-summary is an
automaton $\mathcal{A}_{2}$ over alphabet $(\\{\pi_{1}\\}\to S)$ such that for
every $\Pi:\\{\pi_{1}\\}\to S^{\omega}$ we have
$\mathit{zip}(\Pi)\in\mathcal{L}(\mathcal{A}_{2})$ iff

$\displaystyle\exists f_{z}\mathpunct{.}\forall f_{w}\mathpunct{.}\exists
f_{v}\mathpunct{.}\Pi\big{[}\pi_{2}\mapsto\mathit{Play}_{\mathcal{G}}(\dot{s},(f_{w},f_{z},f_{v},f_{v}))\big{]}\models_{\mathcal{G}}\psi,$

i.e., we mimic the quantification of block $\flat_{2}$ to construct path
$\pi_{2}$ (using the quantified strategies
$f_{z},f_{w},f_{v}\in\mathit{Str}(\mathcal{G})$) and add this path to $\Pi$
(which already contains $\pi_{1}$). $\triangle$

###  6.4. Constructing $(\mathcal{G},\dot{s},k)$-Summaries

Algorithm 1 Simulation construction for block elimination.

⬇

@@$\calA_\mathit{det} = (Q, q_0, \delta, c)$ = toDPA($\calA$) //
(*\color{comment-color}Using \Cref{prop:toDPA} \label{line:toDPA}*)

@@$\calB$ = $(Q \times S, (q_0, \dot{s}), \delta’, c’\big)$ where

@@@@$c’(q, s) := c(q)$ (*\label{line:color}*)

@@@@$\begin{aligned}

\delta’\big( (q, s) , \bT\big) := \biglandlor^{\quant_1}_{a_{x_1} \in \moves
}\\!\\! \cdots \\!\\! \biglandlor^{\quant_n}_{a_{x_n} \in \moves}
\bigg(\delta\big(q, \bT[\pi \mapsto s] \big), \kappa\Big(s, \prod_{\agent{i}
\in \agents} a_{\bX(\agent{i})} \Big)\bigg)

\end{aligned}$(*\label{line:tran}*)

@@return $\calB$

We write
$\mathop{\vphantom{\sum}\mathchoice{\vbox{\hbox{\leavevmode\resizebox{9.00005pt}{}{$\mathrlap{\vee}\wedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{10.00012pt}{}{$\mathrlap{\vee}\wedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{7.00009pt}{}{$\mathrlap{\vee}\wedge$}}}}{\vbox{\hbox{\leavevmode\resizebox{5.00006pt}{}{$\mathrlap{\vee}\wedge$}}}}}\slimits@^{\mathds{Q}}$
for a conjunction ($\bigwedge$) if $\mathds{Q}=\forall$ and a disjunction
($\bigvee$) if $\mathds{Q}=\exists$. The backbone of our model-checking
algorithm (which we present in Section 6.5) is an effective construction of a
$(\mathcal{G},\dot{s},k)$-summary $\mathcal{A}_{k}$ for each $1\leq k\leq
m+1$. To construct these summaries, we simulate quantification over
strategies. We describe this simulation construction in Algorithm 1. Before
explaining the construction, we state the result of Algorithm 1 as follows:

propositionsimProp Given $\dot{s}\in S$, $\pi\in\mathcal{V}$, a strategy
profile $\@vec{x}:\mathit{{Agts}}\to\mathcal{X}$, a quantifier block $\flat$
such that for every
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}$,
$\@vec{x}({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})$
is quantified in $\flat$, and an APA $\mathcal{A}$ over alphabet
$(V\uplus\\{\pi\\}\to S)$. Let $\mathcal{B}$ be the results of
simulate($\mathcal{G}$,$\dot{s}$,$\pi$,${\@vec{x}}$,$\flat$,$\mathcal{A}$).
Then for any path assignment $\Pi:V\to S^{\omega}$, we have
$\mathit{zip}(\Pi)\in\mathcal{L}(\mathcal{B})$ iff

$\displaystyle\widetilde{\flat}\mathpunct{.}\mathit{zip}\Big{(}\Pi\big{[}\pi\mapsto\mathit{Play}_{\mathcal{G}}\big{(}\dot{s},\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}f_{{\@vec{x}}({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})}\big{)}\big{]}\Big{)}\in\mathcal{L}(\mathcal{A}).$
(1)

That is, the automaton $\mathcal{B}$ accepts the zipping of an assignment
$\Pi:V\to S^{\omega}$ iff by simulating the quantifier prefix in $\flat$, we
construct a path for $\pi$ that, when added to $\Pi$, is accepted by
$\mathcal{A}$. Note the similarity to Definition 10: In Definition 10 we
simulate multiple quantifier blocks to construct paths
$\pi_{k},\ldots,\pi_{m}$ that, when added to $\Pi$, should satisfy the body
$\psi$. In Algorithm 1, we simulate a single path that, when added to $\Pi$,
should be accepted by automaton $\mathcal{A}$. We will later use Algorithm 1
to simulate one quantifier block at a time, eventually reaching an automaton
required by Definition 10.

Before proving Algorithm 1, let us explain the automaton construction in
simulate (Algorithm 1). In Eq. (1), $\widetilde{\flat}$ quantifies over
strategies in $\mathcal{G}$, which are infinite objects (function
$S^{+}\to\mathbb{A}$). The crucial point that we will exploit is that the
underlying game the strategies operate on is _positionally determined_. The
automaton we construct can, therefore, _simulate_ the path $\pi$ in
$\mathcal{G}$ and select fresh actions in each step (instead of fixing
strategies globally) Beutner and Finkbeiner (2021, 2023b, 2024). To do this,
we first translate the APA $\mathcal{A}$ to a DPA
$\mathcal{A}_{\mathit{det}}=(Q,q_{0},\delta,c)$ (in line LABEL:line:toDPA).
The new automaton $\mathcal{B}$ then simulates path $\pi$ by tracking its
current state in $\mathcal{G}$ and simultaneously tracks the current state of
$\mathcal{A}_{\mathit{det}}$, thus operating on states in $Q\times S$. We
start in state $(q_{0},\dot{s})$, i.e., the initial state of
$\mathcal{A}_{\mathit{det}}$ and the designed state $\dot{s}$ from which we
want to start the simulation of $\pi$. The color of each state is simply the
color of the automaton we are tracking, i.e., $c^{\prime}(q,s)=c(q)$ (line
LABEL:line:color). During each transition, we then update the current state of
$\mathcal{A}_{\mathit{det}}$ and the state of the simulation (defined in line
LABEL:line:tran). Concretely, when in state $(q,s)$, we read a letter
${\@vec{t}}:V\to S$ that assigns states to all path variables in $V$ (recall
that the alphabet of $\mathcal{A}$ is $V\cup\\{\pi\\}\to S$ and the alphabet
of $\mathcal{B}$ is $V\to S$). We update the state of
$\mathcal{A}_{\mathit{det}}$ to $\delta(q,{\@vec{t}}[\pi\mapsto s])$, i.e., we
extend the input letter ${\@vec{t}}$ with the current state $s$ of the
simulation of path $\pi$ (note that ${\@vec{t}}[\pi\mapsto
s]:V\cup\\{\pi\\}\to S$). To update the simulation state $s$, we make use of
the positional determinacy of the game: Instead of quantifying over strategies
(as in Eq. (1)), we can quantify over actions in each step of the automaton.
Concretely, for each universally quantified strategy variable in $\flat$, we
pick an action conjunctively, and for each existentially quantified variable,
we pick an action disjunctively. After we have picked actions
$a_{x_{1}},\ldots,a_{x_{n}}$ for all strategies quantified in $\flat$, we can
update the state of the $\pi$-simulation by constructing the action assignment
$\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}a_{\@vec{x}({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})}$,
i.e., assign each agent the corresponding action, and obtain the next state
using $\mathcal{G}$’s transition function $\kappa$.

######  Example 0.

Let us use Example 7 to illustrate the construction in Algorithm 1. Assume we
are given an $(\mathcal{G},\dot{s},3)$-summary $\mathcal{A}_{3}$ over alphabet
$(\\{\pi_{1},\pi_{2}\\}\to S)$, i.e., for every $\Pi:\\{\pi_{1},\pi_{2}\\}\to
S^{\omega}$, we have $\mathit{zip}(\Pi)\in\mathcal{L}(\mathcal{A}_{3})$ iff
$\Pi\models_{\mathcal{G}}\psi$ (cf. Example 11). We invoke
simulate($\mathcal{G}$,$\dot{s}$,$\pi_{2}$,${\@vec{x}}$,$\flat_{2}$,$\mathcal{A}_{3}$)
where ${\@vec{x}}=(w,z,v,v)$ and $\flat_{2}=\exists z\forall w\exists v$, and
let $(Q,q_{0},\delta,c)$ be the DPA equivalent to $\mathcal{A}_{3}$ (computed
in line LABEL:line:toDPA). In this case, simulate computes the APA
$\mathcal{B}=(Q\times S,(q_{0},\dot{s}),\delta^{\prime},c^{\prime})$ over
alphabet $\\{\pi_{1}\\}\to S$ where
$\delta^{\prime}\big{(}(q,s),{\@vec{t}}\big{)}$ is defined as

$\displaystyle\bigvee_{a_{z}\in\mathbb{A}}\;\bigwedge_{a_{w}\in\mathbb{A}}\;\bigvee_{a_{v}\in\mathbb{A}}\Big{(}\delta(q,{\@vec{t}}[\pi_{2}\mapsto
s]),\kappa\big{(}s,(a_{w},a_{z},a_{v},a_{v})\big{)}\Big{)}.$

That is, in each step, we disjunctively choose an action $a_{z}$
(corresponding to the action selected by existentially quantified strategy
$z$), conjunctively pick an action $a_{w}$ (corresponding to the action
selected by universally quantified strategy $w$), and finally disjunctively
select action $a_{v}$. After we have fixed actions $a_{z}$, $a_{w}$ and
$a_{v}$, we take a step in $\mathcal{G}$ by letting each agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
play action
$a_{{\@vec{x}}({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})}$,
i.e., agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}1}$
chooses action $a_{w}$, agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}2}$
chooses $a_{z}$, and agents
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}3}$
and
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}4}$
pick $a_{v}$. By Algorithm 1, every $\Pi:\\{\pi_{1}\\}\to S^{\omega}$
satisfies $\mathit{zip}(\Pi)\in\mathcal{L}(\mathcal{B})$ iff

$\displaystyle\exists f_{z}\mathpunct{.}\forall f_{w}\mathpunct{.}\exists
f_{v}\mathpunct{.}\mathit{zip}\big{(}\Pi[\pi_{2}\mapsto\mathit{Play}_{\mathcal{G}}(\dot{s},(f_{w},f_{z},f_{v},f_{v}))]\big{)}\in\mathcal{L}(\mathcal{A}_{3})$

which (by assumption on $\mathcal{A}_{3}$) holds iff

$\displaystyle\exists f_{z}\mathpunct{.}\forall f_{w}\mathpunct{.}\exists
f_{v}\mathpunct{.}\Pi[\pi_{2}\mapsto\mathit{Play}_{\mathcal{G}}(\dot{s},(f_{w},f_{z},f_{v},f_{v}))]\models_{\mathcal{G}}\psi.$

We have thus used simulate (Algorithm 1) to compute a
$(\mathcal{G},\dot{s},2)$-summary from a $(\mathcal{G},\dot{s},3)$-summary
(cf. Example 11).  $\triangle$

We can now formally prove Algorithm 1:

###### Proof Sketch of Algorithm 1.

The idea of automaton $\mathcal{B}$ constructed in Algorithm 1 is to simulate
the path that corresponds to path variable $\pi$. To argue that $\mathcal{B}$
expresses the desired language, we make use of the positional determinacy of
concurrent parity games (CPG) Malvone et al. (2016). A CPG is a simple multi-
player game model where we can quantify over strategies for each of the
players. For any fixed $\Pi$, we design an (infinite-state) CPG, that is won
iff Eq. (1) holds. We then exploit the fact that CPGs are determined (cf.
(Malvone et al., 2016, Thm. 4.1)), i.e., instead of quantifying over entire
strategies in the CPG, we can quantify over Skolem functions for actions in
each step. This allows us to show that the CPG is won iff $\mathcal{B}$ has an
accepting run (on the fixed $\Pi$), giving us the desired result. We refer the
interested reader to Appendix D for details. ∎

###  6.5. Model-Checking Algorithm

Algorithm 2 Model-checking algorithm for HyperSL[SPE].

⬇

// Assume (*\color{comment-color}$\psi$*) contains no nested state formulas

$\calA_{m+1}$ $\boldsymbol{=}$ LTLtoAPA($\psi$)

// (*\color{black!50!white}$\calA_{m+1}$ is a $(\calG, \dot{s},
m+1)$-summary*)(*\label{line$\boldsymbol{:}$ltlToApa}*)

for $k$ from $m$ to $1$$\boldsymbol{:}$

$\calA_k$ $\boldsymbol{=}$
simulate($\calG$,$\dot{s}$,$\pi_k$,$\bX_k$,$\flat_k$,$\calA_{k+1}$)
(*\label{line$\boldsymbol{:}$product}*)

// (*\color{black!50!white}$\calA_k$ is a $(\calG, \dot{s}, k)$-summary*)
(*\label{line$\boldsymbol{:}$inv}*)

if $\calL(\calA_1) \neq \emptyset$ then
(*\label{line$\boldsymbol{:}$emptinessCheck}*)

return SAT // (*\color{black!50!white}$\dot{s}, \\{\\} \models_\calG
\varphi$*)

else

return UNSAT // (*\color{black!50!white}$\dot{s}, \\{\\} \not\models_\calG
\varphi$ *)

Equipped with the concept of $(\mathcal{G},\dot{s},k)$-summary and the
simulation construction, we can now present our MC algorithm for HyperSL[SPE]
in Algorithm 2. The modelCheck procedure is given a CGS $\mathcal{G}$, a state
$\dot{s}$, and a HyperSL[SPE] formula $\varphi$, and checks if
$\dot{s},\\{\\}\models_{\mathcal{G}}\varphi$. Our algorithm assumes, w.l.o.g.,
that the path formula $\psi$ contains no nested state formulas. In case there
are nested state formulas, we can eliminate them iteratively: We recursively
check each nested state formula on all states of the CGS, and label all states
where the state formula holds with a fresh atomic proposition. In the path
formula, we can then replace each state formula with a reference to the fresh
atomic proposition. See, e.g., Emerson and Halpern (1986); Beutner and
Finkbeiner (2024) for details.

The main idea of our MC algorithm is to iteratively construct a
$(\mathcal{G},\dot{s},k)$-summary $\mathcal{A}_{k}$ for each $1\leq k\leq
m+1$. Initially, in line LABEL:line:ltlToApa, we construct a
$(\mathcal{G},\dot{s},m+1)$-summary $\mathcal{A}_{m+1}$ using a standard
construction to translate the LTL formula $\psi$ to an APA over alphabet
$(\\{\pi_{1},\ldots,\pi_{m}\\}\to S)$, as is, e.g., standard for HyperCTL∗
Finkbeiner et al. (2015). For each $k$ from $m$ to $1$, we then use the
$(\mathcal{G},\dot{s},k+1)$-summary $\mathcal{A}_{k+1}$ to compute a
$(\mathcal{G},\dot{s},k)$-summary $\mathcal{A}_{k}$ using the simulate
construction from Algorithm 1 (similar to what we illustrated in Example 12).
From Algorithm 1, we can conclude the following invariant:

lemmalemmaInd In line LABEL:line:inv, $\mathcal{A}_{k}$ is a
$(\mathcal{G},\dot{s},k)$-summary.

After the loop, we are thus left with a $(\mathcal{G},\dot{s},1)$-summary
$\mathcal{A}_{1}$ (over the simpleton alphabet $(\emptyset\to S)$) and can
check if $\dot{s},\\{\\}\models_{\mathcal{G}}\varphi$ by testing
$\mathcal{A}_{1}$ for emptiness (line LABEL:line:emptinessCheck):

lemmalemmaInit For any $(\mathcal{G},\dot{s},1)$-summary $\mathcal{A}$, we
have that $\mathcal{L}(\mathcal{A})\neq\emptyset$ if and only if
$\dot{s},\\{\\}\models_{\mathcal{G}}\varphi$.

From Algorithms 2 and 2, it follows that
modelCheck($\mathcal{G}$,$\dot{s}$,$\varphi$) returns SAT iff
$\dot{s},\\{\\}\models_{\mathcal{G}}\varphi$, proving Theorem 9.

###  6.6. Model-Checking Complexity

The determinization in line LABEL:line:toDPA of Algorithm 1 results in a DPA
$\mathcal{A}_{\mathit{det}}$ of doubly exponential size (cf. Proposition 1).
The size of $\mathcal{B}$ is then linear in the size of
$\mathcal{A}_{\mathit{det}}$ and $\mathcal{G}$. In the worst case, each call
of simulate thus increases the size of the automaton by two exponents. For a
HyperSL[SPE] formula with block-rank $m$, simulate is called $m$ times, so the
final automaton $\mathcal{A}_{1}$ has, in the worst case, $2m$-exponential
many states (in the size of $\psi$ and $\mathcal{G}$). As we can check
emptiness of APAs over the singleton alphabet $(\emptyset\to S)$ in polynomial
time, we get:

theoremcompTheo Model checking for a HyperSL[SPE] formula with block-rank $m$
is in $2m$-EXPTIME.

From Section 5.2 and the lower bounds known for HyperATL∗ Beutner and
Finkbeiner (2023b), it follows that our algorithm is asymptotically almost
optimal:

lemmalowerBound Model checking for a HyperSL[SPE] formula with block-rank $m$
is $(2m-1)$-EXPSPACE-hard.

Table 1. We compare HyMASMC and MCMAS-SL[1G] on the scheduler problem from Cermák et al. (2015). We give the size of the system ($\boldsymbol{|S|}$), the size of the reachable fragment ($\boldsymbol{|S_{\mathit{reach}}|}$), and the times in seconds ($\boldsymbol{t}$). The timeout (TO) is set to 1 h.  $\boldsymbol{n}$ | $\boldsymbol{|S|}$ | $\boldsymbol{|S_{\mathit{reach}}|}$ | $\boldsymbol{t}_{\texttt{MCMAS-SL[1G]}{}}$ | $\boldsymbol{t}_{\texttt{HyMASMC}}{}$
---|---|---|---|---
2 | 72 | 9 | 0.1 | 0.4
3 | 432 | 21 | 6.71 | 1.9
4 | 2592 | 49 | 313.7 | 24.5
5 | 15552 | 113 | TO | 332.1

###  6.7. Beyond HyperSL[SPE]

HyperSL[SPE] is defined purely in terms of the structure of the quantifier
prefix. As soon as strategy variables are quantified in an order such that
they cannot be grouped together, MC becomes, in general, undecidable: Already
the simplest such property
$\mathds{Q}x.\mathds{Q}y.\mathds{Q}z.\mathds{Q}w\mathpunct{.}\allowbreak\psi[\pi_{1}:(x,z),\pi_{2}:(y,w)]$,
leads to undecidable MC (see Section C.3). The fragment we have identified is
thus the largest possible (when only considering the quantifier prefix). Any
further study into decidable fragments of HyperSL needs to impose restrictions
beyond the prefix and, e.g., analyze how different path variables are related
within an LTL path formula (see also Section 8).

##  7\. Implementation and Experiments

We have implemented our HyperSL[SPE] model-checking algorithm in the HyMASMC
tool Beutner and Finkbeiner (2024).

###  7.1. Model-Checking For Strategy Logic

We compare HyMASMC against MCMAS-SL[1G] Cermák et al. (2015) on (non-hyper)
SL[1G] properties (cf. Section 6.2). In Table 1, we depict the verification
times for the scheduling problem from Cermák et al. (2015) (which can be
expressed in SL[1G] and ATL∗). As in Beutner and Finkbeiner (2024), we observe
that HyMASMC performs much faster than MCMAS-SL[1G], which we largely accredit
to HyMASMC’s efficient automata backend using spot Duret-Lutz et al. (2022).
Note that we use MCMAS-SL[1G] and HyMASMC directly on the original model,
i.e., we did not perform any prepossessing using, e.g., abstraction techniques
Ball and Kupferman (2006); Belardinelli and Lomuscio (2017); Belardinelli et
al. (2023) (which would reduce the system size and make the verification more
scaleable for both tools).

###  7.2. Model-Checking For Hyperproperties

Table 2. We check random formulas from the (Sec), (GE), and (Rnd) templates on the ISPL models from Lomuscio et al. (2009). For each model and template, we sample 10 formulas and report the average time (in seconds).  Model | Sec | GE | Rnd2 | Rnd3 | Rnd4
---|---|---|---|---|---
bit-transmission | 0.6 | 0.7 | 0.8 | 0.8 | 2.7
book-store | 0.4 | 0.4 | 0.4 | 0.5 | 0.5
card-game | 0.4 | 0.5 | 0.4 | 0.5 | 0.5
dining-cryptographers | 0.6 | 2.7 | 11.4 | 22.6 | 10.3
muddy-children | 0.4 | 3.0 | 1.7 | 0.8 | 0.9
simple-card-game | 0.3 | 3.4 | 2.9 | 25.3 | 32.6
software-development | - | - | - | - | -
strongly-connected | 0.6 | 0.8 | 0.8 | 1.7 | 3.2
tianji-horse-racing | 0.4 | 0.5 | 0.4 | 0.5 | 0.5

In a second experiment, we demonstrate that HyMASMC can verify hyperproperties
on various MASs from the literature. We use the ISPL models from the MCMAS
benchmarks suit Lomuscio et al. (2009), and generate random HyperSL[SPE]
formulas from various property templates:

  * •

(Sec): We check if some agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
can reach some target state without leaking information about some secret AP
via some observable AP. Concretely, we check if
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
can play such that on some other path, the same observation sequence is
coupled with a different high-security input, a property commonly referred to
as _non-inference_ McLean (1994) or _opacity_ Zhang et al. (2019); Saboori and
Hadjicostis (2013).

  * •

(GE): We check if a given SL[1G] formula holds on all input sequences for
which _some_ winning output sequence exists, as is, e.g., required in _good-
enough_ synthesis Almagor and Kupferman (2020); Aminof et al. (2021).

  * •

(Rnd): We randomly generate HyperSL[SPE] formulas with block-rank $2,3$, and
$4$ (called Rnd2, Rnd3, and Rnd4, respectively).

We depict the results in Table 2, demonstrating that HyMASMC can handle most
instances. The only exception is the software-development model, which
includes $\approx$15k states and is therefore too large for an automata-based
representation.

We stress that we do not claim that all formulas in each of the templates
model realistic properties in each of the systems. Rather, our evaluation (1)
demonstrates that HyperSL[SPE] can express interesting properties, and (2)
empirically shows that HyMASMC can check such properties in existing ISPL
models (confirming this via further real-world scenarios is interesting future
work).

###  7.3. Model-Checking For Optimal Planning

Table 3. We use HyMASMC to solve the optimal adversarial planning problem (cf. Example 8) for varying sizes. Times are given in seconds, and the TO is set to 120 sec.  Size | 40 | 50 | 60 | 70 | 80 | 90 | 100 | 110 | 120
---|---|---|---|---|---|---|---|---|---
t | 14.2 | 22.0 | 31.2 | 42.5 | 57.6 | 70.1 | 86.8 | 104.6 | TO

In our last experiment, we challenge HyMASMC with planning examples as those
outlined in Example 8. We randomly generate planning instances between the
robot
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}r}$,
adversary
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}a}$,
and
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}\mathit{ndet}}$,
and check if robot
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}r}$
_can_ reach the goal following some shortest path in the problem. For a
varying size $n$, we randomly create $10$ planning instances with $n$ states.
We report the verification times in Table 3. With increasing size, the running
time of HyMASMC clearly increases, but the increase seems to be quadratic
rather than exponential.

##  8\. Conclusion and Future Work

We have presented HyperSL, a new temporal logic that extends strategy logic
with the ability to reason about hyperproperties. HyperSL can express complex
properties in MASs that require a combination of strategic reasoning and
hyper-requirements (such as optimalilty, GE, non-interference, and
quantitative Nash equilibria); many of which were out of reach of existing
logics. As such, HyperSL can serve as a unifying foundation for an exact
exploration of the interaction of strategic behavior with hyperproperties, and
provides a formal language to express (un)decidability results. Moreover, we
have taken a first step towards the ambitious goal of automatically model-
checking HyperSL. Our fragment HyperSL[SPE] subsumes many relevant other
logics and captures unique properties not expressible in existing frameworks.
Our implementation in HyMASMC shows that our MC approach is practical in small
MASs.

A particularly interesting future direction is to search for further fragments
of HyperSL with decidable model checking. As argued in Section 6.7, any such
fragment needs to take the structure of the LTL-formula(s) into account. For
example, Mogavero et al. Mogavero et al. (2013) showed that SL[CG] (a fragment
of SL that only allows conjunctions of goal formulas) still admits behavioral
strategies (i.e., strategies that do not depend on future or counterfactual
decisions of other strategies). When extending this to our hyper setting, it
seems likely that if a strategy is used on multiple path variables, but these
paths occur in disjoint conjuncts of path formulas, MC remains decidable. We
leave such extensions as future work.

This work was supported by the European Research Council (ERC) Grant HYPER
(101055412), and by the German Research Foundation (DFG) as part of TRR 248
(389792660).

## References

  * (1)
  * Almagor and Kupferman (2020) Shaull Almagor and Orna Kupferman. 2020.  Good-Enough Synthesis. In _International Conference on Computer Aided Verification, CAV 2020_.
  * Alur et al. (2002) Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. 2002\.  Alternating-time temporal logic.  _J. ACM_ (2002).
  * Aminof et al. (2021) Benjamin Aminof, Giuseppe De Giacomo, and Sasha Rubin. 2021\.  Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up. In _International Joint Conference on Artificial Intelligence, IJCAI 2021_.
  * Aminof et al. (2019) Benjamin Aminof, Marta Kwiatkowska, Bastien Maubert, Aniello Murano, and Sasha Rubin. 2019\.  Probabilistic Strategy Logic. In _International Joint Conference on Artificial Intelligence, IJCAI 2019_.
  * Ball and Kupferman (2006) Thomas Ball and Orna Kupferman. 2006.  An Abstraction-Refinement Framework for Multi-Agent Systems. In _Symposium on Logic in Computer Science LICS 2006_.
  * Belardinelli et al. (2023) Francesco Belardinelli, Angelo Ferrando, Wojciech Jamroga, Vadim Malvone, and Aniello Murano. 2023\.  Scalable Verification of Strategy Logic through Three-Valued Abstraction. In _International Joint Conference on Artificial Intelligence, IJCAI 2023_.
  * Belardinelli et al. (2021) Francesco Belardinelli, Sophia Knight, Alessio Lomuscio, Bastien Maubert, Aniello Murano, and Sasha Rubin. 2021.  Reasoning About Agents That May Know Other Agents’ Strategies. In _International Joint Conference on Artificial Intelligence, IJCAI 2021_.
  * Belardinelli and Lomuscio (2017) Francesco Belardinelli and Alessio Lomuscio. 2017.  Agent-based Abstractions for Verifying Alternating-time Temporal Logic with Imperfect Information. In _Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017_.
  * Belardinelli et al. (2019) Francesco Belardinelli, Alessio Lomuscio, and Vadim Malvone. 2019\.  An Abstraction-Based Method for Verifying Strategic Properties in Multi-Agent Systems with Imperfect Information. In _Conference on Artificial Intelligence, AAAI 2019_.
  * Belardinelli et al. (2017) Francesco Belardinelli, Alessio Lomuscio, Aniello Murano, and Sasha Rubin. 2017.  Verification of Multi-agent Systems with Imperfect Information and Public Actions. In _Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017_.
  * Berthon et al. (2017a) Raphaël Berthon, Bastien Maubert, and Aniello Murano. 2017a.  Decidability Results for ATL* with Imperfect Information and Perfect Recall. In _Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017_.
  * Berthon et al. (2017b) Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin, and Moshe Y. Vardi. 2017b.  Strategy logic with imperfect information. In _Symposium on Logic in Computer Science, LICS 2017_.
  * Berthon et al. (2021) Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin, and Moshe Y. Vardi. 2021\.  Strategy Logic with Imperfect Information.  _ACM Trans. Comput. Log._ (2021).
  * Beutner and Finkbeiner (2021) Raven Beutner and Bernd Finkbeiner. 2021.  A Temporal Logic for Strategic Hyperproperties. In _International Conference on Concurrency Theory, CONCUR 2021_.
  * Beutner and Finkbeiner (2022) Raven Beutner and Bernd Finkbeiner. 2022.  Software Verification of Hyperproperties Beyond k-Safety. In _International Conference on Computer Aided Verification, CAV 2022_.
  * Beutner and Finkbeiner (2023a) Raven Beutner and Bernd Finkbeiner. 2023a.  AutoHyper: Explicit-State Model Checking for HyperLTL. In _International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023_.
  * Beutner and Finkbeiner (2023b) Raven Beutner and Bernd Finkbeiner. 2023b.  HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems.  _Log. Methods Comput. Sci._ (2023).
  * Beutner and Finkbeiner (2024) Raven Beutner and Bernd Finkbeiner. 2024.  On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing. In _Conference on Artificial Intelligence, AAAI 2024_.
  * Beutner et al. (2023) Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, and Niklas Metzger. 2023.  Second-Order Hyperproperties. In _International Conference on Computer Aided Verification, CAV 2023_.
  * Bouyer et al. (2019) Patricia Bouyer, Orna Kupferman, Nicolas Markey, Bastien Maubert, Aniello Murano, and Giuseppe Perelli. 2019.  Reasoning about Quality and Fuzziness of Strategic Behaviours. In _International Joint Conference on Artificial Intelligence, IJCAI 2019_.
  * Bozzelli et al. (2015) Laura Bozzelli, Bastien Maubert, and Sophie Pinchinat. 2015\.  Unifying Hyper and Epistemic Temporal Logics. In _International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2015_.
  * Bulling and Jamroga (2014) Nils Bulling and Wojciech Jamroga. 2014.  Comparing variants of strategic ability: how uncertainty and memory influence general properties of games.  _Auton. Agents Multi Agent Syst._ (2014).
  * Cermák et al. (2015) Petr Cermák, Alessio Lomuscio, and Aniello Murano. 2015\.  Verifying and Synthesising Multi-Agent Systems against One-Goal Strategy Logic Specifications. In _Conference on Artificial Intelligence, AAAI 2015_.
  * Chatterjee et al. (2010) Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. 2010\.  Strategy logic.  _Inf. Comput._ (2010).
  * Chaudhuri et al. (2012) Swarat Chaudhuri, Sumit Gulwani, and Roberto Lublinerman. 2012\.  Continuity and robustness of programs.  _Commun. ACM_ (2012).
  * Clarkson et al. (2014) Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. 2014\.  Temporal Logics for Hyperproperties. In _International Conference on Principles of Security and Trust, POST 2014_.
  * Clarkson and Schneider (2008) Michael R. Clarkson and Fred B. Schneider. 2008.  Hyperproperties. In _Computer Security Foundations Symposium, CSF 2008_.
  * Coenen et al. (2019) Norine Coenen, Bernd Finkbeiner, Christopher Hahn, and Jana Hofmann. 2019.  The Hierarchy of Hyperlogics. In _Symposium on Logic in Computer Science, LICS 2019_.
  * Dima and Tiplea (2011) Catalin Dima and Ferucio Laurentiu Tiplea. 2011.  Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable.  _CoRR_ (2011).
  * Duret-Lutz et al. (2022) Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. 2022\.  From Spot 2.0 to Spot 2.10: What’s New?. In _International Conference on Computer Aided Verification, CAV 2022_.
  * Emerson and Halpern (1986) E. Allen Emerson and Joseph Y. Halpern. 1986.  ”Sometimes” and ”Not Never” revisited: on branching versus linear time temporal logic.  _J. ACM_ (1986).
  * Finkbeiner et al. (2018) Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. 2018\.  Synthesizing Reactive Systems from Hyperproperties. In _International Conference on Computer Aided Verification, CAV 2018_.
  * Finkbeiner et al. (2015) Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. 2015.  Algorithms for Model Checking HyperLTL and HyperCTL*. In _International Conference on Computer Aided Verification, CAV 2015_.
  * Finkbeiner and Zimmermann (2017) Bernd Finkbeiner and Martin Zimmermann. 2017.  The First-Order Logic of Hyperproperties. In _Symposium on Theoretical Aspects of Computer Science, STACS 2017_.
  * Gutsfeld et al. (2020) Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. 2020.  Propositional Dynamic Logic for Hyperproperties. In _International Conference on Concurrency Theory, CONCUR 2020_.
  * Knight and Maubert (2019) Sophia Knight and Bastien Maubert. 2019.  Dealing with imperfect information in Strategy Logic.  _CoRR_ (2019).
  * Laroussinie and Markey (2015) François Laroussinie and Nicolas Markey. 2015.  Augmenting ATL with strategy contexts.  _Inf. Comput._ (2015).
  * Laroussinie et al. (2015) François Laroussinie, Nicolas Markey, and Arnaud Sangnier. 2015\.  ATLsc with partial observation. In _International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2015_.
  * Lomuscio et al. (2009) Alessio Lomuscio, Hongyang Qu, and Franco Raimondi. 2009\.  MCMAS: A Model Checker for the Verification of Multi-Agent Systems. In _International Conference on Computer Aided Verification, CAV 2009_.
  * Malvone et al. (2016) Vadim Malvone, Aniello Murano, and Loredana Sorrentino. 2016\.  Concurrent Multi-Player Parity Games. In _International Conference on Autonomous Agents & Multiagent Systems, AAMAS 2016_.
  * Maubert and Murano (2018) Bastien Maubert and Aniello Murano. 2018.  Reasoning about Knowledge and Strategies under Hierarchical Information. In _International Conference on Principles of Knowledge Representation and Reasoning, KR 2018_.
  * McCullough (1988) Daryl McCullough. 1988\.  Noninterference and the composability of security properties. In _Symposium on Security and Privacy, SP 1988_.
  * McLean (1994) John McLean. 1994\.  A general theory of composition for trace sets closed under selective interleaving functions. In _Symposium on Research in Security and Privacy, SP 1994_.
  * Miyano and Hayashi (1984) Satoru Miyano and Takeshi Hayashi. 1984.  Alternating Finite Automata on omega-Words.  _Theor. Comput. Sci._ (1984).
  * Mogavero et al. (2014b) Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. 2014b.  Reasoning About Strategies: On the Model-Checking Problem.  _ACM Trans. Comput. Log._ (2014).
  * Mogavero et al. (2013) Fabio Mogavero, Aniello Murano, and Luigi Sauro. 2013\.  On the Boundary of Behavioral Strategies. In _Symposium on Logic in Computer Science, LICS 2013_.
  * Mogavero et al. (2014a) Fabio Mogavero, Aniello Murano, and Luigi Sauro. 2014a.  A Behavioral Hierarchy of Strategy Logic. In _International Workshop on Computational Logic in Multi-Agent Systems, CLIMA 2014_.
  * Nash Jr (1950) John F Nash Jr. 1950\.  Equilibrium points in n-person games.  _Proceedings of the national academy of sciences_ (1950).
  * Pauly and Parikh (2003) Marc Pauly and Rohit Parikh. 2003.  Game Logic - An Overview.  _Stud Logica_ (2003).
  * Piterman (2007) Nir Piterman. 2007\.  From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata.  _Log. Methods Comput. Sci._ (2007).
  * Sabelfeld (2003) Andrei Sabelfeld. 2003\.  Confidentiality for Multithreaded Programs via Bisimulation. In _International Conference on Perspectives of Systems Informatics, PSI 2003_.
  * Saboori and Hadjicostis (2013) Anooshiravan Saboori and Christoforos N. Hadjicostis. 2013\.  Verification of initial-state opacity in security applications of discrete event systems.  _Inf. Sci._ (2013).
  * Vardi (1995) Moshe Y. Vardi. 1995\.  Alternating Automata and Program Verification.  In _Computer Science Today: Recent Trends and Developments_.
  * Wittbold and Johnson (1990) J. Todd Wittbold and Dale M. Johnson. 1990.  Information Flow in Nondeterministic Systems. In _Symposium on Security and Privacy, SP 1990_.
  * Zhang et al. (2019) Kuize Zhang, Xiang Yin, and Majid Zamani. 2019.  Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach.  _IEEE Trans. Autom. Control._ (2019).

##  Appendix A Additional Material for Section 3

In this section we give details on the semantics of APAs. To make our later
proofs (which use the APA semantics) easier, we use a DAG-based semantics
(opposed to the more prominently used – but equivalent – tree-based
semantics). We refer the reader to Vardi (1995) for more details.

######  Definition 0.

For a set $Q$, we write $\mathbb{B}^{+}(Q)$ for the set of all positive
boolean formulas over $Q$, i.e., all formulas generated by the grammar

$\displaystyle\theta:=q\mid\theta_{1}\land\theta_{2}\mid\theta_{1}\lor\theta_{2}$

where $q\in Q$. Given a subset $X\subseteq Q$ and
$\theta\in\mathbb{B}^{+}(Q)$, we write $X\models\theta$ if the assignment that
maps all states in $X$ to $\top$ and those in $Q\setminus X$ to $\bot$
satisfies $\Psi$. For example $\\{q_{0},q_{1}\\}\models q_{0}\land(q_{1}\lor
q_{2})$.

Let $\mathcal{A}=(Q,q_{0},\delta,c)$ be an APA. A run DAG of $\mathcal{A}$ is
a pair $\mathbb{D}=(V,E)$ of nodes and edges such that $V\subseteq Q\times
Nature$, $E\subseteq\bigcup_{i\in
Nature}(Q\times\\{i\\})\times(Q\times\\{i+1\\})$. That is, each node in $V$
consist of a state in $Q$ and a depth and the edges in $E$ only reach from
depth $i$ to depth $i+1$. For every $(q,i)\in V$, we define
$\mathit{sucs}(q,i):=\\{q^{\prime}\mid((q,i),(q^{\prime},i+1))\in E\\}$ as the
state component of $(q,i)$’s successor nodes.

A run of $\mathcal{A}$ on a word $u\in\Sigma^{\omega}$ is a run DAG
$\mathbb{D}=(V,E)$ such that $(q_{0},0)\in V$ and for every $(q,i)\in V$,
$\mathit{sucs}(q,i)\models\delta(q,u(i))$. That is, the run DAG starts in the
initial state $q_{0}$ at depth $0$, and for each node in the DAG the
successors of each node satisfy the transition formula given by the transition
function $\delta$.

For example, consider a node $(q,i)$ and assume that $\delta(q,u(i))=q_{1}\lor
q_{2}$. Then the DAG must include either $q_{1}$ or $q_{2}$ (or both) as
successors in the next level. In particular, if the transition function
$\delta$ uses only disjunctions (no conjunctions) the automataon is non-
deterministic. In this case, each node in the DAG can have a unique successor;
the DAG is a line (a infinite sequence of states). Conversely, if
$\delta(q,u(i))=q_{1}\land q_{2}$ then both $q_{1}$ and $q_{2}$ need to appear
in the next level, i.e., we need to construct accepting runs from both of
these states.

A run DAG $\mathbb{D}$ is accepting if for every infinite path in the DAG the
minimal color that occurs infinitely many times (as given by $c$) is even. We
define $\mathcal{L}(\mathcal{A})\subseteq\Sigma^{\omega}$ as all infinite
words on which $\mathcal{A}$ has an accepting run DAG.

##  Appendix B Additional Material for Section 5

We provide some background on the temporal logics HyperLTL, SL, HyperATL∗, and
HyperATL${}^{*}_{S}$ and give their full semantics.

###  B.1. SL and HyperSL

In this subsection, we provide addition details on the relation of SL and
HyperSL (cf. Section 5.1). We consider a variant of SL that allows multiple
agents to share the strategy by using explicit agent binding, but disallows
agent bindings under temporal operators.

######  Remark 0.

The strategy logic by Mogavero et al. (2014b) allows arbitrary nesting of
agent binding within temporal operators. Our variant is equivalent to SL[BG]
Mogavero et al. (2014b) – a fragment that follows a strict separation between
state and path formulas and thereby forbids agent binding under temporal
operators. Note that SL[BG] strictly subsumes the strategy logic by Chatterjee
et al. Chatterjee et al. (2010). We choose to restrict to the SL[BG] fragment
as it is syntactically closer to temporal logics like CTL∗ and HyperCTL∗ and,
thereby, also to HyperSL.

State and path formulas in SL are defined as follows:

$\displaystyle{\psi}$
$\displaystyle:=a\mid{\varphi}\mid\neg{\psi}\mid{\psi}\land{\psi}\mid\operatorname{\textsf{X}}{\psi}\mid{\psi}\operatorname{\textsf{U}}{\psi}$
$\displaystyle{\varphi}$
$\displaystyle:={\psi}\mid{\varphi}\land{\varphi}\mid{\varphi}\lor{\varphi}\mid\forall
x\mathpunct{.}{\varphi}\mid\exists
x\mathpunct{.}{\varphi}\mid({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},x){\varphi}$

where $a\in\mathit{AP}$, $x\in\mathcal{X}$, and
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}$.
Importantly, we assume that every state formula occurring in a path formula is
closed.

The idea of SL is to separate the quantification of a strategy and the binding
of a strategy to some agent. To accomplish the latter, it features an explicit
agent-binding construct
$({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},x){\varphi}$
which evaluates ${\varphi}$ after binding agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
to strategy $x$.

##### Semantics

Assume $\mathcal{G}=(S,s_{0},\mathbb{A},\kappa,L)$ is a fixed CGS. Given a
path $p\in S^{\omega}$ we define the semantics of path formulas as expected:

$\displaystyle p$ $\displaystyle\models_{\mathcal{G}}a$ iff $\displaystyle
a\in L(p(0))$ $\displaystyle p$ $\displaystyle\models_{\mathcal{G}}{\varphi}$
iff $\displaystyle p(0),\\{\\},\\{\\}\models_{\mathcal{G}}{\varphi}$
$\displaystyle p$
$\displaystyle\models_{\mathcal{G}}{\psi}_{1}\land{\psi}_{2}$ iff
$\displaystyle p\models_{\mathcal{G}}{\psi}_{1}\text{ and
}p\models_{\mathcal{G}}{\psi}_{2}$ $\displaystyle p$
$\displaystyle\models_{\mathcal{G}}\neg{\psi}$ iff $\displaystyle
p\not\models_{\mathcal{G}}{\psi}$ $\displaystyle p$
$\displaystyle\models_{\mathcal{G}}\operatorname{\textsf{X}}{\psi}$ iff
$\displaystyle p[1,\infty]\models_{\mathcal{G}}{\psi}$ $\displaystyle p$
$\displaystyle\models_{\mathcal{G}}{\psi}_{1}\operatorname{\textsf{U}}{\psi}_{2}$
iff $\displaystyle\exists j\in
Nature\mathpunct{.}p[j,\infty]\models_{\mathcal{G}}{\psi}_{2}\text{ and }$
$\displaystyle\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\forall 0\leq
k<j\mathpunct{.}p[k,\infty]\models_{\mathcal{G}}{\psi}_{1}$

In the semantics of state formulas, we keep track of a strategy for each
strategy variable via a (partial) strategy assignment
$\Delta:\mathcal{X}\rightharpoonup\mathit{Str}(\mathcal{G})$, similar to the
HyperSL semantics. As SL works with explicit agent bindings, we also keep
track of a strategy for each agent using a (partial) function
$\Theta:\mathit{{Agts}}\rightharpoonup\mathit{Str}(\mathcal{G})$. We can then
define:

$\displaystyle s,\Delta,\Theta\models_{\mathcal{G}}\forall
x\mathpunct{.}{\varphi}$ iff $\displaystyle\forall
f\in\mathit{Str}(\mathcal{G})\mathpunct{.}s,\Delta[x\mapsto
f],\Theta\models_{\mathcal{G}}{\varphi}$ $\displaystyle
s,\Delta,\Theta\models_{\mathcal{G}}\exists x\mathpunct{.}{\varphi}$ iff
$\displaystyle\exists
f\in\mathit{Str}(\mathcal{G})\mathpunct{.}s,\Delta[x\mapsto
f],\Theta\models_{\mathcal{G}}{\varphi}$ $\displaystyle
s,\Delta,\Theta\models_{\mathcal{G}}({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},x){\varphi}$
iff $\displaystyle
s,\Delta,\Theta[{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mapsto\Delta(x)]\models_{\mathcal{G}}{\varphi}$
$\displaystyle
s,\Delta,\Theta\models_{\mathcal{G}}{\varphi}_{1}\land{\varphi}_{2}$ iff
$\displaystyle s,\Delta,\Theta\models_{\mathcal{G}}{\varphi}_{1}\text{ and
}s,\Delta,\Theta\models_{\mathcal{G}}{\varphi}_{2}$ $\displaystyle
s,\Delta,\Theta\models_{\mathcal{G}}{\varphi}_{1}\lor{\varphi}_{2}$ iff
$\displaystyle s,\Delta,\Theta\models_{\mathcal{G}}{\varphi}_{1}\text{ or
}s,\Delta,\Theta\models_{\mathcal{G}}{\varphi}_{2}$ $\displaystyle
s,\Delta,\Theta\models_{\mathcal{G}}{\psi}$ iff
$\displaystyle\mathit{Play}_{\mathcal{G}}\big{(}s,\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}\Theta({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})\big{)}\models_{\mathcal{G}}{\psi}$

Strategy quantification updates the binding in $\Delta$ (as in HyperSL),
whereas strategy binding updates the assignment of agents in $\Theta$. For
each path formula we use the strategy profile $\Theta$ (mapping each agent to
a strategy) to construct the path on which we evaluate $\psi$. We write
$\mathcal{G}\models_{\text{SL}}{\varphi}$ if
$s_{0},\\{\\},\\{\\}\models_{\mathcal{G}}{\varphi}$ in the SL semantics.

##### Encoding

We can easily encode SL into HyperSL. Instead of using explicit agent bindings
as in SL, in HyperSL, each path is annotated with an explicit strategy profile
that assigns a strategy (variable) to each agent. We assume that in the SL
formula no two quantifiers quantify the same strategy variable (which we can
always ensure by $\alpha$-renaming). Let $\dot{\pi}$ denote some _fixed_ path
variable. In our translation, we maintain an auxiliary mapping
${\@vec{x}}:\mathit{{Agts}}\rightharpoonup\mathcal{X}$ mapping agents to
strategy variables. We then translate path formulas as follows:

$\displaystyle{\llparenthesis}a{\rrparenthesis}$
$\displaystyle:=a_{\dot{\pi}}$
$\displaystyle{\llparenthesis}\neg{\psi}{\rrparenthesis}$
$\displaystyle:=\neg{\llparenthesis}{\psi}{\rrparenthesis}$
$\displaystyle{\llparenthesis}{\psi}_{1}\land{\psi}_{2}{\rrparenthesis}$
$\displaystyle:={\llparenthesis}{\psi}_{1}{\rrparenthesis}\land{\llparenthesis}{\psi}_{2}{\rrparenthesis}$
$\displaystyle{\llparenthesis}{\varphi}{\rrparenthesis}$
$\displaystyle:={\llparenthesis}{\varphi}{\rrparenthesis}^{\\{\\}}$
$\displaystyle{\llparenthesis}\operatorname{\textsf{X}}{\psi}{\rrparenthesis}$
$\displaystyle:=\operatorname{\textsf{X}}{\llparenthesis}{\psi}{\rrparenthesis}$
$\displaystyle{\llparenthesis}{\psi}_{1}\operatorname{\textsf{U}}{\psi}_{2}{\rrparenthesis}$
$\displaystyle:={\llparenthesis}{\psi}_{1}{\rrparenthesis}\operatorname{\textsf{U}}{\llparenthesis}{\psi}_{2}{\rrparenthesis}$

For state formulas we define:

$\displaystyle{\llparenthesis}{\varphi}_{1}\land{\varphi}_{2}{\rrparenthesis}^{\@vec{x}}$
$\displaystyle:={\llparenthesis}{\varphi}_{1}{\rrparenthesis}^{\@vec{x}}\land{\llparenthesis}{\varphi}_{2}{\rrparenthesis}^{\@vec{x}}$
$\displaystyle{\llparenthesis}{\varphi}_{1}\lor{\varphi}_{2}{\rrparenthesis}^{\@vec{x}}$
$\displaystyle:={\llparenthesis}{\varphi}_{1}{\rrparenthesis}^{\@vec{x}}\lor{\llparenthesis}{\varphi}_{2}{\rrparenthesis}^{\@vec{x}}$
$\displaystyle{\llparenthesis}\forall
x\mathpunct{.}{\varphi}{\rrparenthesis}^{\@vec{x}}$ $\displaystyle:=\forall
x\mathpunct{.}{\llparenthesis}{\varphi}{\rrparenthesis}^{\@vec{x}}$
$\displaystyle{\llparenthesis}\exists
x\mathpunct{.}{\varphi}{\rrparenthesis}^{\@vec{x}}$ $\displaystyle:=\exists
x\mathpunct{.}{\llparenthesis}{\varphi}{\rrparenthesis}^{\@vec{x}}$
$\displaystyle{\llparenthesis}{\psi}{\rrparenthesis}^{\@vec{x}}$
$\displaystyle:={\llparenthesis}{\psi}{\rrparenthesis}[\dot{\pi}:{\@vec{x}}]$
$\displaystyle{\llparenthesis}({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},x){\varphi}{\rrparenthesis}^{\@vec{x}}$
$\displaystyle:={\llparenthesis}{\varphi}{\rrparenthesis}^{{\@vec{x}}[{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mapsto
x]}$

For path formulas, we resolve all atomic propositions on the fixed path
variable $\dot{\pi}$. For state formulas, we record the strategy variable
played by each agent in the function ${\@vec{x}}$, and whenever we reach a
path formula, use ${\@vec{x}}$ to construct the fixed path $\dot{\pi}$. Note
that the formula resulting from the translation uses boolean combination of
state formulas. As already argued in Section 4, we can bring such formulas
into the HyperSL syntax by introducing multiple paths (see Example 2). We can
show that our translation is correct and thus prove Section 5.1:

*

###### Proof.

We can easily show that for any game structure $\mathcal{G}$ and SL formula
${\varphi}$, we have that $\mathcal{G}\models_{\text{SL}}{\varphi}$ if an only
if $\mathcal{G}\models{\llparenthesis}{\varphi}{}{\rrparenthesis}^{\\{\\}}$. ∎

###  B.2. HyperATL∗ and HyperSL

In this subsection, we provide addition details on the relation of HyperATL∗
and HyperSL (cf. Section 5.2).

Our hyper variant of strategy logic considers strategies as first-order
objects that can be compared in different strategy profiles. A weaker form of
strategic reasoning is offered in ATL∗ Alur et al. (2002) by only reasoning
about the _outcome_ of a strategic interaction. The ATL∗ formula $\llangle
A\rrangle\psi$ expresses that the agents in $A$ have a joint strategy to
enforce that the system follows some path that satisfies $\psi$. HyperATL∗
Beutner and Finkbeiner (2021, 2023b) is a hyper-variant of ATL that combines
strategic reasoning with the ability to express hyperproperties. Similar to
ATL∗, HyperATL∗ only considers the outcomes of a strategy but binds this
outcome to a path variable which allows comparison w.r.t. a hyperproperty.
Formulas in HyperATL∗ are generated by the following grammar:

$\displaystyle{\psi}$
$\displaystyle:=a_{\pi}\mid\neg{\psi}\mid{\psi}\land{\psi}\mid\operatorname{\textsf{X}}{\psi}\mid{\psi}\operatorname{\textsf{U}}{\psi}$
$\displaystyle{\varphi}$ $\displaystyle:=\llangle
A\rrangle\pi\mathpunct{.}{\varphi}\mid\llbracket
A\rrbracket\pi\mathpunct{.}{\varphi}\mid{\psi}$

where $a\in\mathit{AP}$, $\pi\in\mathcal{V}$, and $A\subseteq\mathit{{Agts}}$.

##### Semantics

The semantics of HyperATL∗ operates on a path assignment
$\Pi:\mathcal{V}\rightharpoonup S^{\omega}$. For path formulas, we follow a
similar semantics as used in HyperSL (cf. Section 4):

$\displaystyle\Pi$ $\displaystyle\models_{\mathcal{G}}a_{\pi}$ iff
$\displaystyle a\in L(\Pi(\pi)(0))$ $\displaystyle\Pi$
$\displaystyle\models_{\mathcal{G}}{\psi}_{1}\land{\psi}_{2}$ iff
$\displaystyle\Pi\models_{\mathcal{G}}{\psi}_{1}\text{ and
}\Pi\models_{\mathcal{G}}{\psi}_{2}$ $\displaystyle\Pi$
$\displaystyle\models_{\mathcal{G}}\neg{\psi}$ iff
$\displaystyle\Pi\not\models_{\mathcal{G}}{\psi}$ $\displaystyle\Pi$
$\displaystyle\models_{\mathcal{G}}\operatorname{\textsf{X}}{\psi}$ iff
$\displaystyle\Pi[1,\infty]\models_{\mathcal{G}}{\psi}$ $\displaystyle\Pi$
$\displaystyle\models_{\mathcal{G}}{\psi}_{1}\operatorname{\textsf{U}}{\psi}_{2}$
iff $\displaystyle\exists j\in
Nature\mathpunct{.}\Pi[j,\infty]\models_{\mathcal{G}}{\psi}_{2}\text{ and }$
$\displaystyle\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\forall 0\leq
k<j\mathpunct{.}\Pi[k,\infty]\models_{\mathcal{G}}{\psi}_{1}$

For state formulas, we need to consider all possible outcomes under strategies
for a subset of the agents. Given $A\subseteq\mathit{{Agts}}$ and strategies
$\\{f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mid{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in
A\\}$ we define
$\mathit{out}_{\mathcal{G}}\big{(}s,\\{f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mid{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in
A\\}\big{)}\subseteq S^{\omega}$ as

$\displaystyle\mathit{out}_{\mathcal{G}}\big{(}s,$
$\displaystyle\\{f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mid{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in
A\\}\big{)}:=$
$\displaystyle\Big{\\{}\mathit{Play}_{\mathcal{G}}(s,\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})\mid\forall{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}\setminus
A\mathpunct{.}f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{Str}(\mathcal{G})\Big{\\}}.$

That is,
$\mathit{out}_{\mathcal{G}}\big{(}s,\\{f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mid{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in
A\\}\big{)}$ contains all possible paths compatible with the strategies in
$\\{f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mid{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in
A\\}$. We can then evaluate a state formula in the context of a state $s$ and
path assignment $\Pi$.

$\displaystyle s,\Pi$ $\displaystyle\models_{\mathcal{G}}{\psi}\quad$
$\displaystyle\text{iff}\quad\Pi\models_{\mathcal{G}}{\psi}$ $\displaystyle
s,\Pi$ $\displaystyle\models_{\mathcal{G}}\llangle
A\rrangle\pi\mathpunct{.}{\varphi}$
$\displaystyle\text{iff}\quad\exists\\{f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mid{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in
A\\}\mathpunct{.}$ $\displaystyle\quad\quad\quad\forall
p\in\mathit{out}_{\mathcal{G}}\big{(}s,\\{f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mid{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in
A\\}\big{)}\mathpunct{.}s,\Pi[\pi\mapsto p]\models_{\mathcal{G}}{\varphi}$
$\displaystyle s,\Pi$ $\displaystyle\models_{\mathcal{G}}\llbracket
A\rrbracket\pi\mathpunct{.}{\varphi}$
$\displaystyle\text{iff}\quad\forall\\{f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mid{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in
A\\}\mathpunct{.}$ $\displaystyle\quad\quad\quad\exists
p\in\mathit{out}_{\mathcal{G}}\big{(}s,\\{f_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mid{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in
A\\}\big{)}\mathpunct{.}s,\Pi[\pi\mapsto p]\models_{\mathcal{G}}{\varphi}$

That is, a formula $\llangle A\rrangle\pi\mathpunct{.}{\varphi}$ holds when
there exist strategies for all agents in $A$ such that all possible outcomes
under those fixed strategies, when bound to $\pi$, satisfy ${\varphi}$.
Likewise, $\llbracket A\rrbracket\pi\mathpunct{.}{\varphi}$ holds when all
possible strategies admits some path that, when bound to $\pi$, satisfies
${\varphi}$. We write $\mathcal{G}\models_{\text{HyperATL${}^{*}$}}{\varphi}$
if $s_{0},\\{\\}\models_{\mathcal{G}}{\varphi}$ in the HyperATL∗ semantics.

##### Encoding

Similar to the fact that ATL∗ can be encoded in SL Chatterjee et al. (2010),
we can encode HyperATL∗ in HyperSL. The idea is to treat the ATL-quantifier
$\llangle A\rrangle$ as a strategy quantifier that existentially quantifies
over strategies for agents in $A$ and then universally over strategies for
agents outside of $A$. HyperATL∗ path formulas can be translated verbatim into
HyperSL path formulas. To translate state formulas we maintain a auxiliary
mapping
${\boldsymbol{l}}:\mathcal{V}\rightharpoonup\mathcal{X}^{\mathit{{Agts}}}$
from path variables to strategy profiles:

$\displaystyle{\llparenthesis}{\psi}{\rrparenthesis}^{\boldsymbol{l}}$
$\displaystyle:={\psi}[\pi_{1}:{\boldsymbol{l}}(\pi_{1}),\ldots,\pi_{m}:{\boldsymbol{l}}(\pi_{m})]$
$\displaystyle{\llparenthesis}\llangle
A\rrangle\pi.{\varphi}{\rrparenthesis}^{\boldsymbol{l}}$
$\displaystyle:=\operatorname*{\vphantom{\sum}\mathchoice{\vbox{\hbox{$\exists$}}}{\vbox{\hbox{$\exists$}}}{\vbox{\hbox{$\exists$}}}{\vbox{\hbox{$\exists$}}}}_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in
A}x_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mathpunct{.}\operatorname*{\vphantom{\sum}\mathchoice{\vbox{\hbox{$\forall$}}}{\vbox{\hbox{$\forall$}}}{\vbox{\hbox{$\forall$}}}{\vbox{\hbox{$\forall$}}}}_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}\setminus
A}\\!\\!\\!x_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mathpunct{.}\,{\llparenthesis}{\varphi}{\rrparenthesis}^{{\boldsymbol{l}}[\pi\mapsto\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}x_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}]}$
$\displaystyle{\llparenthesis}\llbracket
A\rrbracket\pi.{\varphi}{\rrparenthesis}^{\boldsymbol{l}}$
$\displaystyle:=\operatorname*{\vphantom{\sum}\mathchoice{\vbox{\hbox{$\forall$}}}{\vbox{\hbox{$\forall$}}}{\vbox{\hbox{$\forall$}}}{\vbox{\hbox{$\forall$}}}}_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in
A}x_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mathpunct{.}\operatorname*{\vphantom{\sum}\mathchoice{\vbox{\hbox{$\exists$}}}{\vbox{\hbox{$\exists$}}}{\vbox{\hbox{$\exists$}}}{\vbox{\hbox{$\exists$}}}}_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}\setminus
A}\\!\\!\\!x_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\mathpunct{.}\,{\llparenthesis}{\varphi}{\rrparenthesis}^{{\boldsymbol{l}}[\pi\mapsto\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}x_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}]}$

In the first case, we assume that $\pi_{1},\ldots,\pi_{m}$ are the path
variables used in ${\psi}$. In the second and third case, we assume that
$x_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}1},\ldots,x_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}n}$
are fresh strategy variables for each agent. Intuitively, we replace each
$\llangle A\rrangle\pi$ quantifier with existential quantification over fresh
strategies for $A$, followed by universal quantification over strategies for
$\mathit{{Agts}}\setminus A$. In the auxiliary mapping ${\boldsymbol{l}}$, we
record which strategy profile we later want to use to construct $\pi$. For the
path formula $\psi$ we then reconstruct all paths used in the formula using
the strategy profiles recorded in ${\boldsymbol{l}}$. We can use our
translation to prove Section 5.2:

*

###### Proof.

An easy induction shows that for any game structure $\mathcal{G}$ and
HyperATL∗ formula ${\varphi}$ it holds that
$\mathcal{G}\models_{\text{HyperATL${}^{*}$}}{\varphi}$ if and only if
$\mathcal{G}\models{\llparenthesis}{\varphi}{\rrparenthesis}^{\\{\\}}$. ∎

##### HyperATL${}^{*}_{S}$

As our translation ${\llparenthesis}{\varphi}{\rrparenthesis}^{\\{\\}}$
explicitly quantifies over strategies for all agents, we can easily enforce
that two agents _share_ a strategy by simply using the same strategy
(variable) for both. Using a slight modification of the previous translation,
we can thus handle the sharing constraints from HyperATL${}^{*}_{S}$ Beutner
and Finkbeiner (2024):

*

###  B.3. SLii and HyperSL

In this subsection, we provide addition details on the relation of SLii and
HyperSL (cf. Section 5.3).

SLii Berthon et al. (2017b) extends SL (cf. Section 5.1) by allowing
strategies that only observe parts of the system. The formal model of SLii are
game structures that are endowed with an observations. Let
$\mathcal{G}=(S,s_{0},\mathbb{A},\kappa,L)$ be a fixed game structure and let
$\mathit{Obs}$ be a fixed finite set of so-called _observations_. An
_observation family_ $\\{\sim_{o}\\}_{o\in\mathit{Obs}}$ associates an
equivalence relation $\sim_{o}\subseteq S\times S$ with each
$o\in\mathit{Obs}$.

For a strategy with observation $o$, two states $s\sim_{o}s^{\prime}$ appear
identical. This naturally extends to finite plays: Two finite plays
$p,p^{\prime}\in S^{+}$ are $o$-indistinguishable, written
$p\sim_{o}p^{\prime}$, if $|p|=|p^{\prime}|$ and for each $0\leq i<|p|$,
$p(i)\sim_{o}p^{\prime}(i)$. An _$o$ -strategy_ is a function
$f:S^{+}\to\mathbb{A}$ that cannot distinguish between $o$-indistinguishable
plays, i.e., for all $p,p^{\prime}\in S^{+}$ with $p\sim_{o}p^{\prime}$ we
have $f(p)=f(p^{\prime})$. We denote with $\mathit{Str}(\mathcal{G},o)$ the
set of all $o$-strategies in $\mathcal{G}$. We consider SLii formulas that are
generated by the following grammar:

$\displaystyle{\psi}$
$\displaystyle:=a\mid\neg{\psi}\mid{\psi}\land{\psi}\mid\operatorname{\textsf{X}}{\psi}\mid{\psi}\operatorname{\textsf{U}}{\psi}$
$\displaystyle{\varphi}$
$\displaystyle:={\psi}\mid{\varphi}\land{\varphi}\mid{\varphi}\lor{\varphi}\mid\forall
x^{o}\mathpunct{.}{\varphi}\mid\exists
x^{o}\mathpunct{.}{\varphi}\mid({\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},x){\varphi}$

where $a\in\mathit{AP}$, $x\in\mathcal{X}$,
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}$,
and $o\in\mathit{Obs}$ is an observation. Compared to SL, strategy
quantification in SLii does not range over arbitrary strategies but over
strategies that respect a given observation.

##### Semantics

The semantics of SL (cf. Section B.1) only needs to be changed in the case of
strategy quantification:

$\displaystyle s,\Delta,\Theta\models_{\mathcal{G}}\forall
x^{o}\mathpunct{.}{\varphi}$ iff $\displaystyle\forall
f\in\mathit{Str}(\mathcal{G},o)\mathpunct{.}s,\Delta[x\mapsto
f],\Theta\models_{\mathcal{G}}{\varphi}$ $\displaystyle
s,\Delta,\Theta\models_{\mathcal{G}}\exists x^{o}\mathpunct{.}{\varphi}$ iff
$\displaystyle\exists
f\in\mathit{Str}(\mathcal{G},o)\mathpunct{.}s,\Delta[x\mapsto
f],\Theta\models_{\mathcal{G}}{\varphi}$

where we restrict quantification to $o$-strategies. Given a game structure
$\mathcal{G}$, a family $\\{\sim_{o}\\}_{o\in\mathit{Obs}}$, and an SLii
formula ${\varphi}$ we write
$(\mathcal{G},\\{\sim_{o}\\}_{o\in\mathit{Obs}})\models_{\text{SL${}_{\mathit{ii}}$}}{\varphi}$
if $s_{0},\\{\\},\\{\\}\models_{\mathcal{G}}{\varphi}$ in the SLii semantics.
See Berthon et al. (2017b, 2021) for concrete examples of SLii.

##### Injective Labeling and Action Recording

To prove Section 5.3, we need to translate SLii MC instances into
equisatisfiable HyperSL instances. In order to translate the model-checking
instances, we first modify the underlying game structure. The reason for this
is simple: Strategies are defined as functions $S^{+}\to\mathbb{A}$ and
$\sim_{o}$ is defined as a direct relation on states, i.e., both are defined
directly on _components of the game structure_. In contrast, _within_ our
logic, we only observe the evaluation of the atomic propositions. In a first
step, we thus modify the game structure provided us with sufficient
information within its atomic propositions:

######  Definition 0.

A game structure $\mathcal{G}=(S,s_{0},\mathbb{A},\kappa,L)$ is _injectively
labeled_ (IL), if $L:S\to 2^{\mathit{AP}}$ is injective, i.e., two labels are
equal iff the state is equal. A game structure is _action recording_ (AR) if
for each agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}$
and every action $a\in\mathbb{A}$, there exists an atomic proposition
$\langle{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},a\rangle\in\mathit{AP}$
that holds in a state exactly when
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
played action $a$ in the last step. That is, for all $s\in S$ and all action
profile
$\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}a_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$,
we have

$\displaystyle
L\big{(}\kappa(s,\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}a_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})\big{)}\cap\\{\langle{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},a\rangle\mid{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}},a\in\mathbb{A}\\}=\bigcup_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}\\{\langle{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},a_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\rangle\\}.$

We can always ensure that $\mathcal{G}$ is injectively labeled by adding at
most $\lceil\log|S|\rceil$ fresh atomic propositions. The evaluation of all
formulas (which do not refer to these fresh propositions) remains unchanged
when adding such fresh propositions. Similarly, we can always ensure that a
structure records actions. This increases the number of states by a factor of
$|\mathbb{A}|^{|\mathit{{Agts}}|}$ but does not increase the branching in the
system, nor does it change the semantics of SLii if we extend $\sim_{o}$ to
the new states in the obvious way:

######  Lemma 0.

Given an SLii MC instance
$(\mathcal{G},\\{\sim_{o}\\}_{o\in\mathit{Obs}},{\varphi})$ there exists an
effectively computable SLii instance
$(\mathcal{G}^{\prime},\\{\sim^{\prime}_{o}\\}_{o\in\mathit{Obs}},{\varphi}^{\prime})$
where (1) $\mathcal{G}^{\prime}$ is IL and AR, and (2)
$(\mathcal{G},\\{\sim_{o}\\}_{o\in\mathit{Obs}})\models_{\text{SL${}_{\mathit{ii}}${}}}{\varphi}$
iff
$(\mathcal{G}^{\prime},\\{\sim^{\prime}_{o}\\}_{o\in\mathit{Obs}})\models_{\text{SL${}_{\mathit{ii}}${}}}{\varphi}^{\prime}$.

###### Proof.

Assume $\mathcal{G}=(S,s_{0},\mathbb{A},\kappa,L)$. Define
$\mathit{AP}^{\prime}:=\mathit{AP}\uplus\\{\langle{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},a\rangle\mid{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}},a\in\mathbb{A}\\}$.
We then define

$\displaystyle\textstyle\mathcal{G}^{\prime}=(S\times(\mathit{{Agts}}\to\mathbb{A}),(s_{0},\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}a),\mathbb{A},\kappa^{\prime},L^{\prime})$

where $a\in\mathbb{A}$ is some arbitrary action (in the initial state, we do
not need to track the last played action). For an action profile
$\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}a_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$,
we define $\kappa^{\prime}$ and $l^{\prime}$ by

$\displaystyle\kappa^{\prime}\big{(}(s,\\_),\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}a_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\big{)}$
$\displaystyle:=(\kappa(s,\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}a_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}),\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}a_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})$
$\displaystyle
L^{\prime}(s,\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}a_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i})$
$\displaystyle:=L(s)\uplus\\{\langle{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},a_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\rangle\mid{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}\\}.$

The idea behind $\mathcal{G}^{\prime}$ is that we record the action profile
that was last used in the second component of each state. In each transition,
we ignore the action profile in the current step, and record the new action
profile n the second component. In the labeling function, we can then use the
action profile
$\prod_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}}a_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
in the second component to set the APs
$\langle{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},a_{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\rangle$
for all
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}$.
We define $\\{\sim^{\prime}_{o}\\}_{o\in\mathit{Obs}}$ by

$\displaystyle\sim^{\prime}_{o}:=\Big{\\{}\big{(}(s,\\_),(s^{\prime},\\_)\big{)}\mid
s\sim_{o}s^{\prime}\Big{\\}}.$

That is, for any observation cannot distinguish states based on the second
position. In particular note that $(s,\\_)$ and $(s,\\_)$ are always
indistinguishable, i.e., all states we expanded that we added are
indistinguishable under the new observation.

It is easy to see that $\mathcal{G}^{\prime}$ is AR and that
$(\mathcal{G},\\{\sim_{o}\\}_{o\in\mathit{Obs}})\models_{\text{SL${}_{\mathit{ii}}${}}}{\varphi}$
iff
$(\mathcal{G}^{\prime},\\{\sim^{\prime}_{o}\\}_{o\in\mathit{Obs}})\models_{\text{SL${}_{\mathit{ii}}${}}}{\varphi}$.
Note that we did not change the formula. In a second step, we can ensure that
$\mathcal{G}^{\prime}$ is also IL by simply adding sufficiently many new
propositions. As those new propositions are never used in ${\varphi}$ the
semantics is unchanged. ∎

##### Identifying Indistinguishable States

In the next step, we construct a formula that identifies pairs of states that
are indistinguishable according to $\sim_{o}$. For $o\in\mathit{Obs}$, we
define formula $\mathit{ind}_{o}(\pi_{1},\pi_{2})$ as follows:

$\displaystyle\\!\\!\bigvee_{(s,s^{\prime})\in\sim_{o}}\Big{(}\bigwedge_{a\in
L(s)}a_{\pi}\land\\!\\!\\!\\!\\!\bigwedge_{a\in\mathit{AP}\setminus
L(s)}\\!\\!\\!\\!\\!\neg a_{\pi}\land\\!\\!\\!\\!\\!\bigwedge_{a\in
L(s^{\prime})}a_{\pi^{\prime}}\land\\!\\!\\!\\!\\!\bigwedge_{a\in\mathit{AP}\setminus
L(s^{\prime})}\\!\\!\\!\\!\\!\neg a_{\pi^{\prime}}\Big{)}$

It is easy to see that on any injectively labeled game structure
$\mathit{ind}_{o}(\pi_{1},\pi_{2})$ holds if the two paths bound to
$\pi_{1},\pi_{2}$ are $\sim_{o}$-related in their first state.

##### Enforcing Partial Information

Given an observation $o\in\mathit{Obs}$, and strategy variable $x$, we define
a formula $\mathit{indStrat}_{o}(x)$ that holds on a strategy iff this
strategy is an $o$-strategy (in all reachable situations and for all agents)
as follows:

$\displaystyle\mathit{indStrat}_{o}(x)$ $\displaystyle:=\forall
y_{1},\ldots,y_{n},y^{\prime}_{1},\ldots,y^{\prime}_{n}.$
$\displaystyle\bigwedge_{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}=1}^{n}{\psi}^{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}}_{o}\left[\begin{matrix}\pi_{1}:(y_{1},\ldots,y_{i-1},x,y_{i+1},\ldots,y_{n})\\\
\pi_{2}:(y^{\prime}_{1},\ldots,y^{\prime}_{i-1},x,y^{\prime}_{i+1},\ldots,y^{\prime}_{n})\end{matrix}\right]$

where

$\displaystyle{\psi}_{o}^{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}}:=\Big{(}\operatorname{\textsf{X}}\Big{(}\bigwedge_{a\in\mathbb{A}}$
$\displaystyle\langle{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},a\rangle_{\pi_{1}}\leftrightarrow\langle{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i},a\rangle_{\pi_{2}}\Big{)}\Big{)}\operatorname{\textsf{W}}\Big{(}\neg\mathit{ind}_{o}(\pi_{1},\pi_{2})\Big{)}.$

The path formula
${\psi}_{o}^{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}}$
compares two paths $\pi_{1},\pi_{2}$ and states that as long as a prefix on
those to paths is $o$-indistinguishable (i.e.,
$\mathit{ind}_{o}(\pi_{1},\pi_{2})$ holds in each step), the action selected
by agent
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
is the same on both paths (using the fact that the structure records actions).
As we do not know which agents might end up playing strategy $x$ we assert
that $x$ behaves as a $o$-strategy for all agents. For each
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}\in\mathit{{Agts}}$
we thus compare two paths where
${\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}$
plays $x$, but all other agents play some arbitrary strategy, and assert that
${\psi}_{o}^{{\color[rgb]{0.2890625,0.1875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.2890625,0.1875,0.46875}i}}$
holds for those two paths. Strategy $x$ must thus respond to two
$o$-indistinguishable prefixes with the same action in all reachable
situations for all agents.

##### The Translation

Using $\mathit{indStrat}_{o}(x)$ as a building block, we can modify the
translation of SL into HyperSL from Section B.1, and instead translate the
much stronger SLii.

*

###### Proof.

In a first step, we use Lemma 16 to ensure that $\mathcal{G}$ is IL and AR. We
can then translate $\varphi$ using a similar translation to the one used in
Section B.1. The only cases that require changening are the translation of
quantification:

$\displaystyle{\llparenthesis}\forall
x^{o}.{\varphi}{\rrparenthesis}^{\@vec{x}}$ $\displaystyle:=\forall