Swarm Safety Detector is a web tool for helping you detect threats posed by swarms of robots. Their strength is represented by:

their diverse individual and group capabilities, for which the combination of synchronous or asynchronous actions can lead to unexpected circumstances;
their number, which is unknown and assumed unlimited (and it is also unknown how many agents will possess each capability, e.g., whether this is a redundant and/or generalist multi-agent system).

Will the swarm reach its objective or is your system safe? Swarm Safety Detector can make available to you advanced verification tools providing formal guarantees based only on your assumptions. No programming required.

Swarm Safety Detector is the result of a study on how to employ verification techniques on a so-called parameterised multi-agent system (PMASs), and in particular the task of verifying whether states satisfying a given goal formula, which existentially quantifies over the existence of agents, are reachable in a given MAS.

Differently from regular multi-agent systems, the model of a PMAS only describes a finite set of possible agent templates, while the actual number of concrete agent instances for each template is unbounded and cannot be foreseen at verification-time. This makes the state-space infinite. As the reachability of the goal may of course depend on the number of agent instances, the verification result must be correct irrespective of such number (unless the formula expresses a specific cardinality).

For the first time, this problem was addressed via model-checking based on satisfiability-modulo theory (SMT): the SAFE procedure is based on a special encoding of a PMAS into an array-based system (ABS) representation, ready to be verified by the MCMT model-checker (link).

Swarm Safety Detector is not simply a modelling GUI: it is based on a formal definition of different execution semantics for PMASs that were studied so that their translation into ABS would maintain desired guarantees on the verification task at hand. Thanks to the known results available on SMT-based verification for such system, the SAFE-based procedure is proven to be sound and complete for a large class of parameterized MAS, while it is proven to be complete and partially-sound for even more complex cases (see SAFE For All). Other verification tools for unsafety cannot offer these guarantees for entire classes of problems, but require a case-by-case analysis.

Moreover, our approach for unsafety checking of PMASs is unique in that it is currently being extended to account for relational data storages with read and write access (see SAFE Data). We are not aware of existing solutions for this kind of data-aware PMAS.

About MCMT

MCMT (link) is a model checker for infinite state systems based on the integration of Satisfiability Modulo Theories (SMT) solving and backward reachability. In its actual implementation, MCMT is capable of model checking invariant (safety) properties of a large class of infinite state systems called array-based systems (ABS). SAFE is developed by Safe Swarms Club and the Swarm Safety Detector and MCMT are not joint nor affiliated projects: our strength is that we are able to rely on a general-purpose model checker.

About MCMT

Safe Swarms Club

SAFE Base

SAFE For All

SAFE Data