none 2023 2023 University of Luxembourg Luxembourg Luxembourg University of
Luxembourg Luxembourg Luxembourg

# Practical Abstraction for Model Checking of Multi-Agent Systems

Wojciech Jamroga<EMAIL_ADDRESS>and  Yan Kim<EMAIL_ADDRESS>
###### Abstract.

Model checking of multi-agent systems (MAS) is known to be hard, both
theoretically and in practice. A smart abstraction of the state space may
significantly reduce the model, and facilitate the verification. In this
paper, we propose and study an intuitive agent-based abstraction scheme, based
on the removal of variables in the representation of a MAS. This allows to
achieve a desired reduction of a state space without generating the global
model of the system. Moreover, the process is easy to understand and control
even for domain experts with little knowledge of computer science. We formally
prove the correctness of the approach, and evaluate the gains experimentally
on a family of a postal voting procedure models.

###### Key words and phrases:

model checking, abstraction, multi-agent systems

##  1\. Introduction

_Multi-agent systems (MAS)_ describe interactions of multiple entities called
agents, often assumed to be autonomous, intelligent, and/or rational. The
theoretical foundations of MAS are mostly based on modal logic and game theory
Wooldridge (2002); Shoham and Leyton-Brown (2009). In particular, the temporal
logics $\mathbf{CTL}$, $\mathbf{LTL}$, and $\mathbf{CTL^{\star}}$ provide
intuitive formalizations of many relevant properties, including reachability,
liveness, safety, and fairness Emerson (1990). Algorithms and tools for
verification have been in constant development for 40 years, with temporal
model checking being the most popular approach Baier and Katoen (2008); Clarke
et al. (2018).

However, formal verification of MAS is known to be hard, both theoretically
and in practice. The state-space explosion is a major source of the
computational hardness, as faithful models of real-world systems are immensely
huge and infeasible even to generate, let alone verify. In consequence, model
checking of MAS with respect to their _modular representations_ ranges from
$\mathbf{{PSPACE}}$-complete to undecidable Schnoebelen (2003); Bulling et al.
(2010). No less importantly, it is often unclear how to create the input
model, especially if the system to be modeled involves human behavior Jamroga
et al. (2020a). Similarly, formalizing the relevant properties in the right
way is by no means trivial Jamroga et al. (2021). Both parts of the
specification are error-prone and difficult to debug and validate: most model-
checkers for MAS do not even have a graphical user interface.111 Notable
exceptions include Uppaal Behrmann et al. (2004) and STV Kurpiewski et al.
(2021).  Thus, in realistic cases, one does not even know if what they are
verifying and what they _think_ they verify are indeed the same thing.

Much work has been done on containing the state-space explosion by smart
representation and/or reduction of input models. Symbolic model checking based
on SAT- or BDD-based representations of the state/transition space McMillan
(1993, 2002); Penczek and Lomuscio (2003); Kacprzak et al. (2004); Lomuscio
and Penczek (2007); Huang and van der Meyden (2014) fall into the former
group. Model reduction methods include partial-order reduction Peled (1993);
Gerth et al. (1999); Jamroga et al. (2020b), equivalence-based reductions de
Bakker et al. (1984); Alur et al. (1998); Belardinelli et al. (2021), and
state/action-abstraction Cousot and Cousot (1977); Clarke et al. (1994);
Godefroid and Jagadeesan (2002). More specific variants of abstraction for
multi-agent systems have been proposed in de Alfaro et al. (2004); Enea and
Dima (2008); Cohen et al. (2009); Lomuscio et al. (2010b), and more recently
in Kouvaros and Lomuscio (2017); Belardinelli and Lomuscio (2017);
Belardinelli et al. (2019). A smart abstraction of the state space may reduce
the model to manageable size by clustering “similar” concrete states into
_abstract states_ , which should facilitate verification. Unfortunately, such
clustering may remove essential information from the model, thus making the
verification of the abstract model inconclusive for the original model.
Lossless abstractions can be obtained by means of abstraction-refinement
Clarke et al. (2000, 2003); Shoham and Grumberg (2004); Ball and Kupferman
(2006); Dams and Grumberg (2018) but, typically, they are difficult to compute
or provide insufficient reduction of the model – quite often both.

In consequence, one has to live with abstractions that only approximate the
concrete model. Moreover, crafting a good abstraction is an art that relies on
the domain expertise of the modeler. Since domain experts are seldom computer
scientists or specialists in formal methods, the theoretical formulation of
abstraction as an arbitrary mapping from the concrete to the abstract state
space has little appeal. Moreover, model checking tools typically do not
support abstraction, so doing one would require to manipulate the input
specification code, which is a difficult task in itself. What we need is a
simple and intuitive methodology for selecting information to be removed from
a MAS model, and for its automated removal that preserves certain guarantees.
Last but not least, practical abstraction should be applied on modular
representations of MAS, unlike the theoretical concept that is usually defined
with respect to explicit models of global states.

In this paper, we suggest that the conceptually simplest kind of abstraction
consists in removing a domain variable from the input model. This can be
generalized to the merging of several variables into a single one, and
possibly clustering their valuations. It is also natural to restrict the scope
of abstraction to a part of the graph. As the main technical contribution, we
propose a correct-by-design method to generate such abstractions. We prove
that the abstractions preserve the valuations of temporal formulae in
Universal $\mathbf{CTL^{\star}}$ ($\mathbf{ACTL^{\star}}$). More precisely,
our may-abstractions preserve the falsity of $\mathbf{ACTL^{\star}}$
properties, so if $\varphi\in\mathbf{ACTL^{\star}}$ holds in the abstract
model, it must also hold in the original one. Conversely, our must-
abstractions preserve the truth of $\mathbf{ACTL^{\star}}$ formulae, so if
$\varphi\in\mathbf{ACTL^{\star}}$ is false in the abstract model, it must also
be false in the original one. We also evaluate the efficiency of the method by
verifying a scalable model of postal voting in Uppaal. The experiments show
that the method is user-friendly, compatible with a state of the art
verification tool, and capable of providing significant computational gains.

##  2\. Preliminaries

We start by introducing the models and formulae which serve as an input to
model checking.

###  2.1. MAS Graphs

To represent the behavior of a multi-agent system, we use modular
representations inspired by reactive modules Alur and Henzinger (1999),
interleaved interpreted systems Lomuscio et al. (2010a); Jamroga et al.
(2020b), and in particular by the way distributed systems are modeled in
Uppaal Behrmann et al. (2004).

Let Var be a finite set of typed variables over finite domain222We will focus
exclusively on variables over finite domains, the only variant of variables
supported by Uppaal, and, naturally, the one interpreted by the programs.. By
$\textit{Eval}(\\!\textit{Var})$ we denote a set of evaluation functions which
map variables $v\in\textit{Var}$ to values in their domains $\textit{dom}(v)$.

Cond is a set of logical expressions (also called _guards_) over Var and
literal values, possibly involving arithmetic operators (i.e., “$+$”, “$-$”,
“$*$”, “$/$” and “$\%$”).

Let Chan be a finite set of asymmetric synchronization channels. We define the
set of synchronizations as $\textit{Sync}=\\{{c!,c?\mid
c\in\textit{Chan}}\\}\cup\\{{-}\\}$, with $c!$ and $c?$ for sending and
receiving on a channel $c$ accordingly, and “$-$” standing for no
synchronization. For the paper, we will focus only on 1-to-1 type of
synchronization; adding the 1-to-many (broadcast) and many-to-many is
straightforward (by minor tweaks of subsection 2.2), is of a less academic
value, and therefore omitted.

######  Definition .

An _agent graph_ is a tuple
$G=(\textit{Var},\textit{Loc},l_{0},g_{0},\textit{Act},$
$\textit{Effect},\hookrightarrow)$, consisting of:

  * •

Var: a finite set of typed _variables_ over finite domains;

  * •

Loc: a non-empty finite set of _locations_ (nodes in the graph);

  * •

$l_{0}\in\textit{Loc}$: the initial location;

  * •

$g_{0}\in\textit{Cond}$: the initial condition;

  * •

Act: a set of _actions_ , with $\tau\in\textit{Act}$ standing for “do
nothing”;

  * •

$\textit{Effect}:\textit{Act}\times\textit{Eval}(\\!\textit{Var})\mapsto\textit{Eval}(\\!\textit{Var})$:
the _effect_ of an action333Clearly, on an argument $\tau$ it will behave just
as an identity function over $\textit{Eval}(\\!\textit{Var})$.;

  * •

$\hookrightarrow\subseteq\textit{Loc}\times\textit{Label}\times\textit{Loc}$:
the set of labelled edges defining the local _transition relation_.

The set of labels is defined as
$\textit{Label}\subseteq\textit{Cond}\times\textit{Sync}\times\textit{Act}$.
An edge $(l,T,l^{\prime})\in\,\hookrightarrow$, where $T\in\textit{Label}$,
will often be denoted by
$l\lhook\joinrel\xrightarrow{g:ch\,\alpha}l^{\prime}$, where
$g=\textit{cond}(T)$, $ch=\textit{sync}(T)$ and
$\alpha=\textit{act}(T)$.444For the sake of readability, when $ch=-$, the
channel sub-label will be omitted.

A condition $g\in\textit{Cond}$ can be associated with a set of evaluations
$\textit{Sat}(g)=\\{\eta\in\textit{Eval}(\\!\textit{Var})\ |\ \eta\models
g\\}$ satisfying it. An edge labelled with $T\in\textit{Label}$ is said to be
_locally enabled_ for evaluation $\eta\in\textit{Eval}(\\!\textit{Var})$ iff
$\eta\in\textit{Sat}(\textit{cond}(T))$. Furthermore, every action
$\alpha\in\textit{Act}\setminus\\{{\tau}\\}$ can be associated with a non-
empty sequence of atomic assignment statements (also called _updates_) of the
form $\alpha^{(1)}\alpha^{(2)}\ldots\alpha^{(m)}$.

A function $\mathcal{V}:\\!\textit{Cond}\cup\\!\textit{Act}\mapsto
2^{\textit{Var}}$ maps an expression or an assignment statement to the set of
occurring variables.

Without loss of generality, we assume that for the set
$\textit{Var}=\\{{v_{1},\ldots,v_{k}}\\}$ its elements are enumerated and/or
ordered in some arbitrary yet fixed way. Then the evaluation of any
$V\subseteq\textit{Var}$ can be represented as a vector
$\eta(V)=[\eta(v_{i_{1}}),\ldots,\eta(v_{i_{l}})]$, where
$\forall_{j=1..l}.i_{j}\in\\{{1,\ldots,k}\\}\wedge\forall_{j=1..l}.i_{j}\leq
i_{j+1}$.

Let $V\subseteq\\!\textit{Var}$ and
$r\in\textit{Cond}\cup\textit{Act}\cup\textit{Eval}(\\!\textit{Var})$, by
$r[V=C]$ we denote the substitution of all free occurrences of variables $V$
in $r$ by $C\in\textit{dom}(V)$.

######  Definition .

A _MAS graph_ is a multiset of agent graphs additionally parameterized by a
set of shared (global) variables. We assume w.l.o.g. that all local variables
have unique names (e.g., achieved by prefixing those with a name of its agent
graph), then a set of shared variables can be derived by taking an
intersection over the variable sets of component agents.

Figure 1. MAS graph for ASV: (a) Voter, (b) Coercer

######  Example  (ASV)

As the running example, we use a variation of the Asynchronous Simple Voting
scenario of Jamroga et al. (2020b). Its MAS graph
${\mathit{ASV}}=\\{\\!|{\textit{Var}_{sh},G_{\textit{Voter}},G_{\textit{Coercer}}}|\\!\\}$
is shown in Figure 1. The system is parameterized by the number of candidates
$NC$ and consists of a voter graph $G_{\textit{Voter}}$, a coercer graph
$G_{\textit{Coercer}}$, a set of shared variables $\textit{Var}_{sh}=\\{sh\\}$
and an implicit $g_{0}=\bigwedge_{v\in\textit{Var}}(v==0)$.

The voter starts by non-deterministically selecting one of the candidates
(i:int$[$1,NC$]$), and casting a vote for the candidate (idle$\to$voted).
Then, she decides to either give the proof of how she voted to the coercer
(voted$\to$obeyed), or to refuse it (voted$\to$disobeyed). Both options
require executing a synchronous transition with the coercer. In turn, the
coercer either gets the proof and learns for whom the vote was cast, or
becomes aware of the voter’s refusal.

###  2.2. Models of MAS Graphs

|
---
|
---
Figure 2. Models of MAS: (a) combined MAS graph of ASV; (b) Unwrapping for ASV
with $\mathit{NC}=3$ candidates

We define the execution of a MAS graph by its _unwrapping_.

######  Definition .

Let $\textit{MG}=\\{\\!|{\textit{Var}_{sh},G_{1},\ldots,G_{n}}|\\!\\}$ be a
MAS graph having a set of shared variables $\textit{Var}_{sh}$. The _combined
MAS graph_ of MG is the agent graph
$G_{\textit{MG}}=(\textit{Var},\textit{Loc},l_{0},g_{0},\textit{Act},\textit{Effect},\hookrightarrow)$,
where $\textit{Var}=\bigcup_{i=1}^{n}\textit{Var}_{i}$,
$\textit{Loc}=\textit{Loc}_{1}\times\ldots\times\textit{Loc}_{n}$,
$l_{0}=(l_{0,0},\ldots,l_{n,0})$, $g_{0}=g_{0,0}\wedge\ldots\wedge g_{n,0}$,
$\textit{Act}=\bigcup_{i=1}^{n}\textit{Act}_{i}$.

Relation $\hookrightarrow$ is obtained inductively by the following rules
(where $l_{i},l^{\prime}_{i}\in\textit{Loc}_{i}$,
$l_{j},l_{j}^{\prime}\in\textit{Loc}_{j}$,
$c\in\textit{Chan}_{i}\cap\textit{Chan}_{j}$ for two agent graphs $G_{i}$ and
$G_{j}$ of distinct indices $1\leq i,j\leq n$):

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 1.68001pt\hbox{$\displaystyle\penalty 1l_{i}\lhook\joinrel\xrightarrow{g_{i}:c!\alpha_{i}}_{i}l_{i}^{\prime}\wedge l_{j}\lhook\joinrel\xrightarrow{g_{j}:c?\alpha_{j}}_{j}l_{j}^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=97.59726pt\hbox{}}}\hbox{\kern 0.0pt\hbox{$\displaystyle(l_{i},l_{j})\lhook\joinrel\xrightarrow{g_{i}\wedge g_{j}:(\alpha_{j}\circ\alpha_{i})}(l_{i}^{\prime},l_{j}^{\prime})$}}}}$ | ${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 15.35832pt\hbox{$\displaystyle\penalty 1l_{i}\lhook\joinrel\xrightarrow{g_{i}:\alpha_{i}}_{i}l_{i}^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=64.9963pt\hbox{}}}\hbox{\kern 0.0pt\hbox{$\displaystyle(l_{i},l_{j})\lhook\joinrel\xrightarrow{g_{i}:\alpha_{i}}(l_{i}^{\prime},l_{j})$}}}}$
---|---
${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 1.68001pt\hbox{$\displaystyle\penalty 1l_{i}\lhook\joinrel\xrightarrow{g_{i}:c?\alpha_{i}}_{i}l_{i}^{\prime}\wedge l_{j}\lhook\joinrel\xrightarrow{g_{j}:c!\alpha_{j}}_{j}l_{j}^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=97.59726pt\hbox{}}}\hbox{\kern 0.0pt\hbox{$\displaystyle(l_{i},l_{j})\lhook\joinrel\xrightarrow{g_{i}\wedge g_{j}:(\alpha_{i}\circ\alpha_{j})}(l_{i}^{\prime},l_{j}^{\prime})$}}}}$ | ${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 14.41684pt\hbox{$\displaystyle\penalty 1l_{j}\lhook\joinrel\xrightarrow{g_{j}:\alpha_{j}}_{j}l_{j}^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=66.25162pt\hbox{}}}\hbox{\kern 0.0pt\hbox{$\displaystyle(l_{i},l_{j})\lhook\joinrel\xrightarrow{g_{j}:\alpha_{j}}(l_{i},l_{j}^{\prime})$}}}}$

Lastly, the effect function is defined by:

$\small\textit{Effect}(\alpha,\eta)=\begin{cases}\textit{Effect}_{i}(\alpha,\eta)&\text{if
}\alpha\in\textit{Act}_{i}\\\
\textit{Effect}(\alpha_{i},\textit{Effect}(\alpha_{j},\eta))&\text{if
}\alpha=\alpha_{i}\circ\alpha_{j}\end{cases}$

Note that by construction of combined MAS graph its edges can be labelled only
by $T\in\textit{Label}$ where $\textit{sync}(T)=-$.

###### Example

The combined MAS graph $G_{{\mathit{ASV}}}$ for asynchronous simple voting of
subsection 2.1 is depicted in Figure 2a.

######  Definition .

A _model_ is a tuple $M=(\textit{St},I,\longrightarrow,AP,L)$, where St is a
set of states, $I\subseteq\textit{St}$ is a non-empty set of initial states,
$\longrightarrow\subseteq\textit{St}\times\textit{St}$ is a transition
relation, $AP$ is a set of atomic propositions, $L:\textit{St}\to 2^{AP}$ is a
labelling function. We assume $\longrightarrow$ to be serial, i.e., there is
at least one outgoing transition at every state.

Nodes and edges in an agent graph correspond to _sets_ of states and
transitions, defined by its unwrapping.

######  Definition .

The _unwrapping_ of an agent graph $G$ is a model
$\mathcal{M}(G)=(\textit{St},I,\longrightarrow,AP,L)$, where:

  * •

$\textit{St}=\textit{Loc}\times\textit{Eval}(\\!\textit{Var})$,

  * •

$I=\\{\langle{l_{0},\eta}\rangle\in\textit{St}\mid\eta\in\textit{Sat}(g_{0})\\}$,

  * •

$\longrightarrow\ =\longrightarrow_{0}\
\cup\\{(s,s)\in\textit{St}\times\textit{St}\mid\lnot\exists
s^{\prime}\in\textit{St}\ .\ s\longrightarrow_{0}s^{\prime}\\}$, where
$\longrightarrow_{0}\
=\\{(\langle{l,\eta}\rangle,\langle{l^{\prime},\eta^{\prime}}\rangle)\in\textit{St}\times\textit{St}\mid\exists\
l\lhook\joinrel\xrightarrow{g:\alpha}l^{\prime}\,.\,\eta\in\textit{Sat}(g)\wedge\eta^{\prime}=\textit{Effect}(\alpha,\eta)\\}$,555Note
that $\longrightarrow$ adds loops wherever necessary to make the relation
serial.

  * •

$AP=\textit{Loc}\cup\\!\textit{Cond}$,

  * •

$L(\langle{l,\eta}\rangle)=\\{l\\}\cup\\{g\in\textit{Cond}\mid\eta\in\textit{Sat}(g)\\}$.

The unwrapping $\mathcal{M}(\textit{MG})$ of a MAS graph MG is given by the
unwrapping of its combined graph.

By a slight abuse of notation, we lift some operators to sets of states. For
example, $L(S)=\bigcup_{s\in S}L(s)$ for $S\subseteq\textit{St}$. Moreover, we
will use $AP(V)$ to denote the subset of propositions that do not use
variables from outside $V$.

###### Example

The unwrapping $\mathcal{M}({{\mathit{ASV}}})$ of the MAS graph for
asynchronous simple voting (subsection 2.1) with 3 candidates is shown in
Figure 2b.

######  Definition .

Let $M$ be a model. A _run_ in $M$ is a sequence of states $s_{0}s_{1}\dots$,
such that $s_{i}\in\textit{St}$ and $s_{i}\longrightarrow s_{i+1}$ for every
$i$. A _path_ is an infinite run. For a finite run $\pi=s_{0}s_{1}\ldots
s_{n}$, let $\textit{length}(\pi)=n$ denote its length. By $\pi[k]$ and
$\pi[i,j]$ we will denote a $k$-th state and a run fragment from $i$ to $j$ of
$\pi$ accordingly. The sets of all runs in $M$, all paths in $M$, and all
paths starting from state $s$ are denoted by $\textit{Runs}(M)$,
$\textit{Paths}(M)$, and $\textit{Paths}(s)$. Similarly, $\textit{Runs}^{t}$
will denote the set of runs of fixed length
$t\in\mathbb{N}^{+}\cup\\{\infty\\}$.

A state $s\in\textit{St}$ is said to be _reachable_ in model $M$ if there
exists a run $\pi=s_{0}\ldots s_{n}$, s.t. $s_{0}\in I$ and $s_{n}=s$.

###  2.3. Branching-Time Logic $\mathbf{ACTL^{\star}}$

To specify requirements, we use the _universal fragment_ of the branching-time
logic $\mathbf{CTL^{\star}}$ Emerson (1990) (denoted
$\mathbf{ACTL^{\star}}$)666Not to be confused with “Action $\mathbf{CTL}$” of
Nicola and Vaandrager (1990). with $\mathsf{A}$ (“for every path”) as the only
path quantifier. The syntax for $\mathbf{ACTL^{\star}}$ over a set of atomic
propositions $AP$ is formally given by:

$\displaystyle\psi$ $\displaystyle::=$ $\displaystyle\top\mid\bot\mid
a\mid\neg a\mid\psi\wedge\psi\mid\psi\vee\psi\mid\mathsf{A}\varphi$
$\displaystyle\varphi$ $\displaystyle::=$
$\displaystyle\psi\mid\varphi\wedge\varphi\mid\varphi\vee\varphi\mid\mathrm{X}\varphi\mid\varphi\,\mathrm{U}\,\varphi$

where $a\in AP$, and $\mathrm{X},\\!\,\mathrm{U}\,$ stand for “next” and
“until,” respectively. Formulae $\psi$ are called state formulae, and
$\varphi$ are called path formulae. The semantics of $\mathbf{ACTL^{\star}}$
is given with respect to states $s$ and paths $\pi$ of a model $M$.

$\displaystyle M,s\models a$ $\displaystyle\quad\text{iff }a\in L(s)$
$\displaystyle M,s\models\mathsf{A}\varphi$ $\displaystyle\quad\text{iff
}M,\pi\models\varphi\text{ for all }\pi\in\textit{Paths}(s)$ $\displaystyle
M,\pi\models\psi$ $\displaystyle\quad\text{iff }M,\pi[0]\models\psi$
$\displaystyle M,\pi\models\mathrm{X}\varphi$ $\displaystyle\quad\text{iff
}M,\pi[1,\infty]\models\varphi$ $\displaystyle
M,\pi\models\varphi_{1}\,\mathrm{U}\,\varphi_{2}$ $\displaystyle\quad\text{iff
}\exists j\,.\,(M,\pi[j,\infty]\models\varphi_{2}\;\wedge$
$\displaystyle\quad\forall 1\leq i<j\,.\,M,\pi[i,\infty]\models\varphi_{1})$

The clauses for Boolean connectives are standard. Additional (dual) temporal
operators “sometime” and “always” can be defined as
$\mathrm{F}\psi\equiv\top\,\mathrm{U}\,\psi$ and
$\mathrm{G}\psi\equiv\neg\mathrm{F}\neg\psi$. Model $M$ satisfies formula
$\psi$ (written $M\models\psi$) iff $M,s_{0}\models\psi$ for all $s_{0}\in I$.

###### Example

Model $M=\mathcal{M}({\mathit{ASV}})$ in Figure 2b satisfies the
$\mathbf{ACTL^{\star}}$ formulae
$\mathsf{A}\mathrm{G}(\neg\texttt{obeyed}\vee\texttt{K\\_voted[x]=1})$, saying
that if Voter obeys, a Coercer gets to know how she voted, and
$\mathsf{A}\mathrm{G}(\neg\texttt{disobeyed}\vee\texttt{K\\_refused=1})$,
saying that she cannot disobey Coercer’s instructions without his knowledge.
It does not satisfy $\mathsf{A}\mathrm{F}(\neg\texttt{K\\_voted=[0,0,0]})$,
saying that Coercer will eventually get to know how Voter voted.

##  3\. Variable Abstraction for MAS Graphs

In this section, we describe how to automatically reduce MAS graphs by
simplifying their local variables.

1 compute the combined graph $G_{\textit{MG}}$ of MG

2 compute the approximate local domain $d$ for $V$ in $G_{\textit{MG}}$

3 foreach  _agent graph $G_{i}\in\textit{MG}$_ do

4 compute abstract graph $\mathcal{A}(G_{i})$ w.r.t. $\textit{Var}_{i}\cap V$
and $d_{i}$

5

6 end foreach

return
$\mathcal{A}(\textit{MG})=\\{\\!|{\textit{Var}_{sh},\mathcal{A}(G_{1}),\ldots,\mathcal{A}(G_{n})}|\\!\\}$

Algorithm 1 Abstraction of MAS graph
$\textit{MG}=\\{\\!|{\textit{Var}_{sh},G_{1},\ldots,G_{n}}|\\!\\}$ w.r.t.
variables $V$

###  3.1. Main Idea

We transform the MAS graph
$\textit{MG}=\\{\\!|{\textit{Var}_{sh},G_{1},\ldots,G_{n}}|\\!\\}$ in such a
way that: (i) the resulting abstract MAS graph $\mathcal{A}(\\!\textit{MG})$
is transformed _locally_ , i.e.,
$\mathcal{A}(\textit{MG})=\\{\\!|{\textit{Var}_{sh},\mathcal{A}(G_{1}),\ldots,\mathcal{A}(G_{n})}|\\!\\}$;
(ii) the abstract agent graphs $\mathcal{A}(G_{i})$ have the same structure of
locations as their concrete versions $G_{i}$; (iii) the only change results
from removal of a subset of local variables $V$, or simplifying their domains
of values.

Moreover, we want may-abstraction
$\mathcal{A}^{\textit{may}}=\mathcal{A}(\\!\textit{MG})$ to _over-approximate_
MG, in the sense that every transition in MG has its counterpart in
$\mathcal{A}^{\textit{may}}$. Then, every formula of type $\mathsf{A}\varphi$
that holds in the model $\mathcal{M}(\mathcal{A}^{\textit{may}})$ must also
hold in the model $\mathcal{M}(\textit{MG})$.

Alternatively, we may want must-abstraction
$\mathcal{A}^{\textit{must}}=\mathcal{A}(\textit{MG})$ to _under-approximate_
MG, in the sense that all transitions in $\mathcal{A}^{\textit{must}}$ have
their counterparts in MG. Then, if $\mathsf{A}\varphi$ is false in
$\mathcal{M}(\mathcal{A}^{\textit{must}})$, it also cannot be true in
$\mathcal{M}(\textit{MG})$.

The general structure of the procedure is shown in Algorithm 1. First, we
approximate the set of reachable evaluations $d(V,l)$ in every location of a
combined MAS graph $G_{\textit{MG}}$. This can be done following the algorithm
ApproxLocalDomain, presented in Appendix A. Then, its output is used to
transform the agent graphs $G_{i}$, one by one, by removing (or simplifying)
those variables of $V$ that occur in $G_{i}$. We implement it by function
ComputeAbstraction in Sections 3.2–3.4.

Assumptions and Notation. Assume there is a unique initial evaluation
$\eta_{0}$ satisfying initial condition $g_{0}$,
$\exists!\eta_{0}\in\textit{Eval}(\\!\textit{Var})\cap\textit{Sat}(g_{0})$,
and assigning each $v\in\textit{Var}$ with its default value
$v_{0}=\eta_{0}(v)$.

Furthermore, for an approximation $d$ obtained from variables $V$ and
$\textit{Loc}=\textit{Loc}_{1}\times\ldots\times\textit{Loc}_{n}$, by $d_{i}$
we denote a reduced on the $i$-th location component “narrowing” of a local
domain, where $1\leq i\leq n$. Intuitively, for $l_{j}\in\textit{Loc}_{i}$ the
value of $d_{i}(V,l_{j})$ is defined as
$\bigcup_{l\in\textit{Loc}_{1}\times\ldots\times\textit{Loc}_{i-1}\times\\{{l_{j}}\\}\times\textit{Loc}_{i+1}\times\ldots\times\textit{Loc}_{n}}d(V,l)$.

Upper- vs. Lower-Approximation. We define two variants of the algorithm. The
upper-approximation of local domain for every $l\in\textit{Loc}$ initializes
$d(V,l)=\varnothing$, and then adds new, possibly reachable values of $V$
whenever they are produced on an edge coming to $l$. The lower-approximation
initializes $d(V,l)=\textit{dom}(V)$, and iteratively removes the values might
be unreachable. To this end, ApproxLocalDomain is parameterized by symbols
$d_{0}$ and $\otimes$, such that $d_{0}=\varnothing$ and $\otimes=\cup$ for
the upper-approximation, and $d_{0}=\textit{dom}(V)$ and $\otimes=\cap$ for
the lower-approximation. Note that $d_{0}$ is simply a neutral (identity)
element of the $\otimes$-operation.

$l\in\textit{Loc}$ | $r(l)$ | $d(x,l)$
---|---|---
$\langle{\texttt{idle,idle}}\rangle$ | $3$ | $\\{0\\}$
$\langle{\texttt{voted,idle}}\rangle$ | $2$ | $\\{1,2,3\\}$
$\langle{\texttt{obeyed,halt}}\rangle$ | $0$ | $\\{1,2,3\\}$
$\langle{\texttt{disobeyed,halt}}\rangle$ | $0$ | $\\{1,2,3\\}$
Table 1. Reachability index $r$ and upper-approximation domain $d$ for ASV

###### Example

The output of ApproxLocalDomain for the upper-approximation of variable $x$ in
the combined ASV graph of subsection 2.2 can be found in Table 1.

###  3.2. Abstraction by Removal of Variables

1 _ComputeAbstraction(_$G=G_{i}$ , $V$, $d=d_{i}$_)_

2 $\hookrightarrow_{a}:=\varnothing$

3 foreach  _$l\lhook\joinrel\xrightarrow{g:ch\,\alpha}l^{\prime}$_ do

4 foreach  _$c\in d(V,l)$_ do

5 $g^{\prime}:=g[V=c]$

6 $\delta_{0}=\\{{\eta\in\mathit{Sat}(g)\mid\eta(V)=c}\\}$

7 let $\alpha^{\prime}=\alpha^{(1)}\ldots\alpha^{(m)}$

8 for  _$i=1$ to $m$_ do

9
$\delta_{i}=\\{{\eta^{\prime}=\textit{Effect}(\eta,\alpha^{(i)})\mid\eta\in\delta_{i-1}}\\}$

10 if  _ $\textit{lhs}(\alpha^{(i)})\notin V$_ then

11 $\alpha^{(i)}:=\tau$

12

13 end for

14 $A=\prod_{i=1}^{m}\\{{\alpha^{(i)}[V=\eta(V)]\mid\eta\in\delta_{i}}\\}$

15 $\hookrightarrow_{a}:=\hookrightarrow_{a}\cup(\bigcup_{\alpha^{\prime}\in
A}\\{l\lhook\joinrel\xrightarrow{g^{\prime}:ch\,\alpha^{\prime}}l^{\prime}\\})$

16 end foreach

17

18 end foreach

19 $G.\hookrightarrow:=\hookrightarrow_{a}$

20 return _$G$_

21

Algorithm 2 Abstraction by variable removal

The simplest form of variable-based abstraction consists in the complete
removal of a given variable $x$ from the MAS graph. To this end, we use the
approximation of reachable values of $V\subseteq\textit{Var}$, produced by
ApproxLocalDomain. More precisely, we transform every edge between $l$ and
$l^{\prime}$ that includes variables from $V^{\prime}\subseteq V$ in its guard
and/or its update into a set of edges (between the same locations), each
obtained by substituting $V^{\prime}$ with a different value $C\in
d(V^{\prime},l)$, see Algorithm 2. The abstract agent graph obtained by
removing variables $V$ from $G$ in the context of MG is denoted by
$\mathcal{A}_{\\{{V}\\}}\left(G,\textit{MG}\right)$. Whenever relevant, we
will use $\mathcal{A}^{\textit{may}}$ (resp. $\mathcal{A}^{\textit{must}}$) to
indicate the used variant of abstraction.

###### Example

The result of removing variable $x$ from the voter graph, according to the
domain’s upper-approximation presented in Table 1, is shown in Figure 3. Note
that its unwrapping (Figure 4) is distinctly smaller than the original one
(Figure 2b). Still, as we will formally show in Section 4, all the paths of
the model in Figure 2b are appropriately represented in the model of Figure 4.

###  3.3. Merging Variables and Their Values

Figure 3. Over-approx. abstraction
$\mathcal{A}^{\textit{may}}_{\\{{x}\\}}(G_{\textit{Voter}},{\mathit{ASV}})$
Figure 4. Unwrapping for the over-approximating abstraction
$\mathcal{A}^{\textit{may}}_{\\{{x}\\}}({\mathit{ASV}})\ =\
\\{\\!|{\textit{Var}_{sh},\
\mathcal{A}^{\textit{may}}_{\\{{x}\\}}(G_{\textit{Voter}},{\mathit{ASV}}),\
G_{\textit{Coercer}})}|\\!\\}$

A more general variant of variable abstraction assumes a collection of
mappings ${F}=\\{f_{1},\ldots,f_{m}\\}$. Each mapping
$f_{i}:\textit{Eval}(X_{i})\mapsto\textit{Eval}(z_{i})$ merges the local
variables $X_{i}\subseteq\textit{Var}_{j}$ of some agent graph $G_{j}$ to a
fresh variable $z_{i}$. The abstraction based on $f_{i}$ removes variables
$X_{i}$ from graph $G_{j}$, and replaces them with $z_{i}$ that “clusters” the
values of $X_{i}$ into appropriate abstraction classes. We will use
$\textit{Args}_{R}(f_{i})=X_{i}$ and
$\textit{Args}_{R}({F})=\bigcup_{i=1}^{m}\textit{Args}_{R}(f_{i})$ to refer to
the variables removed by $f_{i}$ and ${F}$.
$\textit{Args}_{N}(f_{i})=\\{z_{i}\\}$ and
$\textit{Args}_{N}({F})=\bigcup_{i=1}^{m}\textit{Args}_{N}(f_{i})$ refer to
the new variables.

Note that the procedure in Section 3.2 can be seen as a special case, with a
sole mapping $f$ merging $X=\\{{x}\\}$ to a fresh variable $z$ with the
singleton domain $\textit{dom}(z)=\\{{\eta_{0}(x)}\\}$.

###  3.4. Restricting the Scope of Abstraction

The most general variant concerns a set
${F}=\\{(f_{1},\textit{Sc}_{1}),\ldots,(f_{m},\textit{Sc}_{m})\\}$, where each
$f_{i}:\textit{Eval}(X_{i})\mapsto\textit{Eval}(z_{i})$ is a variable mapping
in some graph $G_{j}$, and $\textit{Sc}_{i}\subseteq\textit{Loc}_{j}$ defines
its scope. In the locations $l\in Sc_{i}$, mapping $f_{i}$ is applied and the
values of all $v\in X_{i}$ are set to $v_{0}$ (depending on the needs,
different value can be fixed per location). Outside of $\textit{Sc}_{i}$, the
variables in $X_{i}$ stay intact, and the new variable $z_{i}$ is assigned an
arbitrary default value.

The resulting procedure is presented in Appendix B.

The abstract agent graph obtained by function ComputeAbstraction from $G$ in
the context of MG via ${F}$ is denoted by $\mathcal{A}_{{F}}(G,\textit{MG})$.
The abstraction of the whole MAS graph
$\textit{MG}=\\{\\!|{\textit{Var}_{sh},G_{1},\dots,G_{n}}|\\!\\}$ is defined
(in accordance with Algorithm 1) as

$\mathcal{A}_{{F}}(\textit{MG})=\\{\\!|{\textit{Var}_{sh},\mathcal{A}_{{F}}(G_{1},,\textit{MG})\dots,\mathcal{A}_{{F}}(G_{n},\textit{MG})}|\\!\\}$

(a) Election Authority graph

(b) Voter graph

Figure 5. MAS graph for simplified postal voting

conf | Concrete | Abstract 1 | Abstract 2 | Abstract 3
---|---|---|---|---
NV,NC | #St | tv (sec) | ta (sec) | #St | tv (sec) | ta (sec) | #St | tv (sec) | ta (sec) | #St | tv (sec)
1,1 | 2.30e+1 | 0 | 0.03 | 1.90e+1 | 0 | 0.07 | 1.80e+1 | 0 | 0.16 | 1.60e+1 | 0
1,2 | 2.70e+1 | 0 | 0.03 | 2.10e+1 | 0 | 0.08 | 2.00e+1 | 0 | 0.06 | 1.70e+1 | 0
1,3 | 3.10e+1 | 0 | 0.03 | 2.30e+1 | 0 | 0.06 | 2.20e+1 | 0 | 0.05 | 1.80e+1 | 0
2,1 | 2.41e+2 | 0 | 0.02 | 1.41e+2 | 0 | 0.06 | 1.26e+2 | 0 | 0.06 | 9.30e+1 | 0
2,2 | 3.69e+2 | 0 | 0.02 | 1.77e+2 | 0 | 0.04 | 1.66e+2 | 0 | 0.03 | 1.06e+2 | 0
2,3 | 5.29e+2 | 0 | 0.02 | 2.17e+2 | 0 | 0.06 | 2.14e+2 | 0 | 0.04 | 1.20e+2 | 0
3,1 | 2.99e+3 | 0.01 | 0.02 | 1.14e+3 | 0 | 0.07 | 9.72e+2 | 0.01 | 0.05 | 5.67e+2 | 0
3,2 | 6.08e+3 | 0.01 | 0.02 | 1.62e+3 | 0.01 | 0.05 | 1.57e+3 | 0 | 0.04 | 6.93e+2 | 0
3,3 | 1.09e+4 | 0.04 | 0.02 | 2.20e+3 | 0.02 | 0.03 | 2.44e+3 | 0 | 0.05 | 8.38e+2 | 0.01
4,1 | 3.98e+4 | 0.12 | 0.02 | 9.57e+3 | 0.05 | 0.08 | 7.94e+3 | 0.03 | 0.08 | 3.54e+3 | 0.02
4,2 | 1.06e+5 | 0.55 | 0.01 | 1.52e+4 | 0.08 | 0.08 | 1.60e+4 | 0.05 | 0.06 | 4.62e+3 | 0.04
4,3 | 2.36e+5 | 0.95 | 0.01 | 2.26e+4 | 0.12 | 0.08 | 2.99e+4 | 0.07 | 0.08 | 5.94e+3 | 0.06
5,1 | 5.46e+5 | 1.48 | 0.02 | 8.17e+4 | 0.36 | 0.19 | 6.71e+4 | 0.18 | 0.25 | 2.23e+4 | 0.13
5,2 | 1.90e+6 | 6.42 | 0.02 | 1.43e+5 | 0.76 | 0.18 | 1.69e+5 | 0.5 | 0.23 | 3.09e+4 | 0.23
5,3 | 5.16e+6 | 24.95 | 0.02 | 2.30e+5 | 1.43 | 0.22 | 3.79e+5 | 1.16 | 0.22 | 4.21e+4 | 0.39
6,1 | 7.58e+6 | 31.34 | 0.01 | 7.03e+5 | 4.39 | 0.55 | 5.79e+5 | 1.92 | 0.44 | 1.41e+5 | 0.92
6,2 | 3.41e+7 | 170.25 | 0.01 | 1.34e+6 | 10.87 | 0.50 | 1.82e+6 | 7.64 | 0.40 | 2.07e+5 | 1.83
6,3 | memout | 0.01 | 2.31e+6 | 20.31 | 0.84 | 4.87e+6 | 22.67 | 0.40 | 2.97e+5 | 4.7
7,1 | memout | 0.01 | 6.05e+6 | 46.75 | 2.34 | 5.07e+6 | 22.16 | 1.91 | 8.89e+5 | 8.34
7,2 | memout | 0.02 | 1.25e+7 | 149.84 | 1.33 | 1.98e+7 | 107.95 | 2.01 | 1.38e+6 | 16.11
7,3 | memout | 0.02 | 2.28e+7 | 304.86 | 2.49 | memout | 2.35 | 2.08e+6 | 30.75
8,1 | memout | 0.02 | 5.20e+7 | 482.66 | 10.30 | memout | 8.04 | 5.61e+6 | 66.44
8,2 | memout | 0.19 | memout | 12.17 | memout | 7.58 | 9.15e+6 | 150.86
8,3 | memout | 0.07 | memout | 9.52 | memout | 7.99 | 1.44e+7 | 348.99
9,1 | memout | 0.12 | memout | 70.49 | memout | 64.96 | 3.53e+7 | 474.43
9,2 | memout | 0.06 | memout | 68.46 | memout | 71.69 | memout
9,3 | memout | 0.12 | memout | 70.09 | memout | 72.72 | memout

Table 2. Experimental results for model checking of
$\varphi_{\mathit{bstuff}}$ in over-approximations of postal voting

conf | Concrete | Abstract 1 | Abstract 2 | Abstract 3
---|---|---|---|---
NV,NC | #St | tv (sec) | ta (sec) | #St | tv (sec) | ta (sec) | #St | tv (sec) | ta (sec) | #St | tv (sec)
1,1 | 23 | 0 | 0.03 | 15 | 0 | 0.07 | 14 | 0 | 0.08 | 14 | 0
1,2 | 27 | 0 | 0.03 | 15 | 0 | 0.05 | 14 | 0 | 0.06 | 14 | 0.01
1,3 | 31 | 0 | 0.03 | 15 | 0 | 0.05 | 14 | 0 | 0.04 | 14 | 0
2,1 | 241 | 0 | 0.01 | 81 | 0 | 0.04 | 70 | 0 | 0.04 | 70 | 0
2,2 | 369 | 0 | 0.01 | 81 | 0 | 0.02 | 70 | 0 | 0.03 | 70 | 0
2,3 | 529 | 0 | 0.03 | 81 | 0 | 0.02 | 70 | 0 | 0.04 | 70 | 0
3,1 | 2987 | 0 | 0.01 | 459 | 0 | 0.03 | 368 | 0 | 0.03 | 368 | 0
3,2 | 6075 | 0 | 0.02 | 459 | 0 | 0.03 | 368 | 0 | 0.03 | 368 | 0
3,3 | 1.09e+4 | 0 | 0.02 | 459 | 0 | 0.03 | 368 | 0 | 0.03 | 368 | 0
4,1 | 3.98e+4 | 0 | 0.01 | 2673 | 0 | 0.03 | 2002 | 0.01 | 0.04 | 2002 | 0
4,2 | 1.06e+5 | 0 | 0.01 | 2673 | 0 | 0.05 | 2002 | 0 | 0.03 | 2002 | 0
4,3 | 2.36e+5 | 0 | 0.01 | 2673 | 0 | 0.04 | 2002 | 0 | 0.03 | 2002 | 0
5,1 | 5.46e+5 | 0 | 0.01 | 1.58e+4 | 0 | 0.04 | 1.11e+4 | 0 | 0.06 | 1.11e+4 | 0
5,2 | 1.90e+6 | 0 | 0.01 | 1.58e+4 | 0 | 0.06 | 1.11e+4 | 0 | 0.05 | 1.11e+4 | 0
5,3 | 5.16e+6 | 0 | 0.02 | 1.58e+4 | 0 | 0.07 | 1.11e+4 | 0 | 0.05 | 1.11e+4 | 0.01
6,1 | 7.58e+6 | 0 | 0.01 | 9.40e+4 | 0 | 0.15 | 6.30e+4 | 0 | 0.09 | 6.30e+4 | 0
6,2 | 3.41e+7 | 0.01 | 0.01 | 9.40e+4 | 0 | 0.14 | 6.30e+4 | 0 | 0.10 | 6.30e+4 | 0
6,3 | 1.13e+8 | 0 | 0.01 | 9.40e+4 | 0 | 0.09 | 6.30e+4 | 0 | 0.09 | 6.30e+4 | 0
7,1 | 1.06e+8 | 0 | 0.01 | 5.62e+5 | 0.01 | 0.28 | 3.60e+5 | 0 | 0.24 | 3.60e+5 | 0
7,2 |  $\gg$1e+8 | 0 | 0.01 | 5.62e+5 | 0 | 0.34 | 3.60e+5 | 0 | 0.21 | 3.60e+5 | 0
7,3 |  $\gg$1e+8 | 0.01 | 0.01 | 5.62e+5 | 0 | 0.35 | 3.60e+5 | 0 | 0.23 | 3.60e+5 | 0
8,1 |  $\gg$1e+8 | 0 | 0.01 | 3.37e+6 | 0 | 0.90 | 2.08e+6 | 0 | 0.69 | 2.08e+6 | 0
8,2 |  $\gg$1e+8 | 0 | 0.02 | 3.37e+6 | 0 | 1.03 | 2.08e+6 | 0 | 0.63 | 2.08e+6 | 0
8,3 |  $\gg$1e+8 | 0 | 0.01 | 3.37e+6 | 0 | 0.86 | 2.08e+6 | 0 | 0.55 | 2.08e+6 | 0
9,1 |  $\gg$1e+8 | 0 | 0.01 | 2.02e+7 | 0 | 4.41 | 1.21e+7 | 0 | 2.43 | 1.21e+7 | 0
9,2 |  $\gg$1e+8 | 0 | 0.01 | 2.02e+7 | 0 | 2.80 | 1.21e+7 | 0 | 2.03 | 1.21e+7 | 0
9,3 |  $\gg$1e+8 | 0 | 0.01 | 2.02e+7 | 0 | 2.69 | 1.21e+7 | 0 | 1.99 | 1.21e+7 | 0
10,1 |  $\gg$1e+8 | 0 | 0.01 | 1.21e+8 | 0 | 9.61 | 7.03e+7 | 0 | 7.49 | 7.03e+7 | 0.01
10,2 |  $\gg$1e+8 | 0 | 0.01 | 1.21e+8 | 0 | 7.83 | 7.03e+7 | 0 | 8.02 | 7.03e+7 | 0
10,3 |  $\gg$1e+8 | 0 | 0.01 | 1.21e+8 | 0 | 8.99 | 7.03e+7 | 0 | 7.71 | 7.03e+7 | 0

Table 3. Experimental results for model checking of
$\varphi_{\mathit{dispatch}}$ in under-approximations of postal voting

##  4\. Correctness of Variable Abstraction

We will now prove that the abstraction scheme preserves the formulae of
$\mathbf{ACTL^{\star}}$ if the computation of variable domain $d$ produces an
upper-approximation of their reachable values. In essence, we show that the
abstraction always produces an over-approximation of the MAS graph, which
induces an appropriate simulation relation, and thus guarantees (one-way)
preservation of $\mathbf{ACTL^{\star}}$.

###  4.1. Simulations between Models

We first recall a notion of simulation between models Baier and Katoen (2008);
Clarke et al. (2018); Cohen et al. (2009).

######  Definition .

Let $M_{i}=(\textit{St}_{i},I_{i},\longrightarrow_{i},\textit{AP}_{i},L_{i})$,
$i=1,2$ be a pair of models, and let
$\textit{AP}\subseteq\textit{AP}_{1}\cap\textit{AP}_{2}$ be a subset of common
atomic propositions. Model $M_{2}$ _simulates_ model $M_{1}$ over AP (written
$M_{1}\preceq_{\textit{AP}}M_{2}$) if there exists a _simulation_ relation
$\mathcal{R}\subseteq\textit{St}_{1}\times\textit{St}_{2}$ over AP, s.t.:

  1. (i)

for every $s_{1}\in I_{1}$, there exists $s_{2}\in I_{2}$ with
$s_{1}\mathcal{R}s_{2}$;

  2. (ii)

for each $(s_{1},s_{2})\in\mathcal{R}$:

    1. (a)

$L_{1}(s_{1})\cap\textit{AP}=L_{2}(s_{2})\cap\textit{AP}$, and

    2. (b)

if $s_{1}\to s^{\prime}_{1}$ then there exists $s_{2}\to s^{\prime}_{2}$ such
that $s^{\prime}_{1}\mathcal{R}s^{\prime}_{2}$,

Additionally, for a pair of reachable states $s_{1},s_{2}$ in $M_{1},M_{2}$
such that $(s_{1},s_{2})\in\mathcal{R}$, we say that the pointed model
$(M_{2},s_{2})$ _simulates_ $(M_{1},s_{1})$ over AP, and denote it by
$(M_{1},s_{1})\preceq_{\textit{AP}}(M_{2},s_{2})$.

For $(M_{1},s_{1})\preceq_{\textit{AP}}(M_{2},s_{2})$ and any
$\mathbf{ACTL}^{\ast}$ state formula $\psi$, built of propositions from $AP$
only, it holds that:

$M_{2},s_{2}\models\psi\text{\quad implies\quad}M_{1},s_{1}\models\psi$
($\ast$)

The proof is standard, see e.g. Baier and Katoen (2008).

###  4.2. Over-Approximations of MAS Graphs

Let $M_{1}=\mathcal{M}(\textit{MG}_{1}),M_{2}=\mathcal{M}(\textit{MG}_{2})$ be
models resulting from unwrapping of MAS graphs
$\textit{MG}_{1},\textit{MG}_{2}$. We start with a notion of simulation
between states and runs, and then use that to define what it means for a
$M_{2}$ to be a may-approximation of $M_{1}$.

######  Definition .

State $s_{2}=\langle{l_{2},\eta_{2}}\rangle$ _simulates_ state
$s_{1}=\langle{l_{1},\eta_{1}}\rangle$ with respect to variables
$V\subseteq\textit{Var}_{1}\cap\textit{Var}_{2}$ (denoted
$s_{1}\precsim_{V}s_{2}$) iff $l_{1}=l_{2}$ and for all $v\in V$ we have
${\eta_{1}}(v)={\eta_{2}}(v)$.

Moreover, run $\pi_{2}\in\textit{Runs}(M_{2})$ _simulates_ run
$\pi_{1}\in\textit{Runs}(M_{1})$ with respect to $V$ (denoted
$\pi_{1}\precsim_{V}\pi_{2}$) iff:

  1. (i)

$\textit{length}(\pi_{1})=\textit{length}(\pi_{2})=t$, and

  2. (ii)

for every $1\leq i\leq t$, it holds that $\pi_{1}[i]\precsim_{V}\pi_{2}[i]$.

The following is straightforward.

###### Lemma

If $\pi_{1}\precsim_{V}\pi_{2}$ and their length is $t$, then for all $1\leq
i<j\leq t$ it holds that $\pi_{1}[i,j]\precsim_{V}\pi_{2}[i,j]$.

###### Lemma

For pointed models $(M_{1},s_{1})$ and $(M_{2},s_{2})$, s.t.
$s_{1}=\langle{l,\eta_{1}}\rangle\in\textit{St}_{1}$ and
$s_{2}=\langle{l,\eta_{2}}\rangle\in\textit{St}_{2}$ it holds that:

$(M_{1},s_{1})\precsim_{V}(M_{2},s_{2})$ implies
$(M_{1},s_{1})\preceq_{\mathit{AP(V)}}(M_{2},s_{2})$.

We emphasize that model’s approximation is defined over the set of variables
$V$, which, for its part, establishes the subset of common atomic propositions
$AP(V)$ for the simulation relation.

###  4.3. Variable Abstraction Is Sound

We prove now that the abstraction method in Section 3, based on upper-
approximation of local domain, is indeed a simulation.

###### Lemma

Let MG be a MAS graph and $d$ be an upper-approximation of a local domain for
$B\subsetneq\textit{Var}$. Then, if state $\langle{l,\eta}\rangle$ is
reachable in $\mathcal{M}(\textit{MG})$, it must be that $\eta(B)\in d(B,l)$.

$\mathcal{M}(\textit{MG})\quad\precsim_{\textit{Var}\setminus\textit{Args}_{R}({F})}\quad\mathcal{M}(\mathcal{A}_{{F}}^{\textit{may}}(\textit{MG}))$.

###### Proof.

Let $M_{1}=\mathcal{M}(\textit{MG})$ and
$M_{2}=\mathcal{M}(\mathcal{A}_{{F}}^{\textit{may}}(\textit{MG}))$,
$W=\textit{Args}_{R}({F})$, $V=\textit{Var}_{1}\setminus W$,
$\textit{Var}_{2}=V\cup\textit{Args}_{N}({F})$. Notice that
$\textit{Args}_{N}({F})\cap V=\varnothing$ by definition of ${F}$, thus
applying the mapping functions from ${F}$ on the evaluation $\eta$ will have
no effect on its $V$ fragment, namely for any
$X\subseteq\textit{Var}_{1}\cup\textit{Var}_{2}$ and $c\in\textit{dom}(X)$ if
$X\cap V=\varnothing$ then $\eta(V)=\eta[X=c](V)$.

The requirement (i) from subsection 4.1 is satisfied as the set of locations
Loc remains unchanged and for any $\eta_{1}\in\textit{Sat}(g_{0})$ and
$\eta_{2}\in\textit{Sat}(g_{0}\wedge g_{R})$, where
$g_{R}\in\textit{Cond}(\textit{Args}_{N})$, it holds that
$\eta_{1}(V)=\eta_{2}(V)$.

By the construction of the $\mathcal{A}^{\textit{may}}$ each state
$\langle{l,\eta}\rangle\in\textit{St}_{2}$ is either initial
$\langle{l,\eta}\rangle\in I_{2}$ or
$\exists\langle{l^{\prime},\eta^{\prime}}\rangle\in\textit{St}_{2}$ such that
$\eta=\textit{Effect}(\alpha,\eta^{\prime}[W=c])$ for some $c\in
d(W,l^{\prime})$, $l^{\prime}\lhook\joinrel\xrightarrow{g:\alpha}l$, and
$\eta^{\prime}[W=c]\in\textit{Sat}(g)$. By that, the requirement (ii) is
naturally satisfied. ∎

Our main result follows directly from Theorems 4.1, 4.2, and 4.3. Let MG be a
MAS graph, and ${F}$ a set of mappings as defined in Section 3.4. Then, for
every formula $\psi$ of $\mathbf{ACTL^{\star}}$ that includes no variables
being removed or added by ${F}$:

$\mathcal{M}(\mathcal{A}_{{F}}^{\textit{may}}(\textit{MG}))\models\psi$
implies $\mathcal{M}(\textit{MG})\models\psi.$

Under-approximating abstractions. An analogous result can be obtained for
must-abstraction $\mathcal{A}_{{F}}^{\textit{must}}(\textit{MG})$.

###### Lemma

Let MG be a MAS graph and $d$ be a lower-approximation of a local domain for
$B\subsetneq\textit{Var}$. Then, for any $c\in d(B,l)$ there must exist
reachable $\langle{l,\eta}\rangle$ such that $\eta(B)=c$.

For each formula $\psi\in\mathbf{ACTL^{\star}}$ including no variables removed
by ${F}$:
$\mathcal{M}(\mathcal{A}_{{F}}^{\textit{must}}(\textit{MG}))\not\models\psi$
implies $\mathcal{M}(\textit{MG})\not\models\psi.$

The proof is analogous (see appendix C).

Abstraction for MAS templates. Interestingly, when the MAS graph contains a
subset of agent graphs being instances of the very same template (i.e., almost
identical, up to variable renaming and evaluation of a constant parameters),
one could apply an abstraction on that template fragment resulting with a
coarser abstraction of the original MAS graph, yet exponentially faster to
compute.

######  Definition .

MAS template $MT$, a compact representation of a MAS graph MG, as a tuple
$(\textit{Var}_{sh},\textit{Const}_{sh},(GT_{1},\\#_{1}),\ldots,(GT_{k},\\#_{k}))$,
which lists of the pairs of agent templates $GT_{i}$ and number of their
instances $\\#_{i}$, as well as the set of shared variables
$\textit{Var}_{sh}$ and additionally the set of shared constant (read-only)
variables $\textit{Const}_{sh}$.

Let $\textit{MG}=\\{\\!|{\textit{Var}_{sh},G_{1},\dots,G_{n}}|\\!\\}$ and $MT$
be a corresponding MAS template. Then upper-approximating a local domain
$d_{i}$ of an agent template $GT_{i}$ discarding all of the synchronisation
labels from its edges, will induce a may-abstraction
$\mathcal{A}^{\textit{may}}(MT)$.

Analogously, lower-approximating a local domain $d_{i}$ of an agent template
$GT_{i}$ discarding all edges with synchronisation label, will induce a must-
abstraction $\mathcal{A}^{\textit{must}}(MT)$.

###### Proof.

Follows directly from the fact that discarding synchronisation labels results
with a coarser upper-approximation of a $d_{i}$ and discarding the edges with
synchronisation labels with a coarser lower-approximation. ∎

##  5\. Case Study and Experimental Results

In this section, we evaluate our abstraction scheme on a simplified real-life
scenario.

###  5.1. Case Study: Integrity of Postal Voting

As input, we use a scalable family of MAS graphs that specify a simplified
postal voting system. The system consists of a single agent graph for the
Election Authority (depicted in 5(a)) and $\mathit{NV}$ instances of eligible
Voters (5(b)).

Each voter can vote for one of the $\mathit{NC}$ candidates. The voter starts
at the location idle, and declares if she wants to receive the election
package (that contains the voting declaration and a ballot) by post or to pick
it up in person. Then, the voter waits until it can be collected, which leads
to location has. At this point, the voter sends the forms back to the
authority, either filled in or blank (e.g., by mistake). The authority
collects the voters’ intentions (at location coll_dec), distributes the
packages (at send_ep), collects the votes, and computes the tally (at
coll_vts). A vote is added to the tally only if the declaration is signed and
the ballot is filled.

In the experiments for over-approximating abstraction, we have verified the
formula

$\varphi_{\mathit{bstuff}}\equiv\mathsf{A}\mathrm{G}\mathsf{{(\sum_{i=1}^{\mathit{NC}}tally[i]\leq\sum_{j=1}^{\mathit{NV}}pack\\_sent[j]\leq\mathit{NV})}}$

expressing the important property of resistance to _ballot stuffing_. More
precisely, the formula says that the amount of sent packages can never be
higher than the number of voters, and there will be no more tallied votes than
packages. The formula is satisfied in all the instances of our voting model.

In the experiments for under-approximation, we used

$\varphi_{\mathit{dispatch}}\equiv\mathsf{A}\mathrm{G}\mathsf{{{\
coll\\_vts}\textit{ imply
}(\sum_{j=1}^{\mathit{NV}}pack\\_sent[j]=\mathit{NV})}}$

expressing that the election packages must be eventually dispatched to all the
voters.777The aforementioned formula is equivalent to
$\mathsf{A}\mathrm{F}\mathsf{{(\sum_{j=1}^{\mathit{NV}}pack\\_sent[j]=\mathit{NV})}}$
in our model; the former variant is used due to Uppaal’s non-standard
interpretation of the $\mathsf{A}\mathrm{F}$.  The formula is false in all the
considered instances of the system.

###  5.2. Results of Experiments

We have used the following abstractions:

  * •

Abstraction 1: globally removes variables mem_sg and mem_vt, i.e., the voters’
memory of the cast vote and whether the voting declaration has been signed;

  * •

Abstraction 2: removes the variable mem_dec at locations {has, voted}, and
dec_recv at {coll_vts};

  * •

Abstraction 3: combines the previous two.

Model checking of $\varphi_{\mathit{bstuff}}$ and
$\varphi_{\mathit{dispatch}}$ has been performed with 32-bit version of Uppaal
4.1.24 on a laptop with Intel i7-8665U 2.11 GHz CPU, running Ubuntu 22.04. The
abstract models were generated using a script in node.js with default 2GB RAM
memory limit.888 Implementation prototype and utilized models can be found at
https://github.com/aamas23submission/postal-voting-model.  The results are
presented in Tables 2 and 3. Each row lists the scalability factors (i.e., the
number of voters and candidates), the size and verification time for the
original model (so called “concrete model”), and the results for Abstractions
1–3. “Memout” indicates that the verification process ran out of memory. The
columns ‘ta’ and ‘tv’ stand for abstract model generation and verification
time accordingly. In all the other cases, the verification of the abstract
model was conclusive (i.e., the output was “true” for all the instances in
Table 2 and “false” for all the instances in Table 3).

The results show significant gains. In particular, for the variant with
$\mathit{NC}=3$ candidates, our over-approximating may-abstractions allowed to
increase the main scalability factor by 3, i.e., to verify up to 9 instead of
6 voters.

In case when a $\mathsf{A}\mathrm{G}$ formula is not satisfied by the model,
its verification is in fact equivalent to finding a witness for a
$\mathsf{E}\mathrm{F}$ formula, which is often easy in practice. And it
becomes even more so if model checker utilizes on-the-fly techniques (as is
the case of Uppaal) and examines the model simultaneously with generation of
states. This is confirmed by experimental results for model checking of
$\varphi_{\mathit{dispatch}}$. However, it is worth noting that despite the
lack of notable gains in terms of verification time from must-abstraction, the
reduction in state space could be of immense importance when model is
generated prior to its exploration.

##  6\. Conclusions

In this paper, we present a correct-by-design method for model reductions that
facilitates model checking. Theoretically speaking, our reductions are
_may/must_ state abstractions. Their main appeal, however, lies in their ease
of use, rather than theoretical characteristics. They come with a natural
methodology, and require almost no technical knowledge from the user. All that
the user needs to do is to select a subset of variables to be removed from the
MAS graph representing the system (in the simplest case). The more involved
approach relies on defining mappings that merge information stored in local
variables of an agent module.

The methodology is agent-based, meaning that the abstractions transform the
specification of the system at the level of agent graphs, without changing the
overall structure. Moreover, they are guaranteed to generate a correct
abstract MAS graph, i.e., one that provides the lower (resp. upper) bound for
the truth values of formulae to be verified. Note also that the procedure is
generic enough to be used in combination with other techniques, such as
partial-order reduction.

We demonstrate the effectiveness of the method on a case study involving the
verification of a postal voting procedure using the Uppaal model checker. As
we have shown, simple abstractions allow to expand the range of verification
by many orders of magnitude. Clearly, the efficiency of the method depends on
the right selection of variables and the abstraction scope; ideally, this
should be provided by a domain expert.

In the future, we want to combine variable abstraction with abstractions that
transform locations in a MAS graph. Even more importantly, we plan to extend
the methodology from branching-time properties to formal verification of
strategic ability. An implementation as an extension of the STV model checker
Kurpiewski et al. (2021) is also considered.

## References

  * (1)
  * Alur et al. (1998) R. Alur, T.A. Henzinger, O. Kupferman, and M.Y. Vardi. 1998\.  Alternating refinement relations. In _Proceedings of CONCUR_ _(Lecture Notes in Computer Science, Vol. 1466)_. 163–178.
  * Alur and Henzinger (1999) R. Alur and T. A. Henzinger. 1999.  Reactive Modules.  _Formal Methods in System Design_ 15, 1 (1999), 7–48.
  * Baier and Katoen (2008) C. Baier and J.-P. Katoen. 2008.  _Principles of Model Checking_.  MIT Press.
  * Ball and Kupferman (2006) T. Ball and O. Kupferman. 2006.  An Abstraction-Refinement Framework for Multi-Agent Systems. In _Proceedings of Logic in Computer Science (LICS)_. IEEE, 379–388.  https://doi.org/10.1109/LICS.2006.10
  * Behrmann et al. (2004) G. Behrmann, A. David, and K.G. Larsen. 2004.  A Tutorial on Uppaal. In _Formal Methods for the Design of Real-Time Systems: SFM-RT_ _(LNCS, 3185)_. Springer, 200–236.
  * Belardinelli et al. (2021) Francesco Belardinelli, Rodica Condurache, Catalin Dima, Wojciech Jamroga, and Michal Knapik. 2021\.  Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol.  _Information and Computation_ 276 (2021), 104552.  https://doi.org/10.1016/j.ic.2020.104552
  * Belardinelli and Lomuscio (2017) Francesco Belardinelli and Alessio Lomuscio. 2017.  Agent-based Abstractions for Verifying Alternating-time Temporal Logic with Imperfect Information. In _Proceedings of AAMAS_. ACM, 1259–1267.
  * Belardinelli et al. (2019) Francesco Belardinelli, Alessio Lomuscio, and Vadim Malvone. 2019\.  An Abstraction-Based Method for Verifying Strategic Properties in Multi-Agent Systems with Imperfect Information. In _Proceedings of AAAI_. 6030–6037.
  * Bulling et al. (2010) N. Bulling, J. Dix, and W. Jamroga. 2010.  Model Checking Logics of Strategic Ability: Complexity.  In _Specification and Verification of Multi-Agent Systems_ , M. Dastani, K. Hindriks, and J.-J. Meyer (Eds.). Springer, 125–159.
  * Clarke et al. (1994) E.M. Clarke, O. Grumberg, and D.E. Long. 1994.  Model Checking and Abstraction.  _ACM Transactions on Programming Languages and Systems_ 16, 5 (1994), 1512–1542.
  * Clarke et al. (2018) E.M. Clarke, T.A. Henzinger, H. Veith, and R. Bloem (Eds.). 2018.  _Handbook of Model Checking_.  Springer.  https://doi.org/10.1007/978-3-319-10575-8
  * Clarke et al. (2000) Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000.  Counterexample-Guided Abstraction Refinement. In _Proceedings of CAV_ _(Lecture Notes in Computer Science, Vol. 1855)_. Springer, 154–169.  https://doi.org/10.1007/10722167_15
  * Clarke et al. (2003) Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2003.  Counterexample-guided abstraction refinement for symbolic model checking.  _J. ACM_ 50, 5 (2003), 752–794.  https://doi.org/10.1145/876638.876643
  * Cohen et al. (2009) Mika Cohen, Mads Dam, Alessio Lomuscio, and Francesco Russo. 2009\.  Abstraction in model checking multi-agent systems. In _Proceedings of (AAMAS_. IFAAMAS, 945–952.
  * Cormen et al. (2009) Thomas H Cormen, Charles E Leiserson, Ronald L Rivest, and Clifford Stein. 2009.  _Introduction to algorithms_.  MIT press.
  * Cousot and Cousot (1977) P. Cousot and R. Cousot. 1977.  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_. 238–252.  https://doi.org/10.1145/512950.512973
  * Dams and Grumberg (2018) Dennis Dams and Orna Grumberg. 2018.  Abstraction and Abstraction Refinement.  In _Handbook of Model Checking_. Springer, 385–419.  https://doi.org/10.1007/978-3-319-10575-8_13
  * de Alfaro et al. (2004) Luca de Alfaro, Patrice Godefroid, and Radha Jagadeesan. 2004\.  Three-Valued Abstractions of Games: Uncertainty, but with Precision. In _Proceedings of Logic in Computer Science (LICS)_. IEEE Computer Society, 170–179.
  * de Bakker et al. (1984) J.W. de Bakker, J.A. Bergstra, Jan Willem Klop, and J.-J. Ch. Meyer. 1984.  Linear Time and Branching Time Semantics for Recursion with Merge.  _Theor. Comput. Sci._ 34 (1984), 135–156.  https://doi.org/10.1016/0304-3975(84)90114-2
  * Emerson (1990) E.A. Emerson. 1990\.  Temporal and Modal Logic.  In _Handbook of Theoretical Computer Science_ , J. van Leeuwen (Ed.). Vol. B. Elsevier, 995–1072.
  * Enea and Dima (2008) C. Enea and C. Dima. 2008\.  Abstractions of multi-agent systems.  _International Transactions on Systems Science and Applications_ 3, 4 (2008), 329–337.
  * Gerth et al. (1999) R. Gerth, R. Kuiper, D. Peled, and W. Penczek. 1999\.  A Partial Order Approach to Branching Time Logic Model Checking. In _Proceedings of ISTCS_. IEEE, 130–139.
  * Godefroid and Jagadeesan (2002) P. Godefroid and R. Jagadeesan. 2002.  Automatic Abstraction Using Generalized Model Checking. In _Proceedings of Computer Aided Verification (CAV)_ _(Lecture Notes in Computer Science, Vol. 2404)_. Springer, 137–150.  https://doi.org/10.1007/3-540-45657-0_11
  * Huang and van der Meyden (2014) X. Huang and R. van der Meyden. 2014.  Symbolic Model Checking Epistemic Strategy Logic. In _Proceedings of AAAI Conference on Artificial Intelligence_. 1426–1432.
  * Jamroga et al. (2020a) Wojciech Jamroga, Yan Kim, Damian Kurpiewski, and Peter Y. A. Ryan. 2020a.  Towards Model Checking of Voting Protocols in Uppaal. In _Proceedings of E-Vote-ID_ _(Lecture Notes in Computer Science, Vol. 12455)_. Springer, 129–146.  https://doi.org/10.1007/978-3-030-60347-2_9
  * Jamroga et al. (2021) Wojciech Jamroga, David Mestel, Peter B. Roenne, Peter Y. A. Ryan, and Marjan Skrobot. 2021\.  A Survey of Requirements for COVID-19 Mitigation Strategies.  _Bulletin of The Polish Academy of Sciences: Technical Science_ 69, 4 (2021), e137724.  https://doi.org/10.24425/bpasts.2021.137724
  * Jamroga et al. (2020b) W. Jamroga, W. Penczek, T. Sidoruk, P. Dembiński, and A. Mazurkiewicz. 2020b.  Towards Partial Order Reductions for Strategic Ability.  _Journal of Artificial Intelligence Research_ 68 (2020), 817–850.  https://doi.org/10.1613/jair.1.11936
  * Kacprzak et al. (2004) M. Kacprzak, A. Lomuscio, and W. Penczek. 2004.  Verification of Multiagent Systems via Unbounded Model Checking. In _Proceedings of AAMAS_. IEEE Computer Society, 638–645.  https://doi.org/10.1109/AAMAS.2004.10086
  * Kouvaros and Lomuscio (2017) P. Kouvaros and A. Lomuscio. 2017.  Parameterised Verification of Infinite State Multi-Agent Systems via Predicate Abstraction. In _Proceedings of AAAI_. 3013–3020.
  * Kurpiewski et al. (2021) Damian Kurpiewski, Witold Pazderski, Wojciech Jamroga, and Yan Kim. 2021.  STV+Reductions: Towards Practical Verification of Strategic Ability Using Model Reductions. In _Proceedings of AAMAS_. ACM, 1770–1772.
  * Lomuscio and Penczek (2007) A. Lomuscio and W. Penczek. 2007.  Symbolic Model Checking for Temporal-Epistemic Logics.  _SIGACT News_ 38, 3 (2007), 77–99.  https://doi.org/10.1145/1324215.1324231
  * Lomuscio et al. (2010a) A. Lomuscio, W. Penczek, and H. Qu. 2010a.  Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems.  _Fundamenta Informaticae_ 101, 1-2 (2010), 71–90.  https://doi.org/10.3233/FI-2010-276
  * Lomuscio et al. (2010b) Alessio Lomuscio, Hongyang Qu, and Francesco Russo. 2010b.  Automatic Data-Abstraction in Model Checking Multi-Agent Systems. In _Model Checking and Artificial Intelligence_ _(Lecture Notes in Computer Science, Vol. 6572)_. Springer, 52–68.  https://doi.org/10.1007/978-3-642-20674-0_4
  * McMillan (1993) K.L. McMillan. 1993\.  _Symbolic Model Checking: An Approach to the State Explosion Problem_.  Kluwer Academic Publishers.
  * McMillan (2002) K.L. McMillan. 2002\.  Applying SAT Methods in Unbounded Symbolic Model Checking. In _Proceedings of Computer Aided Verification (CAV)_ _(Lecture Notes in Computer Science, Vol. 2404)_. 250–264.
  * Nicola and Vaandrager (1990) Rocco De Nicola and Frits W. Vaandrager. 1990.  Action versus State based Logics for Transition Systems. In _Semantics of Systems of Concurrent Processes, Proceedings of LITP Spring School on Theoretical Computer Science_ _(Lecture Notes in Computer Science, Vol. 469)_. Springer, 407–419.  https://doi.org/10.1007/3-540-53479-2_17
  * Peled (1993) Doron A. Peled. 1993\.  All from One, One for All: on Model Checking Using Representatives. In _Proceedings of CAV_ _(Lecture Notes in Computer Science, Vol. 697)_ , Costas Courcoubetis (Ed.). Springer, 409–423.  https://doi.org/10.1007/3-540-56922-7_34
  * Penczek and Lomuscio (2003) W. Penczek and A. Lomuscio. 2003.  Verifying Epistemic Properties of Multi-Agent Systems via Bounded Model Checking. In _Proceedings of AAMAS_ (Melbourne, Australia). ACM Press, New York, NY, USA, 209–216.
  * Schnoebelen (2003) Ph. Schnoebelen. 2003\.  The Complexity of Temporal Model Checking. In _Advances in Modal Logics, Proceedings of AiML 2002_. World Scientific.
  * Shoham and Grumberg (2004) Sharon Shoham and Orna Grumberg. 2004.  Monotonic Abstraction-Refinement for CTL. In _Proceedings of TACAS_ _(Lecture Notes in Computer Science, Vol. 2988)_. Springer, 546–560.  https://doi.org/10.1007/978-3-540-24730-2_40
  * Shoham and Leyton-Brown (2009) Y. Shoham and K. Leyton-Brown. 2009.  _Multiagent Systems - Algorithmic, Game-Theoretic, and Logical Foundations_.  Cambridge University Press.
  * Wooldridge (2002) M. Wooldridge. 2002\.  _An Introduction to Multi Agent Systems_.  John Wiley & Sons.

_ApproxLocalDomain(_$G=G_{\textit{MG}}$ , $V$_)_

1 foreach  _ $l\in\textit{Loc}$_ do

2 $l.d:=d_{0}$

3 $l.p:=\varnothing$

4 $l.\mathit{color}:=\textit{white}$

5

6 end foreach

7 $l_{0}.d:=\\{{\eta(V)\mid\eta\in\textit{Sat}(g_{0})}\\}$

8 $Q:=\varnothing$

9 $\textnormal{{Enqueue}}(Q,l_{0})$

10 while  _$Q\neq\varnothing$_

11 $l:=\textnormal{{ExtractMax}}(Q)$

// process incoming edges

12 $d^{\prime}:=l.d$

13 foreach  _$l^{\prime}\in l.p$_ do

14 foreach  _$l^{\prime}\lhook\joinrel\xrightarrow{g:\alpha}l$_ do

15 $l.d:=l.d\cup
d^{\prime}\otimes\textnormal{{ProcEdge}}(l^{\prime},g,\alpha,l,V)$

16

17 end foreach

18

19 end foreach

20 $l.p=\varnothing$

21 if  _$d^{\prime}\neq l.d$_ then

22 $l.\mathit{color}:=\textit{grey}$

23

// process self-loops

24 $d^{\prime\prime}:=l.d$

25 foreach  _$l\lhook\joinrel\xrightarrow{g:\alpha}l$_ do

26 $l.d:=l.d\cup\textnormal{{ProcEdge}}(l,g,\alpha,l,V)$

27

28 end foreach

29

30 if  _$d^{\prime\prime}\neq l.d$_ then

31 $l.\mathit{color}:=\textit{grey}$

32 go to 3

33

// enqueue immeadiate-neighbours

34 if  _$l.\mathit{color}\neq\textit{black}$_ then

35 foreach  _$l^{\prime}\in\textit{Succ}^{{=}1}(l)$_ do

36 $Q:=\textnormal{{Enqueue}}(Q,l^{\prime})$

37 $l^{\prime}.p:=l^{\prime}.p\cup\\{{l}\\}$

38

39 end foreach

40 $l.\mathit{color}=\textit{black}$

41

42

43 end while

44 return _$\\{{\langle{(V,l),l.d}\rangle\mid l\in\textit{Loc}}\\}$_

45

46

47

_ProcEdge(_$l$ , $g$, $\alpha$, $l^{\prime}$, $V$_)_

1 $\delta_{0}:=\\{{\eta\in\textit{Sat}(g)\mid\eta(V)\in l.d}\\}$

2 let $\alpha:=\alpha^{(1)}\ldots\alpha^{(m)}$

3 for  _$i=1$ to $m$_ do

4
$\delta_{i}:=\\{{\eta^{\prime}=\textit{Effect}(\alpha^{(i)},\eta)\mid\eta\in\delta_{i-1}}\\}$

5 end for

6 return _$\\{{\eta(V)\mid\eta\in\delta_{m}}\\}$_

7

8

Algorithm 3 Approximation of local domain for $x\in\textit{Var}$

1 _ComputeAbstraction(_$G$ , $d$, ${F}$_)_

2 $X:=\textit{Args}_{R}({F})$

3 $Z:=\textit{Args}_{N}({F})$

4 $\textit{Sc}:=\bigcup_{(f_{i},\textit{Sc}_{i})\in{F}}\textit{Sc}_{i}$

5 $g_{0}:=g_{0}\wedge(Z=f(\eta_{0}(X)))$

6 $\hookrightarrow_{a}:=\varnothing$

7 foreach  _$l\lhook\joinrel\xrightarrow{g:ch\,\alpha}l^{\prime}$_ do

8 $F_{1}:=\\{f_{i}\mid(f_{i},\textit{Sc}_{i})\in{F}\wedge
l^{\prime}\in\textit{Sc}_{i}\\}$

9 $F_{2}:=\\{f_{i}\mid(f_{i},\textit{Sc}_{i})\in{F}\wedge
l^{\prime}\in\textit{Sc}_{i}\\}$

10 if  _$\\{{l,l^{\prime}}\\}\cap\textit{Sc}=\varnothing$_ then

11
$\hookrightarrow_{a}:=\hookrightarrow_{a}\cup\\{l\lhook\joinrel\xrightarrow{g:ch\,\alpha}l^{\prime}\\}$

12

13 else

14 foreach  _$\@vec{c}\in d(V,l)$_ do

15 $W_{1}:=\bigcup_{f\in F_{1}}\textit{Args}_{R}(f)$

16 $W_{2}:=\bigcup_{f\in F_{1}}\textit{Args}_{N}(f)$

17

18 $Y_{1}:=\bigcup_{f\in F_{2}}\textit{Args}_{R}(f)$

19 $Y_{2}:=\bigcup_{f\in F_{2}}\textit{Args}_{N}(f)$

20

21 $g^{\prime}:=g[W_{1}={\left.\kern-1.2pt\@vec{c}\right|_{W_{1}}}]$

22

23 $\alpha^{\prime}:=(W_{2}:=\eta_{0}(W_{2}).\alpha$

24
$\alpha^{\prime}:=(W_{1}:={\left.\kern-1.2pt\@vec{c}\right|_{W_{1}}}).\alpha^{\prime}$

25

26
$\alpha^{\prime}:=\alpha^{\prime}.(Y_{2}:=F_{2}({\left.\kern-1.2pt\@vec{c}\right|_{Y_{1}}}))$

27 $\alpha^{\prime}:=\alpha^{\prime}.(Y_{1}:=\eta_{0}(Y_{1}))$

28

29
$\hookrightarrow_{a}:=\hookrightarrow_{a}\cup\\{l\lhook\joinrel\xrightarrow{g^{\prime}:ch\,\alpha^{\prime}}l^{\prime}\\}$

30 end foreach

31

32

33 end foreach

34 $G.\hookrightarrow:=\hookrightarrow_{a}$

35 return _$G$_

36

Algorithm 4 General abstraction

##  Appendix A Approximating the Domains of Variables

Given MAS graph MG over variables Var, the approximation of reachable values
for a set of variables $V\subseteq\textit{Var}$ takes the combined MAS graph
$G_{\textit{MG}}$, and traverses it using a modified version of a priority-BFS
algorithm Cormen et al. (2009). It begins with the complement of the coarsest
approximation of a local domain $d_{0}$, and starting from $l_{0}$
systematically explores locations of graph, and iteratively refines $d(V,l)$
with each visit of $l$ (until the stable approximation is obtained). Each
location $l$ must be visited at least once, and whenever some of its
predecessors $l^{\prime}$ gets approximation $d(V,l^{\prime})$ refined, the
location $l$ gets to be re-visited.

The max-priority queue $Q$ stores the locations that must be visited (possibly
anew). Within the queue, the higher traversal-priority is given for locations
with greater reachability index $r(l)$, that is defined as the number of
locations $l^{\prime}\neq l$ reachable from $l$.999The values of $r(l)$ can be
derived from reachability matrix produced by Warshall’s algorithm, taking a
row-wise sum of non-zero elements apart from those in the main diagonal. This
will reduce the number of potential re-visits in comparison with generic FIFO
variant.

In the algorithm we associate each location $l$ with attributes
$\textit{color}\in\\{{\textit{white},\textit{grey},\textit{black}}\\}$, subset
of relevant predecessors $p\subseteq\textit{Loc}\setminus\\{{l}\\}$ and its
current local domain approximation $d$.

In lines 3–3, locations are initialized with white color, an empty set of
predecessors and initial approximation $d_{0}$. The color indicates if the
location is not visited yet (white), being visited and a finer approximation
of its local domain was found (grey), or if it was visited (black). Lines 3–3
initialize the queue with location $l_{0}$. The while-loop of lines 3–3
describes the visit of a location $l$. The set of relevant predecessors
indicates which had its approximation updated, that, for its part, may result
in a ‘finer’ $l.d$ (lines 3–3). After those were taken into account for $l.d$,
the $l.p$ is reset (line 3). Self-loops are processed separately with possible
repetitions until stabilization (lines 3–3). The auxiliary procedure ProcEdge
simulates potential transitions by computing the image (restricted by $V$) of
update $\alpha$ over evaluations satisfying guard $g$ and having their $V$
counterpart in source’s $l.d$. If during its visit, a location $l$ was colored
grey (from either black or white), then all of its immediate neighbours
$l^{\prime}$ must be inspected independently of their color, adding $l$ as the
relevant predecessor of each and lastly painting it black (lines 3–3).

The algorithm halts and returns the now stable approximation $d$ (line 3) when
the queue is empty and all locations are black. Clearly, the termination is
guaranteed by the finiteness of the variable domains.

##  Appendix B General variant of abstraction

For each pair $(f_{i},\textit{Sc}_{i})$ of mapping and its scope, it
transforms the edges in $G=G_{j}$ in the following way:

  * •

edges entering or inner the $\textit{Sc}_{i}$ have their actions appended with
(1) update of the target variable $z_{i}$ and (2) update which sets the values
of the source variables $X_{i}$ to their defaults (resetting those),

  * •

edges leaving or within the $\textit{Sc}_{i}$ an have actions prepended with
(1) update of source variables $X_{i}$ (a temporarily one to be assumed for
original action) and (2) update which resets the values of the target variable
$z_{i}$.

##  Appendix C Proof for must-abstraction

Let $M_{1}=\mathcal{M}(\textit{MG})$ and
$M_{2}=\mathcal{M}(\mathcal{A}_{{F}}^{\textit{must}}(\textit{MG}))$,
$W=\textit{Args}_{R}({F})$, $V=\textit{Var}_{1}\setminus W$,
$\textit{Var}_{2}=V\cup\textit{Args}_{N}({F})$.

Now, we show that $M_{1}$ simulates $M_{2}$ over $AP(V)$ using the subsection
4.1.

The requirement (i) is satisfied as the set of locations Loc remains unchanged
and for any $\eta_{1}\in\textit{Sat}(g_{0})$ and
$\eta_{2}\in\textit{Sat}(g_{0}\wedge g_{R})$, where
$g_{R}\in\textit{Cond}(\textit{Args}_{N})$, it holds that
$\eta_{1}(V)=\eta_{2}(V)$.

By the construction of the $\mathcal{A}^{\textit{must}}$ each state
$\langle{l,\eta}\rangle\in\textit{St}_{2}$ is either initial
$\langle{l,\eta}\rangle\in I_{2}$ or
$\exists\langle{l^{\prime},\eta^{\prime}}\rangle\in\textit{St}_{2}$ such that
$\eta=\textit{Effect}(\alpha,\eta^{\prime}[W=c])$ for some $c\in
d(W,l^{\prime})$, $l^{\prime}\lhook\joinrel\xrightarrow{g:\alpha}l$, and
$\eta^{\prime}[W=c]\in\textit{Sat}(g)$. Now we can utilize subsection 4.3 and
construct a sequence of corresponding states in $M_{1}$ up intill
$\langle{l,\eta[W=c]}\rangle$, which concludes with (ii) being satisfied.