Better be safe than sorry.
SMT-based verification of parameterized MASs
via the MCMT model checker
Better be safe than sorry.
SMT-based verification of parameterized MASs
via the MCMT model checker
Swarm Safety Detector is a web tool developed for studying the verification of parameterised multi-agent system (MASs), 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.
For the first time, this problem was addressed via model-checking based on satisfiability-modulo theory (SMT): the SAFE verification technique is based on the theory of array-based systems (ABS). Swarm Safety Detector allows you to model your agent templates and environment and translate this into an ABS representation, ready to be verified by the MCMT model-checker.
If the ABS is assessed to be safe by MCMT, you're set. If not, the output can be loaded back on SAFE which then converts it into the original PMAS representation, showing an example of how the unsafety condition was reached.
Crucially, the Swarm Safety Detector does not require any computation on your PMAS to determine whether soundness, completeness and termination of the verification approach can be guaranteed. The class of problems we can solve, and with which guarantees, are clearly and syntactically defined. It is enough to model your PMAS in one of the available versions of SAFE to immediately inherit the different guarantees from MCMT. More info below.
For PMASs with asynchronous execution (the execution semantics assumed by SAFE Base), the SMT-based verification procedure is sound and complete. When instead universal quantification is allowed (the execution semantics assumed by SAFE For All), the SMT-based verification procedure is partially-sound and complete. Termination is guaranteed unless a multi-array comparison feature is enabled - see the GUI. The MCMT model-checker can be effectively used in all these cases.
Note that existing verification tools cannot provide decidability guarantees based only on these assumptions, but require a costly analysis of the scenario before being able to answer this question. Instead, the difference between the PMASs allowed in SAFE Base and SAFE For All is syntactic.
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