Towards scalable proofs of robot swarm dependability

The concept of robot swarm has demonstrated its relevance in many safety critical applications as a cost-effective solution providing natural fault-tolerance by large number of mutually replacing agents. A critical factor to the swarm functionality is the high complexity of intra swarm coordination.We propose a fully distributed coordination algorithm that uses parameters like bidding distance and random waiting time between decision and action. Another key result is a formal method for predicting the success of swarm missions that rely on given coordination algorithm. The scalability of the model checking based proof method is addressed and a state symmetry based solution proposed.