# Modelling MAC-Layer Communications in Wireless Systems

Andrea Cerone, Matthew Hennessy, Massimo Merro

► To cite this version:

Andrea Cerone, Matthew Hennessy, Massimo Merro. Modelling MAC-Layer Communications in Wireless Systems. 15th International Conference on Coordination Models and Languages (COORDINATION), Jun 2013, Florence, Italy. pp.16-30, 10.1007/978-3-642-38493-6_2. hal-01486032

HAL Id: hal-01486032

https://inria.hal.science/hal-01486032

Submitted on 9 Mar 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Modelling MAC-layer communications in wireless systems (Extended abstract)

Andrea Cerone<fnref n="1" />, Matthew Hennessy<fnref n="1" />*, and Massimo Merro<fnref n="2" />**

**Abstract** We present a timed broadcast process calculus for wireless networks at the MAC-sublayer where time-dependent communications are exposed to collisions. We define a reduction semantics for our calculus which leads to a contextual equivalence for comparing the external behaviour of wireless networks. Further, we construct an extensional LTS (labelled transition system) which models the activities of stations that can be directly observed by the external environment. Standard bisimulations in this novel LTS provide a sound proof method for proving that two systems are contextually equivalent. In addition, the main contribution of the paper is that our proof technique is also complete for a large class of systems.

## 1 Introduction

Wireless networks are becoming increasingly pervasive with applications across many domains, [19,1]. They are also becoming increasingly complex, with their behaviour depending on ever more sophisticated protocols. There are different levels of abstraction at which these can be defined and implemented, from the very basic level in which the communication primitives consist of sending and receiving electromagnetic signals, to the higher level where the basic primitives allow the set up of connections and exchange of data between two nodes in a wireless system [23].

Assuring the correctness of the behaviour of a wireless network has always been difficult. Several approaches have been proposed to address this issue for networks described at a high level [16,13,6,5,22,11,2,3]; these typically allow the formal description of protocols at the *network layer* of the *TCP/IP* reference model [23]. However there are few frameworks in the literature which consider networks described at the MAC-Sublayer of the *TCP/IP* reference model [12,14]. This is the topic of the current paper. We propose a process calculus for describing and verifying wireless networks at the *MAC-Sublayer* of the *TCP/IP* reference model.

This calculus, called the Calculus of Collision-prone Communicating Processes (CCCP), has been largely inspired by TCWS [14]; in particular CCCP inherits its communication features but simplifies considerably the syntax, the reduction semantics, the

<footnote n="1">¹ Department of Computer Science and Statistics, Trinity College Dublin, Ireland
{acerone, Matthew.Hennessy}@scss.tcd.ie</footnote>

<footnote n="2">² Dipartimento di Informatica,
Università degli Studi di Verona, Italy
massimo.merro@univr.it</footnote>

<footnote>* Supported by SFI project SFI 06 IN.1 1898.</footnote>

<footnote>** Author partially supported by the PRIN 2010-2011 national project "Security Horizons"</footnote>
notion of observation, and as we will see the behavioural theory. In CCCP a wireless
system is considered to be a collection of wireless stations which transmit and receive
messages. The transmission of messages is broadcast, and it is time-consuming; the
transmission of a message v can require several time slots (or instants). In addition,
wireless stations in our calculus are sensitive to collisions; if two different stations are
transmitting a value over a channel c at the same time slot a collision occurs, and the
content of the messages originally being transmitted is lost.

More specifically, in CCCP a state of a wireless network (or simply network, or
system) will be described by a *configuration* of the form Γ ▷ W where W describes the
code running at individual wireless stations and Γ represents the communication state
of channels. At any given point of time there will be *exposed* communication channels,
that is channels containing messages (or values) in transmission; this information will
be recorded in Γ.

Such systems evolve by the broadcast of messages between stations, the passage
of time, or some other internal activity, such as the occurrence of collisions and their
consequences. One of the topics of the paper is to capture formally these complex evol-
utions, by defining a *reduction semantics*, whose judgments take the form Γ₁▷W₁ ↣
Γ₂▷W₂. The reduction semantics satisfies some desirable properties such as *time de-
terminism*, *patience* and *maximal progress* [17,9,25].

However the main aim of the paper is to develop a behavioural theory of wireless
networks. To this end we need a formal notion of when two such systems are indis-
tinguishable from the point of view of users. Having a reduction semantics it is now
straightforward to adapt a standard notion of *contextual equivalence*: Γ₁▷W₁ ≈ Γ₂▷W₂.
Intuitively this means that either system, Γ₁▷W₁ or Γ₂▷W₂, can be replaced by the
other in a larger system without changing the observable behaviour of the overall sys-
tem. Formally we use the approach of [10], often called *reduction barbed congruence*;
the only parameter in the definition is the choice of primitive observation or *barb*. Our
choice is natural for wireless systems: the ability to transmit on an idle channel, that is
a channel with no active transmissions.

As explained in papers such as [20,7], contextual equivalences are determined by
so-called *extensional actions*, that is the set of minimal observable interactions which a
system can have with its external environment. For CCCP determining these actions is
non-trivial. Although values can be transmitted and received on channels, the presence
of collisions means that these are not necessarily observable. In fact the important point
is not the transmission of a value, but its successful delivery. Also, although the basic
notion of observation on systems does not involve the recording of the passage of time,
this has to be taken into account extensionally in order to gain a proper extensional
account of systems.

The extensional semantics determines an LTS (labelled transition system) over con-
figurations, which in turn gives rise to the standard notion of (weak) bisimulation equi-
valence between configurations. This gives a powerful co-inductive proof technique: to
show that two systems are behaviourally equivalent it is sufficient to exhibit a witness
bisimulation which contains them.

One result of this paper is that weak bisimulation in the extensional LTS is sound
with respect to the touchstone contextual equivalence: if two systems are related by
some bisimulation in the extensional LTS then they are contextually equivalent. However, the main contribution is that completeness holds for a large class of networks, called *well-formed*. If two such networks are contextually equivalent then there is some bisimulation, based on our novel extensional actions, which contains them. In [14], a sound but not complete bisimulation based proof method is developed for (a different form of) reduction barbed congruence. Here, by simplifying the calculus and isolating novel extensional actions we obtain both soundness and completeness.

The rest of the paper is organised as follows: in Section 2 we define the syntax which we will use for modelling wireless networks. The reduction semantics is given in Section 3 from which we develop in the same section our notion of reduction barbed congruence. In Section 4 we define the extensional semantics of networks, and the (weak) bisimulation equivalence it induces. In Section 5 we state the main results of the paper, namely that bisimulation is sound with respect to barbed congruence and, for a large class of systems, it is also complete. Detailed proofs of the results can be found in the associated technical report [4]. The latter also contains an initial case study showing the usefulness of our proof technique. Two particular instances of networks are compared; the first forwards two messages to the external environment using a TDMA modulation technique, the second performs the same task by routing the messages along different stations.

## 2 The calculus

Formally we assume a set of channels **Ch**, ranged over by *c*, *d*, ..., and a set of values **Val**, which contains a set of data-variables, ranged over by *x*, *y*, ... and a special value *err*; this value will be used to denote faulty transmissions. The set of *closed values*, that is those not containing occurrences of variables, are ranged over by *v*, *w*, .... We also assume that every closed value *v* ∈ **Val** has an associated strictly positive integer *δ*<sub>*v*</sub>, which denotes the number of time slots needed by a wireless station to transmit *v*.

A channel environment is a mapping $\Gamma : \mathbf{Ch} \to \mathbb{N} \times \mathbf{Val}$. In a configuration $\Gamma \succ W$ where $\Gamma(c) = (n, v)$ for some channel $c$, a wireless station is currently transmitting the value $v$ for the next $n$ time slots. We will use some suggestive notation for channel environments: $\Gamma \vdash_t c : n$ in place of $\Gamma(c) = (n, w)$ for some $w$, $\Gamma \vdash_v c : w$ in place of $\Gamma(c) = (n, w)$ for some $n$. If $\Gamma \vdash_t c : 0$ we say that channel $c$ is idle in $\Gamma$, and we denote it with $\Gamma \vdash c : \mathbf{idle}$. Otherwise we say that $c$ is exposed in $\Gamma$, denoted by $\Gamma \vdash c : \mathbf{exp}$. The channel environment $\Gamma$ such that $\Gamma \vdash c : \mathbf{idle}$ for every channel $c$ is said to be *stable*.

The syntax for system terms *W* is given in Table 1, where *P* ranges over code for programming individual stations, which is also explained in Table 1. A system term *W* is a collection of individual threads running in parallel, with possibly some channels restricted. Each thread may be either an inactive piece of code *P* or an active code of the form $c[x].P$. This latter term represents a wireless station which is receiving a value from the channel *c*; when the value is eventually received the variable *x* will be replaced with the received value in the code *P*. The restriction operator $\mathrm{vc} : (n, v).W$ is non-standard, for a restricted channel has a positive integer and a closed value associated with it; roughly speaking, the term $\mathrm{vc} : (n, v).W$ corresponds to the term *W* where
<table><caption>**Table 1** CCCP: Syntax</caption><tr><td>W ::= P</td><td>station code</td></tr><tr><td>c[x].P</td><td>active receiver</td></tr><tr><td>W<sub>1</sub> | W<sub>2</sub></td><td>parallel composition</td></tr><tr><td>vc:(n, v).W</td><td>channel restriction</td></tr><tr><td>P, Q ::= c!&lt;u&rang;.P</td><td>broadcast</td></tr><tr><td>[c?(x).P]Q</td><td>receiver with timeout</td></tr><tr><td>&sigma;.P</td><td>delay</td></tr><tr><td>&tau;.P</td><td>internal activity</td></tr><tr><td>P + Q</td><td>choice</td></tr><tr><td>[b]P, Q</td><td>matching</td></tr><tr><td>X</td><td>process variable</td></tr><tr><td>nil</td><td>termination</td></tr><tr><td>fix X.P</td><td>recursion</td></tr></table>

Channel Environment: $\Gamma: \mathbf{Ch} \to \mathbb{N} \times \mathbf{Val}$

channel *c* is local to *W*, and the transmission of value *v* over channel *c* will take place for the next *n* slots of time.

The syntax for station code is based on standard process calculus constructs. The main constructs are time-dependent reception from a channel $[c?(x).P]Q$, explicit time delay $\sigma.P$, and broadcast along a channel $c!&lt;u&rang;.P$. Here *u* denotes either a data-variable or closed value $v \in \mathbf{Val}$. Of the remaining standard constructs the most notable is matching, $[b]P, Q$ which branches to *P* or *Q*, depending on the value of the Boolean expression *b*. We leave the language of Boolean expressions unspecified, other than saying that it should contain equality tests for values, $u_1 = u_2$. More importantly, it should also contain the expression $\exp(c)$ for checking if in the current configuration the channel *c* is exposed, that is it is being used for transmission.

In the construct fix *X*.P occurrences of the recursion variable *X* in *P* are bound; similarly in the terms $[c?(x).P]Q$ and $c[x].P$ the data-variable *x* is bound in *P*. This gives rise to the standard notions of free and bound variables, $\alpha$-conversion and capture-avoiding substitution; we assume that all occurrences of variables in system terms are bound and we identify systems up to $\alpha$-conversion. Moreover we assume that all occurrences of recursion variables are guarded; they must occur within either a broadcast, input or time delay prefix, or within an execution branch of a matching construct. We will also omit trailing occurrences of nil, and write $[c?(x).P]$ in place of $[c?(x).P]nil$.

Our notion of wireless networks is captured by pairs of the form $\Gamma \triangleright W$, which represent the system term *W* running in the channel environment $\Gamma$. Such pairs are called configurations, and are ranged over by the metavariable *C*.
<table><caption>**Table 2** Intensional semantics: transmission</caption><tr><td>(Snd)</td><td>Γ ▷ c !⟨v⟩.P <span style="text-decoration: overline;">c!v</span> → σ<sup>δv</sup>.P</td><td>(Rcv)</td><td>Γ ▷ c : idle<br>Γ ▷ ⌊c?(x).P⌋Q <span style="text-decoration: overline;">c?v</span> → c[x].P</td></tr><tr><td>(RcvIgn)</td><td>¬rcv(W, c)<br>Γ ▷ W <span style="text-decoration: overline;">c?v</span> → W</td><td>(Sync)</td><td>Γ ▷ W<sub>1</sub> <span style="text-decoration: overline;">c!v</span> → W'<sub>1</sub><br>Γ ▷ W<sub>2</sub> <span style="text-decoration: overline;">c?v</span> → W'<sub>2</sub><br>Γ ▷ W<sub>1</sub> | W<sub>2</sub> <span style="text-decoration: overline;">c!v</span> → W'<sub>1</sub> | W'<sub>2</sub></td></tr><tr><td>(RcvPar)</td><td>Γ ▷ W<sub>1</sub> <span style="text-decoration: overline;">c?v</span> → W'<sub>1</sub><br>Γ ▷ W<sub>2</sub> <span style="text-decoration: overline;">c?v</span> → W'<sub>2</sub><br>Γ ▷ W<sub>1</sub> | W<sub>2</sub> <span style="text-decoration: overline;">c?v</span> → W'<sub>1</sub> | W'<sub>2</sub></td><td></td><td></td></tr></table>

### 3 Reduction semantics and contextual equivalence

The reduction semantics is defined incrementally. We first define the evolution of system terms with respect to a channel environment Γ via a set of SOS rules whose judgments take the form Γ ▷ W<sub>1</sub> λ → W<sub>2</sub>. Here λ can take the form c!v denoting a broadcast of value v along channel c, c?v denoting an input of value v being broadcast along channel c, τ denoting an internal activity, or σ, denoting the passage of time. However these actions will also have an effect on the channel environment, which we first describe, using a functional upd<sub>λ</sub>(·) : Env → Env, where Env is the set of channel environments.

The channel environment upd<sub>λ</sub>(Γ) describes the update of the channel environment Γ when the action λ is performed, is defined as follows: for λ = σ we let

$$ \text{upd}_{\sigma}(\Gamma) \vdash_t c : (n-1) \text{ whenever } \Gamma \vdash_t c : n, \quad \text{upd}_{\sigma}(\Gamma) \vdash_v c : w \text{ whenever } \Gamma \vdash_v c : w. $$

For λ = c!v we let upd<sub>c!v</sub>(Γ) be the channel environment such that

$$ \text{upd}_{c!v}(\Gamma) \vdash_t c : \begin{cases} \delta_v & \text{if } \Gamma \vdash c : \text{idle} \\ \max(\delta_v, k) & \text{if } \Gamma \vdash c : \text{exp} \end{cases} \quad \text{\textbf{upd}}_{c!v}(\Gamma) \vdash_v c : \begin{cases} v & \text{if } \Gamma \vdash c : \text{idle} \\ \text{err} & \text{if } \Gamma \vdash c : \text{exp} \end{cases} $$

where Γ ⊢<sub>t</sub> c : k. Finally, we let upd<sub>c?v</sub>(Γ) = upd<sub>c!v</sub>(Γ) and upd<sub>τ</sub>(Γ) = Γ.

Let us describe the intuitive meaning of this definition. When time passes, the time of exposure of each channel decreases by one time unit<fnref n="3" />. The predicates upd<sub>c!v</sub>(Γ) and upd<sub>c?v</sub>(Γ) model how collisions are handled in our calculus. When a station begins broadcasting a value v over a channel c this channel becomes exposed for the amount of time required to transmit v, that is δ<sub>v</sub>. If the channel is not free a collision happens. As a consequence, the value that will be received by a receiving station, when all transmissions over channel c terminate, is the error value err, and the exposure time is adjusted accordingly.

For the sake of clarity, the inference rules for the evolution of system terms, Γ ▷ W<sub>1</sub> λ → W<sub>2</sub>, are split in four tables, each one focusing on a particular form of activity.

<footnote n="3">³ For convenience we assume 0 − 1 to be 0.</footnote>
Table 2 contains the rules governing transmission. Rule (Snd) models a non-blocking broadcast of message $v$ along channel $c$. A transmission can fire at any time, independently on the state of the network; the notation $\sigma^{\delta_v}$ represents the time delay operator $\sigma$ iterated $\delta_v$ times. So when the process $c!\langle v \rangle.P$ broadcasts it has to wait $\delta_v$ time units before the residual $P$ can continue. On the other hand, reception of a message by a time-guarded listener $\lfloor c?(x).P \rfloor Q$ depends on the state of the channel environment. If the channel $c$ is free then rule (Rcv) indicates that reception can start and the listener evolves into the active receiver $c[x].P$.

The rule (RcvIgn) says that if a system can not receive on the channel $c$ then any transmission along it is ignored. Intuitively, the predicate rcv($W$, $c$) means that $W$ contains among its parallel components at least one non-guarded receiver of the form $\lfloor c?(x).P \rfloor Q$ which is actively awaiting a message. Formally, the predicate rcv($W$, $c$) is the least predicate such that rcv($\lfloor c?(x).P \rfloor Q$, $c$) = true and which satisfies the equations rcv($P$ + $Q$, $c$) = rcv($P$, $c$) $\lor$ rcv($Q$, $c$), rcv($W_1$ | $W_2$, $c$) = rcv($W_1$, $c$) $\lor$ rcv($W_2$, $c$) and rcv($vd.W$, $c$) = rcv($W$, $c$) if $d \neq c$. The remaining two rules in Table 2 (Sync) and (RcvPar) serve to synchronise parallel stations on the same transmission [8,17,18].

*Example 1 (Transmission).* Let $C_0 = \Gamma_0 \triangleright W_0$, where $\Gamma_0 \vdash c$, $d$: **idle** and $W_0 = c!\langle v_0 \rangle$ | $\lfloor d?(x).nil \rfloor([c?(x).Q])$ | $\lfloor c?(x).P \rfloor$ where $\delta_{v_0} = 2$.

Using rule (Snd) we can infer $\Gamma_0 \triangleright c!\langle v_0 \rangle \xrightarrow{c!v_0} \sigma^2$; this station starts transmitting the value $v_0$ along channel $c$. Rule (RcvIgn) can be used to derive the transition $\Gamma_0 \triangleright [d?(x).nil]([c?(x).Q]) \xrightarrow{c?v_0} [d?(x).nil]([c?(x).Q])$, in which the broadcast of value $v_0$ along channel $c$ is ignored. On the other hand, Rule (RcvIgn) cannot be applied to the configuration $\Gamma_0 \triangleright \lfloor c?(x).P \rfloor$, since this station is waiting to receive a value on channel $c$; however we can derive the transition $\Gamma_0 \triangleright \lfloor c?(x).P \rfloor \xrightarrow{c?v_0} c[x].P$ using Rule (Rcv).

We can put the three transitions derived above together using rule (Sync), leading to the transition $C_0 \xrightarrow{c!v} W_1$, where $W_1 = \sigma^2$ | $\lfloor d?(x).nil \rfloor([c?(x).Q])$ | $c[x].P$. $\square$

The transitions for modelling the passage of time, $\Gamma \triangleright W \xrightarrow{\sigma} W'$, are given in Table 3. In the rules (ActRcv) and (EndRcv) we see that the active receiver $c[x].P$ continues to wait for the transmitted value to make its way through the network; when the allocated transmission time elapses the value is then delivered and the receiver evolves to $\{w/x\}P$. The rule (SumTime) is necessary to ensure that the passage of time does not resolve non-deterministic choices. Finally (Timeout) implements the idea that $\lfloor c?(x).P \rfloor Q$ is a time-guarded receptor; when time passes it evolves into the alternative $Q$. However this only happens if the channel $c$ is not exposed. What happens if it is exposed is explained later in Table 4. Finally, Rule (TimePar) models how $\sigma$-actions are derived for collections of threads.

*Example 2 (Passage of Time).* Let $C_1 = \Gamma_1 \triangleright W_1$, where $\Gamma_1(c) = (2, v_0)$, $\Gamma_1 \vdash d$: **idle** and $W_1$ is the system term derived in Example 1.

We show how a $\sigma$-action can be derived for this configuration. First note that $\Gamma_1 \triangleright \sigma^2 \xrightarrow{\sigma} \sigma$; this transition can be derived using Rule (Sleep). Since $d$ is idle in $\Gamma_1$, we can apply Rule (TimeOut) to infer the transition $\Gamma_1 \triangleright \lfloor d?(x).nil \rfloor([c?(x).Q]) \xrightarrow{\sigma} \lfloor c?(x).Q \rfloor$; time passed before a value could be broadcast along channel $d$, causing a timeout in the
<figure><img src="image_2.png" /><figcaption>**Table 4** Intensional semantics: internal activity</figcaption></figure>

<figure><img src="image_3.png" /></figure>

station waiting to receive a value along *d*. Finally, since Γ₁ ⊢ₙ c : 2, we can use Rule (ActRcv) to derive Γ₁ ⊢ c[x].P ⊝ c[x].P.

At this point we can use Rule (TimePar) twice to infer a σ-action performed by C₁.
This leads to the transition C₁ ↪→ W₂, where W₂ = σ | [c?(x).Q] | c[x].P. □

Table 4 is devoted to internal transitions Γ ▷ W τ ↪ → W'. Let us first explain rule (RcvLate). Intuitively the process [c?(x).P]Q is ready to start receiving a value on an exposed channel c. This means that a transmission is already taking place. Since the process has therefore missed the start of the transmission it will receive an error value. Thus Rule (RcvLate) reflects the fact that in wireless systems a broadcast value cannot be correctly received by a station in the case of a misalignment between the sender and the receiver.

The remaining rules are straightforward except that we use a channel environment dependent evaluation function for Boolean expressions [[b]]<sub>Γ</sub>, because of the presence of the exposure predicate exp(c) in the Boolean language. However in wireless systems it is not possible to both listen and transmit within the same time unit, as communication is half-duplex, [19]. So in our intensional semantics, in the rules (Then) and (Else), the execution of both branches is delayed of one time unit; this is a slight simplification,
<table><caption>**Table 5** Intensional semantics: - structural rules</caption><tr><td>(TauPar)</td><td><div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">Γ ⧸ W<sub>1</sub></div><div style="padding: 0 5px;">|<br>W<sub>2</sub></div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">τ</div><div style="padding: 0 5px;">τ</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">W'<sub>1</sub></div><div style="padding: 0 5px;">|<br>W<sub>2</sub></div></div></td><td>(Rec)</td><td><div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">{fix X.P/X}P</div><div style="padding: 0 5px;">|<br>W</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">λ</div><div style="padding: 0 5px;">λ</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">W</div><div style="padding: 0 5px;">|<br>W</div></div></td></tr><tr><td>(Sum)</td><td><div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">Γ ⧸ P</div><div style="padding: 0 5px;">|<br>W</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">λ</div><div style="padding: 0 5px;">λ</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">λ</div><div style="padding: 0 5px;">λ</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">λ</div><div style="padding: 0 5px;">λ</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">W</div><div style="padding: 0 5px;">|<br>W</div></div></td><td>(SumRcv)</td><td><div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">Γ ⧸ P</div><div style="padding: 0 5px;">|<br>W</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">c<sup>?v</sup></div><div style="padding: 0 5px;">c<sup>?v</sup></div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">rcv(P, c)</div><div style="padding: 0 5px;">|<br>W</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">Γ ⧸ c</div><div style="padding: 0 5px;">|<br>c</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">c : idle</div><div style="padding: 0 5px;">|<br>W</div></div></td></tr><tr><td>(ResI)</td><td><div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">Γ[c ↦ (n, v)] ⧸ W</div><div style="padding: 0 5px;">|<br>W'</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">c<sup>?v</sup></div><div style="padding: 0 5px;">c<sup>?v</sup></div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">W'</div><div style="padding: 0 5px;">|<br>W'</div></div></td><td>(ResV)</td><td><div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">Γ[c ↦ (n, v)] ⧸ W</div><div style="padding: 0 5px;">|<br>W'</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">λ</div><div style="padding: 0 5px;">λ</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">W'</div><div style="padding: 0 5px;">|<br>W'</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">c ∉ λ</div><div style="padding: 0 5px;">c ∉ λ</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding: 0 5px;">W<sub>3</sub></div><div style="padding: 0 5px;">|<br>W<sub>3</sub></div></div></td></tr></table>

as evaluation is delayed even if the Boolean expression does not contain an exposure predicate.

*Example 3.* Let $Γ_2$ be a channel environment such that $Γ_2(c) = (1, v)$, and consider the configuration $C_2 = Γ_2 ⧸ W_2$, where $W_2$ has been defined in Example 2.

Note that this configuration contains an active receiver along the exposed channel $c$. We can think of such a receiver as a process which missed the synchronisation with a broadcast which has been previously performed along channel $c$; as a consequence this process is doomed to receive an error value.

This situation is modelled by Rule (RcvLate), which allows us to infer the transition $Γ_2 ⧸ [c?(x).Q] \xrightarrow{\tau} c[x].{err/x}Q$. As we will see, Rule (TauPar), introduced in Table 5, ensures that $τ$-actions are propagated to the external environment. This means that the transition derived above allows us to infer the transition $C_2 \xrightarrow{\tau} W_3$, where $W_3 = σ | c[x].{err/x}Q | c[x].P$. □

The final set of rules, in Table 5, are structural. Here we assume that Rules (Sum), (SumRcv) and (SumTime) have a symmetric counterpart. Rules (ResI) and (ResV) show how restricted channels are handled. Intuitively moves from the configuration $Γ ⧸ vc:(n, v).W$ are inherited from the configuration $Γ[c ↦ (n, v)] ⧸ W$; here the channel environment $Γ[c ↦ (n, v)]$ is the same as $Γ$ except that $c$ has associated with it (temporarily) the information $(n, v)$. However if this move mentions the restricted channel $c$ then the inherited move is rendered as an internal action $τ$, (ResI). Moreover the information associated with the restricted channel in the residual is updated, using the function upd<sub>c!v</sub>(·) previously defined.

We are now ready to define the reduction semantics; formally, we let $Γ_1 ⧸ W_1 \to Γ_2 ⧸ W_2$ whenever $Γ_1 ⧸ W_1 \xrightarrow{\lambda} W_2$ and $Γ_2 = upd_λ(Γ_1)$ for some $λ = τ, σ, c!v$. Note that input actions cannot be used to infer reductions for computations; following the approach of [15,21] reductions are defined to model only the internal of a system. In order to distinguish between timed and untimed reductions in $Γ_1 ⧸ W_1 \to Γ_2 ⧸ W_2$ we use $Γ_1 ⧸ W_1 \to_σ Γ_2 ⧸ W_2$ if $Γ_2 = upd_σ(W_1)$ and $Γ_1 ⧸ W_1 \to_i Γ_2 ⧸ W_2$ if $Γ_2 = upd_λ(Γ_1)$ for some $λ = τ, c!v$.
**Proposition 1 (Maximal Progress and Time Determinism).** Suppose $C \to_{\sigma} C_1$; then $C \to_{\sigma} C_2$ implies $C_1 = C_2$, and $C \not\to_i C_3$ for any $C_3$.

*Example 4.* We now show how the transitions we have inferred in the Examples 1-3 can be combined to derive a computation fragment for the configuration $C_0$ considered in Example 1.

Let $C_i = \Gamma_i \triangleright W_i$, $i = 0, \dots, 2$ be as defined in these examples. Note that $\Gamma_1 = \text{upd}_{c!v_0}(\Gamma_0)$ and $\Gamma_2 = \text{upd}_{\sigma}(\Gamma_1)$. We have already shown that $C_0 \xrightarrow{c!v_0} W_1$; this transition, together with the equality $\Gamma_1 = \text{upd}_{c!v_0}(\Gamma_0)$, can be used to infer the reduction $C_0 \to_i C_1$. A similar argument shows that $C_1 \to_{\sigma} C_2$. Also if we let $C_3$ denote $\Gamma_2 \triangleright W_3$ we also have $C_2 \to_i C_3$ since $\Gamma_2 = \text{upd}_{\tau}(\Gamma_2)$. $\square$

*Example 5 (Collisions).* Consider the configuration $C = \Gamma \triangleright W$, where $\Gamma \vdash c : \text{idle}$ and $W = c!\langle w_0 \rangle | c!\langle w_1 \rangle | \lfloor c?(x).P \rfloor$; here we assume $\delta_{w_0} = \delta_{w_1} = 1$. Using rules (Snd), (RcvIgn), (Rcv) and (Sync) we can infer the transition $\Gamma \triangleright W \xrightarrow{c!w_0} W_1$, where $W_1 = \sigma | c!\langle w_1 \rangle | c[x].P$. Let $\Gamma_1 := \text{upd}_{c!w_0}(\Gamma)$, that is $\Gamma_1(c) = (1, w_0)$. This equality and the transition above lead to the instantaneous reduction $C \to_i C_1 = \Gamma_1 \triangleright W_1$.

For $C_1$ we can use the rules (RcvIgn), (Snd) and (Sync) to derive the transition $C_1 \xrightarrow{c!w_1} W_2$, where $W_2 = \sigma | \sigma | c[x].P$. This transition gives rise to the reduction $C_1 \to_i C_2 = \Gamma_2 \triangleright W_2$, where $\Gamma_2 = \text{upd}_{c!w_1}(\Gamma_1)$. Note that, since $\Gamma_1 \vdash c : \text{exp}$ we obtain that $\Gamma_2(c) = (1, \text{err})$. The broadcast along a busy channel caused a collision to occur.

Finally, rules (Sleep), (EndRcv) and (TimePar) can be used to infer the transition $C_2 \xrightarrow{\sigma} W_3 = \text{nil} | \text{nil} | \{\text{err}/x\}P$. Let $\Gamma_3 := \text{upd}_{\sigma}(\Gamma'')$; then the transition above induces the timed reduction $C_2 \to_{\sigma} C_3 = \Gamma_3 \triangleright W_3$, in which an error is received instead of either of the transmitted values $w_0, w_1$. $\square$

We now define a contextual equivalence between configurations, following the approach of [10]. This relies on two crucial concepts: a notion of reduction, already been defined, and a notion of minimal observable activity, called a *barb*.

While in other process algebras the basic observable activity is chosen to be an output on a given channel [21,7], for our calculus it is more appropriate to rely on the exposure state of a channel: because of possible collisions transmitted values may never be received. Formally, we say that a configuration $\Gamma \triangleright W$ has a barb on channel $c$, written $\Gamma \triangleright W \downarrow_c$, whenever $\Gamma \vdash c : \text{exp}$. A configuration $\Gamma \triangleright W$ has a weak barb on $c$, denoted by $\Gamma \triangleright W \downarrow_c$, if $\Gamma \triangleright W \to^* \Gamma' \triangleright W'$ for some $\Gamma' \triangleright W'$ such that $\Gamma' \triangleright W' \downarrow_c$. As we will see, it turns out that using this notion of barb we can observe the content of a message being broadcast only at the end of its transmission. This is in line with the standard theory of wireless networks, in which it is stated that collisions can be observed only at reception time [23,19].

**Definition 1.** Let $\mathcal{R}$ be a relation over configurations.

(1) $\mathcal{R}$ is said to be barb preserving if $\Gamma_1 \triangleright W_1 \downarrow_c$ implies $\Gamma_2 \triangleright W_2 \downarrow_c$, whenever $(\Gamma_1 \triangleright W_1) \mathcal{R} (\Gamma_2 \triangleright W_2)$.

(2) It is reduction-closed if $(\Gamma_1 \triangleright W_1) \mathcal{R} (\Gamma_2 \triangleright W_2)$ and $\Gamma_1 \triangleright W_1 \to \Gamma'_1 \triangleright W'_1$ imply there is some $\Gamma'_2 \triangleright W'_2$ such that $\Gamma_2 \triangleright W_2 \to^* \Gamma'_2 \triangleright W'_2$ and $(\Gamma'_1 \triangleright W'_1) \mathcal{R} (\Gamma'_2 \triangleright W'_2)$.
<table><caption>**Table 6** Extensional actions</caption><tr><td>(Input)</td><td><div style="text-align: center;"><span style="display: inline-block; text-align: center; line-height: 1em;"><span style="display: block; padding-bottom: 0.1em;">Γ ▷ W</span><span style="display: block; border-top: 1px solid black; padding-top: 0.1em;">c<sup>2</sup><sub>v</sub></span></div> &rarr; W'</td></td><td>(Time)</td><td><div style="text-align: center;"><span style="display: inline-block; text-align: center; line-height: 1em;"><span style="display: block; padding-bottom: 0.1em;">Γ ▷ W</span><span style="display: block; border-top: 1px solid black; padding-top: 0.1em;">c<sup>2</sup><sub>v</sub></span></div> &rarr; W'</td></td></tr><tr><td>(Shh)</td><td><div style="text-align: center;"><span style="display: inline-block; text-align: center; line-height: 1em;"><span style="display: block; padding-bottom: 0.1em;">Γ ▷ W</span><span style="display: block; border-top: 1px solid black; padding-top: 0.1em;">c<sup>1</sup><sub>v</sub></span></div> &rarr; W'</td></td><td>(TauExt)</td><td><div style="text-align: center;"><span style="display: inline-block; text-align: center; line-height: 1em;"><span style="display: block; padding-bottom: 0.1em;">Γ ▷ W</span><span style="display: block; border-top: 1px solid black; padding-top: 0.1em;">&tau;</span></div> &rarr; W'</td></td></tr><tr><td>(Deliver)</td><td><div style="text-align: center;"><span style="display: inline-block; text-align: center; line-height: 1em;"><span style="display: block; padding-bottom: 0.1em;">Γ(c) = (1, v)</span><span style="display: block; border-top: 1px solid black; padding-top: 0.1em;">Γ ▷ W</span></div> &rarr; W'</td></td><td>(Idle)</td><td><div style="text-align: center;"><span style="display: inline-block; text-align: center; line-height: 1em;"><span style="display: block; padding-bottom: 0.1em;">Γ &vdash; c</span><span style="display: block; border-top: 1px solid black; padding-top: 0.1em;">: idle</span></div> &rarr; W'</td></td></tr></table>

(3) It is contextual if $Γ_1 ▷ W_1 R Γ_2 ▷ W_2$, implies $Γ_1 ▷ (W_1 | W) R Γ_2 ▷ (W_2 | W)$ for all processes $W$. □

Reduction barbed congruence, written $\cong$, is the largest symmetric relation over configurations which is barb preserving, reduction-closed and contextual.

**Example 6.** We first give some examples of configurations which are not barbed congruent; here we assume that $Γ$ is the stable environment.

- $Γ ▷ c!⟨v_0⟩ \neq Γ ▷ c!⟨v_1⟩$; let $T = [c?(x).[x = v_0]d!⟨ok⟩nil, ]$, where $d \neq c$ and $ok$ is an arbitrary value. It is easy to see that $Γ ▷ c!⟨v_0⟩ | T \twoheadleftarrow_d$, whereas $Γ ▷ c!⟨v_1⟩ | T \twoheadleftarrow_d$.

- $Γ ▷ c!⟨v⟩ \neq Γ ▷ σ.c!⟨v⟩$; let $T = [\exp(c)]d!⟨ok⟩, \text{nil}$. In this case we have that $Γ ▷ c!⟨v⟩ | T \twoheadleftarrow_d$, while $Γ ▷ σ.c!⟨v⟩ | T \twoheadleftarrow_d$.

On the other hand, consider the configurations $Γ ▷ c!⟨v_0⟩ | c!⟨v_1⟩$ and $Γ ▷ c!⟨err⟩$, where $δ_{v_0} = δ_{v_1}$ and for the sake of convenience we assume that $δ_{err} = δ_{v_0}$. In both cases a communication along channel $c$ starts, and in both cases the value that will be eventually delivered to some receiving station is `err`, independently of the behaviour of the external environment. This gives us the intuition that these two configurations are barbed congruent. Later in the paper we will develop the tools that will allow us to prove this statement formally. □

# 4 Extensional Semantics

In this section we give a co-inductive characterisation of the contextual equivalence $\cong$ between configurations, using a standard bisimulation equivalence over an extensional LTS, with configurations as nodes, but with a special collection of extensional actions; these are defined in Table 6.

Rule (Input) simply states that input actions are observable, as is the passage of time, by Rule (Time). Rule (TauExt) propagates $τ$-intensional actions to the extensional semantics. Rule (Shh) states that broadcasts are always treated as internal activities in the extensional semantics. This choice reflects the intuition that the content of a message being broadcast cannot be detected immediately; in fact, it cannot be detected until the end of the transmission.
Rule (Idle) introduces a new label $\iota(c)$, parameterized in the channel $c$, which is not inherited from the intensional semantics. Intuitively this rules states that it is possible to observe whether a channel is exposed. Finally, Rule (Deliver) states that the delivery of a value $v$ along channel $c$ is observable, and it corresponds to a new action whose label is $\gamma(c, v)$. In the following we range over extensional actions by $\alpha$.

**Example 7.** Consider the configuration $\Gamma \triangleright c!\langle v \rangle$, where $\Gamma$ is the stable channel environment. By an application of Rule (Shh) we have the transition $\Gamma \triangleright c!\langle v \rangle \xrightarrow{\tau} \Gamma' \triangleright \sigma^{\delta_v}$, with $\Gamma' \vdash c : \text{exp}$. Furthermore, $\Gamma \triangleright c!\langle v \rangle \xrightarrow{\iota(c)}$ since channel $c$ is idle in $\Gamma$. Notice that $\Gamma' \triangleright \sigma^{\delta_v}$ cannot perform a $\iota(c)$ action, and that the extensional semantics gives no information about the value $v$ which has been broadcast.

The extensional semantics endows configurations with the structure of an LTS. Weak extensional actions in this LTS are defined as usual, and the formulation of bisimulations is facilitated by the notation $C \stackrel{\hat{\alpha}}{\rightleftharpoons} C'$, which is again standard: for $\alpha = \tau$ this denotes $C \mapsto^* C'$ while for $\alpha \neq \tau$ it is $C \mapsto^* C' \mapsto^* C'$.

**Definition 2 (Bisimulations).** Let $\mathcal{R}$ be a symmetric binary relation over configurations. We say that $\mathcal{R}$ is a (weak) bisimulation if for every extensional action $\alpha$, whenever $C_1 \mathcal{R} C_2$, then $C_1 \stackrel{\alpha}{\rightleftharpoons} C'_1$ implies $C_2 \stackrel{\hat{\alpha}}{\rightleftharpoons} C'_2$ for some $C'_2$ satisfying $C'_1 \mathcal{R} C'_2$. We let $\approx$ be the largest bisimulation. $\square$

**Example 8.** Let us consider again the configurations $\Gamma \triangleright W_0 = c!\langle v_0 \rangle | c!\langle v_1 \rangle$, $\Gamma \triangleright W_1 = c!\langle \text{err} \rangle$ of Example 6. Recall that in this example we assumed that $\Gamma$ is the stable channel environment; further, $\delta_{v_0} = \delta_{v_1} = \delta_{\text{err}} = k$ for some $k > 0$.

We show that $\Gamma \triangleright W_0 \approx \Gamma \triangleright W_1$ by exhibiting a witness bisimulation $S$ such that $\Gamma \triangleright W_0 S \Gamma \triangleright W_1$. To this end, let us consider the relation

$$ S = \{ (\Delta \triangleright W_0, \Delta \triangleright W_1) , (\Delta' \triangleright \sigma^k | c!\langle v_1 \rangle, \Delta'' \triangleright \sigma^k) , (\Delta' \triangleright c!\langle v_0 \rangle, \Delta'' \triangleright \sigma^k) , (\Delta \triangleright \sigma^j | \sigma^j, \Delta \triangleright \sigma^j) | \Delta' \vdash_t c : n, \Delta''(c) = (n, \text{err}) \text{ for some } n > 0, j \leq k \} $$

Note that this relation contains an infinite number of pairs of configurations, which differ by the state of channel environments. This is because input actions can affect the channel environment of configurations. It is easy to show that the relation $S$ is a bisimulation which contains the pair $(\Gamma_0 \triangleright W_0, \Gamma_1 \triangleright W_1)$, therefore $\Gamma \triangleright W_0 \approx \Gamma \triangleright W_1$. $\square$

One essential property of weak bisimulation is that it does not relate configurations which differ by the exposure state of some channel:

**Proposition 2.** Suppose $\Gamma_1 \triangleright W_1 \approx \Gamma_2 \triangleright W_2$. Then for any channel $c$, $\Gamma_1 \vdash c : \text{idle}$ iff $\Gamma_2 \vdash c : \text{idle}$. $\square$

# 5 Full abstraction

The aim of this section is to prove that weak bisimilarity in the extensional semantics is a proof technique which is both sound and complete for reduction barbed congruence.

**Theorem 1 (Soundness).** $C_1 \approx C_2$ implies $C_1 \approx C_2$.
**Proof.** It suffices to prove that bisimilarity is reduction-closed, barb preserving and contextual. Reduction closure follows from the definition of bisimulation equivalence. The preservation of barbs follows directly from Proposition 2. The proof of contextuality on the other hand is quite technical, and is addressed in detail in the associated technical report [4]. One subtlety lies in the definition of $\tau$-extensional actions, which include broadcasts. While broadcasts along exposed do not affect the external environment, and hence cannot affect the external environment, this is not true for broadcasts performed along idle channels. However, we can take advantage of Proposition 2 to show that these extensional $\tau$-actions preserve the contextuality of bisimilar configurations. $\square$

To prove completeness, the converse of Theorem 1, we restrict our attention to the subclass of *well-formed* configurations. Informally $\Gamma \vdash W$ is well-formed if the system term $W$ does not contain active receivers along idle channels; a wireless station cannot be receiving a value along a channel if there is no value being transmitted along it.

**Definition 3 (Well-formedness).** The set of well-formed configurations WNets is the least set such that for all processes $P$ (i) $\Gamma \vdash P \in WNets$, (ii) if $\Gamma \vdash c : \mathbf{exp}$ then $\Gamma \vdash c[x].P \in WNets$, (iii) is closed under parallel composition and (iv) if $\Gamma[c \mapsto (n, v)] \vdash W \in WNets$ then $\Gamma \vdash vc : (n, v).W \in WNets$. $\square$

By focusing on well-formed configurations we can prove a counterpart of Proposition 2 for our contextual equivalence:

**Proposition 3.** Let $\Gamma_1 \vdash W_1, \Gamma_2 \vdash W_2$ be two well formed configurations such that $\Gamma_1 \vdash W_1 \approx \Gamma_2 \vdash W_2$. Then for any channel $c$, $\Gamma_1 \vdash c : \mathbf{idle}$ implies $\Gamma_2 \vdash c : \mathbf{idle}$. $\square$

Proposition 3 does not hold for ill-formed configurations. For example, let $\Gamma_1 \vdash c : \mathbf{exp}$, $\Gamma_1 \vdash d : \mathbf{idle}$ and $\Gamma_2 \vdash c, d : \mathbf{idle}$ and consider the two configurations $C_1 = \Gamma_1 \vdash \text{nil} | d[x].P$ and $C_2 = \Gamma_2 \vdash c!\langle v \rangle | d[x].P$, neither of which are well-formed; nor do they let time pass, $C_i \nvDash_{\sigma}$. As a consequence $C_1 \approx C_2$. However Proposition 2 implies that they are not bisimilar, since they differ on the exposure state of $c$.

Another essential property of well-formed systems is patience: time can always pass in networks with no instantaneous activities.

**Proposition 4 (Patience).** If $C$ is well-formed and $C \nvDash_i$, then $C \nvDash_{\sigma'} C'$ for some $C'$. $\square$

This means that, if we restrict our attention to well-formed configurations, we can never reach a configuration which is deadlocked; at the very least time can always proceed.

**Theorem 2 (Completeness).** On well-formed configurations, reduction barbed congruence implies bisimilarity.

The proof relies on showing that for each extensional action $\alpha$ it is possible to exhibit a test $T_\alpha$ which determines whether or not a configuration $\Gamma \vdash W$ can perform the action $\alpha$. The main idea is to equip the test with some fresh channels; the test $T_\alpha$ is designed so that a configuration $\Gamma \vdash W | T_\alpha$ can reach another one $C' = \Gamma' \vdash W' | T'$, where $T'$ is determined uniquely by the barbs of the introduced fresh channel; these are enabled in $\Gamma' \vdash T'$, if and only if $C$ can weakly perform the action $\alpha$.
The tests $T_\alpha$ are defined by performing a case analysis on the extensional action $\alpha$:

$$
\begin{align*}
T_{\tau} &= \text{eureka!}\langle\text{ok}\rangle \\
T_{\sigma} &= \sigma.(\tau.\text{eureka!}\langle\text{ok}\rangle + \text{fail!}\langle\text{no}\rangle) \\
T_{\gamma(c,v)} &= \text{vd:}(0, \cdot).((c[x].([x=v]d!\langle\text{ok}\rangle, \text{nil}) + \text{fail!}\langle\text{no}\rangle) | \\
&\qquad \quad | \sigma^2.[\text{exp}(d)]\text{eureka!}\langle\text{ok}\rangle, \text{nil} | \sigma.\text{halt!}\langle\text{ok}\rangle) \\
T_{c^?v} &= (c!\langle\text{v}\rangle.\text{eureka!}\langle\text{ok}\rangle + \text{fail!}\langle\text{no}\rangle) | \text{halt!}\langle\text{ok}\rangle \\
T_{t(c)} &= ([\text{exp}(c)]\text{nil, eureka!}\langle\text{ok}\rangle) + \text{fail!}\langle\text{no}\rangle | \text{halt!}\langle\text{ok}\rangle
\end{align*}
$$

where eureka, fail, halt are arbitrary distinct channels and ok, no are two values such that $\delta_{ok} = \delta_{no} = 1$.

For the sake of simplicity, for any action $\alpha$ we define also the tests $T'_\alpha$ as follows:

$$
\begin{align*}
T'_{\tau} &= T'_{\sigma} = \text{eureka!}\langle\text{ok}\rangle \\
T'_{\gamma(c,v)} &= \text{vd:}(0, \cdot).(\sigma.d!\langle\text{ok}\rangle\text{nil} | \sigma.[\text{exp}(d)]\text{eureka!}\langle\text{ok}\rangle, \text{nil} | \text{halt!}\langle\text{ok}\rangle) \\
T'_{c^?v} &= \sigma^{\delta_v}.\text{eureka!}\langle\text{ok}\rangle | \text{halt!}\langle\text{ok}\rangle \\
T'_{t(c)} &= \sigma.\text{eureka!}\langle\text{ok}\rangle | \text{halt!}\langle\text{ok}\rangle
\end{align*}
$$

**Proposition 5 (Distinguishing contexts).** Let $\Gamma \triangleright W$ be a well-formed configuration, and suppose that the channels eureka, halt, fail do not appear free in $W$, nor they are exposed in $\Gamma$. Then for any extensional action $\alpha$, $\Gamma \triangleright W \stackrel{\alpha}{\implies} \Gamma' \triangleright W'$ iff $\Gamma \triangleright W \mid T_\alpha \to^* \Gamma' \triangleright W' \mid T'_\alpha$. $\square$

A pleasing property of the tests $T'_\alpha$ is that they can be identified by the (both strong and weak) barbs that they enable in a computation rooted in the configuration $\Gamma \triangleright W \mid T_\alpha$.

**Proposition 6 (Uniqueness of successful testing components).** Let $\Gamma \triangleright W$ be a configuration such that eureka, halt, fail do not appear free in $W$, nor they are exposed in $\Gamma$. Suppose that $\Gamma \triangleright W \mid T_\alpha \to^* C'$ for some configuration $C'$ such that

- if $\alpha = \tau, \sigma$, then $C' \searrow_{\text{eureka}, C'} C' \searrow_{\text{eureka}, C'} C' \searrow_{\text{fail}}$,

- otherwise, $C' \searrow_{\text{eureka}, C'} C' \searrow_{\text{halt}, C'} C' \searrow_{\text{eureka}, C'} C' \searrow_{\text{halt}, C'} C' \searrow_{\text{fail}}$.

Then $C' = \Gamma' \triangleright W' \mid T'_\alpha$ for some configuration $\Gamma' \triangleright W'$. $\square$

Note the use of the fresh channel halt when testing some of these actions. This is because of a time mismatch between a process performing the action, and the test used to detect it. For example the weak action $\stackrel{t(c)}{\implies}$ does not involve the passage of time but the corresponding test uses a branching construct which needs at least one time step to execute. Requiring a weak barb on halt in effect prevents the passage of time.

**Outline proof of Theorem 2:** It is sufficient to show that reduction barbed congruence, $\simeq$, is a bisimulation. As an example suppose $\Gamma_1 \triangleright W_1 \simeq \Gamma_2 \triangleright W_2$ and $\Gamma_1 \triangleright W_1 \stackrel{\gamma(c,v)}{\implies} \Gamma'_1 \triangleright W'_1$. We show how to find a matching move from $\Gamma_2 \triangleright W_2$.

Suppose that $\Gamma_1 \triangleright W_1 \stackrel{\gamma(c,v)}{\implies} \Gamma'_1 \triangleright W'_1$, we need to show that $\Gamma_2 \triangleright W_2 \stackrel{\gamma(c,v)}{\implies} \Gamma'_2 \triangleright W'_2$ for some $\Gamma'_2 \triangleright W'_2$ such that $\Gamma'_1 \triangleright W'_1 \simeq \Gamma'_2 \triangleright W'_2$. By Proposition 5 we know that $\Gamma_1 \triangleright W_1 \mid T_{\gamma(c,v)} \to^* \Gamma'_1 \triangleright W'_1 \mid T'_\alpha$. By the hypothesis it follows that $\Gamma_1 \triangleright W_1 \mid T_{\gamma(c,v)} \simeq \Gamma_2 \triangleright W_2 \mid T_{\gamma(c,v)}$, therefore $\Gamma_2 \triangleright W_2 \mid T_{\gamma(c,v)} \to^* C_2$ for some $C_2 \simeq \Gamma'_1 \triangleright W'_1 \mid T'_\alpha$.
Let $C_1 = \Gamma'_1 \triangleright W'_1 | T'_{\gamma(c,v)}$. It is easy to check that $C_1 \Vdash_{eureka} C_1 \Vdash_{halt} C_1 \Vdash_{fail}$ and $C_1 \Vdash_{eureka} C_1 \Vdash_{halt}$. By definition of reduction barbed congruence and Proposition 3 we obtain that $C_2 \Vdash_{eureka} C_2 \Vdash_{halt} C_2 \Vdash_{eureka} C_2 \Vdash_{halt}$ and $C_2 \Vdash_{fail}$. Proposition 6 ensures then that $C_2 = \Gamma'_2 \triangleright W'_2 | T'_{\gamma(c,v)}$ for some $\Gamma'_2, W'_2$. An application of Proposition 5 leads to $\Gamma_2 \triangleright W_2 \mathrel{\substack{\mathop{\gamma(c,v)}\\[-0.8ex]\longrightarrow}} \Gamma'_2 \triangleright W'_2$. Now standard process calculi techniques enable us to infer from this that $\Gamma'_1 \triangleright W'_1 \approx \Gamma'_2 \triangleright W'_2$. $\square$

# 6 Conclusions and Related work

In this paper we have given a behavioural theory of wireless systems at the MAC level. We believe that our reduction semantics, given in Section 2, captures much of the subtlety of intensional MAC-level behaviour of wireless systems. We also believe that our behavioural theory is the only one for wireless networks at the MAC-Layer which is both sound and complete. The only other calculus which considers such networks is TCWS from [14] which contains a sound theory; as we have already stated we view CCCP as a simplification of this TCWS, and by using a more refined notion of extensional action we also obtain completeness.

We are aware of only two other papers modelling networks at the MAC-Sublayer level of abstraction, these are [12,24]. They present a calculus CWS which views a network as a collection of nodes distributed over a metric space. [12] contains a reduction and an intensional semantics and the main result is their consistency. In [24], time and node mobility is added.

On the other hand there are numerous papers which consider the problem of modelling networks at a higher level. Here we briefly consider a selection; for a more thorough review see [4].

Nanz and Hankin [16] have introduced an untimed calculus for Mobile Wireless Networks (CBS$^#$), relying on a graph representation of node localities. The main goal of that paper is to present a framework for specification and security analysis of communication protocols for mobile wireless networks. Merro [13] has proposed an untimed process calculus for mobile ad-hoc networks with a labelled characterisation of reduction barbed congruence, while [6] contains a calculus called CMAN, also with mobile ad-hoc networks in mind. Singh, Ramakrishnan and Smolka [22] have proposed the $\omega$-calculus, a conservative extension of the $\pi$-calculus. A key feature of the $\omega$-calculus is the separation of a node's communication and computational behaviour from the description of its physical transmission range. Another extension of the $\pi$-calculus, which has been used for modelling the LUNAR ad-hoc routing protocol, may be found in [2].

In [3] a calculus is proposed for describing the probabilistic behaviour of wireless networks. There is an explicit representation of the underlying network, in terms of a connectivity graph. However this connectivity graph is static. In contrast Ghassemi et al. [5] have proposed a process algebra called RBPT where topological changes to the connectivity graph are implicitly modelled in the operational semantics rather than in the syntax. Kouzapas and Philippou [11] have developed a theory of confluence for a calculus of dynamic networks and they use their machinery to verify a leader-election algorithm for mobile ad hoc networks.
References

1. I. F. Akyildiz, W. Su, Y. Sankarasubramaniam, and E. Cayirci. Wireless sensor networks: a survey. *Computer Networks*, 38(4):393-422, March 2002.

2. J. Borgström, S. Huang, M. Johansson, P. Raabjerg, B. Victor, J. Å. P., and Joachim Parrow. Broadcast psi-calculi with an application to wireless protocols. In *SEFM*, volume 7041 of LNCS, pages 74–89. Springer, 2011.

3. A. Cerone and M. Hennessy. Modelling probabilistic wireless networks (extended abstract). In Holger Giese and Grigore Rosu, editors, *FMOODS/FORTE*, volume 7273 of LNCS, pages 135–151. Springer, 2012.

4. A. Cerone, M. Hennessy, and M. Merro. Modelling mac-layer communications in wireless systems. Technical Report, Trinity College Dublin, 2012. https://www.scss.tcd.ie/~acerone/works/CCCP.pdf.

5. F. Ghassemi, W. Fokkink, and A. Movaghar. Equational reasoning on mobile ad hoc networks. *Fundamenta Informaticae*, 105(4):375–415, 2010.

6. J.C. Godskesen. A Calculus for Mobile Ad Hoc Networks. In *COORDINATION*, volume 4467 of LNCS, pages 132–150. Springer Verlag, 2007.

7. M. Hennessy. *A distributed Pi-calculus*. Cambridge University Press, 2007.

8. M. Hennessy and J. Rathke. Bisimulations for a calculus of broadcasting systems. *TCS*, 200(1-2):225–260, 1998.

9. M. Hennessy and T. Regan. A process algebra for timed systems. *IaC*, 117(2):221–239, March 1995.

10. K. Honda and N. Yoshida. On reduction-based process semantics. *TCS*, 152(2):437–486, 1995.

11. D. Kouzapas and A. Philippou. A process calculus for dynamic networks. In *FMOODS/FORTE*, volume 6722 of LNCS, pages 213–227. Springer, 2011.

12. I. Lanese and D. Sangiorgi. An operational semantics for a calculus for wireless systems. *TCS*, 411(19):1928–1948, 2010.

13. M. Merro. An Observational Theory for Mobile Ad Hoc Networks (full paper). *IaC*, 207(2):194–208, 2009.

14. M. Merro, F. Ballardin, and E. Sibilio. A timed calculus for wireless systems. *TCS*, 412(47):6585–6611, 2011.

15. R. Milner. *Communicating and Mobile Systems: The π-calculus*. Cambridge University Press, 1999.

16. S. Nanz and C. Hankin. Static analysis of routing protocols for ad-hoc networks. In *ACM SIGPLAN and IFIP WG*, volume 1, pages 141–152. Citeseer, 2004.

17. X. Nicollin and J. Sifakis. The algebra of timed processes, atp: Theory and application. *IaC*, 114(1):131–178, 1994.

18. K. V. S. Prasad. A calculus of broadcasting systems. *SCP*, 25(2-3):285–327, December 1995. ESOP '94 (Edinburgh, 1994).

19. T.S. Rappaport. *Wireless communications - principles and practice*. Prentice Hall, 1996.

20. J. Rathke and P. Sobocinski. Deconstructing behavioural theories of mobility. In *Fifth IFIP ICTCScience*, volume 273 of IFIP, pages 507–520. Springer, 2008.

21. D. Sangiorgi and D. Walker. *The Pi-Calculus — A Theory of Mobile Processes*. Cambridge University Press, 2001.

22. A. Singh, C.R. Ramakrishnan, and S.A. Smolka. A process calculus for mobile ad hoc networks. *SCP*, 75(6):440–469, 2010.

23. A.S. Tanenbaum. *Computer Networks*, 4th ed. Prentice-Hall International, Inc., 2003.

24. M. Wang and Y. Lu. A timed calculus for mobile ad hoc networks. *arXiv preprint arXiv:1301.0045*, 2013.

25. W. Yi. *A Calculus of Real Time Systems*. Ph.D Thesis, Chalmers University, 1991.