\subsubsection{Proof of Correctness}

Without loss of generality, let $L$ be the size of the border that is connected to the Door corner by an edge with a maximal port number among two edges of the Door corner.
Let $l$ be the other size of the border.
We call the $L$-size border connected to the Door corner ``the first border", and the $l$-size border not-connected to the Door corner ``the second border", like Fig.~\ref{fig:st1}(b).
Additionally, we call the second border \emph{0-line}, and count the lines in the following way: the line that is adjacent and parallel to 0-line is \emph{1-line}, and the border that is connected to the Door corner but not the first border is \emph{$(L-1)$-line}.

First, we show that robots cannot collide.
\begin{lemma}\label{collide}
Robots cannot collide when executing Algorithm 1.
\end{lemma}
\begin{proof}
If there exists an outdated robot $r_o$ that is to move using its outdated view, the outdated view is one of the types in ${\cal D}$, ${\cal C}$, ${\cal M}_1$, or ${\cal M}_2$ by the definition of the algorithm.
Thus, if a collision with $r_o$ occurs, then $r_o$'s view is one of the types in ${\cal D}$, ${\cal C}$, ${\cal M}_1$, or ${\cal M}_2$.
In that case, because a Finished robot does not move forever, a non-Finished robot in $r_o$'s view may have moved,
or other non-Finished robot came into the visible region of $r_o$.

On the Door corner, if a robot $r_i$ cannot see other robots, then its view is {\sf StartP1} in ${\cal M}_1$.
Then, because $r_i$ has $c(r_i)=p_1$ initially, its view becomes {\sf MovP1} in ${\cal M}_1$.
By the definition of {\sf MovP1}, $r_i$ moves only on the first border according to the degree of nodes until it arrives at the end of the first border, or it can see Finished robots.
Then, the first border is one-way because each robot can recognize its previous node.
Additionally, if $r_i$ can see other non-Finished robots than its successor, then $r_i$ cannot move because there is no such rule.
That is, $r_i$ keeps the distance from its predecessor (if it exists) two or more hops on the first border.
Thus, on the first border (while $c(r_i)=p_1$), if $r_i$ has an outdated view in ${\cal D}$, ${\cal C}$, or ${\cal M}_1$, the current configuration can be the same view type as its outdated view, because only $r_i$'s successor is allowed to move toward $r_i$.
Thus, $r_i$ cannot collide with other robots while $c(r_i)=p_1$.

Consider when $r_i$ arrives at the end of the first border, or can see Finished robots.
\begin{itemize}
\item If ${\it view}(r_i)$ becomes {\sf P1Stop} or {\sf OnCP1F} in ${\cal F}_1$, then $r_i$ changes its color to $F$ by Rule 1.
\item If ${\it view}(r_i)$ becomes {\sf OnCP1} in ${\cal C}$, then $r_i$ changes its color to $p_2$, and moves to the second border by Rule 2.
After that, ${\it view}(r_i)$ becomes {\sf MovP2} in ${\cal M}_2$ until it arrives at the diagonal corner (\emph{i.e.}, {\sf OnCP2} in ${\cal F}_2$), or it can see Finished robots on the second border (\emph{i.e.}, {\sf P2Stop} in ${\cal F}_2$).
By the definition of {\sf MovP2}, each robot moves on the second border according to the degree of nodes, and the second border is one-way.
By the definition of the algorithm, there is no rule to make $r_i$ stray from the second border.
Then, $r_i$ keeps the distance from its predecessor (if it exists) two or more hops on the second border.
\item If ${\it view}(r_i)$ becomes {\sf GoCo} in ${\cal M}_1$, then $r_i$ moves to the adjacent node occupied by a Finished robot on the first border and ${\it view}(r_i)$ becomes {\sf ColP1A} in ${\cal C}$.
\item If ${\it view}(r_i)$ becomes {\sf ColP1A} or {\sf ColP1B} in ${\cal C}$, then $r_i$ changes its color to $p_2$, and moves to one of the lines. Without loss of generality, let the line be $m$-line where $m>0$.
Then, robots on $(m-1)$-line are Finished and $(m+1)$-line is empty (if it exists on the grid) by the definition of {\sf ColP1A} or {\sf ColP1B}.
Thus, after that, ${\it view}(r_i)$ becomes {\sf MovP2A} or {\sf MovP2B} in ${\cal M}_2$ until it arrives at the end of $m$-line (\emph{i.e.}, {\sf P2StopA} or {\sf P2StopB} in ${\cal F}_2$), or it can see a Finished robot on $m$-line (\emph{i.e.}, {\sf P2StopC} in ${\cal F}_2$).
By the definition of the algorithm, there is no rule to make $r_i$ stray from $m$-line.
By the definitions of {\sf MovP2A} and {\sf MovP2B}, $m$-line is also one-way, and $r_i$ keeps the distance from its predecessor (if it exists on the line) two or more hops.
\end{itemize}
In any case, on each line (while $c(r_i)=p_2$), if $r_i$ has an outdated view in ${\cal C}$ or ${\cal M}_2$, then the current configuration is the same view type as its outdated view, because only $r_i$'s successor is allowed to move toward $r_i$.
Thus, $r_i$ cannot collide with other robots while $c(r_i)=p_2$.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

Next, we show that Algorithm 1 constructs a maximum independent set.
\begin{lemma}\label{1st}
The first robot $r_1$ moves to the diagonal corner, and $c(r_1)$ becomes $F$ on the corner.
\end{lemma}
\begin{proof}
When the first robot $r_1$ is in the Door node, then its view is {\sf Door1} in ${\cal D}$.
Thus, it moves to the Door corner by ${\it Enter\_Grid}(r_1)$, and its view becomes {\sf StartP1} in ${\cal M}_1$.
Then, $r_1$ moves to the adjacent node through the edge with the maximal port number by Rule 3.
Then, because it is the first robot, its view becomes {\sf MovP1} in ${\cal M}_1$ and moves to the adjacent node on the first border by Rule 3.

By the proof of Lemma~\ref{collide}, the first border and second border are one-way, and any other robots cannot pass $r_1$ on these borders.
Thus, ${\it view}(r_1)$ remains {\sf MovP1}, and $r_1$ moves on the first border according to the node degree.
Therefore, $r_1$ arrives at the end of the first border eventually, and then ${\it view}(r_1)$ becomes {\sf OnCP1} in ${\cal C}$.
After that, by Rule 2, $r_1$ changes its color to $p_2$ and moves to the adjacent node on the second border.
${\it view}(r_1)$ becomes {\sf MovP2} in ${\cal M}_2$, $r_1$ moves towards the next (diagonal) corner through the second border according to the node degree by Rule 5, eventually ${\it view}(r_1)$ becomes {\sf OnCP2} in ${\cal F}_2$.
By Rule 4, because $c(r_1)=p_2$, $r_1$ changes its color to $F$ on the corner.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{1stB}
The first $\lceil l/2 \rceil$ robots move to the second border, and their color becomes $F$.
Additionally, nodes on the second border are occupied by a robot or empty alternately from the diagonal corner.
\end{lemma}
\begin{proof}
By Lemma~\ref{1st}, the first robot $r_1$ eventually becomes Finished on the diagonal corner.

First, we consider the second robot $r_2$, which follows $r_1$ in the case that $l>3$.
By the assumption, $r_2$ appears to the Door node just after $r_1$ enters into the grid.
Because $r_1$ does not become Finished before it arrives at the diagonal corner, $r_2$ can move from the Door node only when ${\it view}(r_2)={\sf Door1}$ in ${\cal D}$ holds.
After that, by the definition of the algorithm, $r_2$ moves in the same way as $r_1$, $c(r_2)$ becomes $p_2$ on the end of the first border eventually and $r_2$ moves on the second border.
Finally, $r_2$ can see $r_1$ on the diagonal corner two hops away.
Then, there is no rule such that $r_2$ executes before $c(r_1)$ becomes $F$.
Because of Lemma~\ref{1st}, ${\it view}(r_2)$ eventually becomes {\sf P2Stop} in ${\cal F}_2$.
Then, by Rule 4, $c(r_2)$ becomes $F$.

In the case that $l=3$, when $r_2$ arrives at the end of the first border, ${\it view}(r_2)$ becomes {\sf OnCP1F} in ${\cal F}_1$ and $c(r_2)$ becomes $F$ by Rule 1.
Note that, in any case, the distance between $r_1$ and $r_2$ is two hops when they are Finished.

For the successors of $r_2$, we can discuss their movements in the same way as $r_2$.
Thus, by the definitions of {\sf OnCP1F} and {\sf P2Stop},
the distance between a robot and its successor is two hops when they are Finished on the second border.
Therefore, on the second border, beginning with the diagonal corner, every even node is occupied, and the number of robots is $\lceil l/2 \rceil$.
If $l$ is odd, when the $\lceil l/2 \rceil$-th robot arrives at the end of the first border, its view becomes {\sf OnCP1F} and it changes its color to $F$ by Rule 1.
Otherwise, it changes its color to $p_2$ and moves to the second border.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{1-line}
From the $(\lceil l/2 \rceil+1)$-th to the $l$-th robots, each robot moves to the $1$-line, and its color becomes $F$.
Additionally, nodes on the $1$-line are empty or occupied by a robot alternately, beginning with an empty node.
\end{lemma}
\begin{proof}
By Lemma~\ref{1stB}, $\lceil l/2 \rceil$ robots on $0$-line eventually become Finished.
Let $r_i$ be the $(\lceil l/2 \rceil+1)$-th robot, $r_j$ be the $(\lceil l/2 \rceil)$-th robot that is the predecessor of $r_i$.
$r_i$ moves from the Door node in the same way as $r_j$ while $c(r_i)=p_1$.
Because robots on $0$-line become Finished eventually, one of the following two
cases occurs: \emph{(1)} if $l$ is odd, ${\it view}(r_i)$ becomes {\sf GoCo} in ${\cal M}_1$, because the end of the first border is occupied by $r_j$, or \emph{(2)} if $l$ is even, ${\it view}(r_i)$ becomes {\sf ColP1B} in ${\cal C}$, because the end of the first border is empty but its adjacent node on the $0$-line is occupied by $r_j$.

In case \emph{(1)}, by Rule 3, $r_i$ moves to the node in front of the end of the first border, ${\it view}(r_i)$ becomes {\sf ColP1A} in ${\cal C}$.
Then, by Rule 2, $c(r_i)$ becomes $p_2$ and $r_i$ moves to $1$-line.
After that, if $l=3$, ${\it view}(r_i)$ becomes {\sf P2StopA} in ${\cal F}_2$ and $r_i$ changes its color to $F$ by Rule 4.
Otherwise, because $r_i$ can see Finished robots on $0$-line, ${\it view}(r_i)$ becomes {\sf MovP2A} in ${\cal M}_2$.
Then, because the nodes on $0$-line are occupied alternately by Lemma~\ref{1stB}, ${\it view}(r_i)$ becomes {\sf MovP2B} and {\sf MovP2A} in ${\cal M}_2$ alternately by the execution of Rule 5.
Thus, $r_i$ moves toward the other side border that is parallel to the first border by Rule 5, and ${\it view}(r_i)$ eventually becomes {\sf P2StopA} because the diagonal corner is occupied by a Finished robot (Lemma~\ref{1st}).
Then, by Rule 4, $c(r_i)$ eventually becomes $F$.
Because $l$ is odd, $\lfloor l/2 \rfloor-1$ successors of $r_i$ follow $r_i$, and eventually, their views become {\sf P2StopC} in ${\cal F}_2$, and they change their colors to $F$ by Rule 4 on $1$-line.

In case \emph{(2)}, $r_i$ also changes its color to $p_2$, and moves to $1$-line by Rule 2.
After that, because $r_i$ can see Finished robots on $0$-line, ${\it view}(r_i)$ becomes {\sf MovP2B} in ${\cal M}_2$.
Then, in the same way as for case \emph{(1)}, $l/2-1$ robots including $r_i$ become Finished on $1$-line.
After that, the view of the next robot $r_l$ ($l$-th robot) becomes {\sf P1Stop} in ${\cal F}_1$ on the intersection between the first border and $1$-line, and $r_l$ becomes Finished by Rule 1.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{2hops}
The distance between any two robots on the grid is two hops after every robot becomes Finished.
\end{lemma}
\begin{proof}
By
the definitions of ${\cal F}_1$ and ${\cal F}_2$, the distance between a robot $r_i$ and its predecessor is two hops after $r_i$ becomes Finished if the predecessor is on the same line as $r_i$.
Thus, when the robots on $m$-line ($0<m<L-1$) become Finished, if there are two adjacent Finished robots, then there is a robot $r_r$ on $m$-line that cannot move from the node that is adjacent to a node occupied by a Finished robot on $(m-1)$-line.
However, by the same argument as in Lemmas~\ref{1stB} and \ref{1-line}, if $m$ is odd (resp. even), the nodes on $m$-line are occupied alternately beginning with an empty node (resp. occupied node) because the nodes on $(m-1)$-line are also occupied alternately beginning with an occupied node (resp. empty node).
Thus, before such $r_r$ becomes Finished, $r_r$ has a view of type {\sf MovP2B} and can move by Rule 5, i.e., it cannot exist.

Now, to consider the end of the execution of the algorithm, we consider $(L-1)$-line when nodes on $(L-2)$-line are occupied by Finished robots.
The $(L-1)$-line is a border connected to the Door node.
Then, if both $l$ and $L$ are odd or both are even, the view from the Door node becomes {\sf Door1}, otherwise {\sf Door2} (See Fig.~\ref{fig:checkers}).
\begin{itemize}
\item If the view from the Door node is {\sf Door1}, the robot on the Door node moves to the Door corner by Rule 0.
Then, the view from the Door corner is {\sf ColP1B} in ${\cal C}$.
By the above discussion, the view from the Door corner eventually becomes {\sf P1Stop} in ${\cal F}_1$, thus the final robot on the Door corner becomes Finished by Rule 1.
Then, any other robots cannot enter into the grid because there is no such rule.
\item If the view from the Door node is {\sf Door2}, the view from the Door corner is {\sf ColP1A} in ${\cal C}$.
Then, the empty node $v$ that is adjacent to the Door corner is eventually occupied by a Finished robot on $(L-1)$-line.
After that, any other robots on the Door node cannot enter into the grid because there is no such rule.
\end{itemize}
Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}
Every robot on the grid is eventually Finished.
\end{lemma}
\begin{proof}
By the proofs of Lemmas~\ref{collide}-\ref{2hops}, the transitions of the view type of each robot are shown as Fig.~\ref{fig:Alg1}.
Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{theorem}\label{1MIS}
Algorithm 1 constructs a maximum independent set of occupied locations on the grid.
\end{theorem}
\begin{proof}
By Lemma~\ref{2hops}, distances between any two occupied nodes are two. On a grid, only checkers patterns satisfy this constraint.
When at least one dimension of even, there are as many occupied locations as non-occupied locations, so any checkers pattern is a maximum independent set (see Fig.~\ref{fig:checkers}(a) and Fig.~\ref{fig:checkers}(b)). When both dimensions are odd, there may be either one more occupied locations than non-occupied locations, or the contrary (See Fig.~\ref{fig:checkers}(c)). The situation that corresponds to the maximum independent set is the one with occupied locations in the corners, which is what our algorithm constructs.
Hence, the theorem holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{figure}[t]
\centering
\subfigure[even-even dimensions]{
\centering
\includegraphics[height=.12\textheight]{eveneven}
}
\subfigure[even-odd dimensions]{
\centering
\includegraphics[height=.15\textheight]{oddeven}
}
\subfigure[odd-odd dimensions]{
\centering
\includegraphics[height=.15\textheight]{oddodd}
}
\caption{Checkers patterns in grids.}
\label{fig:checkers}
\end{figure}

\begin{figure}[t]
    \centering
    \includegraphics[width=0.57\textwidth]{Alg1-crop.pdf}
    \caption{View type transitions of Algorithm 1. Each solid arrow (resp. dotted arrow) represents a transition by a {\it Move} (resp. {\it Enter\_Grid}) operation. }
    \label{fig:Alg1}
\end{figure}

\begin{lemma}\label{number}
When a maximum independent set is constructed, $\lceil n/2 \rceil$ robots are on the grid.
\end{lemma}
\begin{proof}
By the proofs of Lemmas~\ref{1stB}--\ref{2hops}, nodes on the even-numbers (resp. odd-numbers) lines are occupied by $\lceil l/2\rceil$ (resp. $\lfloor l/2 \rfloor$) robots.
Therefore, if $L$ is even, the number of robots in the maximum independent set is $lL/2$.
If $L$ is odd, the number of robots in the maximum independent set is $l\lfloor L/2\rfloor+\lceil l/2\rceil$.
Because $n=lL$, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

To analyze the time complexity of the algorithm, we count the sum of individual executions of rules.

\begin{theorem}\label{time}
The time complexity by Algorithm 1 is $O(n(L+l))$ steps.
\end{theorem}
\begin{proof}
The first robot moves $L+l-1$ steps and becomes Finished, thus it executes $L+l$ steps.
The first robot moves the longest way.
Therefore, by Lemma~\ref{number}, the sum of the number of steps
is $O(n(L+l))$.
Thus, the theorem holds.\hfill$\Box$\par\vskip1em
\end{proof}

\subsubsection{Proof of Correctness}

Without loss of generality, let $L$ be the size of the border chosen by the first robot on the Door corner in {\sf StartP10} in ${\cal M}_1^\prime$.
Let $l$ be the other size of the border.
In the same way as Algorithm 1, we define ``the first border", ``the second border", and lines.

In the following, we first show that each robot can recognize its successor and robots cannot collide.

\begin{lemma}\label{predecessor}
Each non-Finished robot except the first robot can recognize its predecessor and successor if it keeps two neighboring non-Finished robots.
\end{lemma}
\begin{proof}
By the assumption, each robot $r_i$ initializes its $c(r_i)$ to $p_1(0)$.
The view of the first robot $r_1$ on the Door node is {\sf Door1} in ${\cal D}^\prime$, thus it moves to the Door corner with $c(r_1)=p_1(0)$ by Rule 0-2.
After that, by the assumption, its successor $r_2$ appears on the Door node with $c(r_2)=p_1(0)$.
Thus, $r_1$ cannot move until its view becomes {\sf StartP10} in ${\cal M}_1^\prime$, i.e., $r_2$ has $c(r_2)=p_1((k_1+1)\mod 3))=p_1((0+1)\mod 3)=p_1(1)$.
Thus, ${\it view}(r_2)$ on the Door node becomes {\sf Door0} and $r_2$ sets $c(r_2)$ to $p_1(1)$ by Rule 0-1.
Then, ${\it view}(r_1)$ becomes {\sf StartP10} in ${\cal M}_1^\prime$, $r_1$ selects the first border arbitrarily and moves on the border by Rule 3.

Consider a robot $r_i$ sets $c(r_i)$ to $p_1(k_i)$ on the Door node in {\sf Door0}.
Then, its predecessor $r_h$ on the Door corner has $c(k_h)$ where $k_i=(k_h+1)\mod 3$ by the definition of ${\it SetC}(r_i)$.
After $r_i$ enters the grid, on the Door corner, it cannot move until its successor $r_j$ sets $c(r_j)$ to $p_1(k_j)$ where $k_j=(k_i+1)\mod 3$ by the definitions of {\sf StartP11}, {\sf MovP13}, {\sf MovP14}, {\sf GoCo1} (in ${\cal M}_1^\prime$), {\sf ColP1A1} or {\sf ColP1B1} (in ${\cal C}^\prime$).
Therefore, each robot $r_i$ on the grid has its order modulo 3 as its value $k_i$, and the value $k_i$ is not changed after that.
Thus, if each robot keeps two neighboring non-Finished robots, it can recognize its neighboring non-Finished robot with smaller (resp. larger) $k$ value than its own as its predecessor (resp. successor), lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{3collide1}
While the light color is $p_1(k_i)$, each robot $r_i$
can recognize its successor, and cannot collide.
\end{lemma}
\begin{proof}
If there exists an outdated robot $r_o$ that is to move according to its outdated view, the view type is in ${\cal D}^\prime$, ${\cal C}^\prime$, ${\cal M}_1^\prime$, and ${\cal M}_2^\prime$ by the definition of the algorithm.
Thus, if a collision with $r_o$ occurs, then $r_o$'s view type is in ${\cal D}^\prime$, ${\cal C}^\prime$, ${\cal M}_1^\prime$, and ${\cal M}_2^\prime$.
In that case, because a Finished robot does not move forever, it could be that a non-Finished robot in $r_o$'s view moved,
or that another non-Finished robot came into the visible region of $r_o$.

The first robot $r_1$ keeps its color $c(r_1)=p_1(0)$.
On the Door node, the view of $r_1$ becomes {\sf Door1} in ${\cal D}^\prime$, and $r_1$ moves to the Door corner.
After that, $r_1$ can move only when its view becomes {\sf StartP10} in ${\cal M}_1^\prime$, i.e., $c(r_2)$ has to be set to $p_1(1)$ by ${\it SetC}(r_2)$, where $r_2$ is $r_1$'s successor.
Thus, the view of $r_2$ on the Door node becomes {\sf Door0}, and eventually $r_2$ sets its color to $p_1(1)$.
Then, $r_1$ selects one border as the first border arbitrarily in {\sf StartP10} and moves.
Because the distance from $r_2$ becomes two, ${\it view}(r_1)$ becomes {\sf MovP10} and $r_1$ moves one hop.
Then, because there is no rule to move for $r_1$ when the distance from $r_2$ is three, $r_1$ cannot move.
Thus, ${\it view}(r_2)$ becomes {\sf Door1} in ${\cal D}^\prime$ and $r_2$ enters the grid.
After that, $r_1$ can move because the distance from $r_2$ is two, i.e., {\sf MovP10} in ${\cal M}_1^\prime$ by Rule 3.
Thus, by Rule 3, $r_2$ can move from the Door corner only when ${\it view}(r_2)$ becomes {\sf StartP11} in ${\cal M}_1^\prime$.
That is, when $r_2$ can move, the distance between $r_1$ and $r_2$ is three, and $r_2$'s successor $r_3$ has $c(r_3)=p_1(2)$ by the definition of {\sf StartP11}.
By the definition of ${\cal M}_1^\prime$, they move only on the first border according to the degree of nodes until they arrive at the end of the first border.
While they move on the first border, only $r_1$ and $r_3$ are neighbors for $r_2$, and $r_3$'s successors also follow $r_3$ in the same way as $r_2$.
When the view of robots become {\sf OnCP1} in ${\cal C}^\prime$ (i.e., they arrive at the end of the first border), they change their colors from $p_1(k_i)$ to $p_2(k_i)$ in the same order as they entered the grid.

By the same argument, each robot $r_i$ moves only on the first border using the degree of nodes while $c(r_i)=p_1(k_i)$ holds, by the definition of the views in ${\cal M}_1^\prime$.
Then, on the first border, if $r_i$ is not on the Door node or the Door corner, $r_i$ can move only when the distance from its predecessor $r_h$ is three and from its successor $r_j$ is two.
That is, while $r_i$ moves on the first border, $r_j$ follows $r_i$.
Then, by the definition of the views in ${\cal M}_1^\prime$, while $r_i$ moves on the first border, there are at most two non-Finished neighboring robots $r_h$ and $r_j$ for $r_i$ and they are kept by $r_i$'s movement, i.e., robots move on the first border keeping in the order they entered the grid.
By the definition of the algorithm, only when $r_h$ becomes Finished two hops away by ${\cal F}_1^\prime$ or ${\cal F}_2^\prime$,
the number of non-Finished neighboring robots for $r_i$ becomes one, but $r_i$ keeps $r_j$ with $k_i<k_j$ in its view and recognizes $r_j$ as its successor.
By Lemma~\ref{predecessor}, on the first border, each non-Finished robot can always recognize its successor, that is, each robot can recognize its direction.
Therefore, the first border is one-way.
Thus, while $c(r_i)=p_1(k_i)$ holds, if the view is in ${\cal D}^\prime$, ${\cal C}^\prime$, or ${\cal M}_1^\prime$, $r_i$ cannot become outdated as any non-Finished robot cannot come into $r_i$'s visible region, and any non-Finished robots in $r_i$'s view cannot move.
That is, each robot cannot collide with other robots.

For each robot $r_i$, when its view becomes in ${\cal F}_1^\prime$ on the first border, $r_i$ changes its color to $F$ by Rule 1.
When its view belongs to ${\cal C}^\prime$ on the first border, $r_i$ changes its color from $p_1(k_i)$ to $p_2(k_i)$ and changes its direction to a line by Rule 2.
Thus lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{3collide2}
While the light color is $p_2(k_i)$, each robot $r_i$ can recognize its successor, and cannot collide.
\end{lemma}
\begin{proof}
Consider the time $t$ when each robot $r_i$ changes its color to $p_2(k_i)$ on the first border.
Then, its view is in ${\cal C}^\prime$ by Rule 2, and $r_i$ moves to a line.
By the proof of Lemma~\ref{3collide1} and the definition of the views in ${\cal C}^\prime$, $r_i$'s successor $r_j$ is two hops behind at $t$.
After that, by the definition of views in ${\cal M}_2^\prime$, $r_i$ can move only when the distance from $r_j$ is two and the distance from its non-Finished predecessor $r_h$ (if exists) is three.
Thus, after $r_i$ moves by the view in ${\cal M}_2^\prime$, $r_i$ cannot move unless $r_j$ moves.
\begin{itemize}
\item If ${\it view}(r_i)$ is {\sf OnCP1} at $t$, $r_i$ moves to the $0$-line (i.e., the second border) and $r_j$ also follows $r_i$.
After that, ${\it view}(r_i)$ becomes {\sf MovP2} in ${\cal M}_2^\prime$ until $r_i$ arrives at the diagonal corner (i.e., {\sf OnCP2} in ${\cal F}_2^\prime$) or $r_h$ becomes Finished on $0$-line (i.e., {\sf P2Stop} in ${\cal F}_2^\prime$).
By the definition of {\sf MovP2} in ${\cal M}_2^\prime$, $r_i$ moves on the second border according to the degree of nodes.
By the definition of the algorithm, there is no rule to make $r_i$ stray from the second border.
Then, by the definition of {\sf MovP2} in ${\cal M}_2^\prime$, $r_i$ keeps the distance from $r_j$ two or three hops and has at most two non-Finished neighboring robots, while $r_i$ moves on the second border.
By this distance, these non-Finished neighboring robots are kept by the movement.
Because robots on the second border keep the same order as when they entered the grid, only when $r_h$ becomes Finished by ${\cal F}_2^\prime$ (i.e., {\sf P2Stop} or {\sf OnCP2}), or $r_i$ is the first robot, the number of non-Finished neighboring robots for $r_i$ becomes one.
Then, $r_i$ can recognize $r_j$ as its successor, because $r_j$ is always in ${\it view}(r_i)$ and $k_i<k_j$ holds.
Thus, by Lemma~\ref{predecessor}, $r_i$ can always recognize $r_j$ as its successor, and the second border is one way.

\item If ${\it view}(r_i)$ is {\sf ColP1A0} (resp. {\sf ColP1A1}) at $t$, $r_i$ moves on a line except $0$-line and $(L-1)$-line (resp. $(L-1)$-line) and $r_j$ also follows $r_i$.
Without loss of generality, let the line be $m$-line where $m>0$.
Then, by the definition of {\sf ColP1A0} (resp. {\sf ColP1A1}), robots on $(m-1)$-line are Finished and $(m+1)$-line is empty (if it exists on the grid).
Thus, after that, because $r_j$ follows $r_i$, ${\it view}(r_i)$ becomes {\sf MovP2A} or {\sf MovP2B} in ${\cal M}_2^\prime$ until $r_i$ arrives at the end of the line (i.e., {\sf P2StopA} or {\sf P2StopB} in ${\cal F}_2^\prime$) or $r_h$ becomes Finished on $m$-line (i.e., {\sf P2StopC} in ${\cal F}_2^\prime$).
By the definition of the algorithm, there is no rule to make $r_i$ stray from $m$-line.
By the definitions of {\sf MovP2A} and {\sf MovP2B} in ${\cal M}_2^\prime$, $r_i$ keeps the distance from $r_j$ two or three hops, and has at most two non-Finished neighboring robots, while $r_i$ moves on $m$-line.
By this distance, these non-Finished neighboring robots are kept by the movement.
Because robots on $m$-line keep the same order as when they entered the grid, only when $r_h$ becomes Finished on $m$-line by ${\cal F}_2^\prime$ (i.e., {\sf P2StopA}, {\sf P2StopB} or {\sf P2StopC}), or $r_i$ is the first robot for $m$-line (i.e., $r_h$ is Finished on the intersection of the first border and $(m-1)$-line in {\sf ColP1A0} (resp. {\sf ColP1A1})), the number of non-Finished neighboring robots for $r_i$ becomes one. Then, $r_i$ also recognizes $r_j$ as its successor, because $r_j$ is always in ${\it view}(r_i)$ and $k_i<k_j$ holds.
Thus, by Lemma~\ref{predecessor}, $r_i$ can always recognize $r_j$ as its successor, and $m$-line is one way.

\item If ${\it view}(r_i)$ is {\sf ColP1B0} (resp. {\sf ColP1B1}) at $t$, $r_i$ moves on a line except $0$-line and $(L-1)$-line (resp. $(L-1)$-line) and $r_j$ also follows $r_i$.
After that, ${\it view}(r_i)$ becomes {\sf MovP2B} or {\sf MovP2A} in ${\cal M}_2^\prime$ until $r_i$ arrives at the end of the line (i.e., {\sf P2StopA} or {\sf P2StopB} in ${\cal F}_2^\prime$) or $r_h$ becomes Finished on the same line (i.e., {\sf P2StopC} in ${\cal F}_2^\prime$).
By the same discussion as above, $r_i$ can always recognize $r_j$ as its successor, and the line is one way.
\end{itemize}
Therefore, in any case, while $r_i$ has $p_2(k_i)$,
if the view is in ${\cal C}^\prime$ or ${\cal M}_2^\prime$, then $r_i$ cannot become outdated as any non-Finished robots cannot come into $r_i$'s visible region, and any non-Finished robots in $r_i$'s view cannot move.
Thus, $r_i$ cannot collide with other robots while $r_i$ has $p_2(k_i)$, and the lemma holds. \hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{predecessor2}
Each non-Finished robot can recognize its successor.
\end{lemma}
\begin{proof}
By Lemma~\ref{3collide1} (resp. Lemma~\ref{3collide2}), each non-Finished robot $r_i$ can always recognize its successor while $c(r_i)=p_1(k_i)$ (resp. $c(r_i)=p_2(k_i)$) holds.
Thus, the lemma holds.
\hfill$\Box$\par\vskip1em\end{proof}

\begin{lemma}\label{3collide}
Robots cannot collide when executing Algorithm 2.
\end{lemma}
\begin{proof}
By Lemma~\ref{3collide1} (resp. Lemma~\ref{3collide2}), while the light color is $p_1(k_i)$ (resp. $p_2(k_i)$), robots cannot collide.
Because each robot cannot move after it becomes Finished, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

Next, we show that Algorithm 2 constructs a maximum independent set.

\begin{lemma}\label{31st}
The first robot $r_1$ moves to the diagonal corner, and $c(r_1)$ becomes $F$ on the corner.
\end{lemma}
\begin{proof}
By the proofs of Lemmas~\ref{3collide1} and \ref{3collide2}, while robots move on the grid, they keep the order they entered the grid.

By the proof of Lemma~\ref{3collide1}, $r_1$ eventually arrives at the end of the first border, and then
$r_1$'s successor $r_2$ is on the node three hops behind.
When the distance between $r_1$ and $r_2$ becomes two, then ${\it view}(r_1)$ becomes {\sf OnCP1} in ${\cal C}^\prime$.

After that, by the proof of Lemma~\ref{3collide2}, $r_1$ eventually arrives at the diagonal corner because $r_1$ is the first robot.
When the distance between $r_1$ and $r_2$ becomes two, ${\it view}(r_1)$ becomes {\sf OnCP2} in ${\cal F}_2^\prime$.
By Rule 4, because $c(r_1)=p_2(k_1)$, it changes its color to $F$ on the corner.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{31stB}
The first $\lceil l/2 \rceil$ robots move to the second border, and their colors become $F$.
Additionally, nodes on the second border are empty or occupied by a robot alternately from the diagonal corner.
\end{lemma}
\begin{proof}
By Lemma~\ref{31st}, the first robot $r_1$ eventually becomes Finished on the diagonal corner.
Then, by the definition of {\sf OnCP2} in ${\cal F}_2^\prime$ for $r_1$, the distance between $r_1$ and its successor $r_2$ is two.

Consider the execution of $r_2$ after $c(r_1)$ becomes $F$.
If $l$ is more than three, ${\it view}(r_2)$ becomes {\sf P2Stop} in ${\cal F}_2^\prime$ when the distance between $r_2$ and its successor $r_3$ becomes two.
Then, by Rule 4, $c(r_2)$ becomes $F$.
If $l$ is three, then $r_2$ is at the end of the first border, thus ${\it view}(r_2)$ becomes {\sf OnCP1F} in ${\cal F}_1^\prime$ when the distance between $r_2$ and $r_3$ becomes two.
Then, $c(r_2)$ becomes $F$ by Rule 1.
Note that, in both cases, the distance between $r_1$ and $r_2$ remains two hops.

For the successors of $r_2$, we can discuss their movements in the same way as $r_2$.
By the definitions of {\sf OnCP1F} in ${\cal F}_1^\prime$ and {\sf P2Stop} in ${\cal F}_2^\prime$, when robots become $F$ on the second border, the distance between a robot and its successor is two hops because there is no rule to move to the adjacent node of the occupied node on the border.
Therefore, on the second border, beginning with the diagonal corner, every even node is occupied, and the number of robots is $\lceil l/2 \rceil$.
If $l$ is odd, when the $\lceil l/2 \rceil$-th robot $r_i$ arrives at the end of the first border and the distance between $r_i$ and its successor becomes two, $r_i$'s view becomes {\sf OnCP1F} in ${\cal F}_1^\prime$ and $r_i$ changes its color to $F$ by Rule 1.
Otherwise, $r_i$ changes its color to $p_2(k_i)$ and moves to the second border.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{31-line}
From the $(\lceil l/2 \rceil+1)$-th to the $l$-th robots, each robot moves to the $1$-line, and its color becomes $F$.
Additionally, nodes on the $1$-line are empty or occupied by a robot alternately, beginning with an empty node.
\end{lemma}
\begin{proof}
By Lemma~\ref{31stB}, $\lceil l/2 \rceil$ robots on $0$-line eventually become Finished.
By the definitions of ${\cal F}_1^\prime$ and ${\cal F}_2^\prime$, except on the Door corner, each robot can change its color to $F$ only when the distance from its successor is two.

Let $r_i$ be the $(\lceil l/2 \rceil+1)$-th robot, $r_h$ be the $(\lceil l/2 \rceil)$-th robot (i.e., $r_h$ is the predecessor of $r_i$), and $r_j$ be the $(\lceil l/2 \rceil+2)$-th robot (i.e., $r_j$ is the successor of $r_i$).
$r_i$ and $r_j$ move from the Door node in the same way as $r_h$ while $c(r_h)\neq F$.
Because robots on $0$-line (including $r_h$) become Finished eventually and then the distance between $r_i$ and $r_h$ is two, one of the following two cases occurs: When the distance between $r_i$ and $r_j$ becomes two, \emph{(1)} if $l$ is odd, ${\it view}(r_i)$ becomes {\sf GoCo0} or {\sf GoCo1} in ${\cal M}_1^\prime$, because the end of the first border is occupied by $r_h$, or \emph{(2)} if $l$ is even, ${\it view}(r_i)$ becomes {\sf ColP1B0}, because the end of the first border is empty but its adjacent node on the second border is occupied by $r_h$.

In case \emph{(1)}, by Rule 3, $r_i$ moves to the node in front of the end of the first border.
Then, after $r_j$ comes to the node two hops behind by {\sf MovP10}, ${\it view}(r_i)$ becomes {\sf ColP1A0} in ${\cal C}^\prime$.
Then, by Rule 2, $c(r_i)$ becomes $p_2(k_i)$ and $r_i$ moves to $1$-line.
After that, when $r_j$ comes to the node two hops away from $r_i$ by {\sf MovP11}, if $l=3$, ${\it view}(r_i)$ becomes {\sf P2StopA} in ${\cal F}_2^\prime$ and $r_i$ changes its color to $F$ by Rule 4.
Otherwise, because $r_i$ can see Finished robots on $0$-line, ${\it view}(r_i)$ becomes {\sf MovP2A} in ${\cal M}_2^\prime$.
Then, because the nodes on $0$-line are occupied alternately, ${\it view}(r_i)$ becomes {\sf MovP2B} and {\sf MovP2A} (in ${\cal M}_2^\prime$) alternately by the execution of Rule 5.
Thus, $r_i$ moves toward the other side border that is parallel to the first border by Rule 5 and $r_j$ follows $r_i$.
Finally, ${\it view}(r_i)$ eventually becomes {\sf P2StopA} in ${\cal F}_2^\prime$ because the diagonal corner is occupied by a Finished robot (Lemma~\ref{31st}).
Then, by Rule 4, $c(r_i)$ eventually becomes $F$.
Because $l$ is odd, $\lfloor l/2 \rfloor-1$ successors of $r_i$ follow $r_i$, and eventually their views become {\sf P2StopC} in ${\cal F}_2^\prime$, and they change their colors to $F$ by Rule 4 on $1$-line.

In case \emph{(2)}, $r_i$ also changes its color to $p_2(k_i)$, and moves to $1$-line by Rule 2.
After that, because $r_i$ can see Finished robots on $0$-line, ${\it view}(r_i)$ becomes {\sf MovP2B} in ${\cal M}_2^\prime$.
Then, in the same way as for case \emph{(1)}, $l/2-1$ robots including $r_i$ become Finished on $1$-line.
After that, the view of the next robot $r_l$ ($l$-th robot) becomes {\sf P1Stop1} in ${\cal F}_1^\prime$ on the intersection of the first border and $1$-line, and $r_l$ becomes Finished by Rule 1.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{32hops}
The distance between any two robots on the grid is two hops after every robot becomes Finished.
\end{lemma}
\begin{proof}
By the definitions of ${\cal F}_1^\prime$ and ${\cal F}_2^\prime$, the distance between a robot $r_i$ and its predecessor $r_j$ is two hops after each robot becomes Finished if $r_i$ and $r_j$ are on the same line.
Thus, when the robots on $m$-line ($0<m<L-1$) become Finished, if there are two adjacent Finished robots to the contrary, then there is a robot $r_r$ on $m$-line that cannot move from the node that is adjacent to a node occupied by a Finished robot on $(m-1)$-line.
However, by the same argument as in Lemmas~\ref{31stB} and \ref{31-line}, if $m$ is odd (resp. even), the nodes on $m$-line are occupied alternately beginning with an empty node (resp. occupied node) because the nodes on $(m-1)$-line are also occupied alternately beginning with an occupied node (resp. empty node).
Thus, before such $r_r$ becomes Finished, $r_r$ has a view of type {\sf MovP2B} and can move by Rule 5, i.e., such $r_r$ cannot exist.

Now, to consider the end of the execution of the algorithm, we consider $(L-1)$-line when nodes on $(L-2)$-line are occupied by Finished robots.
The $(L-1)$-line is a border connected to the Door corner.
Then, if both $l$ and $L$ are odd or both are even, the view from the Door node becomes {\sf Door4} or {\sf Door3}, otherwise {\sf Door2} in ${\cal D}^\prime$ (See Fig.~\ref{fig:checkers}).
Note that, in the case of {\sf Door3}, the last robot $r_i$ on the $(L-2)$-line becomes Finished by {\sf P2StopC} in ${\cal F}_2^\prime$ when its successor $r_j$ arrives at the Door corner.
Then, after $r_j$ moves two hops (i.e., by {\sf ColP1B1} in ${\cal C}^\prime$ and {\sf MovP2B} in ${\cal M}_2^\prime$ respectively), the view from the Door node becomes {\sf Door4} for $r_j$'s successor.
\begin{itemize}
\item If the view from the Door node is {\sf Door4} or {\sf Door3}, the robot on the Door node moves to the Door corner by Rule 0-2.
Then, the view from the Door corner is {\sf ColP1B1} in ${\cal C}^\prime$.
By the same discussion as above (Fig.~\ref{fig:checkers}), the view from the Door corner eventually becomes {\sf P1Stop0} in ${\cal F}_1^\prime$, thus the final robot on the Door corner becomes Finished by Rule 1.
Then, any other robots cannot enter into the grid because there is no such rule.
\item If the view from the Door node is {\sf Door2}, the view from the Door corner is {\sf ColP1A1} in ${\cal C}^\prime$.
Then, the empty node $v$ that is adjacent to the Door corner is eventually occupied by a Finished robot on $(L-1)$-line (Fig.~\ref{fig:checkers}).
After that,
any other robots on the Door node cannot enter into the grid because there is no such rule.
\end{itemize}
Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}
Every robot on the grid is eventually Finished.
\end{lemma}
\begin{proof}
By the proofs of Lemmas~\ref{predecessor}-\ref{32hops}, the transitions of the view type of each robot are shown as Fig.~\ref{fig:Alg2}.
Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}
\begin{figure}[t]
    \centering
    \subfigure[For $0$-line]{\includegraphics[width=0.38\textwidth]{0-line-crop.pdf}}\hspace{0.15cm}
    \subfigure[For $(L-2)$-line and $(L-3)$-line]{\includegraphics[width=0.53\textwidth]{L1L2-line-crop.pdf}}\\
    \subfigure[For $(L-1)$-line]{\includegraphics[width=0.43\textwidth]{L-line-crop.pdf}}\hspace{0.15cm}
    \subfigure[For other lines]{\includegraphics[width=0.52\textwidth]{other-line-crop.pdf}}
    \caption{View type transitions of Algorithm 2. Each solid arrow (resp. dotted arrow) represents a transition by a {\it Move} (resp. {\it Enter\_Grid}) operation. We omitted the view {\sf Door0}.}
    \label{fig:Alg2}
\end{figure}

By Lemma~\ref{32hops}, distances between any two occupied nodes are two.
Thus, by the same discussion as Theorem~\ref{1MIS},
we are now able to state our main result:

\begin{theorem}\label{MIS}
Algorithm 2 constructs a maximum independent set by occupied locations on the grid.
\end{theorem}

By the proofs of Lemmas~\ref{31stB}--\ref{32hops}, nodes on the even-numbers (resp. odd-numbers) lines are occupied by $\lceil l/2\rceil$ (resp. $\lfloor l/2 \rfloor$) robots.
By the same discussion as Lemma~\ref{number}, the following lemma holds.
\begin{lemma}\label{3number}
When a maximum independent set is constructed, $\lceil n/2 \rceil$ robots are on the grid.
\end{lemma}

Each robot $r_i$ sets its value $k_i$ at most once by Rule 0-1.
By the same discussion of Theorem~\ref{time}, the following theorem holds.
\begin{theorem}\label{3time}
The time complexity of Algorithm 2 is $O(n(L+l))$ steps.
\end{theorem}

\section{Introduction}
\input{introduction.tex}
\input{relatedwork-Contribution}

\section{Model}\label{model}
\input{model.tex}

\section{Proposed Algorithms}

In this section, we present two algorithms to construct a maximum independent set when the Door node is connected to a corner node.
The first algorithm makes the assumption that outgoing edges are labeled ``locally'' (that is, the labels may be inconsistent for the two adjacent nodes of the edge, however, a node must assign distinct labels to different outgoing edges), and assumes that each robot is endowed with a light enabling $3$ colors and has visibility radius $2$.
To remove the edge labeling assumption, the second algorithm makes use of more colors (7 colors are needed) and a larger visibility radius (i.e., $3$). As a result, it operates in the ``vanilla'' Look-Compute-Move model (no labeling of nodes or edges, etc.).
In both algorithms, we assume no agreement on the grid axes or directions.

\subsection{Algorithm with 3 colors lights, $\phi=2$, and port numbering}\label{sec:3colors}
\input{alg1.tex}

\subsection{Algorithm with 7 colors lights, and $\phi=3$}\label{sec:7colors}
\input{alg2.tex}

\section{Conclusion}
\input{conclusion.tex}

\bibliographystyle{splncs04}

\subsubsection{Proof of Correctness}

Without loss of generality, let $L$ be the size of the border that is connected to the Door corner by an edge with a maximal port number among two edges of the Door corner.
Let $l$ be the other size of the border.
We call the $L$-size border connected to the Door corner ``the first border", and the $l$-size border not-connected to the Door corner ``the second border", like Fig.~\ref{fig:st1}(b).
Additionally, we call the second border \emph{0-line}, and count the lines in the following way: the line that is adjacent and parallel to 0-line is \emph{1-line}, and the border that is connected to the Door corner but not the first border is \emph{$(L-1)$-line}.

First, we show that robots cannot collide.
\begin{lemma}\label{collide}
Robots cannot collide when executing Algorithm 1.
\end{lemma}
\begin{proof}
If there exists an outdated robot $r_o$ that is to move using its outdated view, the outdated view is one of the types in ${\cal D}$, ${\cal C}$, ${\cal M}_1$, or ${\cal M}_2$ by the definition of the algorithm.
Thus, if a collision with $r_o$ occurs, then $r_o$'s view is one of the types in ${\cal D}$, ${\cal C}$, ${\cal M}_1$, or ${\cal M}_2$.
In that case, because a Finished robot does not move forever, a non-Finished robot in $r_o$'s view may have moved,
or other non-Finished robot came into the visible region of $r_o$.

On the Door corner, if a robot $r_i$ cannot see other robots, then its view is {\sf StartP1} in ${\cal M}_1$.
Then, because $r_i$ has $c(r_i)=p_1$ initially, its view becomes {\sf MovP1} in ${\cal M}_1$.
By the definition of {\sf MovP1}, $r_i$ moves only on the first border according to the degree of nodes until it arrives at the end of the first border, or it can see Finished robots.
Then, the first border is one-way because each robot can recognize its previous node.
Additionally, if $r_i$ can see other non-Finished robots than its successor, then $r_i$ cannot move because there is no such rule.
That is, $r_i$ keeps the distance from its predecessor (if it exists) two or more hops on the first border.
Thus, on the first border (while $c(r_i)=p_1$), if $r_i$ has an outdated view in ${\cal D}$, ${\cal C}$, or ${\cal M}_1$, the current configuration can be the same view type as its outdated view, because only $r_i$'s successor is allowed to move toward $r_i$.
Thus, $r_i$ cannot collide with other robots while $c(r_i)=p_1$.

Consider when $r_i$ arrives at the end of the first border, or can see Finished robots.
\begin{itemize}
\item If ${\it view}(r_i)$ becomes {\sf P1Stop} or {\sf OnCP1F} in ${\cal F}_1$, then $r_i$ changes its color to $F$ by Rule 1.
\item If ${\it view}(r_i)$ becomes {\sf OnCP1} in ${\cal C}$, then $r_i$ changes its color to $p_2$, and moves to the second border by Rule 2.
After that, ${\it view}(r_i)$ becomes {\sf MovP2} in ${\cal M}_2$ until it arrives at the diagonal corner (\emph{i.e.}, {\sf OnCP2} in ${\cal F}_2$), or it can see Finished robots on the second border (\emph{i.e.}, {\sf P2Stop} in ${\cal F}_2$).
By the definition of {\sf MovP2}, each robot moves on the second border according to the degree of nodes, and the second border is one-way.
By the definition of the algorithm, there is no rule to make $r_i$ stray from the second border.
Then, $r_i$ keeps the distance from its predecessor (if it exists) two or more hops on the second border.
\item If ${\it view}(r_i)$ becomes {\sf GoCo} in ${\cal M}_1$, then $r_i$ moves to the adjacent node occupied by a Finished robot on the first border and ${\it view}(r_i)$ becomes {\sf ColP1A} in ${\cal C}$.
\item If ${\it view}(r_i)$ becomes {\sf ColP1A} or {\sf ColP1B} in ${\cal C}$, then $r_i$ changes its color to $p_2$, and moves to one of the lines. Without loss of generality, let the line be $m$-line where $m>0$.
Then, robots on $(m-1)$-line are Finished and $(m+1)$-line is empty (if it exists on the grid) by the definition of {\sf ColP1A} or {\sf ColP1B}.
Thus, after that, ${\it view}(r_i)$ becomes {\sf MovP2A} or {\sf MovP2B} in ${\cal M}_2$ until it arrives at the end of $m$-line (\emph{i.e.}, {\sf P2StopA} or {\sf P2StopB} in ${\cal F}_2$), or it can see a Finished robot on $m$-line (\emph{i.e.}, {\sf P2StopC} in ${\cal F}_2$).
By the definition of the algorithm, there is no rule to make $r_i$ stray from $m$-line.
By the definitions of {\sf MovP2A} and {\sf MovP2B}, $m$-line is also one-way, and $r_i$ keeps the distance from its predecessor (if it exists on the line) two or more hops.
\end{itemize}
In any case, on each line (while $c(r_i)=p_2$), if $r_i$ has an outdated view in ${\cal C}$ or ${\cal M}_2$, then the current configuration is the same view type as its outdated view, because only $r_i$'s successor is allowed to move toward $r_i$.
Thus, $r_i$ cannot collide with other robots while $c(r_i)=p_2$.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

Next, we show that Algorithm 1 constructs a maximum independent set.
\begin{lemma}\label{1st}
The first robot $r_1$ moves to the diagonal corner, and $c(r_1)$ becomes $F$ on the corner.
\end{lemma}
\begin{proof}
When the first robot $r_1$ is in the Door node, then its view is {\sf Door1} in ${\cal D}$.
Thus, it moves to the Door corner by ${\it Enter\_Grid}(r_1)$, and its view becomes {\sf StartP1} in ${\cal M}_1$.
Then, $r_1$ moves to the adjacent node through the edge with the maximal port number by Rule 3.
Then, because it is the first robot, its view becomes {\sf MovP1} in ${\cal M}_1$ and moves to the adjacent node on the first border by Rule 3.

By the proof of Lemma~\ref{collide}, the first border and second border are one-way, and any other robots cannot pass $r_1$ on these borders.
Thus, ${\it view}(r_1)$ remains {\sf MovP1}, and $r_1$ moves on the first border according to the node degree.
Therefore, $r_1$ arrives at the end of the first border eventually, and then ${\it view}(r_1)$ becomes {\sf OnCP1} in ${\cal C}$.
After that, by Rule 2, $r_1$ changes its color to $p_2$ and moves to the adjacent node on the second border.
${\it view}(r_1)$ becomes {\sf MovP2} in ${\cal M}_2$, $r_1$ moves towards the next (diagonal) corner through the second border according to the node degree by Rule 5, eventually ${\it view}(r_1)$ becomes {\sf OnCP2} in ${\cal F}_2$.
By Rule 4, because $c(r_1)=p_2$, $r_1$ changes its color to $F$ on the corner.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{1stB}
The first $\lceil l/2 \rceil$ robots move to the second border, and their color becomes $F$.
Additionally, nodes on the second border are occupied by a robot or empty alternately from the diagonal corner.
\end{lemma}
\begin{proof}
By Lemma~\ref{1st}, the first robot $r_1$ eventually becomes Finished on the diagonal corner.

First, we consider the second robot $r_2$, which follows $r_1$ in the case that $l>3$.
By the assumption, $r_2$ appears to the Door node just after $r_1$ enters into the grid.
Because $r_1$ does not become Finished before it arrives at the diagonal corner, $r_2$ can move from the Door node only when ${\it view}(r_2)={\sf Door1}$ in ${\cal D}$ holds.
After that, by the definition of the algorithm, $r_2$ moves in the same way as $r_1$, $c(r_2)$ becomes $p_2$ on the end of the first border eventually and $r_2$ moves on the second border.
Finally, $r_2$ can see $r_1$ on the diagonal corner two hops away.
Then, there is no rule such that $r_2$ executes before $c(r_1)$ becomes $F$.
Because of Lemma~\ref{1st}, ${\it view}(r_2)$ eventually becomes {\sf P2Stop} in ${\cal F}_2$.
Then, by Rule 4, $c(r_2)$ becomes $F$.

In the case that $l=3$, when $r_2$ arrives at the end of the first border, ${\it view}(r_2)$ becomes {\sf OnCP1F} in ${\cal F}_1$ and $c(r_2)$ becomes $F$ by Rule 1.
Note that, in any case, the distance between $r_1$ and $r_2$ is two hops when they are Finished.

For the successors of $r_2$, we can discuss their movements in the same way as $r_2$.
Thus, by the definitions of {\sf OnCP1F} and {\sf P2Stop},
the distance between a robot and its successor is two hops when they are Finished on the second border.
Therefore, on the second border, beginning with the diagonal corner, every even node is occupied, and the number of robots is $\lceil l/2 \rceil$.
If $l$ is odd, when the $\lceil l/2 \rceil$-th robot arrives at the end of the first border, its view becomes {\sf OnCP1F} and it changes its color to $F$ by Rule 1.
Otherwise, it changes its color to $p_2$ and moves to the second border.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{1-line}
From the $(\lceil l/2 \rceil+1)$-th to the $l$-th robots, each robot moves to the $1$-line, and its color becomes $F$.
Additionally, nodes on the $1$-line are empty or occupied by a robot alternately, beginning with an empty node.
\end{lemma}
\begin{proof}
By Lemma~\ref{1stB}, $\lceil l/2 \rceil$ robots on $0$-line eventually become Finished.
Let $r_i$ be the $(\lceil l/2 \rceil+1)$-th robot, $r_j$ be the $(\lceil l/2 \rceil)$-th robot that is the predecessor of $r_i$.
$r_i$ moves from the Door node in the same way as $r_j$ while $c(r_i)=p_1$.
Because robots on $0$-line become Finished eventually, one of the following two
cases occurs: \emph{(1)} if $l$ is odd, ${\it view}(r_i)$ becomes {\sf GoCo} in ${\cal M}_1$, because the end of the first border is occupied by $r_j$, or \emph{(2)} if $l$ is even, ${\it view}(r_i)$ becomes {\sf ColP1B} in ${\cal C}$, because the end of the first border is empty but its adjacent node on the $0$-line is occupied by $r_j$.

In case \emph{(1)}, by Rule 3, $r_i$ moves to the node in front of the end of the first border, ${\it view}(r_i)$ becomes {\sf ColP1A} in ${\cal C}$.
Then, by Rule 2, $c(r_i)$ becomes $p_2$ and $r_i$ moves to $1$-line.
After that, if $l=3$, ${\it view}(r_i)$ becomes {\sf P2StopA} in ${\cal F}_2$ and $r_i$ changes its color to $F$ by Rule 4.
Otherwise, because $r_i$ can see Finished robots on $0$-line, ${\it view}(r_i)$ becomes {\sf MovP2A} in ${\cal M}_2$.
Then, because the nodes on $0$-line are occupied alternately by Lemma~\ref{1stB}, ${\it view}(r_i)$ becomes {\sf MovP2B} and {\sf MovP2A} in ${\cal M}_2$ alternately by the execution of Rule 5.
Thus, $r_i$ moves toward the other side border that is parallel to the first border by Rule 5, and ${\it view}(r_i)$ eventually becomes {\sf P2StopA} because the diagonal corner is occupied by a Finished robot (Lemma~\ref{1st}).
Then, by Rule 4, $c(r_i)$ eventually becomes $F$.
Because $l$ is odd, $\lfloor l/2 \rfloor-1$ successors of $r_i$ follow $r_i$, and eventually, their views become {\sf P2StopC} in ${\cal F}_2$, and they change their colors to $F$ by Rule 4 on $1$-line.

In case \emph{(2)}, $r_i$ also changes its color to $p_2$, and moves to $1$-line by Rule 2.
After that, because $r_i$ can see Finished robots on $0$-line, ${\it view}(r_i)$ becomes {\sf MovP2B} in ${\cal M}_2$.
Then, in the same way as for case \emph{(1)}, $l/2-1$ robots including $r_i$ become Finished on $1$-line.
After that, the view of the next robot $r_l$ ($l$-th robot) becomes {\sf P1Stop} in ${\cal F}_1$ on the intersection between the first border and $1$-line, and $r_l$ becomes Finished by Rule 1.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{2hops}
The distance between any two robots on the grid is two hops after every robot becomes Finished.
\end{lemma}
\begin{proof}
By
the definitions of ${\cal F}_1$ and ${\cal F}_2$, the distance between a robot $r_i$ and its predecessor is two hops after $r_i$ becomes Finished if the predecessor is on the same line as $r_i$.
Thus, when the robots on $m$-line ($0<m<L-1$) become Finished, if there are two adjacent Finished robots, then there is a robot $r_r$ on $m$-line that cannot move from the node that is adjacent to a node occupied by a Finished robot on $(m-1)$-line.
However, by the same argument as in Lemmas~\ref{1stB} and \ref{1-line}, if $m$ is odd (resp. even), the nodes on $m$-line are occupied alternately beginning with an empty node (resp. occupied node) because the nodes on $(m-1)$-line are also occupied alternately beginning with an occupied node (resp. empty node).
Thus, before such $r_r$ becomes Finished, $r_r$ has a view of type {\sf MovP2B} and can move by Rule 5, i.e., it cannot exist.

Now, to consider the end of the execution of the algorithm, we consider $(L-1)$-line when nodes on $(L-2)$-line are occupied by Finished robots.
The $(L-1)$-line is a border connected to the Door node.
Then, if both $l$ and $L$ are odd or both are even, the view from the Door node becomes {\sf Door1}, otherwise {\sf Door2} (See Fig.~\ref{fig:checkers}).
\begin{itemize}
\item If the view from the Door node is {\sf Door1}, the robot on the Door node moves to the Door corner by Rule 0.
Then, the view from the Door corner is {\sf ColP1B} in ${\cal C}$.
By the above discussion, the view from the Door corner eventually becomes {\sf P1Stop} in ${\cal F}_1$, thus the final robot on the Door corner becomes Finished by Rule 1.
Then, any other robots cannot enter into the grid because there is no such rule.
\item If the view from the Door node is {\sf Door2}, the view from the Door corner is {\sf ColP1A} in ${\cal C}$.
Then, the empty node $v$ that is adjacent to the Door corner is eventually occupied by a Finished robot on $(L-1)$-line.
After that, any other robots on the Door node cannot enter into the grid because there is no such rule.
\end{itemize}
Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}
Every robot on the grid is eventually Finished.
\end{lemma}
\begin{proof}
By the proofs of Lemmas~\ref{collide}-\ref{2hops}, the transitions of the view type of each robot are shown as Fig.~\ref{fig:Alg1}.
Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{theorem}\label{1MIS}
Algorithm 1 constructs a maximum independent set of occupied locations on the grid.
\end{theorem}
\begin{proof}
By Lemma~\ref{2hops}, distances between any two occupied nodes are two. On a grid, only checkers patterns satisfy this constraint.
When at least one dimension of even, there are as many occupied locations as non-occupied locations, so any checkers pattern is a maximum independent set (see Fig.~\ref{fig:checkers}(a) and Fig.~\ref{fig:checkers}(b)). When both dimensions are odd, there may be either one more occupied locations than non-occupied locations, or the contrary (See Fig.~\ref{fig:checkers}(c)). The situation that corresponds to the maximum independent set is the one with occupied locations in the corners, which is what our algorithm constructs.
Hence, the theorem holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{figure}[t]
\centering
\subfigure[even-even dimensions]{
\centering
\includegraphics[height=.12\textheight]{eveneven}
}
\subfigure[even-odd dimensions]{
\centering
\includegraphics[height=.15\textheight]{oddeven}
}
\subfigure[odd-odd dimensions]{
\centering
\includegraphics[height=.15\textheight]{oddodd}
}
\caption{Checkers patterns in grids.}
\label{fig:checkers}
\end{figure}

\begin{figure}[t]
    \centering
    \includegraphics[width=0.57\textwidth]{Alg1-crop.pdf}
    \caption{View type transitions of Algorithm 1. Each solid arrow (resp. dotted arrow) represents a transition by a {\it Move} (resp. {\it Enter\_Grid}) operation. }
    \label{fig:Alg1}
\end{figure}

\begin{lemma}\label{number}
When a maximum independent set is constructed, $\lceil n/2 \rceil$ robots are on the grid.
\end{lemma}
\begin{proof}
By the proofs of Lemmas~\ref{1stB}--\ref{2hops}, nodes on the even-numbers (resp. odd-numbers) lines are occupied by $\lceil l/2\rceil$ (resp. $\lfloor l/2 \rfloor$) robots.
Therefore, if $L$ is even, the number of robots in the maximum independent set is $lL/2$.
If $L$ is odd, the number of robots in the maximum independent set is $l\lfloor L/2\rfloor+\lceil l/2\rceil$.
Because $n=lL$, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

To analyze the time complexity of the algorithm, we count the sum of individual executions of rules.

\begin{theorem}\label{time}
The time complexity by Algorithm 1 is $O(n(L+l))$ steps.
\end{theorem}
\begin{proof}
The first robot moves $L+l-1$ steps and becomes Finished, thus it executes $L+l$ steps.
The first robot moves the longest way.
Therefore, by Lemma~\ref{number}, the sum of the number of steps
is $O(n(L+l))$.
Thus, the theorem holds.\hfill$\Box$\par\vskip1em
\end{proof}

\subsubsection{Proof of Correctness}

Without loss of generality, let $L$ be the size of the border chosen by the first robot on the Door corner in {\sf StartP10} in ${\cal M}_1^\prime$.
Let $l$ be the other size of the border.
In the same way as Algorithm 1, we define ``the first border", ``the second border", and lines.

In the following, we first show that each robot can recognize its successor and robots cannot collide.

\begin{lemma}\label{predecessor}
Each non-Finished robot except the first robot can recognize its predecessor and successor if it keeps two neighboring non-Finished robots.
\end{lemma}
\begin{proof}
By the assumption, each robot $r_i$ initializes its $c(r_i)$ to $p_1(0)$.
The view of the first robot $r_1$ on the Door node is {\sf Door1} in ${\cal D}^\prime$, thus it moves to the Door corner with $c(r_1)=p_1(0)$ by Rule 0-2.
After that, by the assumption, its successor $r_2$ appears on the Door node with $c(r_2)=p_1(0)$.
Thus, $r_1$ cannot move until its view becomes {\sf StartP10} in ${\cal M}_1^\prime$, i.e., $r_2$ has $c(r_2)=p_1((k_1+1)\mod 3))=p_1((0+1)\mod 3)=p_1(1)$.
Thus, ${\it view}(r_2)$ on the Door node becomes {\sf Door0} and $r_2$ sets $c(r_2)$ to $p_1(1)$ by Rule 0-1.
Then, ${\it view}(r_1)$ becomes {\sf StartP10} in ${\cal M}_1^\prime$, $r_1$ selects the first border arbitrarily and moves on the border by Rule 3.

Consider a robot $r_i$ sets $c(r_i)$ to $p_1(k_i)$ on the Door node in {\sf Door0}.
Then, its predecessor $r_h$ on the Door corner has $c(k_h)$ where $k_i=(k_h+1)\mod 3$ by the definition of ${\it SetC}(r_i)$.
After $r_i$ enters the grid, on the Door corner, it cannot move until its successor $r_j$ sets $c(r_j)$ to $p_1(k_j)$ where $k_j=(k_i+1)\mod 3$ by the definitions of {\sf StartP11}, {\sf MovP13}, {\sf MovP14}, {\sf GoCo1} (in ${\cal M}_1^\prime$), {\sf ColP1A1} or {\sf ColP1B1} (in ${\cal C}^\prime$).
Therefore, each robot $r_i$ on the grid has its order modulo 3 as its value $k_i$, and the value $k_i$ is not changed after that.
Thus, if each robot keeps two neighboring non-Finished robots, it can recognize its neighboring non-Finished robot with smaller (resp. larger) $k$ value than its own as its predecessor (resp. successor), lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{3collide1}
While the light color is $p_1(k_i)$, each robot $r_i$
can recognize its successor, and cannot collide.
\end{lemma}
\begin{proof}
If there exists an outdated robot $r_o$ that is to move according to its outdated view, the view type is in ${\cal D}^\prime$, ${\cal C}^\prime$, ${\cal M}_1^\prime$, and ${\cal M}_2^\prime$ by the definition of the algorithm.
Thus, if a collision with $r_o$ occurs, then $r_o$'s view type is in ${\cal D}^\prime$, ${\cal C}^\prime$, ${\cal M}_1^\prime$, and ${\cal M}_2^\prime$.
In that case, because a Finished robot does not move forever, it could be that a non-Finished robot in $r_o$'s view moved,
or that another non-Finished robot came into the visible region of $r_o$.

The first robot $r_1$ keeps its color $c(r_1)=p_1(0)$.
On the Door node, the view of $r_1$ becomes {\sf Door1} in ${\cal D}^\prime$, and $r_1$ moves to the Door corner.
After that, $r_1$ can move only when its view becomes {\sf StartP10} in ${\cal M}_1^\prime$, i.e., $c(r_2)$ has to be set to $p_1(1)$ by ${\it SetC}(r_2)$, where $r_2$ is $r_1$'s successor.
Thus, the view of $r_2$ on the Door node becomes {\sf Door0}, and eventually $r_2$ sets its color to $p_1(1)$.
Then, $r_1$ selects one border as the first border arbitrarily in {\sf StartP10} and moves.
Because the distance from $r_2$ becomes two, ${\it view}(r_1)$ becomes {\sf MovP10} and $r_1$ moves one hop.
Then, because there is no rule to move for $r_1$ when the distance from $r_2$ is three, $r_1$ cannot move.
Thus, ${\it view}(r_2)$ becomes {\sf Door1} in ${\cal D}^\prime$ and $r_2$ enters the grid.
After that, $r_1$ can move because the distance from $r_2$ is two, i.e., {\sf MovP10} in ${\cal M}_1^\prime$ by Rule 3.
Thus, by Rule 3, $r_2$ can move from the Door corner only when ${\it view}(r_2)$ becomes {\sf StartP11} in ${\cal M}_1^\prime$.
That is, when $r_2$ can move, the distance between $r_1$ and $r_2$ is three, and $r_2$'s successor $r_3$ has $c(r_3)=p_1(2)$ by the definition of {\sf StartP11}.
By the definition of ${\cal M}_1^\prime$, they move only on the first border according to the degree of nodes until they arrive at the end of the first border.
While they move on the first border, only $r_1$ and $r_3$ are neighbors for $r_2$, and $r_3$'s successors also follow $r_3$ in the same way as $r_2$.
When the view of robots become {\sf OnCP1} in ${\cal C}^\prime$ (i.e., they arrive at the end of the first border), they change their colors from $p_1(k_i)$ to $p_2(k_i)$ in the same order as they entered the grid.

By the same argument, each robot $r_i$ moves only on the first border using the degree of nodes while $c(r_i)=p_1(k_i)$ holds, by the definition of the views in ${\cal M}_1^\prime$.
Then, on the first border, if $r_i$ is not on the Door node or the Door corner, $r_i$ can move only when the distance from its predecessor $r_h$ is three and from its successor $r_j$ is two.
That is, while $r_i$ moves on the first border, $r_j$ follows $r_i$.
Then, by the definition of the views in ${\cal M}_1^\prime$, while $r_i$ moves on the first border, there are at most two non-Finished neighboring robots $r_h$ and $r_j$ for $r_i$ and they are kept by $r_i$'s movement, i.e., robots move on the first border keeping in the order they entered the grid.
By the definition of the algorithm, only when $r_h$ becomes Finished two hops away by ${\cal F}_1^\prime$ or ${\cal F}_2^\prime$,
the number of non-Finished neighboring robots for $r_i$ becomes one, but $r_i$ keeps $r_j$ with $k_i<k_j$ in its view and recognizes $r_j$ as its successor.
By Lemma~\ref{predecessor}, on the first border, each non-Finished robot can always recognize its successor, that is, each robot can recognize its direction.
Therefore, the first border is one-way.
Thus, while $c(r_i)=p_1(k_i)$ holds, if the view is in ${\cal D}^\prime$, ${\cal C}^\prime$, or ${\cal M}_1^\prime$, $r_i$ cannot become outdated as any non-Finished robot cannot come into $r_i$'s visible region, and any non-Finished robots in $r_i$'s view cannot move.
That is, each robot cannot collide with other robots.

For each robot $r_i$, when its view becomes in ${\cal F}_1^\prime$ on the first border, $r_i$ changes its color to $F$ by Rule 1.
When its view belongs to ${\cal C}^\prime$ on the first border, $r_i$ changes its color from $p_1(k_i)$ to $p_2(k_i)$ and changes its direction to a line by Rule 2.
Thus lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{3collide2}
While the light color is $p_2(k_i)$, each robot $r_i$ can recognize its successor, and cannot collide.
\end{lemma}
\begin{proof}
Consider the time $t$ when each robot $r_i$ changes its color to $p_2(k_i)$ on the first border.
Then, its view is in ${\cal C}^\prime$ by Rule 2, and $r_i$ moves to a line.
By the proof of Lemma~\ref{3collide1} and the definition of the views in ${\cal C}^\prime$, $r_i$'s successor $r_j$ is two hops behind at $t$.
After that, by the definition of views in ${\cal M}_2^\prime$, $r_i$ can move only when the distance from $r_j$ is two and the distance from its non-Finished predecessor $r_h$ (if exists) is three.
Thus, after $r_i$ moves by the view in ${\cal M}_2^\prime$, $r_i$ cannot move unless $r_j$ moves.
\begin{itemize}
\item If ${\it view}(r_i)$ is {\sf OnCP1} at $t$, $r_i$ moves to the $0$-line (i.e., the second border) and $r_j$ also follows $r_i$.
After that, ${\it view}(r_i)$ becomes {\sf MovP2} in ${\cal M}_2^\prime$ until $r_i$ arrives at the diagonal corner (i.e., {\sf OnCP2} in ${\cal F}_2^\prime$) or $r_h$ becomes Finished on $0$-line (i.e., {\sf P2Stop} in ${\cal F}_2^\prime$).
By the definition of {\sf MovP2} in ${\cal M}_2^\prime$, $r_i$ moves on the second border according to the degree of nodes.
By the definition of the algorithm, there is no rule to make $r_i$ stray from the second border.
Then, by the definition of {\sf MovP2} in ${\cal M}_2^\prime$, $r_i$ keeps the distance from $r_j$ two or three hops and has at most two non-Finished neighboring robots, while $r_i$ moves on the second border.
By this distance, these non-Finished neighboring robots are kept by the movement.
Because robots on the second border keep the same order as when they entered the grid, only when $r_h$ becomes Finished by ${\cal F}_2^\prime$ (i.e., {\sf P2Stop} or {\sf OnCP2}), or $r_i$ is the first robot, the number of non-Finished neighboring robots for $r_i$ becomes one.
Then, $r_i$ can recognize $r_j$ as its successor, because $r_j$ is always in ${\it view}(r_i)$ and $k_i<k_j$ holds.
Thus, by Lemma~\ref{predecessor}, $r_i$ can always recognize $r_j$ as its successor, and the second border is one way.

\item If ${\it view}(r_i)$ is {\sf ColP1A0} (resp. {\sf ColP1A1}) at $t$, $r_i$ moves on a line except $0$-line and $(L-1)$-line (resp. $(L-1)$-line) and $r_j$ also follows $r_i$.
Without loss of generality, let the line be $m$-line where $m>0$.
Then, by the definition of {\sf ColP1A0} (resp. {\sf ColP1A1}), robots on $(m-1)$-line are Finished and $(m+1)$-line is empty (if it exists on the grid).
Thus, after that, because $r_j$ follows $r_i$, ${\it view}(r_i)$ becomes {\sf MovP2A} or {\sf MovP2B} in ${\cal M}_2^\prime$ until $r_i$ arrives at the end of the line (i.e., {\sf P2StopA} or {\sf P2StopB} in ${\cal F}_2^\prime$) or $r_h$ becomes Finished on $m$-line (i.e., {\sf P2StopC} in ${\cal F}_2^\prime$).
By the definition of the algorithm, there is no rule to make $r_i$ stray from $m$-line.
By the definitions of {\sf MovP2A} and {\sf MovP2B} in ${\cal M}_2^\prime$, $r_i$ keeps the distance from $r_j$ two or three hops, and has at most two non-Finished neighboring robots, while $r_i$ moves on $m$-line.
By this distance, these non-Finished neighboring robots are kept by the movement.
Because robots on $m$-line keep the same order as when they entered the grid, only when $r_h$ becomes Finished on $m$-line by ${\cal F}_2^\prime$ (i.e., {\sf P2StopA}, {\sf P2StopB} or {\sf P2StopC}), or $r_i$ is the first robot for $m$-line (i.e., $r_h$ is Finished on the intersection of the first border and $(m-1)$-line in {\sf ColP1A0} (resp. {\sf ColP1A1})), the number of non-Finished neighboring robots for $r_i$ becomes one. Then, $r_i$ also recognizes $r_j$ as its successor, because $r_j$ is always in ${\it view}(r_i)$ and $k_i<k_j$ holds.
Thus, by Lemma~\ref{predecessor}, $r_i$ can always recognize $r_j$ as its successor, and $m$-line is one way.

\item If ${\it view}(r_i)$ is {\sf ColP1B0} (resp. {\sf ColP1B1}) at $t$, $r_i$ moves on a line except $0$-line and $(L-1)$-line (resp. $(L-1)$-line) and $r_j$ also follows $r_i$.
After that, ${\it view}(r_i)$ becomes {\sf MovP2B} or {\sf MovP2A} in ${\cal M}_2^\prime$ until $r_i$ arrives at the end of the line (i.e., {\sf P2StopA} or {\sf P2StopB} in ${\cal F}_2^\prime$) or $r_h$ becomes Finished on the same line (i.e., {\sf P2StopC} in ${\cal F}_2^\prime$).
By the same discussion as above, $r_i$ can always recognize $r_j$ as its successor, and the line is one way.
\end{itemize}
Therefore, in any case, while $r_i$ has $p_2(k_i)$,
if the view is in ${\cal C}^\prime$ or ${\cal M}_2^\prime$, then $r_i$ cannot become outdated as any non-Finished robots cannot come into $r_i$'s visible region, and any non-Finished robots in $r_i$'s view cannot move.
Thus, $r_i$ cannot collide with other robots while $r_i$ has $p_2(k_i)$, and the lemma holds. \hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{predecessor2}
Each non-Finished robot can recognize its successor.
\end{lemma}
\begin{proof}
By Lemma~\ref{3collide1} (resp. Lemma~\ref{3collide2}), each non-Finished robot $r_i$ can always recognize its successor while $c(r_i)=p_1(k_i)$ (resp. $c(r_i)=p_2(k_i)$) holds.
Thus, the lemma holds.
\hfill$\Box$\par\vskip1em\end{proof}

\begin{lemma}\label{3collide}
Robots cannot collide when executing Algorithm 2.
\end{lemma}
\begin{proof}
By Lemma~\ref{3collide1} (resp. Lemma~\ref{3collide2}), while the light color is $p_1(k_i)$ (resp. $p_2(k_i)$), robots cannot collide.
Because each robot cannot move after it becomes Finished, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

Next, we show that Algorithm 2 constructs a maximum independent set.

\begin{lemma}\label{31st}
The first robot $r_1$ moves to the diagonal corner, and $c(r_1)$ becomes $F$ on the corner.
\end{lemma}
\begin{proof}
By the proofs of Lemmas~\ref{3collide1} and \ref{3collide2}, while robots move on the grid, they keep the order they entered the grid.

By the proof of Lemma~\ref{3collide1}, $r_1$ eventually arrives at the end of the first border, and then
$r_1$'s successor $r_2$ is on the node three hops behind.
When the distance between $r_1$ and $r_2$ becomes two, then ${\it view}(r_1)$ becomes {\sf OnCP1} in ${\cal C}^\prime$.

After that, by the proof of Lemma~\ref{3collide2}, $r_1$ eventually arrives at the diagonal corner because $r_1$ is the first robot.
When the distance between $r_1$ and $r_2$ becomes two, ${\it view}(r_1)$ becomes {\sf OnCP2} in ${\cal F}_2^\prime$.
By Rule 4, because $c(r_1)=p_2(k_1)$, it changes its color to $F$ on the corner.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{31stB}
The first $\lceil l/2 \rceil$ robots move to the second border, and their colors become $F$.
Additionally, nodes on the second border are empty or occupied by a robot alternately from the diagonal corner.
\end{lemma}
\begin{proof}
By Lemma~\ref{31st}, the first robot $r_1$ eventually becomes Finished on the diagonal corner.
Then, by the definition of {\sf OnCP2} in ${\cal F}_2^\prime$ for $r_1$, the distance between $r_1$ and its successor $r_2$ is two.

Consider the execution of $r_2$ after $c(r_1)$ becomes $F$.
If $l$ is more than three, ${\it view}(r_2)$ becomes {\sf P2Stop} in ${\cal F}_2^\prime$ when the distance between $r_2$ and its successor $r_3$ becomes two.
Then, by Rule 4, $c(r_2)$ becomes $F$.
If $l$ is three, then $r_2$ is at the end of the first border, thus ${\it view}(r_2)$ becomes {\sf OnCP1F} in ${\cal F}_1^\prime$ when the distance between $r_2$ and $r_3$ becomes two.
Then, $c(r_2)$ becomes $F$ by Rule 1.
Note that, in both cases, the distance between $r_1$ and $r_2$ remains two hops.

For the successors of $r_2$, we can discuss their movements in the same way as $r_2$.
By the definitions of {\sf OnCP1F} in ${\cal F}_1^\prime$ and {\sf P2Stop} in ${\cal F}_2^\prime$, when robots become $F$ on the second border, the distance between a robot and its successor is two hops because there is no rule to move to the adjacent node of the occupied node on the border.
Therefore, on the second border, beginning with the diagonal corner, every even node is occupied, and the number of robots is $\lceil l/2 \rceil$.
If $l$ is odd, when the $\lceil l/2 \rceil$-th robot $r_i$ arrives at the end of the first border and the distance between $r_i$ and its successor becomes two, $r_i$'s view becomes {\sf OnCP1F} in ${\cal F}_1^\prime$ and $r_i$ changes its color to $F$ by Rule 1.
Otherwise, $r_i$ changes its color to $p_2(k_i)$ and moves to the second border.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{31-line}
From the $(\lceil l/2 \rceil+1)$-th to the $l$-th robots, each robot moves to the $1$-line, and its color becomes $F$.
Additionally, nodes on the $1$-line are empty or occupied by a robot alternately, beginning with an empty node.
\end{lemma}
\begin{proof}
By Lemma~\ref{31stB}, $\lceil l/2 \rceil$ robots on $0$-line eventually become Finished.
By the definitions of ${\cal F}_1^\prime$ and ${\cal F}_2^\prime$, except on the Door corner, each robot can change its color to $F$ only when the distance from its successor is two.

Let $r_i$ be the $(\lceil l/2 \rceil+1)$-th robot, $r_h$ be the $(\lceil l/2 \rceil)$-th robot (i.e., $r_h$ is the predecessor of $r_i$), and $r_j$ be the $(\lceil l/2 \rceil+2)$-th robot (i.e., $r_j$ is the successor of $r_i$).
$r_i$ and $r_j$ move from the Door node in the same way as $r_h$ while $c(r_h)\neq F$.
Because robots on $0$-line (including $r_h$) become Finished eventually and then the distance between $r_i$ and $r_h$ is two, one of the following two cases occurs: When the distance between $r_i$ and $r_j$ becomes two, \emph{(1)} if $l$ is odd, ${\it view}(r_i)$ becomes {\sf GoCo0} or {\sf GoCo1} in ${\cal M}_1^\prime$, because the end of the first border is occupied by $r_h$, or \emph{(2)} if $l$ is even, ${\it view}(r_i)$ becomes {\sf ColP1B0}, because the end of the first border is empty but its adjacent node on the second border is occupied by $r_h$.

In case \emph{(1)}, by Rule 3, $r_i$ moves to the node in front of the end of the first border.
Then, after $r_j$ comes to the node two hops behind by {\sf MovP10}, ${\it view}(r_i)$ becomes {\sf ColP1A0} in ${\cal C}^\prime$.
Then, by Rule 2, $c(r_i)$ becomes $p_2(k_i)$ and $r_i$ moves to $1$-line.
After that, when $r_j$ comes to the node two hops away from $r_i$ by {\sf MovP11}, if $l=3$, ${\it view}(r_i)$ becomes {\sf P2StopA} in ${\cal F}_2^\prime$ and $r_i$ changes its color to $F$ by Rule 4.
Otherwise, because $r_i$ can see Finished robots on $0$-line, ${\it view}(r_i)$ becomes {\sf MovP2A} in ${\cal M}_2^\prime$.
Then, because the nodes on $0$-line are occupied alternately, ${\it view}(r_i)$ becomes {\sf MovP2B} and {\sf MovP2A} (in ${\cal M}_2^\prime$) alternately by the execution of Rule 5.
Thus, $r_i$ moves toward the other side border that is parallel to the first border by Rule 5 and $r_j$ follows $r_i$.
Finally, ${\it view}(r_i)$ eventually becomes {\sf P2StopA} in ${\cal F}_2^\prime$ because the diagonal corner is occupied by a Finished robot (Lemma~\ref{31st}).
Then, by Rule 4, $c(r_i)$ eventually becomes $F$.
Because $l$ is odd, $\lfloor l/2 \rfloor-1$ successors of $r_i$ follow $r_i$, and eventually their views become {\sf P2StopC} in ${\cal F}_2^\prime$, and they change their colors to $F$ by Rule 4 on $1$-line.

In case \emph{(2)}, $r_i$ also changes its color to $p_2(k_i)$, and moves to $1$-line by Rule 2.
After that, because $r_i$ can see Finished robots on $0$-line, ${\it view}(r_i)$ becomes {\sf MovP2B} in ${\cal M}_2^\prime$.
Then, in the same way as for case \emph{(1)}, $l/2-1$ robots including $r_i$ become Finished on $1$-line.
After that, the view of the next robot $r_l$ ($l$-th robot) becomes {\sf P1Stop1} in ${\cal F}_1^\prime$ on the intersection of the first border and $1$-line, and $r_l$ becomes Finished by Rule 1.

Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}\label{32hops}
The distance between any two robots on the grid is two hops after every robot becomes Finished.
\end{lemma}
\begin{proof}
By the definitions of ${\cal F}_1^\prime$ and ${\cal F}_2^\prime$, the distance between a robot $r_i$ and its predecessor $r_j$ is two hops after each robot becomes Finished if $r_i$ and $r_j$ are on the same line.
Thus, when the robots on $m$-line ($0<m<L-1$) become Finished, if there are two adjacent Finished robots to the contrary, then there is a robot $r_r$ on $m$-line that cannot move from the node that is adjacent to a node occupied by a Finished robot on $(m-1)$-line.
However, by the same argument as in Lemmas~\ref{31stB} and \ref{31-line}, if $m$ is odd (resp. even), the nodes on $m$-line are occupied alternately beginning with an empty node (resp. occupied node) because the nodes on $(m-1)$-line are also occupied alternately beginning with an occupied node (resp. empty node).
Thus, before such $r_r$ becomes Finished, $r_r$ has a view of type {\sf MovP2B} and can move by Rule 5, i.e., such $r_r$ cannot exist.

Now, to consider the end of the execution of the algorithm, we consider $(L-1)$-line when nodes on $(L-2)$-line are occupied by Finished robots.
The $(L-1)$-line is a border connected to the Door corner.
Then, if both $l$ and $L$ are odd or both are even, the view from the Door node becomes {\sf Door4} or {\sf Door3}, otherwise {\sf Door2} in ${\cal D}^\prime$ (See Fig.~\ref{fig:checkers}).
Note that, in the case of {\sf Door3}, the last robot $r_i$ on the $(L-2)$-line becomes Finished by {\sf P2StopC} in ${\cal F}_2^\prime$ when its successor $r_j$ arrives at the Door corner.
Then, after $r_j$ moves two hops (i.e., by {\sf ColP1B1} in ${\cal C}^\prime$ and {\sf MovP2B} in ${\cal M}_2^\prime$ respectively), the view from the Door node becomes {\sf Door4} for $r_j$'s successor.
\begin{itemize}
\item If the view from the Door node is {\sf Door4} or {\sf Door3}, the robot on the Door node moves to the Door corner by Rule 0-2.
Then, the view from the Door corner is {\sf ColP1B1} in ${\cal C}^\prime$.
By the same discussion as above (Fig.~\ref{fig:checkers}), the view from the Door corner eventually becomes {\sf P1Stop0} in ${\cal F}_1^\prime$, thus the final robot on the Door corner becomes Finished by Rule 1.
Then, any other robots cannot enter into the grid because there is no such rule.
\item If the view from the Door node is {\sf Door2}, the view from the Door corner is {\sf ColP1A1} in ${\cal C}^\prime$.
Then, the empty node $v$ that is adjacent to the Door corner is eventually occupied by a Finished robot on $(L-1)$-line (Fig.~\ref{fig:checkers}).
After that,
any other robots on the Door node cannot enter into the grid because there is no such rule.
\end{itemize}
Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}

\begin{lemma}
Every robot on the grid is eventually Finished.
\end{lemma}
\begin{proof}
By the proofs of Lemmas~\ref{predecessor}-\ref{32hops}, the transitions of the view type of each robot are shown as Fig.~\ref{fig:Alg2}.
Thus, the lemma holds.\hfill$\Box$\par\vskip1em
\end{proof}
\begin{figure}[t]
    \centering
    \subfigure[For $0$-line]{\includegraphics[width=0.38\textwidth]{0-line-crop.pdf}}\hspace{0.15cm}
    \subfigure[For $(L-2)$-line and $(L-3)$-line]{\includegraphics[width=0.53\textwidth]{L1L2-line-crop.pdf}}\\
    \subfigure[For $(L-1)$-line]{\includegraphics[width=0.43\textwidth]{L-line-crop.pdf}}\hspace{0.15cm}
    \subfigure[For other lines]{\includegraphics[width=0.52\textwidth]{other-line-crop.pdf}}
    \caption{View type transitions of Algorithm 2. Each solid arrow (resp. dotted arrow) represents a transition by a {\it Move} (resp. {\it Enter\_Grid}) operation. We omitted the view {\sf Door0}.}
    \label{fig:Alg2}
\end{figure}

By Lemma~\ref{32hops}, distances between any two occupied nodes are two.
Thus, by the same discussion as Theorem~\ref{1MIS},
we are now able to state our main result:

\begin{theorem}\label{MIS}
Algorithm 2 constructs a maximum independent set by occupied locations on the grid.
\end{theorem}

By the proofs of Lemmas~\ref{31stB}--\ref{32hops}, nodes on the even-numbers (resp. odd-numbers) lines are occupied by $\lceil l/2\rceil$ (resp. $\lfloor l/2 \rfloor$) robots.
By the same discussion as Lemma~\ref{number}, the following lemma holds.
\begin{lemma}\label{3number}
When a maximum independent set is constructed, $\lceil n/2 \rceil$ robots are on the grid.
\end{lemma}

Each robot $r_i$ sets its value $k_i$ at most once by Rule 0-1.
By the same discussion of Theorem~\ref{time}, the following theorem holds.
\begin{theorem}\label{3time}
The time complexity of Algorithm 2 is $O(n(L+l))$ steps.
\end{theorem}

\section{Introduction}
\input{introduction.tex}
\input{relatedwork-Contribution}

\section{Model}\label{model}
\input{model.tex}

\section{Proposed Algorithms}

In this section, we present two algorithms to construct a maximum independent set when the Door node is connected to a corner node.
The first algorithm makes the assumption that outgoing edges are labeled ``locally'' (that is, the labels may be inconsistent for the two adjacent nodes of the edge, however, a node must assign distinct labels to different outgoing edges), and assumes that each robot is endowed with a light enabling $3$ colors and has visibility radius $2$.
To remove the edge labeling assumption, the second algorithm makes use of more colors (7 colors are needed) and a larger visibility radius (i.e., $3$). As a result, it operates in the ``vanilla'' Look-Compute-Move model (no labeling of nodes or edges, etc.).
In both algorithms, we assume no agreement on the grid axes or directions.

\subsection{Algorithm with 3 colors lights, $\phi=2$, and port numbering}\label{sec:3colors}
\input{alg1.tex}

\subsection{Algorithm with 7 colors lights, and $\phi=3$}\label{sec:7colors}
\input{alg2.tex}

\section{Conclusion}
\input{conclusion.tex}

\bibliographystyle{splncs04}