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.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500