کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
428898 686958 2015 6 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Impossibility of gathering, a certification
ترجمه فارسی عنوان
عدم امکان جمع آوری، صدور گواهینامه
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی


• We expand the Pactole Coq framework to use actual real numbers as robot positions.
• We certify correctness of Suzuki and Yamashita's impossibility result for two robots.
• We certify an even number of robots cannot gather if we allow initial multiplicity.

Recent advances in Distributed Computing highlight models and algorithms for autonomous swarms of mobile robots that self-organise and cooperate to solve global objectives. The overwhelming majority of works so far considers handmade algorithms and proofs of correctness.This paper builds upon a previously proposed formal framework to certify the correctness of impossibility results regarding distributed algorithms that are dedicated to autonomous mobile robots evolving in a continuous space. As a case study, we consider the problem of gathering all robots at a particular location, not known beforehand. A fundamental (but not yet formally certified) result, due to Suzuki and Yamashita, states that this simple task is impossible for two robots executing deterministic code and initially located at distinct positions. Not only do we obtain a certified proof of the original impossibility result, we also get the more general impossibility of gathering with an even number of robots, when any two robots are possibly initially at the same exact location.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information Processing Letters - Volume 115, Issue 3, March 2015, Pages 447–452
نویسندگان
, , , ,