# Bisimulations for Verifying Strategic Abilities
with an Application to the ThreeBallot Voting Protocol

Francesco Belardinelli  Imperial College London, UK, and Université d’Evry,
France  Rodica Condurache  LACL, Université Paris-Est Créteil, France  Cătălin
Dima  Wojciech Jamroga  Institute of Computer Science, Polish Academy of
Sciences, Poland  Michal Knapik

###### Abstract

We propose a notion of alternating bisimulation for strategic abilities under
imperfect information. The bisimulation preserves formulas of ATL∗ for both
the objective and subjective variants of the state-based semantics with
imperfect information, which are commonly used in the modeling and
verification of multi-agent systems. Furthermore, we apply the theoretical
result to the verification of coercion-resistance in the ThreeBallot voting
system, a voting protocol that does not use cryptography. In particular, we
show that natural simplifications of an initial model of the protocol are in
fact bisimulations of the original model, and therefore satisfy the same ATL∗
properties, including coercion-resistance. These simplifications allow the
model-checking tool MCMAS to terminate on models with a larger number of
voters and candidates, compared with the initial model.

###### keywords:

Alternating-time Temporal Logic , Bisimulations , Voting Protocols , Formal
Verification.

††journal: Information & Computation

##  1 Introduction

Formal languages for expressing strategic abilities of rational agents have
witnessed a steady growth in recent years [1, 2, 3]. Among the most
significant contributions we mention Alternating-time Temporal Logic [4, 5],
(possibly enriched with strategy contexts [6]), Strategy Logic [7, 8], and
Coalition Logic [9]. These languages allow to express that a group of agents
has a strategy to enforce a certain outcome, regardless of the behavior of the
other agents. That provides syntactical and semantic means to characterize
winning conditions in multi-player games, notions of equilibrium (e.g. Nash),
strategy-proofness, and so on [7, 10, 11, 12].

However, if logics for strategies are to be applied to the specification and
verification of multi-agent systems (MAS) [13, 14, 15], they need to be
coupled with efficient model checking techniques. Unfortunately, while in
contexts of perfect information we benefit from tractable algorithms for model
checking [5], the situation is rather different once we consider imperfect
information. In contexts of imperfect information the complexity of the
verification task ranges between $\Delta^{P}_{2}$-completeness [16] to
undecidability [17], depending on whether we assume perfect recall. In this
setting, complementary model checking techniques are being investigated, in
order to make the problem feasible in practice, including semantic [18, 19]
and syntactic restrictions [20], as well as approximations [21].

Amongst these, model reduction seems one of the more promising paths. In
particular, reductions by state- and action-space abstraction have proved to
be a valuable tool for efficient verification [22, 23, 24], also in the
context of strategic abilities [10, 25, 26, 27]. Within that approach, the
“concrete” system $S$ to be model-checked is abstracted into a “simpler” model
$S^{A}$, which typically contains less states and transitions and therefore
can be easier to verify. Then, the verification result is transferred from
abstraction $S^{A}$ to the concrete $S$ by virtue of some preservation result.
Normally, preservation is guaranteed by proving that abstraction $S^{A}$ is
_similar_ or _bisimilar_ to $S$. (Bi)simulations are a powerful tool to
analyze the expressiveness of modal languages, starting with van Benthem’s
characterisation of modal logic as the bisimulation-invariant fragment of
first-order logic [28]. However, (bi)simulations are a lot less understood in
logics for strategies, where they have been studied mostly in the contexts of
perfect information scenarios [29, 30, 31].

In this paper, we advance the state-of-the-art by introducing simulations and
bisimulations for alternating-time temporal logic under imperfect information.
We prove that these (bi)simulations preserve the interpretation of formulas
for the whole syntax of ATL∗, when interpreted with imperfect information and
imperfect recall, for both the objective and subjective variants of the
semantics [2, 32]. Most interestingly for MAS verification, we apply the
(bi)simulations to the model reduction of a class of electronic voting
protocols without encryption.

Electronic voting is often considered as an attractive alternative to paper-
based elections and referendums due to a number of advantages: increased
accessibility, availability, voter turnout, cost-efficiency, and usability, as
well as speed and accuracy of the voting, counting and publication processes.
However, electronic voting poses a number of challenges: resistance to
coercion and other types of fraud, secrecy, anonymity, verifiability,
democracy (the right to vote at most once), accountability, etc. Those threats
exist also in paper voting, but the use of technology magnifies their scope
and potential impact. There are also other issues, specific to electronic
voting, such as limited access to technology and complex interaction between
technology and public understanding and trust in the procedure [33, 34]. In
this paper, we focus on the property of _coercion resistance_ that captures
the voters’ ability to choose freely how they vote: whatever course of action
the coercer adopts, the voter always has a strategy to vote as they intend
while appearing to comply with the coercer’s requirements.

An increasing amount of research has focused recently on the verification of
many of these properties for various types of voting protocols [35, 36]. The
frameworks used for modeling and verifying security properties of voting
protocols include, to mention only a few, process calculi such as the applied
$\pi$-calculus or _CSP_ [37, 38, 39], rewriting-based approaches [40, 41, 42],
approaches based on flat transition systems etc.

In this paper, we show how our bisimulation can be used to obtain significant
model reductions for some voting protocols. In consequence, we develop a
verification procedure for those voting protocols, based on the multi-agent
approach. The main advantage of multi-agent logics is the provision of a
unified specification language for a vast array of properties. Due to that
feature, the logics can for instance serve to disambiguate the variety of
informal intuitions behind coercion resistance that are found in the
literature, cf. [43]. Moreover, multi-agent logics allow for a more flexible
and expressive specification of variants of coercion-resistance, involving
explicit references to the dynamics of attacker’s knowledge, as well as the
(non)existence of strategies suitable for the attacker and/or the voter. The
same applies to specification of other important properties, such as
individual verifiability, end-to-end (universal) verifiability, and
accountability.

Here, we focus on a particular formalization of coercion resistance, and
verify it for a simplified version of the ThreeBallot voting protocol [44,
45]. Our first results in this line already allow for verification of models
with a larger number of voters and candidates compared to the approach based
on process calculi in [46, 47]. Even more importantly, our experiments show
that bisimulation-based reductions can turn verification from a utterly
difficult task to something feasible in practice.

###  1.1 Structure of the Paper and Technical Contributions

The article is structured as follows. In Section 2, we introduce the syntax
and semantics of ATL∗ interpreted under the assumption of imperfect
information and imperfect recall. In Section 3, we propose the novel relations
of simulation and bisimulation for the setting. Moreover, we prove the main
theoretical result of this paper, namely that the bisimulation preserves the
interpretation of ATL∗ formulas. In Section 4, we show that our notion of
bisimulation does not enjoy the Hennessy-Milner property, and we discuss some
necessary conditions for two models to be logically equivalent. The results
highlight some interesting features of the current semantics of ATL∗ with
imperfect information, and might point to a novel semantics for logics of
strategic ability. Further, in Section 5, we present our case study based on
the ThreeBallot voting protocol. We formalize ThreeBallot as a game structure,
and provide two abstractions of the protocol. Then, we point out that the
abstractions are indeed bisimilar with the original game structure. Finally,
in Section 6, we evaluate the gains in terms of verification time, by
comparing model checking of the abstractions to model checking of the original
model. We conclude in Section 7, and indicate some future directions of
research.

Previous version of the material. This work extends and revises the results
presented in the conference paper [48]. The main technical differences are as
follows. First, our results are now given for the whole language of ATL∗,
while [48] considered only its restricted fragment ATL. Secondly, we correct a
mistake in the main preservation result. In the previous version, we
erroneously used a weaker notion of bisimulation, which actually does not
preserve even formulas of ATL. We discuss the details, and point out some
differences between the two definitions in Section 3.3. Thirdly, we report
completely new theoretical research in Section 3.4 (computational complexity
of checking for bisimulation) and Section 4 (Hennessy-Milner property and
necessary conditions for logical equivalence of models). Finally, we revise
the implementation of our ThreeBallot models, and present entirely new
experimental results. In particular, we extend our model checking experiments
to the imperfect information semantics of ATL, for which the bisimulation-
based reductions were in fact designed.

Regarding the presentation, we add a running example, and streamline the
introduction of the bisimulation, in order to make the concept easier to
understand.

###  1.2 Related Work

The literature on both logics for strategies and the formal verification of
voting protocols is extensive and rapidly growing. Hereafter we only consider
the works most closely related to the present contribution.

Bisimulations for ATL. An in-depth study of model equivalences induced by
various temporal logics appears in [30]. Bisimulations for ATL∗ with perfect
information have been introduced in [29]. Since then there have been various
attempts to extend these to more expressive languages (including Strategy
Logic recently [49]), as well as to contexts of imperfect information [31,
50]. In [50, 51] non-local model equivalences for ATL with imperfect
information have been put forward. However, these works do not deal with the
imperfect information/imperfect recall setting here considered, nor do they
provide a local account of bisimulations. Finally, in [48] we provided a
different notion of bisimulation for ATL only with imperfect information and
imperfect recall. We remarked in the introduction that such definition was
flawed and provided a counterexample in Section 3.3. The present contribution
is also aimed at rectifying this result.

Verification of Voting Protocols. Our work is inspired by recent contributions
on the verification of voting protocols, mostly by using the $\pi$-calculus
and _CSP_ [37, 38, 39]. Some existing attempts at verification of e-voting
protocols follow this approach by using one of the security verifiers [52,
53], or even a general equivalence checker for a process algebra [46, 47, 54],
where privacy-type and anonymity properties of the protocols are verified by
using CSP. An important strand in verification of voting protocols is based on
specifications in first-order logic or linear logic. The verification is done
by means of theorem proving [55, 56, 57, 58] or bounded model checking (BMC)
[35, 59, 60, 61]. In particular [61] presents a BMC-based analysis of risk-
limiting audits and [58] applies theorem proving to automated verification of
the Selene voting protocol. In [35] the authors define two semantic criteria
for single transferable vote (STV) schemes, then show how BMC and SMT solvers
can be used to check whether these criteria are met. In [47] the authors
construct CSP models of the ThreeBallot system and use them to produce an
automated formal analysis of their anonymity properties. Finally, some
challenges and solutions for verification of end-to-end verifiable systems
were addressed in [62, 63].

An issue that can be identified with many of the above approaches is that the
description of the system, and the property to be verified, are not clearly
distinguished. We emphasize that multi-agent logics allow for a clear
separation of the two. Moreover, they provide a wider variety of properties,
including ones that are related to the existence of the attacker’s strategies.
Last but not least, they give reasonable hope for interesting verification
performance. In our experiments, we have been able to model-check ThreeBallot
models with 5 voters and 2 candidates, or 4 candidates and 3 voters, while
e.g. the results in [47] are provided for at most 3 voters and 2 candidates.
In this respect, the closest work to ours is the recent paper [64], presenting
some experimental results for verification of the voting protocol SELENE,
based on the multi-agent logic ATLir.

##  2 The Formal Setting

In this section, we introduce the syntax of the Alternating-time Temporal
Logic ATL∗ [5], and present its semantics for agents with imperfect
information and imperfect recall, defined on imperfect information concurrent
game structures (iCGS). The assumption of _imperfect information_ means that
agents can only partially observe the global state of the system. Thus, they
have to make their decisions, and execute their strategies, with only partial
knowledge about the current situation. The assumption of _imperfect recall_
means that they do not necessarily memorize all of their past observations.
This does not mean that the agents have no memory at all. However, an agent’s
recall of the past must be encapsulated in the current local state of the
agent.

The formal definitions and notation follow [17].

###  2.1 Concurrent Game Structures

Concurrent game structures have originally been introduced in [5] in a perfect
information setting. Here we consider their version for contexts of imperfect
information [65].

######  Definition 1.

A concurrent game structure with imperfect information, or iCGS, is a tuple
$\mathcal{G}=\langle Ag,AP,S,s_{0},Act,\\{\sim_{i}\\}_{i\in
Ag},d,\to,\pi\rangle$ such that

  * 1.

$Ag$ is a nonempty and finite set of _agents_. Subsets $A\subseteq Ag$ of
agents are called _coalitions_.

  * 2.

$AP$ is a set of _atomic propositions_ , or atoms.

  * 3.

$S$ is a non-empty set of _states_ and $s_{0}\in S$ is the _initial state_ of
$\mathcal{G}$.

  * 4.

$Act$ is a finite non-empty set of actions. A tuple $\vec{a}=(a_{i})_{i\in
Ag}\in Act^{Ag}$ is called a _joint action_.

  * 5.

For every agent $i\in Ag$, $\sim_{i}$ is an equivalence relation on $S$,
called the _indistinguishability relation_ for $i$.

  * 6.

$d:Ag\times S\to(2^{Act}\setminus\\{\emptyset\\})$ is the _protocol function_
, satisfying the property that, for all states $s,s^{\prime}\in S$ and any
agent $i$, $s\sim_{i}s^{\prime}$ implies $d(i,s)=d(i,s^{\prime})$. That is,
the same (non-empty) set of actions is available to agent $i$ in
indistinguishable states.

  * 7.

$\to\subseteq S\times Act^{Ag}\times S$ is the transition relation such that,
for every state $s\in S$ and joint action $\vec{a}\in Act^{Ag}$,
$(s,\vec{a},s^{\prime})\in\to$ for some state $s^{\prime}\in S$ iff $a_{i}\in
d(i,s)$ for every agent $i\in Ag$. We normally write $s\xrightarrow{\vec{a}}r$
for $(s,\vec{a},r)\in\to$.

  * 8.

$\pi:S\to 2^{AP}$ is the state-labeling function.

By Def. 1 at any given state $s$, every agent $i\in Ag$ can perform the
enabled actions in $d(i,s)$. A joint action $\vec{a}$ fires a transition from
state $s$ to some state $s^{\prime}$ only if each $a_{i}$ is enabled for agent
$i$ in $s$. Further, every agent $i$ is equipped with an indistinguishability
relation $\sim_{i}$, with $s\sim_{i}s^{\prime}$ meaning that $i$ cannot tell
state $s$ from state $s^{\prime}$, i.e., agent $i$ possesses the same
information, makes the same observation in the two states. In particular, the
same actions are enabled in indistinguishable states.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$q_{4}$$q_{5}$$q_{6}$$q_{7}$$\mathsf{{win_{1}}}$$q_{8}$$\mathsf{{win_{2}}}$$(vote_{1},-)$$(vote_{2},-)$$(flip,-)$$(pass,-)$$(pass,-)$$(flip,-)$$(-,pub)$$(-,pub)$$(-,pub)$$(-,pub)$2222$(-,np)$$(-,np)$$(-,np)$$(-,np)$$(-,-)$$(-,-)$
Figure 1: Simple model of 2-stage voting. Dotted lines represent
indistinguishability for agent 2 (the election official).

######  Example 1.

Consider a two-stage voting system with a simple anti-coercion mechanism. In
the first stage, the voter casts her vote for one of the candidates; we assume
for simplicity that there are only two candidates in the election. In the
second stage, the voter has the option to send a signal – by an independent
communication channel – that flips her vote to the other candidate. After
that, the election official publishes the result of the election (action
_pub_). However, a dishonest official can also decide not to publish the
outcome (action _np_). An iCGS modeling the scenario for a single voter
(represented by agent $1$) is depicted in Figure 1. The election official is
represented by agent $2$; the dotted lines indicate that the official does not
directly see the choices made by the voter. Note that this toy model is in
fact a turn-based game, i.e., in every state only a single agent has a choice
of decision while the other agent is passive.

Runs. Given an iCGS $\mathcal{G}$ as above, a run is a finite or infinite
sequence $\lambda=s_{0}\vec{a}_{0}s_{1}\ldots$ in $((S\cdot Act^{Ag})^{*}\cdot
S)\cup(S\cdot Act^{Ag})^{\omega}$ such that for every $j\geqslant 0$,
$s_{j}\xrightarrow{\vec{a}_{j}}s_{j+1}$. Given a run
$\lambda=s_{0}\vec{a}_{0}s_{1}\ldots$ and $j\geqslant 0$, $\lambda[j]$ denotes
the $j+1$-th state $s_{j}$ in the sequence; while $\lambda_{\geqslant j}$
denotes run $s_{j}\vec{a}_{j}s_{j+1}\ldots$ starting from $\lambda[j]$. We
denote by $Run(\mathcal{G})$ the set of all runs in iCGS $\mathcal{G}$. For a
coalition $A\subseteq Ag$ of agents, a joint $A$-action denotes a tuple
$\vec{a}_{A}=(a_{i})_{i\in A}\in Act^{A}$ of actions, one for each agent in
$A$. For coalitions $A\subseteq B\subseteq Ag$ of agents, a joint $A$-action
$\vec{a}_{A}$ _is extended_ by a joint $B$-action $\vec{b}_{B}$, denoted
$\vec{a}_{A}\sqsubseteq\vec{b}_{B}$, if for every $i\in A$, $a_{i}=b_{i}$.
Also, a joint $A$-action $\vec{a}_{A}$ is _enabled_ at state $s\in S$ if for
every agent $i\in A$, $a_{i}\in d(i,s)$.

Epistemic neighbourhoods. Given a coalition $A\subseteq Ag$ of agents, the
_collective knowledge relation_ $\sim^{E}_{A}$ is defined as $\bigcup_{i\in
A}\sim_{i}$, while the _common knowledge relation_ $\sim^{C}_{A}$ is the
transitive closure $(\bigcup_{i\in A}\sim_{i})^{+}$ of $\sim^{E}_{A}$. Then,
$C_{A}^{\mathcal{G}}(q)=\\{q^{\prime}\in S\mid q^{\prime}\sim_{A}^{C}q\\}$ is
the common knowledge neighbourhoods (CKN), of state $q$ for coalition $A$ in
the iCGS $\mathcal{G}$. We will omit the superscript $\mathcal{G}$ whenever it
is clear from the context.

Uniform strategies. We now recall a notion of strategy adapted to iCGS with
imperfect information [65].

######  Definition 2.

A _(uniform)_ strategy for an agent $i\in Ag$ is a function $\sigma:S\to Act$
that is compatible with $d$ and $\sim_{i}$, i.e.,

  * 1.

for every state $s\in S$, $\sigma(s)\in d(i,s)$;

  * 2.

for all states $s,s^{\prime}\in S$, $s\sim_{i}s^{\prime}$ implies
$\sigma(s)=\sigma(s^{\prime})$.

By Def. 2 a strategy has to be uniform in the sense that in indistinguishable
states it must return the same action. Such strategies are also known as
observational in the literature on game theory and control theory. Note that
in this paper we use memoryless strategies, whereby only the current state
determines the action to perform. This choice is dictated by the application
in hand, namely voting protocols, where the unbounded recall is not needed.
Namely, the information available to the agents is fully encoded in global
states together with help of indistinguishability relations111Therefore
memoryless strategies already encode the agent’s memory of all her past
observations.. Note that the finite memory of a given depth of recall can be
obtained in practical setting by introducing an adequate number of special
variables, i.e., dimensions in iCGSs whose states are valuations of variables.

Perfect recall strategies with imperfect information can be defined similarly,
as memoryless strategies on tree unfoldings of iCGS. We leave this extension
for future work.

A strategy for a coalition $A$ of agents is a set
$\sigma_{A}=\\{\sigma_{a}\mid a\in A\\}$ of strategies, one for each agent in
$A$. Given coalitions $A\subseteq B\subseteq Ag$, a strategy $\sigma_{A}$ for
coalition $A$, a state $s\in S$, and a joint $B$-action $\vec{b}_{B}\in
Act^{B}$ that is enabled at $s$, we say that $\vec{b}_{B}$ is _compatible
with_ $\sigma_{A}$ (in $s$) whenever $\sigma_{A}(s)\sqsubseteq\vec{b}_{B}$.
For states $s,s^{\prime}\in S$ and strategy $\sigma_{A}$, we write
$s\xrightarrow{\sigma_{A}(s)}r$ if $s\xrightarrow{\vec{a}}r$ for some joint
action $\vec{a}\in Act^{Ag}$ that is compatible with $\sigma_{A}$.

There exist two alternative semantics of strategic operators under imperfect
information, corresponding to two different notions of success for a strategy.
The idea of _subjective_ ability [66, 65] requires that a winning strategy
must succeed from all the states that the coalition considers possible in the
initial state of the play. The alternative notion of _objective_ ability [2]
assumes that it suffices for the strategy to succeed from the initial state
alone. Accordingly, we define two notions of the _outcome_ of a strategy
$\sigma_{A}$ at state $s$, corresponding to the objective and the subjective
interpretation of alternating-time operators. Fix a state $s$ and a strategy
$\sigma_{A}$ for coalition $A$.

  1. 1.

The set of _objective outcomes of $\sigma_{A}$ at $s$_ is defined as
$out^{\mathcal{G}}_{obj}(s,\sigma_{A})=\big{\\{}\lambda\in
Run(\mathcal{G})\mid\lambda[0]=s\text{ and for all }j\geqslant
0,\lambda[j]\xrightarrow{\sigma_{A}(\lambda[j])}\lambda[j+1]\big{\\}}$.

  2. 2.

The set of _subjective outcomes of $\sigma_{A}$ at $s$_ is defined as
$out^{\mathcal{G}}_{subj}(s,\sigma_{A})=\displaystyle\bigcup_{i\in
A,s^{\prime}\sim_{i}s}out^{\mathcal{G}}_{obj}(s^{\prime},\sigma_{A})$.

###  2.2 Alternating-Time Temporal Logic.

We now introduce the alternating-time temporal logic ATL∗ to be interpreted on
iCGS.

######  Definition 3 (ATL∗).

The language of ATL∗ is formally defined by the following grammar, where $p\in
AP$ and $A\subseteq Ag$:

$\displaystyle\varphi$ $\displaystyle::=$ $\displaystyle
p\mid\neg\varphi\mid\varphi\to\varphi\mid\llangle A\rrangle\psi$
$\displaystyle\psi$ $\displaystyle::=$
$\displaystyle\varphi\mid\neg\psi\mid\psi\to\psi\mid X\psi\mid\psi U\psi$

Formulas $\varphi$ are called _state formulas of ATL ∗_, or simply _formulas
of ATL ∗_. Formulas $\psi$ are sometimes called _path formulas of ATL ∗_.

The ATL∗ operator $\llangle A\rrangle$ intuitively means that ‘the agents in
coalition $A$ have a (collective) strategy to achieve …’, where the goals are
LTL formulas built by using operators ‘next’ $X$ and ‘until’ $U$. We define
$A$-formulas as the formulas in ATL∗ in which $A$ is the only coalition
appearing in ATL∗ modalities.

Traditionally, ATL∗ under imperfect information has been given either state-
based or history-based semantics, and several variations have been considered
on the interpretation of strategy operators. Here we present both the
objective and subjective variants of the state-based semantics with imperfect
information and imperfect recall.

######  Definition 4.

Given an iCGS $\mathcal{G}$, a state formula $\varphi$, and path formula
$\psi$, the _subjective_ (resp. _objective_) satisfaction of $\varphi$ at
state $s$ and of $\psi$ in path $\lambda$, denoted
$(\mathcal{G},s)\\!\models_{x}\\!\varphi$ and
$(\mathcal{G},\lambda)\\!\models_{x}\\!\psi$ for $x\\!=\\!subj$ (resp.
$x\\!=\\!obj$), is defined recursively as follows:

$\displaystyle(\mathcal{G},s)\models_{x}p$ iff $\displaystyle p\in\pi(s)$
$\displaystyle(\mathcal{G},s)\models_{x}\lnot\varphi$ iff
$\displaystyle(\mathcal{G},s)\not\models_{x}\varphi$
$\displaystyle(\mathcal{G},s)\models_{x}\varphi\to\varphi^{\prime}$ iff
$\displaystyle(\mathcal{G},s)\not\models_{x}\varphi\text{ or
}(\mathcal{G},s)\models_{x}\varphi^{\prime}$
$\displaystyle(\mathcal{G},s)\models_{x}\llangle A\rrangle\psi$ iff
$\displaystyle\text{ for some }\sigma_{A},\text{ for all }\lambda\in
out^{\mathcal{G}}_{x}(s,\sigma_{A}),(\mathcal{G},\lambda)\models_{x}\psi$
$\displaystyle(\mathcal{G},\lambda)\models_{x}\varphi$ iff
$\displaystyle(\mathcal{G},\lambda[0])\models_{x}\varphi$
$\displaystyle(\mathcal{G},\lambda)\models_{x}\lnot\psi$ iff
$\displaystyle(\mathcal{G},\lambda)\not\models_{x}\psi$
$\displaystyle(\mathcal{G},\lambda)\models_{x}\psi\to\psi^{\prime}$ iff
$\displaystyle(\mathcal{G},\lambda)\not\models_{x}\psi\text{ or
}(\mathcal{G},\lambda)\models_{x}\psi^{\prime}$
$\displaystyle(\mathcal{G},\lambda)\models_{x}X\psi$ iff
$\displaystyle(\mathcal{G},\lambda_{\geqslant 1})\models_{x}\psi$
$\displaystyle(\mathcal{G},\lambda)\models_{x}\psi U\psi^{\prime}$ iff
$\displaystyle\text{ for some }j\geqslant 0,(\mathcal{G},\lambda_{\geqslant
j})\models_{x}\psi^{\prime}$ $\displaystyle\text{ and for all }k,0\leqslant
k<j\text{ implies }(\mathcal{G},\lambda_{\geqslant k})\models_{x}\psi$

######  Example 2.

Consider the simple voting model in Example 1. Clearly, the voter cannot
enforce a win of any candidate, since the election official might block the
publication of the outcome:
$\mathcal{G},q_{0}\models\neg\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{F}\mathsf{{win_{1}}}\land\neg\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{F}\mathsf{{win_{2}}}$.
On the other hand, she can prevent any given candidate from being elected, by
casting her vote for the other candidate:
$\mathcal{G},q_{0}\models\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{G}\neg\mathsf{{win_{1}}}\land\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{G}\neg\mathsf{{win_{2}}}$.
Finally, the voter and the official together can get any arbitrary candidate
elected:
$\mathcal{G},q_{0}\models\langle\\!\langle{1,2}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{F}\mathsf{{win_{1}}}\land\langle\\!\langle{1,2}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{F}\mathsf{{win_{2}}}$.
Note that the truth value of formulae in $q_{0}$ does not depend on whether we
use the subjective or the objective semantics.

The difference between the two semantics can be demonstrated, e.g., in state
$q_{3}$. In that state, the election official has the objective ability to
make candidate 1 win
($\mathcal{G},q_{3}\models_{obj}\langle\\!\langle{2}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{F}\mathsf{{win_{1}}}$)
by playing _pub_ regardless of anything. On the other hand, there is no
uniform strategy for $2$ that guarantees the same from all the states
indistinguishable from $q_{3}$ (i.e., from $q_{3},q_{4},q_{5},q_{6}$). In
consequence,
$\mathcal{G},q_{3}\models_{subj}\neg\langle\\!\langle{2}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{F}\mathsf{{win_{1}}}$.

The individual knowledge operator $K_{i}$ can be added to the syntax of ATL∗
with the following semantics:

$(\mathcal{G},s)\models_{x}K_{i}\varphi\text{ iff for all }s^{\prime}\in
S,s^{\prime}\sim_{i}s\text{ implies
}(\mathcal{G},s^{\prime})\models_{x}\varphi$

By considering the subjective interpretation of ATL∗, this operator can be
derived: $(\mathcal{G},s)\models_{subj}K_{i}\varphi$ iff
$(\mathcal{G},s)\models_{subj}\llangle i\rrangle\varphi U\varphi$. There
exists no such definition for the knowledge operator in ATL∗ with the
objective semantics. The latter is easy to see, as the objective semantics of
$\langle\\!\langle{i}\rangle\\!\rangle_{{}_{\\!\mathit{}}}$ in
$(\mathcal{G},s)$ does not refer in any way to the states epistemically
indistinguishable from $s$.

##  3 Simulations and Bisimulations

In this section we introduce a notion of bisimulation for imperfect
information concurrent game structures. Then, we show that it preserves the
meaning of formulas in ATL∗, when interpreted under the assumptions of
imperfect information and imperfect recall, introduced in Section 2.

###  3.1 Bisimulation for ATL∗ with Imperfect Information and Imperfect Recall

We start with some auxiliary notions and definitions.

Partial strategies and outcome states. A _partial (uniform) strategy_ for
agent $i\in Ag$ is a partial function $\sigma:S\rightarrow Act$ such that for
each $s,s^{\prime}\in S$, if $s\sim_{i}s^{\prime}$ then
$\sigma(s)=\sigma(s^{\prime})$. We denote the domain of the partial strategy
$\sigma$ as $dom(\sigma)$. Given a coalition $A\subseteq Ag$, a _partial
strategy for $A$_ is a tuple $(\sigma_{i})_{i\in A}$ of partial strategies,
one for each agent $i\in A$. The set of partial uniform strategies for $A$ is
denoted $PStr_{A}$. Given set $Q\subseteq S$ of states and coalition
$A\subseteq Ag$, we denote by $PStr_{A}(Q)$ the set of partial uniform
strategies whose domain is $Q$:

$PStr_{A}(Q)=\big{\\{}(\sigma_{i})_{i\in A}\in PStr_{A}\mid
dom(\sigma_{i})=Q\text{ for all }i\in A\big{\\}}$

Additionally, given a (total or partial) strategy $\sigma_{A}$ and a state
$q\in dom(\sigma_{A})$, define the set of _successor states of $q$ by
$\sigma$_ as $succ(q,\sigma_{A})=\\{s\in S\mid
q\xrightarrow{\sigma_{A}(q)}s\\}$, and put
$succ(\sigma_{A})=succ(dom(\sigma_{A}),\sigma_{A})=\bigcup_{s\in
dom(\sigma_{A})}succ(s,\sigma_{A})$.

Strategy simulators. Let $\mathcal{G},\mathcal{G}^{\prime}$ be two iCGS. A
_simulator of partial strategies for coalition $A$_ from $\mathcal{G}$ into
$\mathcal{G}^{\prime}$ is a set $ST$ of functions
$ST_{Q,Q^{\prime}}:PStr_{A}(Q)\rightarrow PStr_{A}(Q^{\prime})$ for some
subsets $Q\subseteq S$ and $Q^{\prime}\subseteq S^{\prime}$. Intuitively,
every $ST_{Q,Q^{\prime}}$ maps each partial strategy $\sigma_{A}$ defined on
set $Q$ in the iCGS $\mathcal{G}$ into a “corresponding” strategy
$\sigma^{\prime}_{A}$ defined on $Q^{\prime}$ in $\mathcal{G}^{\prime}$.
Typically, we will map strategies between the common knowledge neighborhoods
of “bisimilar” states in $\mathcal{G}$ and $\mathcal{G}^{\prime}$. We
formalize this idea as follows. Let $R\subseteq S\times S^{\prime}$ be some
relation between states in $\mathcal{G}$ and $\mathcal{G}^{\prime}$. A
_simulator of partial strategies for coalition $A$ with respect to relation
$R$_ is a family $ST$ of functions
$ST_{C_{A}(q),C_{A}^{\prime}(q^{\prime})}:PStr_{A}(C_{A}(q))\rightarrow
PStr_{A}(C_{A}^{\prime}(q^{\prime}))$ such that $q\in S$, $q^{\prime}\in
S^{\prime}$, and $qRq^{\prime}$. Note that, since the functions are indexed by
equivalence classes of states, the following additional property is
automatically guaranteed:

  * 1.

for every $r\in S$, $r^{\prime}\in S^{\prime}$, if $r\in C_{A}(q)$,
$r^{\prime}\in C_{A}^{\prime}(q^{\prime})$, and $rRr^{\prime}$, then
$ST_{C_{A}(q),C_{A}^{\prime}(q^{\prime})}=ST_{C_{A}(r),C_{A}^{\prime}(r^{\prime})}$.

Simulation and bisimulation. We can now present our notions of simulation and
bisimulation on iCGS.

######  Definition 5 (Simulation).

Let $\mathcal{G}=\langle Ag,AP,S,s_{0},Act,\\{\sim_{i}\\}_{i\in
Ag},d,\to,\pi\rangle$ and $\mathcal{G}^{\prime}=\langle
Ag,AP,S^{\prime},s^{\prime}_{0},Act^{\prime},\\{\sim^{\prime}_{i}\\}_{i\in
Ag},d^{\prime},\to^{\prime},\pi^{\prime}\rangle$ be two iCGS defined on the
same sets $Ag$ of agents and $AP$ of atoms. Let $A\subseteq Ag$ be a coalition
of agents. A relation $\Rrightarrow_{A}\subseteq S\times S^{\prime}$ is a
_simulation for $A$_ iff

  1. 1.

There exists a simulator $ST$ of partial strategies for $A$ w.r.t.
$\Rrightarrow_{A}$, such that $q\Rrightarrow_{A}q^{\prime}$ implies that:

    1. (a)

$\pi(q)=\pi^{\prime}(q^{\prime})$;

    2. (b)

for every $i\in A$ , $r^{\prime}\in S^{\prime}$, if
$q^{\prime}\sim^{\prime}_{i}r^{\prime}$ then for some $r\in S$, $q\sim_{i}r$
and $r\Rrightarrow_{A}r^{\prime}$.

    3. (c)

For every states $r\in C_{A}(q)$, $r^{\prime}\in C_{A}^{\prime}(q^{\prime})$
such that $r\Rrightarrow_{A}r^{\prime}$, for every partial strategy
$\sigma_{A}\in PStr_{A}(C_{A}(q))$, and every state $s^{\prime}\in
succ(r^{\prime},ST(\sigma_{A}))$, there exists a state $s\in
succ(r,\sigma_{A})$ such that $s\Rrightarrow_{A}s^{\prime}$.

  2. 2.

If $q_{1}\Rrightarrow_{A}q^{\prime}$ and $q_{2}\Rrightarrow_{A}q^{\prime}$,
then $C_{A}(q_{1})=C_{A}(q_{2})$.

A relation $\Lleftarrow\\!\\!\\!\Rrightarrow_{A}$ is a bisimulation iff both
$\Lleftarrow\\!\\!\\!\Rrightarrow_{A}$ and its converse
$\Lleftarrow\\!\\!\\!\Rrightarrow_{A}^{-1}=\\{(q^{\prime},q)\mid
q\Lleftarrow\\!\\!\\!\Rrightarrow_{A}q^{\prime}\\}$ are simulations.

By Def. 5 if state $q^{\prime}$ simulates $q$, i.e.,
$q\Rrightarrow_{A}q^{\prime}$, then 1.(a) $q$ and $q^{\prime}$ agree on the
interpretation of atoms; 1.(b) $q$ simulates the epistemic transitions from
$q^{\prime}$, that is, information encoded in states is preserved by
(bi)similarity; and 1.(c) for every partial strategy $\sigma_{A}$, defined on
the common knowledge neighborhood $C_{A}(q)$, we are able to find some partial
strategy $ST(\sigma_{A})$ (the same for all states in $C_{A}(q)$) such that
the transition relations $\xrightarrow{ST(\sigma_{A})}$ and
$\xrightarrow{\sigma_{A}}$ commute with the simulation relation
$\Rrightarrow_{A}$. Moreover, (2) the simulation relation is injective when
lifted to common knowledge neighborhoods.

$q_{0}^{\prime}$$q_{1}^{\prime}$$q_{3}^{\prime}$$q_{6}^{\prime}$$q_{7}^{\prime}$$\mathsf{{win_{1}}}$$q_{8}^{\prime}$$\mathsf{{win_{2}}}$$(-,-)$$(vote_{1},-)$$(vote_{2},-)$$(-,pub)$$(-,pub)$2$(-,np)$$(-,np)$$(-,-)$$(-,-)$

$q_{0}^{\prime}$$q_{1}^{\prime}$$q_{3}^{\prime}$$q_{7}^{\prime}$$\mathsf{{win_{1}}}$$q_{8}^{\prime}$$\mathsf{{win_{2}}}$$(-,-)$$(-,-)$$(vote_{1},pub)$$(vote_{2},pub)$$(-,np)$$(-,-)$$(-,-)$

Figure 2: (a) Even simpler model of 2-stage voting (from the point of view of
the election official). (b) Yet simpler model of 2-stage voting.

######  Example 3.

Let us go back to the simple two-stage voting from Example 1 and Figure 1. We
observe that the model is bisimilar for $A=\\{2\\}$ to the one in Figure 2.
The bisimulation connects $q_{0}$ with $q_{0}^{\prime}$; $q_{1}$ and $q_{2}$
with $q_{1}^{\prime}$; $q_{3}$ and $q_{4}$ with $q_{3}^{\prime}$; $q_{5}$ and
$q_{6}$ with $q_{6}^{\prime}$; $q_{7}$ with $q_{7}^{\prime}$; and $q_{8}$ with
$q_{8}^{\prime}$. As we will see in Section 3.2, this implies that the
abilities of the election official in both models must be exactly the same.

The iCGS can be reduced even further, and still retain the same abilities of
the singleton coalition $\\{2\\}$, see Figure 2. We leave it to the interested
reader to find the bisimulation for $\\{2\\}$ between the two models.

######  Remark 6.

Technically, condition (2) in Def. 5 is required as is shown in the end of
this section by a counterexample (cf. Subsection 3.3). The extra property (2)
corrects the statement and proof of Theorem 9 in [48]. Notice that, for every
bisimulation $\Lleftarrow\\!\\!\\!\Rrightarrow_{A}$ defined on
$\mathcal{G}=\mathcal{G}^{\prime}$, condition (2) says that two bisimilar
states must lie in the same common knowledge neighborhood, which is a natural
constraint considering that two bisimilar states should satisfy the same
formulas in ATL∗.

###  3.2 Preservation Theorem

In order to show that bisimilar states satisfy the same formulas in ATL∗, we
prove the following auxiliary result. Hereafter, runs $\lambda\in S^{+}$,
$\lambda^{\prime}\in S^{\prime+}$ are $A$-bisimilar, or
$\lambda\Lleftarrow\\!\\!\\!\Rrightarrow_{A}\lambda^{\prime}$ iff for every
$i\geqslant 0$,
$\lambda[i]\Lleftarrow\\!\\!\\!\Rrightarrow_{A}\lambda^{\prime}[i]$

######  Proposition 7.

If $q\Rrightarrow_{A}q^{\prime}$ then for every strategy $\sigma_{A}$, there
exists a strategy $\sigma_{A}^{\prime}$ such that

  * ($*$)

for every run $\lambda^{\prime}\in
out^{\mathcal{G}^{\prime}}_{x}(q^{\prime},\sigma_{A}^{\prime})$, for
$x\in\\{subj,obj\\}$, there exists an infinite run $\lambda\in
out^{\mathcal{G}}_{x}(q,\sigma_{A})$ such that
$\lambda\Rrightarrow_{A}\lambda^{\prime}$.

###### Proof.

First of all we define the sequence
$\big{(}dom^{n}(\sigma_{A})\big{)}_{n\in\mathbb{N}}$, of sets of states in
$\mathcal{G}$ such that $s\in dom^{n}(\sigma_{A})$ iff $s$ can be reached in
at most $n$ steps from $C_{A}(q)$ by applying actions compatible with strategy
$\sigma_{A}$:

$\displaystyle dom^{0}(\sigma_{A})$ $\displaystyle=C_{A}(q)$ $\displaystyle
dom^{n+1}(\sigma_{A})$
$\displaystyle=dom^{n}(\sigma_{A})\cup\bigcup\big{\\{}C_{A}(r)\mid
r\in\bigcup_{s\in dom^{n}(\sigma_{A})}succ(s,\sigma_{A})\big{\\}}$

Also, we denote by $\sigma^{n}_{A}$ the partial strategy resulting from
restricting $\sigma_{A}$ to $dom^{n}(\sigma_{A})$.

We now define inductively a sequence
$(\overline{\sigma}^{n}_{A})_{n\in\mathbb{N}}$ of partial strategies in
$\mathcal{G}^{\prime}$ such that $dom(\overline{\sigma}^{n}_{A})\subseteq
dom(\overline{\sigma}^{n+1}_{A})$ for every $n\in\mathbb{N}$. These partial
strategies will be constructed using strategy $\sigma_{A}$ and mapping $ST$
from point (1) in Def. 5. The desired sequence of partial strategies
$\overline{\sigma}^{n}_{A}$, for $n\geqslant 1$, is defined as follows:

  1. 1.

$dom(\overline{\sigma}_{A}^{0})=C^{\prime}_{A}(q^{\prime})$ and
$dom(\overline{\sigma}_{A}^{n+1})=dom(\overline{\sigma}_{A}^{n})\cup\\{r^{\prime}\mid
C^{\prime}_{A}(r^{\prime})\cap
succ(\overline{\sigma}_{A}^{n})\neq\emptyset\\}$;

  2. 2.

for all $r^{\prime}\in dom(\overline{\sigma}_{A}^{0})$,
$\overline{\sigma}_{A}^{0}(r^{\prime})=ST_{C_{A}\\!(q),C_{A}^{\prime}\\!(q^{\prime})}(\sigma^{0}_{A})(r^{\prime})$;

  3. 3.

for all $r^{\prime}\in dom(\overline{\sigma}_{A}^{n+1})$,

$\overline{\sigma}^{n+1}_{A}(r^{\prime})=\begin{cases}\overline{\sigma}^{n}_{A}(r^{\prime})&\text{for
}r^{\prime}\in dom(\overline{\sigma}^{n}_{A})\\\
ST_{C_{A}\\!(r),C_{A}^{\prime}\\!(r^{\prime})}(\sigma^{n+1}_{A})(r^{\prime})&\text{for
}r^{\prime}\not\in
dom(\overline{\sigma}^{n}_{A}),C_{A}^{\prime}\\!(r^{\prime})\cap
succ(\\!\overline{\sigma}^{n}_{A}\\!)\neq\emptyset,\\\ &\text{and }r\text{ is
any state in $\mathcal{G}$ s.t.~{}}r\Rrightarrow_{A}r^{\prime}\end{cases}$

We give first a number of properties for this sequence of partial strategies.
First note that, in the last line of the definition of
$\overline{\sigma}_{A}^{n+1}(r^{\prime})$, $r$ can indeed be chosen
arbitrarily, since, by point (2) in Def. 5, whenever
$r_{1}\Rrightarrow_{A}r^{\prime}$ and $r_{2}\Rrightarrow_{A}r^{\prime}$ we
must have $C_{A}(r_{1})=C_{A}(r_{2})$, which implies that
$ST_{C_{A}(r_{1}),C_{A}^{\prime}(r^{\prime})}=ST_{C_{A}(r_{2}),C_{A}^{\prime}(r^{\prime})}$.

Further, if $C_{A}^{\prime}(r^{\prime})\cap
dom(\overline{\sigma}^{n}_{A})\neq\emptyset$ then
$C_{A}^{\prime}(r^{\prime})\subseteq dom(\overline{\sigma}^{n}_{A})$. This is
trivial for $n=0$. As for the induction step, if
$C_{A}^{\prime}(r^{\prime})\cap
dom(\overline{\sigma}^{n+1}_{A})\neq\emptyset$, but
$C_{A}^{\prime}(r^{\prime})\not\subseteq dom(\overline{\sigma}^{n}_{A})$, then
by induction hypothesis we have $C_{A}^{\prime}(r^{\prime})\cap
dom(\overline{\sigma}^{n}_{A})=\emptyset$. Further, by definition of
$\overline{\sigma}^{n+1}_{A}$ we obtain $C_{A}^{\prime}(r^{\prime})\cap
succ(\overline{\sigma}^{n}_{A})\neq\emptyset$, which is the case for all
$r^{\prime\prime}\in C_{A}^{\prime}(r^{\prime})$. Hence
$C_{A}^{\prime}(r^{\prime})\subseteq dom(\overline{\sigma}^{n+1}_{A})$.

We now show that, whenever we take some $u^{\prime}\in
C_{A}^{\prime}(r^{\prime})\cap succ(\overline{\sigma}^{n}_{A})\neq\emptyset$
with $r^{\prime}\not\in dom(\overline{\sigma}^{n}_{A})$, we have $\\{u\in
dom^{n+1}(\sigma_{A})\mid u\Rrightarrow_{A}u^{\prime}\\}\neq\emptyset$ and, by
the induction hypothesis $\overline{\sigma}^{n+1}_{A}$ is uniform over
$dom(\overline{\sigma}^{n}_{A})$. To see the former, whenever $u^{\prime}\in
C_{A}^{\prime}(\\!r^{\prime}\\!)\cap succ(\\!\overline{\sigma}^{n}_{A}\\!)$,
one can find $v^{\prime}\\!\in\\!dom(\overline{\sigma}^{n}_{A})$ s.t.
$u^{\prime}\in succ(v^{\prime},\overline{\sigma}_{A}^{n}(v^{\prime}))$. By
definition of $\overline{\sigma}_{A}^{n}$, there exists
$v\Rrightarrow_{A}v^{\prime}$ s.t. $v\in dom(\sigma^{n}_{A})$ and
$\overline{\sigma}^{n}_{A}(v^{\prime})=ST_{C_{A}(v),C_{A}^{\prime}(v^{\prime})}(\sigma^{n}_{A})(v^{\prime})$.
From property 1.(c), this implies the existence of $u$ with
$u\Rrightarrow_{A}u^{\prime}$ and $u\in succ(v,\sigma_{A}(v))$, which entails
$u\in dom(\sigma^{n+1}_{A})$.

We then prove by induction on $n$ that $\overline{\sigma}^{n}_{A}$ is uniform.
The case for $n=0$ is immediate by application to $\sigma^{0}_{A}$ of
simulator $ST$ of partial strategies. For $n>0$, as noted above if
$C_{A}^{\prime}(r^{\prime})\cap dom(\overline{\sigma}^{n}_{A})\neq\emptyset$
for some $r^{\prime}$, then $C_{A}^{\prime}(r^{\prime})\subseteq
dom(\overline{\sigma}^{n}_{A})$. Therefore, the induction step only needs
proof for $r_{1}^{\prime},r_{2}^{\prime}\in
dom(\overline{\sigma}^{n+1}_{A})\setminus dom(\overline{\sigma}^{n}_{A})$. So
assume, in this case, that $r_{1}^{\prime}\sim_{i}r_{2}^{\prime}$ for some
$i\in A$, hence
$C_{A}^{\prime}(r_{1}^{\prime})=C_{A}^{\prime}(r_{2}^{\prime})$. Consider then
some $r_{1}\Rrightarrow_{A}r_{1}^{\prime}$ and
$r_{2}\Rrightarrow_{A}r_{2}^{\prime}$, which exist by the previous paragraph.
Then condition 1.(b) in Def. 5 implies the existence of some $r_{3}$ such that
$r_{3}\sim_{i}r_{1}$ and $r_{3}\Rrightarrow_{A}r_{2}^{\prime}$, which then, by
condition (2) implies $C_{A}(r_{1})=C_{A}(r_{3})=C_{A}(r_{2})$, which in turn
implies that
$ST_{C_{A}(r_{1}),C_{A}^{\prime}(r_{1}^{\prime})}=ST_{C_{A}(r_{2}),C_{A}^{\prime}(r_{2}^{\prime})}$.
Then
$\overline{\sigma}_{A}^{n+1}(r_{1}^{\prime})=ST_{C_{A}(r_{1}),C_{A}^{\prime}(r_{1}^{\prime})}(\sigma_{A}^{n+1})(r_{1}^{\prime})=ST_{C_{A}(r_{2}),C_{A}^{\prime}(r_{2}^{\prime})}(\sigma_{A}^{n+1})(r_{2}^{\prime})=\overline{\sigma}_{A}^{n+1}(r_{2}^{\prime})$
as $ST$ is a simulator of partial strategies which maps uniform strategies for
$A$ in $\mathcal{G}$ to uniform strategies for $A$ in $\mathcal{G}^{\prime}$.

As a result, the “limit” partial strategy
$\overline{\sigma}_{A}={\displaystyle\bigcup_{n\in\mathbb{N}}}\overline{\sigma}^{n}_{A}$
defined as
$\overline{\sigma}_{A}(r^{\prime})=\overline{\sigma}^{n}_{A}(r^{\prime})$
whenever $r^{\prime}\in dom(\overline{\sigma}^{n}_{A})$, is also uniform and
has $dom(\overline{\sigma}_{A})=succ(\overline{\sigma}_{A})$. We then only
need to transform it into a (total) uniform strategy by imposing a fixed
action $a_{0}\in Act$ wherever $\overline{\sigma}^{n}_{A}$ is undefined, that
is, introducing the following uniform strategy $\sigma_{A}^{\prime}$:

$\sigma_{A}^{\prime}(r^{\prime})=\begin{cases}\overline{\sigma}_{A}(r^{\prime})&\text{
for }r^{\prime}\in dom(\overline{\sigma}_{A})\\\ a_{0}&\text{
otherwise}\end{cases}$

To prove property ($*$) for the subjective semantics, consider a run
$\lambda^{\prime}\in
out^{\mathcal{G}^{\prime}}_{subj}(q^{\prime},\sigma_{A}^{\prime})$. We build
inductively the run $\lambda$ as follows: for the base case, by condition
1.(b) in Def. 5 (and a short induction on the length of the
indistinguishability path connecting $q^{\prime}$ with $\lambda^{\prime}[0]$),
we obtain a state $r\in C_{A}(q)$ such that
$r\Rrightarrow_{A}\lambda^{\prime}[0]$. Then, set $\lambda[0]:=r$. For the
inductive step, assume $\lambda[k]$ has been built, with
$\lambda[j]\Rrightarrow_{A}\lambda^{\prime}[j]$ for all $j\leqslant k$. Now,
we have $\lambda^{\prime}[k+1]\in
succ(\lambda^{\prime}[k],\sigma^{\prime}_{A})$. By definition,
$\sigma^{\prime}_{A}(\lambda^{\prime}[k])=ST_{C_{A}(\lambda[k]),C_{A}^{\prime}(\lambda^{\prime}[k])}(\sigma_{A})(\lambda^{\prime}[k])$
since $\lambda[k]\Rrightarrow_{A}\lambda^{\prime}[k]$. This, by property 1.(c)
implies the existence of some $u\in succ(\lambda[k],\sigma_{A})$ such that
$u\Rrightarrow_{A}\lambda^{\prime}[k+1]$. We then set $\lambda[k+1]:=u$, and
obtain the desired result. The same proof works for the objective semantics,
by simply starting the induction with $\lambda[0]=q$. Property ($*$) is then
proved for both semantics. ∎

By using Proposition 7 we are finally able to prove the main preservation
result of this paper.

######  Theorem 8.

Let $\mathcal{G}$ and $\mathcal{G}^{\prime}$ be iCGS, $q\in S$ and
$q^{\prime}\in S^{\prime}$ be states such that
$q\Lleftarrow\\!\\!\\!\Rrightarrow_{A}q^{\prime}$, and $\lambda\in S^{+}$ and
$\lambda^{\prime}\in S^{\prime+}$ be runs such that
$\lambda\Lleftarrow\\!\\!\\!\Rrightarrow_{A}\lambda^{\prime}$. Then, for every
state $A$-formula $\varphi$ and path $A$-formula $\psi$,

$\displaystyle(\mathcal{G},q)\models\varphi$ iff
$\displaystyle(\mathcal{G}^{\prime},q^{\prime})\models\varphi$
$\displaystyle(\mathcal{G},\lambda)\models\psi$ iff
$\displaystyle(\mathcal{G}^{\prime},\lambda^{\prime})\models\psi$

###### Proof.

The proof is by mutual induction on the structure of $\varphi$ and $\psi$.

The case for propositional atoms is immediate as $(\mathcal{G},q)\models p$
iff $p\in\pi(q)$, iff $p\in\pi^{\prime}(q^{\prime})$ by definition of
bisimulation, iff $(\mathcal{G}^{\prime},q^{\prime})\models p$. The inductive
cases for propositional connectives are also immediate.

For $\psi=\varphi$, suppose that $(\mathcal{G},\lambda)\models\psi$, that is,
$(\mathcal{G},\lambda[0])\models\varphi$. By assumption,
$\lambda[0]\Lleftarrow\\!\\!\\!\Rrightarrow_{A}\lambda^{\prime}[0]$ as well,
and by induction hypothesis
$(\mathcal{G}^{\prime},\lambda^{\prime}[0])\models\varphi$. Thus,
$(\mathcal{G}^{\prime},\lambda^{\prime})\models\psi$.

For $\psi=X\psi^{\prime}$, suppose that $(\mathcal{G},\lambda)\models\psi$,
that is, $(\mathcal{G},\lambda_{\geqslant 1}])\models\psi^{\prime}$. By
assumption, $\lambda_{\geqslant
1}\Lleftarrow\\!\\!\\!\Rrightarrow_{A}\lambda^{\prime}_{\geqslant 1}$ as well,
and by induction hypothesis $(\mathcal{G}^{\prime},\lambda^{\prime}_{\geqslant
1})\models\psi^{\prime}$. Thus,
$(\mathcal{G}^{\prime},\lambda^{\prime})\models\psi$. The inductive cases for
$\psi=\psi^{\prime}U\psi^{\prime\prime}$ and
$\psi=\psi^{\prime}R\psi^{\prime\prime}$ are similar.

For $\varphi=\llangle A\rrangle\psi$, $(\mathcal{G},q)\models\varphi$ iff that
for some strategy $\sigma_{A}$, for all $\lambda\in
out^{\mathcal{G}}_{x}(q,\sigma_{A})$, $(\mathcal{G},\lambda)\models\psi$. By
Prop. 7, there exists strategy $\sigma^{\prime}_{A}$ s.t. for all
$\lambda^{\prime}\in
out^{\mathcal{G}^{\prime}}_{x}(q^{\prime},\sigma^{\prime}_{A})$, there exists
$\lambda\in out^{\mathcal{G}}_{x}(q,\sigma_{A})$ s.t.
$\lambda\Lleftarrow\\!\\!\\!\Rrightarrow_{A}\lambda^{\prime}$. By the
induction hypothesis, $(\mathcal{G},\lambda)\models\psi$ iff
$(\mathcal{G}^{\prime},\lambda^{\prime})\models\psi$. Hence,
$(\mathcal{G}^{\prime},q^{\prime})\models\varphi$. ∎

######  Corollary 9.

Let $\mathcal{G}$ and $\mathcal{G}^{\prime}$ be iCGS, and $q\in S$,
$q^{\prime}\in S^{\prime}$ be states such that
$q\Lleftarrow\\!\\!\\!\Rrightarrow_{A}q^{\prime}$. Then, for every $A$-formula
$\varphi$,

$\displaystyle(\mathcal{G},q)\models\varphi$ if and only if
$\displaystyle(\mathcal{G}^{\prime},q^{\prime})\models\varphi$

By Theorem 8 we obtain that bisimilar states preserve the interpretation of
ATL⋆ formulas. More precisely, if states $q$ and $q^{\prime}$ are
$A$-bisimilar then they satisfy the same $A$-formulas. Observe that only
$A$-formulas are normally preserved by $A$-bisimulations. This is already a
feature of $A$-bisimulations for the case of perfect information [29, Theorem
6].

###  3.3 Discussion

In [48] we introduced a different notion of bisimulation for the ATL fragment
only of ATL∗. Specifically, the original Def. 6 of bisimulation in [48]
differs from Def. 5 in that it lacks condition 2 (we refer to the paper for
further details). Unfortunately, this weaker notion of bisimulation makes the
preservation theorem false. In this paper we remedy the problem by requiring
the injectiveness of the bisimulation relation w.r.t. common knowledge
neighbourhoods, i.e., by including condition 2 in Def. 5.

To illustrate the issue consider the single-agent iCGS with states, actions,
and transitions as illustrated in Fig. 3, and a relation
$\Leftarrow\\!\\!\\!\Rightarrow_{[}A]$ such that
$q_{i}\Leftarrow\\!\\!\\!\Rightarrow_{[}A]q^{\prime}_{i}$ for $i\in\\{0,3\\}$
and $q_{i}\Leftarrow\\!\\!\\!\Rightarrow_{[}A]q^{\prime}_{ij}$ for
$i,j\in\\{1,2\\}$, as indicated by the red lines in Fig. 3. A case-by-case
analysis shows that $\Leftarrow\\!\\!\\!\Rightarrow_{[}A]$ satisfies condition
1 in Def. 5, and therefore the two iCGS are bisimilar according to the notion
presented in [48]. However, they do not satisfy condition 2. Indeed, we have
that $q_{1}\Leftarrow\\!\\!\\!\Rightarrow_{[}A]q^{\prime}_{1j}$, for
$j\in\\{1,2\\}$, but $C_{1}(q^{\prime}_{11})\neq C_{1}(q^{\prime}_{12})$, and
similarly for $q_{2}$, $q^{\prime}_{21}$, $q^{\prime}_{22}$. In particular,
the iCGS $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ do not satisfy the same
formulas: we have
$(\mathcal{G}_{1},q_{0})\not\models\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}Fp$
while
$(\mathcal{G}_{2},q_{0})\models\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}Fp$.
Indeed, in $\mathcal{G}_{2}$ a memoryless strategy for agent $1$ to achieve
$Fp$ is to choose action $a$ in knowledge set
$\\{q^{\prime}_{1,1},q^{\prime}_{2,1}\\}$ and action $b$ in
$\\{q^{\prime}_{1,2},q^{\prime}_{2,2}\\}$. Such a strategy is not transferable
as a memoryless strategy into $\mathcal{G}_{1}$, as it would require one bit
memory, that is, on the first visit of knowledge set $\\{q_{1},q_{2}\\}$ agent
$1$ would play $a$, then $b$ on the second visit. Hence, the notion of
bisimulation introduced in [48] is too weak even to preserve formulas in the
fragment ATL; while the present Def. 5 does preserve the whole ATL∗.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$pbaba$q^{\prime}_{0}$$q^{\prime}_{11}$$q^{\prime}_{21}$$q^{\prime}_{12}$$q^{\prime}_{22}$$q^{\prime}_{3}$paabbbaba$\mathcal{G}_{1}$$\mathcal{G}_{2}$
Figure 3: two iCGS satisfying only condition 1 in Def. 5.

###  3.4 Computational Complexity

Theorem 8 shows that two $A$-bisimilar iCGS are equivalent with respect to
coalition $A$’s strategic abilities. This can be useful when verifying
abilities in realistic multi-agent systems. In such cases, the iCGS typically
arises through some kind of product of local components, and suffers from
state-space explosion as well as transition-space explosion. If there is a
smaller bisimilar iCGS, one can use the latter as the input to the model
checking procedure. Since the hardness of the model checking problem for ATL∗
with imperfect information is mostly related to the size of the model, using
an equivalent reduced iCGS can turn an impossible task into a feasible one. An
interesting question is therefore if one can automatically synthesise such
reduced models, or at least check whether two given iCGS are bisimilar. We
briefly investigate the issue hereafter. We call a pair $(\mathcal{G},s)$, for
$s$ in $\mathcal{G}$, a pointed model.

######  Theorem 10.

Checking $A$-bisimilarity of two pointed iCGS is in
$\mathbf{{\Sigma_{{5}}^{\mathbf{{P}}}}}$.

###### Proof.

Complexity-wise, the most problematic part of Def. 5 is the quantification
over strategy simulators $ST$. Being a mapping from partial strategies to
partial strategies, $ST$ has exponential size w.r.t. the size of the model,
which suggests at least exponential time for verifying bisimilarity.
Fortunately, a closer look at the definition of strategy simulators, and at
condition 2 in Def. 5, reveals that $ST$ can be split into local mappings from
mutually disjoint common knowledge neighbourhoods $C_{A}$ in $\mathcal{G}$ to
unique common knowledge neighbourhoods $C_{A}^{\prime}$ in
$\mathcal{G}^{\prime}$. Thus, the conceptual structure of Def. 5 can be (with
a slight abuse of notation) summarized as:

$\displaystyle bisimilar((\mathcal{G},q),(\mathcal{G}^{\prime},q^{\prime}))$
iff $\displaystyle\boldsymbol{\exists}(\Lleftarrow\\!\\!\\!\Rrightarrow_{A})\
\
simul((\mathcal{G},q),(\mathcal{G}^{\prime},q^{\prime}),\Lleftarrow\\!\\!\\!\Rrightarrow_{A})$
$\displaystyle\quad\land\
simul((\mathcal{G}^{\prime},q^{\prime}),(\mathcal{G},q),\Lleftarrow\\!\\!\\!\Rrightarrow_{A})\
\land\ q\Lleftarrow\\!\\!\\!\Rrightarrow_{A}q^{\prime},$ $\displaystyle
simul((\mathcal{G},q),(\mathcal{G}^{\prime},q^{\prime}),\Lleftarrow\\!\\!\\!\Rrightarrow_{A})$
iff
$\displaystyle\boldsymbol{\forall}(\mathcal{C}_{A}\in\mathcal{G}^{\prime})\
\boldsymbol{\forall}(\sigma_{A}\in\mathcal{C}_{A})\boldsymbol{\exists}(\sigma_{A}^{\prime}\in\mathcal{C}_{A}^{\prime})$
$\displaystyle\boldsymbol{\forall}(\hat{q}\in\mathcal{C}_{A},\hat{q}^{\prime}\in\mathcal{C}_{A}^{\prime},\hat{q}\Lleftarrow\\!\\!\\!\Rrightarrow_{A}\hat{q}^{\prime})\
\ match(\hat{q},\hat{q}^{\prime})$ $\displaystyle\quad\land\
simulepist(\hat{q},\hat{q}^{\prime})\ \land\
simultrans(\mathcal{C}_{A},\mathcal{C}_{A}^{\prime}),$ $\displaystyle
match(\hat{q},\hat{q}^{\prime})$ iff
$\displaystyle\pi(\hat{q})=\pi(\hat{q}^{\prime}),$ $\displaystyle
simulepist(\hat{q},\hat{q}^{\prime})$ iff
$\displaystyle\boldsymbol{\forall}(i\in A)\
\boldsymbol{\forall}(\hat{q}^{\prime}\sim_{i}r^{\prime})\
\boldsymbol{\exists}(r)\ \ \hat{q}\sim_{i}r,\
r\Lleftarrow\\!\\!\\!\Rrightarrow_{A}r^{\prime}$ $\displaystyle
simultrans(\mathcal{C}_{A},\mathcal{C}_{A}^{\prime})$ iff
$\displaystyle\boldsymbol{\forall}(r\in\mathcal{C}_{A},r^{\prime}\in\mathcal{C}_{A}^{\prime},r\Lleftarrow\\!\\!\\!\Rrightarrow_{A}r^{\prime})\
\boldsymbol{\forall}(s^{\prime}\in succ(r^{\prime},\sigma_{A}^{\prime}))$
$\displaystyle\boldsymbol{\exists}(s\in succ(r,\sigma_{A}))\ \
s\Lleftarrow\\!\\!\\!\Rrightarrow_{A}s^{\prime}.$

Notice that all the structures quantified in the above expressions are of
polynomial size with respect to the number of states, transitions, and
epistemic links in $\mathcal{G}$ and $\mathcal{G}^{\prime}$. Thus, it is
relatively straightforward to observe, by a suitable translation to the QBF
problem (i.e., satisfiability of Quantified Boolean Formulae) that:

  1. 1.

checking $simulepist(\hat{q},\hat{q}^{\prime})$ and
$simultrans(\mathcal{C}_{A},\mathcal{C}_{A}^{\prime})$ is in
$\mathbf{{\Pi_{{2}}^{\mathbf{{P}}}}}$,

  2. 2.

checking
$simul((\mathcal{G},q),(\mathcal{G}^{\prime},q^{\prime}),\Lleftarrow\\!\\!\\!\Rrightarrow_{A})$
is in $\mathbf{{\Pi_{{4}}^{\mathbf{{P}}}}}$,

  3. 3.

and thus, finally, checking
$bisimilar((\mathcal{G},q),(\mathcal{G}^{\prime},q^{\prime}))$ is in
$\mathbf{{\Sigma_{{5}}^{\mathbf{{P}}}}}$.

∎

We suspect that the upper bound is tight, as we do not see how any of the
quantifier alternations, included in the above QBF translation, could be
collapsed. For the moment, however, we only show the following, and leave the
question of the exact complexity for future work.

$q^{C_{1}}_{x_{1}}$$q^{C_{1}}_{x_{2}}$$q^{C_{2}}_{\neg
x_{1}}$$q^{C_{2}}_{x_{2}}$${\;}q_{\top}{\;}$$\mathsf{{yes}}$${\;}q_{\bot}{\;}$$1$$1$$2$$2$$3$$3$$3$$x_{1},\bot$$x_{2},\bot$$\neg
x_{1},\top$$x_{2},\bot$ Figure 4: Model $M_{\Phi}$ for $\Phi\equiv C_{1}\land
C_{2}$ with $C_{1}\equiv x_{1}\lor x_{2}$ and $C_{2}\equiv\neg x_{1}\lor
x_{2}$. Only transitions leading to $q_{\bot}$ are labeled; the other
combinations of actions lead to $q_{\top}$.

######  Theorem 11.

Checking $A$-bisimilarity of two pointed iCGS is $\mathbf{{NP}}$-hard.

###### Proof.

We adapt the SAT reduction from [67, Proposition 11]. Let us first recall the
idea of that reduction. Given a Boolean formula $\Phi$ in CNF, we build a
$3$-agent iCGS $\mathcal{G}_{\Phi}$ where each literal $l$ from clause $\psi$
in $\Phi$ is associated with a state $q^{\psi}_{l}$. Each agent has a
different role in the construction: player 1 selects the literals to be
satisfied (one literal per clause in $\Phi$), and player 2 chooses the truth
values for those literals. Player 3 “simulates” the common knowledge
neighborhood for $\\{1,2\\}$, and thus ensures that a successful assignment
must work for all the clauses in $\Phi$.

Formally, at state $q^{\psi}_{l}$, player $1$ indicates a literal from $\psi$,
and player $2$ decides on the valuation of the underlying Boolean variable. If
$1$ indicated a “wrong” literal $l^{\prime}\neq l$ then the system proceeds to
state $q_{\top}$ where proposition $\mathsf{{yes}}$ holds. The same happens if
$1$ indicated the “right” literal ($l$) and $2$ selected the valuation that
makes $l$ true. Otherwise the system proceeds to the “sink” state $q_{\bot}$.
Player $1$ must select literals uniformly within clauses, which is imposed by
fixing $q^{\psi}_{l}\sim_{1}q^{\psi^{\prime}}_{l^{\prime}}$ iff
$\psi=\psi^{\prime}$. Player $2$ is to select uniform valuations of variables,
i.e., $q^{\psi}_{l}\sim_{2}q^{\psi^{\prime}}_{l^{\prime}}$ iff
$var(l)=var(l^{\prime})$, where $var(l)$ is the variable contained in $l$.
Finally, all states except $q_{\top},q_{\bot}$ are indistinguishable for agent
$3$. An example of the construction is presented in Figure 4. Let $q_{0}$ be
an arbitrary “literal” state, e.g., the one for the first literal in the first
clause. Then, $\mathbf{SAT}(\Phi)$ iff
$(\mathcal{G}_{\Phi},q_{0})\models\langle\\!\langle{1,2,3}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{X}\mathsf{{yes}}$
according to the subjective semantics of $\mathbf{ATL_{\mathrm{}}}$ with
imperfect information and imperfect recall.

Now, we construct iCGS $\mathcal{G}_{\Phi}^{\prime}$ by adding action $skip$,
available to agent $1$ at every “literal” state, which always enforces a
transition to $q_{\top}$ regardless of the actions selected by agents 2 and 3.
In particular, $\mathcal{G}_{\Phi}^{\prime}$ adds to $\mathcal{G}_{\Phi}$ a
strategy for coalition $\\{1,2,3\\}$ whose only successor state from all the
“literal” states is $q_{\top}$. Thus,
$(\mathcal{G}_{\Phi},q_{0})\models\langle\\!\langle{1,2,3}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{X}\mathsf{{yes}}$
iff
$(\mathcal{G}_{\Phi},q_{0})\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{1,2,3\\}}(\mathcal{G}_{\Phi}^{\prime},q_{0})$,
which completes the reduction. ∎

In sum, the problem of deciding bisimilarity is easier than exponential time,
but still far from practically automatizable. To obtain a reduction, one must
propose the reduced model and the bisimulation according to one’s intuition,
and verify correctness of the bisimulation by hand. We will show an extensive
example of how this can be done in Section 5.

##  4 Towards the Hennessy-Milner Property

In this section we show that the notion of bisimulation we introduced in
Section 3 does not enjoy the Hennessy-Milner (HM) property, that is, some iCGS
are logically equivalent (i.e., they satisfy the same formulas in ATL∗) and
yet they are not bisimilar. This is the case for both the subjective and
objective variants of our semantics. More precisely, for $x\in\\{sub,obj\\}$,
we say that states $q\in\mathcal{G}$ and $q^{\prime}\in\mathcal{G}^{\prime}$
are $A$-equivalent, or $q\thickapprox_{A}^{x}q^{\prime}$, iff for every
$A$-formula $\varphi$, $(\mathcal{G},q)\models_{x}\varphi$ iff
$(\mathcal{G},q^{\prime})\models_{x}\varphi$. The iCGS
$\mathcal{G},\mathcal{G}^{\prime}$ will be omitted as clear from the context.
In other words, relation $\thickapprox_{A}^{x}$ connects those states of two
iCGS that satisfy the same formulas in ATL∗ that refer to coalition $A$.

In many logics, such as the Hennessy-Milner logic, CTL, CTL∗, ATL and ATL∗
interpreted under perfect information [29], logical equivalence can be
characterised in a local and efficient way by means of bisimulations. By
contrast, the bisimulations for ATL∗ introduced in this paper are strictly
weaker than logical equivalence $\thickapprox_{A}^{x}$. In particular, in
Section 4.1 we show that there are iCGS that satisfy the same formulas in
ATL∗, while not being bisimilar. Then, in Section 4.2 we present a necessary
local condition that needs to be satisfied by $\thickapprox_{A}^{subj}$. As we
show, the condition is not sufficient however. Nevertheless, it is an
important piece of the currently partially known puzzle about the
characterisation power of bisimulations for ATL∗ under imperfect information.

In the rest of the section let $T\subseteq S$ and $R\subseteq S\times
S^{\prime}$. We define _the image_ of $T$ w.r.t. $R$:

$\displaystyle\mathit{Img}({T},{R})$ $\displaystyle=\\{q\in
S^{\prime}\;|\;\text{for some }q^{\prime}\in T\;(q^{\prime},q)\in R\\}.$

For each $q\in S$, let $E_{A}(q)$ denote the set of all states that are
indistinguishable from $q$ according to the “everybody in $A$ knows” relation
$\sim_{A}^{E}$.

###  4.1 Failure of the HM Property

We immediately state the failure of the HM property for our notion of
bisimulation for ATL∗ under imperfect information.

######  Theorem 12.

For $x\in\\{sub,obj\\}$, there exists iCGS $\mathcal{G},\mathcal{G}^{\prime}$,
and states $q,q^{\prime}$, such that $q\thickapprox_{Ag}^{x}q^{\prime}$ and
$q\Lleftarrow\\!\\!\not\\!\\!\\!\Rrightarrow_{Ag}q^{\prime}$.

We prove Theorem 12 first for the subjective and then for the objective
semantics.

$\mathcal{G}_{3}$ |  | $\mathcal{G}_{4}$
---|---|---
$q_{1}$$q_{2}$$q_{3}$$q_{4}$$q_{\top}$$p$$q_{\bot}$121 $(a,x)$ $(b,y)$ $(a,x)$ $(b,y)$ $(a,x)$ $(b,y)$ $(a,x)$ $(b,y)$ |  | $q^{\prime}_{1}$$q^{\prime}_{2}$$q^{\prime}_{3}$$q^{\prime}_{4}$$q^{\prime}_{\top}$$p$$q^{\prime}_{\bot}$121$(a,x)$ $(a,x)$ $(b,y)$ $(a,x)$ $(b,y)$ $(b,y)$
Figure 5: A counterexample to Hennessy-Milner property for subjective
semantics. Available actions: $\\{a,b,c\\}$ for agent 1, $\\{x,y,z\\}$ for
agent 2.

Subjective Semantics. Consider the two-agent iCGS in Fig. 5. In each state
agent 1 can execute actions $\\{a,b,c\\}$ while agent 2 can execute
$\\{x,y,z\\}$. The transitions shown lead to $q_{\top}$ and
$q^{\prime}_{\top}$, while the omitted transitions lead to $q_{\bot}$ and
$q^{\prime}_{\bot}$, respectively. Via case-by-case analysis it can be proved
that $q_{i}\thickapprox_{Ag}^{subj}q_{j}$,
$q^{\prime}_{i}\thickapprox_{Ag}^{subj}q^{\prime}_{j}$, and
$q_{i}\thickapprox_{Ag}^{subj}q^{\prime}_{j}$, for $i,j\in\\{1,2,3,4\\}$, and
also $q_{\bot}\thickapprox_{Ag}^{subj}q^{\prime}_{\bot}$,
$q_{\top}\thickapprox_{Ag}^{subj}q^{\prime}_{\top}$. Therefore,
$\mathcal{G}_{3}$ and $\mathcal{G}_{4}$ are $Ag$-equivalent, i.e., they
satisfy the same $Ag$-formulas in ATL∗. However, we show that there is no
$Ag$-bisimulation between the two iGCS. In particular, for any
$i,j\in\\{1,2,3,4\\}$, state $q_{i}$ cannot be $Ag$-bisimular with any state
$q^{\prime}_{j}$. In the proof we make use of the following lemma.

######  Lemma 13.

Let $A\subseteq Ag$. If $q\Lleftarrow\\!\\!\\!\Rrightarrow_{A}q^{\prime}$ then

  1. 1.

for all $r^{\prime}\in C_{A}(q^{\prime})$, there exists $r\in C_{A}(q)$ such
that $r\Rrightarrow_{A}r^{\prime}$;

  2. 2.

for all $r\in C_{A}(q)$, there exists $r^{\prime}\in C_{A}(q^{\prime})$ such
that $r\Rrightarrow_{A}r^{\prime}$.

###### Proof.

The thesis of the lemma follows immediately from the observation that
$C_{A}(q^{\prime})\subseteq\mathit{Img}({C_{A}(q)},{\Rrightarrow_{A}})$, which
in turn can be shown via straightforward induction on the length of the path
w.r.t. relation $\sim^{C}_{A}$ that joins $q^{\prime}$ with $r^{\prime}$. ∎

Now, set $T=\\{q_{1},q_{2},q_{3},q_{4}\\}$ and
$T^{\prime}=\\{q_{1}^{\prime},q_{2}^{\prime},q_{3}^{\prime},q_{4}^{\prime}\\}$,
and note that, for the partial strategy $\sigma_{Ag}$ whose domain is $T$ and
is defined by $\sigma_{Ag}(q_{i})=(a,x)$ for all $q_{i}\in T$, we have
$succ(T,\sigma_{Ag})=\\{q_{\top}\\}$. On the other hand, note that for any
partial strategy $\sigma^{\prime}_{Ag}$ whose domain is $T^{\prime}$, we have
$succ(T^{\prime},\sigma^{\prime}_{Ag})=\\{q^{\prime}_{\top},q^{\prime}_{\bot}\\}$.

So, if we assume the existence of a strategy simulator
$ST:\mathit{PStr}_{A}(C_{A}(q_{i}))\rightarrow\mathit{PStr}_{A}(C_{A}^{\prime}(q^{\prime}_{i}))$,
then
$succ(T^{\prime},ST(\sigma^{1}_{Ag}))=\\{q^{\prime}_{\bot},q^{\prime}_{\top}\\}$,
which implies that there exists $q^{\prime}_{j}\in T^{\prime}$ such that
$succ(q^{\prime}_{j},\sigma^{\prime}_{Ag})=q^{\prime}_{\bot}$. On the other
hand, by Lemma 13, there exist $q_{i}\in T$ such that
$q_{i}\Rrightarrow_{Ag}q^{\prime}_{j}$. But
$succ(q_{i},\sigma^{1}_{Ag})=q_{\top}$, which is in contradiction with point
$1.(c)$ in Def. 5, as it cannot be the case that
$q_{\top}\Rrightarrow_{Ag}q^{\prime}_{\bot}$.

$\mathcal{G}_{5}$ |  | $\mathcal{G}_{6}$
---|---|---
${\;}q_{0}{\;}$${\;}q_{1}{\;}$${\;}q_{2}{\;}$$\mathsf{{win}}$${\;}q_{3}{\;}$$1$$L$$R$$R$$L$ |  | ${\;}q^{\prime}_{0}{\;}$${\;}q^{\prime}_{2}{\;}$$\mathsf{{win}}$${\;}q^{\prime}_{3}{\;}$$L$$R$
Figure 6: A counterexample to the Hennessy-Milner property for objective
semantics.

Objective Semantics. Consider the single-agent iCGS in Fig. 6 in which
$q_{0}\not\thickapprox_{Ag}^{subj}q^{\prime}_{0}$. Observe first that, by
symmetry, we have $q_{0}\thickapprox_{Ag}^{x}q_{1}$, for
$x\in\\{\mathit{subj},\mathit{obj}\\}$. Hence, the same two strategies (play
$R$, play $L$) can be executed in $q_{0}$ and $q_{1}$. For each such strategy,
its subtree starting from $q_{0}$ is isomorphic to the corresponding tree
starting from $q^{\prime}_{0}$, we thus have
$q_{0}\thickapprox_{Ag}^{obj}q^{\prime}_{0}$. In particular, we can establish
that $q_{i}\thickapprox_{Ag}^{obj}q^{\prime}_{i}$, for all $i\in\\{0,2,3\\}$.
On the other hand, as both $q_{0}\thickapprox_{Ag}^{obj}q^{\prime}_{0}$ and
$q_{1}\thickapprox_{Ag}^{obj}q^{\prime}_{0}$, the simulator function
$ST_{\\{q_{0},q_{1}\\},\\{q^{\prime}_{0}\\}}$ should satisfy
$ST_{\\{q_{0},q_{1}\\},\\{q^{\prime}_{0}\\}}(L)=L$ and
$ST_{\\{q_{0},q_{1}\\},\\{q^{\prime}_{0}\\}}(L)=R$, a contradiction. Hence, it
is not the case that
$q_{0}{\Lleftarrow\\!\\!\\!\Rrightarrow_{Ag}}q^{\prime}_{0}$.

As a consequence of Theorem 12, our notion of bisimulation is sufficient for
the preservation of formulas in ATL∗, but it is not necessary. In particular,
it does not enjoy the Hennessy-Milner property. In the following section we
investigate this problem more closely.

###  4.2 Towards a Tight Characterization of ATL∗-Equivalence

In this section we investigate necessary, rather than sufficient, conditions
for logical equivalence. Specifically, we introduce a notion of pre-simulation
and prove that it is implied by logical equivalence for the subjective variant
of the semantics, while being strictly weaker.

######  Definition 14 (Pre-bisimulation).

Let $\mathcal{G}$ and $\mathcal{G}^{\prime}$ be two iCGS defined on the same
sets $Ag$ of agents and $AP$ of atoms. Let $A\subseteq Ag$ be a coalition of
agents. A relation $\rightsquigarrow_{A}\subseteq S\times S^{\prime}$ is a
_pre-simulation_ iff there exists a simulator $ST$ of partial strategies for
$A$ w.r.t. $\rightsquigarrow_{A}$, such that $q\rightsquigarrow_{A}q^{\prime}$
implies that conditions (a) and (b) in Def. 5 hold and

  1. (c’)

For every states $r\in E_{A}(q)$, $r^{\prime}\in E_{A}^{\prime}(q^{\prime})$
such that $r\rightsquigarrow_{A}r^{\prime}$, for every partial uniform
strategy $\sigma_{A}\in PStr_{A}(E_{A}(q))$, and every state $s^{\prime}\in
succ(r^{\prime},ST(\sigma_{A}))$, there exists a state $s\in
succ(r,\sigma_{A})$ such that $s\rightsquigarrow_{A}s^{\prime}$.

A relation $\leftrightsquigarrow_{A}$ is called _pre-bisimulation_ if both
$\leftrightsquigarrow_{A}$ and $\leftrightsquigarrow_{A}^{-1}$ are _pre-
simulations_.

The key difference between the pre-bisimulations in Def. 14 and the
bisimulations in Def. 5 regards the domains of the partial uniform strategies
mapped by strategy simulator $ST$: these are common knowledge neighbourhoods
for bisimulation, and simple collective knowledge neighbourhoods for pre-
bisimulations. Moreover, pre-bisimulation need not to satisfy condition (2) in
Def. 5.

We can now prove the following result.

######  Theorem 15 (Necessary Conditions on $\thickapprox_{A}^{subj}$).

If $q\thickapprox_{A}^{subj}q^{\prime}$, then there exists a pre-bisimulation
$\leftrightsquigarrow_{A}$ such that $q\leftrightsquigarrow_{A}q^{\prime}$.

###### Proof.

We prove that $\thickapprox_{A}^{subj}$ is a pre-bisimulation. The proof is by
contradiction. It is routine to prove that $\thickapprox_{A}^{subj}$ satisfies
points (a) and (b) in Def. 5, we therefore focus on point (c’). Let
$q\thickapprox_{A}^{subj}q^{\prime}$ and to obtain a contradiction suppose
that $\sigma_{A}\in\mathit{PStr}_{A}(E_{A}(q))$ is such that for every
$\sigma_{A}^{\prime}\in\mathit{PStr}_{A}(E_{A}(q^{\prime}))$ there exists
$r\in E_{A}(q)$, $r^{\prime}\in E_{A}(q^{\prime})$, and $s^{\prime}\in
succ(r^{\prime},\sigma_{A}^{\prime})$ such that for every $s\in
succ(r,\sigma_{A})$, we have $s\not\thickapprox_{A}^{subj}s^{\prime}$. This in
particular means that for each such $s$ there exists a formula
$\varphi_{s}^{\sigma_{A}^{\prime}}$ in ATL∗ such that
$(\mathcal{G},s)\models_{\mathit{subj}}\varphi_{s}^{\sigma_{A}^{\prime}}$ and
$(\mathcal{G}^{\prime},s^{\prime})\models_{\mathit{subj}}\neg\varphi_{s}^{\sigma_{A}^{\prime}}$.
Now, define formula $\varphi_{r}^{\sigma_{A}^{\prime}}=\bigvee_{s\in
succ(r,\sigma_{A})}\varphi_{s}^{\sigma_{A}^{\prime}}$ and observe that
$\varphi_{r}^{\sigma_{A}^{\prime}}$ is true in the next step from $r$ by using
$\sigma_{A}$, whereas this is not the case for $r^{\prime}$. Finally, let
$\varphi=\bigwedge_{\sigma_{A}^{\prime}\in\mathit{PStr}_{A}(E_{A}(q^{\prime}))}\varphi_{r}^{\sigma_{A}^{\prime}}$.
To conclude, it suffices to observe that
$(\mathcal{G},q)\models_{\mathit{subj}}\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}X\varphi$
and
$(\mathcal{G}^{\prime},q^{\prime})\models_{\mathit{subj}}\neg\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}X\varphi$,
a contradiction with $q\thickapprox_{A}^{subj}q^{\prime}$. ∎

The following corollary to Theorem 15 deals with the case of objective
semantics.

######  Corollary 16 (Necessary Condition on $\thickapprox_{A}^{obj}$).

If $q\thickapprox_{A}^{obj}q^{\prime}$, then for each uniform strategy
$\sigma_{A}$ there exists a uniform strategy $\sigma_{A}^{\prime}$ such that:

$succ(q^{\prime},\sigma_{A}^{\prime})\subseteq\mathit{Img}({succ(q,\sigma_{A})},{\thickapprox_{A}^{obj}})$

$\mathcal{G}_{7}$ |  | $\mathcal{G}_{8}$
---|---|---
$q_{I}^{1}$$q_{I}^{4}$$q_{I}^{2}$$q_{I}^{3}$$q_{1}$$q_{2}$$q_{3}$$q_{4}$$q_{\top}$$p$$q_{\bot}$1111121 $(a,x)$ $(a,x)$ $(b,y)$ $(a,x)$ $(b,y)$ $(b,y)$ |  | ${q^{\prime}}^{1}_{I}$${q^{\prime}}^{3}_{I}$${q^{\prime}}^{2}_{I}$$q^{\prime}_{1}$$q^{\prime}_{2}$$q^{\prime}_{3}$$q^{\prime}_{\top}$$p$$q^{\prime}_{\bot}$11112$(a,x)$ $(a,x)$ $(b,y)$ $(a,x)$ $(b,y)$
Figure 7: Pre-bisimulation does not imply logical equivalence.

It should be noted that pre-bisimilarity does not imply logical equivalence of
two models. Consider the two-agent iCGS in Fig. 7. In the states that are
$1$-indistinguishable from $q_{I}^{1}$ (respectively, ${q^{\prime}}^{1}_{I}$)
the models are equipped with a single deterministic transition. In each of the
remaining states agent 1 can execute actions $\\{a,b,c\\}$ and agent 2 can
execute $\\{x,y,z\\}$. We assume that the transitions that are not depicted in
the figure lead to $q_{\bot}$ or $q_{\bot}^{\prime}$, respectively. Now,
observe that
$(\mathcal{G}_{7},q_{I}^{1})\models_{\mathit{subj}}\neg\langle\\!\langle{Ag}\rangle\\!\rangle_{{}_{\\!\mathit{}}}Fp$,
as it is not possible to choose a strategies for both agents that select the
same pair of actions over the set of successors of $q_{I}^{1}$ and leads to
$q_{\top}$. On the other hand, such choice is possible for the successors of
${q^{\prime}}_{I}^{1}$, namely it suffices to assign $(a,x)$ to each
${q^{\prime}}^{i}_{I}$, where $i\in\\{1,2,3\\}$, to see that
$(\mathcal{G}_{8},{q^{\prime}}_{I}^{1})\models_{\mathit{subj}}\langle\\!\langle{Ag}\rangle\\!\rangle_{{}_{\\!\mathit{}}}Fp$.
Finally, we can define a relation $\leftrightsquigarrow_{A}$ such that
$q_{i}\leftrightsquigarrow_{A}q^{\prime}_{i}$ and
$q^{i}_{I}\leftrightsquigarrow_{A}{q^{\prime}}^{i}_{I}$ for all
$i\in\\{1,2,3\\}$, $q_{\top}\leftrightsquigarrow_{A}q^{\prime}_{\top}$,
$q_{\bot}\leftrightsquigarrow_{A}q^{\prime}_{\bot}$, and
$q_{4}\leftrightsquigarrow_{A}q^{\prime}_{3}$,
$q^{4}_{I}\leftrightsquigarrow_{A}{q^{\prime}}^{3}_{I}$. A case-by-case check
shows that $\leftrightsquigarrow_{A}$ is a pre-bisimulation. Specifically,
conditions (a) and (b) in Def. 5 are immediate. As regards (c’), notice that
for pre-simulations strategy simulators are defined on collective knowledge
neighbourhoods rather than common knowledge ones. More specifically,
$C_{Ag}(q_{1})=\\{q_{1},q_{2},q_{3},q_{4}\\}$ and
$C_{Ag}(q^{\prime}_{1})=\\{q_{1},q_{2},q_{3}\\}$, while
$E_{Ag}(q_{1})=\\{q_{1},q_{2},q_{3}\\}$ and
$E_{Ag}(q^{\prime}_{1})=\\{q_{1},q_{2},q_{3}\\}$. Then, while a strategy
simulator can be defined on $E_{Ag}(q_{1})$, $E_{Ag}(q^{\prime}_{1})$, so such
simulator exists on $C_{Ag}(q_{1})$, $C_{Ag}(q^{\prime}_{1})$.

##  5 Case Study: the ThreeBallot Voting Protocol

BALLOT | BALLOT | BALLOT
---|---|---
Andy Jones |  |  Andy Jones |  |  Andy Jones |
Bob Smith |  |  Bob Smith |  |  Bob Smith |
Carol Wu |  |  Carol Wu |  |  Carol Wu |
3147524 | 7523416 | 5530219
Figure 8: ThreeBallot showing a vote for Bob Smith

ThreeBallot [44, 45] is a voting protocol that strives to achieve some
desirable properties, such as anonymity and verifiability of voting, without
the use of cryptography. We provide a brief illustration of the protocol
hereafter and refer to [44, 45] for further details. Each voter identifies
herself at the poll site, and receives a “multi-ballot” paper to vote with.
The multi-ballot consists of three vertical ribbons – identical except for ID
numbers at the bottom (see Fig. 8, presented after [44]). The voter fills in
the multi-ballot, separates the three ribbons, and casts them into the ballot
box. The ballot box has the property, as usual, that it effectively scrambles
the ballot order, destroying any indication of which triple of ballots
originally went together, and what order ballots were cast in. To vote for a
candidate, one must mark exactly two (arbitrary) bubbles on the row of the
candidate. To not vote for a candidate, one must mark exactly one of the
bubbles on the candidate’s row (again, arbitrarily). In all the other cases
the vote is invalid. The ballots are tallied by counting the number of bubbles
marked for each candidate, and then subtracting the number of voters from the
count.

While voting, the voter also receives a copy of one of her three ballots, and
she can take it home. After the election has terminated, all the ballots are
scanned and published on a web bulletin board. In consequence, the voter can
check if her receipt matches a ballot listed on the bulletin board. If no
ballot matches the receipt, the voter can file a complaint.

Since ThreeBallot is not a cryptographic protocol, it does not heavily rely on
computers and counting can be done directly. Moreover, voters have no
responsibility to ensure the integrity of cryptographic keys, and the security
process in their vote is essentially the same as with traditional ballots.

Properties. ThreeBallot was proposed to provide several properties that reduce
the possibility of electoral fraud. _Anonymity_ (cf. e.g. [46]) requires that
no agent should ever know how another voter voted, except in cases where it is
inevitable, such as when all voters voted for the same candidate. Anonymity is
important as it limits the opportunities of coercion and vote-buying. The
latter kind of properties is usually captured by the notions of coercion-
resistance and receipt-freeness [68, 69, 70]. In particular, _coercion-
resistance_ requires that the voter cannot reveal the value of her vote beyond
doubt, even if she fully cooperates with the coercer. As a consequence, the
coercer has no way of deciding whether to execute his threat (or, dually, pay
for the vote). A preliminary formalization of coercion-resistance and receipt-
freeness in ATL has been presented in [71].

Finally, _end-to-end voter verifiability_ [34, 33] provides a way to verify
the outcome of the election by allowing voters to audit the information
published by the system. Typically, the focus is on individual verifiability:
each voter should be able check if her vote has been taken into account and
has not been altered.

###  5.1 iCGS Models

Here we present three iCGS models of the ThreeBallot voting protocol. All
models have been specified in ISPL (Interpreted System Programming Language),
the input language of the MCMAS model checker for multi-agent systems [15]. We
do not model several aspects of the voting system: the ID of each ribbon, the
copy of the ribbon which is given back to each voter after casting her ballot,
the possibility for voters to verify the presence of the ribbon they are given
back after voting. Moreover, we model a single attacker who is also a voter
and, as such, follows the voting protocol and does not interact in any
particular way with the other agents.

In the iCGS below, each agent is represented by means of her local variables
and their evolution. The vote collector and bulletin board (BB) are modeled by
the Environment agent (called Env). This agent posesses local variables
modeling the fact that the voting process is open and the values of ribbons on
the BB. These variables are observable by all voters, including the attacker.
Env also owns private variables for collecting ribbons and can perform the
three actions $stop$, $collect$, $nop$ to close the voting process, to collect
the votes, and finally to loop after the publication of the BB.

The agents representing voters have each a private variable representing their
vote for each candidate, and they share three “ballot” variables with the
environment Env. These variables represent the ribbons created by the “voting
machine”. Casting the vote is modeled by creating the three ribbons,
consistently with the choice for each candidate. We assume that votes are
immediately cast in the initial state. Being visible by Env, the values of the
three ribbons are copied by Env onto the (variables represented on the) BB in
a random order. Each agent has two actions: $vote$, by which the voter casts
her vote, and $nop$, a non-voting or idle action. Action $vote$ is enabled
only in the initial state, $nope$ is always enabled. All agent variables are
never modified during the voting process.

In the first iCGS, denoted $\mathcal{G}_{tot}$, for each agent choice, all
configurations of the three ribbons that are compatible with the agent’s
choice may occur. The communication between each agent and Env is entirely at
Env’s charge, who has direct access to agents’ ribbons and copies them onto
the BB. Also, copying is done randomly: Env chooses a not-yet-copied ribbon
from some voter who has cast her vote (boolean variables are provided to help
Env identify these situations) and copies it onto a free position on the BB.

With the second model, denoted $\mathcal{G}_{lex}$, we model a voting machine
which sorts, according to the lexicographic order, the three ribbons produced
for the agent’s vote, and places the greatest one in the first “ballot”
variable of the voter, the second greatest in the second variable, and the
least in the third variable. Hence, for each choice of an agent, there are
still several configurations of ribbons that are produced, but we no longer
consider all permutations of a given configuration, but only a single
representative.

Finally, we modify $\mathcal{G}_{lex}$ into a third model, in which Env no
longer copies ribbons on the BB, but rather counts the votes for each
candidate by peeping at the ”ballot” variables of each voter. This model is
denoted $\mathcal{G}_{count}$.

More formally, in the case of $\mathcal{G}_{tot}$ for $n$ voters and $c$
candidates, each global state has the form
$(vopen,pub,(ribb_{\ell})_{1\leqslant\ell\leqslant
3n},(ch_{i},v_{i})_{1\leqslant i\leqslant n},(s_{ij})_{1\leqslant i\leqslant
n,1\leqslant j\leqslant 3})$ such that

  1. 1.

The Boolean variable $vopen$ is true when the vote is open, while $pub$
signals that all ribbons of agents that have voted have been copied on the BB.

  2. 2.

The local states for voter $i$ is
$(vopen,pub,ribb_{1},ribb_{2},...ribb_{3n},v_{i},s_{i1},s_{i2},s_{i3})$. This
means that each voter sees the BB during the process of copying ribbons. This
is not harmful for anonymity since indistinguishability is state-based, which
means agents do not remember their observations.

  3. 3.

Integer $1\leqslant ch_{i}\leqslant c$ specifies the choice of voter $i$.

  4. 4.

Boolean $v_{i}$ ($1\leqslant i\leqslant n$) registers whether agent $i$ has
voted.

  5. 5.

Variables $s_{ij}$ ($1\leqslant j\leqslant 3$) represent the three ”strips” of
the ballot for voter $i$. They are shared between each agent and Env, who
copies them onto the BB. Value range is $\\{0,2^{c}-1\\}\cup\\{\bot\\}$ with
$s_{ij}=\bot$ denoting that strip $s_{ij}$ has been copied on the BB.

  6. 6.

Integer variables $ribb_{\ell}$ ($1\leqslant\ell\leqslant 3n$) represent the
content of the BB. Value range is $\\{0,2^{c}-1\\}\cup\\{\bot\\}$, with
$ribb_{\ell}=\bot$ denoting that no content of a strip has been copied into
this ribbon on the BB.

Initial states are such that $vopen=true$, $v_{i}=false$ for all $i\leqslant
n$, variables $ribb_{\ell}$ are set to the _undefined_ value $\bot$ and, for
variables $s_{ij}$ we have the following rules modeling the creation of a
triple of ribbons compatible with the choice of a candidate: for each voter
$i$, let $b_{jk}=b^{i}_{jk}$ be the bit representing the bubble on the line
corresponding to candidate $k$ of the $j$th ballot of $i$’s vote, as
represented by the value of $ch_{i}$. A tuple $(b_{jk})_{1\leqslant j\leqslant
3,1\leqslant k\leqslant c}$ is _compatible_ with choice $ch_{i}$ if the
following holds:

  1. 1.

if $ch_{i}=k$ then for some $p\leqslant 3$, $b_{pk}=0$ and for all
$p^{\prime}\neq p$, $b_{p^{\prime}k}=1$

  2. 2.

if $ch_{i}\neq k$ then for some $p\leqslant 3$, $b_{pk}=1$ and for all
$p^{\prime}\neq p$, $b_{p^{\prime}k}=0$

Denote $B(ch_{i})$ the set of bit tuples $(b_{jk})_{1\leqslant j\leqslant
3,1\leqslant k\leqslant c}$ compatible with $ch_{i}$. Denote further by
$R(ch_{i})$ the transformation of these bit tuples into integer triples
modeling the valid ballots compatible with choice $ch_{i}$:

$R(ch_{i})=\\{(st_{j})_{1\leqslant j\leqslant 3}\mid st_{j}=\sum_{1\leqslant
k\leqslant c}b_{jk}\cdot 2^{k-1},(b_{jk})_{1\leqslant j\leqslant 3,1\leqslant
k\leqslant c}\in B(ch_{i})\\}$

As an example, valid triples of integers compatible with a vote for candidate
$2$, for $c=2$, are all permutations of $(3,2,0)$ together with all
permutations of $(2,2,1)$. Then $(s_{ij})_{1\leqslant j\leqslant 3}\in
R(ch_{i})$ for every $1\leqslant i\leqslant n,1\leqslant j\leqslant 3$.

Finally, in $\mathcal{G}_{tot}$ the protocol for the ThreeBallot system is
given as follows:

  1. 1.

actions $vote$ and $nop$ are available to all voters when $vopen=true$;
otherwise, only $nop$ is available.

  2. 2.

$stop$ and $nop$ are available to Env when $vopen=true$.

  3. 3.

$collect$ and $publish$ are available to Env when $vopen=false$.

Then, transitions are of the form:

$\displaystyle(vopen,pub,(ribb_{\ell})_{1\leqslant\ell\leqslant
3n},(\\!ch_{i},v_{i}\\!)_{1\leqslant i\leqslant n},(\\!s_{ij}\\!)_{1\leqslant
i\leqslant n,1\leqslant j\leqslant
3}\\!)\xrightarrow{(a_{e},a_{1},a_{2},...,a_{n})}$
$\displaystyle(vopen^{\prime}\\!,pub^{\prime}\\!,(ribb^{\prime}_{\ell})_{1\leqslant\ell\leqslant
3n},(ch_{i}^{\prime},v_{i}^{\prime})_{1\leqslant i\leqslant
n},(s_{ij}^{\prime})_{1\leqslant i\leqslant n,1\leqslant j\leqslant 3})$

where

  1. 1.

$vopen^{\prime}=false$ if $a_{e}=stop$ or $vopen=false$; $vopen^{\prime}=true$
otherwise.

  2. 2.

For $a_{i}=vote$, $v_{i}^{\prime}=true$, and for $a_{i}=nop$,
$v^{\prime}_{i}=v_{i}$.

  3. 3.

For $a_{e}=collect$ (and hence $a_{i}=nop$ for all $i$) we have the following:

    1. (a)

there exists some subset of pairs
$A\subseteq\\{1,\ldots,n\\}\times\\{1,2,3\\}$ and a pair $(i_{0},j_{0})\not\in
A$ such that

      1. i.

$s_{ij}^{\prime}=s_{ij}=\bot$ for all $(i,j)\in A$

      2. ii.

$s_{i_{0},j_{0}}^{\prime}=\bot$, $s_{i_{0},j_{0}}\neq\bot$

      3. iii.

$s_{ij}^{\prime}=s_{ij}\neq\bot$ for all $(i,j)\not\in
A\cup\\{(i_{0},j_{0})\\}$;

    2. (b)

there exists some $B\subseteq\\{1,\ldots,3n\\}$ with $card(B)=card(A)$ and
some integer $k\not\in B$, $1\leqslant k\leqslant 3n$ such that

      1. i.

$ribb^{\prime}_{\ell}=ribb_{\ell}\neq\bot$ for all $\ell\in B$

      2. ii.

$ribb_{k}=\bot$, $ribb^{\prime}_{k}=s_{i_{0},j_{0}}$

      3. iii.

$ribb_{\ell}=ribb^{\prime}_{\ell}=\bot$ for all $\ell\not\in B\cup\\{k\\}$.

  4. 4.

Action $a_{e}=publish$ can only be executed when, for each $i$, either
$s_{i1}=s_{i2}=s_{i3}=\bot$ or $v_{i}=false$, and its effect is to modify only
$pub^{\prime}=true$, all other variables remaining unchanged.

In the iCGS $\mathcal{G}_{lex}$ transitions are identical to the above, the
only difference being in the initial states, more specifically in the
configuration of variables $s_{ij}$. Intuitively, for each choice $ch_{i}$ of
voter $i$, we only keep those initial configurations in which
$(s_{i1},s_{i2},s_{i3})$ is the maximal, in lexicographic order, among the
encodings $R_{ch_{i}}$ of $ch_{i}$. Formally, given a triple of integers
$t=(t_{1},t_{2},t_{3})$, we denote with $Perm(t)$ the set of all permutations
of triple $t$. Then, the initial states in $\mathcal{G}_{lex}$ are the initial
states of $\mathcal{G}_{tot}$ for which $(s_{i1},s_{i2},s_{i3})=\max
Perm\big{(}(s_{i1},s_{i2},s_{i3})\big{)}$, the maximum being considered under
the lexicographic order.

Finally, the iCGS $\mathcal{G}_{count}$ is similar to $\mathcal{G}_{lex}$ but
all variables $ribb_{\ell}$ are replaced with $c$ variables
$(co_{k})_{1\leqslant k\leqslant c}$. The local states for agent $i$ are then
of the form $(vopen,pub=0,v_{i},s_{i1},s_{i2},s_{i3})$ and
$(vopen,pub=1,co_{1},\ldots,co_{c},v_{i},s_{i1},s_{i2},s_{i3})$. The
specification of transitions is then the same as for $\mathcal{G}_{tot}$,
except for $a_{e}=collect$ and items 3.(b.i)-3.(b.iii) above (defining the
updates of variables $ribb_{\ell}$), which are replaced by the following:

  * 3.(b’)

For each $1\leqslant k\leqslant c$, $co^{\prime}_{k}=co_{k}+d_{i_{0}j_{0}k}$,
where $d_{i_{0}j_{0}k}$ is the $k$-th least significant bit of
$s_{i_{0}j_{0}}$.

###  5.2 Coercion freeness and anonymity properties for the ThreeBallot

In this section we present the formulas that are of interest for the
verification of ThreeBallot. We verify two types of formulas: a variant of
coercion resistance [71] and a variant of anonymity. The coerction resistance
property specifies the fact that the attacker $att$ has no strategy by which
he could know how agent $i$ has voted ($i\neq att$):

$\varphi_{i}=\llangle att\rrangle F\big{(}(pub\wedge
v_{i})\rightarrow\bigvee_{1\leqslant j\leqslant nc}K_{att}(j=ch_{i})\big{)}$

Recall that, in our model the attacker is also a voter, which corresponds to
situations in which a voter fully cooperates with the attacker. Additionnaly,
as already noted in Section 2, the knowledge operator is definable in ATL with
the subjective interpretation as $K_{att}\varphi=\llangle att\rrangle\varphi
U\varphi$.

The anonymity property does not require ATL but rather CTLK, the combination
of branching-time temporal logic with epistemic logic of e.g. [72]. The $AG$
operator from CTLK, whose meaning is that along all paths the target
subformula holds globally, can be defined as usual in ATL as follows:

$AG\varphi\equiv\llangle\emptyset\rrangle G\varphi$

Then, the anonymity property of interest for ThreeBallot is that any of the
agents cannot know, at any time instant, the way another agent has voted:

$\varphi_{i}^{c}=AG(\bigwedge_{1\leqslant j\leqslant nc}\neg
K_{att}p_{ch_{i}=j})$

Note that anonymity is not ensured when there are at most three voters,
including the attacker (who may vote).

###  5.3 Bisimulations for $\mathcal{G}_{tot}$, $\mathcal{G}_{lex}$ and
$\mathcal{G}_{count}$

The three iCGS defined in the previous section appear to be naturally related,
in particular w.r.t. the properties pertaining to the attacker modifying the
outcome of the vote or breaking anonymity. The interest in simplifying the
model is that checking the coercion resistance property can be done faster and
with less memory on $\mathcal{G}_{count}$ than on $\mathcal{G}_{lex}$, which,
on its turn, requires less time and memory than $\mathcal{G}_{tot}$, as we
will see in the last section on experimental results. In this section we show
that the three models are bisimilar for the attacker, for the set of atomic
propositions that refer only to choices of agents. Bisimulations formalize the
“natural relation” between these iCGS and allows us to check coercion
resistance on the smallest iCGS and then transfer the result to the two
others, in particular to the original model $\mathcal{G}_{tot}$. Note that
these bisimulations work because the properties do not refer to the status of
the BB. For instance, these bisimulations would not be useful for simplifying
systems for verifiability [37].

Formally, for each choice for an agent $i$ to vote for candidate $j$, we
introduce an atomic proposition $p_{ch_{i}=j}$, which holds true only in those
states in which $ch_{i}=j$. Then, if we denote the attacker $att=n$ and
$AP=\\{p_{ch_{i}=j}\mid 1\leqslant i\leqslant n,1\leqslant j\leqslant c\\}$,
we prove that the following relation is an $\\{att\\}$-bisimulation over $AP$
between $\mathcal{G}_{tot}$ and $\mathcal{G}_{lex}$:

$\displaystyle(vopen,pub,(ribb_{\ell})_{1\leqslant\ell\leqslant
3n},(ch_{i},v_{i})_{1\leqslant i\leqslant n},(s_{ij},a_{ij})_{1\leqslant
i\leqslant n,1\leqslant j\leqslant
3})\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{1}$
$\displaystyle(vopen^{\prime},pub^{\prime},(ribb^{\prime}_{\ell})_{1\leqslant\ell\leqslant
3n},(ch_{i}^{\prime},v_{i}^{\prime})_{1\leqslant i\leqslant
n},(s_{ij}^{\prime},a_{ij}^{\prime})_{1\leqslant i\leqslant n,1\leqslant
j\leqslant 3})$

iff the following holds:

  1. 1.

$vopen=vopen^{\prime}$, $pub=pub^{\prime}$, $v_{i}=v_{i}^{\prime}$,
$ch_{i}=ch_{i}^{\prime}$ for all $1\leqslant i\leqslant n$,
$s_{att,j}=s_{att,j}^{\prime}$ and $a_{att,j}=a_{att,j}^{\prime}$ for all
$1\leqslant j\leqslant 3$ and $ribb_{\ell}=ribb^{\prime}_{\ell}$ for all
$1\leqslant\ell\leqslant 3n$.

  2. 2.

For every $1\leqslant i\leqslant n$, if we denote $b_{jk}$ the $k$th least
significant bit of $s_{ij}$ and $b^{\prime}_{jk}$ the $k$th bit of
$s^{\prime}_{ij}$, then both $(b_{jk})_{1\leqslant j\leqslant 3,1\leqslant
k\leqslant c},(b^{\prime}_{jk})_{1\leqslant j\leqslant 3,1\leqslant k\leqslant
c}\in B(ch_{i})$.

  3. 3.

Denote $\rho_{i}$ the $S_{3}$-permutation of $(s_{i1},s_{i2},s_{i3})$ into
$(s^{\prime}_{i1},s^{\prime}_{i2},s^{\prime}_{i3})$, i.e.
$s_{ij}=s^{\prime}_{i\rho_{i}(j)}$. Also when $s_{ij}=s^{\prime}_{ij}=\bot$ we
put $\rho_{i}=id_{\\{1,2,3\\}}$. Then $a_{ij}=a^{\prime}_{i\rho_{i}(j)}$ for
all $1\leqslant i\leqslant n-1,1\leqslant j\leqslant 3$.

Intuitively, item (3) above says that $(b^{\prime}_{jk})$ is the largest, in
lexicographic order, among all tuples in $B_{ch_{i}}$ that are permutations of
$(b_{jk})$.

For $\mathcal{G}_{lex}$ and $\mathcal{G}_{count}$, we consider the following
$\\{att\\}$-bisimulation over $AP$:

$\displaystyle(vopen,pub,(\\!ribb_{\ell}\\!)_{1\leqslant\ell\leqslant
3n},\\!(\\!ch_{i},v_{i}\\!)_{1\leqslant i\leqslant
n},(s_{ij},a_{ij})_{1\leqslant i\leqslant n,1\leqslant j\leqslant
3})\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{2}$
$\displaystyle(vopen^{\prime},pub^{\prime},(co_{k})_{1\leqslant k\leqslant
c},(ch_{i}^{\prime},v_{i}^{\prime})_{1\leqslant i\leqslant
n},(s_{ij}^{\prime},a_{ij}^{\prime})_{1\leqslant i\leqslant n,1\leqslant
j\leqslant 3})$

where:

  1. 1.

$vopen=vopen^{\prime}$, $pub=pub^{\prime}$, $v_{i}=v_{i}^{\prime}$,
$ch_{i}=ch_{i}^{\prime}$, $s_{ij}=s_{ij}^{\prime}$ and
$a_{ij}=a_{ij}^{\prime}$ for all $1\leqslant i\leqslant n,1\leqslant
j\leqslant 3$.

  2. 2.

For every $1\leqslant\ell\leqslant 3n$ and $1\leqslant k\leqslant c$, if we
denote $b_{\ell k}$ the $k$th least significant bit on the ribbon
$ribb_{\ell}$, then:

$co_{k}=\sum\big{\\{}b_{\ell k}\mid
ribb_{\ell}\neq\bot,1\leqslant\ell\leqslant 3n\big{\\}}$

To prove that these relations are indeed alternating bisimulations, note that
the condition 1.(a) is immediately satisfied as whenever
$q\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{\iota}q^{\prime}$, for
$\iota=1,2$, we must have that $(ch_{i}=j)\in q$ iff $(ch_{i}=j)\in
q^{\prime}$.

To prove properties 1.(b) and its dual for
$\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{1}$, consider states $q,r$ in
$\mathcal{G}_{tot}$ and $r\in\mathcal{G}_{lex}$ such that
$q\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{1}q^{\prime}$ and
$q\sim_{att}r$. Then it is the case that

$\displaystyle q$
$\displaystyle=(\\!vopen,\\!pub,\\!(\\!ribb_{\ell}\\!)_{1\leqslant\ell\leqslant
3n},\\!(\\!ch_{i},v_{i}\\!)_{1\leqslant i\leqslant
n},\\!(\\!s_{ij},\\!a_{ij}\\!)_{1\leqslant i\leqslant n,1\leqslant j\leqslant
3})$ $\displaystyle q^{\prime}$
$\displaystyle=(\\!vopen,\\!pub,\\!(\\!ribb_{\ell}\\!)_{1\leqslant\ell\leqslant
3n},\\!(\\!ch_{i},v_{i}\\!)_{1\leqslant i\leqslant
n},\\!(s_{ij}^{\prime}\\!,\\!a_{ij}^{\prime}\\!)_{1\leqslant i\leqslant
n,1\leqslant j\leqslant 3})$ $\displaystyle r$
$\displaystyle=(\\!vopen,\\!pub,\\!(\\!ribb_{\ell}\\!)_{1\leqslant\ell\leqslant
3n},\\!(\\!\overline{ch}_{i},\overline{v}_{i}\\!)_{1\leqslant i\leqslant
n},\\!(\\!\overline{s}_{ij},\\!\overline{a}_{ij}\\!)_{1\leqslant i\leqslant
n,1\leqslant j\leqslant 3})$

with $q,q^{\prime}$ related as per the definition of
$\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{1}$ above and
$\overline{ch}_{att}=ch_{att}$, $\overline{s}_{att,j}=s_{att,j}^{\prime}$ and
$\overline{a}_{att,j}=a_{att,j}^{\prime}$ for all $1\leqslant j\leqslant 3$.
Then set

$\displaystyle r^{\prime}$
$\displaystyle=(vopen,pub,(ribb_{\ell})_{1\leqslant\ell\leqslant
3n},(ch_{i}^{\prime},v_{i}^{\prime})_{1\leqslant i\leqslant
n-1},(\overline{ch}_{att},\overline{v}_{att}),(s_{ij}^{\prime},a_{ij}^{\prime})_{1\leqslant
i\leqslant n-1,1\leqslant j\leqslant
3},(\overline{s}_{att,j},\overline{a}_{att,j})_{1\leqslant j\leqslant 3})$

and we obtain the desired result, that is,
$q^{\prime}\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{1}r^{\prime}$ and
$r\sim_{att}r^{\prime}$. The mirror argument works as well: given
$q\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{1}q^{\prime}$ and
$q^{\prime}\sim_{att}r^{\prime}$, we can find $r$ such that
$q\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{1}r$ and
$r\sim_{att}r^{\prime}$.

Conditions 1.(b) and its dual for
$\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{2}$ can be proved similarly, by
observing that, given $q,r\in\mathcal{G}_{lex}$,
$q^{\prime}\in\mathcal{G}_{count}$, such that
$q\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{2}q^{\prime}$ and
$q\sim_{att}r$, then it is the case that

$\displaystyle q$
$\displaystyle=(\\!vopen,\\!pub,\\!(\\!ribb_{\ell}\\!)_{1\leqslant\ell\leqslant
3n},\\!(\\!ch_{i},\\!v_{i}\\!)_{1\leqslant i\leqslant
n},\\!(\\!s_{ij},\\!a_{ij}\\!)_{1\leqslant i\leqslant n,1\leqslant j\leqslant
3})$ $\displaystyle q^{\prime}\\!$
$\displaystyle=(\\!vopen,\\!pub,\\!(co_{k})_{1\leqslant k\leqslant
c},\\!(\\!ch_{i},\\!v_{i}\\!)_{1\leqslant i\leqslant
n},\\!(s_{ij}^{\prime}\\!,\\!a_{ij}^{\prime}\\!)_{1\leqslant i\leqslant
n,1\leqslant j\leqslant 3})$ $\displaystyle r$
$\displaystyle=(\\!vopen,\\!pub,\\!(ribb_{\ell})_{1\leqslant\ell\leqslant
3n},\\!(\overline{ch}_{i},\\!\overline{v}_{i}\\!)_{1\leqslant i\leqslant
n},\\!(\\!\overline{s}_{ij},\\!\overline{a}_{ij}\\!)_{1\leqslant i\leqslant
n,1\leqslant j\leqslant 3})$

with the same relation between variables of $q$ and $r$ as above. Then set

$\displaystyle r^{\prime}$ $\displaystyle=(vopen,pub,(co_{k})_{1\leqslant
k\leqslant c},(ch_{i}^{\prime},v_{i}^{\prime})_{1\leqslant i\leqslant
n-1},(\overline{ch}_{att},\overline{v}_{att}),(s_{ij}^{\prime},a_{ij}^{\prime})_{1\leqslant
i\leqslant n-1,1\leqslant j\leqslant
3},(\overline{s}_{att,j},\overline{a}_{att,j})_{1\leqslant j\leqslant 3})$

and we obtain that
$q^{\prime}\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{2}r^{\prime}$ and
$r\sim_{att}r^{\prime}$.

Further, for conditions 1.(c) and its dual, notice first that for any state
$q\in\mathcal{G}_{tot}$ or $q\in\mathcal{G}_{lex}$, $C_{att}(q)$ is the
equivalence class of $q$ w.r.t. $\sim_{att}$, that is, if
$q=(vopen,pub,(ribb_{\ell})_{1\leqslant\ell\leqslant
3n},(ch_{i},v_{i})_{1\leqslant i\leqslant n},(s_{ij},a_{ij})_{1\leqslant
i\leqslant n,1\leqslant j\leqslant 3})$, then $C_{att}(q)$ includes all and
only states where the local state for $att$ is of the form
$((ribb_{\ell})_{1\leqslant\ell\leqslant
3n},ch_{att},v_{att},(s_{att,j},a_{att,j})_{1\leqslant j\leqslant 3})$.
Similarly, for $q^{\prime}\in\mathcal{G}_{count}$ with
$q^{\prime}\\!=(\\!vopen,pub,(\\!co^{\prime}_{k}\\!)_{1\leqslant k\leqslant
c},(\\!ch_{i}^{\prime}\\!,\\!v_{i}^{\prime}\\!)_{1\leqslant i\leqslant
n},(\\!s_{ij}^{\prime}\\!,\\!a_{ij}^{\prime}\\!)_{1\leqslant i\leqslant
n,1\leqslant j\leqslant 3})$, $C_{att}(q^{\prime})$ includes all and only
states where the local state for $att$ is of the form $((co_{k})_{1\leqslant
k\leqslant c},ch_{att},v_{att},\allowbreak(s_{att,j},a_{att,j})_{1\leqslant
j\leqslant 3})$.

Then, in all three iCGS, on each neighbourhood $C_{att}(q)$, only one or two
partial strategies for $att$ can be defined, depending on whether the vote is
open or not. Therefore, we define the mapping
$ST_{C^{\mathcal{G}_{tot}}_{att}(\cdot),C^{\mathcal{G}_{lex}}_{att}(\cdot)}$
to associate to each partial strategy prescribing $nop$ to $att$ in some
$C^{\mathcal{G}_{tot}}_{att}(q)$ the quasi-identical strategy prescribing the
same action in $C^{\mathcal{G}_{lex}}_{att}(q^{\prime})$. Similarly, to the
partial strategy prescribing $vote$ to $att$ in
$C^{\mathcal{G}_{tot}}_{att}(q)$,
$ST_{C^{\mathcal{G}_{tot}}_{att}(\cdot),C^{\mathcal{G}_{lex}}_{att}(\cdot)}$
associates the strategy prescribing $vote$ in
$C^{\mathcal{G}_{lex}}_{att}(q^{\prime})$. The dual mapping $ST^{\prime}$ is
defined similarly, and analogous definitions work for bisimulation
$\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{2}$. Notice also that these
definitions satisfy the constraints on strategy simulators.

To prove condition 1.(c), consider first the strategy $vote_{att}$ prescribing
$vote$ for $att$ on $C^{\mathcal{G}_{tot}}_{att}(q)$ and consider some state
$r^{\prime}$ such that $q^{\prime}\xrightarrow{vote_{att}}r^{\prime}$. Since
when voting is enabled, Env does not collect votes, $r^{\prime}$ has the same
BB as $q^{\prime}$ and all booleans variables $a_{ij}$ are false. Therefore,
we can choose a state $r$ that has the same values as $r^{\prime}$ for the
local variables of all voters and the same BB as $q$. Then, we obtain
$q^{\prime}\xrightarrow{ST(vote_{att})}r^{\prime}$ and
$r\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{1}r^{\prime}$. A similar line
of reasoning works for $\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{2}$ as
well. The same argument applies if the strategy for the attacker is
$nop_{att}$ and $q$ and $q^{\prime}$ are states in which voting is open.

Consider now a state $q$ in which voting is closed and the strategy
$none_{att}$ prescribing action $nop$ for $att$ on
$C^{\mathcal{G}_{tot}}_{att}(q)$ and consider again some state $r^{\prime}$
such that $q^{\prime}\xrightarrow{nop_{att}}r^{\prime}$. Then the only agent
which executes a non-idle action on the above transition is Env, who copies
one of the ribbons onto the BB. This transition can then be simulated in
$\mathcal{G}_{tot}$ by copying the same ribbon (but which might be stored at a
different position in $q$ than in $q^{\prime}$) onto the BB. A mirror argument
can be used to prove 1.(c) for $ST^{\prime}$.

Thirdly, for proving condition 1.(c) for
$q\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{2}q^{\prime}$, note that the
same considerations above apply for the case of a transition from a state
$q^{\prime}$ in which the voting is open. For the case of states $q$,
$q^{\prime}$ where the voting is closed and hence only strategy $nop_{att}$ is
available to the attacker, we note that the only action that is compatible
with $q\xrightarrow{nop_{att}}r$ in both models is Env collecting votes. This
corresponds in $\mathcal{G}_{count}$ to an action in which Env counts votes,
and hence we can find a state $r$ that is an $nop_{att}$-compatible successor
of $q$, has the same local states for voters as $r^{\prime}$, and in which
each counter $co_{k}$ keeps the sum of the bullets on $k$th line on the copied
ribbons from $r$. This will ensure that
$r\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{2}r^{\prime}$.

Finally, as regards condition (2), if
$q_{1}\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{1}q^{\prime}$ and
$q_{2}\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{1}q^{\prime}$, then the
attacker must have made the same choice in $q_{1}$ and $q_{2}$ (possibly
none), and her ”ballot stripes” $s_{att,j}$ and ”bookkeeping bits” $a_{att,j}$
must be the same in $q_{1}$ and $q_{2}$. But this entails the
indistinguishability of $q_{1}$ and $q_{2}$ for the attacker, i.e., then
$C_{att}(q_{1})=C_{att}(q_{2})$. The proof of (2) for
$\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{2}$ is similar.

To conclude, all iCGS $\mathcal{G}_{tot}$, $\mathcal{G}_{lex}$, and
$\mathcal{G}_{count}$ are bisimilar for the attacker. We will make use of this
fact in the next section on experimental results.

######  Remark 17.

Note that the two relations $\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{1}$
and $\Lleftarrow\\!\\!\\!\Rrightarrow_{\\{att\\}}^{2}$ are also bisimulations
on models $\mathcal{G}_{tot},\mathcal{G}_{lex}$ and $\mathcal{G}_{count}$ in
the sense of (the symmetric variant of) Def. 5.1 in [73]. Therefore, applying
[73, Lemma 5.2] both ways, any CTLK formula that is satisfied in any of the
models, is satisfied in all of them. This justifies our use of CTLK operators
in specification $\varphi^{c}_{i}$ above.

On the other hand, note that CTLK bisimulations in the sense of [73] do not
preserve ATL formulas under imperfect information. Figure 9 provides a
counterexample, with two 1-agent models that are timed epistemic bisimilar,
but do not satisfy the same formulas in ATL.

$\not\models\llangle alice\rrangle
Fp$$s_{1}$$s_{2}$$p$$s_{3}$$s_{4}$$\models\llangle alice\rrangle
Fp$$t_{1}$$t_{2}$$p$$t_{3}$$t_{4}$$*$$*$$a$$b$$a$$b$${\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}alice}$$*$$*$$a$$b$$b$$a$${\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}alice}$
Figure 9:  Two models that are (timed epistemic) bisimilar in the sense of
[73], but do not satisfy the same formula in ATL.

##  6 Experimental Results

In this section, we exhibit the improvements in running time when checking the
same properties over the three bisimilar models. The three models are checked
with growing number of voters and candidates. For our experiments, we have
used the latest version of MCMAS (1.3.0) [15]. Tests were made on a virtual
machine running Ubuntu 16.04.1 LTS on a Dell PowerEdge R720 server with two
Intel Xeon E5-2650 8 core processors at 2GHz, and 128 GB of RAM. In order to
investigate certain non-intuitive results reported in Tables 1, 2, and 3, we
re-ran the experiments on a different machine with a similar setup of 16-core
Xeon E5620 2.4GHz processor with 64GB RAM. The purported anomalies have shown
to be stable over both the tests. In all the following tables, NA means a 2
hours timeout has been reached without obtaining any result. The C programs
that were used to generate the ISPL files for the three ThreeBallot models,
together with the generated ISPL files, are publicly available as [74].

MCMAS provides two options, -atlk 2 or -uniform, for checking ATL formulas
with uniform strategies, with some differences in the semantics of ATL
formulas (-uniform is similar with _“irrevocable strategies”_ of [31]). We
observed that neither of these options were stable, and lead to a number of
experiments ending with inconsistent results or MCMAS terminating abnormally
(segfault on null-pointer assignment in one of the fixpoint computations
related with ATL satisfiability). We refer the interested reader to [75, 76].

Table 1 reports the running times for a selection of $\mathcal{G}_{tot}$ and
$\mathcal{G}_{lex}$ models. Note that several surprising data points are
present. Namely, in the case of $(2v,3c)$ the running time is smaller for
$\mathcal{G}_{tot}$ than for $\mathcal{G}_{lex}$ despite considerably larger
state space (but smaller BDD). Moreover in case of $(2v,4c)$ the computations
for $\mathcal{G}_{lex}$ timed out at the stage of computing the set of
reachable states while the verification of $\mathcal{G}_{tot}$ completed
successfully in an hour. Model checking the cases of $(3v,2c)$ and $(4v,2c)$
resulted in segmentation fault for both $\mathcal{G}_{tot}$ and
$\mathcal{G}_{lex}$ on both the machines. Model checking the cases of
$(3v,3c)$ and $(4v,3c)$ did not succeed in reasonable time for both models.

| (# voters, # candidates)
---|---
| (2v,2c) | (2v,3c) | (2v,4c)
$G_{tot}$ | 1.5 s | 12.8 s | 3714.0 s
$|S|\approx 5.9e+06$ | $|S|\approx 3.3e+08$ | $|S|\approx 8.8e+09$
$|BDD|\approx 1.4e+07$ | $|BDD|\approx 5.5e+07$ | $|BDD|\approx 4.0e+08$
$G_{lex}$ | 1.3 s | 29.0 s | NA
$|S|\approx 2.9e+05$ | $|S|\approx 1.1e+07$
$|BDD|\approx 1.5e+07$ | $|BDD|\approx 6.1e+07$
Table 1: MCMAS statistics for coercion freeness, $\mathcal{G}_{tot}$ and
$\mathcal{G}_{lex}$ with the -atlk 2 flag

To address the segfault issues, we also checked the coercion resistance
property with -atlk 0 option, which utilizes ATL with perfect information.
This is nevertheless consistent with our theoretical setting since all tests
for more than 3 candidates show that the formulas are false, and whenever a
positive ATL formula is false under the perfect information semantics, it is
also false under the imperfect information semantics, and hence preserved by
alternating bisimulations. Tables 2 and 3 show the details of the verification
of the only configurations for which MCMAS produces results in reasonable time
(timeout = 2 hours) for, respectively, $\mathcal{G}_{tot}$ and
$\mathcal{G}_{lex}$. Again, while the state-space of $\mathcal{G}_{lex}$ is
consistently (and predictably) smaller than the state-space of
$\mathcal{G}_{tot}$, the size of corresponding BDDs can increase. This is
notable in particular in the case of $(2v,3c)$ where model checking is twice
faster for $\mathcal{G}_{tot}$ than for $\mathcal{G}_{lex}$. The case of
$(2v,4c)$ that terminated successfully for $\mathcal{G}_{tot}$ and timed-out
for $\mathcal{G}_{lex}$ (the entry omitted from the table) is similar.

Our interpretation for the anomalies between state space, BDD size and running
time is that the ”ribbon” variables being more constrained in
$\mathcal{G}_{lex}$ than in $\mathcal{G}_{tot}$, the default variable ordering
produces larger BDDs for the more constrained model. On the other hand, the
anomaly being present for both the -atlk 0 and the -atlk 2 flags, it does not
seem to come from the difference in dealing with uniform strategies than with
strategies with perfect information. Note that the same anomalies are present
for the CTLK model-checking instances below.

| # candidates
---|---
| 2c | 3c | 4c
# voters | 2v | 1.3 s | 13.3 s | 3558.5 s
$|S|\approx 5.9e+06$ | $|S|\approx 3.3e+08$ | $|S|\approx 8.8e+09$
| $|BDD|\approx 1.2e+07$ | $|BDD|\approx 4.5e+07$ | $|BDD|\approx 2.8e+08$
3v | 25.1 s | NA | NA
| $|S|\approx 2.9e+10$
|  | $|BDD|\approx 5.9e+07$
| 4v | 1291.8 s | NA | NA
| $|S|\approx 1.7e+14$
|  | $|BDD|\approx 3.0e+08$
Table 2: MCMAS statistics for coercion freeness, $\mathcal{G}_{tot}$ and -atlk 0 flag | # candidates
---|---
| 2c | 3c
# voters | 2v | 1.1 s | 26.4 s
$|S|\approx 2.9e+05$ | $|S|\approx 1.1e+07$
| $|BDD|\approx 1.5e+07$ | $|BDD|\approx 5.4e+07$
3v | 10.4 s |
$|S|\approx 3.1e+08$ | NA
| $|BDD|\approx 5.7e+07$ |
| 4v | 297.9 s | NA
| $|S|\approx 3.9e+11$
|  | $|BDD|\approx 8.9e+07$
Table 3: MCMAS statistics for coercion freeness, $\mathcal{G}_{lex}$ and -atlk
0 flag

The models $\mathcal{G}_{count}$ can be verified much faster with the -atlk 2,
the number of reachable states and the BDD size decreasing substantially.
Statistics are given in Table 4.

| # candidates
---|---
| 2c | 3c | 4c | 5c | 6c | 7c
# voters | 2v | 0.1 s | 0.4 s | 1.5 s | 7.1 s | 94.2 s | NA
$|S|=6.3e+03$ | $|S|=1.7e+05$ | $|S|=4.6e+06$ | $|S|=1.2e+08$ | $|S|=2.9e+09$
| $|BDD|=1.0e+07$ | $|BDD|=1.2e+07$ | $|BDD|=1.7e+07$ | $|BDD|=3.9e+07$ | $|BDD|=9.4e+07$
3v | 0.5 s | 4.0 s | 110.0 s | 2917.8 s | NA |
$|S|=9.3e+04$ | $|S|=6.2e+06$ | $|S|=4.2e+08$ | $|S|=3.2e+10$ |
| $|BDD|=1.3e+07$ | $|BDD|=2.9e+07$ | $|BDD|=6.9e+07$ | $|BDD|=3.1e+08$ |
4v | 1.3 s | 32.7 s | 762.5 s | NA |  |
$|S|=7.8e+06$ | $|S|=3.6e+08$ | $|S|=1.6+12$ |  |
| $|BDD|=1.6e+07$ | $|BDD|=5.6e+07$ | $|BDD|=1.7e+08$ |  |
5v | 5.7 s | 341.2 s | NA |  |  |
$|S|=1.7e+08$ | $|S|=2.3e+11$ |  |  |
| $|BDD|=1.9e+07$ | $|BDD|=1.1e+08$ |  |  |
6v | 12.0 s | NA |  |  |  |
$|S|=3.3e+09$ |  |  |  |
| $|BDD|=4.2e+07$ |  |  |  |
7v | 38.8 s | NA |  |  |  |
$|S|=7.6e+10$ |  |  |  |
| $|BDD|=5.9e_{0}7$ |  |  |  |
| 8v | 82.0 s | NA |  |  |  |
| $|S|=8.7e+12$ |  |  |  |
|  | $|BDD|=5.9e+07$ |  |  |  |
| 9v | 139.5 s | NA |  |  |  |
| $|S|=2.6e+14$ |  |  |  |
|  | $|BDD|=6.1e+07$ |  |  |  |
Table 4: MCMAS statistics for coercion freeness, $\mathcal{G}_{count}$ and
-atlk 2 flag

We also ran the same tests for the anonymity property,
$\varphi_{i}^{c}=AG(\bigwedge_{1\leqslant j\leqslant nc}\neg
K_{att}p_{ch_{i}=j})$ The results are given in Tables 5, 6 and 7. Note the
same anomalies of smaller state space but larger BDD size and running time
between some $\mathcal{G}_{lex}$ models and the respective $\mathcal{G}_{tot}$
models.

| # candidates
---|---
| 2c | 3c | 4c
# voters | 2v | 1.1 s | 9.7 s | 3200.2 s
$|S|\approx 5.9e+06$ | $|S|\approx 3.3e+08$ | $|S|\approx 8.8+09$
| $|BDD|\approx 1.2e+07$ | $|BDD|\approx 4.5e+07$ | $|BDD|\approx 2.8e+08$
3v | 14.0 s | 6455.9 s | NA
| $|S|\approx 2.9e+10$ | $|S|\approx 2.4e+13$
|  | $|BDD|\approx 5.4e+07$ | $|BDD|\approx 2.4e+08$
| 4v | 440.0 s | NA |
| $|S|\approx 1.7e+14$ |
|  | $|BDD|\approx 1.1e+08$ |
Table 5: MCMAS statistics for anonymity checking on $\mathcal{G}_{tot}$ | # candidates
---|---
| 2c | 3c | 4c
# voters | 2v | 0.9 s | 18.9 s | NA
$|S|\approx 2.9e+05$ | $|S|\approx 1.1e+07$ |
| $|BDD|\approx 1.3e+07$ | $|BDD|\approx 4.9e+07$ |
3v | 8.3 s | 7100.6 s | NA
| $|S|\approx 3.1e+08$ | $|S|\approx 1.5e+11$
|  | $|BDD|\approx 3.9e+07$ | $|BDD|\approx 3.0e+08$
| 4v | 323.3 s | NA |
| $|S|\approx 4.0e+11$ |
|  | $|BDD|\approx 6.5e+07$ |
Table 6: MCMAS statistics for anonymity checking on $\mathcal{G}_{lex}$ | # candidates
---|---
| 2c | 3c | 4c | 5c | 6c | 7c
# voters | 2v | 0.1 s | 0.4 s | 1.6 s | 7.6 s | 103.6 s | NA
$|S|=6.3e+03$ | $|S|=1.6e+05$ | $|S|=4.6e+06$ | $|S|=1.2e+08$ | $|S|=2.9e+09$
| $|BDD|=1.0e+07$ | $|BDD|=1.2e+07$ | $|BDD|=1.9e+07$ | $|BDD|=5.1e+07$ | $|BDD|=9.3e+07$
3v | 0.5 s | 4.1 s | 114.2 s | 5617.9 | NA |
$|S|=9.3e+04$ | $|S|=6.2e+06$ | $|S|=4.2e+08$ | $|S|=3.2e+10$ |
| $|BDD|=1.2e+07$ | $|BDD|=2.9e+07$ | $|BDD|=7.8e+07$ | $|BDD|=4.2e+08$ |
4v | 1.3 s | 29.5 s | 898.8 s | NA |  |
$|S|=7.8e+06$ | $|S|=3.6e+07$ | $|S|=1.6+12$ |  |
| $|BDD|=1.6e+07$ | $|BDD|=5.4e+07$ | $|BDD|=2.0e+08$ |  |
5v | 5.7 s | 336.9 s | NA |  |  |
$|S|=1.7e+08$ | $|S|=2.3e+11$ |  |  |
| $|BDD|=1.9e+07$ | $|BDD|=1.1e+08$ |  |  |
6v | 12.1 s | NA |  |  |  |
$|S|=3.2e+09$ |  |  |  |
| $|BDD|=4.2e+07$ |  |  |  |
7v | 42.6 s | NA |  |  |  |
$|S|=7.6e+10$ |  |  |  |
| $|BDD|=5.3e+07$ |  |  |  |
| 8v | 73.2 s | NA |  |  |  |
| $|S|=8.7e+12$ |  |  |  |
|  | $|BDD|=5.9e+07$ |  |  |  |
| 9v | 140.0 s | NA |  |  |  |
| $|S|=2.6e+14$ |  |  |  |
|  | $|BDD|=6.0e+07$ |  |  |  |
Table 7: MCMAS statistics for anonymity checking on $\mathcal{G}_{count}$

##  7 Conclusions

In this paper we advance the state-of-the-art in model theory and verification
for the strategy logic ATL∗ under imperfect information and imperfect recall.
Specifically, we introduce a novel notion of (bi)simulation on imperfect
information concurrent game structures that preserves the interpretation of
formulas in ATL∗ both under the objective and subjective variants of the
semantics (Theorem 8). Then, we apply this theoretical result to the
verification of the ThreeBallot voting system, a relevant voting protocol
without cryptography. We show how the ThreeBallot protocol can be captured
within the framework of iCGS, and then provide successive abstractions that
are provably bisimilar to the original iCGS for the ThreeBallot system. In
particular, we have been able to model check the “smaller” bisimilar
reductions of the ThreeBallot model, and then transfer the result to the
original model in virtue of Theorem 8. As reported in the experimental
results, the gains in terms of both time and memory resources are significant.

Future Work. We envisage several extensions of the present contribution.
First, it is of interest to develop bisimulations for strategic properties of
agents with perfect recall and bounded recall, as in many application domains
agents do have some memory of past states and actions. Also for the
verification of voting protocols, it is key to extend ATL∗ with epistemic
modalities to express naturally properties of anonymity and confidentiality.
We remarked that individual knowledge is expressible in the subjective
semantics. However, no such result holds for the objective interpretation, nor
common knowledge happens to be definable. Finally, we aim at automating and
implementing the procedures described in this paper in a model checking tool
for the formal verification of (electronic) voting protocols.

Acknowledgements. F. Belardinelli acknowledges the support of the ANR JCJC
Project SVeDaS (ANR-16-CE40-0021). W. Jamroga acknowledges the support of the
National Centre for Research and Development (NCBR), Poland, under the project
VoteVerif (POLLUX-IV/1/2016).

## References

  * [1] N. Bulling, J. Dix, W. Jamroga, Model checking logics of strategic ability: Complexity, in: Specification and Verification of Multi-agent Systems, Springer, 2010, pp. 125–159.
  * [2] N. Bulling, W. Jamroga, Comparing variants of strategic ability: how uncertainty and memory influence general properties of games, Autonomous Agents and Multi-Agent Systems 28 (3) (2014) 474–518.
  * [3] V. Goranko, W. Jamroga, Comparing semantics for logics of multi-agent systems, Synthese 139 (2) (2004) 241–280.
  * [4] R. Alur, T. A. Henzinger, O. Kupferman, Alternating-time temporal logic, in: Proceedings of the 38th IEEE Symposium on Foundations of Computer Science (FOCS97), IEEE Computer Society, 1997, pp. 100–109.
  * [5] R. Alur, T. A. Henzinger, O. Kupferman, Alternating-time temporal logic, Journal of the ACM 49 (5) (2002) 672–713.
  * [6] F. Laroussinie, N. Markey, Augmenting atl with strategy contexts, Information and Computation 245 (2015) 98–123.
  * [7] K. Chatterjee, T. Henzinger, N. Piterman, Strategy logic, in: Proceedings of the 18th International Conference on Concurrency Theory (CONCUR07), Vol. 4703, 2007, pp. 59–73.
  * [8] F. Mogavero, A. Murano, G. Perelli, M. Y. Vardi, Reasoning about strategies: On the model-checking problem, ACM Transactions in Computational Logic 15 (4) (2014) 34:1–34:47.  doi:10.1145/2631917.
URL http://doi.acm.org/10.1145/2631917

  * [9] M. Pauly, A modal logic for coalitional power in games, Journal of Logic and Computation 12 (1) (2002) 149–166.  doi:10.1093/logcom/12.1.149.
URL http://dx.doi.org/10.1093/logcom/12.1.149

  * [10] T. Ball, O. Kupferman, An abstraction-refinement framework for multi-agent systems, in: Proceedings of Logic in Computer Science (LICS), 2006, pp. 379–388.  doi:10.1109/LICS.2006.10.
  * [11] W. van der Hoek, W. Jamroga, M. Wooldridge, A logic for strategic reasoning, in: Proceedings of the 4th international joint conference on Autonomous agents and multiagent systems (AAMAS05), ACM Press, New York, NY, USA, 2005, pp. 157–164.
  * [12] F. Mogavero, A. Murano, M. Vardi, Reasoning About Strategies, in: Proceedings of the 30th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS10), Vol. 8, Schloss Dagstuhl, 2010, pp. 133–144.
  * [13] P. Gammie, R. van der Meyden, MCK: Model checking the logic of knowledge, in: Proceedings of 16th International Conference on Computer Aided Verification (CAV04), Vol. 3114 of Lecture Notes in Computer Science, Springer, 2004, pp. 479–483.
  * [14] M. Kacprzak, W. Nabialek, A. Niewiadomski, W. Penczek, A. Pólrola, M. Szreter, B. Woźna, A. Zbrzezny, Verics 2007 - a model checker for knowledge and real-time, Fundamenta Informaticae 85 (1) (2008) 313–328.
  * [15] A. Lomuscio, H. Qu, F. Raimondi, MCMAS: A model checker for the verification of multi-agent systems, Software Tools for Technology TransferHttp://dx.doi.org/10.1007/s10009-015-0378-x.  doi:10.1007/s10009-015-0378-x.
URL http://dx.doi.org/10.1007/s10009-015-0378-x

  * [16] W. Jamroga, J. Dix, Model checking abilities under incomplete information is indeed $\delta_{p}^{2}$-complete, in: Proceedings of the 4th European Workshop on Multi-Agent Systems EUMAS’06, Citeseer, 2006, pp. 14–15.
  * [17] C. Dima, F. L. Tiplea, Model-checking ATL under imperfect information and perfect recall semantics is undecidable, CoRR abs/1102.4225.
URL http://arxiv.org/abs/1102.4225

  * [18] F. Belardinelli, A. Lomuscio, A. Murano, S. Rubin, Verification of multi-agent systems with imperfect information and public actions, in: AAMAS’17, 2017, pp. 1268–1276.
  * [19] F. Belardinelli, A. Lomuscio, A. Murano, S. Rubin, Verification of broadcasting multi-agent systems against an epistemic strategy logic, in: IJCAI’17, 2017, pp. 91–97.  doi:10.24963/ijcai.2017/14.
URL https://doi.org/10.24963/ijcai.2017/14

  * [20] P. Cermák, A. Lomuscio, F. Mogavero, A. Murano, Practical verification of multi-agent systems against slk specifications, Information and Computation 261 (Part) (2018) 588–614.  doi:10.1016/j.ic.2017.09.011.
URL https://doi.org/10.1016/j.ic.2017.09.011

  * [21] W. Jamroga, M. Knapik, D. Kurpiewski, Fixpoint approximation of strategic abilities under imperfect information, in: K. Larson, M. Winikoff, S. Das, E. H. Durfee (Eds.), Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, São Paulo, Brazil, May 8-12, 2017, ACM, 2017, pp. 1241–1249.
URL http://dl.acm.org/citation.cfm?id=3091298

  * [22] P. Cousot, R. Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, 1977, pp. 238–252.  doi:10.1145/512950.512973.
  * [23] E. M. Clarke, O. Grumberg, D. Long, Model checking and abstractions, ACM Transactions on Programming Languages and Systems 16 (5) (1994) 1512–1542.
  * [24] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement, in: Proceedings of the 12th International Conference on Computer Aided Verification (CAV00), Vol. 1855 of Lecture Notes in Computer Science, Springer, 2000, pp. 154–169.
  * [25] L. de Alfaro, P. Godefroid, R. Jagadeesan, Three-valued abstractions of games: Uncertainty, but with precision, in: Proceedings of Logic in Computer Science (LICS), IEEE Computer Society, 2004, pp. 170–179.
  * [26] A. Lomuscio, J. Michaliszyn, Verification of multi-agent systems via predicate abstraction against ATLK specifications, in: Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), 2016, pp. 662–670.
  * [27] F. Belardinelli, A. Lomuscio, Agent-based abstractions for verifying alternating-time temporal logic with imperfect information, in: Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), ACM, 2017, pp. 1259–1267.
  * [28] P. Blackburn, M. de Rijke, Y. Venema, Modal Logic, Vol. 53 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2001\.
  * [29] R. Alur, T. A. Henzinger, O. Kupferman, M. Y. Vardi, Alternating refinement relations, in: In Proceedings of the Ninth International Conference on Concurrency Theory (CONCUR’98), volume 1466 of LNCS, Springer-Verlag, 1998, pp. 163–178.
  * [30] U. Goltz, R. Kuiper, W. Penczek, Propositional temporal logics and equivalences, in: Proceedings of CONCUR ’92, 1992, pp. 222–236.  doi:10.1007/BFb0084794.
  * [31] T. Ågotnes, V. Goranko, W. Jamroga, Alternating-time temporal logics with irrevocable strategies, in: Proceedings of TARK XI, 2007, pp. 15–24.
  * [32] W. Jamroga, Logical Methods for Specification and Verification of Multi-Agent Systems, ICS PAS Publishing House, 2015.
  * [33] P. A. Ryan, The computer ate my vote, in: P. Boca, J. P. Bowen, J. Siddiqi (Eds.), Formal Methods: State of the Art and New Directions, Springer Verlag, 2009, Ch. 5, pp. 148–184.
  * [34] P. Y. A. Ryan, S. A. Schneider, V. Teague, End-to-end verifiability in voting systems, from theory to practice, IEEE Security & Privacy 13 (3) (2015) 59–62.  doi:10.1109/MSP.2015.54.
  * [35] B. Beckert, R. Goré, C. Schürmann, T. Bormer, J. Wang, Verifying voting schemes, J. Inf. Secur. Appl. 19 (2) (2014) 115–129.  doi:10.1016/j.jisa.2014.04.005.
URL http://dx.doi.org/10.1016/j.jisa.2014.04.005

  * [36] V. Cortier, Formal verification of e-voting: Solutions and challenges, ACM SIGLOG News 2 (1) (2015) 25–34.  doi:10.1145/2728816.2728823.
URL http://doi.acm.org/10.1145/2728816.2728823

  * [37] S. Delaune, S. Kremer, M. Ryan, Verifying Privacy-Type Properties of Electronic Voting Protocols, Journal of Computer Security 17 (4) (2009) 435–487.
  * [38] C. A. R. Hoare, Communicating Sequential Processes, Commun. ACM 21 (8) (1978) 666–677.
  * [39] S. Schneider, A. Sidiropoulos, CSP and Anonymity, in: Proceedings of the 1996 European Symposium on Research in Computer Security (ESORICS’96), Vol. 1146 of Lecture Notes in Computer Science, Springer-Verlag, 1996, pp. 198–218.
  * [40] I. Cervesato, N. A. Durgin, P. Lincoln, J. C. Mitchell, A. Scedrov, A Meta-Notation for Protocol Analysis, in: Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW’99), IEEE Computer Society, 1999, pp. 55–69.
  * [41] G. Denker, J. K. Millen, Modeling Group Communication Protocols Using Multiset Term Rewriting, Electr. Notes Theor. Comput. Sci. 71 (2002) 20–39.
  * [42] I. Boureanu, A. V. Jones, A. Lomuscio, Automatic Verification of Epistemic Specifications Under Convergent Equational Theories, in: Proceedings of the 11th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS’12), IFAAMAS, 2012, pp. 1141–1148.
  * [43] M. Tabatabaei, W. Jamroga, P. Y. A. Ryan, 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, ACM, 2016, pp. 1:1–1:8.  doi:10.1145/2970030.2970039.
  * [44] R. L. Rivest, The ThreeBallot Voting System, http://theory.lcs.mit.edu/~rivest/Rivest-TheThreeBallotVotingSystem.pdf (October 2006).
  * [45] R. Rivest, W. Smith, Three voting protocols: ThreeBallot, VAV, and Twin, in: Proceedings of USENIX/ACCURATE Electronic Voting Technology Workshop (EVT), 2007.
  * [46] M. Moran, J. Heather, S. Schneider, Verifying anonymity in voting systems using csp, Formal Aspects of Computing 26 (1) (2014) 63–98.  doi:10.1007/s00165-012-0268-x.
URL http://dx.doi.org/10.1007/s00165-012-0268-x

  * [47] M. Moran, J. Heather, S. Schneider, Automated anonymity verification of the ThreeBallot and VAV voting systems, Software & Systems Modeling 15 (4) (2016) 1049–1062.  doi:10.1007/s10270-014-0445-x.
URL http://dx.doi.org/10.1007/s10270-014-0445-x

  * [48] F. Belardinelli, R. Condurache, C. Dima, W. Jamroga, A. V. Jones, Bisimulations for verifying strategic abilities with an application to threeballot, in: Proc. of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS17), 2017, pp. 1286–1295.
  * [49] F. Belardinelli, C. Dima, A. Murano, Bisimulations for logics of strategies: A study in expressiveness and verification, in: M. Thielscher, F. Toni, F. Wolter (Eds.), Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018, Tempe, Arizona, 30 October - 2 November 2018., AAAI Press, 2018, pp. 425–434.
URL https://aaai.org/ocs/index.php/KR/KR18/paper/view/17992

  * [50] M. Dastani, W. Jamroga, Reasoning about strategies of multi-agent programs, in: Proceedings of AAMAS2010, 2010, pp. 625–632.
  * [51] M. Melissen, Game theory and logic for non-repudiation protocols and attack analysis, Ph.D. thesis, University of Luxembourg (2013).
  * [52] Ştefan Ciobâcă, Verification and composition of security protocols with applications to electronic voting. (vérification et composition des protocoles de securité avec des applications aux protocoles de vote electronique), Ph.D. thesis, École normale supérieure de Cachan, France (2011).
  * [53] B. Meng, W. Huang, D. Wang, Automatic verification of remote internet voting protocol in symbolic model, JNW 6 (9) (2011) 1262–1271.
  * [54] S. Delaune, S. Kremer, M. Ryan, Verifying privacy-type properties of electronic voting protocols, Journal of Computer Security 17 (4) (2009) 435–487.
  * [55] H. DeYoung, C. Schürmann, Linear logical voting protocols, in: VoteID, E-Voting and Identity - Third International Conference, Tallinn, Estonia, Vol. 7187 of Lecture Notes in Computer Science, Springer, 2011, pp. 53–70.
  * [56] B. Beckert, R. Goré, C. Schürmann, Analysing vote counting algorithms via logic - and its application to the CADE election scheme, in: Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, Vol. 7898 of Lecture Notes in Computer Science, Springer, 2013, pp. 135–144.