2 Search Results for "Heriban, Adam"

Document
DOI: 10.4230/LITES.8.2.2
Swarms of Mobile Robots: Towards Versatility with Safety

Authors: Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
We present Pactole, a formal framework to design and prove the correctness of protocols (or the impossibility of their existence) that target mobile robotic swarms. Unlike previous approaches, our methodology unifies in a single formalism the execution model, the problem specification, the protocol, and its proof of correctness. The Pactole framework makes use of the Coq proof assistant, and is specially targeted at protocol designers and problem specifiers, so that a common unambiguous language is used from the very early stages of protocol development. We stress the underlying framework design principles to enable high expressivity and modularity, and provide concrete examples about how the Pactole framework can be used to tackle actual problems, some previously addressed by the Distributed Computing community, but also new problems, while being certified correct.
Cite as

Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Swarms of Mobile Robots: Towards Versatility with Safety. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 02:1-02:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{courtieu_et_al:LITES.8.2.2,
  author =	{Courtieu, Pierre and Rieg, Lionel and Tixeuil, S\'{e}bastien and Urbain, Xavier},
  title =	{{Swarms of Mobile Robots: Towards Versatility with Safety}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{02:1--02:36},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.2},
  URN =		{urn:nbn:de:0030-drops-192942},
  doi =		{10.4230/LITES.8.2.2},
  annote =	{Keywords: distributed algorithm, mobile autonomous robots, formal proof}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2019.41
Brief Announcement: Model Checking Rendezvous Algorithms for Robots with Lights in Euclidean Space

Authors: Xavier Défago, Adam Heriban, Sébastien Tixeuil, and Koichi Wada

Published in: LIPIcs, Volume 146, 33rd International Symposium on Distributed Computing (DISC 2019)

Abstract
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.
Cite as

Xavier Défago, Adam Heriban, Sébastien Tixeuil, and Koichi Wada. Brief Announcement: Model Checking Rendezvous Algorithms for Robots with Lights in Euclidean Space. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 41:1-41:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{defago_et_al:LIPIcs.DISC.2019.41,
  author =	{D\'{e}fago, Xavier and Heriban, Adam and Tixeuil, S\'{e}bastien and Wada, Koichi},
  title =	{{Brief Announcement: Model Checking Rendezvous Algorithms for Robots with Lights in Euclidean Space}},
  booktitle =	{33rd International Symposium on Distributed Computing (DISC 2019)},
  pages =	{41:1--41:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-126-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{146},
  editor =	{Suomela, Jukka},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2019.41},
  URN =		{urn:nbn:de:0030-drops-113487},
  doi =		{10.4230/LIPIcs.DISC.2019.41},
  annote =	{Keywords: Autonomous mobile robots, Rendezvous, Lights, Model Checking}
}
  • Refine by Type
  • 2 Document/PDF

  • Refine by Publication Year
  • 1 2022
  • 1 2019

  • Refine by Author
  • 2 Tixeuil, Sébastien
  • 1 Courtieu, Pierre
  • 1 Défago, Xavier
  • 1 Heriban, Adam
  • 1 Rieg, Lionel
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 LITES

  • Refine by Classification
  • 2 Theory of computation → Self-organization
  • 1 Computer systems organization → Robotic autonomy
  • 1 Software and its engineering → Formal methods
  • 1 Theory of computation → Distributed algorithms
  • 1 Theory of computation → Distributed computing models
  • Show More...

  • Refine by Keyword
  • 1 Autonomous mobile robots
  • 1 Lights
  • 1 Model Checking
  • 1 Rendezvous
  • 1 distributed algorithm
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact