pith. sign in

arxiv: 1907.09871 · v1 · pith:XV5YN5B3new · submitted 2019-07-23 · 💻 cs.DC · cs.MA

Using Model Checking to Formally Verify Rendezvous Algorithms for Robots with Lights in Euclidean Space

Xavier D\'efago , Adam Heriban , S\'ebastien Tixeuil , Koichi Wada This is my paper

Pith reviewed 2026-05-24 17:01 UTC · model grok-4.3

classification 💻 cs.DC cs.MA
keywords model checkingrobot rendezvousluminous robotsdistributed algorithmsSPINsynchrony modelscontinuous space
0
0 comments X

The pith

Model checking verifies rendezvous algorithms for two robots with lights in continuous space.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs a generic SPIN model to automatically check correctness of algorithms in which two robots equipped with colored lights attempt to meet in the Euclidean plane. Design choices and supporting theorems keep the state space finite even with continuous positions and arbitrary activation schedules in fully synchronous, semi-synchronous, and asynchronous settings. When the model is run on published algorithms across six synchrony models, it reproduces every known correctness result and supplies counter-example traces for every known failure. This matters because manual proofs of the same algorithms are lengthy and prone to subtle errors arising from possible activation interleavings. The modeling effort also yields theorems showing that certain asynchronous schedules can create an effective memory property in otherwise oblivious robots without compromising luminous rendezvous solutions.

Core claim

The authors built a SPIN verification model for luminous-robot rendezvous in continuous environments and proved the theorems needed to keep its search space finite and faithful. Running the model on several known algorithms in six synchrony models yields outputs that match all published correctness results, including explicit counter-example executions for algorithms known to fail. In the course of the work they establish additional theorems: a well-chosen algorithm together with an ASYNC scheduler can induce an emerging memory property in a system of oblivious mobile robots, yet this property does not invalidate solutions that rely on lights.

What carries the argument

The generic SPIN model for two luminous robots that represents continuous positions and six synchrony schedulers through abstractions whose validity is supported by proved theorems.

If this is right

  • Correctness of rendezvous algorithms whose manual proofs are complex can be checked automatically.
  • The model produces explicit counter-example executions for any algorithm that fails under a given synchrony model.
  • Luminous rendezvous algorithms remain sound even when an ASYNC scheduler induces apparent memory in oblivious robots.
  • The same modeling framework can be reused to check additional known or proposed rendezvous algorithms.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same finite-state modeling approach may be adaptable to gathering or pattern-formation tasks with more than two robots.
  • Model checking could be used to search for the smallest number of colors sufficient in each synchrony model rather than proving bounds by hand.
  • The memory-emergence theorem may affect correctness arguments for other oblivious-robot algorithms that run under asynchronous activation.

Load-bearing premise

The modeling abstractions for continuous positions and asynchronous schedulers capture every relevant real execution without introducing or omitting critical interactions.

What would settle it

The model checker outputs a counter-example for an algorithm already proved correct by hand, or fails to output a counter-example for an algorithm already proved incorrect by hand.

Figures

Figures reproduced from arXiv: 1907.09871 by Adam Heriban, Koichi Wada, S\'ebastien Tixeuil, Xavier D\'efago.

Figure 1
Figure 1. Figure 1: Simulation of main schedulers as a Promela process. [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Rendezvous algorithms from the literature. Guards match the (me.color, other.color). Wildcard [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Proof for Oblivious Complete Self-Stabilization 1 2 3 other is 2 other is 1 other is 3 other {1,3} other is {1,2} other is {2,3} [PITH_FULL_IMAGE:figures/full_fig_p016_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Algorithm for the Luminous Complete Self-Stabilization [PITH_FULL_IMAGE:figures/full_fig_p016_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Execution for the Luminous proof of Theorem 1. W indicates the [PITH_FULL_IMAGE:figures/full_fig_p016_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Activating robot A first (left) leads to a simple-reachable configuration (right) We show a possible memory execution in [PITH_FULL_IMAGE:figures/full_fig_p018_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: A possible memory execution, note the continuing dependency on colors [PITH_FULL_IMAGE:figures/full_fig_p018_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: After activating B then A A B Computed Visible Computed Visible A1 A0 B0 B0 A1 A0 B1(A0) A0 A1 A0 B2(A0) B1(A0) [PITH_FULL_IMAGE:figures/full_fig_p018_8.png] view at source ↗
read the original abstract

The paper details the first successful attempt at using model-checking techniques to verify the correctness of distributed algorithms for robots evolving in a \emph{continuous} environment. The study focuses on the problem of rendezvous of two robots with lights. There exist many different rendezvous algorithms that aim at finding the minimal number of colors needed to solve rendezvous in various synchrony models (e.g., FSYNC, SSYNC, ASYNC). While these rendezvous algorithms are typically very simple, their analysis and proof of correctness tend to be extremely complex, tedious, and error-prone as impossibility results are based on subtle interactions between robots activation schedules. The paper presents a generic verification model written for the SPIN model-checker. In particular, we explain the subtle design decisions that allow to keep the search space finite and tractable, as well as prove several important theorems that support them. As a sanity check, we use the model to verify several known rendezvous algorithms in six different models of synchrony. In each case, we find that the results obtained from the model-checker are consistent with the results known in the literature. The model-checker outputs a counter-example execution in every case that is known to fail. In the course of developing and proving the validity of the model, we identified several fundamental theorems, including the ability for a well chosen algorithm and ASYNC scheduler to produce an emerging property of memory in a system of oblivious mobile robots, and why it is not a problem for luminous rendezvous algorithms.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper presents the first application of model checking (via SPIN) to verify correctness of rendezvous algorithms for two robots with lights operating in continuous Euclidean space. It introduces a generic finite-state verification model, justifies the modeling choices (continuous-position abstraction and ASYNC scheduler encoding) via explicitly proved theorems, and performs a sanity-check validation by checking multiple known algorithms against six synchrony models; the model-checker outputs match published results, including counter-example traces for all known failing cases. Additional theorems on emergent memory properties in ASYNC luminous systems are identified during the modeling process.

Significance. If the modeling theorems hold, the work is significant as the first demonstration that finite-state model checking can faithfully reproduce known outcomes for continuous-space luminous robot algorithms, including both positive and negative results. The explicit supporting lemmas, direct consistency checks against independently published algorithms, and counter-example generation provide a reproducible verification artifact that could reduce reliance on complex manual proofs for similar problems. The identification of the ASYNC memory-emergence theorem is an additional contribution.

minor comments (2)
  1. [Abstract] The abstract and introduction would benefit from an explicit statement of the precise synchrony models covered (e.g., which variants of SSYNC and ASYNC are encoded) rather than referring only to 'six different models'.
  2. [§3] Notation for robot states and light colors is introduced without a consolidated table; a small summary table in §3 or §4 would improve readability when cross-referencing the SPIN model.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive review, accurate summary of the contributions, and recommendation to accept. No major comments were raised.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper's core contribution is a finite-state SPIN encoding of luminous rendezvous algorithms together with supporting lemmas on continuous-position abstraction and ASYNC scheduler modeling. Validation consists of direct consistency checks against independently published algorithms and known correctness/failure outcomes from the literature, including reproduction of counter-example traces. No parameter fitting, self-definitional renaming of results, or load-bearing self-citation chains appear in the derivation; the modeling theorems are presented as internal justification for the abstraction rather than as the source of the verified claims themselves. The work therefore remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on standard model-checking assumptions (finite-state abstraction of continuous space) plus paper-specific theorems that justify the abstraction; no free parameters or invented physical entities are introduced.

axioms (1)
  • domain assumption A well-chosen algorithm and ASYNC scheduler can produce an emerging memory property in oblivious robots, yet this does not break luminous rendezvous correctness.
    Identified during model development and stated as a fundamental theorem supporting the verification approach.

pith-pipeline@v0.9.0 · 5818 in / 1156 out tokens · 17806 ms · 2026-05-24T17:01:24.187656+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

41 extracted references · 41 canonical work pages

  1. [1]

    Fault-tolerant gathering algorithms for autonomous mobile robots

    Noa Agmon and David Peleg. Fault-tolerant gathering algorithms for autonomous mobile robots. SIAM J. Comput., 36(1):56–82, 2006

    work page 2006

  2. [2]

    Distributed memoryless point convergence algorithm for mobile robots with limited visibility

    Hideki Ando, Yoshinobu Oasa, Ichiro Suzuki, and Masafumi Yamashita. Distributed memoryless point convergence algorithm for mobile robots with limited visibility. IEEE Trans. Robotics and Automation , 15(5):818–828, 1999

    work page 1999

  3. [3]

    Certified impossibility results for byzantine-tolerant mobile robots

    C´edric Auger, Zohir Bouzid, Pierre Courtieu, S´ebastien Tixeuil, and Xavier Urbain. Certified impossibility results for byzantine-tolerant mobile robots. In Proc. 15th Intl. Symp. on Stabilization, Safety, and Security of Distributed Systems (SSS), pages 178–190, November 2013

    work page 2013

  4. [4]

    Brief announcement: Continuous vs

    Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, S´ebastien Tixeuil, and Xavier Urbain. Brief announcement: Continuous vs. discrete asynchronous moves: A certified approach for mobile robots. In Proc. 20th Intl. Symp. on Stabilization, Safety, and Security of Distributed Systems (SSS), pages 404–408, November 2018

    work page 2018

  5. [5]

    A foundational framework for certified impossibility results with mobile robots on graphs

    Thibaut Balabonski, Robin Pelle, Lionel Rieg, and S´ebastien Tixeuil. A foundational framework for certified impossibility results with mobile robots on graphs. In Proc. 19th intl. Conf. on Distributed Computing and Networking, (ICDCN), pages 5:1–5:10, January 2018

    work page 2018

  6. [6]

    [Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems

    B´eatrice B ´erard, Pierre Courtieu, Laure Millet, Maria Potop-Butucaru, Lionel Rieg, Nathalie Sznajder, S´ebastien Tixeuil, and Xavier Urbain. [Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems. International Journal of Informatics Society, 7(3):101–114, 2015

    work page 2015

  7. [7]

    Formal verification of mobile robot protocols

    B´eatrice B´erard, Pascal Lafourcade, Laure Millet, Maria Potop-Butucaru, Yann Thierry-Mieg, and S´ebastien Tixeuil. Formal verification of mobile robot protocols. Distributed Computing, 29(6):459–487, 2016

    work page 2016

  8. [8]

    Discovering and assessing fine-grained metrics in robot networks protocols

    Franc ¸ois Bonnet, Xavier D´efago, Franck Petit, Maria Potop-Butucaru, and S´ebastien Tixeuil. Discovering and assessing fine-grained metrics in robot networks protocols. InProc. 33rd IEEE Intl. Symp. on Reliable Distributed Systems Workshops, (SRDS Workshops), pages 50–59, October 2014

    work page 2014

  9. [9]

    Gathering of mobile robots tolerating multiple crash faults

    Zohir Bouzid, Shantanu Das, and S ´ebastien Tixeuil. Gathering of mobile robots tolerating multiple crash faults. In Proc. 33rd IEEE Intl. Conf. on Distributed Computing Systems (ICDCS), pages 337–346, July 2013

    work page 2013

  10. [10]

    Minimum-traveled-distance gathering of oblivious robots over given meeting points

    Serafino Cicerone, Gabriele Di Stefano, and Alfredo Navarra. Minimum-traveled-distance gathering of oblivious robots over given meeting points. In Proc. 10th Intl. Symp. on Algorithms and Experiments for Sensor Systems, Wireless Networks and Distributed Robotics, (ALGOSENSORS), Revised Selected Papers, pages 57–72, September 2014

    work page 2014

  11. [11]

    Convergence properties of the gravitational algorithm in asynchronous robot systems

    Reuven Cohen and David Peleg. Convergence properties of the gravitational algorithm in asynchronous robot systems. SIAM J. Comput., 34(6):1516–1528, 2005. 12

    work page 2005

  12. [12]

    Impossibility of gathering, a certification

    Pierre Courtieu, Lionel Rieg, S´ebastien Tixeuil, and Xavier Urbain. Impossibility of gathering, a certification. Inf. Process. Lett., 115(3):447–452, 2015

    work page 2015

  13. [13]

    Certified universal gathering in R2 for oblivious mobile robots

    Pierre Courtieu, Lionel Rieg, S ´ebastien Tixeuil, and Xavier Urbain. Certified universal gathering in R2 for oblivious mobile robots. In Proc. 30th Intl. Symp. on Distributed Computing (DISC), pages 187–200, September 2016

    work page 2016

  14. [14]

    Autonomous mobile robots with lights

    Shantanu Das, Paola Flocchini, Giuseppe Prencipe, Nicola Santoro, and Masafumi Yamashita. Autonomous mobile robots with lights. Theor. Comput. Sci., 609:171–184, 2016

    work page 2016

  15. [15]

    Fault-tolerant and self- stabilizing mobile robots gathering

    Xavier D´efago, Maria Gradinariu, St´ephane Messika, and Philippe Raipin Parv´edy. Fault-tolerant and self- stabilizing mobile robots gathering. In Proc. 20th Intl. Symp. on Distributed Computing (DISC), pages 46–60, September 2006

    work page 2006

  16. [16]

    Optimal grid exploration by asynchronous oblivious robots

    St´ephane Devismes, Anissa Lamani, Franck Petit, Pascal Raymond, and S ´ebastien Tixeuil. Optimal grid exploration by asynchronous oblivious robots. In Proc. 14th Intl. Symp. on Stabilization, Safety, and Security of Distributed Systems (SSS), pages 64–76, October 2012

    work page 2012

  17. [17]

    Model checking of a mobile robots perpetual exploration algorithm

    Ha Thi Thu Doan, Fran c ¸ois Bonnet, and Kazuhiro Ogata. Model checking of a mobile robots perpetual exploration algorithm. In Proc. 6th Intl. Workshop on Structured Object-Oriented Formal Language and Method (SOFL+MSVL), Revised Selected Papers, pages 201–219, November 2016

    work page 2016

  18. [18]

    Model checking of robot gathering

    Ha Thi Thu Doan, Franc ¸ois Bonnet, and Kazuhiro Ogata. Model checking of robot gathering. In Proc. 21st Intl. Conf. on Principles of Distributed Systems, (OPODIS), pages 12:1–12:16, December 2017

    work page 2017

  19. [19]

    Distributed Computing by Mobile Entities- Current Research in Moving and Computing

    Paola Flocchini, Giuseppe Prencipe, and Nicola Santoro (Eds.). Distributed Computing by Mobile Entities- Current Research in Moving and Computing. Lecture Notes in Computer Science, 11340. Springer, 2019

    work page 2019

  20. [20]

    Distributed Computing by Oblivious Mobile Robots

    Paola Flocchini, Giuseppe Prencipe, and Nicola Santoro. Distributed Computing by Oblivious Mobile Robots. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2012

    work page 2012

  21. [21]

    Gathering of asynchronous robots with limited visibility

    Paola Flocchini, Giuseppe Prencipe, Nicola Santoro, and Peter Widmayer. Gathering of asynchronous robots with limited visibility. Theor. Comput. Sci., 337(1-3):147–168, 2005

    work page 2005

  22. [22]

    Rendezvous with constant memory

    Paola Flocchini, Nicola Santoro, Giovanni Viglietta, and Masafumi Yamashita. Rendezvous with constant memory. Theor. Comput. Sci., 621:57–72, 2016

    work page 2016

  23. [23]

    Optimally gathering two robots

    Adam Heriban, Xavier D´efago, and S´ebastien Tixeuil. Optimally gathering two robots. In Proc. 19th Intl. Conf. on Distributed Computing and Networking, ICDCN, pages 3:1–3:10, January 2018

    work page 2018

  24. [24]

    The gathering problem for two oblivious robots with unreliable compasses

    Taisuke Izumi, Samia Souissi, Yoshiaki Katayama, Nobuhiro Inuzuka, Xavier D´efago, Koichi Wada, and Masafumi Yamashita. The gathering problem for two oblivious robots with unreliable compasses. SIAM J. Comput., 41(1):26–46, 2012

    work page 2012

  25. [25]

    On the synthesis of mobile robots algorithms: The case of ring gathering

    Laure Millet, Maria Potop-Butucaru, Nathalie Sznajder, and S´ebastien Tixeuil. On the synthesis of mobile robots algorithms: The case of ring gathering. In Proc. 16th Intl. Symp. on Stabilization, Safety, and Security of Distributed Systems (SSS), pages 237–251, September 2014

    work page 2014

  26. [26]

    Optimal rendezvous L -algorithms for asynchronous mobile robots with external-lights

    Takashi Okumura, Koichi Wada, and Xavier D´efago. Optimal rendezvous L -algorithms for asynchronous mobile robots with external-lights. In Proc. 22nd Intl. Conf. on Principles of Distributed Systems (OPODIS), pages 24:1–16, December 2018

    work page 2018

  27. [27]

    Brief announcement: Optimal asynchronous rendezvous for mobile robots with lights

    Takashi Okumura, Koichi Wada, and Yoshiaki Katayama. Brief announcement: Optimal asynchronous rendezvous for mobile robots with lights. In Proc. 19th Intl. Symp. on Stabilization, Safety, and Security of Distributed Systems (SSS), pages 484–488, November 2017

    work page 2017

  28. [28]

    Rendezvous of asynchronous mobile robots with lights

    Takashi Okumura, Koichi Wada, and Yoshiaki Katayama. Rendezvous of asynchronous mobile robots with lights. In Adventures Between Lower Bounds and Higher Altitudes - Essays Dedicated to Juraj Hromkoviˇc on the Occasion of His 60th Birthday, pages 434–448, 2018

    work page 2018

  29. [29]

    Formal methods for mobile robots

    Maria Potop-Butucaru, Nathalie Sznajder, S´ebastien Tixeuil, and Xavier Urbain. Formal methods for mobile robots. In Paola Flocchini, Giuseppe Prencipe, and Nicola Santoro, editors, Distributed Computing by Mobile Entities, Current Research in Moving and Computing., volume 11340 of LNCS, pages 278–313. Springer, 2019

    work page 2019

  30. [30]

    Verification of asynchronous mobile- robots in partially-known environments

    Sasha Rubin, Florian Zuleger, Aniello Murano, and Benjamin Aminof. Verification of asynchronous mobile- robots in partially-known environments. In Proc. 18th Intl. Conf. on Principles and Practice of Multi-Agent Systems (PRIMA), pages 185–200, October 2015. 13

    work page 2015

  31. [31]

    Parameterized verification of algorithms for oblivious robots on a ring

    Arnaud Sangnier, Nathalie Sznajder, Maria Potop-Butucaru, and S´ebastien Tixeuil. Parameterized verification of algorithms for oblivious robots on a ring. In Daryl Stewart and Georg Weissenbacher, editors, 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017 , pages 212–219. IEEE, 2017

    work page 2017

  32. [32]

    Using eventually consistent compasses to gather memory-less mobile robots with limited visibility

    Samia Souissi, Xavier D´efago, and Masafumi Yamashita. Using eventually consistent compasses to gather memory-less mobile robots with limited visibility. TAAS, 4(1):9:1–9:27, 2009

    work page 2009

  33. [33]

    Distributed anonymous mobile robots: Formation of geometric patterns

    Ichiro Suzuki and Masafumi Yamashita. Distributed anonymous mobile robots: Formation of geometric patterns. SIAM J. Comput., 28(4):1347–1363, 1999

    work page 1999

  34. [34]

    Rendezvous of two robots with visible bits

    Giovanni Viglietta. Rendezvous of two robots with visible bits. In Proc. 9th Intl. Symp. on Algorithms and Experiments for Sensor Systems, Wireless Networks and Distributed Robotics, (ALGOSENSORS) , pages 291–306, September 2013. 14 A Appendix A.1 Reminder: Robot System Model An execution of robot r is defined as a possibly infinite sequence of activation c...

    work page 2013

  35. [35]

    That the rigid algorithm achieves rendezvous

    work page

  36. [36]

    That the farthest non-rigid algorithm leads to the closest

    work page

  37. [37]

    The first point is proven in the rigid part of the paper

    That the closest non-rigid algorithm leads to the rigid. The first point is proven in the rigid part of the paper. We now only need to prove the second and third points. This is easily done by remembering that any algorithm using only the three moves either allows static executions or not. If it does, then the distance is never reduced, and checking at 3δ ...

    work page

  38. [38]

    Since the same piece of information is being read and written at the same time, the result of the read operation cannot be determined

    In the first case, one event (E1) is a read operation (LOOK), and one event (E2) is a write operation (COMPUTE ). Since the same piece of information is being read and written at the same time, the result of the read operation cannot be determined. In the case of mobile robots, where the write operation is a color transition from color c1 to color c2, we a...

    work page

  39. [39]

    ■ Proof: Theorem 10

    In any other case, since no read and write operation are happening at the same time, activating E1 and E2 simultaneously is identical to activating either E1 then E2, or E2 then E1. ■ Proof: Theorem 10. To properly limit the number of activations of the scheduler, we need to ensure that any change in the configuration made byA that may impact the snapshot ...

    work page

  40. [40]

    In the first branch, the robot reaches NEAR and we continue the process

    work page

  41. [41]

    We increment the counter by 1

    In the second branch, the robot actually did not reach NEAR and is kept at FAR. We increment the counter by 1. We repeat this process until the counter reaches Ncon f− 1. We have then created 2Ncon f− 1 branches to verify. However, we have ensured that any possible rigid motion behavior configurations has been checked. Repeating this process for every poss...

    work page 2018