This report documents the development of the model of a collections of robots implementing the Alpha Algorithm. Chapter 1 presents our model of the Alpha Algorithm collection. Currently, we only verified deadlock freedom, and document the results for different sizes of collections. This is work in progress.
We have verified deadlock freedom using FDR for collections containing up to 4 robots. In particular, for N = 0, the semantics reduces to STOP, for N = 1 the collection deadlocks, and for N = 2, 3 and 4, the collection is indeed deadlock free.
We are currently working on fine tuning the semantics to improve analysis efficiency.