# \(k\)-Circle Formation and \(k\)-epf by Asynchronous Robots
## 4 Algorithm
### Moveto Destination
This implies that for each \(i\in\{j,a\}\), \(V_{i}(t)\) is updated only due to the movement of \(f_{i}\)'s candidate robot. Without loss of generality, suppose candidate robot \(r_{i}\) of the target fixed point \(f_{j}\) has completed its LCM cycle. By Lemma 4, \(d_{j}(t^{\prime})+\delta\leq d_{j}(t)\) is ensured. Lemma 9: _Let \(C(t)\) admit two target fixed points during an execution of \(AlgorithmOneAxis(C(t))\) and \(t^{\prime}>t\) be an arbitrary point of time when at least one candidate robot has completed its LCM cycle. Execution of \(AlgorithmOneAxis(C(t))\) ensures significant progress._

Proof of Lemma 9.: Lemma 8 ensures that for at least one target fixed point \(f_{i}\in\{f_{j},f_{a}\}\) and its candidate robot, \(d_{i}(t^{\prime})+\delta\leq d_{i}(t)\) holds. Without loss of generality, assume that for the target fixed point \(f_{j}\) we have \(d_{j}(t^{\prime})+\delta\leq d_{j}(t)\) in the time interval \(t\) to \(t^{\prime}\). By Lemma 5, we have \(V_{j}(t^{\prime})<V_{j}(t)\), i.e., significant progress is ensured. Theorem 2: _If the initial configuration \(C(0)\in\{\mathcal{I}_{1}\cup\mathcal{I}_{2}\cup\mathcal{I}_{3}\cup\mathcal{I}_ {4}\cup\mathcal{I}_{5}\}\) and \(C(0)\) does not satisfy the unsolvability criterion stated in Theorem 1, then the robots would eventually solve the \(k\)-circle formation problem under one axis agreement, by the execution of \(AlgorithmOneAxis\)._

Proof of Theorem 2.: Lemma 3 guarantees that for any \(t>0\), the configuration \(C(t)\) would not satisfy the unsolvability criterion stated in Theorem 1. We have the following cases:

Case 1.: There is a unique target fixed point (say \(f_{j}\)) in the configuration. Lemma 5 ensures that each time a candidate robot gets activated, significant progress is ensured. If there is a unique candidate robot for \(f_{j}\), then Lemma 6 guarantees that until the candidate robot reaches its destination, it would remain the candidate robot. In case there are two candidate robots for \(f_{j}\), then Lemma 7 guarantees that until one of the candidate robots reaches its destination point, no other robot will become a candidate robot. As a result, one of the candidate robots will reach its destination point eventually. If the other candidate robot does not reach its destination point, then it becomes a candidate robot for \(f_{j}\) when \(N_{j}(t)\) reduces by one. Thus, the circle formation process around all the fixed points will be completed eventually. Case 2.: There are two target fixed points. Note that the target fixed points lie in different half-planes delimited by the \(y\)-axis. Lemma 9 ensures significant progress. Lemma 6 guarantees that until a candidate robot reaches its destination, it remains the candidate robot. Note that in this case for each of the target fixed points, always a unique candidate robot gets selected. Thus, the circle formation process around all the fixed points will be completed eventually. Hence, the robots would eventually solve the \(k\)-circle formation problem with one axis agreement. From Theorem 2, it follows that the robots would solve the \(k\)-circle formation problem under one axis agreement within finite time. Since we have considered the scheduler to be asynchronous, the robots do not have any common notion of time. As a result, the actual time to solve the \(k\)-circle formation problem depends upon the scheduling of the robots. We use the notion of an epoch [30] to discuss the runtime complexity of our proposed algorithm. An epoch is the time interval in which all the robots in the configuration have performed their LCM cycles at least once. According to this definition, the time is divided into global epochs. We also assume that the robots have rigid motion, i.e., the robot is guaranteed to reach its destination whenever it moves. In such a setting, we have the following observations:

1. If a candidate robot does not have to pass through a saturated circle in order to reach the circle centered at its target fixed point, then it would reach the circle within one epoch. 2.