Using Model Checking to Formally Verify Rendezvous Algorithms for Robots with Lights in Euclidean Space

Xavier Défago, Adam Heriban, Sébastien Tixeuil +1

The paper details the first successful attempt at using model-checking techniques to verify the correctness of distributed algorithms for robots evolving in a \emph{continuous} env…