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

TL;DR

This paper introduces ATLH, an extension of ATL with quantitative uncertainty measures, allowing for nuanced specifications of agents' knowledge and secrecy, while maintaining similar complexity and increased succinctness.

Contribution

The paper presents ATLH, a new logic that incorporates uncertainty quantification into ATL, enhancing expressiveness and succinctness without increasing complexity.

Findings

ATLH has the same expressivity as ATLK.

Model checking complexity remains unchanged.

ATLH is exponentially more succinct than ATLK.

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 \phi. Such properties can be e.g. expressed in ATLK, that is, alternating-time temporal logic ATL extended with epistemic operators. In many realistic scenarios, however, players do not need to fully learn the truth value of \phi. They may be almost as well off by gaining some knowledge; in other words, by reducing their uncertainty about \phi. Similarly, in order to keep \phi secret, it is often insufficient that the intruder never fully learns its truth value. Instead, one needs to require that his uncertainty about \phi never drops below a reasonable threshold. With this motivation in mind, we introduce the logic ATLH, extending ATL 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 ATLH has the same expressivity and model checking complexity as ATLK. However, the new logic is exponentially more succinct than ATLK, which is the main technical result of this paper.

Equations

$$M,s_0$$

$$\wedge$$

$$M,s_0$$

$$G\neg ({\mathcal{K}}_c{V}_A\vee {\mathcal{K}}_c\neg V_A\vee {\mathcal{K}}_c{V}_B\vee {\mathcal{K}}_c\neg V_B))$$

$$\wedge ⟨⟨v⟩{⟩}_{{}_{}}F(Voted\wedge V_A\wedge \neg V_B\wedge$$

$$G\neg ({\mathcal{K}}_c{V}_A\vee {\mathcal{K}}_c\neg V_A\vee {\mathcal{K}}_c{V}_B\vee {\mathcal{K}}_c\neg V_B))$$

$$\wedge ⟨⟨v⟩{⟩}_{{}_{}}F(Voted\wedge \neg V_A\wedge V_B\wedge$$

$$G\neg ({\mathcal{K}}_c{V}_A\vee {\mathcal{K}}_c\neg V_A\vee {\mathcal{K}}_c{V}_B\vee {\mathcal{K}}_c\neg V_B))$$

$$\wedge ⟨⟨v⟩{⟩}_{{}_{}}F(Voted\wedge \neg V_A\wedge \neg V_B\wedge$$

$$G\neg ({\mathcal{K}}_c{V}_A\vee {\mathcal{K}}_c\neg V_A\vee {\mathcal{K}}_c{V}_B\vee {\mathcal{K}}_c\neg V_B))$$

$$\nexists q^{\prime }\text{ s.t }{q}^{\prime }{\sim }_{a}q\text{ and }M,q^{\prime }\models C$$

$$\iff$$

$$P({\phi }_1,{\phi }_2)=$$

$$\wedge \neg {\mathcal{K}}_a\neg (\neg {\phi }_1\wedge {\phi }_2)\wedge \neg {\mathcal{K}}_a\neg (\neg {\phi }_1\wedge \neg {\phi }_2))$$

$$\vee$$

$$\wedge \neg {\mathcal{K}}_a\neg (\neg {\phi }_1\wedge {\phi }_2)\wedge \neg {\mathcal{K}}_a\neg (\neg {\phi }_1\wedge \neg {\phi }_2))$$

$$\vee$$

$$\wedge {\mathcal{K}}_a\neg (\neg {\phi }_1\wedge {\phi }_2)\wedge \neg {\mathcal{K}}_a\neg (\neg {\phi }_1\wedge \neg {\phi }_2))$$

$$\vee$$

$$\wedge \neg {\mathcal{K}}_a\neg (\neg {\phi }_1\wedge {\phi }_2)\wedge {\mathcal{K}}_a\neg (\neg {\phi }_1\wedge \neg {\phi }_2)).$$

Full text

With this motivation in mind, we introduce the logic \ATLH, 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 \ATLHhas the same expressivity and model checking complexity as \ATLK. However, the new logic is exponentially more succinct than \ATLK, which is the main technical result of this paper.

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 \ATLK.

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.

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 \ATLKas follows:

[TABLE]

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:

[TABLE]

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 \ATLKthat 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.

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 \thetheorem (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 \ATLHis 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 \ATLHare:

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 \ATLH. 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 \ATLKfor 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 \ATLHis 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 **\thetheorem

If $\varphi$ is an \ATLHformula 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 **\thetheorem

Model checking of \ATLHfor 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 \ATLHsubsumes $\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 \ATLH

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 \thetheorem (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

{theorem}

$\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 \ATLHwould be expressed as $M,q\models_{\mathcal{H}}\varphi\wedge\mathcal{H}_{a}^{=0}\{{\varphi}\}$. ∎

5.2. Uncertainty as Knowledge

{theorem}

ATLK is at least as expressive as \ATLH.

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 \thetheorem (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:

[TABLE]

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:

[TABLE]

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 \thetheorem (Length of formulas in \ATLH).

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 \thetheorem (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 \thetheorem (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.

{theorem}

[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. \ATLHIs More Succinct than \ATLK

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

{theorem}

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}$. ∎

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 \ATLK. In a similar way, we can use \ATLKto 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 \ATLKexpression. 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 \ATLH

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 \ATLHas 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 \ATLK, it is not secure when we define the security requirement as an information-theoretic property, and formalize it in \ATLH.

8. Conclusion

In this work, we introduce the logic \ATLHwhich extends alternating-time temporal logic ATL with quantitative modalities based on the Hartley measure of uncertainty. As the main technical result, we show that \ATLHhas the same expressive power and the same model checking complexity as \ATLK(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 \ATLKand \ATLHhave 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 \ATLHwill be exponentially faster than in \ATLK. 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 \ATLHin a much more intuitive way than in \ATLK. Understanding the information-theoretic intuition of a corresponding \ATLKformula 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 \ATLHas an extension of the STV Kurpiewski et al. (2021) or MCMAS Lomuscio et al. (2017) model checkers.

{acks}

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).

Appendix A Detailed Proofs

Proof of Theorem 5.2

Theorem**.**

ATLK is at least as expressive as \ATLH.

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 \thetheorem.

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 \thetheorem.

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 [math]s and $1$s, such that the number of $1$s is $2^{n}-m$ and the number of [math]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 [math] or $1$).

**Proposition **\thetheorem

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 **\thetheorem

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 \thetheorem.

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 \thetheorem.

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 [math]. 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. ∎