Brief Announcement: Model Checking Rendezvous Algorithms for Robots with Lights in Euclidean Space.

This announces the first successful attempt at using model-checking techniques to verify the correctness of self-stabilizing distributed algorithms for robots evolving in a continuous environment. The study focuses on the problem of rendezvous of two robots with lights and presents a generic verification model for the SPIN model checker. It will be presented in full at an upcoming venue.