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
SAFE For All is a universal-quantifier extension of the Swarm Safety Detector, currently in development. Universal quantification allows to express more demanding MAS execution semantics in which we can require that all agents of given types (or all agents) perform actions at each step. This includes the possibility of requiring that a global event in the MAS will have an effect on all agents that satisfy a given condition.
Our theoretical results show that, when universal quantification is allowed, our SMT-based verification procedure is partially-sound and complete. The MCMT model-checker can however be still effectively used also in this case.
The same result trivially extends to those cases in which such universal semantics is mixed with the basic one.
better be safe than sorry