文章基本信息

标题：Brief Announcement: Model Checking Rendezvous Algorithms for Robots with Lights in Euclidean Space
本地全文：下载
作者：Xavier Dfago ; Adam Heriban ; Sbastien Tixeuil 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：146
页码：1-3
DOI：10.4230/LIPIcs.DISC.2019.41
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Autonomous mobile robots; Rendezvous; Lights; Model Checking