Better be safe than sorry.
SMT-based verification of parameterized MASs
via the MCMT model checker
Swarm Safety Detector is a web tool for helping you detect threats posed by swarms of robots. Their strength is represented by:
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.
better be safe than sorry