Xavier Défago, Adam Heriban, Sébastien Tixeuil, Koichi Wada: Using model checking to formally verify rendezvous algorithms for robots with lights in Euclidean space. Robotics Auton. Syst. 163: 104378 (2023)