%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Submission for ESOP@ETAPS 2016
%% 25 pages max + 2 pages references
%% 
%% Camera-ready:  8 January 2016
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentclass[runningheads,orivec]{llncs}
\usepackage{hyperref}
\usepackage{breakurl}
\usepackage{fancyvrb}
\usepackage{xcolor}
\usepackage{xspace}
\usepackage{url}
\usepackage{aodv}
\usepackage{amsfonts,amsmath,amssymb}
\usepackage{algorithm,algorithmic}
\usepackage{wrapfig}
\usepackage{enumerate}
\usepackage{etex,etoolbox}

%%%% Theorem-like environments
\makeatletter
\spn@wtheorem{observation}{Observation}{\bfseries}{\itshape}
\def\theHALC@line{\thealgorithm-\theALC@line}
\def\theHALC@rem{\thealgorithm-\theALC@rem}
\makeatother

%%%% Proof Environment
\newboolean{qedatend}
\newcommand{\prf}{\setboolean{qedatend}{true}\begin{proof}}
\newcommand{\prfnobox}{\setboolean{qedatend}{false}\begin{proof}}
\newcommand{\eprf}{\ifqedatend\qed\fi\end{proof}}


\floatname{algorithm}{Process}
\renewcommand{\listalgorithmname}{List of Processes}
%%%% Special fonts
\DeclareSymbolFont{frenchscript}{OMS}{ztmcm}{m}{n}
\DeclareMathSymbol{\pow}{\mathord}{frenchscript}{80} % powerset

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%        expanding ARROWS from James; changed by Rob  14-12-10.        %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\makeatletter
\def\comesfrom{\@transition\leftarrowfill}
\def\goesto{\@transition\rightarrowfill}
\def\ngoesto{\@transition\nrightarrowfill}
\def\Goesto{\@transition\Rightarrowfill}
\def\nGoesto{\@transition\nRightarrowfill}
\def\xmapsto{\@transition\mapstofill}
\def\nxmapsto{\@transition\nmapstofill}
\def\@transition#1{\@@transition{#1}}
\newbox\@transbox
\newbox\@arrowbox
\newbox\@downbox
\def\@@transition#1#2%
   {\setbox\@transbox\hbox
      {\vrule height 1.5ex depth .9ex width 0ex\hskip0.25em$\scriptstyle#2$\hskip0.25em}
   \ifdim\wd\@transbox<1.5em
      \setbox\@transbox\hbox to 1.5em{\hfil\box\@transbox\hfil}\fi
   \setbox\@arrowbox\hbox to \wd\@transbox{#1}
   \ht\@arrowbox\z@\dp\@arrowbox\z@
   \setbox\@transbox\hbox{$\mathop{\box\@arrowbox}\limits^{\box\@transbox}$}
   \dp\@transbox\z@\ht\@transbox 10pt
   \mathrel{\box\@transbox}}
\def\nrightarrowfill{$\m@th\mathord-\mkern-6mu%
  \cleaders\hbox{$\mkern-2mu\mathord-\mkern-2mu$}\hfill
  \mkern-6mu\mathord\not\mkern-2mu\mathord\rightarrow$}
\def\Rightarrowfill{$\m@th\mathord=\mkern-6mu%
  \cleaders\hbox{$\mkern-2mu\mathord=\mkern-2mu$}\hfill
  \mkern-6mu\mathord\Rightarrow$}
\def\nRightarrowfill{$\m@th\mathord=\mkern-6mu%
  \cleaders\hbox{$\mkern-2mu\mathord=\mkern-2mu$}\hfill
  \mkern-6mu\mathord\not\mathord\Rightarrow$}
\def\mapstofill{$\m@th\mathord\mapstochar\mathord-\mkern-6mu%
  \cleaders\hbox{$\mkern-2mu\mathord-\mkern-2mu$}\hfill
  \mkern-6mu\mathord\rightarrow$}
\def\nmapstofill{$\m@th\mathord\mapstochar\mathord-\mkern-6mu%
  \cleaders\hbox{$\mkern-2mu\mathord-\mkern-2mu$}\hfill
  \mkern-6mu\mathord\not\mkern-2mu\mathord\rightarrow$}
\makeatother %%%%% end of arrows definition
\newcommand{\ar}[1]{\mathrel{\goesto{#1}}}            % arrow
\newcommand{\nar}[1]{\mathrel{\ngoesto{#1\;}}}        % negated arrow
\newcommand{\dar}[1]{\mathrel{\Goesto{\raisebox{.08em}{\scriptsize$#1$}}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Disjoint union
\makeatletter
\def\moverlay{\mathpalette\mov@rlay}
\def\mov@rlay#1#2{\leavevmode\vtop{%
   \baselineskip\z@skip \lineskiplimit-\maxdimen
   \ialign{\hfil$\m@th#1##$\hfil\cr#2\crcr}}}
\newcommand{\charfusion}[3][\mathord]{
    #1{\ifx#1\mathop\vphantom{#2}\fi
        \mathpalette\mov@rlay{#2\cr#3}
      }
    \ifx#1\mathop\expandafter\displaylimits\fi}
\makeatother
\newcommand{\dcup}{\charfusion[\mathbin]{\cup}{\mbox{\Large$\cdot$}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\comma}{,}
\newcommand{\tawn}{T-AWN\xspace}
\newcommand{\awn}{AWN\xspace}
\newcommand{\otawn}{(T-)AWN\xspace}
\newcommand{\bis}{\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}}
\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
\def\endbox{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
\penalty50\hskip1em\null\nobreak\hfil\squareforqed
\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}

\newcommand{\listingTop}[2][]{%
  \algsetup{linenodelimiter=.,linenosize=\tiny}
  \begin{algorithm}[t]
    {\scriptsize
      \caption{#1}
      \label{pro:#2}
      \begin{algorithmic}[1]\scriptsize
        \input{processes/#2.tex}
	\end{algorithmic}
    }%end scriptsize
  \end{algorithm}%
  	        
}


\newcommand{\highlightspec}[1]{{\color{red}#1}}
\newcommand{\highlightUPD}[1]{\STATE{\textcolor{red}{\ensuremath{\mbox{\bf [\![}#1\mbox{\bf ]\!]}}}}}%
%%%% Spacing commands
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{#1}} % no vertical space
\newcommand{\spaces}[1]{\ #1\ }
\newcommand{\ans}{\spaces{\wedge}}
\newcommand{\ors}{\spaces{\vee}}
\newcommand{\ims}{\spaces{\Rightarrow}}
\newcommand{\iffs}{\spaces{\Leftrightarrow}}

\newcommand{\now}{\keyw{now}\xspace}

\newcommand{\NN}{% natural numbers
    \ensuremath{%
        \mathop{\rm I\mkern-2.5mu N}%
        \nolimits%
    }%
}
\newcommand{\B}{\mathrel{\mathcal{B}}} % a bisimulation
\newcommand{\Sim}{\mathrel{\mathcal{S}}} % a bisimulation
\newcommand{\U}{\mathrel{\mathcal{U}}} % similarity of actions

\newcommand{\hopsc}{\dval{hops}_c}
\newcommand{\dipc}{\dval{dip}_{\hspace{-1pt}c}}
\newcommand{\ripc}{\dval{rip}_{\hspace{-1pt}c}}
\newcommand{\oipc}{\dval{oip}_{\hspace{-1pt}c}}
\newcommand{\rreqidc}{\dval{rreqid}_{c}}
\newcommand{\dsnc}{\dval{dsn}_c}
\newcommand{\rsnc}{\dval{rsn}_c}
\newcommand{\destsc}{\dval{dests}_c}
\newcommand{\osnc}{\dval{osn}_c}
\newcommand{\ipc}{\dval{ip}_{\hspace{-1pt}c}}
\newcommand{\xiN}[2][N]{\xi_{#1}^{#2}}
\newcommand{\zetaN}[2][N]{\zeta_{#1}^{#2}}
\newcommand{\RN}[2][N]{R_{#1}^{#2}}
\newcommand{\PN}[2][N]{P_{#1}^{#2}}

\newcommand{\rtord}[1][\dval{dip}]{\ensuremath{\sqsubseteq_{#1}}}
\newcommand{\rtequiv}[1][\dval{dip}]{\ensuremath{\approx_{#1}}}
\newcommand{\rtsord}[1][\dval{dip}]{\ensuremath{\sqsubset_{#1}}}
\newcommand{\decremented}{\mathbin{\stackrel{\bullet}{\raisebox{0pt}[2pt]{$-$}}}1}
\newcommand{\rte}{routing table entry\xspace}
\newcommand{\rtes}{routing table entries\xspace}

\newcommand{\W}{\mathcal{W}}
\newcommand{\R}{\mathcal{R}}
\newcommand{\I}{\mathcal{I}}
\newcommand{\M}{\mathcal{M}}
\newcommand{\D}{\mathcal{D}}

\newcommand{\nil}{\mathbf{0}}
\newcommand{\RW}{\R\mathop{:}\W}
\newcommand{\Rw}[2][\mathop]{R#1{:}#2}

\newcommand{\exclnow}[1][\xi]{#1_{\backslash\now}}

%%Proof Sketch
\spnewtheorem*{proofsketch}{Proof Sketch}{\itshape}{\rm}

%%%%%%%%%%%%%%%%%
%%new stuff for T-AODV
%%constants
\newcommand{\highlight}[2][red]{\textcolor{#1}{#2}}
\newcommand{\deltime}{\keyw{DELETE\_PERIOD}}
\newcommand{\valtime}{\keyw{ACTIVE\_ROUTE\_TIMEOUT}}
\newcommand{\traversal}{\keyw{NET\_TRAVERSAL\_TIME}}
\newcommand{\nodetraversal}{\keyw{NODE\_TRAVERSAL\_TIME}}
\newcommand{\retries}{\keyw{RREQ\_RETRIES}}
\newcommand{\pathdiscoverytime}{\keyw{PATH\_DISCOVERY\_TIME}}
\newcommand{\myroute}{\keyw{MY\_ROUTE\_TIMEOUT}}
\newcommand{\fnexprt}{\keyw{exp\_rt}}
\newcommand{\fnexpq}{\keyw{exp\_store}}
\newcommand{\exprt}[3]{\fnexprt(#1\comma #2\comma #3)}
\newcommand{\expq}[3]{\fnexpq(#1\comma #2)}
\newcommand{\fnsettimert}{\keyw{setTime\_rt}}
\newcommand{\settimert}[3]{\fnsettimert(#1\comma #2\comma #3)}
\newcommand{\fnsettimequeues}{\keyw{setTime\_store}}
\newcommand{\settimequeues}[3]{\fnsettimequeues(#1\comma #2\comma #3)}
\newcommand{\fnsetretries}{\keyw{resetRetries}}
\newcommand{\setretries}[2]{\fnsetretries(#1\comma #2)}
\newcommand{\fnincretries}{\keyw{incRetries}}
\newcommand{\incretries}[2]{\fnincretries(#1\comma #2)}
\newcommand{\fnexprreqs}{\keyw{exp\_rreqs}}
\newcommand{\exprreqs}[2]{\fnexprreqs(#1\comma #2)}
\newcommand{\lifetime}{\keyw{ltime}}
\newcommand{\tTIME}{\keyw{TIME}}

%%%%%%%%%%%%%%%%%%%%%%%%%
%%labels for sos-tables
\newcommand\tablelabel[2][]{%
  \ifstrempty{#1}{%
    \hypertarget{#2}{\mbox{\color{gray}\scriptsize({\sf #2})}}%
  }{%
    \hypertarget{#1}{\mbox{\color{gray}\scriptsize({\sf #2})}}%
  }%
}
\newcommand\tableref[2][]{%
  \ifstrempty{#1}{%
    \hyperlink{#2}{\mbox{({\sf #2})}}\xspace%
  }{%
    \hyperlink{#1}{\mbox{({\sf #2})}}\xspace%
  }%
}

\hfuzz2pt % Don't report over-full h-boxes if over-edge is small
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{document}%
\titlerunning{A Timed Process Algebra for Wireless Networks}
\title{A Timed Process Algebra for Wireless Networks with an Application in Routing \texorpdfstring{{\\[-4pt]\normalsize (extended abstract)}}{}}
\authorrunning{E.\ Bres, R.J.\ van Glabbeek and P.\ H\"ofner}
  \author{
  Emile Bres\inst{1,3}\and
  Rob van Glabbeek\inst{1,2}\and
  Peter H\"ofner\inst{1,2} 
  }
\institute{
  NICTA, Australia\and
  Computer Science and Engineering, University of New South Wales, Australia\and
  \'Ecole Polytechnique, Paris, France
}

\maketitle 
\setcounter{footnote}{0}
\begin{abstract}
This paper proposes a timed process algebra for wireless networks,
an extension of the Algebra for Wireless Networks. It combines
treatments of local broadcast, conditional unicast and data structures,
which are essential features for the modelling of network protocols.
In this framework we model and analyse the Ad hoc On-Demand Distance
Vector routing protocol, and show that, contrary to claims in the
literature, it fails to be loop free. We also present boundary
conditions for a fix ensuring
that the resulting protocol is indeed loop free.
\end{abstract}

%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}\label{sec:intro} 
%%%%%%%%%%%%%%%%%%%%%
In 2011 we developed the \emph{Algebra for Wireless Networks} (\awn)~\cite{ESOP12},
a process algebra particularly tailored for Wireless Mesh Networks (WMNs) and Mobile Ad Hoc Networks (MANETs).
Such networks are currently being used in a wide range of application areas, such as public safety and mining. 
They are self-organising wireless multi-hop networks that provide network communication without relying on a wired backhaul infrastructure.
A significant characteristic of such networks is that they allow highly dynamic network topologies, meaning that network nodes can 
join, leave, or move within the network at any moment. 
As a consequence routing protocols have constantly to check for broken links, and to replace invalid routes by better ones. 

To capture the typical characteristics of WMNs and MANETs, \awn offers
a unique set of features: 
\emph{conditional unicast} (a message transmission attempt with different follow-up behaviour depending on its success), 
\emph{groupcast} (communication to a specific set of nodes),
\emph{local broadcast} (messages are received only by nodes within transmission range of the sender), 
and \emph{data structure}. 
We are not aware of any other process algebra that provides all these features, and hence
could not use any other algebra to model certain protocols for WMNs or MANETs in a straightforward fashion.%
\footnote{A comparison between \awn and other process algebras can be found in \cite[Sect.~11]{TR13}.}
Case studies~\cite{ESOP12,TR13,GHPT16,EHWripe12} have shown that \awn provides the right level of abstraction to model 
full IETF protocols, such as the Ad hoc On-Demand Distance Vector {(AODV)} routing protocol~\cite{rfc3561}.
\awn has been employed to formally model this
  protocol---thereby eliminating ambiguities\pagebreak[3] and contradictions from the official specification, written in English Prose---and
 to reason about protocol behaviour and provide rigorous proofs of key protocol
properties such as loop freedom and route correctness.

However, \awn\ abstracts from time. 
Analysing routing protocols without considering timing issues is useful in its own right; for AODV it has revealed many shortcomings in drafts as well as in the standard  (e.g.,~\cite{BOG02,MSWIM12,AODVloop}).
Including time in a formal analysis, however, will pave the way to analyse protocols that repeat some procedures every couple of time units; 
examples are OLSR~\cite{rfc3626} and B.A.T.M.A.N.~\cite{batman}.
Even for a reactive protocol such as AODV, which does not schedule tasks regularly, 
it has been shown that timing aspects are important: 
if timing parameters are chosen poorly, 
some routes are not established since data that is stored locally at network nodes 
expires too soon and is erased~\cite{CK05}.
Besides such shortcomings in ``performance'', also fundamental
  correctness properties like loop freedom can be affected by the treatment of time---as we will
  illustrate.

To enable time analyses of WMNs and MANETs, 
this paper proposes a \emph{Timed (process) Algebra for Wireless Networks} (\tawn),
an extension of \awn. It combines \awn's unique set of 
features, such as local broadcast, with~time. 

In this framework we model and analyse the AODV routing protocol, and show that, contrary to claims in the
literature, e.g., \cite{AODV99}, it fails to be loop free, as data required for routing can expire. 
We also present boundary conditions for a fix ensuring
that the resulting protocol is loop free.

\subsection*{Design Decisions}
Prior to the development of \tawn\ we had to make a couple of decisions.

\paragraph{Intranode computations.}
In wireless networks sending a packet from one node to another takes multiple microseconds.
Compared to these ``slow'' actions, time spent for internal (intranode) computations, such as variable assignments or evaluations of expressions,
is negligible. We therefore postulate that only transmissions from one node to another take time.

This decision is debatable for processes that can perform infinite
sequences of intranode computations without ever performing a
durational action.  In this paper (and in all applications), we
restrict ourselves to \emph{well-timed} processes in the spirit of
\cite{NS94}, i.e., to processes where any infinite sequence of actions
contains infinitely many time steps or infinitely many input actions,
such as receiving an incoming packet.

But, in the same spirit as \tawn assigns time to internode communications, 
it is more or less straightforward to assign times to other operations as well.

\paragraph{Guaranteed Message Receipt and Input Enabledness.}
A fundamental assumption underlying the semantics of \otawn is that any broadcast message \emph{is}
received by all nodes within transmission range \cite[\textsection1]{TR13}.%
\footnote{\label{guaranteed receipt}In reality, communication is only
half-duplex: a single-interface network node cannot receive messages while sending and hence
messages can be lost.
However, the CSMA protocol used at the link layer---not 
modelled by {\otawn}---keeps the probability of packet loss due to two nodes (within
range) sending at the same time rather low.
}
This abstraction enables us to interpret a failure of route discovery (as documented for AODV in
\cite[\textsection9]{TR13}) as an imperfection in the protocol, rather than as a result of a chosen formalism not
ensuring guaranteed receipt. 

A consequence of this design decision is that in the operational semantics of \otawn a broadcast of
one node in a network needs to synchronise with some (in)activity of all other nodes in the network~\cite[\textsection11]{TR13}.
If another node is within transmission range of the broadcast, the broadcast synchronises with a
receive action of that node, and otherwise with a non-arrive transition, which signals that the node
is out of range for this broadcast~\cite[\textsection4.3]{TR13}.

A further consequence is that we need to specify our nodes in such a way that they are
\emph{input-enabled}, meaning that in any state they are able to receive messages from any other node
within transmission range.

Since a transmission (broadcast, groupcast, or unicast) takes 
multiple units of time, we postulate 
that another node can only receive a message if it remains
within transmission range during the whole period of sending.%
\footnote{To be precise, we forgive very short
  interruptions in the connection between two nodes---those that begin
  and end within the same unit of time.} 
A possible way to model the receive action that synchronises with a
transmission such as a broadcast is to let it take
the same amount of time as the broadcast action. However, a process that is busy
executing a durational receive action would fail to be input-enabled, for it would not be able to start
receiving another message before the ongoing message receipt is finished.
For this reason, we
model the receipt of a message as an instantaneous action that synchronises with the very end of a broadcast action.%
\footnote{Another solution would be to assume that a broadcast-receiving process can receive multiple messages in parallel.
In case the process is meant to add incoming messages to a message queue (as happens in our application
to AODV), one can assume that a message that is being received in parallel is added to that queue as
soon as its receipt is complete. However, such a model is equivalent to one in which only the very
last stage of the receipt action is modelled.}

\paragraph{\tawn Syntax.} 
When designing or formalising a protocol in \tawn, an engineer should
not be bothered with timing aspects; except for functions and procedures that schedule tasks depending on the current time. 
Because of this, we use the syntax of \awn also for \tawn;
``extended'' by a local timer \now.
Hence we can perform a 
timed analysis of any specification written in \awn, since they are
also \tawn specifications.

%%%%%%%%%%%%%%%%%%%%%
\section{A Timed Process Algebra for Wireless Networks}\label{sec:process_algebra}
%%%%%%%%%%%%%%%%%%%%%
In this section we propose \tawn (Timed Algebra for Wireless Networks), 
an extension of the process algebra AWN \cite{ESOP12,TR13} with time.
AWN itself is a variant of standard process algebras \cite{Mi89,Ho85,BK86,BB87}, 
tailored to protocols in wireless mesh networks, such as the 
Ad-hoc on Demand Distance Vector (AODV) routing protocol.
In \otawn, a WMN is modelled as an encapsulated
parallel composition of network nodes.  On each node several
sequential processes may be running in parallel.  Network nodes
communicate with their direct neighbours---those nodes that are in
transmission range---using either broadcast, groupcast or unicast.  Our
formalism maintains for each node the set of nodes that are currently
in transmission range.  Due to mobility of nodes and variability of
wireless links, nodes can move in or out of transmission range.  The
encapsulation of the entire network inhibits communications between
network nodes and the outside world, with the exception of the receipt
and delivery of data packets from or to clients\footnote{The
application layer that initiates packet sending and/or awaits receipt of
a packet.}  of the modelled protocol that may be hooked up to various
nodes.

In \tawn we apply a discrete model of time, where each sequential process maintains a local variable
\now holding its local clock value---an integer. We employ only one clock for each sequential
process. All sequential processes in a network synchronise in taking time steps, and at each time
step all local clocks advance by one unit.  For the rest, the variable \now behaves as
any other variable maintained by a process: its value can be read when evaluating guards, thereby
making progress time-dependant, and any value can be assigned to it, thereby resetting the local
clock.

In our model of a sequential process $p$ running on a node, time can elapse only when $p$ is
transmitting a message to another node, or when $p$ currently has no way to proceed---for instance,
when waiting on input, or for its local clock to reach a specified value. All other actions of $p$, such as assigning values to variables,
evaluating guards, communicating with other processes running on the same node, or communicating
with clients of the modelled protocol hooked up at that node, are assumed to be an
order of magnitude faster, and in our model take no time at all. Thus they are executed in preference to time steps.

\subsection{The Syntax of \tawn}\label{ssec:syntax}

The syntax of \tawn is the same as the syntax of AWN \cite{ESOP12,TR13}, except for the presence of
the variable \now of the new type \keyw{TIME}.
This brings the advantage that any specification written in AWN can be interpreted and 
analysed in a timed setting. The rest of this Section
\ref{ssec:syntax} is almost copied verbatim from the original articles about AWN \cite{ESOP12,TR13}.

\subsubsection{A Language for Sequential Processes.}

The internal state of a process is determined, in part, by the values
of certain data variables that are maintained by that process.  To
this end, we assume a data structure with several types, variables
ranging over these types, operators and predicates. First order
predicate logic yields terms (or \emph{data expressions}) and formulas
to denote data values and statements about them.\label{pg:undefvalues}\footnote{As
    \label{fn:undefvalues}%
    operators we also allow \emph{partial} functions with the
    convention that any atomic formula containing an undefined subterm
    evaluates to {\tt false}.} Our data structure
always contains the types \keyw{TIME}, \tDATA, \tMSG, {\tIP} and $\pow(\tIP)$ of \emph{time values}, which
we take to be integers (together with the special value $\infty$),
\emph{application layer data}, \emph{messages}, \emph{IP addresses}---or any
other node identifiers---and \emph{sets of IP addresses}. We further assume that 
there is a variable \now of type \keyw{TIME} and a function $\newpktID:\tDATA \times \tIP \rightarrow \tMSG$
that generates a message with new application layer data for a particular destination. 
The purpose of this function is to inject data to the protocol; details will be given later.

In addition, we assume a type \keyw{SPROC} of \emph{sequential processes},
and a collection of \emph{process names}, each being an operator of type
$\keyw{TYPE}_1 \times \cdots \times \keyw{TYPE}_n \rightarrow \keyw{SPROC}$
for certain data types $\keyw{TYPE}_i$.
Each process name $X$ comes with a \emph{defining equation}\vspace{-1pt}
\[X(\keyw{var}_1\comma\ldots\comma\keyw{var}_n) \stackrel{{\it def}}{=} p\ ,\]
\vspace{-1pt}in which, for each $i=1,\ldots,n$, $\keyw{var}_i$ is a variable of type
$\keyw{TYPE}_i$ and $p$ a \emph{guarded}\footnote{\label{guarded}%
An expression $p$ is \emph{guarded} if each call of a process
name $X(\dexp{exp}_1,\ldots,\dexp{exp}_n)$  occurs with a subexpression
$\cond{\varphi}q$, $\assignment{\keyw{var}:=\dexp{exp}}q$,
$\alpha.q$ or $\unicast{\dexp{dest}}{\dexp{ms}}.q \prio r$ of $p$.}
\emph{sequential process expression}
defined by the grammar below. The expression $p$ may contain the variables
$\keyw{var}_i$ as well as $X$; however, all occurrences of data
variables in $\p$ have to be \emph{bound}.
The choice of the underlying data structure and the process names with
their defining equations can be tailored to any particular application
of our language; our decisions made for modelling AODV are presented
in Section~\ref{sec:aodv}.  The process
names are used to denote the processes that feature in this
application, with their arguments $\keyw{var}_i$ binding the current
values of the data variables maintained by these processes.

The \emph{sequential process expressions} are given by the following grammar:
\begin{eqnarray*}
\SP &::=& X(\dexp{exp}_1,\ldots,\dexp{exp}_n) ~\mid~ \cond{\varphi}\SP ~\mid~ \assignment{\keyw{var}:=\dexp{exp}} \SP~\mid~ \SP+\SP ~\mid\\
     &&\alpha.\SP ~\mid~ \unicast{\dexp{dest}}{\dexp{ms}}.\SP \prio \SP \\
\alpha &::=&
  \broadcastP{\dexp{ms}} ~\mid~ \groupcastP{\dexp{dests}}{\dexp{ms}}
  ~\mid~ \send{\dexp{ms}} ~\mid\\
  &&\deliver{\dexp{data}} ~\mid~\receive{\msg}
\end{eqnarray*}
Here $X$ is a process name, $\dexp{exp}_i$ a data expression of the
same type as $\keyw{var}_i$, $\varphi$ a data formula,
$\keyw{var}\mathop{:=}\dexp{exp}$ an assignment of a data expression
\dexp{exp} to a variable \keyw{var} of the same type, \dexp{dest},
\dexp{dests}, \dexp{data} and \dexp{ms} data expressions of types
{\tIP}, $\pow(\tIP)$, {\tDATA} and {\tMSG}, respectively, and $\msg$ a
data variable of type \tMSG.

The internal state of a sequential process described by an expression
$\p$ in this language is determined by $\p$, together with a
\emph{valuation} $\xi$ associating data values $\xi(\keyw{var})$ to
the data variables \keyw{var} maintained by this process.
Valuations naturally extend to \emph{$\xi$-closed} data
expressions---those in which all variables are either bound or in the
domain of $\xi$.

Given a valuation of the data variables by concrete data values, the
sequential process $\cond{\varphi}\p$ acts as $\p$ if $\varphi$
evaluates to {\tt true}, and deadlocks if $\varphi$ evaluates to
{\tt false}. In case $\varphi$ contains free variables that are not
yet interpreted as data values, values are assigned to these variables
in any way that satisfies $\varphi$, if possible.
The sequential process $\assignment{\keyw{var}:=\dexp{exp}}\p$
acts as $\p$, but under an updated valuation of the data variable \keyw{var}.
The sequential process $\p+\q$ may act either as $\p$ or as
$\q$, depending on which of the two processes is able to act at all.  In a
context where both are able to act, it is not specified how the choice 
is made. \pagebreak The sequential process $\alpha.\p$ first performs the action
$\alpha$ and subsequently acts as $\p$.  The action
$\broadcastP{\dexp{ms}}$ broadcasts (the data value bound to the
expression) $\dexp{ms}$ to the other network nodes within transmission range,
whereas $\unicast{\dexp{dest}}{\dexp{ms}}.\p \prio \q$ is a sequential process
that tries to unicast the message $\dexp{ms}$ to the destination
\dexp{dest}; if successful it continues to act as $\p$ and otherwise
as $\q$. In other words, $\unicast{\dexp{dest}}{\dexp{ms}}.\p$ is
prioritised over $\q$; only if the action $\unicast{\dexp{dest}}{\dexp{ms}}$
is not possible, the alternative $q$ will happen. It models an abstraction
of an acknowledgment-of-receipt mechanism that is typical for unicast
communication but absent in broadcast communication, as implemented by
the link layer of relevant wireless standards such as IEEE 802.11~\cite{IEEE80211s}.
The process $\groupcastP{\dexp{dests}}{\dexp{ms}}.\p$ tries
to transmit \dexp{ms} to all destinations $\dexp{dests}$, and proceeds
as $\p$ regardless of whether any of the transmissions is successful.
Unlike {\bf unicast} and  {\bf broadcast}, the expression {\bf groupcast} 
does not have a unique counterpart in networking.
Depending on the protocol and the implementation it can 
be an iterative unicast, a broadcast, or a multicast;
thus  {\bf groupcast} abstracts from implementation details. The
action $\send{\dexp{ms}}$ synchronously transmits a message to another
process running on the same network node; this action can occur only
when this other sequential process is able to receive the message.
The sequential process $\receive{\msg}.\p$ receives any message $m$
(a data value of type \tMSG) either from another node, from another
sequential process running on the same node or from the client hooked
up to the local node.  It then proceeds as $\p$, but with the data
variable $\msg$ bound to the value $m$. 
The submission of data from a client
is modelled by the receipt of a message $\newpkt{\dval{d}}{\dval{dip}}$,
where the function $\newpktID$ generates a message containing the
data $\dval{d}$ and the intended destination $\dval{dip}$. 
Data is delivered to the client by \deliver{\dexp{data}}.%

\subsubsection{A Language for Parallel Processes.}

\emph{Parallel process expressions} are given by the grammar\vspace{-6pt}
$$\PP ~::=~ \xi,\SP ~\mid~ \PP \parl \PP\ ,$$
where $\SP$ is a sequential process expression and $\xi$ a valuation.
An expression $\xi,\p$ denotes a sequential process expression
equipped with a valuation of the variables it maintains.
The process $P\parl Q$ is a parallel composition of $P$ and $Q$,
running on the same network node. An action $\receive{\dval{m}}$ of~$P$
synchronises with an action $\send{\dval{m}}$ of $Q$ into an internal
action $\tau$, as formalised in Table~\ref{tab:sos parallel}. 
These receive actions of $P$ and send actions of $Q$
cannot happen separately. All other actions of $P$ and $Q$, except time steps, including
receive actions of $Q$ and send actions of $P$, occur interleaved in $P\parl Q$.
Therefore, a parallel process expression denotes a parallel composition
of sequential processes $\xi,P$ with information flowing from right to
left. The variables of different sequential processes running on the
same node are maintained separately, and thus cannot be shared.

Though $\parl$ only allows information flow in one direction, it reflects reality of 
WMNs. Usually two sequential processes run on the same node:
$
P \parl Q
$.
The main process $P$ deals with all protocol details  of the node, e.g., message handling 
and maintaining the data such as routing tables.
The process $Q$ manages the queueing of messages as they arrive; it is always able to
receive a message even if $P$ is busy. 
The use of message queueing in combination with $\parl$ is crucial in order to create input-enabled
nodes (cf.~\Sect{intro}).\pagebreak

\subsubsection{A Language for Networks.}\label{ssec:networks}

We model network nodes in the context of a wireless mesh network by
\emph{node expressions} of the form $\dval{ip}:\PP:R$. Here $\dval{ip}
\in \tIP$ is the \emph{address} of the node, $\PP$ is a parallel process
expression, and $R\subseteq \tIP$ is the \emph{range} of the node---the
set of nodes that are currently within transmission range of $\dval{ip}$.

A \emph{partial network} is then modelled by a \emph{parallel
  composition} $\|$ of node expressions, one for every node in the
network, and a \emph{complete network} is a partial network within an
\emph{encapsulation operator} $[\_]$ that limits the communication of
network nodes and the outside world to the receipt and the delivery
of data packets to and from the application layer attached to the
modelled protocol in the network nodes.
This yields the following grammar for network expressions:
\[N ::= [M] \qquad\qquad M::= ~~ \dval{ip}:\PP:R ~~\mid~~ M \| M\ .\vspace{-3pt}\]

\subsection{The Semantics of \tawn}\label{sec:tawnsos}

\newcommand{\tick}{{\rm tick}}
\newcommand{\timestep}{{\rm ts}}
\newcommand{\tr}{{\rm t}}
\newcommand{\w}{{\rm w}}
\newcommand{\wtr}{{\rm wr}}
\newcommand{\ws}{{\rm ws}}
\newcommand{\wrs}{{\rm wrs}}
\newcommand{\timeinc}{[\now\mathord+\mathord{\mkern-1mu}\mathord+]}
\newcommand{\defined}{\mathord\downarrow}
\newcommand{\range}{\dval{dsts}\xspace}

\newcommand{\LB}{\keyw{LB}\xspace}
\newcommand{\LG}{\keyw{LG}\xspace}
\newcommand{\LU}{\keyw{LU}\xspace}
\newcommand{\DB}{\keyw{\Delta B}\xspace}
\newcommand{\DG}{\keyw{\Delta G}\xspace}
\newcommand{\DU}{\keyw{\Delta U}\xspace}

As mentioned in the introduction, the transmission of a message 
takes time.  Since our main application assumes a wireless link and node mobility, 
the packet delivery time varies. Hence we assume a minimum time that is required 
to send a message, as well as an optional extra transmission time. 
In \tawn the values of these parameters are given for each type of sending separately: 
\LB, \LG, and \LU, satisfying $\LB,\LG,\LU > 0$,
specify the minimum bound, in units of time, on the duration of a broadcast, groupcast
and unicast transmission; the optional additional transmission times are denoted by 
$\DB$, $\DG$ and $\DU$, satisfying $\DB,\DG,\DU \geq 0$.
Adding up these parameters (e.g.\ $\LB$ and $\DB$) yields maximum
transmission times. 
We allow any execution consistent with these parameters.
For all other actions our processes can take we postulate execution times of 0.

\begin{table}[tp]
\caption{Structural operational semantics for sequential process expressions
\label{tab:sos sequential}}

\vspace{-5ex}
$$\begin{array}{@{}l@{\ }r@{~}l@{\hspace{-3em}}r@{}}
\tablelabel{bc} &
\xi,\broadcastP{\dexp{ms}}.\p &\ar{\tau} \xi,\stargcast{\tIP}{\xi(\dexp{ms})}[\LB,\DB].\p \prio \p
  \hspace{-7em}
& \mbox{\small(if $\xi(\dexp{ms})\defined$)}
\\[3pt]
\tablelabel{gc} &
\xi,\groupcastP{\dexp{dests}}{\dexp{ms}}.\p &\ar{\tau} \xi,\stargcast{\xi(\dexp{dests})}{\xi(\dexp{ms})}[\LG,\DG].\p \prio \p
\hspace{-10em}
 \\&&& \hspace{-10em}\mbox{\small(if $\xi(\dexp{dests})\defined$ and $\xi(\dexp{ms})\defined$)}
\\[3pt]
\tablelabel{uc} &
  \xi,\unicast{\dexp{dest}}{\dexp{ms}}.\p \prio \q &\ar{\tau} \xi,\stargcast{\{\xi(\dexp{dest})\}}{\xi(\dexp{ms})}[\LU,\DU].\p \prio \q
\hspace{-10em}
\\
&
&& \mbox{\small(if $\xi(\dexp{dest})\defined$ and $\xi(\dexp{ms})\defined$)}
\\[3pt]
\multicolumn{2}{l}{\tablelabel{tr}\,
  \xi,\hspace{-.5pt}\stargcast{\range}{m}[n\mathord+1,o].\p \prio \q}
  &\ar{\Rw[\mathbin]{\w}}
  \xi\timeinc,\stargcast{(\range\mathop\cap R)}{m}[n,o].\p \prio \q
\hspace{-10em}
\\
&
&& \hspace{-20em}\mbox{\small($\forall R\subseteq \tIP$)}
\\[3pt]
\tablelabel{tr-o}&\\
\multicolumn{2}{@{}r@{\ }}{
  \xi,\stargcast{\range}{m}[n\mathord+1,o\mathord+1].\p \prio \q}
  &
  \ar{\Rw[\mathbin]{\w}}
  \xi\timeinc,\stargcast{(\range\mathop\cap R)}{m}[n\mathord+1,o].\p \prio \q 
\hspace{-7em}
\\
&
&& \hspace{-20em}\mbox{\small($\forall R\subseteq \tIP$)}
\\[3pt]
\tablelabel{sc} &
  \xi,\stargcast{\range}{m}[0,o].\p \prio \q & \ar{\colonact{\range}{\starcastP{m}}} \xi,\p
& \hspace{-3pt}\mbox{\small(if $\range\neq \emptyset$)}
\\[3pt]
\tablelabel[nsc]{$\neg$sc} &
    \xi,\stargcast{\range}{m}[0,o].\p \prio \q & \ar{\colonact{\range}{\starcastP{m}}} \xi,\q
  & \hspace{-3pt}\mbox{\small(if $\range=\emptyset$)}
\\[3pt]
\tablelabel{snd} &
  \xi,\send{\dexp{ms}}.\p &\ar{\send{\xi(\dexp{ms})}} \xi,\p
& \mbox{\small(if $\xi(\dexp{ms})\defined$)}
\\[3pt]
\tablelabel{ws}&
  \xi,\send{\dexp{ms}}.\p &\ar{\ws~} \xi\timeinc,\send{\dexp{ms}}.\p
& \mbox{\small(if $\xi(\dexp{ms})\defined$)}
\\[3pt]
\tablelabel{del}&
  \xi,\deliver{\dexp{data}}.\p &\ar{\deliver{\xi(\dexp{data})}} \xi,\p
& \mbox{\small(if $\xi(\dexp{data})\defined$)}
\\[3pt]
\tablelabel{rcv}&
  \xi,\receive{\keyw{msg}}.\p &\ar{\receive{m}} \xi[\keyw{msg}:=m],\p
  & \mbox{\small($\forall m\in \tMSG$)}
\\[3pt]
\tablelabel{wr}&
  \xi,\receive{\keyw{msg}}.\p &\ar{\wtr~} \xi\timeinc,\receive{\keyw{msg}}.\p
\\[3pt]
\tablelabel{ass}&
  \xi,\assignment{\keyw{var}:=\dexp{exp}}\p &\ar{\tau} \xi[\keyw{var}:=\xi(\dexp{exp})],\p
& \mbox{\small(if $\xi(\dexp{exp})\defined$)}
\\[3pt]
\tablelabel{w}&
  \xi,\p & \ar{\w}  \xi\timeinc,p  & \mbox{\small(if $\xi(p)\mathord\uparrow$)}
\\[6pt]
\tablelabel{rec}&
\multicolumn{2}{c}{\displaystyle
  \frac{\emptyset[\keyw{var}_i:=\xi(\dexp{exp}_i)]_{i=1}^n,\p \ar{a} \xii,\p'}
  {\xi,X(\dexp{exp}_1,\ldots,\dexp{exp}_n) \ar{a} \xii,\p'}
  ~\mbox{(\small$X(\keyw{var}_1,\ldots,\keyw{var}_n) \stackrel{{\it def}}{=} \p$)}}
   \hspace{-10em}
\\[-8pt]
&
  && \hspace{-10em}
  \mbox{\small($\forall a\mathbin\in \act-\W$, if $\xi(\dexp{exp}_i)\defined$)}
\\[6pt]
\tablelabel{rec-w}\hspace{-2.5pt}&
\multicolumn{2}{c}{\displaystyle
  \frac{\emptyset[\keyw{var}_i:=\xi(\dexp{exp}_i)]_{i=1}^n,\p \ar{w_1} \xii,\p'}
  {\xi,X(\dexp{exp}_1,...,\dexp{exp}_n) \ar{w_1} \xi\timeinc,X(\dexp{exp}_1,...,\dexp{exp}_n)}
  ~\mbox{(\small$X(\keyw{var}_1,...,\keyw{var}_n) \mathop{\stackrel{{\it def}}{=}} \p$)}\hspace{-10em}}
\\[-8pt]
&
  && \hspace{-8em}\mbox{$(\forall w_1\mathord\in \W\mbox{, if~}\xi(\dexp{exp}_i)\defined)$}
\\[6pt]
\multicolumn{3}{@{}l@{}}{
\tablelabel{grd}\hspace{3mm} 
{\displaystyle\
  \frac{ \xi \stackrel{\varphi}{\rightarrow}\xii}
       {\xi,\cond{\varphi}\p \ar{\tau} \xii,\p} \qquad\qquad
\tablelabel[ngrd]{$\neg$grd}\hspace{3mm} 
  \frac{ \xi \nar{\varphi}}
       {\xi,\cond{\varphi}\p \ar{\w} \xi\timeinc,\cond{\varphi}\p}
       \hspace{-20em}
  }}
\\[14pt]
\multicolumn{3}{@{}l@{}}{
\tablelabel{alt-l}\hspace{3mm} 
{\displaystyle
  \frac{\xi,\p \ar{a} \xii,\p'}{\xi,\p+\q \ar{a} \xii,\p'} \qquad\qquad
\tablelabel{alt-r}\hspace{3mm}  
  \frac{\xi,\q \ar{a} \xii,\q'}{\xi,\p+\q \ar{a} \xii,\q'}
         
  }}\hspace{-15em}
  & \mbox{\small($\forall a\in \act-\W$)}
\\[14pt]
\tablelabel{alt-w}\hspace{-2.5mm}&
\multicolumn{2}{c}{\displaystyle
  \frac{\xi,\p \ar{w_1} \xii,\p' \quad \xi,\q \ar{w_2} \xii,\q'}{\xi,\p+\q \ar{w_1\wedge w_2} \xii,\p'+\q'}
  }
  & \hspace{-5em}\mbox{\small$(\forall w_1,w_2\in \W)$}
\end{array}$$
\end{table}

\subsubsection{Sequential Processes.}

The structural operational semantics of \tawn, given in
Tables~\ref{tab:sos sequential}--\ref{tab:sos network}, is in the style of Plotkin \cite{Pl04}
and describes how one internal state can evolve into another by performing an \emph{action}.

A difference with AWN is that some of the transitions are time steps.
On the level of node and network expressions they are labelled ``$\tick$''
and the parallel composition of multiple nodes can perform such a transition iff each of those
nodes can---see the third rule in Table~\ref{tab:sos network}.
On the level of sequential and parallel process expressions, time-consuming
transitions are labelled with \emph{wait actions} from $\W = \{\w,\ws,\wtr,\wrs\}\subseteq\act$ and
\emph{transmission actions} from $\RW=\{\Rw{w_1} \mid w_1 \mathbin\in \W \wedge R \subseteq \tIP\}\subseteq\act$.
Wait actions $w_1\mathbin\in\W$ indicate that the system is waiting, possibly only as long as it
fails to synchronise on a \textbf{receive} action ($\wtr$), a
\begin{wrapfigure}[6]{r}{0.26\textwidth}\vspace{-4ex}
\centering
\small $\begin{array}{c|cccc}
\wedge& \w   & \wtr & \ws  & \wrs \\
\hline
 \w   & \w   & \wtr & \ws  & \wrs \\
 \wtr & \wtr & \wtr & \wrs & \wrs \\
 \ws  & \ws  & \wrs & \ws  & \wrs \\
 \wrs & \wrs & \wrs & \wrs & \wrs
\end{array}$
\end{wrapfigure}%
 \textbf{send} action ($\ws$) or both of those ($\wrs$); actions $\Rw{w_1}$ indicate that the system
is transmitting a message
while the current transmission range of the node is $R \subseteq \tIP$.
In the operational rule for choice (+) we combine any two
wait actions $w_1,w_2\in\W$ with the operator $\wedge$, which 
joins the conditions under which these wait actions can occur. 

In Table~\ref{tab:sos sequential}, which gives the semantics of sequential process expressions,
a state is given as a pair $\xi,p$ of a sequential process expression $p$ and a valuation $\xi$ of
the data variables maintained by $p$.
The set $\act$ of actions that can be executed by sequential and parallel process expressions, and
thus occurs as transition labels, consists of
$\colonact{R}{\starcastP{m}}$,
$\send{m}$,
$\deliver{\dval{d}}$,
$\receive{m}$,
durational actions $w_1$ and $\Rw{w_1}$,
and internal actions~$\tau$, for each choice of $R\subseteq \tIP$, $m \mathop{\in}\tMSG$, $\dval{d}\mathop{\in}\tDATA$ and $w_1\in\W$.
Here $\colonact{R}{\starcastP{m}}$ is the action of transmitting the message $m$, to be
received by the set of nodes $R$, which is the intersection of the set of intended
destinations with the nodes that are within transmission range throughout the transmission.
We do not distinguish whether this message has been broadcast, groupcast or unicast---the
differences show up merely in the value of $R$.

In Table~\ref{tab:sos sequential} $\xi[\keyw{var}:= v]$ denotes the
valuation that assigns the value $v$ to the variable \keyw{var}, and
agrees with $\xi$ on all other variables.
We use $\xi\timeinc$ as an abbreviation for $\xi[\now:=\xi(\now)\mathord+1]$,
the valuation $\xi$ in which the variable \now is incremented by 1. This describes the state
of data\linebreak[3] variables after 1 unit of time elapses, while no other changes in data occurred.
The empty valuation $\emptyset$ assigns values to no variables. Hence
$\emptyset[\keyw{var}_i:=v_i]_{i=1}^n$ is the valuation that
\emph{only} assigns the values $v_i$ to the variables $\keyw{var}_i$ for $i=1,\ldots,n$.
Moreover, $\xi(\dval{exp})\defined$, with \dval{exp} a data expression, is the
statement that $\xi(\dval{exp})$ is defined; this might fail because \dexp{exp} contains a variable
that is not in the domain of $\xi$ or because \dexp{exp} contains a partial function that is given
an argument for which it is not defined.

A state $\xi,r$ is \emph{unvalued}, denoted by $\xi(r)\mathord\uparrow$, if $r$ has the form
$\broadcastP{\dexp{ms}}.\p$,
$\groupcastP{\dexp{dests}}{\dexp{ms}}.\p$, \hfill
$\unicast{\dexp{dest}}{\dexp{ms}}.\p$, \hfill
$\send{\dexp{ms}}.\p$, \hfill
$\deliver{\dexp{data}}.\p$, \linebreak[3]
$\assignment{\keyw{var}:=\dexp{exp}}\p\,$ or
$\,X(\dexp{exp}_1,\ldots,\dexp{exp}_n)$ with
either $\xi(\dexp{ms})$ or $\xi(\dexp{dests})$ or $\xi(\dexp{dest})$ or $\xi(\dexp{data})$ or
$\xi(\dexp{exp})$ or some $\xi(\dexp{exp}_i)$ undefined.
From such a state no progress is possible.
However, the sixth last line in Table~\ref{tab:sos sequential} does allow time to progress.
We use $\xi(r)\defined$ to denote that a state is not unvalued.

Rule \tableref{rec} for process names in Table~\ref{tab:sos sequential} is
motivated and explained in \cite[\textsection4.1]{TR13}.
The variant \tableref{rec-w} of this rule for wait actions $w_1\in\W$ has been modified such that the recursion
is not yet unfolded while waiting. 
This simulates the behaviour of AWN where a process is only 
    unwound if the first action of the process can be performed.

In the subsequent rules \tableref{grd} and \tableref[ngrd]{$\neg$grd} for variable-binding guards $[\varphi]$, the notation
\plat{$\xi\stackrel{\varphi}{\rightarrow}\xii$} says that
$\xii$ is an extension of $\xi$ that satisfies $\varphi$: a valuation that agrees with
$\xi$ on all variables on which $\xi$ is defined, and valuates the
other variables occurring free in $\varphi$, such that the formula
$\varphi$ holds under $\xii$. All variables not free in $\varphi$ and
not evaluated by $\xi$ are also not evaluated by $\xii$.
Its negation \plat{$\xi\nar{\varphi}$} says that no such extension exists, and thus that $\varphi$
is false in the current state, no matter how we interpret the variables whose values are still undefined.
If that is the case, the process $[\varphi]p$ will idle by performing the action $\w$ (of waiting)
without changing its state, except that the variable \now will be incremented.

\begin{example}
The process $\assignment{\keyw{timeout}:=\now+2} [\now = \keyw{timeout}] p$ first
sets the variable \keyw{timeout} to 2 units after the current time. Then it encounters a guard that
evaluates to {\tt false}, and therefore takes a $\w$-transition, twice. After two time units,
the guard evaluates to {\tt true} and the process proceeds as $p$.
\pagebreak[3]
\end{example}

The process $\receive{\msg}.p$ can receive any message $m$ from the environment in which this
process is running. As long as the environment does not provide a message, this process will wait.
This is indicated by the transition labelled $\wtr$ in Table~\ref{tab:sos sequential}.
The difference between a $\wtr$-and a $\w$-transition is that the former can be taken only when the
environment does not synchronise with the $\textbf{receive}$-transition. In our semantics any state with
an outgoing $\wtr$-transition also has an outgoing $\textbf{receive}$-transition (see \Thm{SP-classification}), which
conceptually has priority over the $\wtr$-transition. Likewise the transition labelled $\ws$ is only enabled in
states that also admit a $\textbf{send}$-transition, and is taken only in a context where the
$\textbf{send}$-transition cannot be taken.

Rules \tableref{alt-l} and \tableref{alt-r}, defining the behaviour of the choice operator for non-wait actions 
are standard. Rule \tableref{alt-w} for wait actions says that a process $p+q$ can wait only if both $p$ and $q$
can wait; if one of the two arguments can make real progress, the choice process $p+q$ always chooses
this progress over waiting.  This is a direct generalisation of the law $p+\nil=p$ of CCS \cite{Mi89}.
As a consequence, a condition on the possibility of $\p$ or $\q$ to wait is inherited by $\p+\q$.
This gives rise to the transition label $\wrs$, that makes waiting conditional on the environment
failing to synchronising with a $\textbf{receive}$ as well as a $\textbf{send}$-transition.
In understanding the target $\xii,\p'{+}\q'$ of this rule, it is helpful to realise that whenever
$\xi,\p \ar{w_1} \xii,\q$, then $\q = \p$ and $\xii = \xi[\now\mathord+\mathord+]$;
see \Prop{time determinism}.

In order to give semantics to the transmission constructs (broadcast, groupcast, unicast),
the language of sequential processes is extended with the auxiliary construct\vspace{-1ex}
$$\stargcast{\dval{\range}}{\dval{m}}[n,o].\SP \prio \SP\ ,$$ 
with $m\in\tMSG$, $n,o\in\NN$ and $\range\subseteq \tIP$.
This is a variant of the \textbf{broadcast}-, \textbf{groupcast}- and \textbf{unicast}-constructs,
describing intermediate states of the transmission of message \dval{m}.
The argument \range of \textbf{*cast} denotes those intended
destinations that were not out of transmission range during the part of the transmission that
already took place.

In a state $\stargcast{\range}{\dval{m}}[n,o].p \prio q$ with $n>0$ the transmission
still needs between $n$ and $n\mathord+o$ time units to complete.
If $n=0$ the actual \textbf{*cast}-transition will take place; resulting in state $p$ if
the message is delivered to at least one node in the network (\range is non-empty), and $q$ otherwise.

Rule \tableref{gc} says that once a process commits to a
\textbf{groupcast}-transmission, it is going to behave as
$\colonact{\range}{\textbf{*cast}}(m)[n,o]$
with time parameters $n:=\LG$ and $o:=\DG$. The transmitted message $m$ is calculated
by evaluating the argument \dexp{ms}, and the  transmission range \range of
this \textbf{*cast} is initialised by evaluating the argument \dexp{dests}, indicating the intended
destinations of the \textbf{groupcast}. 
Rules \tableref{bc} and \tableref{uc} for \textbf{broadcast} and \textbf{unicast} are the same, except that in the case of
\textbf{broadcast} the intended destinations are given by the set $\tIP$ of \emph{all} possible destinations,
whereas a \textbf{unicast} has only one intended destination.
Moreover, only \textbf{unicast} exploits the difference in the continuation process depending on
whether an intended destination is within transmission range.
Subsequently, Rules \tableref{tr} and \tableref{tr-o} come into force; they allow time-consuming transmission steps to take
place, each decrementing one of the time parameters $n$ or $o$. Each time step of a transmission corresponds
to a transition labelled $\Rw{\w}$, where $R$ records the current transmission range. Since
sequential processes store no information on transmission ranges---this information is added only
when moving from process expressions to node expressions---at this stage of the description all
possibilities for the transmission range need to be left open, and hence there is a transition
labelled $\Rw{\w}$ for each choice of $R$.\footnote{Similar to $\receive{\msg}.p$ having a
transition for each possible incoming message~$m$.} When transitions for process expressions are
inherited by node expressions, only one of the transitions labelled $\Rw{\w}$ is going to survive, namely the one
where $R$ equals the transmission range given by the node expression (cf.~Rule~\tableref{n-t} in \Tab{sos node}).
Upon doing a transition $\Rw\w$, the range \range of the \textbf{*cast} is restricted to $R$.
As soon as $n\mathbin=0$, regardless of the value of $o$, the transmission is completed by the execution of
the action $\colonact{\range}{\textbf{*cast}(m)}$ (Rules \tableref{sc} and \tableref[nsc]{$\neg$sc}). Here the actual message
$m$ is passed on for synchronisation with \textbf{receive}-transitions of all nodes $\dval{ip}\in\range$.

This treatment of message transmission is somewhat different from the one in AWN\@.
There, the rule $\xi,\groupcastP{\dexp{dests}}{\dexp{ms}}.\p \ar{\groupcastP{\xi(\dexp{dests})}{\xi(\dexp{ms})}}
\xi,\p$ describes the behaviour of the \textbf{groupcast} construct for sequential processes, and the rule
\vspace{-4ex} 

{\small$$  \frac{P \ar{\groupcastP{D}{m}} P'}
  {\rule[10pt]{0pt}{1pt}
   \dval{ip}\mathbin:P\mathbin:R \ar{\colonact{R\cap D}{\starcastP{m}}} \dval{ip}\mathbin:P'\mathbin:R}$$}%
lifts this behaviour from processes to nodes. In this last stage the \textbf{groupcast}-action is
unified with the \textbf{broadcast}- and \textbf{unicast}-action into a \textbf{*cast},
at which occasion the range of the \textbf{*cast} is calculated as the intersection of the intended
destinations $D$ of the \textbf{groupcast} and the ones in transmission range $R$. In \tawn, on the other hand,
the conversion of \textbf{groupcast} to \textbf{*cast} happens already at the level of sequential processes.

{%local redef of \parl
\renewcommand{\parl}{\mathop{\ensuremath{\!\langle\!\langle\!}}}
\begin{table}[t]
\caption{Structural operational semantics for parallel process expressions
\label{tab:sos parallel}}

\vspace*{-5ex}
$$\begin{array}{@{}c@{}}
\tablelabel{p-al}\hspace{1mm} 
\displaystyle
  \frac{P \ar{a} P'}{P\parl Q \ar{a} P'\parl Q}%
  \,\mbox{\small$\left(\begin{array}{@{}c@{}}\forall a\neq \receive{m},\\a \mathop{\not\in} \W, a \mathop{\not\in} \RW\\
  \end{array}\right)$}
  \quad\hspace{-1pt}
\tablelabel{p-ar}\hspace{1mm} 
  \frac{Q \ar{a} Q'}{P\parl Q \ar{a} P\parl Q'}%
\,\mbox{\small$\left(\begin{array}{@{}c@{}}\forall a\neq \send{m},\\a \mathop{\not\in} \W, a \mathop{\not\in} \RW\end{array}\right)$}
\\[15pt]
\tablelabel{p-a}\hspace{1mm} 
\displaystyle
  \frac{P \ar{\receive{m}} P'\quad Q \ar{\send{m}} Q'}
       {P\parl Q \ar{\tau} P'\parl Q'}
    ~\,\mbox{\small($\forall m\mathbin\in\tMSG$)}
\qquad
\tablelabel{p-w}\hspace{1mm} 
  \frac{P \ar{w_1} P'\quad Q \ar{w_2} Q'}
       {P\parl Q \ar{w_3} P'\parl Q'}
\\[15pt]
\tablelabel{p-tl}\hspace{1mm} 
\displaystyle
\frac{P\!\ar{R\mathbin{:}w_1} P'\quad\! Q\!\ar{w_2} Q'}
	       {P\parl Q \ar{R\mathbin{:}w_3} P'\hspace{-1pt}\parl Q'}
\quad
\tablelabel{p-tr}\hspace{1mm} 
\frac{P\! \ar{w_1} P'\quad\! Q\! \ar{R\mathbin{:}w_2} Q'}
       {P\parl Q \ar{R\mathbin{:}w_3} P'\parl Q'}
\quad
\tablelabel{p-t}\hspace{1mm} 
\frac{P\! \ar{R\mathbin{:}w_1} P'\quad\! Q\! \ar{R\mathbin{:}w_2} Q'}
       {P\parl Q \ar{R\mathbin{:}w_3} P'\parl Q'}
\\[12pt]
\hfill\!(\forall w_{1},w_{2},w_{3}\in\W, w_3=w_1\parl w_2)
\end{array}$$
\vspace*{-5.5ex}
\end{table}
}

\vspace*{-0ex}
\subsubsection{Parallel Processes.}
Rules \tableref{p-al}, \tableref{p-ar} and \tableref{p-a} of Table \ref{tab:sos parallel} are taken from AWN, and formalise
the description of the operator $\parl$ given in \SSect{syntax}.
Rule \tableref{p-w} stipulates under which conditions a process $P\parl Q$
can do a wait action, and 
\begin{wrapfigure}[5]{r}{0.25\textwidth}
\vspace{-5ex}
\label{parallel}
\hypertarget{parallel}{
\centering
\small $\begin{array}{c|cccc}
\parl
      & \w   & \wtr & \ws  & \wrs \\
\hline
 \w   & \w   & \wtr & \w   & \wtr \\
 \wtr & \w   & \wtr &  -   &  -   \\
 \ws  & \ws  & \wrs & \ws  & \wrs \\
 \wrs & \ws  & \wrs &  -   &  -
\end{array}$}
\end{wrapfigure}%
of which kind. 
Here $\parl$ is also
a partial binary function on the set $\W$, specified by
the table on the right.
The process $P\parl Q$ can do a wait action only if both $P$ and $Q$ can do so.
In case $P$ can do a $\wtr$ or a $\wrs$-action, $P$ can also do a \textbf{receive}
and in case $Q$ can do a $\ws$ or a $\wrs$, $Q$ can  \pagebreak also do a \textbf{send}.
When both these possibilities  apply, the \textbf{receive} of $P$
synchronises with the \textbf{send} of $Q$ into a $\tau$-step, which
has priority over waiting. 
In the other 12 cases no synchronisation between $P$ and $Q$ is
possible, and we do obtain a wait action.
Since a \textbf{receive}-action of $P$ that does not synchronise with $Q$
is dropped, so is the corresponding side condition of a wait action of 
$P$. 
Hence (within the remaining 12 cases) a $\wtr$ of $P$ is treated as a $\w$,
and a $\wrs$ as a $\ws$. Likewise a $\ws$ of $Q$ is treated as a $\w$,
and a $\wrs$ as a $\wtr$. This leaves 4 cases to be decided.
In all four, we have $\w_1 \parl \w_2 = \w_1 \wedge \w_2$.

Time steps $\Rw{w_1}$ are treated exactly like wait actions from $\W$
(cf.\ Rules \tableref{p-tl}, \tableref{p-tr} and \tableref{p-t}).
If for instance $P$ can do a $\Rw{\w}$, meaning that it spends a unit of time
on a transmission, while $Q$ can do a $\wtr$, meaning that it waits a unit
of time only when it does not receive anything from another source,
the result is that $P\parl Q$ can spend a unit of time transmitting something,
but only as long as $P\parl Q$ does not receive any message; if it does,
the receive action of $Q$ happens with priority over the wait action of $Q$,
and thus occurs before $P$ spends a unit of time transmitting.

\subsubsection{Node and Network Expressions.}
The operational semantics of node and network expressions of
Tables~\ref{tab:sos node} and~\ref{tab:sos network} uses transition labels
\tick,
$\colonact{R}{\starcastP{m}}$,
$\colonact{H\neg K}{\listen{m}}$,
$\colonact{\dval{ip}}{\deliver{\dval{d}}}$,
$\textbf{connect}(\dval{ip},\dval{ip}')$,
$\textbf{disconnect}(\dval{ip},\dval{ip}')$,
$\tau$
and $\colonact{\dval{ip}}{\textbf{newpkt}(\dval{d},\dval{dip})}$.
As before, $m\in\tMSG$, $d\in\tDATA$, $R\subseteq \tIP$, and $\dval{ip},\dval{ip}'\in\tIP$.
Moreover, $H,K\subseteq\tIP$ are sets of IP addresses.

The actions $\colonact{R}{\starcastP{m}}$ are inherited by nodes from the processes that
run on these nodes (cf.~Rule \tableref{n-sc}).
The action $\colonact{H\neg K}{\listen{m}}$ states that the message $m$
simultaneously arrives at all addresses $\dval{ip}\mathbin\in H$, and fails to
arrive at all addresses $\dval{ip}\mathbin\in K$.
The rules of Table~\ref{tab:sos network} let a $\colonact{R}{\starcastP{m}}$-action of one node
synchronise with an $\listen{m}$ of all other nodes, where this
$\listen{m}$ amalgamates the arrival of message $m$ at the nodes in
the transmission range $R$ of the $\starcastP{m}$, and the non-arrival at the
other nodes. Rules \tableref{n-rcv} and \tableref{n-dis}
state that arrival of a message at a node happens if and only if the
node receives it, whereas non-arrival can happen at any time.
This embodies our assumption that, at any time, any message that is
transmitted to a node within range of the sender is actually received by that node.
(Rule \tableref{n-dis} may appear to say that any node \dval{ip} has the option to
  disregard any message at any time. However, the encapsulation
  operator (below) prunes away all such disregard transitions that do
  not synchronise with a cast action for which \dval{ip} is out of range.)

The action $\send{m}$ of a process does not give rise to any action of
the corresponding node---this action of a sequential process cannot
occur without communicating with a receive action of another sequential
process running on the same node.
Time-consuming actions $w_1$ and $\Rw{w_1}$, with $w_1\in\W$, of a process are renamed into $\tick$ on
the level of node expressions.\footnote{Rule \tableref{n-t} ensures that only those
  $R\mathbin{:}w_1$-transitions survive for which $R$ is the current transmission range of the node.}
 All we need to remember of these actions is that they take one unit
of time. Since on node expressions the actions $\send{m}$ have been dropped, 
\pagebreak[3] the side condition
making the wait actions $\ws$ and $\wrs$ conditional on the absence of a \textbf{send}-action can be
dropped as well. The priority of \textbf{receive}-actions over the wait action $\wtr$ can now also be
dropped, for in the absence of \textbf{send}-actions, \textbf{receive}-actions are entirely
reactive.  A node can do a \textbf{receive}-action only when another node, or the application layer,
casts a message, and in
this case that other node is not available to synchronise with a $\tick$-transition.

\begin{table}[t]
\caption{Structural operational semantics for node expressions
\label{tab:sos node}}

\vspace{-5ex}
$$\begin{array}{@{}c@{\quad}c@{}}
\tablelabel{n-sc}\hspace{1mm} 
\displaystyle
  \frac{P \ar{\colonact{\range}{\starcastP{m}}} P'}
  {\rule[13pt]{0pt}{1pt}
   \dval{ip}\mathbin{:}P\mathord{:}R \ar{\colonact{\range}{\starcastP{m}}} \dval{ip}\mathbin{:}P'\mathord{:}R}
&
\tablelabel{n-rcv}\hspace{1mm} 
\displaystyle
  \frac{P \ar{\receive{m}} P'}
  {\rule[13pt]{0pt}{1pt}
   \dval{ip}\mathbin{:}P\mathord{:}R \ar{\colonact{\{\dval{ip}\}\neg\emptyset}{\listen{m}}} \dval{ip}\mathbin{:}P'\mathord{:}R}
\\[18pt]
\tablelabel{n-del}\hspace{1mm} 
\displaystyle
  \frac{P \ar{\deliver{\dval{d}}} P'}
  {\rule[13pt]{0pt}{1pt}
   \dval{ip}\mathbin{:}P\mathord{:}R \ar{\colonact{\dval{ip}}{\deliver{\dval{d}}}} \dval{ip}\mathbin{:}P'\mathord{:}R}
&
\tablelabel{n-dis}\hspace{1mm} 
 \dval{ip}\mathbin{:}P\mathord{:}R \ar{\colonact{\emptyset\neg\{\dval{ip}\}}{\listen{m}}} \dval{ip}\mathbin{:}P\mathord{:}R
\\[16pt]\multicolumn{2}{@{}c@{}}{
\tablelabel[n-t]{n-$\tau$}\hspace{1mm} 
\displaystyle
  \frac{P \ar{\tau} P'}
  {\dval{ip}\mathbin{:}P\mathord{:}R \ar{\tau} \dval{ip}\mathbin{:}P'\mathord{:}R}
\quad
\tablelabel{n-w}\hspace{1mm} 
\displaystyle
  \frac{P \ar{w_1} P'}
  {\rule[13pt]{0pt}{1pt}
   \dval{ip}\mathbin{:}P\mathord{:}R \ar{\tick} \dval{ip}\mathbin{:}P'\mathord{:}R}
\quad
\tablelabel{n-t}\hspace{1mm} 
\displaystyle
  \frac{P \ar{R\mathord{:}w_1} P'}
  {\rule[13pt]{0pt}{1pt}
   \dval{ip}\mathbin{:}P\mathord{:}R \ar{\tick} \dval{ip}\mathbin{:}P'\mathord{:}R}
}
\\[16pt]
\multicolumn{2}{@{}r@{}}{
\mbox{\footnotesize $\left(\!\forall w_1 \mathbin\in \W \right)$}
}
\\[5pt]
\tablelabel{con}\hspace{1mm} 
\displaystyle
  \dval{ip}\!\mathbin{:}\!P\!\mathbin{:}\!R \ar{\textbf{connect}(\dval{ip},\dval{ip}')} \dval{ip}\!\mathbin{:}\!P\!\mathbin{:}\!R\mathop\cup\{\dval{ip}'\}
  \hspace{-2pt}
&
\tablelabel{dis}\hspace{1mm} 
  \dval{ip}\!\mathbin{:}\!P\!\mathbin{:}\!R \ar{\textbf{disconnect}(\dval{ip},\dval{ip}')} \dval{ip}\!\mathbin{:}\!P\!\mathbin{:}\!R\mathop-\{\dval{ip}'\}
\end{array}$$
\end{table}

\begin{table}[t]
\caption{Structural operational semantics for network expressions
\label{tab:sos network}}

\vspace{-5ex}
{\small
\[\begin{array}{@{}c@{}}
\tablelabel{nw-tl/nw-tr}\hspace{2mm} 
\displaystyle
  \frac{M \ar{\colonact{R}{\starcastP{m}}} M' \quad N \ar{\colonact{H\neg K}{\listen{m}}} N'}
  {\rule[11pt]{0pt}{1pt}
   M \| N \ar{\colonact{R}{\starcastP{m}}} M' \| N'\qquad
   N \| M \ar{\colonact{R}{\starcastP{m}}} N' \| M'}
   \qquad\mbox{\footnotesize
  $\left(\begin{array}{@{}c@{}}H\subseteq R,\\K {\cap} R = \emptyset\end{array}\right)$}
\\[21pt]
\tablelabel{arr}\hspace{2mm} 
  \displaystyle
  \frac{M \ar{\colonact{H\neg K}{\listen{m}}} M' \quad N \ar{\colonact{H'\neg K'}{\listen{m}}} N'}
  {\rule[11pt]{0pt}{1pt}M \| N \ar{\colonact{(H\cup H')\neg(K\cup K')}{\listen{m}}} M' \| N'}
  \qquad\!
  \tablelabel{tck}\hspace{2mm} 
  \frac{M \ar{\tick} M' \quad N \ar{\tick} N'}
  {\rule[11pt]{0pt}{1pt}M \| N \ar{\tick} M' \| N'}
\\[16pt]
  \displaystyle
  \tablelabel{nw-al}\hspace{2mm} 
  \frac{M \ar{a} M'}{M \| N \ar{a} M' \| N}
  \qquad
  \tablelabel{nw-ar}\hspace{2mm} 
  \frac{N \ar{a} N'}{M \| N \ar{a} M \| N'}
  \qquad
  \tablelabel{e-a}\hspace{2mm} 
  \frac{M \ar{a} M'}{
   [M] \ar{a} [M']}
\\[14pt]
~\hfill\!\!
\mbox{\footnotesize $
(\forall a\mathbin\in\{
                        \colonact{\dval{ip}}{\deliver{\dval{d}}},\tau,     
                                     \textbf{connect}(\dval{ip},\dval{ip}'),
                                      \textbf{disconnect}(\dval{ip},\dval{ip}')
\})$}
\\[8pt]
  \displaystyle
  \tablelabel{e-tck}\hspace{1mm} 
  \frac{M \ar{\tick} M'}{[M] \ar{\tick} [M']}
  \quad\!
  \tablelabel{e-sc}\hspace{1mm} 
  \frac{M \mathbin{\ar{\colonact{R}{\starcastP{m}}}} M'}{[M] \ar{\tau} [M']}
  \quad\!
  \tablelabel{e-np}\hspace{1mm} 
  \frac{M \ar{\colonact{\{\dval{ip}\}\neg K}{\listen{\newpkt{\dval{d}}{\dval{dip}}}}} M'}
  {\rule[11pt]{0pt}{1pt}
   [M] \ar{\colonact{\dval{ip}}{\textbf{newpkt}(\dval{d},\dval{dip})}} [M']}
\end{array}\]}
\vspace*{-5ex}
\end{table}



Internal actions $\tau$ and the action $\colonact{\dval{ip}}{\deliver{\dval{d}}}$
are simply inherited by node expressions from the processes that run
on these nodes (Rules \tableref[n-t]{n-$\tau$} and \tableref{n-del}), and are interleaved in the parallel composition of
nodes that makes up a network. Finally, we allow actions
$\textbf{connect}(\dval{ip},\dval{ip}')$ and
$\textbf{disconnect}(\dval{ip},\dval{ip}')$ for
$\dval{ip},\dval{ip}'\mathop\in \tIP$ modelling a change in network
topology. In this formalisation node $\dval{ip}'$ may be in the range of node
$\dval{ip}$, meaning that $\dval{ip}$ can send to $\dval{ip}'$,
even when the reverse does not hold. For some applications, in
particular the one to AODV in \Sect{aodv}, it is useful to assume that
$\dval{ip}'$ is in the range of $\dval{ip}$ if and only if $\dval{ip}$
is in the range of $\dval{ip}'$. 
This symmetry can be enforced by adding the following rules to Table~\ref{tab:sos node}:\pagebreak[3]

\noindent
{\small
\[\begin{array}{@{}c@{\qquad}c@{}}
\displaystyle
  \dval{ip}\!:\!P\!:\!R \ar{\textbf{connect}(\dval{ip}',\dval{ip})} \dval{ip}\!:\!P\!:\!R\cup\{\dval{ip}'\}
&
  \dval{ip}\!:\!P\!:\!R \ar{\textbf{disconnect}(\dval{ip}',\dval{ip})} \dval{ip}\!:\!P\!:\!R-\{\dval{ip}'\}
\\[11pt]\displaystyle
  \frac{\dval{ip} \not\in \{\dval{ip}'\!,\dval{ip}''\}}
  {\rule[11pt]{0pt}{1pt}
   \dval{ip}\!:\!P\!:\!R \ar{\textbf{connect}(\dval{ip}'\!,\dval{ip}'')} \dval{ip}\!:\!P\!:\!R}
&\displaystyle
  \frac{\dval{ip} \not\in \{\dval{ip}'\!,\dval{ip}''\}}
  {\rule[11pt]{0pt}{1pt}
   \dval{ip}\!:\!P\!:\!R \ar{\textbf{disconnect}(\dval{ip}'\!,\dval{ip}'')} \dval{ip}\!:\!P\!:\!R}
\end{array}\]}%
and replacing the rules in the third line of \Tab{sos network} for (dis)connect actions by\vspace{-1ex}
{\small
\[
  \frac{M \ar{a} M' \quad
        N \ar{a} N'}
  {M \| N \ar{a} M' \| N'}
  \qquad
  \frac{M \ar{a} M'}{
   [M] \ar{a} [M']}
  \qquad\mbox{\footnotesize
  $
  \left(\forall a\in\left\{\begin{array}{c}\textbf{connect}(\dval{ip},\dval{ip}'),\\
                                           \textbf{disconnect}(\dval{ip},\dval{ip}')
                    \end{array}\right\}\right).$}
\]}%
The main purpose of the encapsulation operator is to ensure that no
messages will be received that have never been sent. In a parallel
composition of network nodes, any action $\receive{\dval{m}}$ of one
of the nodes \dval{ip} manifests itself as an action $\colonact{H\neg
K}{\listen{\dval{m}}}$ of the parallel composition, with $\dval{ip}\in
H$. Such actions can happen (even) if within the parallel composition
they do not communicate with an action $\starcastP{\dval{m}}$ of
another component, because they might communicate with a
$\starcastP{\dval{m}}$ of a node that is yet to be added to the
parallel composition. However, once all nodes of the network are
accounted for, we need to inhibit unmatched arrive actions,
as otherwise our formalism would allow any node at any time to receive
any message. One exception however are those arrive actions
that stem from an action $\receive{\newpkt{\dval{d}}{\dval{dip}}}$ of a
sequential process running on a node, as those actions represent
communication with the environment. Here, we use the function
$\newpktID$, which we assumed to exist.\footnote{%
\newcommand{\npkt}{\textbf{newpkt}\xspace}%
To avoid the function $\newpktID$ we could have introduced a new
primitive \npkt, which is dual to \textbf{deliver}.}
It models the injection of new data $\dval{d}$ for destination $\dval{\dip}$.

The encapsulation operator passes through internal actions, as well as
delivery of data to destination nodes, this being an interaction
with the outside world (Rule \tableref{e-a}). $\starcastP{m}$-actions are declared internal
actions at this level (Rule \tableref{e-sc}); they cannot be steered by the outside world.
The connect and disconnect actions are passed through in
Table~\ref{tab:sos network} (Rule \tableref{e-a}), thereby placing them under control of the
environment; to make them nondeterministic, their rules should have a
$\tau$-label in the conclusion, or alternatively
$\textbf{connect}(\dval{ip},\dval{ip}')$ and $\textbf{disconnect}(\dval{ip},\dval{ip}')$
should be thought of as internal actions. Finally, actions
$\listen{m}$ are simply blocked by the encapsulation---they
cannot occur without synchronising with a $\starcastP{m}$---except for
$\colonact{\{\dval{ip}\}\neg K}{\listen{\newpkt{\dval{d}}{\dval{dip}}}}$
with $\dval{d}\in\tDATA$ and $\dval{dip}\in \tIP$ (Rule \tableref{e-np}). This action
represents new data \dval{d} that is submitted by a
client of the modelled protocol to node $\dval{ip}$, for delivery at
destination \dval{dip}.

\subsubsection{Optional Augmentations to Ensure Non-Blocking Broadcast.}
\label{ssec:non-blocking}

Our process algebra, as presented above, is intended for networks in which
each node is \emph{input enabled} \cite{LT89}, meaning that it is
always ready to receive any message, i.e., able to engage in the
transition $\receive{m}$ for any $m\in \tMSG$---in the default
version of \tawn, network expressions are required to
have this property. In our model of AODV
(Section~\ref{sec:aodv}) we will ensure this by equipping each node
with a message queue that is always able to accept messages for later
handling---even when the main sequential process is currently busy.
This makes our model input enabled and hence \emph{non-blocking}, meaning that no sender can
be delayed in transmitting a message simply because one of the
potential recipients is not ready to receive it.


In \cite{ESOP12,TR13} we additionally presented
two versions of AWN without the
requirement that all nodes need to be input enabled: one in which we
kept the same operational semantics and simply accept blocking,
and one were we added operational rules to avoid blocking,
thereby giving up on the requirement that any broadcast
message is received by all nodes within transmission range.

The first solution does not work for \tawn, as it would give rise to
\emph{time deadlocks}, reachable states where time is unable to
progress further. 

The second solution is therefore our only alternative to
requiring input enabledness for \tawn. As in \cite{ESOP12,TR13},
it is implemented by the addition of the rule
\hypertarget{non-blocking}{$$\frac{P \nar{\receive{m}}}  {\rule[13pt]{0pt}{1pt}
  \dval{ip}:P:R \ar{\colonact{\{\dval{ip}\}\neg\emptyset}{\listen{m}}} \dval{ip}:P:R}\;.
  \label{non-blocking}$$}
It states that a message may arrive at a node \dval{ip} regardless whether
the node is ready to receive it or not; if it is not ready, the message is simply
ignored, and the process running on the node remains in the same state.

In \cite[\textsection4.5]{TR13} also a variant of this idea is presented that 
avoids negative premises, yet leads to the same transition system.
The same can be done to \tawn in the same way, we
skip the details and refer to \cite[\textsection4.5]{TR13}.

\subsection{Results on the Process Algebra}

In this section we list a couple of useful properties of our timed process algebra. 
In particular, we show that wait actions do not change the data state, except for the value of \now.
Moreover, we show the absence of \emph{time deadlocks}:
a complete network $N$ described by T-AWN always admits a transition,\vspace{1pt} independently of the outside environment.
More precisely, either $N \ar{\tick}$, or $N \ar{\colonact{\dval{ip}}{\deliver{\dval{d}}}}$ or $N \ar{\tau}$.
We also show that
our process algebra admits a translation into one without data structure. 
The operational rules of the translated process algebra are in the de Simone format \cite{dS85}, which 
immediately implies that strong bisimilarity is a congruence, and
yields the associativity of
our parallel operators. Last, we show that \tawn and \awn are related by a simulation relation.
Due to lack of space, most of the proofs are omitted, they can be found in \mbox{\App{proofs}}.

\begin{proposition} On the level of sequential processes, wait actions
change only the value of the variable \now, i.e.,
$\xi, \p \ar{w_1} \zeta, \q  \Rightarrow (\p=\q \wedge \zeta=\xi\timeinc)$.
\label{prop:time determinism}%
\label{w-caracterisation} %
\end{proposition}

\begin{proofsketch}
One inspects all rules of Table~\ref{tab:sos sequential} that can
generate $w$-steps, and then reasons inductively on the derivation of
these steps.
\end{proofsketch}

Similarly, it can be observed that for transmission actions (actions from the set $\R\mathop{:}\W$)
the data state does not change either; 
the process, however, changes. That means \plat{$\xi, \p \ar{rw} \zeta, \q  \Rightarrow \zeta=\xi\timeinc$}
for all $rw \in \RW$.
Furthermore, this result can easily be lifted to all other layers of our process algebra (with minor adaptations: for example on node expressions one has
to consider $\tick$ actions).

To shorten the forthcoming definitions and properties we 
use the following abbreviations:
\noindent
\newcommand{\arrec}{\ar{\makebox[22pt]{\scriptsize\bf rcv.}}}
\newcommand{\arsend}{\ar{\makebox[22pt]{\scriptsize\bf send}}}
\newcommand{\arwait}{\ar{\makebox[22pt]{\scriptsize\bf wait}}}
\newcommand{\arother}{\ar{\makebox[22pt]{\scriptsize\bf other}}}
\newcommand{\arinb}{\ar{\makebox[19.7pt]{\scriptsize\bf inb}}}
\newcommand{\narrec}{\nar{\makebox[19.7pt]{\scriptsize\bf rcv.}}}
\newcommand{\narsend}{\nar{\makebox[19.7pt]{\scriptsize\bf send}}}
\newcommand{\narwait}{\nar{\makebox[19.7pt]{\scriptsize\bf wait}}}
\newcommand{\narother}{\nar{\makebox[19.7pt]{\scriptsize\bf other}}}
\newcommand{\narinb}{\nar{\makebox[19.7pt]{\scriptsize\bf inb}}}
\begin{enumerate}
\item $P {\arrec}$ iff $P{\ar{\receive{m}}}$ for some $m\in\tMSG$,
\item $P {\arsend}$ iff $P{\ar{\send{m}}}$ for some $m\in\tMSG$,
\item $P {\arwait}$ iff $P{\ar{w_1}}$ for some $w_1\in\W$,
\item $P {\arother}$ iff $P{\ar{a}}$ for some $a\in\act$ not of the forms above,
\end{enumerate}
where $P$ is a parallel process expression---possibly
incorporating the construct
$\stargcast{\range}{\dval{m}}[n,o].\p$, but never in a $+$-context.
Note that the last line covers also transmission actions $rw\in\RW$.
The following result shows that the wait actions of a sequential
process (with data evaluation) $P$ are completely determined
by the other actions $P$ offers.

\begin{theorem}
\label{thm:SP-classification}
Let $P$ be a state of a sequential process.\vspace{-1ex}
\begin{enumerate}
\item $P{\stackrel{\w}{\longrightarrow}}$   	\quad iff \quad $P {\narrec} \wedge P {\narsend} \wedge P {\narother}$\,.
\item $P{\stackrel{\wtr}{\longrightarrow}}$	\quad iff \quad $P {\arrec}   \wedge P {\narsend} \wedge P {\narother}$\,.
\item $P{\stackrel{\ws}{\longrightarrow}}$	\quad iff \quad $P {\narrec} \wedge P {\arsend}   \wedge P {\narother}$\,.
\item $P{\stackrel{\wrs}{\longrightarrow}}$ \quad iff \quad $P {\arrec}   \wedge P {\arsend}   \wedge P {\narother}$\,.
\end{enumerate}
\end{theorem}

\begin{proofsketch}
The proof is by structural induction.
It requires, however, a distinction between guarded terms (as defined in Footnote~\ref{guarded})
 and unguarded ones.
\end{proofsketch}
We could equivalently have omitted all transition rules involving wait actions from
\Tab{sos sequential}, and defined the wait transitions for sequential processes as described by 
\Thm{SP-classification} and \Prop{time determinism}.
That our transition rules give the same result constitutes a sanity check of our operational semantics.

\Thm{SP-classification}
does not hold in the presence of unguarded recursion.\vspace{1pt}
A counterexample is given by the expression $X()$
with \plat{$X()\stackrel{{\it def}}{=}X()$}, for which we would have
$X() {\narrec} \wedge X() {\narsend} \wedge X() {\narother} \wedge X() {\narwait}$.

\begin{lemma}\label{lem:transmission actions}
Let $P$ be a state of a sequential or parallel process.
If \plat{$P \ar{\Rw w_1}$} for some $R\subseteq\tIP$ and $w_1\mathbin\in\W$ then
\plat{$P \ar{R'\!\mathop:w_1}$} for any $R'\subseteq \tIP$.
\end{lemma}

\begin{observation}\label{obs:transmission actions}
Let $P$ be a state of a sequential process.
If \plat{$P \ar{\Rw w_1}$} for some $w_1\mathbin\in\W$ then $w_1$ must be $\w$ and all
outgoing transitions of $P$ are labelled $R'\mathop:\w$.
\end{observation}
For $N$ a (partial) network expression, or a parallel process expression, write
$N {\arinb}$ iff $N{\ar{a}}$ with $a$ of the form\vspace{1pt}
$\colonact{R}{\starcastP{m}}$, $\colonact{\dval{ip}}{\deliver{\dval{d}}}$ (or
$\deliver{\dval{d}}$) or $\tau$---an \emph{instantaneous non-blocking action}.\vspace{1pt}
Hence, for a parallel process expression $P$, \plat{$P {\arother}$} iff \plat{$P {\arinb}$} or \plat{$P \ar{\Rw w_1}$} for $w_1\mathbin\in\W$.
Furthermore, write $P {\ar{\bf time}}$ iff $P{\ar{w_1}}$ or $P{\ar{\Rw w_1}}$ for some $w_1\mathbin\in\W$.
We now lift Theorem~\ref{thm:SP-classification} to the level of parallel processes.\pagebreak[3]

\begin{theorem}
\label{thm:PP-classification}
Let $P$ be a state of a parallel process.\vspace{-1ex}
\begin{enumerate}
\item $P{\stackrel{\w}{\longrightarrow}} \vee P{\ar{\Rw\w~\,}}$\hspace{-0.7pt} \quad iff \quad $P {\narrec} \wedge P {\narsend} \wedge P {\narinb}$\,.
\item $P{\stackrel{\wtr}{\longrightarrow}} \vee P{\ar{\Rw\wtr\,}}$ \quad iff \quad $P {\arrec} \wedge P {\narsend} \wedge P {\narinb}$\,.
\item $P{\stackrel{\ws}{\longrightarrow}} \vee P{\ar{\Rw\ws\,}}$ \quad iff \quad $P {\narrec} \wedge P {\arsend} \wedge P {\narinb}$\,.
\item $P{\stackrel{\wrs}{\longrightarrow}} \vee P{\ar{\Rw\wrs}}$\! \quad iff \quad $P {\arrec} \wedge P {\arsend} \wedge P {\narinb}$\,.
\end{enumerate}
\end{theorem}

\begin{corollary}
\label{cor:PP-classification}
Let $P$ be a state of a parallel process.
Then 
$P{\ar{\bf time}}$ 
iff 
$P {\nar{\bf inb}}$.
\qed
\end{corollary}

\begin{lemma}\label{lem:arrive-enabled}
Let $N$ be a partial network expression\vspace{1pt} with $L$ the set of addresses of the nodes of $N$.
Then $N{\ar{\colonact{H\neg K}{\listen{\dval{m}}}}}$\,, for any partition
$L=H\dcup K$ of $L$ into sets $H$ and $K$,
and any $m\in\tMSG$.
\end{lemma}

\noindent
Using this lemma, we can finally show one of our main results: an (encapsulated)
network expression can perform a time-consuming action iff an instantaneous non-blocking action is not possible. 
\begin{theorem}
\label{thm:N-classification}
Let $N$ be a partial or complete network expression.\\
Then $N{\ar{\tick}}$ \quad iff \quad $N {\nar{\bf inb}}$.
\end{theorem}

\prf
We apply structural induction on $N$. First suppose $N$ is a node expression $\dval{ip}\mathop:P\mathop:R$.
Then $N{\ar{\tick}}$ iff $P{\ar{w_1}}\vee P{\ar{\Rw w_1}}$ for some $w_1\mathbin\in\W$.
By \Lem{transmission actions} this is the case iff 
$P{\ar{w_1}}\vee P{\ar{R'\mathop:w_1}}$ for some $R'\subseteq\tIP$ and $w_1\mathbin\in\W$, i.e., iff $P {\ar{\bf time}}$.
Moreover $N{\arinb}$ iff $P{\arinb}$.
Hence the claim follows from \Cor{PP-classification}.

Now suppose $N$ is a partial network expression $M_1\|M_2$.
In case $M_i{\nar{\bf inb}}$ for $i=1,2$ then $N{\nar{\bf inb}}$.
By induction $M_i{\ar{\tick}}$ for $i=1,2$, and hence $N{\ar{\tick}}$.
Otherwise, $M_i{\arinb}$ for $i=1$ or $2$. Now $N {\arinb}$.
In case $M_i{\ar{\tau}}$ or $M_i{\ar{\colonact{\dval{ip}}{\deliver{\dval{d}}}}}$
this follows from the third line of \Tab{sos network}; if 
$M_i{\ar{\colonact{R}{\starcastP{m}}}}$
it follows from the first line, in combination with \Lem{arrive-enabled}.
By induction $M_i{\nar{\tick}}$, and thus $N{\nar{\tick}}$.

Finally suppose that $N$ is a complete network expression $[M]$.
By the rules of \Tab{sos network} $N{\ar{\tick}}$ iff $M{\ar{\tick}}$, and
$N{\arinb}$ iff $M{\ar{\bf inb}}$, so the claim follows from the case for partial network expressions.
\eprf

\begin{corollary}
\label{no_deadlock}
A complete network $N$ described by T-AWN always admits a transition, independently of the outside environment, 
i.e., $\forall N, \exists a$ such that $N \ar{a}$ and $a \not \in \{\textbf{connect}(\dval{ip},\dval{ip}'),\textbf{disconnect}(\dval{ip},\dval{ip}'),\newpkt{\dval{d}}{\dval{dip}}\}$.\\
More precisely, either $N \ar{\tick}$ or $N \ar{\colonact{\dval{ip}}{\deliver{\dval{d}}}}$ or $N \ar{\tau}$.
\qed
\end{corollary}

Our process algebra admits a translation into one without data
structures (although we cannot \emph{describe} the target algebra without
using data structures).  The idea is to replace any variable by all
possible values it can take. 
The target algebra differs from the
original only on the level of sequential processes; the subsequent
layers are unchanged.
A formal definition can be found in \App{eliminating}.
The resulting process algebra has a structural operational semantics in the (infinitary)
\emph{de Simone} format, generating the same transition system---up to strong
bisimilarity, $\bis$\,---as the original, which provides some results `for free'. 
For example, it follows that $\bis\,$, and many other
semantic equivalences, are congruences on our language.

\begin{theorem}
Strong bisimilarity is a congruence for all operators of \tawn.
\end{theorem}
This is a deep result that usually takes many pages to establish (e.g.,~\cite{SRS10}).
Here we get it directly from the existing theory on structural
operational semantics, as a result of carefully designing our
language within the disciplined framework described by de Simone~\cite{dS85}.

\begin{theorem}
$\parl$ is associative, and $\|$ is associative and commutative, up to $\bis\,$.
\end{theorem}

\prf
The operational rules for these operators fit a format presented in \cite{CMR08},
guaranteeing associativity up to~$\bis$. The details are similar to
the case for AWN, as elaborated in \cite{ESOP12,TR13}; the only extra complication is
the associativity of the operator $\parl$ on $\W$, as defined on
\hyperlink{parallel}{Page~\pageref*{parallel}}, which we checked automatically by means of the theorem prover Prover9~\cite{Prover9}.
Commutativity of $\|$ follows by symmetry of the rules.
\eprf

\begin{theorem}
Each AWN process $P$, seen as a \tawn process, can be simulated by the AWN process $P$.
Likewise, each AWN network $N$, seen as a \tawn network, can be simulated by the AWN network $N$.
\label{thm:network_simulation}
\end{theorem}
\noindent
Here a \emph{simulation} refers to a \emph{weak simulation} as
  defined in \cite{vG93}, but treating \textbf{(dis)connect}-actions
  as $\tau$, and with the extra requirement that the data states
  maintained by related expressions are identical---except of course
  for the variables $\now$, that are missing in AWN\@.
Details can be found in \App{simulation}.

Thanks to \Thm{network_simulation}, we can prove that all invariants on the data structure
of a process expressed in AWN are still preserved when the process is
interpreted as a \tawn expression.
As an application of this, an untimed version of AODV\@, formalised as an AWN process, has been
  proven loop free in \cite{TR13,GHPT16}; the same system, seen as a \tawn expression---and thus with
  specific execution times associated to uni-, group-, and broadcast actions---is still loop free when given
  the operational semantics of \tawn.

%%%%%%%%%%%%%%%%%%%%%
\section{Case Study: The AODV Routing Protocol}\label{sec:aodv}
%%%%%%%%%%%%%%%%%%%%%

Routing protocols are crucial to the dissemination of data packets between nodes in 
WMNs and MANETs.
Highly dynamic topologies are a key feature of WMNs and MANETs, due to
mobility of nodes and/or the variability of wireless links. This makes
the design and implementation of robust and efficient routing
protocols for these networks a challenging task.
In this section we present a formal specification of the Ad hoc On-Demand
Distance Vector (AODV) routing protocol.
AODV~\cite{rfc3561} is a widely-used routing protocol designed for
MANETs, and is one of the four protocols currently standardised by the
IETF MANET working group\footnote{\url{http://datatracker.ietf.org/wg/manet/charter/}}.
It also forms the basis of new WMN routing protocols, including
HWMP in the IEEE 802.11s wireless mesh network standard~\cite{IEEE80211s}.

Our formalisation is based on an untimed formalisation of AODV~\cite{TR13,GHPT16}, written in \awn, 
and models the exact details of the core
functionality of AODV as standardised in IETF RFC 3561~\cite{rfc3561}; e.g., route discovery, route maintenance and
error handling. We demonstrate how {\tawn} can be used to reason about
critical protocol properties. As major outcome we demonstrate that 
AODV is \emph{not} loop free, which is in contrast to common belief.
Loop freedom is a critical property for any routing protocol, 
but it is particularly relevant and challenging for WMNs and MANETs. 
We close the section by discussing a fix to the protocol and prove that 
the resulting protocol is indeed loop free.

\subsection{Brief Overview}

%%%%%%%%%%%%%%%%%%%%%%%
{%%%node names...
\newcommand{\gennode}[1]{\ensuremath{\MakeUppercase{#1}}\xspace}
\newcommand{\na}{\gennode{a}}
\newcommand{\nd}{\gennode{d}}
\newcommand{\ns}{\gennode{s}}
AODV is a reactive protocol, which means that routes are established only
on demand.  If a node~\ns wants to send a data packet to  a node \nd, but
currently does not know a route, it temporarily buffers the
packet and initiates a route discovery process
by broadcasting a route request (RREQ) message in the network. An intermediate
node \na that receives the RREQ message creates a routing table entry for a route
towards node~\ns referred to as a \emph{reverse route}, and re-broadcasts the RREQ. This is repeated until the RREQ reaches the destination node~\nd, or alternatively a node that knows a route to \nd. In both cases, the node replies by unicasting a corresponding route reply (RREP) message back to the source~\ns,
via a previously established reverse route. When forwarding RREP messages, nodes
create a \rte for node \nd, called the \emph{forward route}. When the RREP reaches
the originating node \ns, a route from \ns to \nd  is established and data packets
can start to flow. Both forward and reverse routes are maintained in a routing table at every node---details are given below.
In the event of link and route breaks, AODV uses route error (RERR) messages to
notify the affected nodes: if a link break is detected by a node, it first invalidates all routes stored in the node's own routing table that actually use the broken link. Then it sends a RERR message containing the unreachable destinations to all (direct) neighbours using this route. 

In AODV, a routing table consists of a list of entries---at most one for each destination---each containing the following information:
(i) the destination IP address;
(ii) the \emph{destination sequence number};
(iii) the sequence-number-status flag---tagging whether the recorded sequence number
can be trusted;
(iv) a flag tagging the route as being valid or invalid---this flag is set to invalid
when a link break is detected or the route's lifetime is reached;
(v) the hop count, a metric to indicate the distance to the destination;
(vi) the next hop, an IP address that
identifies the next (intermediate) node on the route to the destination;
(vii) a list of precursors, a set of IP addresses of those
  $1$-hop neighbours that use this particular route; and
(viii) the lifetime (expiration or deletion time) of the route.
The destination sequence number constitutes a measure approximating the
relative freshness of the information held---a higher number denotes newer information.  
The  routing table  is updated whenever a node receives an AODV control message (RREQ, RREP or RERR)
or detects a link break. 

During the lifetime of the network, each node not only maintains its routing table, it also stores
its {\em own} {\em sequence number}.  This number is used as a local ``timer'' and is incremented 
whenever a new route request is initiated. It is the source of the destination
sequence numbers in routing tables of other nodes.

\hspace{-5pt}Full details of the protocol are outlined in the request for comments (RFC)~\cite{rfc3561}.
}%end macros

\subsection{Route Request Handling Handled Formally}\label{sec:rreqformal}
Our formal model consists of seven processes: 
$\AODV$ reads a message from the message queue (modelled in process \QMSG, see below) and,
		depending on the type of the message, calls other processes.
         Each time a message has been handled
		the process has the choice between handling another message,
		initiating the transmission of queued data packets or generating
		a new route request.
$\NEWPKT$ and $ \PKT$ describe all actions
                performed by a node when a data packet is
                received.  The former process handles a newly injected
		packet. The latter describes all actions performed
		when a node receives data from another node via the protocol. 
$\RREQ$ models all events that might occur
                after a route request message has been received. 
Similarly, $\RREP$ describes the reaction
		of the protocol to an incoming route reply.
$\RERR$ models the part of AODV that handles error messages.
The last process $\QMSG$ queues incoming messages. Whenever a message is received,
	  it is first stored in a message queue. When the corresponding node is able to handle a message,
	  it pops the oldest message from the queue and handles it.
An AODV network is an encapsulated parallel composition of node expressions, each with a different
node address (identifier), and all initialised with the parallel composition 
$\AODV(\dots)\parl\QMSG(\dots)$.

In this paper, we have room to present parts of the $\RREQ$ process only, depicted in \Pro{rreq_shortened}%
\footnote{The numbering scheme is consistent with the one in~\cite{BGH16}.};
the full formal specification of the entire protocol can be found in  \App{spec}. There, we also discuss 
all differences between the untimed version of AODV, as formalised in~\cite{TR13,GHPT16}, and 
the newly developed timed version. 
These differences mostly consist of setting expiration times for routing table
  entries and other data maintained by AODV, and handling the expiration of this data.

{\newcommand{\dsnf}{sequence-number-status flag\xspace}

\renewcommand{\ip}{\dval{ip}}
\renewcommand{\dip}{\dval{dip}}
\renewcommand{\oip}{\dval{oip}}
\renewcommand{\sip}{\dval{sip}}
\renewcommand{\rip}{\dval{rip}}
\renewcommand{\rt}{\dval{rt}}
\renewcommand{\r}{\dval{r}}
\renewcommand{\osn}{\dval{osn}}
\renewcommand{\dsn}{\dval{dsn}}
\renewcommand{\rsn}{\dval{rsn}}
\renewcommand{\flag}{\dval{flag}}
\renewcommand{\hops}{\dval{hops}}
\renewcommand{\nhip}{\dval{nhip}}
\renewcommand{\pre}{\dval{pre}}
\renewcommand{\dests}{\dval{dests}}
\renewcommand{\rreqid}{\dval{rreqid}}
\renewcommand{\rreqs}{\dval{rreqs}}
A route discovery in AODV is initiated by a source node broadcasting a RREQ message; this message
is subsequently re-broadcast by other nodes.
Process~\ref{pro:rreq_shortened} shows major parts of our process algebra specification for handling a RREQ message received
by a node \ip.
The incoming message carries eight parameters, including
{\hops}, indicating how far the RREQ had travelled so far,
{\rreqid}, an identifier for this request,
{\dip}, the destination IP address,
and {\sip}, the sender of the incoming message;
the parameters {\ip}, \dval{sn} and {\rt}, storing the node's address, sequence number
and routing table, as well as {\rreqs} and \dval{store}, are maintained by the process RREQ itself.

\hspace{-2.3pt}Before handling the incoming message, the process first updates
{\rreqs} (Line~\ref{rreq_short:line1}), a list of (unique) pairs containing the originator IP address {\oip} and a route request identifier {\rreqid} received within 
 the last \pathdiscoverytime: 
 the 
 %%reduce space below Process 4
\pagebreak 
       \vspace*{-5ex}
 \noindent   
 \mbox{update} removes identifiers that are too old. 
 Based on this list, the node then checks whether it has recently received a RREQ with the same
   {\oip} and {\rreqid}.

If this is the case, the RREQ message is ignored, and the protocol continues to execute the main AODV process (Lines~\ref{rreq_short:line2}--\ref{rreq_short:line3}). 
If the
RREQ is new (Line~\ref{rreq_short:line4}), the process updates the routing table by adding a ``reverse route'' entry
to {\oip}, the originator of the RREQ, via node {\sip}, with distance \hops+1 (Line~\ref{rreq_short:line6}).
 If there
already is a route to {\oip} in the node's routing table {\rt}, it is only updated with the new
route if the new route is ``better'', i.e., fresher and/or shorter
and/or replacing an invalid route. 
The lifetime of this reverse route is updated as well (Line~\ref{rreq_short:line7}): it is set to the
maximum of the currently stored lifetime and the minimal lifetime, which is determined by 
$\now+2\cdot\traversal-2\cdot(\hops+1)\cdot\nodetraversal$ \cite[Page 17]{rfc3561}.
The process also adds the message to the list of known RREQs (Line~\ref{rreq_short:line8}).

Lines~\ref{rreq_short:line10}--22 (only shown in \App{spec}) deal with the case where the node receiving the RREQ is the
intended destination, i.e., {\dip}={\ip} (Line~\ref{rreq_short:line10}).
}% end redefined macros

\setcounter{algorithm}{3}
\listingTop[Parts of the RREQ handling]{rreq_shortened}
\setcounter{algorithm}{0}

{\renewcommand{\ip}{\dval{ip}}%
\renewcommand{\dip}{\dval{dip}}%
\renewcommand{\oip}{\dval{oip}}%
\renewcommand{\sip}{\dval{sip}}%
\renewcommand{\rip}{\dval{rip}}%
\renewcommand{\rt}{\dval{rt}}%
\renewcommand{\r}{\dval{r}}%
\renewcommand{\osn}{\dval{osn}}%
\renewcommand{\dsn}{\dval{dsn}}%
\renewcommand{\rsn}{\dval{rsn}}%
\renewcommand{\flag}{\dval{flag}}%
\renewcommand{\hops}{\dval{hops}}%
\renewcommand{\nhip}{\dval{nhip}}%
\renewcommand{\pre}{\dval{pre}}%
\renewcommand{\dests}{\dval{dests}}%
\renewcommand{\rreqid}{\dval{rreqid}}%
\renewcommand{\rreqs}{\dval{rreqs}}%


Lines~\ref{rreq_short:line20}--\ref{rreq_short:line36} deal with the case where the node receiving the RREQ is
not the destination, i.e., ${\dip}\mathop{\neq}{\ip}$ (Line~\ref{rreq_short:line20}).  
The node can respond to the RREQ with a
corresponding RREP on behalf of the destination node \dip, if its route to {\dip} is ``fresh enough''
(Line~\ref{rreq_short:line22}).  This means that (a) the node has a valid route to \dip, (b) the destination sequence
\pagebreak
number in the node's current \rte $(\sqn{\rt}{\dip})$ is greater than or equal to the
requested sequence number to {\dip} in the RREQ message, and (c) the node's destination sequence number is 
trustworthy ($\sqnf{\rt}{\!\dip}\mathbin=\kno$).  If these three conditions are met
(Line~\ref{rreq_short:line22}), the node generates a RREP message, and unicasts it back to the originator
node {\oip} via the reverse route. 
Before
unicasting the RREP message, the intermediate node updates the forward {\rte} to
$\dip$ by placing the last hop node ($\sip$)
into the precursor list for
that entry (Line~\ref{rreq_short:line24}).
Likewise, it updates the reverse {\rte} to {\oip} by placing the first hop $\nhop{\rt}{\dip}$
towards $\dip$ in the precursor list for that entry
(Line~\ref{rreq_short:line25}).
To generate the RREP message, the process copies the sequence number for the
destination $\dip$ from the routing table $\rt$ into the destination sequence number field of the RREP message and it places its distance in hops from the destination ($\dhops{\rt}{\dip}$) in the corresponding field of the new reply
(Line~\ref{rreq_short:line26}).
 The RREP message is unicast to the next hop along the reverse route back to the originator of the
corresponding RREQ message. If this unicast is successful, the process goes back to the AODV routine (Line~\ref{rreq_short:line26a}).
If the unicast of the RREP fails, we proceed with Lines~\ref{rreq_short:line26b}--\ref{rreq_short:line31}, in which a route error
(RERR) message is generated and sent. This conditional unicast is implemented in our model with the \otawn construct 
$\unicast{\dexp{dest}}{\dexp{ms}}.P \prio{Q}$.
In the latter case, the node sends a RERR message to all nodes that rely on the broken link for one of their routes.
For this, the process first determines which destination nodes are affected by the broken link, i.e., the nodes
that have this unreachable node listed as a next hop in the routing table (not shown in the shortened specification).
Then, it invalidates any affected \rtes, and determines the list of
\emph{precursors}, which are the
neighbouring nodes that have a
route to one of the affected destination nodes via the broken link.
Finally, a RERR message is sent via groupcast to all these precursors
(Line~\ref{rreq_short:line31}).

If the node is not the destination and there is either no route to the
destination $\dip$ inside the routing table or the route is not fresh enough,
the route request received has to be forwarded. This happens in Line~\ref{rreq_short:line34}.
The information inside the forwarded request is mostly copied from the request received.
Only the hop count is increased by $1$ and the destination sequence number is set
to the maximum of the destination sequence number in the RREQ packet
and the current sequence number for $\dip$ in the routing table.
In case $\dip$ is an unknown destination, $\sqn{\rt}{\dip}$ returns the
unknown sequence number $0$.
}% end redefined macros

To ensure that our time-free model from \cite{TR13,GHPT16} accurately captures the intended behaviour of AODV \cite{rfc3561}, 
we spent a long time reading and interpreting the RFC, inspecting open-source
implementations, and consulting network engineers.
We now prove that our timed version of AODV behaves similar to our original formal specification, 
and hence (still) captures the intended behaviour.
 
\begin{theorem}\label{thm:timedVSuntimed}
The timed version of AODV (as sketched in this paper, and presented in~\cite{BGH16}) is a proper extension of 
the untimed version (as presented in~\cite{TR13}). By this we mean that if 
all timing constants, such as \valtime\hspace{-1pt}, are set to $\infty$\hspace{-1pt},
and the maximal number of pending route request retries 
\retries\ is set to $1$, then the (\tawn) transition systems of both versions of AODV are 
weakly bisimilar.
\end{theorem}
\begin{proofsketch}
First, one shows that the newly introduced functions, such as \fnexprreqs\ and \fnsettimert\  do not change the data state in case the time parameters equal $\infty$; 
and hence lead to transitions of the form \plat{$\xi,p\ar{\tau}\xi,p'$}. This kind of transitions are the ones that make the bisimulation weak, since they do not occur 
in the formal specification of~\cite{TR13}.
Subsequently, one proves that all other transitions are basically identical.
\end{proofsketch}

\subsection{Loop Freedom}\label{ssec:lf}
Loop freedom is a critical property for any routing protocol, but it is particularly relevant and
challenging for WMNs and MANETs.
``{A routing-table loop is a path specified in the nodes' routing tables at a particular point in time that visits the same node more than once before reaching the intended destination}"~\cite{Garcia-Luna-Aceves89}.
Packets caught in a routing loop can quickly saturate the links and have a detrimental impact on network performance.

For AODV and many other protocols sequence numbers are used to guarantee loop freedom.
Such  protocols usually claim to be loop free due to the use of monotonically increasing sequence numbers.
For example, AODV ``{uses destination sequence numbers to ensure loop freedom at all
 times (even in the face of anomalous delivery of routing control messages), ...}"~\cite{rfc3561}. 
 It has been shown that sequence numbers do not a  priori guarantee loop freedom~\cite{AODVloop}; 
 for some plausible interpretations%
 \footnote{By a plausible interpretation of a protocol standard written in English prose we mean an interpretation that fills the missing bits, and 
 resolves ambiguities and contradictions occurring in the standard in a sensible and meaningful way.}
 of different versions of AODV, however, loop freedom has been
 proven~\cite{AODV99,BOG02,ZYZW09,SRS10,MSWIM12,TR13,GHPT16,NT15}%
\footnote{%
 The proofs in \cite{AODV99} and \cite{BOG02} are incorrect;
 the model of \cite{SRS10} does not capture the full behaviour of the routing protocol; 
 and \cite{ZYZW09} is based on a subset of AODV that
 does not cover the ``intermediate route reply'' feature,
 a source of loops.
In \cite{NT15} a draft of a new version of AODV is modelled, without intermediate route reply.
 For a more detailed discussion see~\cite{GHPT16}.}.
With the exception of~\cite{BOG02}, all these papers consider only untimed versions of AODV. 
As mentioned in \Sect{intro} untimed analyses revealed many shortcomings of AODV;
hence they are necessary. At the same time, a timed analysis is required as well.
\cite{BOG02} shows that the premature deletion of invalid routes, and a too quick restart of a node after a reboot,
can yield routing loops.
Since then, AODV has changed to such a degree that the examples of \cite{BOG02} do not apply any longer. 

In \cite{Garcia04}, ``it is shown that the use of a $\deltime$ in  the current AODV specification can result in loops''.
However, the loop constructed therein at any time passes through at least one invalid routing table entry.
As such, it is not a routing loop in the sense of \cite{TR13,GHPT16}---we only consider loops
consisting of valid routing table entries, since invalid ones do not forward data
packets. In a loop as in \cite{Garcia04} data packets cannot be sent in circles forever.

It turns out that AODV as standardised in the RFC (and carefully formalised  in \Sect{rreqformal} and \App{spec})
is \emph{not} loop free.
A potential cause of routing loops, sketched in \Fig{loop1}, is a situation where a
node $B$ has a {\val}id 
\begin{wrapfigure}[7]{l}{0.55\textwidth}
	\scriptsize
		\begin{tabular}{ll@{\qquad}ll}
			\multicolumn{2}{l}{\ \ \ \includegraphics{fig/loop1_1}}   &   
			\multicolumn{2}{c}{\includegraphics{fig/loop1_2}}\\	[5pt]
			%
			a)&$C$'s entry for $D$ has  &b)& $B$ sends old data;\\
                 &expired; $B$'s has not    &&     $C$ establishes loop\\[-2ex]
		\end{tabular}
		\caption{Premature Route Expiration\label{fig:loop1}}
\end{wrapfigure}%
routing table entry for a destination $D$ (in \Fig{loop1} denoted $D{:}\val{\raisebox{.8pt}{$\scriptstyle\rightarrow$}}C$),
but the next hop $C$ no longer has a routing table entry for $D$ ($D{:}-$), valid or invalid.
In such a case, $C$ might search for a new route to $D$ and create a new
routing table entry pointing to $B$ as next hop, or to a node $A$ upstream
from $B$. We refer to this scenario as a case of \emph{premature route expiration}.

A related scenario, which we  also call premature route expiration, is when a node $C$ sends a RREP message with destination~$D$
or a RREQ messages with originator $D$ to a node $B$, but looses its route to $D$ before that
message arrives. This scenario can easily give rise to the scenario above. 

Premature route expiration can be avoided by setting {\deltime} to $\infty$, 
which is essentially the case in the untimed version of AODV (cf.\ \Thm{timedVSuntimed}).
In that case, no routing table entry expires or is erased. 
Hence,
the situation where $C$ no longer has a routing table entry for $D$ is prevented.

In \cite{TR13} we studied 5184 possible interpretations of the AODV RFC \cite{rfc3561},
a proliferation due to ambiguities, contradictions and cases of
underspecification that could be resolved in multiple ways.
In 5006 of these readings of the standard, including some rather
plausible ones, we found routing loops, even when excluding all loops
that are due to timing issues \cite{AODVloop,TR13}. In \cite{MSWIM12,TR13,GHPT16}
we have chosen a default reading of the RFC that avoids these loops,
formalised it in AWN, and formally proved loop freedom, still
assuming (implicitly) $\deltime = \infty$.

After taking this hurdle, the present paper continues the investigation by 
allowing arbitrary values for time parameters and for \retries; 
hence dropping the simplifying assumption that $\deltime = \infty$.

One of our key results is that for the formalisation of AODV presented
here, premature route expiration is the \emph{only} potential source
of routing loops. Under the assumption that premature route expiration
does not occur, it turns out that, with minor modifications, the 
loop freedom proof of \cite{TR13,GHPT16} applies to our timed model of AODV
as well. A proof of this result is presented in \App{invariants}.
There, we revisit all the invariants from \cite{TR13} that contribute
to the loop-freedom proof, 
and determine which of them are still valid
in the timed setting, and how others need to be modified.

It is trivial to find an example where premature route expiration does
occur in AODV, and a routing loop ensues. This can happen when a
message spends an inordinate amount of time in the queue of incoming
messages of a node. However, this situation tends not to occur in
realistic scenarios. To capture this, we now make the assumption that 
the period a message spends in the queue of incoming messages of the
receiving node, is bounded by \nodetraversal. We also assume that the
period a route request travels through the network is bounded by \traversal.

These assumptions eliminate the ``trivial'' counterexample mentioned above.
As we show in \App{D}, we now \emph{almost} can prove an invariant that
essentially says that premature route expiration does not occur.
Following the methodology from \cite{MSWIM12,TR13,GHPT16}, we establish our
invariants by showing that they hold in all possible initial states of
AODV, and are preserved under the transitions of our operation
semantics, which correspond to the line numbers in our process algebraic specification.

We said ``almost'', because, as indicated in
\App{D}, our main invariant is not preserved by
five lines of our AODV specification.
Additionally, we need to make the assumption that when a RREQ message is forwarded, the forwarding node has
a valid routing table entry to the originator of the route request.
This does not hold for our formalisation of AODV: in \Pro{rreq_shortened} no check 
is performed on $\oip$, only the routing table to the destination node $\dip$ has to satisfy certain conditions
(Lines \ref{rreq_short:line20} and \ref{rreq_short:line32}).

It turns out that for each of these failures we can
construct an example of premature route expiration, and, by that, a
counterexample to loop freedom.

However, if we skip all five offending lines (or adapt them in
appropriate ways) and make a small change to process RREQ that makes
the above assumption valid,%
\footnote{The change basically introduces the test ``$\oip\in\akD{\rt}$'' in
  Line~\ref{rreq_short:line32} or~\ref{rreq_short:line9} of \Pro{rreq_shortened}.}
we obtain a proof of loop freedom for the resulting version of AODV\@. This follows immediately from
the invariants established in \App{D}.

\section{Conclusion }
In this paper we have proposed \tawn, a timed process algebra for wireless networks.
We are aware that there are many other timed process algebras, such as 
timed CCS~\cite{MT90}, 
timed CSP~\cite{RR86,OS06}, 
timed ACP~\cite{BB96},
ATP \cite{NS94} and TPL \cite{HR95},
However, none of these algebras provides the unique set of features needed 
for modelling and analysing protocols for wireless networks (e.g. a conditional unicast).%
\footnote{This is similar to the untimed situation. A detailed comparison between \awn and other process calculi for 
wireless networks is given in \cite[Section 11.1]{TR13}; this discussion can directly be transferred to the timed case.}
These features are provided by \otawn, though. 
Our treatment of time is based on design decisions that appear
  rather different from the ones in \cite{MT90,RR86,OS06,BB96,NS94}.
  Our approach appears to be closest to \cite{HR95}, but
  avoiding the negative premises that play a crucial role in the
  operational semantics of~\cite{HR95}.

We have illustrated the usefulness of \tawn by analysing 
the  Ad hoc On-Demand Distance
Vector routing protocol, and have shown that, contrary to claims in the
literature and to common belief, it fails to be loop free. We have also discussed
boundary conditions for a fix ensuring
that the resulting protocol is loop free.


% % % % % % % % % % % %
\paragraph*{Acknowledgement.}
NICTA is funded by the Australian Government through the Department of Communications and the Australian Research Council through the ICT Centre of Excellence Program. 

\newpage

\begin{thebibliography}{10}
\providecommand{\bibitemdeclare}[2]{}
\providecommand{\surnamestart}{}
\providecommand{\surnameend}{}
\providecommand{\urlprefix}{Available at }
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\href}[2]{\texttt{#2}}
\providecommand{\urlalt}[2]{\href{#1}{#2}}
\providecommand{\doi}[1]{doi:\urlalt{http://dx.doi.org/#1}{#1}}
\providecommand{\bibinfo}[2]{#2}

\bibitemdeclare{article}{BB96}
\bibitem{BB96}
\bibinfo{author}{J.~\surnamestart Baeten\surnameend} \&
  \bibinfo{author}{J.~\surnamestart Bergstra\surnameend}
  (\bibinfo{year}{1996}): \emph{\bibinfo{title}{Discrete Time Process
  Algebra}}.
\newblock {\sl \bibinfo{journal}{Formal Aspects of Computing}}
  \bibinfo{volume}{8}(\bibinfo{number}{2}), pp. \bibinfo{pages}{188--208},
  \doi{10.1007/BF01214556}.

\bibitemdeclare{incollection}{BK86}
\bibitem{BK86}
\bibinfo{author}{J.A. \surnamestart Bergstra\surnameend} \&
  \bibinfo{author}{J.W. \surnamestart Klop\surnameend} (\bibinfo{year}{1986}):
  \emph{\bibinfo{title}{Algebra of Communicating Processes}}.
\newblock In \bibinfo{editor}{J.W. \surnamestart {de Bakker}\surnameend},
  \bibinfo{editor}{M.~\surnamestart Hazewinkel\surnameend} \&
  \bibinfo{editor}{J.K. \surnamestart Lenstra\surnameend}, eds.: {\sl
  \bibinfo{booktitle}{Mathematics and Computer Science}}, \bibinfo{series}{CWI
  Monograph 1}, \bibinfo{publisher}{North-Holland}, pp.
  \bibinfo{pages}{89--138}.

\bibitemdeclare{article}{BOG02}
\bibitem{BOG02}
\bibinfo{author}{K.~\surnamestart Bhargavan\surnameend},
  \bibinfo{author}{D.~\surnamestart Obradovic\surnameend} \&
  \bibinfo{author}{C.A. \surnamestart Gunter\surnameend}
  (\bibinfo{year}{2002}): \emph{\bibinfo{title}{Formal Verification of
  Standards for Distance Vector Routing Protocols}}.
\newblock {\sl \bibinfo{journal}{Journal of the ACM}}
  \bibinfo{volume}{49}(\bibinfo{number}{4}), pp. \bibinfo{pages}{538--576},
  \doi{10.1145/581771.581775}.

\bibitemdeclare{article}{BB87}
\bibitem{BB87}
\bibinfo{author}{T.~\surnamestart Bolognesi\surnameend} \&
  \bibinfo{author}{E.~\surnamestart Brinksma\surnameend}
  (\bibinfo{year}{1987}): \emph{\bibinfo{title}{Introduction to the {ISO}
  Specification Language {LOTOS}}}.
\newblock {\sl \bibinfo{journal}{Computer Networks}} \bibinfo{volume}{14}, pp.
  \bibinfo{pages}{25--59}, \doi{10.1016/0169-7552(87)90085-7}.

\bibitemdeclare{techreport}{BGH16}
\bibitem{BGH16}
\bibinfo{author}{E.~\surnamestart Bres\surnameend}, \bibinfo{author}{R.J.
  \surnamestart van Glabbeek\surnameend} \& \bibinfo{author}{P.~\surnamestart
  H{\"o}fner\surnameend} (\bibinfo{year}{2016}): \emph{\bibinfo{title}{A Timed Process Algebra for Wireless Networks with an Application in Routing}}.
\newblock \bibinfo{type}{Technical Report} \bibinfo{number}{9145},
  \bibinfo{institution}{NICTA}.
\newblock \urlprefix\url{http://nicta.com.au/pub?id=9145}.

\bibitemdeclare{inproceedings}{CK05}
\bibitem{CK05}
\bibinfo{author}{S.~\surnamestart Chiyangwa\surnameend} \&
  \bibinfo{author}{M.~\surnamestart Kwiatkowska\surnameend}
  (\bibinfo{year}{2005}): \emph{\bibinfo{title}{A Timing Analysis of {AODV}}}.
\newblock In: {\sl \bibinfo{booktitle}{Formal Methods for Open Object-based
  Distributed Systems {(FMOODS'05)}}}, {\sl \bibinfo{series}{LNCS}}
  \bibinfo{volume}{3535}, \bibinfo{publisher}{Springer}, pp.
  \bibinfo{pages}{306--322}, \doi{10.1007/11494881\_20}.

\bibitemdeclare{misc}{rfc3626}
\bibitem{rfc3626}
\bibinfo{author}{T.~\surnamestart Clausen\surnameend} \&
  \bibinfo{author}{P.~\surnamestart Jacquet\surnameend} (\bibinfo{year}{2003}):
  \emph{\bibinfo{title}{Optimized Link State Routing Protocol {(OLSR)}}}.
\newblock \bibinfo{howpublished}{RFC 3626 (Experimental), Network Working
  Group}.
\newblock \urlprefix\url{http://www.ietf.org/rfc/rfc3626.txt}.

\bibitemdeclare{inproceedings}{CMR08}
\bibitem{CMR08}
\bibinfo{author}{S.~\surnamestart Cranen\surnameend}, \bibinfo{author}{M.R.
  \surnamestart Mousavi\surnameend} \& \bibinfo{author}{M.A. \surnamestart
  Reniers\surnameend} (\bibinfo{year}{2008}): \emph{\bibinfo{title}{A Rule
  Format for Associativity}}.
\newblock In \bibinfo{editor}{F.~\surnamestart van Breugel\surnameend} \&
  \bibinfo{editor}{M.~\surnamestart Chechik\surnameend}, eds.: {\sl
  \bibinfo{booktitle}{Concurrency Theory {(CONCUR '08)}}}, {\sl
  \bibinfo{series}{LNCS}} \bibinfo{volume}{5201},
  \bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{447--461},
  \doi{10.1007/978-3-540-85361-9\_35}.

\bibitemdeclare{inproceedings}{EHWripe12}
\bibitem{EHWripe12}
\bibinfo{author}{S.~\surnamestart Edenhofer\surnameend} \&
  \bibinfo{author}{P.~\surnamestart H{\"o}fner\surnameend}
  (\bibinfo{year}{2012}): \emph{\bibinfo{title}{Towards a Rigorous Analysis of
  {AODVv2} {(DYMO)}}}.
\newblock In: {\sl \bibinfo{booktitle}{Rigorous Protocol Engineering {(WRiPE
  '12)}}}, \bibinfo{publisher}{IEEE}, \doi{10.1109/ICNP.2012.6459942}.

\bibitemdeclare{inproceedings}{ESOP12}
\bibitem{ESOP12}
\bibinfo{author}{A.~\surnamestart Fehnker\surnameend}, \bibinfo{author}{R.J.
  \surnamestart van Glabbeek\surnameend}, \bibinfo{author}{P.~\surnamestart
  H{\"o}fner\surnameend}, \bibinfo{author}{A.K. \surnamestart
  McIver\surnameend}, \bibinfo{author}{M.~\surnamestart Portmann\surnameend} \&
  \bibinfo{author}{W.L. \surnamestart Tan\surnameend} (\bibinfo{year}{2012}):
  \emph{\bibinfo{title}{A Process Algebra for Wireless Mesh Networks}}.
\newblock In \bibinfo{editor}{H.~\surnamestart Seidl\surnameend}, ed.: {\sl
  \bibinfo{booktitle}{ESOP'12}}, {\sl \bibinfo{series}{LNCS}}
  \bibinfo{volume}{7211}, \bibinfo{publisher}{Springer}, pp.
  \bibinfo{pages}{295--315}, \doi{10.1007/978-3-642-28869-2\_15}.

\bibitemdeclare{techreport}{TR13}
\bibitem{TR13}
\bibinfo{author}{A.~\surnamestart Fehnker\surnameend}, \bibinfo{author}{R.J.
  \surnamestart van Glabbeek\surnameend}, \bibinfo{author}{P.~\surnamestart
  H{\"o}fner\surnameend}, \bibinfo{author}{A.K. \surnamestart
  McIver\surnameend}, \bibinfo{author}{M.~\surnamestart Portmann\surnameend} \&
  \bibinfo{author}{W.L. \surnamestart Tan\surnameend} (\bibinfo{year}{2013}):
  \emph{\bibinfo{title}{A Process Algebra for Wireless Mesh Networks used for
  Modelling, Verifying and Analysing {AODV}}}.
\newblock \bibinfo{type}{Technical Report} \bibinfo{number}{5513},
  \bibinfo{institution}{NICTA}.
\newblock \urlprefix\url{http://arxiv.org/abs/1312.7645}.

\bibitemdeclare{inproceedings}{Garcia-Luna-Aceves89}
\bibitem{Garcia-Luna-Aceves89}
\bibinfo{author}{J.J. \surnamestart Garcia-Luna-Aceves\surnameend}
  (\bibinfo{year}{1989}): \emph{\bibinfo{title}{A Unified Approach to Loop-free
  Routing using Distance Vectors or Link States}}.
\newblock In: {\sl \bibinfo{booktitle}{SIGCOMM'89}}, {\sl
  \bibinfo{series}{SIGCOMM Computer Communication Review}}
  \bibinfo{volume}{19(4)}, \bibinfo{publisher}{ACM Press}, pp.
  \bibinfo{pages}{212--223}, \doi{10.1145/75246.75268}.

\bibitemdeclare{inproceedings}{Garcia04}
\bibitem{Garcia04}
\bibinfo{author}{J.J. \surnamestart Garcia-Luna-Aceves\surnameend} \&
  \bibinfo{author}{H.~\surnamestart Rangarajan\surnameend}
  (\bibinfo{year}{2004}): \emph{\bibinfo{title}{A New Framework for Loop-free
  On-demand Routing using Destination Sequence Numbers}}.
\newblock In: {\sl \bibinfo{booktitle}{MASS'04}}, \bibinfo{publisher}{IEEE},
  pp. \bibinfo{pages}{426--435}, \doi{10.1109/MAHSS.2004.1392182}.

\bibitemdeclare{inproceedings}{vG93}
\bibitem{vG93}
\bibinfo{author}{R.J. \surnamestart van Glabbeek\surnameend}
  (\bibinfo{year}{1993}): \emph{\bibinfo{title}{The Linear Time -- Branching
  Time Spectrum {II}; The semantics of sequential systems with silent moves}}.
\newblock In \bibinfo{editor}{E.~\surnamestart Best\surnameend}, ed.: {\sl
  \bibinfo{booktitle}{CONCUR'93}}, {\sl \bibinfo{series}{LNCS}}
  \bibinfo{volume}{715}, \bibinfo{publisher}{Springer}, pp.
  \bibinfo{pages}{66--81}, \doi{10.1007/3-540-57208-2\_6}.

\bibitemdeclare{article}{GHPT16}
\bibitem{GHPT16}
\bibinfo{author}{R.J. \surnamestart van Glabbeek\surnameend},
  \bibinfo{author}{P.~\surnamestart H{\"o}fner\surnameend},
  \bibinfo{author}{M.~\surnamestart Portmann\surnameend} \&
  \bibinfo{author}{W.L. \surnamestart Tan\surnameend} (\bibinfo{year}{2016}):
  \emph{\bibinfo{title}{Modelling and Verifying the AODV Routing Protocol}}.
\newblock {\sl \bibinfo{journal}{Distributed Computing}}.
\newblock \bibinfo{note}{To appear}.

\bibitemdeclare{inproceedings}{AODVloop}
\bibitem{AODVloop}
\bibinfo{author}{R.J. \surnamestart van Glabbeek\surnameend},
  \bibinfo{author}{P.~\surnamestart H{\"o}fner\surnameend},
  \bibinfo{author}{W.L. \surnamestart Tan\surnameend} \&
  \bibinfo{author}{M.~\surnamestart Portmann\surnameend}
  (\bibinfo{year}{2013}): \emph{\bibinfo{title}{Sequence Numbers Do Not
  Guarantee Loop Freedom ---AODV Can Yield Routing Loops---}}.
\newblock In: {\sl \bibinfo{booktitle}{MSWiM '13}}, \bibinfo{publisher}{ACM
  Press}, pp. \bibinfo{pages}{91--100}, \doi{10.1145/2507924.2507943}.

\bibitemdeclare{article}{HR95}
\bibitem{HR95}
\bibinfo{author}{M.~\surnamestart Hennessy\surnameend} \&
  \bibinfo{author}{T.~\surnamestart Regan\surnameend} (\bibinfo{year}{1995}):
  \emph{\bibinfo{title}{A Process Algebra for Timed Systems}}.
\newblock {\sl \bibinfo{journal}{Information and Computation}}
  \bibinfo{volume}{117}(\bibinfo{number}{2}), pp. \bibinfo{pages}{221--239},
  \doi{10.1006/inco.1995.1041}.

\bibitemdeclare{book}{Ho85}
\bibitem{Ho85}
\bibinfo{author}{C.A.R. \surnamestart Hoare\surnameend} (\bibinfo{year}{1985}):
  \emph{\bibinfo{title}{Communicating Sequential Processes}}.
\newblock \bibinfo{publisher}{Prentice Hall}, \bibinfo{address}{Englewood
  Cliffs}.

\bibitemdeclare{inproceedings}{MSWIM12}
\bibitem{MSWIM12}
\bibinfo{author}{P.~\surnamestart H{\"o}fner\surnameend}, \bibinfo{author}{R.J.
  \surnamestart van Glabbeek\surnameend}, \bibinfo{author}{W.L. \surnamestart
  Tan\surnameend}, \bibinfo{author}{M.~\surnamestart Portmann\surnameend},
  \bibinfo{author}{A.K. \surnamestart McIver\surnameend} \&
  \bibinfo{author}{A.~\surnamestart Fehnker\surnameend} (\bibinfo{year}{2012}):
  \emph{\bibinfo{title}{A Rigorous Analysis of AODV and its Variants}}.
\newblock In: {\sl \bibinfo{booktitle}{MSWiM'12}}, \bibinfo{publisher}{ACM
  Press}, pp. \bibinfo{pages}{203--212}, \doi{10.1145/2387238.2387274}.

\bibitemdeclare{misc}{IEEE80211s}
\bibitem{IEEE80211s}
\bibinfo{author}{\surnamestart IEEE\surnameend} (\bibinfo{year}{2011}):
  \emph{\bibinfo{title}{IEEE Standard for Information
  Technology---Telecommunications and information exchange between
  systems---Local and metropolitan area networks ---Specific requirements Part
  11: Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY)
  specifications Amendment 10: Mesh Networking}},
  \doi{10.1109/IEEESTD.2011.6018236}.

\bibitemdeclare{article}{LT89}
\bibitem{LT89}
\bibinfo{author}{N.~\surnamestart Lynch\surnameend} \&
  \bibinfo{author}{M.~\surnamestart Tuttle\surnameend} (\bibinfo{year}{1989}):
  \emph{\bibinfo{title}{An Introduction to Input/Output Automata}}.
\newblock {\sl \bibinfo{journal}{CWI-Quarterly}}
  \bibinfo{volume}{2}(\bibinfo{number}{3}), pp. \bibinfo{pages}{219--246}.
\newblock \bibinfo{note}{{C}entrum voor Wiskunde en Informatica, Amsterdam}.

\bibitemdeclare{misc}{Prover9}
\bibitem{Prover9}
\bibinfo{author}{W.W. \surnamestart McCune\surnameend}:
  \emph{\bibinfo{title}{{P}rover9 and {M}ace4}}.
\newblock \bibinfo{howpublished}{\url{http://www.cs.unm.edu/~mccune/prover9}}.
\newblock \bibinfo{note}{(accessed 10 October 2015)}.

\bibitemdeclare{book}{Mi89}
\bibitem{Mi89}
\bibinfo{author}{R.~\surnamestart Milner\surnameend} (\bibinfo{year}{1989}):
  \emph{\bibinfo{title}{Communication and Concurrency}}.
\newblock \bibinfo{publisher}{Prentice Hall}.

\bibitemdeclare{inproceedings}{MT90}
\bibitem{MT90}
\bibinfo{author}{F.~\surnamestart Moller\surnameend} \&
  \bibinfo{author}{C.~\surnamestart Tofts\surnameend} (\bibinfo{year}{1990}):
  \emph{\bibinfo{title}{A Temporal Calculus of Communicating Systems}}.
\newblock In: {\sl \bibinfo{booktitle}{CONCUR '90}}, {\sl
  \bibinfo{series}{LNCS}} \bibinfo{volume}{458}, \bibinfo{publisher}{Springer},
  pp. \bibinfo{pages}{401--415}, \doi{10.1007/BFb0039073}.

\bibitemdeclare{inproceedings}{NT15}
\bibitem{NT15}
\bibinfo{author}{K.S. \surnamestart Namjoshi\surnameend} \&
  \bibinfo{author}{R.J. \surnamestart Trefler\surnameend}
  (\bibinfo{year}{2015}): \emph{\bibinfo{title}{Loop Freedom in {AODVv2}}}.
\newblock In \bibinfo{editor}{S.~\surnamestart Graf\surnameend} \&
  \bibinfo{editor}{M.~\surnamestart Viswanathan\surnameend}, eds.: {\sl
  \bibinfo{booktitle}{Formal Techniques for Distributed Objects, Components,
  and Systems (FORTE '15)}}, {\sl \bibinfo{series}{LNCS}}
  \bibinfo{volume}{9039}, \bibinfo{publisher}{Springer}, pp.
  \bibinfo{pages}{98--112}, \doi{10.1007/978-3-319-19195-9\_7}.

\bibitemdeclare{misc}{batman}
\bibitem{batman}
\bibinfo{author}{A.~\surnamestart Neumann\surnameend},
  \bibinfo{author}{M.~\surnamestart Aichele\surnameend, C.~Lindner} \&
  \bibinfo{author}{S.~\surnamestart Wunderlich\surnameend}
  (\bibinfo{year}{2008}): \emph{\bibinfo{title}{Better Approach To Mobile
  Ad-hoc Networking {(B.A.T.M.A.N.)}}}.
\newblock \bibinfo{howpublished}{Internet-Draft (Experimental), Network Working
  Group}.
\newblock
  \urlprefix\url{http://tools.ietf.org/html/draft-openmesh-b-a-t-m-a-n-00}.

\bibitemdeclare{article}{NS94}
\bibitem{NS94}
\bibinfo{author}{X.~\surnamestart Nicollin\surnameend} \&
  \bibinfo{author}{J.~\surnamestart Sifakis\surnameend} (\bibinfo{year}{1994}):
  \emph{\bibinfo{title}{The Algebra of Timed Processes, {ATP:} Theory and
  Application}}.
\newblock {\sl \bibinfo{journal}{Information and Computation}}
  \bibinfo{volume}{114}(\bibinfo{number}{1}), pp. \bibinfo{pages}{131--178},
  \doi{10.1006/inco.1994.1083}.

\bibitemdeclare{article}{OS06}
\bibitem{OS06}
\bibinfo{author}{J.~\surnamestart Ouaknine\surnameend} \&
  \bibinfo{author}{S.~\surnamestart Schneider\surnameend}
  (\bibinfo{year}{2006}): \emph{\bibinfo{title}{Timed {CSP:} {A}
  Retrospective}}.
\newblock {\sl \bibinfo{journal}{Electronic Notes in Theoretical Computer
  Science}} \bibinfo{volume}{162}, pp. \bibinfo{pages}{273--276},
  \doi{10.1016/j.entcs.2005.12.093}.

\bibitemdeclare{misc}{rfc3561}
\bibitem{rfc3561}
\bibinfo{author}{C.E. \surnamestart Perkins\surnameend}, \bibinfo{author}{E.M.
  \surnamestart Belding-Royer\surnameend} \& \bibinfo{author}{S.~\surnamestart
  Das\surnameend} (\bibinfo{year}{2003}): \emph{\bibinfo{title}{Ad hoc
  On-Demand Distance Vector {(AODV)} Routing}}.
\newblock \bibinfo{howpublished}{RFC 3561 (Experimental), Network Working
  Group}.
\newblock \urlprefix\url{http://www.ietf.org/rfc/rfc3561.txt}.

\bibitemdeclare{inproceedings}{AODV99}
\bibitem{AODV99}
\bibinfo{author}{C.E. \surnamestart Perkins\surnameend} \&
  \bibinfo{author}{E.M. \surnamestart Royer\surnameend} (\bibinfo{year}{1999}):
  \emph{\bibinfo{title}{{Ad-hoc On-Demand Distance Vector Routing}}}.
\newblock In: {\sl \bibinfo{booktitle}{Mobile Computing Systems and
  Applications {(WMCSA '99)}}}, \bibinfo{publisher}{IEEE}, pp.
  \bibinfo{pages}{90--100}, \doi{10.1109/MCSA.1999.749281}.

\bibitemdeclare{article}{Pl04}
\bibitem{Pl04}
\bibinfo{author}{G.D. \surnamestart Plotkin\surnameend} (\bibinfo{year}{2004}):
  \emph{\bibinfo{title}{A Structural Approach to Operational Semantics}}.
\newblock {\sl \bibinfo{journal}{Journal of Logic and Algebraic Programming}}
  \bibinfo{volume}{60--61}, pp. \bibinfo{pages}{17--139},
  \doi{10.1016/j.jlap.2004.05.001}.
\newblock \bibinfo{note}{Originally appeared in 1981}.

\bibitemdeclare{inproceedings}{RR86}
\bibitem{RR86}
\bibinfo{author}{G.~\surnamestart Reed\surnameend} \&
  \bibinfo{author}{A.~\surnamestart Roscoe\surnameend} (\bibinfo{year}{1986}):
  \emph{\bibinfo{title}{A Timed Model for Communicating Sequential Processes}}.
\newblock In \bibinfo{editor}{L.~\surnamestart Kott\surnameend}, ed.: {\sl
  \bibinfo{booktitle}{Automata, Languages and Programming (ICALP '86)}}, {\sl
  \bibinfo{series}{LNCS}} \bibinfo{volume}{226}, \bibinfo{publisher}{Springer},
  pp. \bibinfo{pages}{314--323}, \doi{10.1007/3-540-16761-7\_81}.

\bibitemdeclare{article}{dS85}
\bibitem{dS85}
\bibinfo{author}{R.~\surnamestart de~Simone\surnameend} (\bibinfo{year}{1985}):
  \emph{\bibinfo{title}{Higher-Level Synchronising Devices in {{\sc
  Meije}-SCCS}}}.
\newblock {\sl \bibinfo{journal}{Theoretical Computer Science}}
  \bibinfo{volume}{37}, pp. \bibinfo{pages}{245--267},
  \doi{10.1016/0304-3975(85)90093-3}.

\bibitemdeclare{article}{SRS10}
\bibitem{SRS10}
\bibinfo{author}{A.~\surnamestart Singh\surnameend}, \bibinfo{author}{C.R.
  \surnamestart Ramakrishnan\surnameend} \& \bibinfo{author}{S.A. \surnamestart
  Smolka\surnameend} (\bibinfo{year}{2010}): \emph{\bibinfo{title}{A process
  calculus for Mobile Ad Hoc Networks}}.
\newblock {\sl \bibinfo{journal}{Science of Computer Programming}}
  \bibinfo{volume}{75}, pp. \bibinfo{pages}{440--469},
  \doi{10.1016/j.scico.2009.07.008}.

\bibitemdeclare{inproceedings}{ZYZW09}
\bibitem{ZYZW09}
\bibinfo{author}{M.~\surnamestart Zhou\surnameend},
  \bibinfo{author}{H.~\surnamestart Yang\surnameend},
  \bibinfo{author}{X.~\surnamestart Zhang\surnameend} \&
  \bibinfo{author}{J.~\surnamestart Wang\surnameend} (\bibinfo{year}{2009}):
  \emph{\bibinfo{title}{The Proof of {AODV} Loop Freedom}}.
\newblock In: {\sl \bibinfo{booktitle}{Wireless Communications \& Signal
  Processing (WCSP '09)}}, \bibinfo{publisher}{IEEE},
  \doi{10.1109/WCSP.2009.5371479}.

\end{thebibliography}


\end{document}
