Swarm robotics systems usually operate under uncertain conditions (unknown environment, failures, etc.) so that their behavior can only be estimated quantitatively in terms of performance metrics (e.g., average failure rate of the robots, expected energy consumption).

Statistical-model checking (SMC) is a “verification-inspired” approach that performs quantitative analysis of a system. Like model-checking, it uses formally-defined models from which it explores the reachable states. In contrast to standard model-checking, SMC does not require exhaustive computation of the reachable states to conclude about a given property. It answers quantitative questions based on partial state-space coverage, and evaluates confidence in such results based on stochastic models. SMC tools usually stop the analysis when the desired degree of confidence (provided as an input parameter) is reached.

The statistical model-checking tool SMC-BIP has been applied to a swarm robotics scenario in which marXbot robots are deployed in a given arena to find victims. The stochastic model built for such a scenario includes a faithful model of the sensing capabilities of the marXbot. By using SMC-BIP, the performance of different algorithms used for implementing individual robot behavior can be compared which has proven to be very helpful for optimizing solutions to the scenario.

Further Information:

• User Guide
• Download