Better be safe than sorry.

SMT-based verification of parameterized MASs
via the MCMT model checker

SAFE Base is a existential-quantifier version of the Swarm Safety Detector, which allows to capture asynchronous execution semantics of parameterized multi-agent systems. Under this execution semantics, agents are not forced to select a local or synchronization action at each step but can freely remain idle.

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 array-based system representation, ready to be verified by the MCMT model-checker.

Our theoretical results show that, for the asynchronous case, our SMT-based verification procedure is sound and complete.

Existing verification tools cannot provide decidability guarantees based only on this assumption.

Safe Swarms Club

better be safe than sorry

SAFE For All