%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  New template code for TAMU Theses and Dissertations starting Fall 2012.  
%  For more info about this template or the 
%  TAMU LaTeX User's Group, see http://www.howdy.me/.
%
%  Author: Wendy Lynn Turner 
%	 Version 1.0 
%  Last updated 8/5/2012
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                           SECTION IV
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\chapter{\uppercase {Neighbor Detection in Wireless Networks with Arbitrary Motion}}
\label{chap:nd}

%A key challenge for wireless networks in which nodes can move arbitrarily is for each node to keep track of its dynamically changing set of neighbors --- nodes that are within broadcast range --- and to communicate in a point-to-point fashion with its neighbors.  A solution to this ``neighbor detection'' problem serves as a basis for distributed primitives such as routing (\cite{PC97,RRPSS03}), location services (\cite{ADM04}), and distributed token circulation (\cite{MCVW05}).  

In this section, we provide a solution for each mobile node to keep track of its dynamically changing set of neighbors with which it can perform reliable point-to-point communication.  Our solution  tolerates arbitrary motion of the nodes as long as there is an upper bound on the speed, allows unsynchronized clocks subject to a bounded drift rate, and does not require any knowledge about the nodes' future locations.  In addition, we use the abstract MAC layer \cite{Kuhn2011} to provide reliable communication between neighboring nodes.  The abstract MAC layer (AML) takes care of lower layer contention management and provides reliable broadcast with bounded message delay.  This means that by using the AML, we can focus on the algorithmic aspects of the services provided on top of the AML; not worrying about scheduling wireless transmissions.  We use the reliable broadcast property of the abstract MAC layer to provide reliable point-to-point communication where for each message there exists a specific destination.

%Detecting neighboring nodes and gaining neighborhood knowledge serves as a basis for distributed algorithms that provide services such as routing (\cite{PC97,RRPSS03}), location services (\cite{ADM04}), and distributed token circulation (\cite{MCVW05}).  

%In order for neighbor detection to be meaningful, the neighbor detection mechanism should not only include identifying nearby nodes but also include performing reliable communication with them. This is what we want to accomplish in this paper. 

%By ``reliable'' we mean that when a node $p_i$'s communication link has been established (link up) with some other node $p_j$, then messages destined to $p_j$ that are sent by $p_i$ before taking down the communication link (link down) with $p_j$ is guaranteed to be delivered to $p_j$.   

%In this paper, we consider the problem of neighbor detection where detecting neighboring nodes corresponds to identifying nearby nodes where reliable communication can be performed with.  

%In order to provide such reliability in communication, we use the abstract MAC layer \cite{Kuhn2011}.  The abstract MAC layer (AML) takes care of lower layer contention management and provides reliable broadcast with bounded message delay.  This means that by using the AML, we can focus on the algorithmic aspects of the services provided on top of the AML; not worrying about scheduling wireless transmissions.  We use the reliable broadcast property of the abstract MAC layer to provide reliable point-to-point communication where for each message there exists a specific destination.

%To accomplish this,  we consider nodes having three types of communication link states with respect to other nodes: link up, link half-up, and link down.  Node $p_i$'s link state being link up with respect to node $p_j$ indicates that applications of $p_i$ can send/receive application messages to/from applications of $p_j$.  Node $p_i$'s link state being link half-up with respect to node $p_j$ indicates that applications of $p_i$ can only receive application messages from applications of $p_j$.  And, $p_i$'s link state being link down with respect to node $p_j$ indicates that applications of $p_i$ can no longer send/receive application messages to/from applications of $p_j$.

\begin{comment}
We require the neighbor detection algorithm to conform with four properties (conditions): validity, well-formedness, progress, and one-to-one corresponding delivery.  Roughly speaking, each of the four properties states that:\\
(\emph{Validity}) If a node $p_i$ is link up with some other node $p_j$, then they must be within each other's communication radius. \\
(\emph{Well-formedness}) If a node $p_i$ is link up with some other node $p_j$, then the link state of $p_i$ with respect to $p_j$ does not directly change to link down (there is an intermediate link state which does not allow messages to be sent to $p_j$ but allows receiving messages from $p_j$). \\
(\emph{Progress}) If two nodes $p_i$ and $p_j$ are close enough with each other, then there is a time in the near future where both $p_i$ and $p_j$ are link up with each other.\\
(\emph{One-to-one Corresponding Delivery}) Every application message sent has a one-to-one corresponding message delivery.
\end{comment}

We introduce a neighbor detection algorithm that utilizes periodic hello messages considering bounded clock drift.  In our algorithm, two nodes do \emph{not} become neighbors simply because they are within each other's communication radius.  Instead, a node $p_i$ considers some other node $p_j$ as its neighbor when it is ensured that an application message sent from $p_i$ will be received by $p_j$.  The condition that two nodes become neighbors depends on the message delay bounds (provided by the AML), communication radius, hello period, and the maximum speed of a node.  The key strategy that our algorithm uses is the following: when nodes $p_i$ and $p_j$ are close enough and $p_i$ receives $p_j$'s hello message, then $p_i$ sets a deadline of being neighbors with $p_j$; if $p_i$ and $p_j$ remain close enough to each other as time goes on, then this deadline is extended.  More specifically, when nodes $p_i$ and $p_j$ are close enough and $p_i$ considers node $p_j$ as its neighbor by receiving a hello message generated by $p_j$, then the deadline of $p_j$ being $p_i$'s neighbor is set such that the next hello message generated by $p_j$ is received by $p_i$ before the deadline is reached.  This is to allow $p_i$ to continue to consider $p_j$ as its neighbor by extending the deadline if $p_j$ is still close enough to $p_i$.
%Even though when nodes $p_i$ and $p_j$ are not close enough to each other, 
The algorithm also provides a way for $p_j$ to consider $p_i$ as its neighbor by letting $p_j$ to refer to the deadline already calculated by $p_i$: If $p_i$ was already considering $p_j$ as its neighbor, then $p_j$ may receive a hello message from $p_i$, which contains the amount of time left to reach $p_i$'s deadline of considering $p_j$ as its neighbor. At this point, node $p_j$ can estimate $p_i$'s deadline and then calculate its deadline of considering $p_i$ as its neighbor based on this estimation.  
%In this way, $p_j$ gets a chance to consider $p_i$ as its neighbor ($p_j$ gets a chance to broadcast application messages to $p_i$). 

\section{Challenges} 
The main challenges in obtaining the above mentioned deadlines are as follows:
\begin{compactitem}
\item Since we use periodic hello messages, hello messages should be generated and broadcast (sent to the AML) at the right time but, at the same time, we have to handshake with the AML.
\item Since hello messages are control messages that must be generated and broadcast (sent to the AML) at the right time, they can interfere with regular application message broadcasts (application message broadcasts can be blocked by hello message broadcasts).
\item Since we consider bounded clock drift, different nodes may have different hello periods when measured in real time.
\end{compactitem}

Our algorithm overcomes the above challenges in providing neighbor detection with reliable point-to-point communication.

\section{Related Work.}
\label{sec:nd:related}
Cornejo et al. \cite{Cornejo2012} consider the use of abstract MAC layer for neighbor detection.  In their approach, the geographic space is divided into regions.  Also, each node knows its trajectory information up to the near future such that it can correctly join or leave a region by notifying other neighboring nodes that it is \emph{planning} to join or leave the region.  Similar to \cite{Cornejo2012}, our approach utilize the abstract MAC layer, however, we do not require region information nor trajectory information.  Instead, we require periodic hello messages and each node knowing its correct location.

An ALOHA-like neighbor discovery algorithm is presented in \cite{VTG09}.  The authors further extend this algorithm by relaxing clock requirements, allowing different node wake up times, not knowing the total number of nodes in the system, and adding collision detection capability.  The analysis of their algorithm is based on all nodes forming a complete graph.  In our approach, there is absolutely no restriction on the network topology.

Liu \cite{Liu09} considers neighbor discovery in an environment where malicious nodes can deceive benign nodes.  The solution is based on nodes realizing tentative neighbors and then using a neighbor validation function to see if they are truly neighbors.  Even though node deployment is not restricted to a certain network topology, the paper considers the case of nodes being static after deployment.  In our approach, nodes are mobile and there is no restriction on the movement of nodes. However, we do not consider malicious failures.  
%It is shown that the tentative neighbor information by itself is not enough for the neighbor validation function to return true neighbors.  The author considers two ideas in handling this issue: 1) limiting the capability of malicious node in deceiving benign nodes during the deployment stage and 2) two neighbors usually have many common neighbors.  

Neighbor discovery in multi-channel radio networks is discussed in \cite{KCMV06} and \cite{KTKCMVP08}. Depending on each node's id (to determine the assigned synchronous time slot) and channel availability, a schedule for wireless transmission is determined.  In our approach, we delegate such scheduling to the abstract MAC layer and we do not require the clocks to be synchronized.

\begin{comment}
\subsubsection{Organization.}
\label{subsec:nd:orgainization}
The system model is given in Section \ref{sec:nd:sysmodel} and the problem specification is described in Section \ref{sec:nd:probspec}.  Section \ref{sec:nd:algorithm} presents the periodic hello-based neighbor detection algorithm and its proof of correctness is given in Section \ref{sec:nd:proofCorrect}. In Section \ref{sec:nd:discussion}, we compare several situations by considering specific parameter values for the maximum node speed, hello period, and the delay bounds provided by the abstract MAC layer.  Section \ref{sec:nd:conclusion} concludes the paper.
\end{comment}


\section{System Model}
\label{sec:nd:sysmodel}

We consider a collection of mobile nodes sending and receiving messages among each other by means of wireless broadcasts.  We assume that each node has a unique id, knows its own fixed communication radius (the communication radius can be different for different nodes), and knows the maximum speed (denoted as $\sigma$) that any node can move in the system.  

Each node's clock may not run at the same rate, however, clock drift is upper bounded by $\rho$ ($0\leq \rho <1$) with respect to real time: if $\Delta$ real time elapses, then the amount of clock time that elapses is at most $(1+\rho)\Delta$ and at least $(1-\rho)\Delta$.  We further assume that the value of $\rho$ is known to all nodes in the system.  We do \emph{not} assume that the clocks are synchronized.

We further assume that nodes are correct, do not crash, and have equipment that lets them know their correct location at any time.  We also consider that the local processing time at each node is 0.

\begin{comment}
\begin{itemize}
\item Nodes are mobile.
\item Nodes send/receive messages with each other by means of wireless communication.
\item Each node has a unique id.
\item Each node knows its own fixed communication radius (the communication radius can be different for different nodes).
\item The maximum speed (denoted as $\sigma$) that any node can move is known to all nodes in the system.
\item Each node's clock may not run at the same rate, however, their clock drift rate is upper bounded by $\rho$ ($0\leq \rho <1$) with respect to real time: if $\Delta$ real time elapses, then the amount of clock time that elapses is at most $(1+\rho)\Delta$ and at least $(1-\rho)\Delta$.  We further assume that the value of $\rho$ is known to all nodes in the network (each node's clock value does not need to be synchronized).
\item For each individual node, initially the local clock value is 0.
\item Nodes have equipment (such as GPS) that lets them know their location at any time.
\item Local processing time is 0.
\item Nodes are correct and do not crash.
\end{itemize} 
\end{comment}

\begin{figure}[tp]
\centering
\includegraphics[scale=1.2]{figures/nodelayers.pdf}
\caption{Layers of a node.}
\label{fig:nd:fig1}
\end{figure}

Each node is organized with three layers (see Figure \ref{fig:nd:fig1}).  The three layers are described next.

The abstract MAC layer (AML) ensures reliable message delivery despite contention.  It also provides maximum message delay bounds for upper layers to utilize. We assume that message delay bounds, $F^{+}_{rcv}$ and $F^{+}_{ack}$ from the abstract MAC layer, are known to all nodes in the system where $F^{+}_{rcv}$ indicates the maximum message delay for a node to receive a message (by $rcv(m)$ in Figure \ref{fig:nd:fig1}) from another node within communication radius and $F^{+}_{ack}$ indicates the maximum delay of a node receiving an acknowledgement (by $ack(m)$ in Figure \ref{fig:nd:fig1}) for a message that it transmitted.  Typically, $F^{+}_{ack} \geq F^{+}_{rcv}$ (this is also assumed throughout Section \ref{chap:nd}).  In order to utilize message delay bounds, upper layers must follow the \emph{well-formedness} condition of the AML: a message should not be sent to the AML ($bcast(m)$ in Figure \ref{fig:nd:fig1}) unless an acknowledgement of the previous message ($ack(m)$ in Figure \ref{fig:nd:fig1}) has been returned by the AML.  

The neighbor detection \& point-to-point communication layer (ND/P2P) is responsible for detecting neighboring nodes and notifying applications about the the current status (link up, link down, etc.) of neighboring nodes.  As seen in Figure \ref{fig:nd:fig1}, notifications are through $LU(j)$ (link up), $LD(j)$ (link down), and $LHU(j)$ (link half-up).  $LU(j)$ occurring at node $p_i$ indicates that a communication link has been established between $p_i$ and $p_j$ such that applications of $p_i$ can send/receive messages to/from applications of $p_j$.  $LHU(j)$ occurring at node $p_i$ indicates that a communication link has been established between $p_i$ and $p_j$ such that applications of $p_i$ can receive messages from applications of $p_j$ but cannot send messages to $p_j$.  And finally, $LD(j)$ occurs at node $p_i$ indicates that applications of $p_i$ cannot send/receive messages to/from applications of $p_j$. We refer to $LU(j)$, $LHU(j)$, and $LD(j)$ as link state events.  When $LU(j)$ (resp. $LHU(j)$; $LD(j)$) is the most recent link state event, we say that the link state is link up (resp. link half-up; link down).    Furthermore, the ND/P2P layer is responsible for sending application messages to the AML.  In order to conform with the well-formedness condition of the AML, the ND/P2P layer includes a $k$-bounded send buffer where each message sent by the application layer ($appSnd(m)$ in Figure \ref{fig:nd:fig1}) is stored and sent to the AML one-by-one.  Upon receiving an application message (generated by a different node) from the AML (by $rcv(m)$ in Figure \ref{fig:nd:fig1}), the ND/P2P layer is also responsible for sending the received message to the application layer (by $appRcv(m)$ in Figure \ref{fig:nd:fig1}).

The application layer models the set of applications that utilize the notifications provided by the ND/P2P layer ($LU(j)$, $LHU(j)$, and $LD(j)$ in Figure \ref{fig:nd:fig1}) and also sends/receives messages to/from the ND/P2P layer ($appSnd(m)$ and $appRcv(m)$ in Figure \ref{fig:nd:fig1}). We assume that the set of applications in the application layer at node $p_i$ do not send messages to node $p_j$ if the most recent link state event with respect to $p_j$ is not $LU(j)$.  For simplicity, we also assume that the set of applications in the application layer send messages to the ND/P2P layer at a rate that does not overflow the $k$-bounded send buffer.  This assumption can be implemented by a hand-shaking mechanism between the applications and the ND/P2P layer.

An execution $\gamma$ is a sequence of events happening in the system where the events are either application events ($appSnd(m)$ and $appRcv(m)$ in Figure \ref{fig:nd:fig1}), link state events ($LU(j)$, $LHU(j)$, and $LD(j)$ in Figure \ref{fig:nd:fig1}), abstract MAC layer events ($bcast(m)$, $rcv(m)$, and $ack(m)$ in Figure \ref{fig:nd:fig1}), or internal events (timers expiring at each nodes).  Each event in $\gamma$ is associated with the real time at which it occurs.  Additional constraints on the execution, that are related to the problem of neighbor detection, will be given in  Section \ref{sec:nd:probspec}.

%Let $\gamma_i$ be the projection of $\gamma$ onto the events of node $p_i$.  Two or more events in the system may happen at the same time in $\gamma$, however, each event in $\gamma_i$ should be associated with a unique non-zero time.  Additional constraints on the execution, that are related to the problem of neighbor detection, will be given in the next section. 

\section{The Problem Specification}
\label{sec:nd:probspec}

Let $LS^t_i(j)$ refer to the most recent link state event occurring at node $p_i$ with respect to node $p_j$ at or before time $t$.  $LS^t_i(j)$ can be either $LU$ (link up), $LHU$ (link half up), or $LD$ (link down).  %Similarly, from $p_i$'s perspective, let $RLS^t_i(j)$ refer to the most recent link state event with respect to $p_j$ at real time $t$.    

For any execution $\gamma$ of the system, we require the following constraints on $\gamma$:
\begin{compactitem}
\item (\emph{Usability}) An application send ($appSnd(m)$ in Figure \ref{fig:nd:fig1}) should not occur unless the current link state is $LU$ and an application receive ($appRcv(m)$ in Figure \ref{fig:nd:fig1}) should not occur if the current link state is $LD$.
\item (\emph{Validity}) For all real times $t$, if $LS^t_i(j)=LU$, then $p_i$ and $p_j$ are within each other's communication radius at time $t$.
\item (\emph{Well-formedness}) For all real times $t$ and $t'$ where $t<t'$, suppose $LS^t_i(j)=LU$ and $LS^{t'}_i(j)=LD$.  Then there exists a real time $t''\in(t,t')$ such that $LS^{t''}_i(j)=LHU$; The link state does not change directly from $LU$ to $LD$.
\item (\emph{Progress}) There exists positive reals $x_p$, $\alpha_p'$, and $\alpha_p''$ where $\alpha_p' \leq \alpha_p''$ such that, for every real $\alpha_p \geq 0$, if the distance between two nodes $p_i$ and $p_j$ is at most $x_p$ for a time duration of $[t,t+\alpha_p]$ (in real time), then both $LS^{t'}_i(j)=LU$ and $LS^{t'}_j(i)=LU$ for all times $t' \in [t+\alpha_p',t+\alpha_p+\alpha_p'']$ (in real time); Roughly speaking, this property says that if two nodes $p_i$ and $p_j$ stays close enough with each other, then there is a time in the near future where both $p_i$ and $p_j$ will be link up with each other.
\item (\emph{Reliable Delivery}) Each application send has a subsequent matching application receive and each application receive has exactly one preceding application send.
\end{compactitem}

\section{The Neighbor Detection Algorithm}
\label{sec:nd:algorithm}

We consider an algorithm where periodic hello messages are utilized in establishing communication links.  The algorithm uses two parameters, $h$ and $b$ (in addition to $\rho$, $\sigma$, $F^{+}_{rcv}$, and $F^{+}_{ack}$), which we explain next.  We assume that the value of the hello period duration $h$ in clock time is known to all nodes in the system.   We select the hello period $h$ to satisfy $h \geq (b+2)F^{+}_{ack} \cdot \frac{1+\rho}{1-\rho}$ where $b$ is a parameter which indicates the maximum number of application message broadcasts to the AML that we want to allow during a hello period considering each broadcast taking $F^{+}_{ack}$ amount of real time.  Each hello message of node $p_i$ consists of the following five fields: 1) $id$ : node id of $p_i$; 2) $location$ : $p_i$'s location when the hello message is generated; 3) $radius$ : communication radius of $p_i$; 4) $neighbors$ : $p_i$'s current neighbor set (all nodes $p_j$ where $LS_i(j)$ is either $LU$ or $LHU$); 5) $remaining$ : an array where $remaining[j]$ indicates the amount of local clock time left until reaching the time that the applications of $p_i$ should stop sending messages to node $p_j$. 

To allow hello messages to be sent to the AML every $h$ local time units while satisfying the well-formedness condition of the AML, we disallow application messages to be sent to the AML in the local time duration of $[t-(1+\rho)F^{+}_{ack},t]$ where $t$ is each local time the hello message is scheduled to be sent to the AML (note that the amount of local time $(1+\rho)F^{+}_{ack}$ in real time is always greater than or equal to the amount of real time $F^{+}_{ack}$). We call this time duration the \emph{pre-hello} interval.   Note that since we are assuming clock drift, nodes may generate hello messages at different times (in real time). 
\begin{comment}
\begin{itemize}
\item $id$ : node id of $p_i$.
\item $location$ : $p_i$'s location when the hello message is generated.
\item $radius$ : communication radius of $p_i$.
\item $neighbors$ : $p_i$'s current neighbor set (all nodes $p_j$ where $LS_i(j)$ is either $LU$ or $LHU$).
\item $remaining$ : an array; $remaining[j]$ indicates the amount of local clock time left until reaching the time that the applications of $p_i$ should stop sending messages to node $j$.
\end{itemize}
\end{comment}

For our algorithm, we assume that $kF^{+}_{ack} \geq h/(1+\rho)$.  We also assume the following functions for our algorithm:nd:
\begin{compactitem}
\item Loc(): returns the current location; provided by the GPS.
\item LC() : returns the current local clock time.
\item closeEnough($loc_1,rad_1,loc_2,rad_2$) : returns true \emph{iff} the following formula is satisfied : \\$dist(loc_1,loc_2) + 2\sigma((h/(1-\rho)+F^{+}_{rcv}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack})\cdot\frac{1+\rho}{1-\rho} + kF^{+}_{ack} + F^{+}_{rcv})\leq \min(rad_1, rad_2)$  where function $dist(\phi_1,\phi_2)$ returns the Euclidean distance between location $\phi_1$ and $\phi_2$.
\begin{compactitem}
\item $2\sigma$ corresponds to the maximum speed in which two nodes moving away from each other.
\item In our algorithm, closeEnough() is called at some node $p_i$ only when a hello message is received from some other node $p_j$.  The parameters passed to closeEnough() are $p_i$'s current location, $p_i$'s communication radius, $p_j$'s location when the hello message was generated, and $p_j$'s communication radius.  If closeEnough() returns true at $p_i$, then $p_i$ sets a deadline of which $p_i$ should stop sending application messages to $p_j$.  The deadline is determined under the condition that before the deadline is reached, the next hello message from $p_j$ should be received by $p_i$.  In the above formula, $(h/(1-\rho)+F^{+}_{rcv})\cdot\frac{1+\rho}{1-\rho}$ accounts for the amount of time (in real time) in reaching this deadline (in every $h$ local time units a hello message is generated and it takes at most $F^{+}_{rcv}$ (real) time to receive the hello message).
\item An additional $F^{+}_{rcv}$ accounts for the time the hello message of $p_j$ was in transit.
\item $kF^{+}_{ack} + 2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}$ accounts for the total (real) time in emptying the $k$-bounded send buffer if the buffer is full.  $kF^{+}_{ack}$ corresponds to the maximum overhead in emptying the $k$-bounded send buffer when application message broadcast has is no interference with control (hello) message broadcast.  However, since, in our case, hello messages are broadcast every $h$ local time units, hello message broadcasts may interfere with application message broadcasts. $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}$ accounts for the total time of hello messages interfering with the $k$ consecutive messages in the send buffer.  This is because $\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil$ corresponds to the maximum number of hello message broadcasts during $kF^{+}_{ack}$ amount of (real) time and for each hello message broadcast there is a pre-hello interval and a $F^{+}_{ack}$ time for receiving an ack for the transmitted hello message.
\item Now, suppose closeEnough() returned true at $p_i$ by receiving a hello message generated by $p_j$.  We can deduce from the above that $p_j$ will receive $p_i$'s application messages that were sent before reaching the deadline since even after $p_i$ sends an application message just before the deadline, $p_i$ and $p_j$ will be within each other's communication radius for a time duration of emptying the $k$-bounded send buffer even though $p_i$ and $p_j$ are moving away from each other in maximum speed.
\end{compactitem}    
	\begin{comment}
	\begin{itemize}
	\item The function $dist(\phi_1,\phi_2)$ returns the Euclidean distance between location $\phi_1$ and $\phi_2$.
	\item $2\sigma$ corresponds to the maximum speed in which two nodes moving away from each other.
	\item $h/(1-\rho)+F^{+}_{rcv}$ corresponds to the amount of real time where if node $p_i$ is within $p_j$'s communication radius for $h/(1-\rho)+F^{+}_{rcv}$ real time units, then $p_i$ is guaranteed to receive $p_j$'s hello message (see Lemma \ref{lem:nd:helloRecv} in Section \ref{sec:nd:proofCorrect}). 
	\item $kF^{+}_{ack}$ corresponds to the upper bound on the total time (in real time) of emptying the $k$-bounded send buffer if the buffer is full.
	\item $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}$ corresponds to the upper bound on the total time (in real time) of hello messages interfering with the transmission of $k$ consecutive messages in the send buffer. This is because within the real time duration of $kF^{+}_{ack}$ there could be at most $h/(1+\rho)$ hello message transmissions and for each hello message, there is a pre-hello interval and a $F^{+}_{ack}$ time for receiving an ack. 
	\end{itemize}
	\end{comment}
\end{compactitem}

Furthermore, we define the following macros for our algorithm : 
\begin{compactitem}
\item $Neighbors$ : \{$j~ |~ status[j]= LU$ or $LHU$\}
\item $SU_1$ : $rmn[i]\cdot\frac{1-\rho}{1+\rho}-(1+\rho)F^{+}_{rcv}$
\item $RU_1$ : If $rmn[i]\geq0$, then  $rmn[i]\cdot\frac{1+\rho}{1-\rho}+(1+\rho)(kF^{+}_{ack}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho})$. \\
$~~~~~~~~~$Otherwise, $rmn[i]\cdot\frac{1-\rho}{1+\rho}+(1+\rho)(kF^{+}_{ack}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho})$.
\item $SU_2$ : $h \cdot \frac{1+\rho}{1-\rho} + (1+\rho)F^{+}_{rcv}$
\item $RU_2$ : $h \cdot \frac{1+\rho}{1-\rho} + (1+\rho)(F^{+}_{rcv}+kF^{+}_{ack}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho})$
\end{compactitem}

Formulas $SU_1$, $RU_1$, $SU_2$, and $RU_2$ are used in the algorithm when a hello message is received.  We first explain $SU_2$ and $RU_2$.  Suppose node $p_i$ receives a hello message from $p_j$ and closeEnough() returned true at $p_i$ at $p_i$'s local time $t$.  Then, the deadline for $p_i$ to stop sending application messages to $p_j$ is set as $t+SU_2$ (called the \emph{sending deadline}) and the deadline for $p_i$ to even stop receiving application messages from $p_j$ is set as $t+RU_2$ (called the \emph{receiving deadline}).  $SU_2$ and $RU_2$ are both based on the formula that makes closeEnough() to return true.  However, they refer to local clock time rather than real time.  First, note that $SU_2$ corresponds to the amount of (local) time of $p_i$ receiving $p_j$'s next hello message even if $p_i$'s clock runs at the fastest rate and $p_j$'s clock runs at the slowest rate.  Next, note that $SU_2/(1-\rho) = (h/(1-\rho)+F^{+}_{rcv})\cdot\frac{1+\rho}{1-\rho}$.  This means that even if $p_i$'s clock runs at the slowest rate, the amount of local time $SU_2$ in real time will not exceed the amount of real time $(h/(1-\rho)+F^{+}_{rcv})\cdot\frac{1+\rho}{1-\rho}$. So, since closeEnough() returned true, we can deduce that $p_j$ will receive $p_i$'s application messages that were sent before reaching $t+SU_2$.  Formula $RU_2$ simply considers the amount of (local) time in emptying the $k$-bounded send buffer after the sending deadline $t+SU_2$.

We now explain $SU_1$ and $RU_1$. Suppose node $p_i$ receives a hello message $hello_j$ from $p_j$ at $p_i$'s local time $t$ where $i \in hello_j.neighbors$ ($p_i$ was considered as $p_j$'s neighbor at the time when $hello_j$ was generated).  Then, formulas $SU_1$ and $RU_1$ are used in setting the sending and receiving deadlines at $p_i$ (as $t+SU_1$ and $t+RU_1$, respectively) referring to $hello_j.remaining[i]$ (=$rmn[i]$) which was set based on $p_j$'s local clock.  Setting $p_i$'s deadlines in this way is to allow $p_i$ to consider $p_j$ as its neighbor even though closeEnough() did not return true ($p_i$ gets a chance to send application messages to $p_j$).   Since $p_i$'s clock and $p_j$'s clock may run at different rates, $p_i$ can only \emph{estimate} the deadlines set at $p_j$.  In estimating $p_j$'s sending deadline, it is important that $p_i$ does \emph{not} set its sending deadline to be greater than $p_j$'s sending deadline when both deadlines are transformed into real time.  Formula $SU_1$ guarantees this since 1) the amount of $p_i$'s local time $(hello_j.remaining[i])\cdot\frac{1-\rho}{1+\rho}$ in real time does not exceed  the amount of $p_j$'s local time $hello_j.remaining[i]$ in real time even if $p_i$'s clock runs at the slowest rate and $p_j$'s clock runs at the fastest rate, and 2) it also considers the maximum (local) time $hello_j$ might have been in transit ($(1+\rho)F^{+}_{rcv}$). In determining $p_i$'s receiving deadline, it is important that $p_i$'s receiving deadline is set such that $p_i$ receives all application messages from $p_j$ that was sent before reaching $p_j$'s sending deadline. Formula $RU_1$ guarantees this since, in calculating the $p_i$'s receive deadline, $p_i$ first considers the greatest possible value of the sending deadline in local time referring to $hello_j.remaining[i]$ (the situation where $hello_j$ is instantaneously received by $p_i$ and $p_i$'s clock runs at the fastest rate (resp. slowest rate) while $p_j$'s clock runs at the slowest rate (resp. fastest rate) considering $hello_j.remaining[i] \geq 0$ (resp. $hello_j.remaining[i] < 0$)) and then adds the the amount of (local) time in emptying the $k$-bounded send buffer.

We now describe the neighbor detection algorithm (the ND/P2P layer of node $p_i$).  The pseudocode is given in Figures \ref{fig:nd:alg1} and \ref{fig:nd:alg2}.

\begin{figure}[tp]
\centering
\begin{framed}
\begin{algorithmic}[1]
\item[] $\langle${\bf Variables and Initialization}$\rangle$
\STATE $R \la$ communication radius of node $p_i$;
\STATE $sendUntil$; \COMMENT{array[1..$n$]; initialized to 0}
\STATE $receiveUntil$; \COMMENT{array[1..$n$]; initialized to 0}
\STATE $remaining$; \COMMENT{array[1..$n$]; initialized to 0}
\STATE $sendQueue$; \COMMENT{the $k$-bounded send queue; initialized to $\emptyset$}
\STATE $recvBuff$; \COMMENT{array[1..$n$] of queues; initialized to $\emptyset$}
\STATE $state$; \COMMENT{array[1..$n$]; initialized to $LD$}
\EMPTY \hrulefill
\EMPTY

\STATE $\langle${\bf When} LC() is a multiple of $h\rangle$
\STATE $\forall j \in Neighbors$ : $remaining[j] \la sendUntil[j] - \mbox{LC()}$;
\EMPTY\COMMENT{send a hello msg to AML}
\STATE broadcast $hello(i,\mbox{Loc()},R,Neighbors,remaining)$; %\COMMENT{send hello msg to AML}
\EMPTY

\STATE $\langle${\bf When} $hello(j,loc,rad,nbrs,rmn)$ is received$\rangle$
\IF{$i \in nbrs$}
	\STATE updateDeadlines($j$, $\mbox{LC()}+SU_1$, $\mbox{LC()}+RU_1$); \label{line:nd:uDL1}
\ENDIF
\IF{closeEnough(Loc(),$R$,$loc$,$rad$)} \label{line:nd:closeEnough}
	\STATE updateDeadlines($j$, $\mbox{LC()}+SU_2$, $\mbox{LC()}+RU_2$); \label{line:nd:uDL2}
\ENDIF
\EMPTY

\STATE $\langle${\bf When} LC() $=sendUntil[j]\rangle$
\STATE $state[j] \la LHU$; \label{line:nd:assignLHU}
\STATE enable $LHU(j)$; \COMMENT{an event that goes to the application layer}
\EMPTY

\STATE $\langle${\bf When} LC() $=recvUntil[j]\rangle$
\STATE $state[j] \la LD$; \label{line:nd:assignLD}
\STATE enable $LD(j)$; \COMMENT{an event that goes to the application layer}
\EMPTY

\STATE $\langle${\bf When} app msg $m$ is received from application layer$\rangle$
\STATE enqueue($sendQueue$,$m$);
\end{algorithmic}
\end{framed}
\caption{ND/P2P layer; code for node $p_i$ (part 1 of 2).}
\label{fig:nd:alg1}
\end{figure}

\begin{figure}[tp]
\centering
\begin{framed}
\begin{algorithmic}[1]
\setalglineno{24}
\STATE $\langle${\bf When} ($sendQueue \neq \emptyset$) $\wedge$ (LC() is not in a pre-hello interval) $\wedge$
\item[] ~($p_i$ is not waiting for an ack of a previously broadcast msg from the AML)$\rangle$
\STATE broadcast dequeue($sendQueue$); \COMMENT{send to AML}
\EMPTY

\STATE $\langle${\bf When} app msg $m$ is received from $p_j \rangle$
\IF{$m$ is destined for $p_i$}
	\IF{$state[j] \neq LD$} \label{line:nd:appRecvCond}
		\STATE deliver $m$ to application layer; \label{line:nd:appRecv}
	\ELSE
		%\EMPTY\COMMENT{store msgs that arrived ``early''}
		\STATE enqueue($recvBuff[j]$,$m$); \label{line:nd:appMsgEnQ} \COMMENT{store msgs that arrived ``early''}
	\ENDIF
\ENDIF
\EMPTY

\PROC{updateDeadlines($j$, $s$, $r$)}
\IF{$sendUntil[j] < s$} \label{line:nd:updateCondSend}
	\STATE $sendUntil[j] \la s$;
	\IF{$state[j] \neq LU$}
		\STATE $state[j] \la LU$; \label{line:nd:assignLU}
		%\EMPTY\COMMENT{deliver msgs that arrived ``early''}
		\STATE deliverPendingAppMsgs($j$); \label{line:nd:deliverMsg1} \COMMENT{deliver msgs that arrived ``early''}
		\STATE enable $LU(j)$; \COMMENT{an event that goes to the application layer}
	\ENDIF
\ENDIF
\IF{$recvUntil[j] < r$} \label{line:nd:updateCondRecv}
	\STATE $recvUntil[j] \la r$;
	\IF{$state[j]= LD$} \label{line:nd:ifLD}
		\STATE $state[j] \la  LHU$; \label{line:nd:assignLHUfromLD}
		%\EMPTY\COMMENT{deliver msgs that arrived ``early''}
		\STATE deliverPendingAppMsgs($j$); \label{line:nd:deliverMsg2} \COMMENT{deliver msgs that arrived ``early''}
		\STATE enable $LHU(j)$; \COMMENT{an event that goes to the application layer}
	\ENDIF
\ENDIF
\ENDPROC
\EMPTY

\PROC{deliverPendingAppMsgs($j$)}
\STATE deliver each app msg in $recvBuff[j]$ to application layer;
\ENDPROC
\end{algorithmic}
\end{framed}
\caption{ND/P2P layer; code for node $p_i$ (part 2 of 2).}
\label{fig:nd:alg2}
\end{figure}

There are seven main variables used in the algorithm: 1) $R$ stores the communication radius of node $p_i$, 2) $sendUntil$ is an array where $sendUntil[j]$ indicates the local time that the applications of $p_i$ should stop sending messages to node $p_j$ (the sending deadline), 3) $receiveUntil$ is an array where $receiveUntil[j]$ indicates the local time that the applications of $p_i$ should stop receiving messages from node $p_j$ (the receiving deadline), 4) $remaining$ is an array that is only temporarily used when a hello message is constructed where $remaining[j]$ indicates the local time remaining until applications of $p_i$ should stop sending messages to node $p_j$, 5) $sendQueue$ corresponds to the $k$-bounded send queue, 6) $recvBuff$ is an array of queues where $recvBuff[j]$ stores the messages received by $p_j$ when the link state is $LD$, and finally 7) $state$ is an array where $state[j]$ indicates the current link state with respect to $p_j$.

In every $h$ local time units, a hello message is broadcasted (sent to the AML).  When node $p_i$ receives a hello message from node $p_j$, $p_i$ first checks if the hello message contains the information regarding $p_i$ being $p_j$'s neighbor.  If so, then $p_i$ attempts to update $sendUntil[j]$ and $recvUntil[j]$ by calling updateDeadlines().  The parameter values passed to updateDeadlines() are \emph{estimates} of $sendUntil[i]$ and $recvUntil[i]$ at $p_j$ (LC()+$SU_1$ and LC()+$RU_1$). Procedure updateDeadlines() only allows $sendUntil[j]$ and $recvUntil[j]$ to be updated when the parameters passed to updateDeadlines() is greater than $sendUntil[j]$ and/or $recvUntil[j]$.  If $sendUntil[j]$ gets to be updated, then the link state with respect to $p_j$ either remains or changes to $LU$.  And, if $recvUntil[j]$ gets to be updated, then the link state with respect to $p_j$ either remains or changes to $LU$ or $LHU$.  If the link state with respect to $p_j$ \emph{changed} to $LU$ or $LHU$, then each application message from $p_j$ in $recvBuff[j]$ (messages that arrived ``early'' from $p_j$) will be delivered to the application layer.

If $p_i$ receives a hello message from node $p_j$ and a call to closeEnough() returns true (line \ref{line:nd:closeEnough} in Figure \ref{fig:nd:alg1}), then updateDeadlines() is called with different parameter values than the values mentioned in the previous paragraph.  These parameter values (LC()+$SU_2$ and LC()+$RU_2$) guarantee that the link state will be $LU$ (if it was not already $LU$) and while the link state is $LU$, $p_i$ will receive $p_j$'s next hello message (see Lemmas \ref{lem:nd:distCond} and \ref{lem:nd:helloRecv} in Section \ref{sec:nd:proofCorrect}).

If the sending deadline with respect to node $p_j$ is reached (LC()=$sendUntil[j]$) at $p_i$, then $p_i$ changes its link state with respect to $p_j$ to $LHU$.  This stops applications from sending messages to $p_j$ while still allows them to receive messages from $p_j$.  And, if the receiving deadline with respect to node $p_j$ is reached (LC()=$recvUntil[j]$) at $p_i$, then $p_i$ changes its link state with respect to $p_j$ to $LD$.  This makes the applications of $p_i$ to stop sending and receiving messages regarding $p_j$. 

When an application message is received by the application layer, then the message is simply enqueued in the $k$-bounded send buffer $sendQueue$.

In order to broadcast a message in the $sendQueue$ (sending it to AML), the following three conditions must be satisfied: 1) $sendQueue$ must not be empty, 2) the current local time (LC()) must not be in the pre-hello interval, 3) the ND/P2P layer must not be waiting for an ack of a previously broadcast message from the AML (this is to conform with the well-formedness condition of the AML).

When an application message is received from node $p_j$ at $p_i$, then depending on the current link state, the received message is either directly delivered to the application or stored in $recvBuff[j]$: if the current link state is $LU$ or $LHU$, then deliver the received message to the application layer; otherwise, store it in $recvBuff[j]$ for later delivery when the link becomes either $LU$ or $LHU$.  This is to prevent applications from receiving messages while the current link state is $LD$.


\section{Proof of Correctness}
\label{sec:nd:proofCorrect}

An overview of the proofs is as follows.  Our objective is to prove that the five properties mentioned in Section \ref{sec:nd:probspec} are satisfied.  The usability property (Lemma \ref{lem:nd:usability}) is trivially proven by inspecting the code.  In proving the well-formedness property (Theorem \ref{thm:nd:wellformed}), we show that when a node is link up with some other node $p_j$, the deadline for sending messages to $p_j$ is reached (causing the link state to change to $LHU$) prior to changing the link state with respect to $p_j$ to $LD$ by utilizing the fact that the link is up with respect to $p_j$ at time $t$ if and only if the deadline for sending messages to $p_j$ is some time after $t$ (Lemma \ref{lem:nd:linkUpIff}).  

The proof of the validity property (Theorem \ref{thm:nd:validity}) is based on how the deadline for sending messages to a certain node is set (again using Lemma \ref{lem:nd:linkUpIff}).  There are two ways in setting the deadline: executing line  \ref{line:nd:uDL2} or line  \ref{line:nd:uDL1} of Figure \ref{fig:nd:alg1}.  In the case of executing line  \ref{line:nd:uDL2}, we show the desired result by using the fact that the function closeEnough() returning true has the meaning of two nodes being within each other's communication radius for a certain time duration (Lemma \ref{lem:nd:distCond}).  In the case of executing line  \ref{line:nd:uDL1}, we reason about how formula $SU_1$ gives us the desired result.

The proof of the progress property (Theorem \ref{thm:nd:progress}) is based on the fact that when two nodes are close enough, they will receive each other's hello message (Lemma \ref{lem:nd:helloRecv}) even though they move away from each other and by receiving each other's hello message, function closeEnough() will return true which will cause the link state to be $LU$ for both nodes.

In proving the reliable delivery property (Theorem \ref{thm:nd:onetoone}), we first use the \emph{no duplication} property of the AML (no two receive events are caused by the same broadcast event) to show that no two application receives are caused by the same application send.  Then, we show that application messages sent to $p_j$ by $p_i$ while the link is up are guaranteed to be received by the ND/P2P layer of $p_j$.  Finally it is shown that the application message at the ND/P2P layer of $p_j$ will be delivered to the application layer of $p_j$.    

Throughout the analysis, we denote the value of variable $var$ of node $p_i$ at time $t$ as $var^t_i$.  Fix $\gamma$ to be an arbitrary execution of the algorithm in Figures \ref{fig:nd:alg1} and \ref{fig:nd:alg2}.

By the assumption that an application send occurs only when the current link state is up and by the fact that an application receive does not occur while the link state is $LD$ (line \ref{line:nd:appMsgEnQ} of the pseudocode), we immediately get the following lemma:

\begin{lemma}
\label{lem:nd:usability}
$\gamma$ satisfies the usability property.
\end{lemma}

The next lemma shows that the values of both $sendUntil$ and $recvUntil$ does not decrease over time.

\begin{lemma}
\label{lem:nd:nondecreasing}
For all nodes $p_i$ and $p_j$ and for all times $t$ and $t'$ where $t\leq t'$, $sendUntil^t_i[j] \leq sendUntil^{t'}_i[j]$ and $recvUntil^t_i[j] \leq recvUntil^{t'}_i[j]$.
\end{lemma}
\begin{proof}
The proof is straightforward from the fact that (1) the only way to update $sendUntil_i[j]$ and/or $recvUntil_i[j]$ is by calling updateDeadlines(), and (2) updateDeadline() only allows updates to $sendUntil_i[j]$ and/or $recvUntil_i[j]$ when a greater parameter value is passed to it (lines \ref{line:nd:updateCondSend} and \ref{line:nd:updateCondRecv}).
\end{proof}

The following lemma and corollary shows that at any given time, the value of $sendUntil[j]$ is at most the value of $recvUntil[j]$.

\begin{lemma}
\label{lem:nd:sendLessRecv}
Suppose, at time $t_1$, updateDeadlines($j,\_,\_$) is executed for the first time at node $p_i$ by receiving a hello message from node $p_j$. Then, $sendUntil^t_i[j] < recvUntil^t_i[j]$ for all times $t \geq t_1$. 
\end{lemma}
\begin{proof}
When updateDeadlines($j,s,r$) is called at lines \ref{line:nd:uDL1} or \ref{line:nd:uDL2} at some time $t'$, we have $0<s<r$ since $0<t'+SU_1<t'+RU_1$ and $0<t'+SU_2<t'+RU_2$.  Since the only way to update $sendUntil_i[j]$ and $recvUntil_i[j]$ is by calling updateDeadlines($j,\_,\_$) and since $sendUntil_i[j]$ and $recvUntil_i[j]$ is updated only when their current value is less than $s$ and $r$, respectively, it is straightforward that $sendUntil^t_i[j] < recvUntil^t_i[j]$ for all times $t \geq t_1$.
\end{proof}

\begin{corollary}
\label{cor:sendLessRecv}
For all nodes $p_i$ and $p_j$ and for all times $t$, $sendUntil^t_i[j] \leq recvUntil^t_i[j]$.
\end{corollary}
\begin{proof}
The proof is immediate from Lemma \ref{lem:nd:sendLessRecv} and the fact that for all nodes, the elements of $sendUntil$ and $recvUntil$ are initialized to $0$.
\end{proof}

The following lemma is the key lemma in proving the well-formedness and validity property which says that the link state is link up with respect to some node $p_j$ at a given time $t$ if and only if the value of $sendUntil[j]$ is greater than $t$.  

%This lemma uses Lemma \ref{lem:nd:nondecreasing} in getting a contradiction assuming $sendUntil[j]$ is less than or equal to $t$ in the \emph{if} direction and Corollary \ref{cor:sendLessRecv} in getting a contradiction assuming that the link state with respect to $p_j$ at time $t$ is not link up (the link state is either link half-up or link down) in the \emph{only if} direction.

\begin{lemma}
\label{lem:nd:linkUpIff}
For all nodes $p_i$ and $p_j$ and for all times $t$, $LS^t_i(j) = LU$ if and only if $sendUntil^t_i[j] > t$ (in $p_i$'s local time).
\end{lemma}
\begin{proof}
($\Rightarrow$) Suppose, in contradiction, that $sendUntil^t_i[j] \leq t$.  This implies that there exists a local time $t'(\leq t)$ such that $t'=sendUntil^t_i[j]$.  If $t'=0$, then we have $LS^{t'}_i(j)=LD$ by the initialization code.  If $t' \neq 0$, then we have $LS^{t'}_i(j)=LHU$ at local time $t'$ by line \ref{line:nd:assignLHU}.  Hence, at local time $t'$, we have a link state that is not $LU$.  Now, since $LS^{t}_i(j)=LU$, there exists a local time during $[t',t]$ where line \ref{line:nd:assignLU} is executed.  In order to execute \ref{line:nd:assignLU}, $sendUntil_i[j]$ must have been modified to a greater value than $t'$ during $[t',t]$.  Since $sendUntil_i[j]$ is nondecreasing over time by Lemma \ref{lem:nd:nondecreasing}, it must be that $sendUntil^t_i[j] > t'$, a conradiction.\\
($\Leftarrow$) Suppose, in contradiction, that $LS^t_i(j) \neq LU$. We distinguish two cases:\\
--(\emph{Case} 1; $LS^t_i(j) = LD$): In this case, we have either $sendUntil^t_i[j]=0$ by the initialization code or $recvUntil^t_i[j] \leq t$ by the fact that the only case the link state becomes $LD$ is when LC()$=recvUntil_i[j]$ (line \ref{line:nd:assignLD}).  If $sendUntil^t_i[j]=0$, then we directly get a contradiction since $sendUntil^t_i[j]>t\geq0$.  If $recvUntil^t_i[j] \leq t$, then by Corollary \ref{cor:sendLessRecv}, $sendUntil^t_i[j] \leq recvUntil^t_i[j] \leq t$, a contradiction.\\
--(\emph{Case} 2; $LS^t_i(j) = LHU$): This case implies that there exists a time prior or equal to time $t$ such that the link state became $LHU$.  Let $t'(\leq t)$ be the latest local time that the link state became $LHU$.  By the code, either line \ref{line:nd:assignLHUfromLD} or \ref{line:nd:assignLHU} was executed at time $t'$.  Also, since the link state remains as $LHU$ during $[t',t]$, we have $sendUntil^{t'}_i[j] = sendUntil^t_i[j]$.  If line \ref{line:nd:assignLHU} was executed at time $t'$, then it is straightforward that $t'=sendUntil^{t'}_i[j]$.  Thus, we get $sendUntil^t_i[j] = t' \leq t$, a contradiction.  If line \ref{line:nd:assignLHUfromLD} was executed at time $t'$, then the latest link state prior to time $t'$ must have been $LD$ by line \ref{line:nd:ifLD}.  This implies that there exists a time prior to time $t'$ such that the link state became $LD$.  Let $t''(<t')$ be the latest local time that the link state became $LD$.  We have $recvUntil^{t''}_i[j]=t''$ by line \ref{line:nd:assignLD}.  During $[t'',t')$ updateDeadlines() must not have been called because otherwise the link state must have changed to either $LU$ or $LHU$ by the fact that $sendUntil^{t''}_i[j] \leq recvUntil^{t''}_i[j]=t''$ (Corollary \ref{cor:sendLessRecv}) and the fact that updateDealine() is called with parameters that have a values greater than the current local time value.  Moreover, the if-condition at line \ref{line:nd:updateCondSend} should have been evalutated to false because otherwise the if-condition at line \ref{line:nd:ifLD} would have evaluated to false.  Hence, $sendUntil_i[j]$ was not updated during $[t'',t']$ and we get $sendUntil^{t''}_i[j] = sendUntil^{t'}_i[j] = sendUntil^t_i[j]$.  Therefore, since $sendUntil^{t''}_i[j] \leq recvUntil^{t''}_i[j]=t''$, we finally get $sendUntil^t_i[j] \leq t'' < t$, a contradiction.
\end{proof}

The following theorem shows that the well-formedness property holds.  It uses both lemmas \ref{lem:nd:sendLessRecv} and \ref{lem:nd:linkUpIff} in obtaining a contradiction in the situation where the link state changes directly from $LU$ to $LD$.

\begin{theorem}
\label{thm:nd:wellformed}
$\gamma$ satisfies the well-formedness property.
\end{theorem}
\begin{proof}
Suppose, for two nodes $p_i$ and $p_j$, that $LS^t_i(j)=LU$ and $LS^{t'}_i(j)=LD$ where $t < t'$ in real time.  Now, suppose, in contradiction, that for all real times $t''\in(t,t')$, $LS^{t''}_i(j) \neq LHU$.  Since $LS^{t'}_i(j)=LD$, we have $recvUntil^{t'}_i[j] \leq t'$ in real time.  Also, since $LS^t_i(j)=LU$, we know that updateDeadlines() is called at least once.  So, by Lemma \ref{lem:nd:sendLessRecv} and Lemma \ref{lem:nd:linkUpIff}, we get $t < sendUntil^{t'}_i[j] < recvUntil^{t'}_i[j] \leq t'$ in real time.  This implies that there exists a real time $t_1\in(t,t')$ such that $sendUntil^{t_1}_i[j] = t_1$ in real time which results in executing line \ref{line:nd:assignLHU}, a contradiction.
\end{proof}

The next lemma shows that the function closeEnough() returning true has the meaning of two nodes being within each other's communication radius for a certain time duration. 

\begin{lemma}
\label{lem:nd:distCond}
Suppose, at real time $t$, node $p_i$ received a hello message from node $p_j$ and closeEnough() returned true.  Then, $p_i$ and $p_j$ will be in each other's communication radius during $[t,t+T]$ in real time where $T=(h/(1-\rho)+F^{+}_{rcv}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack})\cdot\frac{1+\rho}{1-\rho}+kF^{+}_{ack}$. 
\end{lemma}
\begin{proof}
If instantaneous message delivery is assumed, the condition that needs to be satisfied for closeEnough() to return true simply guarantees that $p_i$ and $p_j$ remain in each other's communication radius during $[t,t+T+F^{+}_{rcv}]$ in real time even though $p_i$ and $p_j$ moves in the maximum speed (=$\sigma$) away from each other.  However, in our case, the hello message generated by $p_j$ might have took $F^{+}_{rcv}$ real time to reach $p_i$.  Hence, we can say that $p_i$ and $p_j$ will be in each other's communication radius during $[t,t+T]$ in real time.
\end{proof}

The following theorem shows that the validity property holds.  Using Lemma \ref{lem:nd:linkUpIff}, the proof is based on how $sendUntil_i[j]$ is set at $p_i$.  

%As already mentioned in the overview of proofs, if $sendUntil_i[j]$ was set by executing line  \ref{line:nd:uDL2} of Algorithm \ref{fig:nd:alg1}, then Lemma \ref{lem:nd:distCond} is applied in getting the desired result.  Otherwise ($sendUntil_i[j]$ was set by executing line  \ref{line:nd:uDL1}), we reason about how formula $SU_1$ guarantees the desired result.

\begin{theorem}
\label{thm:nd:validity}
$\gamma$ satisfies the validity property.
\end{theorem}
\begin{proof}
First, let $T=(h/(1-\rho)+F^{+}_{rcv}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack})\cdot\frac{1+\rho}{1-\rho}+kF^{+}_{ack}$.  Suppose $LS^t_i(j) = LU$ at local time $t$.  By Lemma \ref{lem:nd:linkUpIff}, we know that $LS^t_i(j) = LU$ if and only if $sendUntil^t_i[j] > t$.  We distinguish two cases based on how $sendUntil_i[j]$ was set:\\
--(\emph{Case} 1; By line \ref{line:nd:uDL2} (at local time $t'$)): In this case, the call to closeEnough() returned true.  When closeEnough() returns true, it is guaranteed by Lemma \ref{lem:nd:distCond} that $p_i$ and $p_j$ remain in each other's communication radius for at least $T$ amount of time in real time from time $t'$.  At line \ref{line:nd:uDL2}, we set $sendUntil_i[j]=t'+SU_2$.  Since $0\leq\rho<1$, the amount of local time $SU_2$ in real time is always less than the amount of real time $T$.  Hence, $p_i$ and $p_j$ will remain in each other's communication radius until time $sendUntil_i[j]$ in $p_i$'s local time.\\
--(\emph{Case} 2; By line \ref{line:nd:uDL1}): In this case, $sendUntil_i[j]$ was updated by $hello_j.remaining[i]$.  For two nodes $p_i$ and $p_j$ where $LS^{t_1}_i(j)=LD$ and $LS^{t_1}_j(j)=LD$ for some real time $t_1$, respectively, line \ref{line:nd:uDL2} must be executed first to execute line \ref{line:nd:uDL1} since either $j\in Neighbors_i$ or $i \in Neighbors_j$ must first be satisfied to execute line \ref{line:nd:uDL1}.  Hence, for this case, it suffices to prove that (1) when $sendUntil_i[j]$ is set by executing line \ref{line:nd:uDL2} at $p_i$ at time $t$, $p_i$ and $p_j$ are within each other's communication radius until time $sendUntil^t_i[j]$ and (2) assuming that $hello_j$ was generated by $p_j$ at $p_j$'s local time $t_j$ and it is guaranteed that $p_i$ and $p_j$ remain within each other's communication radius at least until $t_j+hello_j.remaining[i]$ in $p_j$'s local time, if $sendUntil_i[j]$ is set by executing line \ref{line:nd:uDL1} at $p_i$ at time t, then $p_i$ and $p_j$ are within each other's communication radius until time $sendUntil^t_i[j]$.  Part (1) is already proven in (Case 1).  We focus on part (2).  By the code, $sendUntil_i[j]$ is set by the formula $t_i + hello_j.remaining[i]\cdot\frac{1-\rho}{1+\rho} - (1+\rho)F^{+}_{rcv}$ where $t_i$ is $p_i$'s local time when $p_i$ receives $hello_j$.  First note that $hello_j.remaining[i] >0$ because otherwise $sendUntil_i[j]$ will not have been set in the first place.  Since $0\leq\rho<1$, the amount of $p_j$'s local time $hello_j.remaining[i]$ in real time is always greater than or equal to the amount of $p_i$'s local time $hello_j.remaining[i]\cdot\frac{1-\rho}{1+\rho}$ in real time.  In worst case, $hello_j$ might have took $F^{+}_{rcv}$ real time from when $p_j$ generating $hello_j$ to $p_i$ receiving $hello_j$.  Again, since $0\leq\rho<1$, the amount of $p_i$'s local time $(1+\rho)F^{+}_{rcv}$ in real time is always greater than or equal to $F^{+}_{rcv}$ in real time.  Hence, we get that $p_j$'s local time $t_j+hello_j.remaining[i]$ in real time is greater than or equal to $p_i$'s local time $sendUntil^{t_i}_{i}[j]$ in real time.  Therefore, $p_i$ and $p_j$ will remain in each other's communication radius until time $sendUntil^{t_i}_i[j]$ in $p_i$'s local time.
\end{proof}

The following lemma shows how two nodes remaining in each other's communication radius for a specific time duration implies that both nodes will receive each other's hello message.

\begin{lemma}
\label{lem:nd:helloRecv}
Suppose nodes $p_i$ and $p_j$ remain in each other's communication radius for the entire time duration of $[t,t+h/(1-\rho)+F^{+}_{rcv}]$ in real time.  Then, $p_i$ and $p_j$ will receive at least one of each other's hello message during $[t,t+h/(1-\rho)+F^{+}_{rcv}]$ in real time.
\end{lemma}
\begin{proof}
Since the clock drift is bounded by $\rho$ where $0\leq\rho<1$ and each node generates and broadcasts a hello message every $h$ time units with respect to its local clock, each node generates and broadcasts at least one hello message during a time duration of size $h/(1-\rho)$ in real time (the amount of time $h/(1-\rho)$ in real time corresponds to the amount of local time $h$ for the node with the slowest clock rate).  Hence, considering the message delay bound $F^{+}_{rcv}$ in real time, $p_i$ and $p_j$ receive each other's hello message during $[t,t+h/(1-\rho)+F^{+}_{rcv}]$ in real time.
\end{proof}

The next theorem shows that the progress property holds for certain values of $x_p$, $\alpha_p'$, and $\alpha_p''$.

\begin{theorem}
\label{thm:nd:progress}
Let $DC=2\sigma(h/(1-\rho)+F^{+}_{rcv}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack})\cdot\frac{1+\rho}{1-\rho} +2\sigma(F^{+}_{rcv} + kF^{+}_{ack})$.  $\gamma$ satisfies the progress property with $x_p = min(R_i,R_j)-2\sigma(\frac{h}{1-\rho}+F^{+}_{rcv}) - DC$, $\alpha_p'=\frac{h}{1-\rho}+F^{+}_{rcv}$, and $\alpha_p''=\frac{h}{1-\rho} + F^{+}_{rcv}$.
\end{theorem}
\begin{proof}
Without loss of generality, suppose two nodes $p_i$ and $p_j$ are within distance $x_p$ at real time $t'$.  $dist(p_i,p_j) \leq x_p$ at time $t'$ guarantees that $p_i$ and $p_j$ remain in each other's communication radius for at least the amount of time $h/(1-\rho)+F^{+}_{rcv}$ in real time even though both $p_i$ and $p_j$ moves at a maximum speed ($\sigma$) away from each other.  Applying Lemma \ref{lem:nd:helloRecv}, we get that $p_i$ and $p_j$ receives each other's hello message during $[t',t'+h/(1-\rho)+F^{+}_{rcv}]$ in real time.  Furthermore, $dist(p_i,p_j) \leq x_p$ at time $t'$ also guarantees that by receiving the hello message during $[t',t'+h/(1-\rho)+F^{+}_{rcv}]$ in real time, the call to closeEnough() returns true causing the link state to be $LU$ if the link state was not $LU$ and the link state to remain in $LU$ otherwise.  

Now, without loss of generality, suppose that $p_i$ and $p_j$ are within distance $x_p$ for all times during $[t,t+\alpha_p]$ in real time.  By the above argument, it is clear that at real time $t+h/(1-\rho)+F^{+}_{rcv}$($=t+\alpha_p'$) the link state of both $p_i$ and $p_j$ are $LU$. Also, from real time $t+\alpha_p$ to real time $t+\alpha_p +\alpha_p''$, each call to closeEnough() will return true at both $p_i$ and $p_j$.  When closeEnough() returns true at $p_i$ (resp. $p_j$), $sendUntil_i[j]$ (resp. $sendUntil_j[i]$) is set to at least $SU_2$.  Considering the worst case, the amount of local time $SU_2$ can be at least $SU_2/(1+\rho)=\alpha_p''$ in real time.  Also, considering the worst case, closeEnough() might have returned true at time $t+\alpha_p$.  Hence, until real time $t+\alpha_p+SU_2/(1+\rho)=t+\alpha_p+\alpha_p''$, $LS_i(j)=LU$ and $LS_j(i) = LU$.  Therefore, we have $LS^{t_1}_i(j)=LU$ and $LS^{t_1}_j(i) = LU$ for all $t_1\in[t+\alpha_p',t+\alpha_p+\alpha_p'']$ in real time.   
\end{proof}

%Before proving the next theorem we define the following: we say that a node $p_i$ is \emph{indirectly close} to node $p_j$ if the most recent update to $sendUntil_i[j]$ was by executing line \ref{line:nd:uDL1} of Algorithm \ref{fig:nd:alg1}.  

The final theorem shows that the reliable delivery property holds.  

%The proof first uses the \emph{no duplication} property of the AML to show that it suffices to only prove that application messages sent to $p_j$ by $p_i$ while the link is up is guaranteed to be received by the application layer of $p_j$.  The proof continues by reasoning about how it is guaranteed that the ND/P2P layer of $p_j$ receives the application message and then finally it is shown that the application message will be delivered to the application layer of $p_j$ (eventually, the link state of $p_j$ with respect to $p_i$ will be either $LU$ or $LHU$). 

\begin{theorem}
\label{thm:nd:onetoone}
$\gamma$ satisfies the reliable delivery property.
\end{theorem}
\begin{proof}
The AML guarantees the \emph{no duplication} property.  This property says, for a node $p_k$, no two receive events at $p_k$ are caused by the same broadcast event.  Since the ND/P2P layer simply forwards application messages to the AML, we can say that, for a node $p_k$, no two application receives are caused by the same application send.  So, for the reliable delivery property, it only remains to prove that an application message sent from $p_i$ to $p_j$ while $p_i$'s link state is $LU$ with respect to $p_j$ is received by the application layer of $p_j$.

Without loss of generality, suppose node $p_i$ sends an application message at local time $t$ to node $p_j$ while $LS^{t}_i(j)=LU$.  Notice how $sendUntil_i[j]$ and $recvUntil_i[j]$ is set by lines \ref{line:nd:uDL1} and \ref{line:nd:uDL2}.  By the values of $SU_1$, $RU_1$, $SU_2$, and $RU_2$, $sendUntil_i[j]$ and $recvUntil_i[j]$ satisfies $sendUntil^{t'}_i[j] + (1+\rho)(kF^{+}_{ack}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}) \leq recvUntil^{t'}_i[j]$ for all local time $t'$.  If the last update to $sendUntil_i[j]$ before local time $t$ was by calling updateDeadlines() at line \ref{line:nd:uDL2}, then Lemma \ref{lem:nd:distCond} implies that, starting from local time $sendUntil^t_i[j]$, during the next $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}+kF^{+}_{ack}$ amount of time in real time, $p_i$ and $p_j$ will be within each other's communication radius.  Even if the the most recent update to $sendUntil_i[j]$ before local time $t$ was by calling updateDeadlines() at line \ref{line:nd:uDL1}, we still have that starting from local time $sendUntil^t_i[j]$, during the next $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}+kF^{+}_{ack}$ amount of time in real time, $p_i$ and $p_j$ will be within each other's communication radius. This is because formula $SU_1$ guarantees that $sendUntil^t_i[j]$ is set to a local time value such that the real time left for $p_i$ to reach the local time $sendUntil^t_i[j]$ is less than or equal to the real time left for $p_j$ to reach its local time $sendUntil^{t_j}_j[i]$ where $t_j$ is the local time of $p_j$ that is equal to $p_i$'s local time $t$ when both are transformed to real time (see the proof of Theorem \ref{thm:nd:validity} (Case 2)).

Now, recall that $kF^{+}_{ack}$ is the upper bound on the total real time of emptying the the $k$-bounded buffer if the buffer is full (when there is no control (hello) message interference) and $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}$ is the upper bound on the total real time of hello message transmissions interfering with $k$ consecutive application messages in the $k$-bounded send buffer.  Thus, a message already in the $k$-bounded send buffer is guaranteed to be sent to the AML within the amount of real time $kF^{+}_{ack}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}-F^{+}_{ack}$.  From the previous paragraph and by Lemma \ref{lem:nd:linkUpIff}, we therefore have that the ND/P2P layer of $p_j$ receives the application message sent by $p_i$ while $LS^{t}_i(j)=LU$.

%and $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}(1+\rho)$ is the upperbound on the total time (in local time) of hello message tranmissions interfering with $k$ consecutive application messages in the $k$-bounded send buffer.  Since $0\leq\rho<1$, the amount of local time $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}(1+\rho)$ in real time is less than or equal to the amount of real time $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}$.   So, we can say that a message in the $k$-bounded send buffer is guaranteed to be sent to the AML within the amount of time $kF^{+}_{ack}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}$ in real time.  Hence, from the previous paragraph and by Lemma \ref{lem:nd:linkUpIff}, we have that the ND/P2P layer of $p_j$ receives the application message sent by $p_i$ while $LS^{t}_i(j)=LU$.  

It remains to show that the application layer of $p_j$ receives the message by $p_i$.  Considering $p_i$, if $sendUntil^t_i[j]$ was set by calling updateDeadlines() at line \ref{line:nd:uDL2} at real time $t''$ ($p_i$'s local time $t$ in real time corresponds to $t''$), then by Lemma \ref{lem:nd:distCond} and \ref{lem:nd:helloRecv}, $p_j$ will receive $hello_i$ from $p_i$ until $t''+h/(1-\rho)+F^{+}_{rcv}$ in real time.  Upon $p_j$ receiving $hello_i$ from $p_i$ at $p_j$'s local time $t_j'$, the call to updateDeadline() at line \ref{line:nd:uDL1} and the value of $RU_1$ ensures that $recvUntil^{t_j'}_j[i]$ in real time is greater than or equal to $p_i$'s local time $sendUntil^t_i[j]$ in real time plus $kF^{+}_{ack}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}$ in real time.  Hence, for all $t_1 \in [t_j',recvUntil^{t_j'}_j[i])$ in $p_j$'s local time, $LS^{t_1}_j(i)\neq LD$ holds.  Thus, by lines \ref{line:nd:deliverMsg1}, \ref{line:nd:deliverMsg2}, and \ref{line:nd:appRecv}, the application message sent by $p_i$ will be delivered to $p_j$'s application layer.  Now, if $sendUntil^t_i[j]$ was set by calling updateDeadlines() at line \ref{line:nd:uDL1} at real time $t''$ ($p_i$'s local time $t$ in real time corresponds to $t''$), then, by formula $SU_1$, $sendUntil^{t}_i[j]$ in real time is less than $sendUntil^{t_j''}_j[i]$ in real time where $p_i$'s local time $t$ and $p_j$'s local time $t_j''$ have the same time value when both are transformed to real time.  Since $sendUntil^{t'}_j[i] + (1+\rho)(kF^{+}_{ack}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}) \leq recvUntil^{t'}_j[i]$ holds for all local times $t'$ and $LS^{t_2}_j(i)\neq LD$ holds for all local times $t_2 \in [sendUntil^{t'}_j[i],recvUntil^{t'}_j[i])$, lines \ref{line:nd:deliverMsg1}, \ref{line:nd:deliverMsg2}, and \ref{line:nd:appRecv} guarantee that the application message sent by $p_i$ will be delivered to $p_j$'s application layer.
\end{proof}

\section{Discussion}
\label{sec:nd:discussion}

In this section, we apply parameter values to obtain the maximum distance between two nodes that guarantee link up with each other and compare the results of different parameter values.

\begin{figure}[tp]
\centering
\includegraphics[scale=1.0]{figures/speed50.pdf}
\caption{Max distance between two nodes for guaranteed link up with each other ($x_p$ of Theorem \ref{thm:nd:progress}) when max speed is 50km/h.}
\label{fig:nd:fig2}
\end{figure}

\begin{figure}[tp]
\centering
\includegraphics[scale=1.0]{figures/speed100.pdf}
\caption{Max distance between two nodes for guaranteed link up with each other ($x_p$ of Theorem \ref{thm:nd:progress}) when max speed is 100km/h.}
\label{fig:nd:fig3}
\end{figure}

\begin{figure}[tp]
\centering
\includegraphics[scale=1.0]{figures/speed160.pdf}
\caption{Max distance between two nodes for guaranteed link up with each other ($x_p$ of Theorem \ref{thm:nd:progress}) when max speed is 160km/h.}
\label{fig:nd:fig4}
\end{figure}

%\begin{figure}[tp]
%\centering
%\subfloat[Max speed = 50km/h]{\label{fig:nd:fig2:50}\includegraphics[scale=0.8]{figures/speed50.pdf}}\\
%\subfloat[Max speed = 100km/h]{\label{fig:nd:fig2:100}\includegraphics[scale=0.8]{figures/speed100.pdf}}\\
%\subfloat[Max speed = 160km/h]{\label{fig:nd:fig2:160}\includegraphics[scale=0.8]{figures/speed160.pdf}}
%\caption{Max distance between two nodes for guaranteed link up with each other ($x_p$ of Theorem \ref{thm:nd:progress}) when max speed is 50km/h.}
%\label{fig:nd:fig2}
%\end{figure}

Figures \ref{fig:nd:fig2}, \ref{fig:nd:fig3}, and \ref{fig:nd:fig4} show the $x_p$ value (the maximum distance between two nodes to guarantee link up with each other) of Theorem \ref{thm:nd:progress} for different $F^{+}_{rcv}$ and $F^{+}_{ack}$ values and different $\sigma$ values by increasing the maximum number of broadcasts to the AML per hello period (parameter $b$; see Section \ref{sec:nd:algorithm}) given $R=250$ meters (typical value for IEEE 802.11 \cite{FZLLZG03,NHJ05}), $k=110$ (maximum size of the send buffer), $\rho=10^{-6}$, and $h=(b+2)F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}$.

Figure \ref{fig:nd:fig2} shows the $x_p$ value by ranging $b$ from $1$ to $100$ where nodes move in a maximum speed of $50$km/h (an urban area considering vehicles as nodes).  Expecting that $F^{+}_{rcv}$ and $F^{+}_{ack}$ to be tens of milliseconds (ms) and assuming that $F^{+}_{rcv}=F^{+}_{ack}$, we have considered three cases for the values of $F^{+}_{ack}$: $10$ms, $20$ms, and $50$ms.  For the cases of $10$ms and $20$ms, the $x_p$ values stay above $160$ meters and $71$ meters, respectively, even though $b=100$.  For the case of $50$ms, the $x_p$ value hits its maximum value $34.7203$ meters when $b=8$ and we also get that $x_p > 0$ only when $b$ ranges from $2$ to $27$.  So, Figure \ref{fig:nd:fig2} shows that a large $x_p$ value can be obtained even though having a large $b$, when $F^{+}_{ack}$ ranges from $10$ms to $20$ms.  The reason why the $x_p$ value first increases and then gradually decreases as $b$ grows is as follows: In our algorithm, when node $p_i$'s link state becomes link up with respect to node $p_j$ by calling closeEnough(), we require that the next hello message from $p_j$ to be received by $p_i$.  So, as the hello period $h$ grows large (=as $b$ grows large) $p_i$ and $p_j$ have to be closer to each other to guarantee link up with each other.  However, as $h$ grows large (=as $b$ grows large), there will be fewer hello message broadcasts interfering with application message broadcasts which means that $p_i$ and $p_j$ can be farther away from each other but still guarantee link up with each other.  The increase and decrease of the $x_p$ value is showing the result of this trade-off.

Figure \ref{fig:nd:fig3} shows the case when nodes move in a maximum speed of $100$km/h (a regular highway considering vehicles as nodes).  In this case, even $F^{+}_{rcv} = F^{+}_{ack}=10$ms is still suitable in obtaining a large value of $x_p$ for large values of $b$.  Considering an even higher maximum speed of $160$km/h (the autobahn considering vehicles as nodes), Figure \ref{fig:nd:fig4} shows that even $F^{+}_{rcv} = F^{+}_{ack}=10$ms is not suitable in obtaining a large value of $x_p$ for large values of $b$.  However, for a small value of $b$ ($\leq 50$), $F^{+}_{rcv} = F^{+}_{ack}=10$ms is still suitable in getting a large value of $x_p$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{comment}

\section{Conclusion}
\label{sec:nd:conclusion}

We have presented a periodic hello-based neighbor detection algorithm using the abstract MAC layer that tolerates bounded clock drift.  Our algorithm has an advantage of not requiring trajectory information.  However, there is a trade-off in which the distance between two nodes must be somewhat closer than their communication radius for them to become link up with each other. For future work, we plan to explore variations of hello message based approaches such as event-based hello (where upper layer messages affect the transmission time of the hello message) and adaptive hello (where hello messages are broadcast depending on the movement speed of a node) \cite{GS05} instead of periodic hello and compare their performance when used with the abstract MAC layer for neighbor detection. 

\end{comment}

\begin{comment}

\appendix
\section{Proofs of Section \ref{sec:nd:proofCorrect}}
\label{sec:nd:appendix}

\begin{proof}[Lemma~\ref{lem:nd:nondecreasing}]
The proof is straightforward from the fact that the only way to update $sendUntil_i[j]$ and/or $recvUntil_i[j]$ is by calling updateDeadlines() and updateDeadline() only allows updates to $sendUntil_i[j]$ and/or $recvUntil_i[j]$ when a greater parameter value is passed to it (lines \ref{line:nd:updateCondSend} and \ref{line:nd:updateCondRecv}).
\qed
\end{proof}

\begin{proof}[Lemma~\ref{lem:nd:sendLessRecv}]
When updateDeadlines($j,s,r$) is called at lines \ref{line:nd:uDL1} or \ref{line:nd:uDL2} at some time $t'$, we have $0<s<r$ since $0<t'+SU_1<t'+RU_1$ and $0<t'+SU_2<t'+RU_2$.  Since the only way to update $sendUntil_i[j]$ and $recvUntil_i[j]$ is by calling updateDeadlines($j,\_,\_$) and since $sendUntil_i[j]$ and $recvUntil_i[j]$ is updated only when their current value is less than $s$ and $r$, respectively, it is straightforward that $sendUntil^t_i[j] < recvUntil^t_i[j]$ for all times $t \geq t_1$.
\qed
\end{proof}

\begin{proof}[Corollary~\ref{cor:sendLessRecv}]
The proof is immediate from Lemma \ref{lem:nd:sendLessRecv} and the fact that for all nodes, the elements of $sendUntil$ and $recvUntil$ are initialized to $0$.
\qed
\end{proof}

\begin{proof}[Lemma~\ref{lem:nd:linkUpIff}]
($\Rightarrow$) Suppose, in contradiction, that $sendUntil^t_i[j] \leq t$.  This implies that there exists a local time $t'(\leq t)$ such that $t'=sendUntil^t_i[j]$.  If $t'=0$, then we have $LS^{t'}_i(j)=LD$ by the initialization code.  If $t' \neq 0$, then we have $LS^{t'}_i(j)=LHU$ at local time $t'$ by line \ref{line:nd:assignLHU}.  Hence, at local time $t'$, we have a link state that is not $LU$.  Now, since $LS^{t}_i(j)=LU$, there exists a local time during $[t',t]$ where line \ref{line:nd:assignLU} is executed.  In order to execute \ref{line:nd:assignLU}, $sendUntil_i[j]$ must have been modified to a greater value than $t'$ during $[t',t]$.  Since $sendUntil_i[j]$ is nondecreasing over time by Lemma \ref{lem:nd:nondecreasing}, it must be that $sendUntil^t_i[j] > t'$, a conradiction.\\
($\Leftarrow$) Suppose, in contradiction, that $LS^t_i(j) \neq LU$. We distinguish two cases:\\
(Case 1. $LS^t_i(j) = LD$): In this case, we have either $sendUntil^t_i[j]=0$ by the initialization code or $recvUntil^t_i[j] \leq t$ by the fact that the only case the link state becomes $LD$ is when LC()$=recvUntil_i[j]$ (line \ref{line:nd:assignLD}).  If $sendUntil^t_i[j]=0$, then we directly get a contradiction since $sendUntil^t_i[j]>t\geq0$.  If $recvUntil^t_i[j] \leq t$, then by Corollary \ref{cor:sendLessRecv}, $sendUntil^t_i[j] \leq recvUntil^t_i[j] \leq t$, a contradiction.\\
(Case 2. $LS^t_i(j) = LHU$): This case implies that there exists a time prior or equal to time $t$ such that the link state became $LHU$.  Let $t'(\leq t)$ be the latest local time that the link state became $LHU$.  By the code, either line \ref{line:nd:assignLHUfromLD} or \ref{line:nd:assignLHU} was executed at time $t'$.  Also, since the link state remains as $LHU$ during $[t',t]$, we have $sendUntil^{t'}_i[j] = sendUntil^t_i[j]$.  If line \ref{line:nd:assignLHU} was executed at time $t'$, then it is straightforward that $t'=sendUntil^{t'}_i[j]$.  Thus, we get $sendUntil^t_i[j] = t' \leq t$, a contradiction.  If line \ref{line:nd:assignLHUfromLD} was executed at time $t'$, then the latest link state prior to time $t'$ must have been $LD$ by line \ref{line:nd:ifLD}.  This implies that there exists a time prior to time $t'$ such that the link state became $LD$.  Let $t''(<t')$ be the latest local time that the link state became $LD$.  We have $recvUntil^{t''}_i[j]=t''$ by line \ref{line:nd:assignLD}.  During $[t'',t')$ updateDeadlines() must not have been called because otherwise the link state must have changed to either $LU$ or $LHU$ by the fact that $sendUntil^{t''}_i[j] \leq recvUntil^{t''}_i[j]=t''$ (Corollary \ref{cor:sendLessRecv}) and the fact that updateDealine() is called with parameters that have a values greater than the current local time value.  Moreover, the if-condition at line \ref{line:nd:updateCondSend} should have been evalutated to false because otherwise the if-condition at line \ref{line:nd:ifLD} would have evaluated to false.  Hence, $sendUntil_i[j]$ was not updated during $[t'',t']$ and we get $sendUntil^{t''}_i[j] = sendUntil^{t'}_i[j] = sendUntil^t_i[j]$.  Therefore, since $sendUntil^{t''}_i[j] \leq recvUntil^{t''}_i[j]=t''$, we finally get $sendUntil^t_i[j] \leq t'' < t$, a contradiction.
\qed
\end{proof}

\begin{proof}[Theorem~\ref{thm:nd:wellformed} (Well-formedness)]
Suppose, for two nodes $p_i$ and $p_j$, that $LS^t_i(j)=LU$ and $LS^{t'}_i(j)=LD$ where $t < t'$ in real time.  Now, suppose, in contradiction, that for all real times $t''\in(t,t')$, $LS^{t''}_i(j) \neq LHU$.  Since $LS^{t'}_i(j)=LD$, we have $recvUntil^{t'}_i[j] \leq t'$ in real time.  Also, since $LS^t_i(j)=LU$, we know that updateDeadlines() is called at least once.  So, by Lemma \ref{lem:nd:sendLessRecv} and Lemma \ref{lem:nd:linkUpIff}, we get $t < sendUntil^{t'}_i[j] < recvUntil^{t'}_i[j] \leq t'$ in real time.  This implies that there exists a real time $t_1\in(t,t')$ such that $sendUntil^{t_1}_i[j] = t_1$ in real time which results in executing line \ref{line:nd:assignLHU}, a contradiction.
\qed
\end{proof}

\begin{proof}[Lemma~\ref{lem:nd:distCond}]
If instantaneous message delivery is assumed, the condition that needs to be satisfied for closeEnough() to return true simply guarantees that $p_i$ and $p_j$ remain in each other's communication radius during $[t,t+T+F^{+}_{rcv}]$ in real time even though $p_i$ and $p_j$ moves in the maximum speed (=$\sigma$) away from each other.  However, in our case, the hello message generated by $p_j$ might have took $F^{+}_{rcv}$ real time to reach $p_i$.  Hence, we can say that $p_i$ and $p_j$ will be in each other's communication radius during $[t,t+T]$ in real time.
\qed
\end{proof}

\begin{proof}[Theorem~\ref{thm:nd:validity} (Validity)]
First, let $T=(h/(1-\rho)+F^{+}_{rcv}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack})\cdot\frac{1+\rho}{1-\rho}+kF^{+}_{ack}$.  Suppose $LS^t_i(j) = LU$ at local time $t$.  By Lemma \ref{lem:nd:linkUpIff}, we know that $LS^t_i(j) = LU$ if and only if $sendUntil^t_i[j] > t$.  We distinguish two cases based on how $sendUntil_i[j]$ was set:\\
(Case 1. By line \ref{line:nd:uDL2} (at local time $t'$)): In this case, the call to closeEnough() returned true.  When closeEnough() returns true, it is guaranteed by Lemma \ref{lem:nd:distCond} that $p_i$ and $p_j$ remain in each other's communication radius for at least $T$ amount of time in real time from time $t'$.  At line \ref{line:nd:uDL2}, we set $sendUntil_i[j]=t'+SU_2$.  Since $0\leq\rho<1$, the amount of local time $SU_2$ in real time is always less than the amount of real time $T$.  Hence, $p_i$ and $p_j$ will remain in each other's communication radius until time $sendUntil_i[j]$ in $p_i$'s local time.\\
(Case 2. By line \ref{line:nd:uDL1}): In this case, $sendUntil_i[j]$ was updated using $hello_j.remaining[i]$.  For two nodes $p_i$ and $p_j$ where $LS^{t_1}_i(j)=LD$ and $LS^{t_1}_j(j)=LD$ for some real time $t_1$, respectively, line \ref{line:nd:uDL2} must be executed first to execute line \ref{line:nd:uDL1} since either $j\in Neighbors_i$ or $i \in Neighbors_j$ must first be satisfied to execute line \ref{line:nd:uDL1}.  Hence, for this case, it suffices to prove that (1) when $sendUntil_i[j]$ is set by executing line \ref{line:nd:uDL2} at $p_i$ at time $t$, $p_i$ and $p_j$ are within each other's communication radius until time $sendUntil^t_i[j]$ and (2) assuming that $hello_j$ was generated by $p_j$ at $p_j$'s local time $t_j$ and it is guaranteed that $p_i$ and $p_j$ remain within each other's communication radius at least until $t_j+hello_j.remaining[i]$ in $p_j$'s local time, if $sendUntil_i[j]$ is set by executing line \ref{line:nd:uDL1} at $p_i$ at time t, then $p_i$ and $p_j$ are within each other's communication radius until time $sendUntil^t_i[j]$.  Part (1) is already proven in (Case 1).  We focus on part (2).  By the code, $sendUntil_i[j]$ is set by the formula $t_i + hello_j.remaining[i]\cdot\frac{1-\rho}{1+\rho} - (1+\rho)F^{+}_{rcv}$ where $t_i$ is $p_i$'s local time when $p_i$ receives $hello_j$.  First note that $hello_j.remaining[i] >0$ because otherwise $sendUntil_i[j]$ will not have been set in the first place.  Since $0\leq\rho<1$, the amount of $p_j$'s local time $hello_j.remaining[i]$ in real time is always greater than or equal to the amount of $p_i$'s local time $hello_j.remaining[i]\cdot\frac{1-\rho}{1+\rho}$ in real time.  In worst case, $hello_j$ might have took $F^{+}_{rcv}$ real time from when $p_j$ generating $hello_j$ to $p_i$ receiving $hello_j$.  Again, since $0\leq\rho<1$, the amount of $p_i$'s local time $(1+\rho)F^{+}_{rcv}$ in real time is always greater than or equal to $F^{+}_{rcv}$ in real time.  Hence, we get that $p_j$'s local time $t_j+hello_j.remaining[i]$ in real time is greater than or equal to $p_i$'s local time $sendUntil^{t_i}_{i}[j]$ in real time.  Therefore, $p_i$ and $p_j$ will remain in each other's communication radius until time $sendUntil^{t_i}_i[j]$ in $p_i$'s local time.
\qed
\end{proof}

\begin{proof}[Lemma~\ref{lem:nd:helloRecv}]
Since the clock drift is bounded by $\rho$ where $0\leq\rho<1$ and each node generates and broadcasts a hello message every $h$ time units with respect to its local clock, each node generates and broadcasts at least one hello message during a time duration of size $h/(1-\rho)$ in real time (the amount of time $h/(1-\rho)$ in real time corresponds to the amount of local time $h$ for the node with the slowest clock rate).  Hence, considering the message delay bound $F^{+}_{rcv}$ in real time, $p_i$ and $p_j$ receive each other's hello message during $[t,t+h/(1-\rho)+F^{+}_{rcv}]$ in real time.
\qed
\end{proof}

\begin{proof}[Theorem~\ref{thm:nd:progress} (Progress)]
Without loss of generality, suppose two nodes $p_i$ and $p_j$ are within distance $x_p$ at real time $t'$.  $dist(p_i,p_j) \leq x_p$ at time $t'$ guarantees that $p_i$ and $p_j$ remain in each other's communication radius for at least the amount of time $h/(1-\rho)+F^{+}_{rcv}$ in real time even though both $p_i$ and $p_j$ moves at a maximum speed ($\sigma$) away from each other.  Applying Lemma \ref{lem:nd:helloRecv}, we get that $p_i$ and $p_j$ receives each other's hello message during $[t',t'+h/(1-\rho)+F^{+}_{rcv}]$ in real time.  Furthermore, $dist(p_i,p_j) \leq x_p$ at time $t'$ also guarantees that by receiving the hello message during $[t',t'+h/(1-\rho)+F^{+}_{rcv}]$ in real time, the call to closeEnough() returns true causing the link state to be $LU$ if the link state was not $LU$ and the link state to remain in $LU$ otherwise.  Now, without loss of generality, suppose that $p_i$ and $p_j$ are within distance $x_p$ for all times during $[t,t+\alpha_p]$ in real time.  By the above argument, it is clear that at real time $t+h/(1-\rho)+F^{+}_{rcv}$($=t+\alpha_p'$) the link state of both $p_i$ and $p_j$ are $LU$. Also, at real time $t+\alpha_p''$, we get that by real time $t+\alpha_p''+\alpha_p'$, closeEnough() will return true at both $p_i$ and $p_j$.  When closeEnough() returns true at time $t''$, $sendUntil_i[j]$ (resp. $sendUntil_j[i]$) is set to at least $SU_2$.  Considering the worst case, the amount of local time $SU_2$ can be at least $SU_2/(1+\rho)=\alpha_p''$ in real time.  Also, considering the worst case, closeEnough() might have returned true at time $t+\alpha_p$.  Hence, until real time $t+\alpha_p+SU_2/(1+\rho)=t+\alpha_p+\alpha_p''$, $LS_i(j)=LU$ and $LS_j(i) = LU$.  Therefore, we have $LS^{t_1}_i(j)=LU$ and $LS^{t_1}_j(i) = LU$ for all $t_1\in[t+\alpha_p',t+\alpha_p+\alpha_p'']$ in real time.   
\qed
\end{proof}

\begin{proof}[Theorem~\ref{thm:nd:onetoone} (Reliable Delivery)]
The AML guarantees the \emph{no duplication} property.  This property says, for a node $p_k$, no two receive events at $p_k$ is caused by the same broadcast event.  Since the ND/P2P layer simply forwards application messages to the AML, we can say that, for a node $p_k$, no two application receive is caused by the same application send.  So, for the reliable delivery property, it only remains to prove that an application message sent from $p_i$ to $p_j$ while $p_i$'s link state is $LU$ with respect to $p_j$ is received by the application layer of $p_j$.

Without loss of generality, suppose node $p_i$ sends an application message at local time $t$ to node $p_j$ while $LS^{t}_i(j)=LU$.  Notice how $sendUntil_i[j]$ and $recvUntil_i[j]$ is set by lines \ref{line:nd:uDL1} and \ref{line:nd:uDL2}.  By the values of $SU_1$,$RU_1$,$SU_2$, and $RU_2$, $sendUntil_i[j]$ and $recvUntil_i[j]$ satisfies $sendUntil^{t'}_i[j] + (1+\rho)(kF^{+}_{ack}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}) \leq recvUntil^{t'}_i[j]$ for all local time $t'$.  If the most recent update to $sendUntil_i[j]$ before local time $t$ was by calling updateDeadlines() at line \ref{line:nd:uDL2}, then Lemma \ref{lem:nd:distCond} implies that, starting from local time $sendUntil^t_i[j]$, during the next $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}+kF^{+}_{ack}$ amount of time in real time, $p_i$ and $p_j$ will be within each other's communication radius.  Even if the the most recent update to $sendUntil_i[j]$ before local time $t$ was by calling updateDeadlines() at line \ref{line:nd:uDL1}, we still have that starting from local time $sendUntil^t_i[j]$, during the next $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}+kF^{+}_{ack}$ amount of time in real time, $p_i$ and $p_j$ will be within each other's communication radius since the formula $SU_1$ guarantees that $sendUntil^t_i[j]$ is set to a local time value such that the real time left for $p_i$ to reach the local time $sendUntil^t_i[j]$ is less than or equal to the real time left for $p_j$ to reach its local time $sendUntil^{t_j}_j[i]$ where $t_j$ is the local time of $p_j$ that is equal to $p_i$'s local time $t$ when both are transformed to real time (see the proof of Theorem \ref{thm:nd:validity} (Case 2)).

Now, recall that $kF^{+}_{ack}$ is the upper bound on the total time (in real time) of emptying the the $k$-bounded buffer if the buffer is full (when there is no control (hello) message interference) and $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}$ is the upper bound on the total time (in real time) of hello message tranmissions interfering with $k$ consecutive application messages in the $k$-bounded send buffer.  So, we can say that a message already in the $k$-bounded send buffer is guaranteed to be sent to the AML within the amount of time $kF^{+}_{ack}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}-F^{+}_{ack}$ in real time.  Hence, from the previous paragraph and by Lemma \ref{lem:nd:linkUpIff}, we have that the ND/P2P layer of $p_j$ receives the application message sent by $p_i$ while $LS^{t}_i(j)=LU$.

%and $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}(1+\rho)$ is the upperbound on the total time (in local time) of hello message tranmissions interfering with $k$ consecutive application messages in the $k$-bounded send buffer.  Since $0\leq\rho<1$, the amount of local time $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}(1+\rho)$ in real time is less than or equal to the amount of real time $2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}$.   So, we can say that a message in the $k$-bounded send buffer is guaranteed to be sent to the AML within the amount of time $kF^{+}_{ack}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}$ in real time.  Hence, from the previous paragraph and by Lemma \ref{lem:nd:linkUpIff}, we have that the ND/P2P layer of $p_j$ receives the application message sent by $p_i$ while $LS^{t}_i(j)=LU$.  

It remains to show that the application layer of $p_j$ receives the message by $p_i$.  Considering $p_i$, if $sendUntil^t_i[j]$ was set by calling updateDeadlines() at line \ref{line:nd:uDL2} at real time $t''$, then by Lemma \ref{lem:nd:distCond} and \ref{lem:nd:helloRecv}, $p_j$ will receive $hello_i$ from $p_i$ until $t''+h/(1-\rho)+F^{+}_{rcv}$ in real time.  Upon $p_j$ receiving $hello_i$ from $p_i$ at $p_j$'s local time $t_j'$, the call to updateDeadline() at line \ref{line:nd:uDL1} and the value of $RU_1$ ensures that $recvUntil^{t_j'}_j[i]$ in real time is greater than or equal to $p_i$'s local time $sendUntil^t_i[j]$ in real time plus $kF^{+}_{ack}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}$ in real time.  Hence, for all $t_1 \in [t_j',recvUntil^{t_j'}_j[i])$ in $p_j$'s local time, $LS^{t_1}_j(i)\neq LD$ since $t_1 < recvUntil^{t_j'}_j[i]$.  Thus, by lines \ref{line:nd:deliverMsg1}, \ref{line:nd:deliverMsg2}, and \ref{line:nd:appRecv}, the application message sent by $p_i$ will be delivered to $p_j$'s application layer.  Now, if $sendUntil^t_i[j]$ was set by calling updateDeadlines() at line \ref{line:nd:uDL1} at real time $t''$, then, by the formula of $SU_1$, $sendUntil^{t}_i[j]$ in real time is less than $sendUntil^{t_j''}_j[i]$ where $t$ and $t_j''$ have the same time value when both are transformed to real time.  Since $sendUntil^{t'}_j[i] + (1+\rho)(kF^{+}_{ack}+2\lceil\frac{kF^{+}_{ack}}{h/(1+\rho)}\rceil F^{+}_{ack}\cdot\frac{1+\rho}{1-\rho}) \leq recvUntil^{t'}_j[i]$ for all local time $t'$ and $LS^{t_2}_j(i)\neq LD$ for all local times $t_2 \in [sendUntil^{t'}_j[i],recvUntil^{t'}_j[i])$, lines \ref{line:nd:deliverMsg1}, \ref{line:nd:deliverMsg2}, and \ref{line:nd:appRecv} guarantee that the application message sent by $p_i$ will be delivered to $p_j$'s application layer.
\qed
\end{proof}

\end{comment}

%Text goes here.

%\section{New Section}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\begin{figure}[H]
%\centering
%\includegraphics[scale=.50]{figures/Penguins.jpg}
%\caption{TAMU figure - This is an example of a long figure title.  Figure titles need to be single-spaced within and double spaced between in the list of figures.}
%\label{fig:nk:landscapepenguins}
%\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{Subsection}
%\begin{table}[H]
%\centering
%\caption{This is a table template - This is an example of a long table title.  Table titles need to be single-spaced within and double spaced between in the list of tables.}
%\begin{tabular}{|l|c|c|c|c|c|}
%\hline
%Product & 1 & 2 & 3 & 4 & 5\\
%\hline
%Price & 124.- & 136.- & 85.- & 156.- & 23.-\\
%Guarantee [years] & 1 & 2 & - & 3 & 1\\
%Rating & 89\% & 84\% & 51\% & & 45\%\\
%\hline
%\hline
%Recommended & yes & yes & no & no & no\\
%\hline
%\end{tabular}
%\label{tab:template1}
%\end{table}


%\subsection{Subsection}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\begin{figure}[H]
%\centering
%\includegraphics[scale=.50]{figures/Sunset.jpg}
%\caption{Sunset figure}
%\label{fig:nk:sunset-fig2}
%\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsubsection{This is a subsubsection}
%\begin{table}[H]
%\centering
%\caption{This is a table template - This is an example of a long table title.  Table titles need to be single-spaced within and double spaced between in the list of tables.}
%\begin{tabular}{|l|c|c|c|c|c|}
%\hline
%Product & 1 & 2 & 3 & 4 & 5\\
%\hline
%Price & 124.- & 136.- & 85.- & 156.- & 23.-\\
%Guarantee [years] & 1 & 2 & - & 3 & 1\\
%Rating & 89\% & 84\% & 51\% & & 45\%\\
%\hline
%\hline
%Recommended & yes & yes & no & no & no\\
%\hline
%\end{tabular}
%\label{tab:template1-2}
%\end{table}
%\section{Another Section}
