Konur, Dixon and Fisher model a foraging swarm in the PRISM probabilistic model checker and check properties of the whole swarm. Each robot follows a probabilistic state machine (searching, grabbing, depositing, homing, resting) with timeouts and probabilities of finding, grabbing and losing food. To avoid building a product of N identical machines, they use a counting abstraction: one machine whose states carry the number of robots in each, updated by difference equations. Swarm energy is tracked as a discretised state variable.
Findings
- With 100 robots and the paper’s energy parameters, simulation shows swarm energy falls when the probability of finding food is below 0.5 and rises above it.
- In verification mode, the probability that swarm energy never drops below its initial value after t = 2000 (over N from 100 to 500 and food probability from 0 to 1 in steps of 0.01, up to t = 10000) came out as 0.59, matching the simulations.
- The counting abstraction is what makes swarm-sized models tractable. The authors say they could not have verified even tens of robots by composing individual machines.
Limits
- Robots are identical and independent. Collision avoidance and interference between robots are left out (the authors say so), and the abstraction cannot express one robot behaving differently from the rest.
- Fractional robot counts are rounded and energy is discretised, so results are about an approximation of the swarm.
- A short workshop-style paper. The fuller version is the authors’ 2012 Robotics and Autonomous Systems article.
Relevance
A faulty or Byzantine member breaks the counting abstraction: one robot that does not follow the shared state machine cannot be represented. Checking swarm-level properties when some members deviate is still open. See aerial swarms, multi-robot systems and runtime monitoring; the broader picture is in Luckcuck et al..
Links
- DOI · author copy
- Subfield: Safety and verification, Multi-robot systems