DROPS

Document

DOI: 10.4230/LIPIcs.SAND.2026.18

Searching for an Eventually-Emerging Black Hole in Rings

Authors: François Bonnet, Quentin Bramas, and Anissa Lamani

Published in: LIPIcs, Volume 373, 5th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2026)

Abstract

We study a novel variant of the Black Hole Search (BHS) problem where the black hole, a node that silently destroys visiting agents, can appear at any time during execution, rather than being present initially, as is assumed in all previous work. Our focus is on ring networks, and we examine this variant of the BHS problem under various assumptions, including whether the ring size is known and whether agents can use pebbles for marking nodes. For synchronous agents, we provide four solutions: (1) a 4-agent algorithm for rings without additional assumptions, (2) a 3-agent algorithm assuming known ring size, (3) a 3-agent algorithm using pebbles, and (4) a 3-agent solution without additional assumptions but having a quadratic time complexity. For asynchronous agents, we develop two algorithms: one using n agents without additional assumptions, and another using only 4 agents with pebbles.

Cite as

François Bonnet, Quentin Bramas, and Anissa Lamani. Searching for an Eventually-Emerging Black Hole in Rings. In 5th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 373, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bonnet_et_al:LIPIcs.SAND.2026.18,
  author =	{Bonnet, Fran\c{c}ois and Bramas, Quentin and Lamani, Anissa},
  title =	{{Searching for an Eventually-Emerging Black Hole in Rings}},
  booktitle =	{5th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2026)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-427-7},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{373},
  editor =	{Mertzios, George B. and Richa, Andr\'{e}a W.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAND.2026.18},
  URN =		{urn:nbn:de:0030-drops-262527},
  doi =		{10.4230/LIPIcs.SAND.2026.18},
  annote =	{Keywords: Black hole search, mobile agent, distributed computing}
}

Document

DOI: 10.4230/LIPIcs.OPODIS.2017.12

Model Checking of Robot Gathering

Authors: Ha Thi Thu Doan, François Bonnet, and Kazuhiro Ogata

Published in: LIPIcs, Volume 95, 21st International Conference on Principles of Distributed Systems (OPODIS 2017)

Abstract

Recent advances in distributed computing highlight models and algorithms for autonomous mo- bile robots that self-organize and cooperate together in order to solve a global objective. As results, a large number of algorithms have been proposed. These algorithms are given together with proofs to assess their correctness. However, those proofs are informal, which are error prone. This paper presents our study on formal verification of mobile robot algorithms. We first propose a formal model for mobile robot algorithms on anonymous ring shape network under multiplicity and asynchrony assumptions. We specify this formal model in Maude, a specification and pro- gramming language based on rewriting logic. We then use its model checker to formally verify an algorithm for robot gathering problem on ring enjoys some desired properties. As the result of the model checking, counterexamples have been found. We detect the sources of some unforeseen design errors. We, furthermore, give our interpretations of these errors.

Cite as

Ha Thi Thu Doan, François Bonnet, and Kazuhiro Ogata. Model Checking of Robot Gathering. In 21st International Conference on Principles of Distributed Systems (OPODIS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 95, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{doan_et_al:LIPIcs.OPODIS.2017.12,
  author =	{Doan, Ha Thi Thu and Bonnet, Fran\c{c}ois and Ogata, Kazuhiro},
  title =	{{Model Checking of Robot Gathering}},
  booktitle =	{21st International Conference on Principles of Distributed Systems (OPODIS 2017)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-061-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{95},
  editor =	{Aspnes, James and Bessani, Alysson and Felber, Pascal and Leit\~{a}o, Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2017.12},
  URN =		{urn:nbn:de:0030-drops-86324},
  doi =		{10.4230/LIPIcs.OPODIS.2017.12},
  annote =	{Keywords: Mobile Robot, Robot Gathering, Formal Verification, Model Checking, Maude}
}

Search Results

Documents authored by Bonnet, François

Searching for an Eventually-Emerging Black Hole in Rings

Abstract

Cite as

Model Checking of Robot Gathering

Abstract

Cite as

Thanks for your feedback!

Could not send message