  In this paper we study the verification of parameterised multi-agent systems
(MASs), and in particular the task of verifying whether unwanted states,
characterised as a given state formula, are reachable in a given MAS, i.e.,
whether the MAS is unsafe. The MAS is parameterised and the model only
describes the finite set of possible agent templates, while the actual number
of concrete agent instances for each template is unbounded and cannot be
foreseen. This makes the state-space infinite. As safety may of course depend
on the number of agent instances in the system, the verification result must be
correct irrespective of such number. We solve this problem via infinite-state
model checking based on satisfiability modulo theories (SMT), relying on the
theory of array-based systems: we present parameterised MASs as particular
array-based systems, under two execution semantics for the MAS, which we call
concurrent and interleaved. We prove our decidability results under these
assumptions and illustrate our implementation approach, called SAFE: the Swarm
Safety Detector, based on the third-party model checker MCMT, which we evaluate
experimentally. Finally, we discuss how this approach lends itself to richer
parameterised and data-aware MAS settings beyond the state-of-the-art solutions
in the literature, which we leave as future work.
