ifaamas [AAMAS ’23]Proc. of the 22nd International Conference on Autonomous
Agents and Multiagent Systems (AAMAS 2023)May 29 – June 2, 2023 London, United
KingdomA. Ricci, W. Yeoh, N. Agmon, B. An (eds.) 2023 2023 877
Interdisciplinary Centre for Security and Trust, SnT,
University of Luxembourg Institute of Computer Science, Polish Academy of
Sciences and SnT, University of Luxembourg

# Playing to Learn, or to Keep Secret:
Alternating-Time Logic Meets Information Theory

Masoud Tabatabaei<EMAIL_ADDRESS>and  Wojciech Jamroga
<EMAIL_ADDRESS>
###### Abstract.

Many important properties of multi-agent systems refer to the participants’
ability to achieve a given goal, or to prevent the system from an undesirable
event. Among intelligent agents, the goals are often of epistemic nature,
i.e., concern the ability to obtain knowledge about an important fact
$\varphi$. Such properties can be e.g. expressed in , that is, alternating-
time temporal logic ATL${}_{\textup{{}}}$ extended with epistemic operators.
In many realistic scenarios, however, players do not need to fully learn the
truth value of $\varphi$. They may be almost as well off by gaining _some_
knowledge; in other words, by reducing their uncertainty about $\varphi$.
Similarly, in order to keep $\varphi$ secret, it is often insufficient that
the intruder never fully learns its truth value. Instead, one needs to require
that his uncertainty about $\varphi$ never drops below a reasonable threshold.

With this motivation in mind, we introduce the logic , extending
ATL${}_{\textup{{}}}$ with quantitative modalities based on the Hartley
measure of uncertainty. The new logic enables to specify agents’ abilities
w.r.t. the uncertainty of a given player about a given set of statements. It
turns out that has the same expressivity and model checking complexity as .
However, the new logic is exponentially more succinct than , which is the main
technical result of this paper.

###### Key words and phrases:

Multiagent Systems, Knowledge Representation, Uncertainty

##  1\. Introduction

Many important properties of multi-agent systems refer to _strategic
abilities_ of agents and their groups Bulling et al. (2015); Ågotnes et al.
(2015). They can be formalized in logics of strategic ability, such as
alternating-time temporal logic ATL Alur et al. (2002); Schobbens (2004) or
strategy logic SL Chatterjee et al. (2007); Mogavero et al. (2010). For
example, the ATL formula
$\langle\\!\langle{taxi}\rangle\\!\rangle_{{}_{\\!\mathit{}}}F\mathsf{{destination}}$,
built upon the strategic operator
$\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\varphi$ for “there
is a strategy for $A$ such that $\varphi$ holds” and the temporal modality $F$
(“eventually”), can be used to express that the autonomous cab can deliver the
passenger to his/her destination. Similarly,
$\langle\\!\langle{passg}\rangle\\!\rangle_{{}_{\\!\mathit{}}}(\lnot\mathsf{{dead}})\,\mathcal{U}\,\mathsf{{destination}}$
says that the passenger has the ability to survive the ride alive. Such
statements allow to express important functionality and safety requirements in
a simple and intuitive way. Moreover, they provide input to algorithms and
tools for verification, that have been in constant development for over 20
years Alur et al. (1998, 2001); Kacprzak and Penczek (2004); Lomuscio and
Raimondi (2006); Chen et al. (2013); Busard et al. (2014); Pilecki et al.
(2014); Huang and van der Meyden (2014); Cermak et al. (2014); Lomuscio et al.
(2017); Cermák et al. (2015); Belardinelli et al. (2017, 2017); Jamroga et al.
(2019a); Kurpiewski et al. (2019); Kurpiewski et al. (2021).

Knowledge and information has always been an important aspect of interaction,
but it has become even more important with the emergence of Internet and, more
recently, social networks. Information is an important resource on which
strategies are built, e.g., it is widely acknowledged that executable
strategies must comply with so called uniformity constraints Schobbens (2004);
Jamroga and van der Hoek (2004). More and more often, information becomes also
the _goal_ of the interaction. Agents may play to _learn_ about a particular
subject. People strive to know what the state of the economy is, what is the
latest clothing fashion, and whether the coffee machine at their workplace
serves good espresso or not. Using strategic-epistemic specifications that
involve the knowledge operator $K_{a}$, the latter kind of ability can be
expressed by
$\langle\\!\langle{worker}\rangle\\!\rangle_{{}_{\\!\mathit{}}}F(K_{worker}\mathsf{{good}}\lor
K_{worker}\neg\mathsf{{good}})$. Dually, the user of a social network may want
to post a message for their friends only, in which case no outsider should
learn the content of the message. This kind of ability can be captured by
$\langle\\!\langle{user}\rangle\\!\rangle_{{}_{\\!\mathit{}}}G\neg(K_{outsider}\mathsf{{post=m}}\lor
K_{outsider}\mathsf{{post\neq m}})$.

In many cases, however, strategic-epistemic specifications are too coarse. It
is great if the worker can obtain full knowledge about the quality of
workplace espresso, but being _almost sure_ is almost as good. Dually, leaking
_some_ information about the social network post can be damaging, even if the
intruder does not learn its exact content. With this motivation in mind, we
propose to extend alternating-time temporal logic with new, information-
theoretic modalities $\mathcal{H}$, based on the Hartley measure of
uncertainty Hartley (1928). We also demonstrate the usefulness of the
framework on a real-life voting scenario.

In terms of technical results, we prove that the resulting logic has the same
expressive power and model checking complexity as strategic-epistemic
specifications; however, it is exponentially more succinct. This is an
important result, as it shows that the verification of a given _property_ with
uncertainty operators can take exponentially less time than when one uses
knowledge modalities.

Related work. Strategic-epistemic reasoning has been intensively studied in
the early 2000s, especially within the framework of ATEL van der Hoek and
Wooldridge (2002, 2003a, 2003b); Ågotnes (2006); Jamroga and Ågotnes (2007)
and Dynamic Epistemic Logic van Ditmarsch et al. (2007); Ågotnes and van
Ditmarsch (2008). Dynamic epistemic planning Bolander and Birkegaard Andersen
(2011) is a particularly relevant example. Still, we are not aware of any
works combining logical formalizations of strategic reasoning with
information-theoretic properties. The paper Jamroga and Tabatabaei (2013)
comes closest, as it discusses the relation between a variant of resource-
bounded temporal-epistemic logic and Hartley measure. Moreover, our proposal
is directly inspired by information-theoretic notions of security, cf. Katz
and Lindell (2020) for an introduction.

Another strand of related works concerns quantitative specification and
verification of MAS due to stochastic interaction Chen and Lu (2007); Huang et
al. (2012), graded Aminof et al. (2018); Ferrante et al. (2008) and fuzzy
strategic modalities Bouyer et al. (2019); Belardinelli et al. (2022), or
probabilistic beliefs about the opponents’ response Bulling and Jamroga
(2009). Those papers considered neither knowledge nor information-theoretic
properties, though Ferrante et al. (2008) leaned in that direction by
including a count over the accessible imperfect worlds.

Succinctness of logical representations has been studied since early 1970s
Stockmeyer (1972). In particular, the relative succinctness of branching-time
logics was investigated in Wilke (1999); Adler and Immerman (2001); Markey
(2003), and Bozzelli et al. (2020) studied the succinctness of the strategic
logic ATL* with past-time operators. The methodology of proving succinctness
by means of _formula size games_ was proposed in Adler and Immerman (2001),
and later generalized in French et al. (2013). We adapt the latter approach to
obtain our main technical result here.

##  2\. Logics of Strategic Ability

We first recapitulate the logical foundations that we chose for our approach.

###  2.1. Alternating-Time Logic ATL

_Alternating-time temporal logic_ ATL Alur et al. (1997, 2002); Schobbens
(2004) generalizes the branching-time temporal logic CTL Emerson (1990) by
replacing the path quantifiers $\mathsf{E},\mathsf{A}$ with _strategic
modalities_ $\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}$.
Informally, $\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\gamma$
says that a group of agents $A$ has a collective strategy to enforce temporal
property $\gamma$. ATL formulas can include temporal operators: “$X$” (“in the
next state”), “$G$” (“always from now on”), “$F$” (“now or sometime in the
future”), and $\,\mathcal{U}\,$ (strong “until”).

Syntax. Formally, let $\mathit{Agt}$ be a finite set of agents, and
$\mathit{Prop}$ a countable set of atomic propositions. The language of ATL is
defined as follows:

$\varphi::=\mathsf{{p}}\mid\neg\varphi\mid\varphi\wedge\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}X\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}G\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\varphi\,\mathcal{U}\,\varphi$.

where $A\subseteq\mathit{Agt}$ and $\mathsf{{p}}\in\mathit{Prop}$. Derived
boolean connectives and constants ($\lor,\top,\bot$) are defined as usual.
“Sometime” is defined as $F\varphi\equiv\top\,\mathcal{U}\,\varphi$.

###  2.2. Semantics of ATL

Models. The semantics of ATL is defined over a variant of synchronous multi-
agent transition systems. Let
$S=\\{{\mathit{Agt},St,\mathit{Act},d,\mathit{out}}\\}$ be a concurrent game
structure (CGS) such that: $\mathit{Agt}=\\{{1,...,k}\\}$ is a set of agents
(or players), $St$ is the set of states of the system, $\mathit{act}$ is a set
of actions, $d:\mathit{Agt}\times St\rightarrow
2^{\mathit{Act}}\setminus\\{{\emptyset}\\}$ shows what actions are available
for each player in each state, and
$\mathit{out}:St\times\mathit{Act}^{1}\times...\times\mathit{Act}^{k}\rightarrow
St$ is the transition function which, given a state and one action from each
player in that state, returns the resulting sate. A CGS together with a set of
atomic propositions $\mathit{Pv}$ and a valuation function
$\mathit{V}:\mathit{Pv}\rightarrow 2^{St}$ is called a concurrent game model
(CGM). A _pointed CGM_ is a pair $(M,q_{0})$ consisting of a concurrent game
model $M$ and an initial state $q_{0}$ in $M$.

Strategies and their outcomes. Given a CGS, we define the strategies and their
outcomes as follows. A _strategy_ for $a\in\mathit{Agt}$ is a function
$s_{a}:St\rightarrow\mathit{Act}$ such that $s_{a}(q)\in d(a,q)$.111 This
corresponds to the notion of _memoryless_ or _positional_ strategies. In other
words, we assume that the memory of agents is explicitly defined by the states
of the model.  The set of such strategies is sometimes denoted by
$\Sigma_{a}^{Ir}$, with the capital “I” referring to perfect Information, and
the lowercase “r” for possibly imperfect recall. A _collective strategy_ for a
group of agents $A=\\{{a_{1},\ldots,a_{r}}\\}$ is a tuple of individual
strategies $s_{A}=\langle{s_{a_{1}},\ldots,s_{a_{r}}}\rangle$. The set of such
strategies is denoted by $\Sigma_{A}^{Ir}$.

A _path_ $\lambda=q_{0}q_{1}q_{2}\dots$ in a CGS is an infinite sequence of
states such that there is a transition between each $q_{i}$ and $q_{i+1}$.
$\lambda[i]$ denotes the $i$th position on $\lambda$ (starting from $i=0$) and
$\lambda[i,\infty]$ the suffix of $\lambda$ starting with $i$. The “outcome”
function $out(q,s_{A})$ returns the set of all paths that can occur when
agents $A$ execute strategy $s_{A}$ from state $q$ onward, defined as follows:

$out(q,s_{A})=$:

$\\{\lambda=q_{0},q_{1},q_{2}\ldots\mid q_{0}=q$ and for each $i=0,1,\ldots$
there exists $\langle{\alpha^{i}_{a_{1}},\ldots,\alpha^{i}_{a_{k}}}\rangle$
such that $\alpha^{i}_{a}\in d_{a}(q_{i})$ for every $a\in\mathit{Agt}$, and
$\alpha^{i}_{a}=s_{A}[a](q_{i})$ for every $a\in A$, and
$q_{i+1}=o(q_{i},\alpha^{i}_{a_{1}},\ldots,\alpha^{i}_{a_{k}})\\}$.

Semantic clauses. The semantics of ATL is defined by the following clauses:

$M,q\state\models\mathsf{{p}}$:

iff $q\in V(\mathsf{{p}})$, for $\mathsf{{p}}\in\mathit{Prop}$;

$M,q\state\models\neg\varphi$:

iff $M,\state\not\models\varphi$;

$M,q\state\models\varphi_{1}\wedge\varphi_{2}$:

iff $M,q\models\varphi_{1}$ and $M,q\models\varphi_{2}$;

$M,q\models\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}X\varphi$:

iff there is a strategy $s_{A}\in\Sigma_{A}^{Ir}$ such that, for each path
$\lambda\in out(q,s_{A})$, we have $M,\lambda[1]\models\varphi$.

$M,q\models\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}G\varphi$:

iff there is a strategy $s_{A}\in\Sigma_{A}^{Ir}$ such that, for each path
$\lambda\in out(q,s_{A})$, we have $M,\lambda[i]\models\varphi$ for all $i\geq
0$.

$M,q\models\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\varphi_{1}\,\mathcal{U}\,\varphi_{2}$:

iff there is a strategy $s_{A}\in\Sigma_{A}^{Ir}$ such that, for each path
$\lambda\in out(q,s_{A})$, we have $M,\lambda[i]\models\varphi_{2}$ for some
$i\geq 0$ and $M,\lambda[j]\models\varphi_{1}$ for all $0\leq j<i$.

###  2.3. Imperfect Information and Knowledge

Realistic multi-agent interaction always includes some degree of limited
observability. Here, we use the classical variant of “ATL with imperfect
information”, defined as follows:

We extend concurrent game structures with indistinguishability relations
$\sim_{a}$, for each $a\in\mathit{Agt}$. The resulting structure
$S=\\{{\mathit{Agt},St,\\{{\sim_{a}\mid
a\in\mathit{Agt}}\\},\mathit{Act},d,\mathit{out}}\\}$ is called a concurrent
epistemic game structure (CEGS). A CEGS together with a set of atomic
propositions $\mathit{Pv}$ and a valuation function
$\mathit{V}:\mathit{Pv}\rightarrow 2^{St}$ is called a concurrent epistemic
game model CEGM.

Strategies of agents must specify identical choices in indistinguishable
situations. That is, strategies with imperfect information (ir strategies, for
short) are functions $s_{a}:St\to Act$ such that (1) $s_{a}(q)\in d(a,q)$, and
(2) if $q\sim_{a}q^{\prime}$ then $s_{a}(q)=s_{a}(q^{\prime})$. 222Again, we
consider only positional strategies here. As before, collective strategies for
$A\subseteq\mathit{Agt}$ are tuples of individual strategies for $a\in A$. We
denote the set of $A$’s imperfect information strategies by $\Sigma_{A}^{ir}$
(with the lowercase “i” for imperfect information).

The semantics of “ATL with imperfect information” ($\textbf{ATL}_{ir}$)
differs from the one presented in Section 2.1 only in that the strategies are
taken from $\Sigma_{A}^{ir}$ instead of $\Sigma_{A}^{Ir}$. In other words, the
agents in $A$ should have an executable strategy which enforces $\varphi$ from
all the states that at least one member of the coalition considers possible.

Alternating-time temporal epistemic logic ATLK adds the knowledge modality of
the multi-agent epistemic logic to ATL with imperfect information. In multi-
agent epistemic logic, expressing the _knowledge_ of the agents is formalised
by epistemic formulae of type $\mathcal{K}_{a}\varphi$, stating that agent $a$
_knows that $\varphi$ holds_, with the following semantics:

:

$M,q\models\mathcal{K}_{a}\varphi$ iff, for every state $q^{\prime}$ such that
$q\sim_{a}q^{\prime}$, we have that $M,q^{\prime}\models\varphi$.

The formula stating mutual knowledge $E_{A}\varphi$ (read ”everybody in $A$
knows that $\varphi$”) is defined as:

$M,q\models E_{A}\varphi$ iff $M,q\models\mathcal{K}_{a}\varphi$, for all
$a\in A$.

##  3\. Motivating Example

In this section we show, using an example, how our proposed logic can express
more refined epistemic goals of agents using considerably more concise
formulas. As we will see, not only the new formulation of these epistemic
properties will be significantly shorter; the interpretation of the formulas
will also be easier to understand in comparison to their analogous formulas in
.

###  3.1. Coercion in Referendums

We consider a very simple scenario of an election with a single voter and a
single coercer. The election is a referendum, in the sense that each voter has
to either vote for an issue in question or to vote against it. We consider two
variants. In the first one there is only one issue put for referendum (we call
it proposal A). The model consists of two agents, the voter $v$ and the
coercer $c$. The set of possible actions for the coercer in the model is
$\\{{\epsilon}\\}$ and for the voter is
$\\{{voteA,vote\overline{A},\epsilon}\\}$, where $\epsilon$ represents a null
action (meaning the action of doing nothing). $voteA$ and $vote\overline{A}$
respectively represent voting for and against the proposal $A$. The atomic
proposition $V_{A}$ states that the vote is cast in favor of proposal $A$,
while the atomic proposition $Voted$ shows that the vote is already cast. The
game model is depicted in Figure 1.

$s_{0}$$s_{1}$$s_{2}$$\lnot Voted\,,\,\lnot
V_{A}$$Voted\,,\,V_{A}$$Voted\,,\,\lnot V_{A}$ voteA, $\epsilon$ $\epsilon$,
$\epsilon$ $vote\overline{A},\epsilon$ C$\epsilon$, $\epsilon$$\epsilon$,
$\epsilon$

Figure 1. Single issue referendum with one voter and one coercer

The valuations of atomic propositions are depicted in blue, and the red dashed
line between $s_{1}$ and $s_{2}$ shows that the these two states are
indistinguishable for player $c$. In this simple model, we might express the
property of coercion resistance in as follows:

$\displaystyle M,s_{0}$
$\displaystyle\models\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}F(Voted\wedge
V_{A}\wedge G\lnot(\mathcal{K}_{c}V_{A}\vee\mathcal{K}_{c}\lnot V_{A}))$
$\displaystyle\wedge$
$\displaystyle\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}F(Voted\wedge\lnot
V_{A}\wedge G\lnot(\mathcal{K}_{c}V_{A}\vee\mathcal{K}_{c}\lnot V_{A}))$

The formula states that the voter has a strategy to vote for the proposal $A$
or against it, in a way that in either case the coercer does not know the
value of the vote.

###  3.2. Referendum with Multiple Proposals

Consider a more sophisticated variant in which the voter participates in a
double referendum, i.e., votes on two proposals $A$ and $B$ on a single
ballot. The set of atomic propositions in this scenario is
$\\{{Voted,V_{A},V_{B}}\\}$ and the set of actions for the voter
is$\\{{voteAB,vote\overline{AB},voteA\overline{B},vote\overline{B}A}\\}$. For
expressing the property of coercion resistance in this scenario, a seemingly
reasonable way is to extend the above formulas as below:

$\displaystyle M,s_{0}$
$\displaystyle\models\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}F(Voted\wedge
V_{A}\wedge V_{B}\wedge$ $\displaystyle\qquad
G\lnot(\mathcal{K}_{c}V_{A}\vee\mathcal{K}_{c}\lnot
V_{A}\vee\mathcal{K}_{c}V_{B}\vee\mathcal{K}_{c}\lnot V_{B}))$
$\displaystyle\wedge\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}F(Voted\wedge
V_{A}\wedge\lnot V_{B}\wedge$ $\displaystyle\qquad
G\lnot(\mathcal{K}_{c}V_{A}\vee\mathcal{K}_{c}\lnot
V_{A}\vee\mathcal{K}_{c}V_{B}\vee\mathcal{K}_{c}\lnot V_{B}))$
$\displaystyle\wedge\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}F(Voted\wedge\lnot
V_{A}\wedge V_{B}\wedge$ $\displaystyle\qquad
G\lnot(\mathcal{K}_{c}V_{A}\vee\mathcal{K}_{c}\lnot
V_{A}\vee\mathcal{K}_{c}V_{B}\vee\mathcal{K}_{c}\lnot V_{B}))$
$\displaystyle\wedge\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}F(Voted\wedge\lnot
V_{A}\wedge\lnot V_{B}\wedge$ $\displaystyle\qquad
G\lnot(\mathcal{K}_{c}V_{A}\vee\mathcal{K}_{c}\lnot
V_{A}\vee\mathcal{K}_{c}V_{B}\vee\mathcal{K}_{c}\lnot V_{B}))$

The formula states that the voter can vote in any combination, for or against
$A$ or $B$, without the coercer knowing the value of any single vote. At the
first glance these security properties seem to be strong enough for capturing
the desirable property of coercion resistance. However, if we look at the two
models in Figure 2, both of them satisfy the property above. On the other
hand, we would consider model $M_{1}$ less secure than $M_{2}$. There are 4
possible combinations of the valuations of $V_{A}$ and $V_{B}$. In $M_{2}$,
the coercer considers all 4 of them as plausible, but in $M_{1}$ he could
narrow that down to only two possible combinations. In other words, the
uncertainty of the coercer about propositions $V_{A}$ and $V_{B}$ is higher in
$M_{2}$ than in $M_{1}$. In fact, as we shall see later, it is possible to
write a formula in the language of $\ATLK$ that keeps the above property and
yet distinguishes $M_{1}$ and $M_{2}$. But if we want to write a security
property in that rejects all the models where the coercer has more
distinguishing power over states $s_{1}$ to $s_{4}$ than the model $M_{2}$,
then the length of that formula would be very large – in the worst case, even
exponential in the number of distinguishing properties.

$s_{0}$$s_{2}$$s_{3}$$s_{1}$$s_{4}$$\lnot Voted\,,\,\lnot V_{A}\,,\,\lnot
V_{B}$$Voted\,,\,V_{A}\,,\,\lnot V_{B}$$Voted\,,\,\lnot
V_{A}\,,\,V_{B}$$Voted\,,\,V_{A}\,,\,V_{B}$$Voted\,,\,\lnot V_{A}\,,\,\lnot
V_{B}$$\epsilon$, $\epsilon$ $voteA\overline{B}\,,\,\epsilon$
$vote\overline{A}B\,,\,\epsilon$
$voteAB\,,\,\epsilon$$vote\overline{AB}\,,\,\epsilon$CC$\epsilon$,
$\epsilon$$\epsilon$, $\epsilon$$\epsilon$, $\epsilon$$\epsilon$, $\epsilon$

(a) $M_{1}$

$s_{0}$$s_{2}$$s_{3}$$s_{1}$$s_{4}$$\lnot Voted\,,\,\lnot V_{A}\,,\,\lnot
V_{B}$$Voted\,,\,V_{A}\,,\,\lnot V_{B}$$Voted\,,\,\lnot
V_{A}\,,\,V_{B}$$Voted\,,\,V_{A}\,,\,V_{B}$$Voted\,,\,\lnot V_{A}\,,\,\lnot
V_{B}$$\epsilon$, $\epsilon$ $voteA\overline{B}\,,\,\epsilon$
$vote\overline{A}B\,,\,\epsilon$
$voteAB\,,\,\epsilon$$vote\overline{AB}\,,\,\epsilon$CCC$\epsilon$,
$\epsilon$$\epsilon$, $\epsilon$$\epsilon$, $\epsilon$$\epsilon$, $\epsilon$

(b) $M_{2}$

Figure 2. Double referendum with one voter and one coercer. Model $M_{1}$
depicts a scenario which is less secure than $M2$

###  3.3. Reasoning about Uncertainty

One way of looking at the above situation is that, when reaching any of the
states $s_{1}$ to $s_{4}$, we want the coercer to have the least amount of
information, or in other words the maximum uncertainty about the possible
values of $V_{A}$ and $V_{B}$. To express this concept, we can use one of the
well known quantitative measures of uncertainty. Two measures that come to
mind are Shannon entropy and Hartley measure. Choosing Shannon entropy would
be meaningful only if we knew the intrinsic probabilities of each state.
However, in the models that we are using, and in the scenarios similar to the
one above, what we are interested is the uncertainty of the agents about
different possible outcomes of a set of properties (here $V_{A}$ and $V_{B}$).
We recall the definition of Hartley measure below:

######  Definition  (Hartley measure of uncertainty Hartley (1928)).

If $A$ is a set of possible outcomes, then its Hartley measure is defined by
$H(A)=\log|A|$.

The Hartley function coincides with Shannon entropy when ignorance can be
modeled by the uniform probability distribution. Using this measure, what we
want to specify as a security property in the example above is that the
uncertainty of the coercer about the values of $V_{A}$ and $V_{B}$ should be
maximal. The set of properties of interest $\\{{V_{A},V_{B}}\\}$ could have
$2^{2}=4$ different combinations of values. Therefore if we want that the
coercer considers all of these combinations as possible, the Hartley measure
of uncertainty of the coercer would be $\log 4=2$ bits. To express this, we
add a new operator $\mathcal{H}$, and write the formula:

$\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}F(Voted\wedge\mathcal{H}^{\geq
2}_{c}\\{{V_{A},V_{B}}\\})$

The formula states that the voter has a strategic ability to eventually cast
her vote, while keeping the uncertainty of the coercer about the valuations of
$V_{A}$ and $V_{B}$ at the level of at least 2 bits. Intuitively, the formula
holds in state $s_{1}$ of model $M_{2}$, but not $M_{1}$.

In the next section, we use this idea to formalize the syntax and semantics of
the logic $\ATLH$.

##  4\. ATL with Uncertainty

In this section we define the syntax and semantics of the logic of strategic
abilities with uncertainty operator $\ATLH$. The logic is based on the idea of
using the Hartley measure to quantify the uncertainty of agents about the
possible valuations of a set of formulas. Similarly to $\ATLK$, the semantics
of is also defined with respect to concurrent epistemic game models (CEGM).

###  4.1. Syntax

The syntax of $\ATLH$ is given as follows:

$\varphi::=\mathsf{{p}}\mid\neg\varphi\mid\varphi\wedge\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}X\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}G\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\varphi\,\mathcal{U}\,\varphi\mid\mathcal{H}_{a}^{\otimes\,m}\beta$.

where $A\in 2^{\mathit{Agt}}$ is a set of players, $\beta\in
2^{\varphi}\setminus\\{{\emptyset}\\}$ is a set of formulas,
$a\in\mathit{Agt}$ is a player, and $\otimes\in\\{{<,\leq,>,\geq,=}\\}$ is a
comparison operator. For instance, the formula $\mathcal{H}_{a}^{>m}\beta$
states that the the uncertainty of agent $a$ about the set of formulas $\beta$
is higher than $m$.

###  4.2. Semantics

Let $[q]_{\sim_{a}}=\\{{q^{\prime}\in St\ \mid\ q^{\prime}\sim_{a}q}\\}$
denote the abstraction class of state $q\in St$ with respect to relation
$\sim_{a}$, i.e., the epistemic neighbourhood of $q$ from the perspective of
agent $a\in\mathit{Agt}$. For a given formula $\varphi$, we define relation
$\sim^{\varphi}\in St\times St$ that connects states with the same valuation
of $\varphi$:

$q_{1}\sim^{\varphi}q_{2}\ \text{iff}\ M,q_{1}\models\varphi\Leftrightarrow
M,q_{2}\models\varphi$.

If $\beta=\\{{\varphi_{1},...,\varphi_{n}}\\}$ is a set of formulas and
$a\in\mathit{Agt}$, then we define

$\sim^{\beta}_{a}=\sim_{a}\cap\bigcap^{n}_{i=1}\sim^{\varphi_{i}}$

I.e., $q_{1}\sim^{\beta}_{a}q_{2}$ iff $q_{1},q_{2}$ look the same to $a$ and
cannot be discerned by any formula in $\beta$. Note that $\sim^{\beta}_{a}$ is
an equivalence. We define

$\mathit{R}_{a,q}(\beta)=\\{{[q^{\prime}]_{\sim_{a}^{\beta}}\ \mid\
q^{\prime}\sim_{a}q}\\}$

for the set of equivalence classes of $\sim_{a}^{\beta}$ contained in the
epistemic neighbourhood of state $q$. Then, the truth value of the statement
“agent $a$’s uncertainty about the set of formulas $\beta$ is in $\otimes$
relation to value $m\in\mathbb{R}$” can be defined as follows:

$M,q\models\mathcal{H}^{\otimes m}_{a}\beta,\ \text{iff}\
\log|\mathit{R}_{a,q}(\beta)|\otimes m$

Some straightforward validities of are:

  1. (1)

$\mathcal{H}_{a}^{\begin{subarray}{c}=m\\\ \geqslant m\\\
>m\end{subarray}}\beta\rightarrow\mathcal{H}_{a}^{\begin{subarray}{c}\geqslant
m\\\ \geqslant m\\\ >m\end{subarray}}\beta^{\prime}$, for all
$\beta\subseteq\beta^{\prime}$;

  2. (2)

$\mathcal{H}_{a}^{\begin{subarray}{c}<m\\\ \leqslant m\\\
=m\end{subarray}}\beta\rightarrow\mathcal{H}_{a}^{\begin{subarray}{c}<m\\\
\leqslant m\\\ \leqslant m\end{subarray}}\beta^{\prime}$, for all
$\beta\subseteq\beta^{\prime}$.

Also, if $|St|$ is the number of states in the model, then it holds that
$M,q\models\mathcal{H}_{a}^{<\min(|\beta|,\log(|St|))}\beta$.

###  4.3. Model Checking

In this section, we discuss model checking for . The following results have
long been known in the literature:

  * •

Model checking of epistemic logic is in P with respect to the size of the
model and the length of the formula Halpern and Vardi (1991).

  * •

Model checking of for agents with ir strategies is
$\mathbf{{\Delta_{{2}}^{\mathbf{{P}}}}}$-complete with respect to size of the
model and the length of the formula Bulling et al. (2010). This is a direct
consequence of the fact that model checking of $\textbf{ATL}_{ir}$ is
$\mathbf{{\Delta_{{2}}^{\mathbf{{P}}}}}$-complete Schobbens (2004); Jamroga
and Dix (2006).

In the following, we show that model checking of is also
$\mathbf{{\Delta_{{2}}^{\mathbf{{P}}}}}$-complete. To this end, it suffices to
show that model checking of the uncertainty part of the language is in P.

###### Proposition

If $\varphi$ is an formula without strategic and temporal operators and $M$ is
a CEGM, then checking if $\varphi$ is satisfied in a state $q$ of $M$ can be
done in polynomial time with respect to $|\varphi|$ and $|M|$, where $|M|$ is
the total number of states, transitions, and epistemic relation pairs in $M$.

###### Proof.

Let $\varphi_{1},\varphi_{2},...\varphi_{k}$ be the subformulas of $\varphi$
(which incrementally generate $\varphi$) listed in order of length. We can see
that $k\leq|\varphi|$, as there are at most $|\varphi|$ subformulas of
$\varphi$. We start labeling each state in $M$ in increasing order of $i$,
with labels $\varphi_{i}$ or $\lnot\varphi_{i}$, depending on whether
$\varphi_{i}$ is true in that state or not. It is easy to see that we can do
this in at most $\mathbf{O}(k|M|)$ labeling step. If the formula $\varphi_{i}$
is a propositional formula with respect to it’s subformulas, then it can be
labeled in in each state in constant time. In cases where $\varphi_{i}$ is of
the form $\mathcal{H}_{a}^{\otimes m}\beta$ where $\otimes\in\\{{<,>,=}\\}$
and $\beta=\\{{\alpha_{1},...\alpha_{k^{\prime}}}\\}$, we have that each
$\alpha_{j}$ is a subformula of $\varphi_{i}$. Therefore for labeling
$\varphi_{i}$ we construct the set of equivalence classes
$\mathit{R}_{a,q}(\beta)$ by checking the $k^{\prime}$ labels of formulas in
$\beta$ in all the states $q^{\prime}$ where $q^{\prime}\sim_{a}q$. Then we
calculate $\log|\mathit{R}_{a,q}(\beta)|$ and compare it with $m$ in order to
label $\varphi_{i}$. This procedure can be done in at most
$\mathbf{O}(k^{\prime}|M|)$ steps. Therefore the whole process of checking
whether $\varphi$ is satisfied in a state $q$ or not can be done in at most
$\mathbf{O}({|\varphi|}^{2}{|M|}^{2})$. ∎

###### Proposition

Model checking of for agents with ir strategies is
$\mathbf{{\Delta_{{2}}^{\mathbf{{P}}}}}$-complete with respect to size of the
model and the length of the formula.

###### Proof.

The lower bound follows from the fact that subsumes $\textbf{ATL}_{ir}$, and
model checking $\textbf{ATL}_{ir}$ is
$\mathbf{{\Delta_{{2}}^{\mathbf{{P}}}}}$-hard. The upper bound is
straightforward from Proposition 4.3 and the fact that model checking
$\textbf{ATL}_{ir}$ is in $\mathbf{{\Delta_{{2}}^{\mathbf{{P}}}}}$. ∎

##  5\. Expressive Power of

In this section we show that $\ATLH$ and ATLK have the same expressive power.
We start by recalling the semantic definition of comparative expressivity Wang
and Dechesne (2009).

######  Definition  (Expressivity).

Let $L_{1}=\langle\varPhi_{1},\models_{1},\mathbb{M}\rangle$ and
$L_{1}=\langle\varPhi_{2},\models_{2},\mathbb{M}\rangle$ represents two
logics, such that $\varPhi_{1}$ and $\varPhi_{2}$ are the set of formulas
defined in these logics, $\mathbb{M}$ is a nonempty class of models (or
pointed models) over which the logics are defined, and $\models_{1}$ and
$\models_{2}$ are the truth relations of these logics, such that
$\models_{1}\subseteq\mathbb{M}\times\varPhi_{1}$ and
$\models_{2}\subseteq\mathbb{M}\times\varPhi_{2}$. We say that $L_{2}$ is at
least as expressive as $L_{1}$ on the class of models $\mathbb{M}$, iff for
every formula $\varphi_{1}\in\varPhi_{1}$, there exists a formula
$\varphi_{2}\in\varPhi_{2}$ such that for every $M\in\mathbb{M}$ we have
$M\models_{1}\varphi_{1}$ iff $M\models_{2}\varphi_{2}$. We will write it as
$L_{1}\leqslant_{\mathbb{M}}L_{2}$.

If both $L_{1}\leqslant_{\mathbb{M}}L_{2}$ and
$L_{2}\leqslant_{\mathbb{M}}L_{1}$, then we say that $L_{1}$ and $L_{2}$ are
equally expressive on $\mathbb{M}$, and write $L_{1}=_{\mathbb{M}}L_{2}$.

In the following, we use $\models_{\mathcal{K}}$ and $\models_{\mathcal{H}}$
to denote the semantic relation of ATLK and $\ATLH$, respectively, whenever it
might not be clear from the context.

###  5.1. Knowledge as Uncertainty

$\ATLH$ is at least as expressive as ATLK.

###### Proof.

Because the set of formulas defined in $\ATLH$ includes all the formulas
defined in ATLK except the formulas including $\mathcal{K}$ operator, and the
semantics of the common formulas are similar in both logics, it suffices to
prove that for any formula of type $\varphi_{1}=\mathcal{K}_{a}\varphi$ in
ATLK there is a formula $\varphi_{2}$ in $\ATLH$ such that for every $M$,

$M,q\models\mathcal{K}_{a}\varphi\ \Leftrightarrow\
M,q\models_{\mathcal{H}}\varphi_{2}$

We claim that we can construct such $\varphi_{2}$ from
$\mathcal{K}_{a}{\varphi}$ to be
$\varphi_{2}=\varphi\wedge\mathcal{H}_{a}^{=0}\\{{\varphi}\\}$. Therefore we
need to prove that:

$M,q\models_{\mathcal{K}}\mathcal{K}_{a}\varphi\ \Leftrightarrow\
M,q\models_{\mathcal{H}}\varphi\wedge\mathcal{H}_{a}^{=0}\\{{\varphi}\\}$

We have that $M,q\models_{\mathcal{K}}\mathcal{K}_{a}\varphi$ if and only if
$\varphi$ holds in all the indistinguishable states from $q$ for $a$, which
includes state $q$ itself. This means that $\varphi$ holds in $q$ and
$|R_{a,q}(\varphi)|=1$, which in would be expressed as
$M,q\models_{\mathcal{H}}\varphi\wedge\mathcal{H}_{a}^{=0}\\{{\varphi}\\}$. ∎

###  5.2. Uncertainty as Knowledge

ATLK is at least as expressive as .

The proof proceeds by translating every occurrence of
$\mathcal{H}_{a}^{\otimes m}\beta$ to a Boolean combination of epistemic
formulas that express the knowledge of agent $a$ with respect to the
_indistinguishability classes_ of the formulas in $\beta$, defined as follows:

######  Definition  (Indistinguishability class of a formula).

For a given model $M$, if $q\in St$, $a\in\mathit{Agt}$ and $\varphi$ is a
formula, then we define the indistinguishability class of $\varphi$ with
respect to $q$ and $a$ as follows:

$[\varphi]_{a}^{q}=[\varphi]\cap[q]_{\sim_{a}}$,

where $[q]_{\sim_{a}}$ denotes the set of states that are indistinguishable
from $q$ for $a$, and $[\varphi]$ is the set of states $q^{\prime}\in St$ were
$M,q^{\prime}\models\varphi$.

The full proof is technical and rather tedious; it can be found in the
appendix. Here, we present how the translation works on an example. Let
$\varphi_{1}$ and $\varphi_{2}$ be two formulas that do not contain any
$\mathcal{H}$ operators. We would like to find an ATLK formula
$P(\varphi_{1},\varphi_{2})$, such that:

$M,q\models\mathcal{H}_{a}^{=\log 3}\\{{\varphi_{1},\varphi_{2}}\\}\
\Leftrightarrow\ M,q\models_{\mathcal{K}}P(\varphi_{1},\varphi_{2})$

First we define new formulas $A$, $B$, $C$ and $D$ as follows:
$A=\varphi_{1}\wedge\varphi_{2}$, $B=\varphi_{1}\wedge\lnot\varphi_{2}$,
$C=\lnot\varphi_{1}\wedge\varphi_{2}$ and
$D=\lnot\varphi_{1}\wedge\lnot\varphi_{2}$. It is clear that the sets of
states $[A]_{a}^{q}$, $[B]_{a}^{q}$, $[C]_{a}^{q}$ and $[D]_{a}^{q}$ are
mutually exclusive, and moreover they partition $[q]_{\sim_{a}}$. Because the
truth value of each one of $A$, $B$, $C$, $D$ corresponds to the truth value
of exactly one of four possible different valuation combinations of
$\varphi_{1}$ and $\varphi_{2}$, so they are distinct.

If $M,q\models\mathcal{H}_{a}^{=\log 3}\\{{\varphi_{1},\varphi_{2}}\\}$, then
exactly one of $[A]_{a}^{q}$, $[B]_{a}^{q}$, $[C]_{a}^{q}$ or $[D]_{a}^{q}$
has to be empty. Because these sets are mutually disjoint, if all are non-
empty then we should have at least four different states in $[q]_{\sim_{a}}$
with the four different valuation combinations for the formulas $\varphi_{1}$
and $\varphi_{2}$. This would mean that $M,q\models\mathcal{H}_{a}^{=\log
4}\\{{\varphi_{1},\varphi_{2}}\\}$ which contradicts
$M,q\models\mathcal{H}_{a}^{=\log 3}\\{{\varphi_{1},\varphi_{2}}\\}$.
Similarly if more than one of $[A]_{a}^{q}$, $[B]_{a}^{q}$, $[C]_{a}^{q}$ or
$[D]_{a}^{q}$ are empty, then it means that only two or less possible
valuation combinations of $\varphi_{1}$ and $\varphi_{2}$ exist in
$[q]_{\sim_{a}}$. This entails that $M,q\models\mathcal{H}_{a}^{<\log
3}\\{{\varphi_{1},\varphi_{2}}\\}$, which is again a contradiction. The
converse is also true: if exactly three of the sets $[A]_{a}^{q}$,
$[B]_{a}^{q}$, $[C]_{a}^{q}$ or $[D]_{a}^{q}$ are non-empty, then there are
exactly three valuation combinations of $\varphi_{1}$ and $\varphi_{2}$ in
$[q]_{\sim_{a}}$, which follows that $M,q\models\mathcal{H}_{a}^{=\log
3}\\{{\varphi_{1},\varphi_{2}}\\}$. So the formula
$M,q\models\mathcal{H}_{a}^{=\log 3}\\{{\varphi_{1},\varphi_{2}}\\}$ holds if
and only if exactly one of $[A]_{a}^{q}$, $[B]_{a}^{q}$, $[C]_{a}^{q}$ or
$[D]_{a}^{q}$ is empty. This can happen in four different ways (one
corresponding to each of $[A]_{a}^{q}$, $[B]_{a}^{q}$, $[C]_{a}^{q}$ or
$[D]_{a}^{q}$ being empty).

First consider the case where $[C]_{a}^{q}$ is empty. Then:

$\displaystyle\nexists q^{\prime}\textit{ s.t }\ q^{\prime}\sim_{a}q\textit{
and }M,q^{\prime}\models C$ $\displaystyle\Leftrightarrow$
$\displaystyle(\forall q^{\prime},\ q^{\prime}\sim_{a}q\ \Longrightarrow
M,q^{\prime}\not\models C)$ $\displaystyle\Leftrightarrow$
$\displaystyle(\forall q^{\prime},\ q^{\prime}\sim_{a}q\ \Longrightarrow
M,q^{\prime}\models\lnot C)$ $\displaystyle\Leftrightarrow$ $\displaystyle
M,q\models\mathcal{K}_{a}\lnot C$

In a similar way we can show that $[A]_{a}^{q}$ is non-empty iff
$M,q\models\lnot\mathcal{K}_{a}\lnot A$. The same goes for $[B]_{a}^{q}$, and
$[D]_{a}^{q}$. Therefore among $[A]_{a}^{q}$, $[B]_{a}^{q}$, $[C]_{a}^{q}$ and
$[D]_{a}^{q}$, only $[C]_{a}^{q}$ is empty iff:

$M,q\models\lnot\mathcal{K}_{a}\lnot A\wedge\lnot\mathcal{K}_{a}\lnot
B\wedge\mathcal{K}_{a}\lnot C\wedge\lnot\mathcal{K}_{a}\lnot D$

We got this result by assuming that only $[C]_{a}^{q}$ is empty. Given that
$M,q\models\mathcal{H}_{a}^{=\log 3}\\{{\varphi_{1},\varphi_{2}}\\}$ iff
exactly one of $[A]_{a}^{q}$, $[B]_{a}^{q}$, $[C]_{a}^{q}$ or $[D]_{a}^{q}$ is
empty, and knowing that we have four possible choices for which one is to be
empty, we get that:

$M,q\models\mathcal{H}_{a}^{=\log
3}\\{{\varphi_{1},\varphi_{2}}\\}\Leftrightarrow
M,q\models_{\mathcal{K}}P(\varphi_{1},\varphi_{2})$

where $P(\varphi_{1},\varphi_{2})$ is defined as:

$\displaystyle P(\varphi_{1},\varphi_{2})=\quad$
$\displaystyle(\mathcal{K}_{a}\lnot(\varphi_{1}\wedge\varphi_{2})\wedge\lnot\mathcal{K}_{a}\lnot(\varphi_{1}\wedge\lnot\varphi_{2})$
$\displaystyle\qquad\wedge\lnot\mathcal{K}_{a}\lnot(\lnot\varphi_{1}\wedge\varphi_{2})\wedge\lnot\mathcal{K}_{a}\lnot(\lnot\varphi_{1}\wedge\lnot\varphi_{2}))$
$\displaystyle\vee$
$\displaystyle(\lnot\mathcal{K}_{a}\lnot(\varphi_{1}\wedge\varphi_{2})\wedge\mathcal{K}_{a}\lnot(\varphi_{1}\wedge\lnot\varphi_{2})$
$\displaystyle\qquad\wedge\lnot\mathcal{K}_{a}\lnot(\lnot\varphi_{1}\wedge\varphi_{2})\wedge\lnot\mathcal{K}_{a}\lnot(\lnot\varphi_{1}\wedge\lnot\varphi_{2}))$
$\displaystyle\vee$
$\displaystyle(\lnot\mathcal{K}_{a}\lnot(\varphi_{1}\wedge\varphi_{2})\wedge\lnot\mathcal{K}_{a}\lnot(\varphi_{1}\wedge\lnot\varphi_{2})$
$\displaystyle\qquad\wedge\mathcal{K}_{a}\lnot(\lnot\varphi_{1}\wedge\varphi_{2})\wedge\lnot\mathcal{K}_{a}\lnot(\lnot\varphi_{1}\wedge\lnot\varphi_{2}))$
$\displaystyle\vee$
$\displaystyle(\lnot\mathcal{K}_{a}\lnot(\varphi_{1}\wedge\varphi_{2})\wedge\lnot\mathcal{K}_{a}\lnot(\varphi_{1}\wedge\lnot\varphi_{2})$
$\displaystyle\qquad\wedge\lnot\mathcal{K}_{a}\lnot(\lnot\varphi_{1}\wedge\varphi_{2})\wedge\mathcal{K}_{a}\lnot(\lnot\varphi_{1}\wedge\lnot\varphi_{2})).$

##  6\. Uncertainty Is Exponentially More Succinct than Knowledge

The notion of succinctness Stockmeyer (1972); Wilke (1999); Adler and Immerman
(2001) is a refinement of the notion of expressivity. Assume that one
particular property can be expressed in both languages $L_{1}$ and $L_{2}$,
with formulas $\varphi_{1}$ and $\varphi_{2}$ respectively. When comparing the
representational succinctness of these two languages, we are interested in
whether there is a significant difference in the lengths of $\varphi_{1}$ and
$\varphi_{2}$. Similar to analysis of complexity, what we consider significant
is at least exponential growth of the size of a formula in one of the
languages comparing to the equivalent formula in the other language. In this
section, we prove that the language of $\ATLH$ is exponentially more succinct
than ATLK. We use the so called _formula size games (FSG)_ from French et al.
(2013) to construct the proof. In brief, we will show that for any
$n\in\mathbb{N}$, there is a formula $\varphi_{n}$ of size linear to $n$ in
ATLH, such that for any formula $\varphi_{n}^{\prime}$ in ATLK with the same
set of satisfying models as $\varphi_{n}$, the parse tree of
$\varphi_{n}^{\prime}$ will have at least $2^{n}$ distinct nodes, and
therefore the size of $\varphi_{n}^{\prime}$ is at least exponential in $n$.

###  6.1. Succinctness and Formula Size Games

Before showing that ATL with uncertainty is exponentially more succinct than
ATL with knowledge, we summarize the basic terminology.

######  Definition  (Length of formulas in ).

The length of formula $\varphi$ is denoted by $|\varphi|$, recursively defined
as follows:
$|p|=1$,
$|(\varphi_{1}\vee\varphi_{2})|=|\varphi_{1}\,\mathcal{U}\,\varphi_{2}|=|\varphi_{1}|+|\varphi_{2}|+1$,
$|\lnot\varphi|=|X\varphi|=|G\varphi|=1+|\varphi|$
$|\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\varphi|=|A|+|\varphi|$,
$|\mathcal{H}_{a}^{\otimes
m}\beta|=1+\sum_{\varphi_{i}\in\beta}|\varphi_{i}|$.

######  Definition  (Succinctness).

Let $L_{1}=\langle\varPhi_{1},\models_{1},M\rangle$ and
$L_{2}=\langle\varPhi_{2},\models_{2},M\rangle$ be two logics such that
$L_{1}\leqslant_{M}L_{2}$ and let $f(x)=O(g(n))$ be a strictly increasing
function. If for every $n\in\mathbb{(}N)$ there are two formulas
$\alpha_{n}\in\varPhi_{1}$ and $\beta_{n}\in\varPhi_{2}$ where:

  * •

$|\alpha_{n}|=f(n)$

  * •

$|\beta_{n}|=2^{g(n)}$

  * •

$\beta_{n}$ is the shortest formula on $\varPhi_{2}$ that is equivalent to
$\alpha_{n}$ on $M$,

then we say that $L_{1}$ is exponentially more succinct than $L_{2}$ on $M$
and write it as: $L_{1}\not\leqslant_{M}^{\mathit{subexp}}L_{2}$.

In the following, for a set of pointed models $A$, we use the term
$A\models\varphi$ to mean that $\forall M\in A\,.\,M\models\varphi$.

######  Definition  (FSG).

One-person formula size game (FSG) on two sets of pointed models $A$ and $B$
is played as follows: during the course of the game, a game tree is
constructed such that each node is labeled with pair $\langle C\circ D\rangle$
of sets of pointed models. The possible moves for the player (called _the
spoiler_) on each node of the tree are
$\\{{p\in\mathit{Pv},\lnot,\vee,\mathcal{K}_{i}}\\}$, where
$i\in\mathit{Agt}$. A node can be open or closed. Once a node is closed, no
further move can be played there. The condition and consequences of each of
possible moves are as below:

$p\in\mathit{Pv}$:

(Atomic move): the spoiler chooses $p\in\mathit{Pv}$ such that $C\models p$
and $D\models\lnot p$. Then the node is declared closed.

$\lnot$:

(Not move): A new node $\langle C\circ D\rangle$ is added to the tree.

$\vee$:

(Or move): two nodes $\langle C_{1}\circ D\rangle$ and $\langle C_{2}\circ
D\rangle$ are added to the tree such that $C_{1}\cup C_{2}=C$.

$K_{i}$:

(Knows move), where $i\in\mathit{Agt}$: For each $(M,s)\in D$ the spoiler
chooses a pointed model $(M,s^{\prime})$ such that $s\sim_{a}s^{\prime}$. If
for some $(M,s)\in D$ such $(M,s^{\prime})$ does not exist, then the spoiler
cannot play this move. All such chosen pointed models are collected in
$D^{\prime}$. Moreover, for each $(M,s)\in C$, all possible pointed models
$(M,s^{\prime})$ such that $s\sim_{a}s^{\prime}$ are added to $C^{\prime}$.
Then a new node $\langle C^{\prime}\circ D^{\prime}\rangle$ is added to the
tree.

We say that the spoiler wins FSG starting at $\langle A\circ B\rangle$ in $n$
moves iff there is a game tree $T$ with root $\langle A\circ B\rangle$ and
precisely n nodes such that every leaf of $T$ is closed.

[French et al. (2013)] The spoiler can win the FSG starting at $\langle A\circ
B\rangle$ in less than $k$ moves iff there is some $n<k$ and a formula
$\varphi\in\varPhi_{MEL}$ such that $A\models_{MEL}\varphi$,
$B\models_{MEL}\lnot\varphi$ and $|\varphi|=n$, where $\varPhi_{MEL}$ is the
set of formulas defined in Multiagent epistemic logic and $\models_{MEL}$
shows truth relation in it.

The game tree through which the spoiler wins the FSG is the parse three of
formula $\varphi$ in the language of Multiagent epistemic logic. For any
$\langle A\circ B\rangle$, the set of all closed game trees with root $\langle
A\circ B\rangle$ is denoted by $T(\langle A\circ B\rangle)$. Consequently, the
set of closed trees represents also the set of all formulas $\varphi$ that
could distinguish the set of pointed models $A$ from the set of pointed models
$B$ via the truth relation $\models_{MEL}$.

###  6.2. Is More Succinct than

Theorem 6.1 allows us to use FSG for proving the succinctness of our new logic
with respect to ATLK.

The logic ATLH is exponentially more succinct than the logic ATLK.

The full proof is rather technical; it can be found in the appendix. Here we
explain the sketch of the proof:

###### Proof sketch.

Let $Lang(\textbf{ATLK})$ and $Lang(\textbf{ATLH})$ represent the languages of
the logics ATLK and ATLH respectively. For every $n\in\mathbb{N}$, we define a
formula $\varphi_{n}\in Lang(\textbf{ATLH})$ where $f(n)=n$. Then, we define
two sets of pointed models $A_{n}$ and $B_{n}$, such that
$A_{n}\models_{\mathcal{H}}\varphi_{n}$ and
$B_{n}\models_{\mathcal{H}}\lnot\varphi_{n}$. Because ATLK is as expressive as
ATLH, there exists a formula $\psi_{n}\in Lang(\textbf{ATLK})$ which is the
shortest formula in $Lang(\textbf{ATLK})$ equivalent to $\varphi_{n}$.
Therefore $\psi_{n}$ too can distinguish sets $A_{n}$ and $B_{n}$, which means
the spoiler can win the FSG game starting at $\langle A_{n}\circ B_{n}\rangle$
by playing the formula $\psi_{n}$. We then prove that the spoiler cannot win
the FSG game starting at $\langle A_{n}\circ B_{n}\rangle$ in less than
$2^{n}$ moves, which means the size of $\psi_{n}$ is at least $2^{n}$. ∎

Issue AIssue B

Figure 3. Example ThreeBallot vote. Here the voter has voted for issue $A$ and
against issue $B$. Thus, the value of the vote is $A\overline{B}$. The voter
fills two fields in the row of issue $A$ and one space in the row of issue
$B$, and then she separates the three ballots. The resulting ballot set is
$\\{{FB,BB,FF}\\}$.

  Vote and ballot set (BS) Receipt Possible information sets of the
coercer Vote = $\overline{A}\overline{B}$, BS = $\\{{BB,FB,BF}\\}$ BB
$\\{{\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}\overline{B}}\\}$,
$\\{{\overline{A}B,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ FB
$\\{{\overline{A}\overline{B}}\\}$,
$\\{{\overline{A}B,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},AB,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ BF
$\\{{\overline{A}\overline{B}}\\}$,
$\\{{\overline{A}B,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}\overline{B}}\\}$,
$\\{{\overline{A}B,AB,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ Vote =
$\overline{A}\overline{B}$, BS = $\\{{BB,BB,FF}\\}$ BB
$\\{{\overline{A}\overline{B}}\\}$,
$\\{{\overline{A}B,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}\overline{B}}\\}$,
$\\{{AB,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ FF
$\\{{\overline{A}\overline{B}}\\}$,
$\\{{\overline{A}B,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}\overline{B}}\\}$,
$\\{{AB,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ Vote =
$A\overline{B}$, BS = $\\{{BB,FB,FF}\\}$ BB $\\{{A\overline{B}}\\}$,
$\\{{A\overline{B},AB}\\}$, $\\{{A\overline{B},\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ FB
$\\{{A\overline{B}}\\}$, $\\{{A\overline{B},AB}\\}$,
$\\{{A\overline{B},\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},AB,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ FF
$\\{{A\overline{B}}\\}$, $\\{{A\overline{B},AB}\\}$,
$\\{{A\overline{B},\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ Vote =
$A\overline{B}$, BS = $\\{{FB,FB,BF}\\}$ FB $\\{{A\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B}\\}$, $\\{{A\overline{B},AB}\\}$,
$\\{{A\overline{B},\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ BF
$\\{{A\overline{B}}\\}$, $\\{{A\overline{B},\overline{A}B}\\}$,
$\\{{A\overline{B},AB}\\}$, $\\{{A\overline{B},\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ Vote =
$\overline{A}B$, BS = $\\{{BB,BF,FF}\\}$ BB $\\{{\overline{A}B}\\}$,
$\\{{\overline{A}B,\overline{A}\overline{B}}\\}$, $\\{{\overline{A}B,AB}\\}$,
$\\{{A\overline{B},\overline{A}B,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ BF
$\\{{\overline{A}B}\\}$, $\\{{\overline{A}B,AB}\\}$,
$\\{{\overline{A}B,\overline{A}\overline{B}}\\}$,
$\\{{\overline{A}B,AB,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ FF
$\\{{\overline{A}B}\\}$, $\\{{\overline{A}B,\overline{A}\overline{B}}\\}$,
$\\{{\overline{A}B,AB}\\}$, $\\{{A\overline{B},\overline{A}B,AB}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ Vote =
$\overline{A}B$, BS = $\\{{FB,BF,BF}\\}$ FB $\\{{\overline{A}B}\\}$,
$\\{{\overline{A}B,\overline{A}\overline{B}}\\}$, $\\{{\overline{A}B,AB}\\}$,
$\\{{A\overline{B},\overline{A}B}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ BF
$\\{{\overline{A}B}\\}$, $\\{{\overline{A}B,\overline{A}\overline{B}}\\}$,
$\\{{\overline{A}B,AB}\\}$, $\\{{A\overline{B},\overline{A}B}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ Vote = $AB$,
BS = $\\{{FB,BF,FF}\\}$ FB $\\{{AB}\\}$, $\\{{A\overline{B},AB}\\}$,
$\\{{\overline{A}B,AB}\\}$,
$\\{{A\overline{B},AB,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ BF
$\\{{AB}\\}$, $\\{{A\overline{B},AB}\\}$, $\\{{\overline{A}B,AB}\\}$,
$\\{{\overline{A}B,AB,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ FF
$\\{{AB}\\}$, $\\{{A\overline{B},AB}\\}$, $\\{{\overline{A}B,AB}\\}$,
$\\{{A\overline{B},\overline{A}B,AB}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ Vote = $AB$,
BS = $\\{{BB,FF,FF}\\}$ BB $\\{{AB}\\}$,
$\\{{AB,\overline{A}\overline{B}}\\}$, $\\{{A\overline{B},AB}\\}$,
$\\{{\overline{A}B,AB}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$ FF
$\\{{AB}\\}$, $\\{{AB,\overline{A}\overline{B}}\\}$,
$\\{{A\overline{B},AB}\\}$, $\\{{\overline{A}B,AB}\\}$,
$\\{{A\overline{B},\overline{A}B,AB,\overline{A}\overline{B}}\\}$

Table 1. Indistinguishability sets of the coercer in a two voter, two issue
referendum with ThreeBallot, based on the selected receipt by the voter. Each
row lists the possible epistemic classes $[q]_{\sim_{c}}$ of the coercer,
depending on the voter’s vote and the way she filled her ballots (invisible to
the coercer), the voter’s election receipt (visible to the coercer), and the
set of ballots posted on the public bulletin board

##  7\. Case Study: Three Ballot

We demonstrate the usefulness of our proposal on a real-life voting scenario.

###  7.1. Voting with ThreeBallot

ThreeBallot Rivest (2006); Rivest and Smith (2007) has been proposed by Rivest
as a paper-based end-to-end verifiable voting protocol. Here, we use a
simplified version of the protocol, which can be used for multiple-issue
referendums. Following the example in Section 3, we consider a two-issue
referendum, in which each voter votes to accept or reject two proposals $A$
and $B$.

In ThreeBallot, the ballots are prepared such that for each issue, there are
three empty fields that the voter can fill. For voting to accept the issue,
the voter has to fill exactly two of the empty fields, and to vote to reject
the issue, the voter has to fill exactly one empty field. However, the exact
positions of the filled spaces are up to the voter. After filling the ballots,
the voter separates three columns of fields, and in this way creates three
separate ballots. The voter can make (and keep) a copy of one of those ballots
as the receipt. Finally, she puts all the original ballots in the ballot box.
The tally of the votes is done by counting the filled spaces for each issue.
The difference between the number of filled spaces for each issue and the
number of voters shows the number of votes in favor of that issue. After the
tallying, all the ballots are published on a public bulletin board, so that
everyone can check the correctness of the result.

One of the main goals of ThreeBallot is _coercion resistance_ Juels et al.
(2005), i.e., the protocol should make it impossible for a third party to
successfully coerce or bribe voters into voting in a particular way.
Informally, coercion resistance is usually understood as the inability of the
coercer to learn how the voter has voted, even if the voter cooperates with
the coercer. Interestingly, ThreeBallot was both claimed secure Rivest and
Smith (2007) and insecure Appel (2006). It might seem that one of the claims
must be wrong, but a closer look reveals that they are based on different
concepts of vote privacy. In Rivest and Smith (2007), it is argued that the
coercer cannot get to _know how the voter has voted_ , which is a strategic-
epistemic property. In contrast, Appel (2006) argues that the coercer can
_gain information_ about the value of the vote. We demonstrate the difference
in the remainder of this section.

###  7.2. Model of the Scenario

In our example, the two propositions that determine the vote of the voter are
$V_{A}$ and $V_{B}$. We encode a vote against an issue by using overline. So,
$\overline{A}B$ indicates a vote for issue $B$ and against issue $A$; in other
words, it states that $V_{A}$ is false and $V_{B}$ is true. This way, the set
of possible votes from the voter is
$Votes=\\{{AB,\overline{A}B,A\overline{B},\overline{A}\overline{B}}\\}$.
Similarly, we encode a filled space by $F$ and a blank (not filled) space by
$B$. For instance, a $\\{{Blank,Filled}\\}$ ballot is denoted by $BF$. Figure
3 depicts an example ThreeBallot card and the resulting ballots.

We consider a scenario with two voters and a two issue referendum with issues
$A$ and $B$. Let us call the first voter the voter, as she will be the one
that we are focusing on in this example. We call the second voter the other
voter. During the election, the voter has several choices. The first is what
vote she is going to cast. Then for each possible vote, there are various ways
that the ballots can be filled, which will result in different ballot sets.
After that, the voter has the choice of which of the ballots to keep a copy as
the receipt. In our scenario, there exist a coercer who after the election
will force the voter to reveal her receipt. The coercer then tries to infer
the actual value of the voter’s vote, based on the receipt and the published
bulletin board.

Table 1 shows the different ways how the choices of the voter affect the
possible indistinguishability set of the coercer about the value of the vote,
after the receipt has been revealed. The different indistinguishability sets
in each row result from various ways in which the other voter might fill his
ballot.

###  7.3. Analysis: Epistemic Security

The coercion resistance security property is usually framed following the idea
that the coercer cannot _get to know_ how the voter has voted, even if the
voter cooperates with the coercer. In Tabatabaei et al. (2016), various
nuances of coercion resistance are formulated in the logic . In a similar way,
we can use to express coercion resistance in our ThreeBallot example as
follows:

$\bigwedge_{V_{i}\in
Votes}\lnot\langle\\!\langle{v,c}\rangle\\!\rangle_{{}_{\\!\mathit{}}}F(V_{1}=V_{i}\wedge(V_{1}\neq
V_{2}\rightarrow\mathcal{K}_{c}(V_{1}=V_{i})))$

The formula states that for any vote choice, there exists no common strategy
for the voter and the coercer, such that the voter selects that vote and given
that the choice of the two voters are different (the reason for this condition
is explained below), the coercer would know the value of the vote.333 Note
that we use $(V_{1}=V_{i})$ in the role of an atomic proposition which
evaluates to true whenever $V_{1}$ is indeed equal to $V_{i}$. Condition
$(V_{1}\neq V_{2})$ is treated analogously.

It is obvious that in the cases where both voters have voted identically, even
without revealing the receipt, the coercer will know the value of the vote
just by looking at the bulletin board. This is similar to the case when in an
election all the voters vote similarly, in which case the privacy of their
votes will be broken after publishing the tally (unless some sort of
obfuscation is used Jamroga et al. (2019b)). We added the condition
$(V_{1}\neq V_{2})$ to the above formula to account for this. Also in the
following we only focus on the cases where the two voters has voted
differently.

By looking at Table 1 we can see that the model satisfies the coercion
resistance property as formulated in the above expression. This is because
there is no row in the table that consists of only one indistinguishability
set for the coercer which has only one member (the actual value of the vote).
However the voter votes and selects the receipt, there is at least one
possible indistinguishability set with more than one member, meaning that the
coercer might not get to know the actual vote of the voter.

###  7.4. Information-Theoretic Security in

We can alternatively define the coercion resistance property in the
information-theoretic sense, namely that the coercer cannot _gain information_
on how the voter has voted, even if the voter cooperates with the coercer.
Phrasing this differently, we want that no matter the course of actions of the
voter and coercer, the coercer has always maximum uncertainty about the actual
value of the vote. We can express this property in as follows:

$\bigwedge_{V_{i}\in
Votes}\lnot\langle\\!\langle{v,c}\rangle\\!\rangle_{{}_{\\!\mathit{}}}F(V_{1}=V_{i}\wedge(V_{1}\neq
V_{2}\rightarrow\mathcal{H}^{=\log(|Votes|)}_{c}\\{{V_{A},V_{B}}\\}))$

The above formula states that, for any joint strategy of the coercer and the
voter, the uncertainty of the coercer will always be at the maximum. Looking
at Table 1, we can see that the ThreeBallot protocol does not satisfy this
property. This is because in each row there exists a possible
indistinguishability set whose size is less than the number of possible votes.

This example shows that, although ThreeBallot could be considered secure with
respect to the epistemic notion of coercion resistance expressed in , it is
not secure when we define the security requirement as an information-theoretic
property, and formalize it in .

##  8\. Conclusion

In this work, we introduce the logic which extends alternating-time temporal
logic ATL with quantitative modalities based on the Hartley measure of
uncertainty. As the main technical result, we show that has the same
expressive power and the same model checking complexity as (i.e., ATL with
epistemic modalities), but it is exponentially more succinct.

The succinctness result, together with the model checking complexity, is of
major significance. As we have seen in Section 4.3, both and have the same
verification complexity with respect to the size of the model and the length
of the formula. Theorem 6.2 promises that, for some properties, their
verification in will be exponentially faster than in . Also, a more succinct
language often results in better readability, which in turn helps the
designers of a system to make less mistakes in the specification of desired
properties. Last but not least, many properties can be expressed in in a much
more intuitive way than in . Understanding the information-theoretic intuition
of a corresponding formula can be a real challenge.

We suggest the specification of security requirements as an important
application area for our proposal. In particular, the framework can be used to
expose the logical structure of security claims, for example, the difference
between the epistemic and information-theoretic notions of privacy. We
demonstrate this on a real-life voting scenario involving the ThreeBallot
protocol, which has been both claimed secure and insecure in the past. Indeed,
the protocol is secure with respect to an epistemic notion of privacy, but it
may fail to obtain the information-theoretic one.

In the future, we plan to implement model checking for as an extension of the
STV Kurpiewski et al. (2021) or MCMAS Lomuscio et al. (2017) model checkers.

The work has been supported by NCBR Poland and FNR Luxembourg under the
PolLux/FNR-CORE projects STV (POLLUX-VII/1/2019 & C18/IS/12685695/IS/STV/Ryan)
and SpaceVote (POLLUX-XI/14/SpaceVote/2023).

## References

  * (1)
  * Adler and Immerman (2001) Micah Adler and Neil Immerman. 2001.  An n! Lower Bound on Formula Size. In _Proceedings of IEEE Symposium on Logic in Computer Science_. 197–206.
  * Ågotnes (2006) T. Ågotnes. 2006\.  Action and Knowledge in Alternating-time Temporal Logic.  _Synthese_ 149, 2 (2006), 377–409.
  * Ågotnes et al. (2015) T. Ågotnes, V. Goranko, W. Jamroga, and M. Wooldridge. 2015.  Knowledge and Ability.  In _Handbook of Epistemic Logic_. 543–589.
  * Ågotnes and van Ditmarsch (2008) T. Ågotnes and H. van Ditmarsch. 2008.  Coalitions and Announcements. In _Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS)_. 673–680.
  * Alur et al. (2001) R. Alur, L. de Alfaro, R. Grossu, T.A. Henzinger, M. Kang, C.M. Kirsch, R. Majumdar, F.Y.C. Mang, and B.-Y. Wang. 2001.  jMocha: A Model-Checking Tool that Exploits Design Structure. In _Proceedings of International Conference on Software Engineering (ICSE)_. 835–836.
  * Alur et al. (1998) R. Alur, T. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran. 1998\.  MOCHA: Modularity in Model Checking. In _Proceedings of Computer Aided Verification (CAV)_ _(Lecture Notes in Computer Science, Vol. 1427)_. 521–525.
  * Alur et al. (1997) R. Alur, T. A. Henzinger, and O. Kupferman. 1997.  Alternating-Time Temporal Logic. In _Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS)_. 100–109.
  * Alur et al. (2002) R. Alur, T. A. Henzinger, and O. Kupferman. 2002.  Alternating-Time Temporal Logic.  _J. ACM_ 49 (2002), 672–713.  https://doi.org/10.1145/585265.585270
  * Aminof et al. (2018) Benjamin Aminof, Vadim Malvone, Aniello Murano, and Sasha Rubin. 2018.  Graded modalities in Strategy Logic.  _Information and Computation_ 261 (2018), 634–649.
  * Appel (2006) Andrew W. Appel. 2006\.  How to defeat Rivest’s ThreeBallot voting system. (2006).  https://www.cs.princeton.edu/~appel/papers/DefeatingThreeBallot.pdf
  * Belardinelli et al. (2022) Francesco Belardinelli, Wojtek Jamroga, Vadim Malvone, Munyque Mittelmann, Aniello Murano, and Laurent Perrussel. 2022.  Reasoning about Human-Friendly Strategies in Repeated Keyword Auctions. In _Proceedings of AAMAS_. 62–71.
  * Belardinelli et al. (2017) F. Belardinelli, A. Lomuscio, A. Murano, and S. Rubin. 2017\.  Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic. In _Proceedings of IJCAI_. 91–97.
  * Bolander and Birkegaard Andersen (2011) T. Bolander and M. Birkegaard Andersen. 2011.  Epistemic planning for single- and multi-agent systems.  _Journal of Applied Non-Classical Logics_ 21, 1 (2011), 9–34.
  * 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 _Proceedings of IJCAI_. 1588–1594.
  * Bozzelli et al. (2020) Laura Bozzelli, Aniello Murano, and Loredana Sorrentino. 2020\.  Alternating-time temporal logics with linear past.  _Theor. Comput. Sci._ 813 (2020), 199–217.
  * Bulling et al. (2010) N. Bulling, J. Dix, and W. Jamroga. 2010.  Model Checking Logics of Strategic Ability: Complexity.  In _Specification and Verification of Multi-Agent Systems_. 125–159.
  * Bulling et al. (2015) N. Bulling, V. Goranko, and W. Jamroga. 2015.  Logics for Reasoning About Strategic Abilities in Multi-Player Games.  In _Models of Strategic Reasoning. Logics, Games, and Communities_. Lecture Notes in Computer Science, Vol. 8972. 93–136.
  * Bulling and Jamroga (2009) N. Bulling and W. Jamroga. 2009.  What Agents Can Probably Enforce.  _Fundamenta Informaticae_ 93, 1-3 (2009), 81–96.
  * Busard et al. (2014) S. Busard, C. Pecheur, H. Qu, and F. Raimondi. 2014\.  Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints.  In _Formal Methods and Software Engineering_. Lecture Notes in Computer Science, Vol. 8829. 27–42.
  * Cermak et al. (2014) P. Cermak, A. Lomuscio, F. Mogavero, and A. Murano. 2014\.  MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications. In _Proc. of Computer Aided Verification (CAV)_ _(Lecture Notes in Computer Science, Vol. 8559)_. 525–532.
  * 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 _Proceedings of AAAI_. 2038–2044.
  * Chatterjee et al. (2007) K. Chatterjee, T. A. Henzinger, and N. Piterman. 2007\.  Strategy Logic. In _Proceedings of CONCUR_. 59–73.
  * Chen et al. (2013) T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis. 2013.  PRISM-games: A Model Checker for Stochastic Multi-Player Games. In _Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS)_ _(Lecture Notes in Computer Science, Vol. 7795)_. 185–191.
  * Chen and Lu (2007) Taolue Chen and Jian Lu. 2007.  Probabilistic Alternating-time Temporal Logic and Model Checking Algorithm. In _Proceedings of FSKD, Volume 2_. 35–39.
  * Emerson (1990) E.A. Emerson. 1990\.  Temporal and Modal Logic.  In _Handbook of Theoretical Computer Science_. Vol. B. 995–1072.
  * Ferrante et al. (2008) Alessandro Ferrante, Aniello Murano, and Mimmo Parente. 2008\.  Enriched $\mathrm{\mu}$-Calculi Module Checking.  _Log. Methods Comput. Sci._ 4, 3 (2008).
  * French et al. (2013) Tim French, Wiebe van der Hoek, Petar Iliev, and Barteld P. Kooi. 2013.  On the succinctness of some modal logics.  _Artificial Intelligence_ 197 (2013), 56–85.
  * Halpern and Vardi (1991) Joseph Y Halpern and Moshe Y Vardi. 1991.  Model checking vs. theorem proving: a manifesto.  _Artificial intelligence and mathematical theory of computation_ 212 (1991), 151–176.
  * Hartley (1928) R.V.L. Hartley. 1928\.  Transmission of Information.  _Bell Systems Technical Journal_ 7 (1928), 535.
  * Huang et al. (2012) X. Huang, K. Su, and C. Zhang. 2012.  Probabilistic Alternating-Time Temporal Logic of Incomplete Information and Synchronous Perfect Recall. In _Proceedings of AAAI-12_.
  * Huang and van der Meyden (2014) X. Huang and R. van der Meyden. 2014.  Symbolic Model Checking Epistemic Strategy Logic. In _Proceedings of AAAI Conference on Artificial Intelligence_. 1426–1432.
  * Jamroga and Ågotnes (2007) W. Jamroga and T. Ågotnes. 2007.  Constructive Knowledge: What Agents Can Achieve under Incomplete Information.  _Journal of Applied Non-Classical Logics_ 17, 4 (2007), 423–475.
  * Jamroga and Dix (2006) W. Jamroga and J. Dix. 2006\.  Model Checking ATLir is Indeed $\Delta_{2}^{P}$-complete. In _Proceedings of EUMAS_ _(CEUR Workshop Proceedings, Vol. 223)_.
  * Jamroga et al. (2019a) Wojciech Jamroga, Michał Knapik, Damian Kurpiewski, and Łukasz Mikulski. 2019a.  Approximate Verification of Strategic Abilities under Imperfect Information.  _Artificial Intelligence_ 277 (2019).
  * Jamroga et al. (2019b) Wojciech Jamroga, Peter B. Rønne, Peter Y. A. Ryan, and Philip B. Stark. 2019b.  Risk-Limiting Tallies. In _Electronic Voting: Proceedings of E-Vote-ID_. 183–199.
  * Jamroga and Tabatabaei (2013) W. Jamroga and M. Tabatabaei. 2013.  Accumulative Knowledge Under Bounded Resources. In _Proceedings of CLIMA XIV_ _(Lecture Notes in Computer Science, Vol. 8143)_. 206–222.
  * Jamroga and van der Hoek (2004) W. Jamroga and W. van der Hoek. 2004.  Agents that Know how to Play.  _Fundamenta Informaticae_ 63, 2–3 (2004), 185–219.
  * Juels et al. (2005) A. Juels, D. Catalano, and M. Jakobsson. 2005.  Coercion-resistant electronic elections. In _Proceedings of the 2005 ACM workshop on Privacy in the electronic society_. ACM, 61–70.
  * Kacprzak and Penczek (2004) M. Kacprzak and W. Penczek. 2004.  Unbounded Model Checking for Alternating-Time Temporal Logic. In _Proceedings of AAMAS_. 646–653.
  * Katz and Lindell (2020) Jonathan Katz and Yehuda Lindell. 2020.  _Introduction to Modern Cryptography, Third Edition_.
  * Kurpiewski et al. (2019) Damian Kurpiewski, Wojciech Jamroga, and Michał Knapik. 2019.  STV: Model Checking for Strategies under Imperfect Information. In _Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019_. 2372–2374.
  * Kurpiewski et al. (2021) Damian Kurpiewski, Witold Pazderski, Wojciech Jamroga, and Yan Kim. 2021.  STV+Reductions: Towards Practical Verification of Strategic Ability Using Model Reductions. In _Proceedings of AAMAS_. 1770–1772.
  * Lomuscio et al. (2017) A. Lomuscio, H. Qu, and F. Raimondi. 2017.  MCMAS: An Open-Source Model Checker for the Verification of Multi-Agent Systems.  _International Journal on Software Tools for Technology Transfer_ 19, 1 (2017), 9–30.
  * Lomuscio and Raimondi (2006) A. Lomuscio and F. Raimondi. 2006.  MCMAS : A Model Checker for Multi-Agent Systems. In _Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS)_ _(Lecture Notes in Computer Science, Vol. 4314)_. 450–454.
  * Markey (2003) Nicolas Markey. 2003\.  Temporal logic with past is exponentially more succinct.  _Bull. EATCS_ 79 (2003), 122–128.
  * Mogavero et al. (2010) F. Mogavero, A. Murano, and M.Y. Vardi. 2010.  Reasoning About Strategies. In _Proceedings of FSTTCS_. 133–144.
  * Pilecki et al. (2014) J. Pilecki, M.A. Bednarczyk, and W. Jamroga. 2014\.  Synthesis and Verification of Uniform Strategies for Multi-Agent Systems. In _Proceedings of CLIMA XV_ _(Lecture Notes in Computer Science, Vol. 8624)_. 166–182.
  * Rivest (2006) R. Rivest. 2006\.  The ThreeBallot Voting System. (2006).  Available online at http://theory.csail.mit.edu/~rivest/Rivest-TheThreeBallotVotingSystem.pdf.
  * Rivest and Smith (2007) R. Rivest and W. Smith. 2007.  Three Voting Protocols: ThreeBallot, VAV, and Twin. In _Proceedings of USENIX/ACCURATE Electronic Voting Technology Workshop (EVT)_.
  * Schobbens (2004) P. Y. Schobbens. 2004\.  Alternating-Time Logic with Imperfect Recall.  _Electronic Notes in Theoretical Computer Science_ 85, 2 (2004), 82–93.
  * Stockmeyer (1972) Larry J. Stockmeyer. 1972\.  _The Complexity of Decision Problems in Automata Theory and Logic_.  Ph.D. Dissertation. Massachusetts Institute of Technology.
  * Tabatabaei et al. (2016) M. Tabatabaei, W. Jamroga, and Peter Y. A. Ryan. 2016\.  Expressing Receipt-Freeness and Coercion-Resistance in Logics of Strategic Ability: Preliminary Attempt. In _Proceedings of the 1st International Workshop on AI for Privacy and Security, PrAISe@ECAI 2016_. 1:1–1:8.
  * van der Hoek and Wooldridge (2002) W. van der Hoek and M. Wooldridge. 2002.  Tractable Multiagent Planning for Epistemic Goals. In _Proceedings of the First International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS-02)_. 1167–1174.
  * van der Hoek and Wooldridge (2003a) W. van der Hoek and M. Wooldridge. 2003a.  Cooperation, Knowledge and Time: Alternating-time Temporal Epistemic Logic and its Applications.  _Studia Logica_ 75, 1 (2003), 125–157.
  * van der Hoek and Wooldridge (2003b) W. van der Hoek and M. Wooldridge. 2003b.  Model Checking Cooperation, Knowledge and Time – A Case Study.  _Research in Economics_ 57, 3 (2003), 235–265.
  * van Ditmarsch et al. (2007) H. van Ditmarsch, W. van der Hoek, and B. Kooi. 2007\.  _Dynamic Epistemic Logic_.
  * Wang and Dechesne (2009) Y. Wang and F. Dechesne. 2009.  On expressive power and class invariance.  _CoRR_ abs/0905.4332 (2009).
  * Wilke (1999) Thomas Wilke. 1999\.  CTL+ is Exponentially more Succinct than CTL. In _Proceedings of FSTTCS_ _(Lecture Notes in Computer Science, Vol. 1738)_. 110–121.

##  Appendix A Detailed Proofs

### Proof of Theorem 5.2

######  Theorem.

ATLK is at least as expressive as .

Because the set of formulas defined in ATLK includes all the formulas defined
in $\ATLH$, except the formulas including $\mathcal{H}$ operator, and the
semantics of the common formulas are similar in both logics, we formulate the
proof by giving a translation from an ATLH formula of type
$\mathcal{H}_{a}^{\otimes m}\beta$ to an equivalent ATLK formula. Before
giving the translation, we introduce some helper definitions: For a given
formula $\varphi$, let ${(\lnot)}^{0}:=\lnot\varphi$ and
${(\lnot)}^{1}:=\varphi$.

######  Definition .

If $\beta=\\{{\varphi_{1},...\varphi_{n}}\\}$ is a set of $n$ formulas, we
define the set of formulas $\varPhi_{\beta}$ as

$\varPhi_{\beta}=\\{{(\lnot)^{t_{1}}\varphi_{1}\wedge(\lnot)^{t_{2}}\varphi_{2}\wedge\
...\ \wedge(\lnot)^{t_{n}}\varphi_{n}\,\mid\,t_{i}\in\\{{0,1}\\}}\\}$

Each member of $\varPhi_{\beta}$ is formula which is constructed by the
conjunction of $n$ terms, each term being either a member of $\beta$ or its
negation. Because $\beta$ has $n$ members, the size of $\varPhi_{\beta}$ is
$2^{n}$. It can be seen that for any $q\in St$ and $a\in\mathit{Agt}$, the
indistinguishablity classes of members of $\varPhi_{\beta}$ with respect to
$q$ and $a$ (Definition.5.2) are mutually exclusive and they partition
$[q]_{\sim_{a}}$ (with the same reasoning as explained in Section 5.2).

######  Definition .

For $m,n\in\mathbb{N}$, and $m\leqslant 2^{n}$, we define the set $T_{n,m}$ as
follows:

$T_{n,m}=\\{{(s_{1},s_{2},...,s_{2^{n}})\mid\forall
i.s_{i}\in\\{{0,1}\\},\,\sum_{i=1}^{2^{n}}s_{i}=2^{n}-m}\\}$

$T_{n,m}$ is the set of $\binom{2^{n}}{m}$ possible orderings of $0$s and
$1$s, such that the number of $1$s is $2^{n}-m$ and the number of $0$s is $m$.
If $t\in T_{n,m}$, then we refer to $j$th element of $t$ by $t(j)$ (which of
course could be either $0$ or $1$).

###### Proposition

If $\beta=\\{{\varphi_{1},...\varphi_{n}}\\}$ is a set of $n$ formulas then
for a model $M$, $q\in St$ and $a\in\mathit{Agt}$ we have

$M,q\models\mathcal{H}_{a}^{=\log m}\beta\ \Longleftrightarrow\
M,q\models_{\mathcal{K}}P_{m}(\varphi_{1},...,\varphi_{n})$

where $1\leq m\leq 2^{n}$ and $P_{m}(\varphi_{1},...,\varphi_{n})$ is defined
as below:

$P_{m}(\varphi_{1},...,\varphi_{n})=\bigvee_{t_{i}\in
T_{n,m}}((\lnot)^{t_{i}(1)}\mathcal{K}_{a}\lnot\alpha_{1}\wedge(\lnot)^{t_{i}(2)}\mathcal{K}_{a}\lnot\alpha_{2}\wedge...\wedge(\lnot)^{t_{i}(2^{n})}\mathcal{K}_{a}\lnot\alpha_{2^{n}})$,

and $(\alpha_{1},\alpha_{2},...,\alpha_{2^{n}})$ is any ordering on the
members of $\varPhi_{\beta}$.

###### Proof.

The idea of the proof is similar to the example in Section 5.2. By the way we
constructed $\varPhi_{\beta}$, we have that the members of the set
$\omega=\\{{[\alpha_{i}]_{a}^{q}\mid 1\leqslant i\leqslant 2^{n}}\\}$ are
mutually exclusive, and they partition $[q]_{\sim_{a}}$. Therefore
$M,q\models\mathcal{H}_{a}^{=\log m}\beta$ if and only if exactly $m$ members
of the set $\omega$ are non-empty. For any $i$, we have that
$[\alpha_{i}]_{a}^{q}$ is empty if and only if
$M,q\models\mathcal{K}_{a}\lnot\alpha_{i}$, and similarly
$[\alpha_{i}]_{a}^{q}$ is non-empty if and only if
$M,q\models\lnot\mathcal{K}_{a}\lnot\alpha_{i}$. Therefore
$M,q\models\mathcal{H}_{a}^{=\log m}\beta$ if and only if for some subsets
$\varPhi_{\beta}^{\prime}\subseteq\varPhi_{\beta}$ such that
$|\varPhi_{\beta}^{\prime}|=m$ , we have that
$\alpha\in\varPhi_{\beta}^{\prime}\Rightarrow
M,q\models\lnot\mathcal{K}_{a}\lnot\alpha_{i}$ and
$\alpha\in\varPhi_{\beta}\setminus\varPhi_{\beta}^{\prime}\Rightarrow
M,q\models\mathcal{K}_{a}\lnot\alpha_{i}$. This statement could be exactly
represented by the formula $P_{m}(\varphi_{1},...,\varphi_{n})$ defined as
above. ∎

For formulas of type $\mathcal{H}_{a}^{<\log m}\beta$ and
$\mathcal{H}_{a}^{>\log m}\beta$ the construction could be written as below:

$M,q\models\mathcal{H}_{a}^{<\log m}\beta\ \Longleftrightarrow\
M,q\models_{\mathcal{K}}P_{1}(\varphi_{1},...,\varphi_{n})\vee...\vee
P_{m-1}(\varphi_{1},...,\varphi_{n})$ $M,q\models\mathcal{H}_{a}^{>\log
m}\beta\ \Longleftrightarrow\
M,q\models_{\mathcal{K}}P_{m+1}(\varphi_{1},...,\varphi_{n})\vee...\vee
P_{2^{n}}(\varphi_{1},...,\varphi_{n})$

where $P(N)$ is defined as in Proposition A.

### Proof of Theorem 6.2

For introducing the proof of Theorem 6.2 we need some prerequisites which will
follow.

###### Lemma

In any concurrent game model $M$, if the outcome function contains only
reflexive transitions, then for any $A\subseteq\mathit{Agt}$ and any state
$q$:

  * •

$M,q\models\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}X\varphi$
iff $M,q\models E_{A}\varphi$.

  * •

$M,q\models\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}G\varphi$
iff $M,q\models E_{A}\varphi$.

  * •

$M,q\models\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\psi\,\mathcal{U}\,\varphi$
iff $M,q\models E_{A}\varphi$.

###### Proof.

The proof follows directly from the semantics of the temporal operators and
the fact that for any strategy $s_{A}\in\Sigma_{A}^{ir}$ and any $\lambda\in
out(q,s_{A})$, we have that $\lambda[i]=q$ for any $i\geq 0$. So in a sense
the agents can never ”escape” from the state $q$. As the indistinguishability
relation of the agents are also reflexive, it follows that the strategic
abilities of agents to bring about $\varphi$ in any future state is equivalent
to having mutual knowledge about $\varphi$ in the current state. ∎

######  Observation 1.

In any concurrent game model $M$, if the outcome function contains only
reflexive transitions and $\mathit{Agt}$ is a singleton (for example
$\mathit{Agt}=\\{{a}\\}$), then any formula in the language of ATLK has an
equivalent formula in Multiagent epistemic logic which does not have a higher
length. This follows from the lemma A and that in this model $E_{A}$ is
equivalent to $\mathcal{K}_{a}$.

######  Definition .

For $n\in\mathbb{N}$, we define
$M^{n}=\\{{\mathit{Agt}^{n},St^{n},\\{{\sim_{a}\mid
a\in\mathit{Agt}}\\},\mathit{Act}^{n},d^{n},\mathit{out}^{n},\mathit{Pv}^{n},\mathit{V}^{n}}\\}$
to be a concurrent epistemic game model, such that
$\mathit{Agt}^{n}=\\{{a}\\}$, $St^{n}=\\{{0,...,2^{n}-1}\\}$,
$\mathit{Pv}^{n}=\\{{p_{1},...,p_{n}}\\}$ and $s\sim_{a}t,\forall s,t\in St$.
We allow $\mathit{Act}^{n}$, $d^{n}$ to be defined arbitrarily, and the
transition function $\mathit{out}^{n}$ is reflexive. The valuation function
$\mathit{V}^{n}$ is defined as follows: If $d_{n}d_{n-1}...d_{1}$ is the
binary representation of the number $t\leqslant 2^{n}-1$, then in state $t\in
St$, we let $p_{i}$ be true iff $d_{i-1}=1$. In other words, we let the set of
$n$ atomic propositions $\mathit{Pv}^{n}$ have a distinct valuation out of
$2^{n}$ possible combinations in each of $2^{n}$ states.

######  Definition .

For a given $n,j\in\mathbb{N}$, we define $N^{n}_{j}$ to be constructed by
removing state $j$ from $M^{n}$. We also modify $\sim^{n}$,
$\mathit{Act}^{n}$, $d^{n}$, $\mathit{V}^{n}$ and $\mathit{out}^{n}$ as needed
to be compatible be the removing of the state.

We denote the set of states of $N^{n}_{j}$ by $St^{n}_{j}$. We define
$\widetilde{N}^{n}_{j}$ to be the set of all pointed models $(N^{n}_{j},s)$,
where $s\in St^{n}_{j}$. Therefore $\widetilde{N}^{n}_{j}$ contains $2^{n}-1$
pointed models, corresponding to each of $2^{n}-1$ states of $N^{n}_{j}$. For
any $t\in St^{n}$, we define $(M^{n},t)^{+}$ to be any set of pointed models
that contains $(M^{n},t)$. Similarly $(N^{n}_{j},t)^{+}$ could be any set of
pointed models that contain $(N^{n}_{j},t)$ (therefore, these terms are not
referring to specific sets, but rather they show a property of a set of
pointed models).

######  Observation 2.

If $n>1$, then $\forall p_{i}\in\mathit{Pv}^{n},\forall s\in St^{n}$, there
exists $t\in St^{n},t\neq s$ such that $s$ and $t$ have same valuation for
$p_{i}$. This is true, because for $n>1$, $M^{n}$ has at least 4 states, and
each $p_{i}$ holds in at least 2 of them, and does not hold in at least 2
other states.

######  Observation 3.

If $(M^{n},t)\in A$ and $(N^{n}_{j},t)\in B$, then the spoiler cannot play an
atomic move in a node which is labeled by $\langle A\circ B\rangle$ or
$\langle B\circ A\rangle$. Because state $t$ prevents any
$p\in\mathit{Pv}^{n}$ to hold on all models on the left side and to not hold
on all models on the right side.

We will use the models $M^{n}$ and $N^{n}_{j}$ to construct our proof.
Throughout the proof, we will create a formula size game tree. As we saw
before, every node in a formula size game tree is labeled with a pair of sets
of pointed models. Below we define six types of nodes, parameterized by a
given state $j\in St^{n}$, based on properties of their labels.

  * •

$\mathbf{S1_{j}}$: The label could be represented by
$\langle(M^{n},t)^{+}\circ(N^{n}_{j},t)^{+}\rangle,\,\exists t\neq j$

  * •

$\mathbf{S2_{j}}$: The label could be represented by
$\langle(N^{n}_{j},t)^{+}\circ(M^{n},t)^{+}\rangle,\,\exists t\neq j$

  * •

$\mathbf{S3_{j}}$: The label could be represented by
$\langle\widetilde{N}^{n}_{j}\circ(M_{n},j)\rangle$

  * •

$\mathbf{S4_{j}}$: The label could be represented by
$\langle(M^{n},j)\circ\widetilde{N}^{n}_{j}\rangle$

  * •

$\mathbf{S5_{j}}$: The label could be represented by
$\langle(N^{n}_{j},t)^{+}\circ(M^{n},j)\rangle,\,\exists t\neq j$

  * •

$\mathbf{S6_{j}}$: The label could be represented by
$\langle(M^{n},j)\circ(N^{n}_{j},t)^{+}\rangle,\,\exists t\neq j$

Next, we investigate that if in a FSG, a node has one of the above types, what
will be the result of each of the spoiler’s possible moves. In particular, we
are interested to see a) whether the spoiler can close a node of a certain
type be playing one of her moves, and b) if it is not closed then, what type
of child nodes will be generated.

$\mathbf{S1_{j}}$, defined by
$\langle(M^{n},t)^{+}\circ(N^{n}_{j},t)^{+}\rangle,\,\exists t\neq j$
\- Atomic move is not possible (by observation 3).
\- Or move will generate at least one child node of type $\mathbf{S1_{j}}$.
Because it splits the set of pointed models on the left side, therefore
$(M^{n},t)$ will end up on the left side of one of the child nodes.
\- Knows move will generate a child node of type $\mathbf{S1_{j}}$. Because it
expands the pointed models on the left side to $\\{{(M^{n},s)|\,\forall s\in
St^{n}}\\}$. Therefore, no matter how we generate the right side, we can
always select one of the pointed models on the right side which are of form
$(N^{n}_{j},t)$ (for some $t\in St^{n}_{j}$) and because $t\in St^{n}$,
therefore $(M^{n},t)$ will be included on the left side. Hence the child node
is of type $\mathbf{S1_{j}}$.
\- Not move will generate a child node of type $\mathbf{S2_{j}}$. Because it
just reverses the pointed models on right side and left side.

$\mathbf{S2_{j}}$, defined by
$\langle(N^{n}_{j},t)^{+}\circ(M^{n},t)^{+}\rangle,\,\exists t\neq j$
\- Atomic move is not possible (by observation 3).
\- Or move will generate at least one child node of type $\mathbf{S2_{j}}$.
Because it splits the set of pointed models on the left side, therefore
$(N^{n}_{j},t)$ will end up on the left side of one of the child nodes.
\- Knows move will generate a child node of either type $\mathbf{S2_{j}}$ or
$\mathbf{S3_{j}}$. By playing the knows move (which could be only
$\mathcal{K}_{a}$ move), the left side of the label in the generated node will
be expanded to $\widetilde{N}^{n}_{j}$. On the right side, we either select
pointed models such that at least for one $(M^{n},t)$ among them,
$(N^{n}_{j},t)$ exists on the left side, in which case the resulting node will
be of type $\mathbf{S2_{j}}$. Or we select the pointed models on the right
side such that for no $(N^{n}_{j},t)$ on the left side there exist a
$(M^{n},t)$ on the right side. This can happen only if the new generated node
is labeled with $\langle\widetilde{N}^{n}_{j}\circ(M_{n},j)\rangle$, which
means it is of type $\mathbf{S3_{j}}$.
\- Not move will generate a child node of type $\mathbf{S1_{j}}$. Because it
just reverses the pointed models on right side and left side.

$\mathbf{S3_{j}}$, defined by
$\langle\widetilde{N}^{n}_{j}\circ(M_{n},j)\rangle$
\- Atomic move is not possible. Because by observation 3, for any
$p\in\mathit{Pv}^{n}$ which is not true in $j$, there is $s\in St^{n}_{j}$
where where $p$ does not hold in $s$ too, therefore no atomic proposition
could close this node.
\- Or move will generate at least one child node of either type
$\mathbf{S3_{j}}$ or $\mathbf{S5_{j}}$. If we select the all the pointed
models on the left side, to be the left side of a child node, then the label
of that child node is the same as this node and therefore it is also of type
$\mathbf{S3_{j}}$. Otherwise we can select any of the child nodes generated by
or move and one of the pointed models $(N^{n}_{j},t)$ on its left side.
Because $t\neq j$, this node’s label will be of type $\mathbf{S5_{j}}$.
\- Knows move will generate a child node of either type $\mathbf{S2_{j}}$ or
$\mathbf{S3_{j}}$. By playing the knows move (which could be only
$\mathcal{K}_{a}$ move), the left side of the label in the generated node will
remain to be $\widetilde{N}^{n}_{j}$. On the right side, we either select
$(M^{n},t),t\neq j$, in which case $(N^{n}_{j},t)$ exists on the left side,
and therefore the resulting node will be of type $\mathbf{S2_{j}}$. Or we
select the pointed model $(M^{n},j)$, in which case the label of the child
node stays intact and hence is of type $\mathbf{S3_{j}}$.
\- Not move will generate a child node of type $\mathbf{S4_{j}}$. Because it
just reverses the pointed models on right side and left side.

$\mathbf{S4_{j}}$, defined by
$\langle(M^{n},j)\circ\widetilde{N}^{n}_{j}\rangle$
\- Atomic move is not possible. Because by observation 3, for every
$p\mathit{Pv}^{n}$, there is $s\in St^{n}_{j},s\neq j$ such that $p$ does hold
in both $s$ and $j$, therefore no atomic proposition could close this node.
\- Or move will generate a node of type $\mathbf{S4_{j}}$. This is because the
set of pointed models on the left side of this node has only one member, so at
least one of the child nodes will have a similar label as of this one, which
is of type $\mathbf{S4_{j}}$.
\- Knows move will generate a child node of $\mathbf{S1_{j}}$. Because after a
knows move (which could be only $\mathcal{K}_{a}$ move), the left side of the
label in the generated node will be $\\{{(M^{n},s)|\ \forall s\in St^{n}}\\}$.
Therefore no matter how we generate the pairs on the right side, for any
chosen pair $(N^{n}_{j},t)$ on the right side $(M^{n},t)$ exists on the left
side, and therefore the resulting node would be of type $\mathbf{S1_{j}}$.
\- Not move will generate a child node of type $\mathbf{S3_{j}}$. Because it
just reverses the pointed models on right side and left side.

$\mathbf{S5_{j}}$, defined by
$\langle(N^{n}_{j},t)^{+}\circ(M^{n},j)\rangle,\,\exists t\neq j$
\- Atomic move is possible. If it is played, then the node will be closed and
there won’t be any further child. Notice that we are not saying the for every
node of type $\mathbf{S5_{j}}$ the atomic move is possible. What we state is
that by the definition of this type alone, we cannot discard the possibility
of an atomic move, and this will be enough for our purpose.
\- Or move will generate a child node of type $\mathbf{S5_{j}}$. Because for
all $(N^{n}_{j},t)$ on the left side of this node’s label, we have that $t\neq
j$. Therefore any subset of it also retains this property and hence an or move
will generate at least one child node of type $\mathbf{S5_{j}}$.
\- Knows move will generate at least one node of either type $\mathbf{S3_{j}}$
or $\mathbf{S2_{j}}$. The reasoning is similar to the knows move for the node
type $\mathbf{S3_{j}}$.
\- Not move will generate a child node of type $\mathbf{S6_{j}}$. It follows
directly from the definitions of node types $\mathbf{S5_{j}}$ and
$\mathbf{S6_{j}}$.

$\mathbf{S6_{j}}$, defined by
$\langle(M^{n},j)\circ(N^{n}_{j},t)^{+}\rangle,\,\exists t\neq j$
\- Atomic move is possible. Again, this only means that only by the definition
of type $\mathbf{S6_{j}}$, we cannot reject the possibility of an atomic move,
which will be enough for our proof.
\- Or move will generate a child node of type $\mathbf{S5_{j}}$. The reasoning
is similar to the or move of node type $\mathbf{S4_{j}}$.
\- Knows move will generate a child node of type $\mathbf{S1_{j}}$. The
reasoning is similar to the knows move of node type $\mathbf{S4_{j}}$.
\- Not move will generate a child node of type $\mathbf{S6_{j}}$. It follows
directly from the definitions of node types $\mathbf{S5_{j}}$ and
$\mathbf{S6_{j}}$.

Any node which is tagged with a type $\mathbf{S1_{j}}$ to $\mathbf{S6_{j}}$
defined as above is called a typed node.

######  Observation 4.

If the spoiler wins a FSG starting from a root of type $\mathbf{S1_{j}}$, then
the game tree has at least one leaf of either type $\mathbf{S5_{j}}$ or
$\mathbf{S6_{j}}$ (with a singleton set containing $(M^{n},j)$ on one side of
the label of that leaf).

To see why, notice that every move that the spoiler plays at each step will
generate at least one typed node parameterized by $j$ as a child. So if we
create a path from the root downwards the tree, containing only typed nodes
parameterized by $j$, this path can end only by the node being closed at some
point. As we assumed that the spoiler wins the FSG, then all paths from the
root has to end in a leaf. Among the node types, the spoiler can close the
node only when the type is $\mathbf{S5_{j}}$ or $\mathbf{S6_{j}}$. Therefore,
any path that contains only of typed nodes parameterized by $j$ has to end in
a node of types either $\mathbf{S5_{j}}$ or $\mathbf{S6_{j}}$.

Now we have enough prerequisite materials to construct our proof:

###### Proof.

(Proof of Theorem 6.2)

For every $n\in\mathbb{N}$, we define the formula $\varphi_{n}\in Lang(ATHL)$
as:

$\varphi_{n}=\mathcal{H}_{a}^{=n}\beta_{n}$

where $\beta_{n}=\\{{p_{1},...,p_{n}}\\}$. The size of $\varphi_{n}$ is
$f(n)=n$, which is strictly increasing (and linear) in $n$. Also for every
$n\in\mathbb{N}$, we define two set of pointed models $A_{n}$ and $B_{n}$ as
below:

$A_{n}=\\{{(M^{n},0)}\\}$, $B_{n}=\\{{(N^{n}_{j},0)\mid
j\in\mathbb{N},\,1\leqslant j\leqslant 2^{n}-1}\\}$

where $M^{n}$ and $N^{n}_{j}$ are defined as in Definitions A and A. So
$A_{n}$ contains a single pointed model $(M^{n},0)$, and $B_{n}$ is
constructed by summing all possible ways that we can remove one of the states
of $(M^{n},0)$, other than state 0. Therefore $B_{n}$ consists of $2^{n}-1$
pointed models.

It holds that $A_{n}\models_{\mathcal{H}}\varphi_{n}$, because $M^{n}$ has
$2^{n}$ states and the set $\beta_{n}=\mathit{Pv}^{n}$ has a distinct
combination of values in each of those $2^{n}$ states, which are all in the
same indistinguishability class for agent $a$ from state $0$. Therefore
$|R_{a,0}(\beta)|=2^{n}$, and so
$M,0\models_{\mathcal{H}}\mathcal{H}_{a}^{=n}\beta_{n}$. It is also true that
$B_{n}\models_{\mathcal{H}}\lnot\varphi_{n}$, because for all
$j\in\mathbb{N}$, $N^{n}_{j}$ has $2^{n}-1$ states, and so regardless of the
valuations of atomic propositions in those states, $|R_{a,0}(\beta)|\leqslant
2^{n}-1<2^{n}$. Hence $\log{|R_{a,0}(\beta)|}<\log{2^{n}}=n$. It follows that
$(N^{n}_{j},0)\models_{\mathcal{H}}\mathcal{H}_{a}^{<n}$, which means
$(N^{n}_{j},0)\models_{\mathcal{H}}\lnot\mathcal{H}_{a}^{=n}$.

So we have $A_{n}\models_{\mathcal{H}}\varphi_{n}$ and
$B_{n}\models_{\mathcal{H}}\lnot\varphi_{n}$. Now to prove the succinctness
theorem, by definition 6.1 we need to show that the shortest formula
$\psi_{n}\in Lang(ATEL)$ which is equivalent to $\varphi_{n}$, has the size of
at least $2^{n}$. Assume $\psi_{n}^{\prime}$ is the shortest formula in
$Lang(ATEL)$ which is equivalent to $\varphi_{n}$. By Observation 1, there
exist a formula $\psi_{n}$ in $Lang(MEL)$ which is not longer than
$\psi_{n}^{\prime}$. By theorem 6.1, the spoiler can win the FSG game starting
at $\langle A_{n}\circ B_{n}\rangle$. If $k$ is the lowest number of moves
that the spoiler can win the FSG game starting at $\langle A_{n}\circ
B_{n}\rangle$, then by theorem 6.1, $k$ is a lower bound for the size of
$\psi_{n}$. Now consider that the spoiler actually plays and wins this FSG
game and constructs this winning tree. We will tag each node of this tree by
its type, based on the types $\mathbf{S1_{j}}$ to $\mathbf{S6_{j}}$ that we
defined before. We start from the root. For each $1\leqslant j\leqslant
2^{n}-1$, we can tag the root of this tree as type $\mathbf{S1_{j}}$ by
replacing $t=0$ in the definition of type $\mathbf{S1_{j}}$. Therefore, by
observation 4, this tree has at least one leaf of either type
$\mathbf{S5_{j}}$ or $\mathbf{S6_{j}}$ for each $1\leqslant j\leqslant
2^{n}-1$. Because we have $2^{n}-1$ choice for $j$, and because no node can be
of types $\mathbf{S5_{j}}$ or $\mathbf{S6_{j}}$, and at the same time of types
$\mathbf{S5_{i}}$ or $\mathbf{S6_{i}}$ for $i\neq j$, therefore this tree has
at least $2^{n}-1$ distinct leaves. Moreover, because the root is of type
$\mathbf{S1_{j}}$ and cannot be closed with the first move, the tree has at
least one no-root/no-leaf node. So to win this game the spoiler has to play at
least $2^{n}$ moves, and because this is a lower bound on the size of
$\psi_{n}$, we have that $|\psi_{n}|\geqslant 2^{n}$. As $\psi_{n}^{\prime}$
can only be longer than $\psi$, it follows that $|\psi_{n}^{\prime}|\geqslant
2^{n}$.

So we showed that for any $n\in\mathbb{N}$, we can define a $\varphi_{n}\in
Lang(ATHL)$ with length $n$, such that the shortest $\psi_{n}^{\prime}\in
Lang(ATEL)$ which is equivalent to $\varphi_{n}$ has at least the length of
$2^{n}$. By definition 6.1 this proves that ATLH is exponentially more
succinct than ATLK. ∎