Supervision : Sébastien TIXEUIL

Realistic Robot Networks

The goal of this thesis is to survey and analyze the current work done by the distributed robotics community to find the more realistic variations of the standard OBLOT model, develop new such variations, and determine which approach should be used in the long term. We develop a new, optimal Rendezvous algorithm using lights, and prove it using a model checking framework based on the SPIN model checker. The same luminous model is used to build more robust Leader Election algorithms, which allow for stricter constraints. We design a new vision model for mobile robots, Uncertain Visibility, which introduces a vision adversary for sensors to register false negatives and prove tight bounds under this new model for several benchmark problems. We then define and investigate a new problem, Obstruction, Detection, for the obstructed visibility model.
To facilitate analysis of complex models, we develop a framework for Monte-Carlo simulations of mobile robots, designed to simulate any model or algorithm with minimal effort. It is not a model checker and should be viewed as a replacement for researcher "intuition" to look for unexpected behavior in networks. We test this simulator against numerous algorithms and settings, yielding encouraging results.
Finally, we introduce another two algorithms: the first algorithm ensures the distance traveled for convergence in ASYNC is minimal ; the second allows for Leader Election with errors in vision.

2017-2023 Publications

• 2023
  • X. Défago, A. Heriban, S. Tixeuil, K. Wada : “Using model checking to formally verify rendezvous algorithms for robots with lights in Euclidean space”, Robotics and Autonomous Systems, vol. 163, pp. 104378, (Elsevier) (2023)
• 2021
  • A. Heriban, S. Tixeuil : “Mobile Robots with Uncertain Visibility Sensors: Possibility Results and Lower Bounds”, Parallel Processing Letters, vol. 31 (01), pp. 2150002, (World Scientific Publishing) (2021)
  • A. Heriban, S. Tixeuil : “Unreliable Sensors for Reliable Efficient Robots”, (2021)
• 2020
  • A. Heriban : “Realistic Robot Networks”, thesis, defence 12/09/2020, supervision Tixeuil, Sébastien (2020)
  • X. Défago, A. Heriban, S. Tixeuil, K. Wada : “Using Model Checking to Formally Verify Rendezvous Algorithms for Robots with Lights in Euclidean Space”, 2020 International Symposium on Reliable Distributed Systems (SRDS), Shanghai, China, pp. 113-122, (IEEE) (2020)
• 2019
  • X. Défago, A. Heriban, S. Tixeuil, K. Wada : “Brief Announcement: Model Checking Rendezvous Algorithms for Robots with Lights in Euclidean Space”, 33^rd International Symposium on Distributed Computing (DISC 2019), vol. 146, Leibniz International Proceedings in Informatics (LIPIcs), Budapest, Hungary, pp. 41:1-41:3, (Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik) (2019)
  • A. Heriban, S. Tixeuil : “Mobile Robots with Uncertain Visibility Sensors”, SIROCCO 2019 - 26^th International Colloquium on Structural Information and Communication Complexity, vol. 11639, Lecture Notes in Computer Science, L'Aquila, Italy, pp. 349-352, (Springer) (2019)
• 2018
  • A. Heriban, X. Défago, S. Tixeuil : “Optimally Gathering Two Robots”, The 19^th International Conference on Distributed Computing and Networking, Varanasi, India, pp. 3, (ACM Press) (2018)
• 2017
  • A. Heriban, X. Défago, S. Tixeuil : “Optimally Gathering Two Robots”, (2017)