JAIST Repository
https://dspace.jaist.ac.jp/Title

Automatic Verification of Distributed Mobile
Robot Algorithms

Author(s)Bonnet, Francois

Citation

科学研究費助成事業研究成果報告書: 1‑4

Issue Date

2016‑06‑08

TypeResearch Paper

Text version

publisher

URL

http://hdl.handle.net/10119/13680

RightsDescription

若手研究(B), 研究期間：2014〜2015, 課題番号
：26870228, 研究者番号：60700185, 研究分野
：Distributed Computing

Japan Advanced Institute of Science and Technology

３版

様式

Ｃ−１９、Ｆ−１９、Ｚ−１９ （共通）

科学研究費助成事業

研究成果報告書
平成 ２８ 年

６ 月

８ 日現在

機関番号： １３３０２
研究種目： 若手研究(B)
研究期間： 2014 〜 2015
課題番号： ２６８７０２２８
研究課題名（和文）Automatic Verification of Distributed Mobile Robot Algorithms

研究課題名（英文）Automatic Verification of Distributed Mobile Robot Algorithms

研究代表者
ＢＯＮＮＥＴ

Ｆｒａｎｃｏｉｓ（BONNET, Francois）

北陸先端科学技術大学院大学・情報科学研究科・助教
研究者番号：６０７００１８５
交付決定額（研究期間全体）：（直接経費）

1,400,000 円

研究成果の概要（和文）：二年目も、ツールの開発を行い、このツールによってロボットのgathering問題のアルゴリズムの正しさの確認ができました。Workshop on Distributed Robotics Swarms (WDRS'15)で発表し、さらにAdHoc‑Now'16の国際会議に採択され、発表する予定です。

研究成果の概要（英文）：In this second year of funding, we continued the development of the tool andobtained some new results.
(1) We had a paper accepted in AdHoc‑Now'16 (to be published in July), which is an extension of ourprevious work: With the help of our verification tool, we could design and check new algorithms to solve
the gathering problem in rings with four robots. More precisely, we studied the class of configurations
SP4 which is the single class left open in this context. Same results were also presented in the Workshop
on Distributed Robotic Swarms (WDRS'15).
(2) While being on a totally different topic, namely Game Theory, we would like to mention anotheraccepted paper (in CG'16, to be published in July). Indeed to obtain this result, we used techniques
similar to the ones we introduced in our verification tool. Hence our Kakenhi funding indirectly
contributed to that paper. We developed a tool that compute Nash Equilibrium (NE) and used it to find NE
of the famous Mastermind game.
研究分野： Distributed Computing
キーワード： Algorithm

Distributed Computing

RobotVerification

様 式 Ｃ−１９、Ｆ−１９、Ｚ−１９（共通）１．研究開始当初の背景
This research project belongs to the fieldof theoretical distributed mobile robot
computing. In this area, researchers study
how multiple mobile robots can cooperate
together,
without
anycentralorganization, in order to solve a giventask. Typical studied problems consist ingathering (e.g. [2,3,4]), exploration(e.g. [5,6]), and pattern formation (e.g.
[2,7,8]).
This area of research started around15 years ago [2,7] with the introductionof the first computational models fordistributed robot computing. Later, it
gained popularity and is now a very active
field of research. The recent survey [1],published last year, includes more than130
references(internationalconferences/journals). Most of thesepapers come from the last 10 years.
Nowadays, the research community isgeographically widely spread; there areresearchers from all around the world
working on these subjects; in Japan(Kyushu University, Nagoya Institute ofTechnology, Osaka University, …), inEurope (France, Italy, Spain, …), and in
America (Canada and USA).
Personally, I started to work on these
topics during my PhD, a few years ago(references [9,10]), and I focused more on
this research area during my post‑doctoral
studies at JAIST (Japan Advanced Instituteof Science and Technology) as a JSPS fellow.
Near the end of my fellowship, I realizedthat we need such a verification tool andit is the reason why I now propose thisresearch project.
In our community, papers typicallystudy a specific problem under a given
model. Usually, authors look for therequired assumptions that make the problem
solvable or unsolvable, and then, propose
algorithms solving the problem, including
proofs and/or experimentations to assess
their correctness.
However, some of the proposed
algorithms appear to be incorrect, atleast for some specific cases. For example,
the paper [6] contains two errors that were
not detected prior to publication. Theerrors come from both the intrinsic
complexity of these algorithms and thedifficulty of analyzing distributedalgorithms. We believe that many of theseerrors could be detected using anautomatic verification software.

Bibliography (title&authors only):[1] Distributed Computing by Oblivious
Mobile Robots, Paola Flocchini, Giuseppe
Prencipe, Nicola Santoro.
[2] Distributed Anonymous Mobile Robots,
Ichiro Suzuki, Masafumi Yamashita.
[3] Taking advantage of symmetries:
Gathering of many asynchronous oblivious
robots on a ring, Ralf Klasing, AdrianKosowski, Alfredo Navarra.
[4] Gathering of Robots on Anonymous Grids
without
Multiplicity
Detection,
Gianlorenzo D Angelo, Gabriele Di
Stefano, Ralf Klasing, Alfredo Navarra.
[5] Computing Without Communicating: Ring
Exploration by Asynchronous Oblivious
Robots, Paola Flocchini, David Ilcinkas,
Andrzej Pelc, Nicola Santoro.
[6] Exclusive Perpetual Ring Exploration
without Chirality, Lélia Blin, Alessia
Milani, Maria Potop‑Butucaru, Sébastien
Tixeuil.
[7] Hard Tasks for Weak Robots: The Roleof Common Knowledge in Pattern Formation
by Autonomous Mobile Robots, PaolaFlocchini, Giuseppe Prencipe, Nicola
Santoro, Peter Widmayer.
[8] Distributed Anonymous Mobile Robots:
Formation of Geometric Patterns, IchiroSuzuki, Masafumi Yamashita.
[9] Anonymous graph exploration without
collision by mobile robots, RobertoBaldoni, François Bonnet, Alessia Milani,Michel Raynal.
[10] On the Solvability of Anonymous
Partial Grids Exploration by Mobile Robots,
Roberto Baldoni, François Bonnet, Alessia
Milani, Michel Raynal.

２．研究の目的The main goal of this research is therefore
to propose a tool to automatize theverification of distributed mobile robots
algorithms. We would like to point out thatdesigning and developing such a tool does
not consist only in a simple engineeringtask. Due to the nature of robots
algorithms, we need to investigate newmodeling/verification techniques and itis where the interesting research lies.
The problems to investigate include, but
not limited to, the followings:•
How to include the notion of mobility
in the verification process?
•How to include the multiple possible
scheduling of independent robots?
•How to take in consideration thepotential failures of robots?

３．研究の方法
This project targets the development of averification tool for distributed mobile
robot algorithms. The research plan andmethod can briefly be summarized in threepoints:• Review
existingliterature
todetermine the features which have to beincluded in our tool,• Develop, test, and use the tool toobtain new results (three tasks inparallel),• Disseminate and promote the tool among
the research community. We expect toreceive relevant comments in order toimprove the tool such that it becomeswidely used.
The project is divided into five tasks that
could be summarized as follow:
Task 1: Study existing literature ondistributed mobile robots computing inorder to extract all features that need tobe included in our verification tool.
Task 2: Develop a working prototype
with only few features to illustrate thenecessity of such tool.
Task 3: Include more features.
Task 4: Investigate new problems
assisted by the tool.
Task 5: Disseminate our tool to thecommunity.

４．研究成果For FY2014:
We could include some new functionalities
in our verification tool, such as (1)taking into account the possibility ofrobots to create tower (multiple robots on
the same location), (2) allowing theactivations of multiple robots in the sameround, (3) including the gathering problem
in addition to the exploration problem
that we initially considered. Following
these improvements, as expected in theplan, we could obtain some interesting
results from the first year. Such progress
was made possible due to meetings withother
researchers
whileattendingconferences (especially DISC'14) andduring a visiting trip to LIP6 (Universityof Paris 6) in early 2015.
In particular, we had a paper
published in WSSR‑SRDS'14. Our method
permits to discover new protocols solving
the exploration problem, and to assess

specific optimization criteria (such asindividual coverage, visits frequency,etc.) that are met by those protocols.
For FY2015:
In this second year of funding, wecontinued the development of the tool andobtained some new results.
In particular, we had a paper acceptedin AdHoc‑Now'16 (to be published in July),
which is an extension of our previous work:
With the help of our verification tool, wecould design and check new algorithms tosolve the gathering problem in rings withfour robots. More precisely, we studied
the class of configurations SP4 which isthe single class left open in this context.
For FY2016 (future work):
We did not release yet our tool to thecommunity. In the coming year, we plan tofinish it and finally make our toll
available online.

５．主な発表論文等（研究代表者、研究分担者及び連携研究者には下線）〔雑誌論文〕（計 6 件）(1) François Bonnet, Maria Potop‑Butucaru,
Sébastien Tixeuil, Asynchronous Gatheringin Rings with 4 Robots, In Proceedings ofthe 14th International Conference on
Ad‑hoc, Mobile, and Wireless Networks,
AdHoc‑Now16, 14pages, 2016. (accepted,not yet published)
DOI: not yet available.
(2) François Bonnet, Simon Viennot, NashEquilibrium in Mastermind, In Proceedingsof the 8th International Conference onComputers and Games, refereed, CG16,12pages, 2016. (accepted, not yetpublished)
DOI: not yet available.
(3) François Bonnet, Xavier Défago, Thanh
Dang Nguyen, Maria Potop‑Butucaru, Tightbound on mobile Byzantine Agreement, In
Theoretical Computer Science, refereed,
Volume 609, Part 2, p.361‑373, 2016.
DOI: 10.1016/j.tcs.2015.10.019(4) François Bonnet, Xavier Défago, FranckPetit, Maria Potop‑Butucaru, SébastienTixeuil, Discovering and Assessing
Fine‑Grained Metrics in Robot NetworksProtocols, In 2014 IEEE 33rd InternationalSymposium on Reliable Distributed SystemsWorkshops, refereed, SRDSW14, p.50‑59,
2014.
DOI: 10.1109/SRDSW.2014.34(5) François Bonnet, Xavier Défago, ThanhDang Nguyen, Maria Potop‑Butucaru, Tight
Bound on Mobile Byzantine Agreement, In
Distributed Computing, 28th International
Symposium, refereed, DISC14, p.76‑90,
2014.
DOI: 10.1007/978‑3‑662‑45174‑8̲6(6) Thanh Dang Nguyen, François Bonnet,Xavier Défago, Mitigating the Spread of a
Virus in the Internet, In 2014 IEEE 33rd
International Symposium on Reliable
Distributed Systems Workshops, refereed,
SRDSW14, p.14‑19, 2014.
DOI: 10.1109/SRDSW.2014.26〔学会発表〕（計 1 件）(1)
François
Bonnet,Asynchronous
Gathering in Rings with 4 Robots, In
Workshop on Distributed Robotic Swarms,
5/10/2015, Arcadia Ichigaya hotel,Chioda‑ku, Tokyo.

〔図書〕（計 0 件）〔産業財産権〕○出願状況（計 0 件）
○取得状況（計 0 件）

〔その他〕
ホームページ等

６．研究組織(1)研究代表者
BONNET FRANCOIS (BONNET FRANCOIS)
北陸先端科学技術大学院大学・情報科学研
究科・助教
研究者番号：60700185(2)研究分担者
None(3)連携研究者
None