Brief Announcement: Model Checking Rendezvous Algorithms for Robots with Lights in Euclidean Space
Résumé
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.
Mots clés
2012 ACM Subject Classification Theory of computation → Distributed algorithms
Theory of computation → Verification by model checking
Computer systems organization → Robotic autonomy
Theory of computation → Self-organization Keywords and phrases Autonomous mobile robots
Rendezvous
Lights
Model Checking
Origine : Fichiers produits par l'(les) auteur(s)
Loading...