This paper explores the adaptation of Restricted Broadcast Process Theory to reliable communication in MANETs, analyzing its semantic implications and demonstrating its application through a routing protocol example.
Contribution
It introduces a modified framework for reliable communication in Restricted Broadcast Process Theory and develops a new proof process for protocol correctness.
Findings
01
Reliable communication affects the semantics of the process theory.
02
The non-blocking property and behavioral equivalence are impacted by the adaptation.
03
A novel proof process based on precongruence is proposed.
Abstract
Malfunctions of a mobile ad hoc network (MANET) protocol caused by a conceptual mistake in the protocol design, rather than unreliable communication, can often be detected only by considering communication among the nodes in the network to be reliable. In Restricted Broadcast Process Theory, which was developed for the specification and verification of MANET protocols, the communication operator is lossy. Replacing unreliable with reliable communication invalidates existing results for this process theory. We examine the effects of this adaptation on the semantics of the framework with regard to the non-blocking property of communication in MANETs, the notion of behavioral equivalence relation and its axiomatization. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on a precongruence…
Tables5
Table 1. Table 1: Semantics of RRBPT operators.
Table 2. Table 2: Semantics of the new operators of RCNT
Table 3. Table 3: Axioms for the choice, deployment, left and communication merge, and parallel operators. The sets M 1 subscript 𝑀 1 M_{1} and M 2 subscript 𝑀 2 M_{2} denote 𝑀𝑒𝑠𝑠𝑎𝑔𝑒 ( t 2 , ∅ ) ∖ 𝑀𝑒𝑠𝑠𝑎𝑔𝑒 ( t 1 , ∅ ) 𝑀𝑒𝑠𝑠𝑎𝑔𝑒 subscript 𝑡 2 𝑀𝑒𝑠𝑠𝑎𝑔𝑒 subscript 𝑡 1 {\it Message}(t_{2},\emptyset)\setminus{\it Message}(t_{1},\emptyset) and 𝑀𝑒𝑠𝑠𝑎𝑔𝑒 ( t 1 , ∅ ) ∖ 𝑀𝑒𝑠𝑠𝑎𝑔𝑒 ( t 2 , ∅ ) 𝑀𝑒𝑠𝑠𝑎𝑔𝑒 subscript 𝑡 1 𝑀𝑒𝑠𝑠𝑎𝑔𝑒 subscript 𝑡 2 {\it Message}(t_{1},\emptyset)\setminus{\it Message}(t_{2},\emptyset) respectively.
, if
Table 4. Table 4: Axiomatization of hiding, abstraction and encapsulation operators.
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Distributed systems and fault tolerance · Petri Nets in System Modeling
Malfunctions of a mobile ad hoc network (MANET) protocol caused by a conceptual mistake in the protocol design, rather than unreliable communication, can often be detected only by considering communication among the nodes in the network to be reliable. In Restricted Broadcast Process Theory, which was developed for the specification and verification of MANET protocols, the communication operator is lossy. Replacing unreliable with reliable communication invalidates existing results for this process theory. We examine the effects of this adaptation on the semantics of the framework with regard to the non-blocking property of communication in MANETs, the notion of behavioral equivalence relation and its axiomatization. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on a precongruence relation.
keywords:
Mobile ad hoc network, restricted broadcast, process algebra, behavioral congruence, refinement.
Reliable Restricted Process Theory
1 Introduction
The applicability of wireless communication is growing rapidly in areas like home networks and satellite transmissions,
due to their broadcasting nature. Mobile ad hoc networks (MANETs) consist of several portable hosts
with no pre-existing infrastructure, such as routers in wired networks or access points in managed (infrastructure) wireless
networks. The design of MANET protocols is complicated, because due to mobility of nodes the topology of communication links is dynamic.
Important MANET protocols such as the Ad hoc On Demand Distance Vector (AODV) routing protocol [1] contained flaws in their original design and have been revised accordingly.
Formal methods can be applied in the early phases of the protocol development to analyze and capture conceptual errors before their implementation. For instance, some errors in the design of AODV were found in [2, 3, 4, 5] using formal techniques.
There are numerous applications of existing formal frameworks such as SPIN [6, 7, 2] and UPPAAL [7, 8, 9, 10, 11, 12] for the analysis of MANET protocols. Lack of support for compositional modeling and arbitrary topology changes motivates developing a new approach, tailored to the domain of MANETs, with a primitive for local broadcast and supporting the verification of MANET protocols against changes of the underlying topology. The tailored formal modeling framework should provide some form of wireless communication which varies at the different layers of the Open Systems Interconnection (OSI) model: physical, data link, network, transport, session, presentation, and application. For instance, the data link layer is responsible for transferring data across the physical link and handling conflicts due to simultaneous accesses to the shared media. In contrast, communication at the network layer provides point-to-point communication between two nodes that are not directly connected through appropriate routing of messages by using the communication service of the data link layer.
Most frameworks for the formal analysis of MANET protocols, such as [13, 14, 15, 16, 17, 18, 19, 20, 21, 5], focus on protocols above the data link layer; hence they support the core services of this layer, which means that local broadcast is the primitive means of communication. Wireless communication at this layer is non-blocking, i.e., the sender broadcasts irrespective of the readiness of its receivers, and is asynchronous, i.e., received packets are buffered at the receiver. The data link layer of a node processes the packet if it is an intended destination. While a node is busy processing a message, it can still receive messages, buffer them and process them later. However, if two different nodes broadcast simultaneously with a common node in their range, the latter node cannot receive both messages and drops one of them, which is called the hidden node problem. We say that wireless communication is reliable if the intended receivers successfully receive the packet. In other words, message delivery is guaranteed to all connected neighbors.
Although lossy communication is an integral part of MANETs, mimicking it faithfully in a formal framework can hamper the formal analysis of MANET protocols. To obtain a deeper understanding of a malfunctioning of such a protocol due to a conceptual mistakes in its design rather than unreliable communication, it may be helpful to consider communication reliable, meaning that the possibility of the hidden node problem is omitted from the framework. Therefore we introduced the process algebra Reliable Restricted Broadcast Process Theory (RRBPT) in [22], to perform model checking of MANET protocols in a setting where communication is reliable. It is a variant of Restricted Broadcast Process Theory (RBPT) that we introduced previously in [23] for the modeling and analysis of protocols above the data link layer. The underlying semantic model of RBPT, a so-called constrained labeled transition system (CLTS), implicitly considers mobility of nodes with the novel notion of a network constraint, which abstractly defines a set of topologies: those satisfying the given connectivity constraints. The transitions of a CLTS are annotated with appropriate network constraints to restrict the behavior to MANETs with a topology of the specified ones. RBPT was extended with a set of auxiliary operators to reason about MANETs by equational reasoning, so-called Computed Network Process Theory (CNT) [24]. We provided a sound and complete axiomatization for CNT terms with finite-state behaviors, modulo so-called rooted branching computed network bisimilarity. This axiomatization enables linearization of processes at the syntactic level to take advantage of symbolic verification [25, 26], especially when the network is composed of similar nodes [27, 28].
Somewhat surprisingly, all these results do not carry over in a
straightforward fashion from RBPT to RRBPT. To put the
model checking approach presented in [22] on a firm basis,
the current paper develops the formal foundations for RRBPT
and modifies the core of CNT. In a lossy setting, the
non-blocking property of local broadcast communication is an
immediate consequence of the rule Par and its counterpart
for the parallel composition: \frac{\raisebox{2.1097pt}{\normalsize{t_{1}\stackrel{{\scriptstyle a}}{{\overrightarrow{\smash{,{\phantom{a}},}}}}t_{1}^{\prime}}}}{\raisebox{-3.01389pt}{\normalsize{t_{1}\parallel t_{2}\stackrel{{\scriptstyle a}}{{\overrightarrow{\smash{,{\phantom{a}},}}}}t_{1}^{\prime}\parallel t_{2}}}}, which expresses that if a node is
not ready to participate in a communication, then we can assume that
either it was disconnected from the sender or it was connected but
has lost the message. However, in the reliable setting, to guarantee
the non-blocking property, nodes should always be input-enabled.
RRBPT provides a sensing operator which allows to change the
control flow of a process depending on the status of node
connectivity with other nodes. The input-enabledness feature is
ensured through the RRBPT operational rules, where the main
difference between RRBPT and RBPT is: in RRBPT,
nodes lose a communication only when they are disconnected and are
always input-enabled. We recap challenges of bringing
input-enabledness feature in the semantics of RRBPT in the
presence of the sensing operator. Furthermore, the behavioral
equivalence relation of CNT setting is not a congruence with
respect to parallel composition anymore. To support the desired
distinguishing power, we provide a new bisimulation relation which
guarantees the congruence property for MANETs. RRBPT can be
extended in the same way as RBPT with computed network terms
and the auxiliary operators left merge ( ) and
communication merge (∣) to provide a sound and complete
axiomatization for the parallel composition. However, the
input-enabledness feature and the new sensing operator require new
auxiliary operators to assist their axiomatization. To this aim, we
discuss the appropriate axioms of RRBPT. We utilize our axioms
to analyze the correctness of protocols at the syntactic level. To
this aim, we facilitate the specification of the protocol behaviors
preconditioned to multihop constraints and then introduce a new
notion of refinement among protocol implementations and their
specifications. We demonstrate the applicability of our framework by
analyzing and proving the correctness of a simple routing protocol
inspired by the AODV protocol.
This paper is organized as follows. Sections 2 and 4 introduce our semantic model and explain how it is helpful in giving semantics to reliable communication. Section 3 introduces the syntax of RRBPT. Sections 5 and 6 provide the appropriate notion of behavioral equivalence and axioms in the reliable setting, respectively. We demonstrate the applicability of our new framework by analyzing a simple routing protocol in Section 7.
We review and compare the related process algebraic frameworks in depth in Section 8 before concluding the paper.
2 Constrained Labeled Transition Systems
Let Loc denote a set of network addresses, ranged over by ℓ. Viewing a network topology as a directed graph, it can be defined as γ:Loc→IP(Loc), where γ(A) expresses the set of nodes that are directly connected to A, and hence, can receive message from A. A network constraint C is a set
of connectivity pairs ⇝:Loc×Loc and
disconnectivity pairs ⇝:Loc×Loc. In this
setting, non-existence of (dis)connectivity information between two
addresses implies lack of information about this link (which can
e.g. be helpful when the link has no effect on the evolution of the
network). For instance, B⇝A denotes that A is connected to
B directly and consequently A can receive data sent by B as before,
while B⇝A denotes that A is not connected to B directly
and consequently cannot receive any message from B. The direction of an arrow shows the direction of information flow. We write
{B⇝A,C,B⇝D,E} instead of {B⇝A,B⇝C,B⇝D,B⇝E}. The set Loc is
extended with the unknown address ? to represent the
address of a node which is still not known or concealed from an
external observer. For instance, the leader
address of a node can be initialized to this value.
Furthermore, to define the semantics of communicating nodes in terms of
restrictions over the topology in a compositional way, the semantics of
receive actions can be defined through an unknown sender, which will be
replaced by a known address when the receive actions are composed with the corresponding send
action at a specific node (see Section 4).
A network
constraint C is said to be well-formed if ∀ℓ,ℓ′∈Loc(ℓ⇝ℓ′∈C∨ℓ⇝ℓ′∈C). Let Cv(Loc) denote the
set of well-formed network constraints that can be defined over
the network addresses in Loc. We define an ordering on network constraints. We say that C1≼C2 iff C2⊆C1 or ∃ℓ∈Loc(C2[ℓ/?]⊆C1), where d[d1/d2]
denotes the substitution of d1 for d2 in d; this can
be extended to process terms. For instance, {B⇝A}≼{?⇝A} and {B⇝A,B⇝C}≼{B⇝A}. Each well-formed network
constraint C represents the set of network topologies
that satisfy the (dis)connectivity pairs in C, i.e., Γ(C)={γ∣CΓ(γ)≼C}
where CΓ(γ)={ℓ⇝ℓ′∣ℓ′∈γ(ℓ)}∪{ℓ⇝ℓ′∣ℓ′∈γ(ℓ)} extracts all one-hop (dis)connectivity
information from γ. So the empty network constraint {} still
denotes all possible topologies over Loc. The negation
¬C of network constraint C is obtained
by negating all its (dis)connectivity pairs. Clearly, if
C is well-formed then so is ¬C.
Constrained labeled transition systems (CLTSs) provide a semantic model for the operational
behavior of MANETs. Let Msg denote a
set of messages communicated over a network and ranged over by
m. Let Act be the network send and receive
actions with signatures nsnd:Msg×Loc
and nrcv:Msg, respectively. The send action
nsnd(m,ℓ) denotes that the message m
is transmitted from a node with the address ℓ, while the
receive action nrcv(m) denotes that the message
m is ready to be received. Let Actτ=Act∪{τ}, ranged over by η.
Definition 2.1
A CLTS is a tuple ⟨S,Λ,→,s0⟩,
with S a set of states, Λ⊆Cv(Loc)×Actτ, →⊆S×Λ×S a
transition relation, and s0∈S the initial state. A transition
(s,(C,η),s′)∈→ is denoted by
s(C,η)(C,η)s′.
Generally speaking, the transition s(C,η)(C,η)s′ expresses that a MANET protocol in
state s with an underlying topology γ∈Γ(C) can
perform action η to evolve to state s′.
The semantics of broadcast communication is defined to be reliable if and if only the nodes that are connected to the sender, as defined by its corresponding network constraint, receive the message. We remark that the status of the links from the receivers to the sender or between two arbitrary receivers are not of importance and hence, they are abstracted away. Therefore, by constructing such network constraints through the semantic rules, reliable communication is brought into our framework.
3 Syntax of RRBPT
Let A denotes a countably infinite set of
process names which are used as recursion variables in recursive
specifications. Besides network send and receive actions, i.e., nsnd(m,ℓ) and nrcv(m), we assume protocol send and receive actions, denoted by
snd,rcv:Msg, i.e., parametrized by messages. Furthermore, let
IAct be a set of internal actions. The syntax of
RRBPT is given by the following grammar:
[TABLE]
The deadlock process is modeled by [math]. The process α.t
performs action α and then behaves as process t, where
α is either an internal action or a protocol send/receive
action snd(m)/rcv(m). Internal actions are
useful in modeling the interactions of a process with other
applications running on the same node. Protocol send/receive actions
specify the interaction of a process with its data-link layer
protocols: these protocols are responsible for transferring messages
reliably throughout the network. These actions are turned into their
corresponding network ones via the semantics (see Section
4). The process t1+t1 behaves non-deterministically as t1 or
t2. The simplest form of a MANET is a node, represented by the network
deployment operator [[t]]ℓ, denoting process t deployed
on a node with the known network address ℓ=? (where ?
denotes the unknown address). A MANET can be
composed by putting MANETs in parallel using ∥; the nodes communicate with
each other by reliable restricted broadcast. A process name is
specified by a recursive equation A=deft where A∈A is a name.
MANET protocols may behave based on the (non-)existence of a link.
A neighbor discovery service can be implemented at the data link layer,
by periodically sending hello messages and acknowledging
such messages received from a neighbor. The sensing operator sense(ℓ′,t1,t2)
examines the status of the link from the node, say with address ℓ, that the sensing is executed
on to the node with the address ℓ′; in case of its existence it behaves as t1, and otherwise as
t2. For instance, the term [[sense(ℓ′,t1,t2)]]ℓ examines the existence of the link
ℓ⇝ℓ′, and then behaves accordingly. As a running example, P=defsense(B,snd(dataB).P,0) denotes a process that recursively broadcasts a data
message dataB as long as it is connected to B; and Q=defrcv(dataB).deliver.Q
a process that recursively receives a data message data and then
the internal action deliver upon successful receipt of data. The network process [[P]]A∥[[Q]]B specifies an ad hoc network composed of two nodes with the
network addresses A and B deploying processes P and Q,
respectively.
The hide operator
(νℓ)t conceals the address ℓ in the process t, by
renaming this address to ? in network send/receive actions. For
each message m∈Msg, the abstraction operator τm(t)
renames network send/receive actions over messages of type m to
τ, and the encapsulation operator ∂m(t) forbids
receiving messages of type m. Let τ{m1,…,mn}(t)
and ∂{m1,…,mn}(t) denote
τm1(…(τmn(t))…) and
∂m1(…(∂mn(t))…).
For example, τMsg(∂Msg([[P]]A∥[[Q]]B)) specifies an isolated MANET that
cannot receive any message from the environment, while its
communications (i.e., send actions) are abstracted away.
Terms should be grammatically well-defined, meaning that processes
deployed at a network address are only defined by action prefix,
choice, sense and process names. Furthermore, the application of action prefix,
choice, sense and process names is restricted to the deployment operator.
4 Semantics of RRBPT
The operational rules in
Table 1
induce a CLTS with transitions of the form tββt′,
where β∈Cv(Loc)×Actτ where Act={NAct∪IAct}, NAct denotes the set of network
send and receive actions, and IAct the set of internal
actions ranged over by i. Assume that α denotes actions of the form {rcv(m),snd(m)∣m∈Msg}. In these rules,
t(C,nrcv(m))(C,nrcv(m)) denotes that there
exists no t′ such that
t(C′,nrcv(m))(C′,nrcv(m))t′ and
C′≼C. The symmetric counterparts of the rules Choice, Bro, and Par hold, but have been omitted for the brevity.
Rule Prefix assigns an empty network constraint to each prefixed action, which may be accumulated by further constraints through application of rules Rcv1 or Sen1,2. The rule Int indicates that a node progresses when the deployed process on the node performs an internal action.
Interaction between the process t and its data-link layer is
specified by the rules Snd and Rcv1,2: when t broadcasts a message, it
is delivered to the nodes in its transmission range, disregarding
their readiness. Rcv1 specifies that a process t with an
enabled receive action can perform it successfully if it has a link
to a sender (not currently known). If a node does not have any
enabled receive action nrcv(m) for the network constraint C, then receiving the
message has no effect on the node behavior, as explained by Rcv2. This rule also implicitly implies that an enabled receive action cannot be performed when the node is disconnected from the
sender (not currently known). Consequently, this rule makes nodes
input-enabled, meaning that a node not ready to receive a
message will drop it. Rule Rcv2 adds a network receive action (C,nrcv(m)) to the behavior of a network node, specified by [[t]]ℓ, if it has no transition (C′,nrcv(m)) such that C′≼C. Furthermore, this rule ensures that a most general C is selected, and hence, the receive action nrcv(m) is defined for all possible network constraints (when combined with rule Exe). Therefore, [[P]]A has a ({},nrcv(dataB))-transition by application of this rule.
Rules Sen1,2 explain the behavior of the sense operator. In case there is
a link to the node with the address ℓ from the node that is running
the sense operator, and currently its address is unknown, then it behaves
like t1; in case this link is not present, it behaves like t2. Therefore, the link status is combined
with the network constraint C generated by its first or
second term argument, as given by Sen1,2 respectively.
For instance, by Prefix and Sen1, P only
generates a ({?⇝B},snd(dataB))-transition.
In rules Snd and Rcv1, the network constraint
C may have the unknown address due to sensing
operators, which is replaced by the address of the deployment
operator, i.e., C[ℓ/?].
Therefore, by applying Snd to the only transition of P, [[P]]A generates a ({A⇝B},nsnd(dataB))-transition.
Rule Recv synchronizes the receive actions of processes
t1 and t2 on message m, while combining together
their (dis)connectivity information in network constraints
C1 and C2. Rule Bro specifies
how a communication occurs between a receiving and a sending
process. This rule combines the network constraints, while the
unknown location (in the network constraint of the receiving
process) is replaced by the concrete address of the sender. In
Bro and Recv it is required that the union of network
constraints on the transition in the conclusion be well-formed.
The rule Par prevents evolution of sub-networks
on network actions, in contrast to lossy settings, and enforces all nodes to specify their
localities with respect to the sender before evolving the whole
network via Recv or Bro rules. It only allows a process to evolve by performing an internal or silent action. Exe explains that a behavior
that is possible for a network constraint, is also possible for a
more restrictive network constraint.
For instance, the MANET [[P]]A∥[[Q]]B can generate the ({B⇝A},nsnd(dataB,A)) transition induced by the deduction tree below, where
y≡deliver.Q:
Rule Hid replaces every occurrence of ℓ in the network
constraint and action of β by ?, and hence hides activities
of a node with address ℓ from external observers. According to
Abs, the abstraction operator τm converts all network
send and receive actions with a message of type m to τ and
leaves other actions unaffected, as defined by the function
τm(η). The encapsulation operator ∂m disallows
all network receive actions on messages of type m, as specified by
Encap.
The semantics of RRBPT was first introduced in [22] with the aim of defining CLTSs with negative connectivity pairs to illustrate their benefit for model checking MANET protocols. In this research, we modify its semantics to properly define the behavior of MANETs in the reliable setting. To this end, two groups of rules have been modified substantially: those of receive actions and the sensing operator. More specifically, the operational semantics of receive action in [22] explicitly specifies the
locality of the receiver node with respect to the sender (that could be connected,
disconnected, or unknown) through three semantic rules. Furthermore, the semantics of the sensing operator in [22] makes [[P]]A move by ({B⇝A,?⇝A},nrcv(dataB)) and ({B⇝A,?⇝A},nrcv(dataB)) to [[0]]A while here it has a self-loop with the label of ({B⇝A},nrcv(dataB)). In other words, the chance of sending dataB is lost after dropping a received message of dataB. Such a drawback is resolved by the newly introduced rule Rcv2 and removing two previous rules of the sensing operator.
Terms of the lossy framework RBPT are considered modulo rooted branching computed
network bisimilarity [24].
This equivalence relation is defined using the following notations:
•
⇒ denotes the reflexive and transitive closure of unobservable actions:
–
t⇒t;
–
if t(C,τ)(C,τ)t′ for some arbitrary network constraint C and
t′⇒t′′, then t⇒t′′.
•
t⟨(C,η)⟩⟨(C,η)⟩t′ iff t(C,η)(C,η)t′ or t(C[ℓ/?],η[ℓ/?])(C[ℓ/?],η[ℓ/?])t′ and
η is of the form nsnd(m,?) for some m.
Intuitively t⇒t′ expresses that after a number of communications, t can behave like t′. Furthermore, an action like
({?⇝B},nsnd(req(?),?)) can be matched to an action like
({A⇝B},nsnd(req(A),A)), which is its ⟨−⟩ counterpart.
Definition 5.1
A binary relation
R on RBPT terms is a branching computed network
simulation if t1Rt2 and t1(C,η)(C,η)t1′ implies that either:
•
η* is of the form nrcv(m) or τ, and t1′Rt2; or*
•
there are t2′ and t2′′ such that t2⇒t2′′⟨(C,η)⟩⟨(C,η)⟩t2′, where t1Rt2′′ and t1′Rt2′.
R* is a branching computed network bisimulation if R and R−1
are branching computed network simulations. Two terms t1 and
t2 are branching computed network bisimilar, denoted by t1≃bt2, if t1Rt2 for some branching computed
network bisimulation relation R.*
This definition distinguishes process terms according to their abilities to broadcast messages, and therefore, MANET protocols that can only receive are treated as deadlock as they cannot send any observable message.
Definition 5.2
Two terms
t1 and t are rooted branching computed network
bisimilar, written t1≃rbt2, if:
•
t1(C,η)(C,η)t1′* implies there is a t2′ such that
t2⟨(C,η)⟩⟨(C,η)⟩t2′ and t1′≃bt2′;*
•
t2(C,η)(C,η)t2′* implies there is a t1′ such that
t1⟨(C,η)⟩⟨(C,η)⟩t1′ and t1′≃bt2′.*
Rooted branching computed network bisimilarity does not constitute a congruence with respect to the RRBPT operators. We still want that a
receiving MANET (after its first action) be equivalent to
deadlock. In this setting, still [[0]]A≃b[[rcv(m).0]]A, but [[0]]A∥[[snd(m).0]]B≃b[[rcv(m).0]]A∥[[snd(m).0]]B, since by application of Rcv1,2, Snd, and Bro:
[TABLE]
while by application of Rcv2, Snd, Bro:
[TABLE]
which cannot be matched to any transition of [[rcv(m).0]]A∥[[snd(m).0]]B according to the second condition of Definition 5.1. However, we observe that the ({},nsnd(m,B))-transition can be matched to the transition sets of actions ({B⇝A},nsnd(m,B)) and ({B⇝A},nsnd(m,B)), as the network constraints {B⇝A} and {B⇝A} provide a partitioning of {} while the resulting states of their corresponding transitions are equivalent. Thus, we revise our Definition 5.1 by generalizing its second condition.
Intuitively, two MANETs are equivalent if they have the same observable behaviors for all possible underlying topologies. In the lossy setting, the observable behaviors exclude receive actions, as the node [[rcv(a).snd(a).0]]A can be distinguished from [[rcv(a).0]]A due to its capability to send a after its receipt. However, the capability of receiving messages implicitly defines a restriction on the underlying topology. For instance, the sending action snd(a) in [[rcv(a).snd(a).0]]A is only possible if the node in question was previously connected to a sender and successfully received a. Thus to distinguish [[rcv(a).snd(a).0]]A from [[snd(a).0]]A, receive actions are included in the observables in the reliable setting. Furthermore, as dropping a message may have the same effect as its processing (as explained above), a transition cannot be matched in the same way as in Definition 5.1 and it may be matched to multiple transitions. A partitioning of a network constraint C consists of network constraints C1, … , Cn such that ∀i,j≤n(i=j⇒Γ(Ci)∩Γ(Cj)=∅)∧⋃k=1nΓ(Ck)=Γ(C).
Definition 5.3
A binary relation
R on RRBPT terms is a branching reliable computed network
simulation if t1Rt2 and t1(C,η)(C,η)t1′ imply that either:
•
η* is a τ action, and t1′Rt2; or*
•
there are s1′′,…,sk′′ and s1′,…,sk′ for some k>0 such that ∀i≤k(t2⇒si′′⟨(Ci,η)⟩⟨(Ci,η)⟩si′, with t1Rsi′′ and t1′Rsi′), and ⟨C1⟩,…,⟨Ck⟩ constitute a partitioning of ⟨C⟩.
R* is a branching reliable computed network bisimulation if R and R−1
are branching reliable computed network simulations. Two terms t1 and
t2 are branching reliable computed network bisimilar, denoted by t1≃brt2, if t1Rt2 for some branching reliable computed network bisimulation relation R.*
Trivially (t1≃bt2)⇒(t1≃brt2).
Theorem 5.4
Branching reliable computed network bisimilarity is an equivalence.
To provide a sound and complete axiomatization for closed RRBPT terms with respect to rooted branching reliable computed network bisimilarity, the framework should be extended with the computed network terms, i.e., (C,η).t which expresses that action η is possible for topologies belonging to C, in the same way as [24]. This prefix operator is helpful to transform protocol send/receive actions into their corresponding network ones. Furthermore, it borrows the operators left merge
( ) and communication merge from the process algebra
ACP [29] to axiomatize
parallel composition. Note that the interleaving semantics for parallel composition is only valid for internal and unobservable actions (see rule Par). To axiomatize the behavior of nodes while being input-enabled, we also exploit two novel auxiliary operators.
RRBPT is extended with new operators and called Reliable Computed Network Process Theory (RCNT). Its syntax contains:
[TABLE]
The prefix operator in
β.t again denotes a process which performs β and then behaves as t. The action β can now be of two types:
either an internal action or a send/receive action snd(m)/rcv(m), denoted by α, or actions of the form
(C,nrcv(m)), (C,nsnd(m,ℓ)) and (C,τ), denoted by (C,η), where the first two
actions are called the network receive and send actions, respectively. The new operator ℓ:t1:t2, so-called local deployment, defines the behavior of process t2 deployed at the network address ℓ while it only considers the input-enabledness feature with regard to the behavior of t2. In cases that it should drop a message (i.e., processing the message has not been defined by t2), it behaves as t1. This operator is helpful to axiomatize the behavior of the deployment operator in the reliable setting. To axiomatize the behavior of the sense operator, the framework is extended with the topology restriction operator C⊳t which restricts the behavior of t by taking restrictions of C into account.
Due to the input-enabledness feature of nodes, their behavior is recursive: upon receiving a message for which no receive action has been defined, a node drops the message. To this aim, we exploit the recursion operator recA⋅t, which specifies the solution of the process name A, defined by the equation A=deft. The process term tA is a solution of the equation A=deft if the replacement of A by tA on both sides of the equation results in equal terms, i.e. tA≃rbt[tA/A]. As we are interested in equations with exactly one solution, we define a guardedness criterion for network names, in the same way as [24]. A free
occurrence of a network name A in t is called
guarded if this occurrence is in the scope of an action
prefix operator (not (C,τ) prefix) and not in the scope of an
abstraction operator [30]; in other words, there is
a subterm (C,η).t′ in t such that η=τ, and
A occurs in t′. A is
(un)guarded in t if (not) every free occurrence of
A in t is guarded. A RCNT term t is
guarded if for every subterm recA⋅t′,
A is guarded in t′. This guardedness criterion
ensures that any guarded recursive term has a unique solution.
A term is grammatically well-defined if its processes
deployed at a network address through either a network or local deployment operator, are only defined by action prefix,
choice, sense, and process names.
The operational semantic rules of the new operators are given in Table 2 while the counterpart of Sync2 holds. In these rules,
trcv(m)rcv(m) denotes that there
exists no t′ such that
t(C′,rcv(m))(C′,rcv(m))t′ for some network constraint C′. The behavior of the local deployment operator is almost similar to the deployment operator. Its rules Inter1′ and Inter2′ are the same as Snd and Rcv1, respectively. However, it substitutes Inter3′ for Rcv2 by which it only adds transitions containing the disconnectivity pair ?⇝ℓ for those possible receive actions of t2 (generated by Rcv1).
Rules Sen3,4 make the behavior of sense(ℓ′,t1,t2) input-enabled toward receive actions that are possible by t1 but not t2 and vice versa. The constraints of the topology restriction operator C⊳t is added to the behaviors of t as explained by the rule TR.
The main differences of extended RCNT with CNT are that its deployed nodes are input-enabled and its communication primitive is reliable. We use the notation ∑m∈Mt to define t[m1/m]+…+t[mk/m], where M={m1,…,mk}. Furthermore, if(b,t1,t2) behaves as t1 if the condition b holds and otherwise as t2.
The axioms regarding the choice, deployment, left and communication merge, and parallel operators are given in Table 3. The axioms Ch1−4, Br, LM2,3 and S1−4 are
standard (cf. [31]). The axiom Ch5
denotes that a network send action
whose sender address is unknown can be
removed if its counterpart action exists. The axiom Ch6 explains that a more liberal network constraint allows more behavior. Axioms Dep0−7, LM1,2′, and TRes1−5 are new in comparison with the lossy setting of [24]. The axiom (\mathcal{C},\eta).t_{1}\,\begin{picture}(1.0,1.75)\put(0.0,0.0){\line(1,0){1.0}}\put(0.0,0.0){\line(0,1){1.75}}\put(0.45,0.0){\line(0,1){1.75}}\end{picture}\,t_{2}=(\mathcal{C},\eta).(t_{1}\parallel t_{2}) has been replaced by LM1,2′ which only allow internal or unobservable actions of the left operand to be performed.
To axiomatize the behavior of a node considering the input-enabledness feature, we need to find the messages that it cannot currently respond to and then add a summand which receives those message without processing them. To this aim, axiom Dep0 expresses the behavior of [[t]]ℓ as a recursive specification which drops messages that it does not handle with the help of the auxiliary function Message(t,S), and the behavior of t with the help of the local deployment operator ℓ:Q:t. The function Message(t,S) returns the set of messages that can be currently processed by t and is defined using structural induction:
[TABLE]
where S keeps track of process names whose right-hand definitions have been examined. We remark that Dep0 extends the deployment behavior of the lossy setting with the input enabledness feature with the help of operator ℓ:Q:t. The axioms Dep1−7 specify the behavior of the operator ℓ:t1:t2. Axiom Dep1 defines the interaction between the network and data link layers. The protocol send action (at the network layer) is transformed into its network version (at the data link layer). Axiom Dep2 indicates that when ℓ is connected to a sender (which is unknown yet), the receive action is successful and its behavior proceeds as [[t]]ℓ. Otherwise, the receive action is unsuccessful and its behavior is defined by t′. Axioms Dep3,4,5 express the effect of the local deployment on choice, deadlock, and process names, respectively while axioms Dep6,7 define its effect on the prefixed internal actions and sense operator, respectively.
The behavior of the topology restriction operator is defined by the axioms TRes1−5 in Table 3. Axiom TRes1 considers the restrictions of C1 by integrating its restrictions with C2 in the computed network term (C2,η).t if C1∪C2 is well-formed. Axiom TRes2 defines that topology restriction can be distributed over the choice operator. Axiom TRes3 expresses that the topology restriction operator can be moved inside and outside of a recursion operator. Axioms TRes4,5 explain that the topology restriction operator has no effect on a process name and deadlock, respectively.
For instance, the behavior of the MANET [[P]]A, where P=defsense(B,snd(dataB).P,0), Msg={dataB}, is simplified as:
[TABLE]
The behavior of [[Q]]B, where Q=defrcv(dataB).deliver.Q, is equated to:
[TABLE]
The axioms of hiding and encapsulation are given in Table
4. Axiom T1 accumulates the network constraints that constitute a partitioning while T2 removes a τ action which preserves the behavior of a network after some
topology changes. The remaining axioms in this table are similar to the lossy setting.
Axioms for process names are given in Table 5. Unfold and Fold express existence and uniqueness of a
solution for the equation A=deft, which correspond to
Milner’s standard axioms, and the Recursive Definition
Principle (RDP) and Recursive Specification
Principle (RSP) in ACP. Unfold states that each
recursive operator has a solution (whether it is guarded or not),
while Fold states that each guarded recursive operator has
at most one solution.
The behavior of τMsg(∂Msg([[P]]A∥[[Q]]B)) by using the axioms of Table 5 is expressed by:
[TABLE]
which explains that in case A is connected to B, each sending of dataB is followed by the internal action deliver
It is not hard to see that the axioms of Table 3, Table 4 and Table 5 provide a sound axiomatization of RCNT. This can be checked by verifying soundness for each axiom individually.
Theorem 6.1
The axiomatization is sound,
i.e. for all closed RCNT terms
t1 and t2, if
t1=t2 then t1≃rbt2.
Our axiomatization is also ground-complete for terms with a finite-state CLTS, but not for infinite-state CLTSs. For example,
recW⋅({},nsnd(req(A),A)).W∥∑lx:Loc({?⇝B},nrcv(req(lx))).W produces
an infinite-state CLTS, since at each recursive call a
new parallel operator is generated. Its equality to recH⋅({},nsnd(req(A),A)).H cannot be proved by our axiomatization.
Theorem 6.2
The axiomatization is ground-complete, i.e., for all closed finite-state reliable computed
network terms t1 and t2,
t1≃rbt2 implies t1=t2.
See sections C and D for the proofs of theorems 6.1 and 6.2, respectively.
7 Case Study
In MANETs, nodes communicate through others via a multi-hop communication. Hence, nodes act as routers to make the communication possible among not directly connected nodes. We illustrate the applicability of our axioms in the analysis of MANET protocols through a simple routing protocol inspired by the AODV protocol.
7.1 Protocol Specification
The protocol consists of three processes P, M, and Q, each specifying the behavior of a node as the source (that finds a route to a specific destination), middle node (that relays messages from the source to the destination), and destination. The description of these process are given in Figure 1.
Process P, deployed at the address A, uses the neighbor discovery service of the data link layer to examine if it has a direct link to the destination with the address B. If it is connected, then it sends its data directly by broadcasting the message dataB; otherwise, it initiates the route discovery procedure by sending the message req, then behaving as P1. This process waits until it receives a reply from a middle name with the address C or B. In the former case, it behaves as P2 which indicates that A sends it data through C as long as C is connected to A. In the latter case, it behaves as P which indicates that A sends it data as long as B is directly connected to A.
Process M relays req messages to find a route to B and then behaves as M1. This process waits until it receives a reply. To model waits with a timeout, it non-deterministically sends a request again. Upon receiving a reply from C it behaves as M2, indicating that it relays data messages of A as long as it has a link to C. Finally, process Q sends a reply upon receiving a request message and receives data messages.
To simplify the route maintenance procedure of AODV, the middle node takes advantage of the sensing operator when it behaves as M2. Whenever it finds out that it has no link to C, it sends an error message to its upstream node, i.e., A, to inform it that its route to B through C is not valid. Afterwards, they both execute the route discovery procedure by sending a request message.
The network with the three nodes of a source, middle, and destination is specified by
[TABLE]
Analyzing (νA)(νB)(νC)N, whose network addresses have been abstracted away, reveals that it is rooted branching bisimilar to recX⋅τ.deliver.X+τ.0. Thus, possibly a deadlock occurs where data is not delivered to B. Such behavior may be the result of a conceptual mistake in the protocol design or lossy communication between A and B. However, the latter one does not exist in our reliable setting. We propose a technique in Section 7.2 to discover only those faulty behaviors that are due to an incorrect protocol design.
The network ∂Msg([[P]]A∥[[M]]C∥[[Q]]B) can be simplified as:
[TABLE]
Next, we simplify ∂Msg([[P1]]A∥[[snd(req).M1]]C∥[[Q]]B) as
[TABLE]
Now, we continue by extending ∂Msg([[P1]]A∥[[M1]]C∥[[snd(repB).Q]]B):
[TABLE]
By simplifying the term ∂Msg([[P]]A∥[[snd(repC).M2]]C∥[[Q]]B), which indicates that A and C have found a direct route to B, we reach ∂Msg([[P]]A∥[[M2]]C∥[[Q]]B):
[TABLE]
By extending ∂Msg([[P]]A∥[[M2]]C∥[[Q]]B), we have:
The following scenario, found by above equations, is valid for a topology in which A has only a multi-hop link to B via C, but B has a direct link to A:
[TABLE]
The reason is found in the specification of M2 which does not handle request messages, and hence, for such a topology no data will be received by B although there is a path form A to B and from B to A. Therefore, we revise M2 as:
[TABLE]
The path above also exists in the lossy setting, but with all disconnectivity pairs removed from the network constraints. However, an exhaustive and therefore expensive inspection of this path is needed to determine that it is due to a design error. The first transition carries the label ({A⇝B,A⇝C},nsnd(req,A)) in the reliable setting, meaning that B is not ready to receive, and the label ({A⇝C},nsnd(req,A)) in the lossy setting. The latter label indicates that either B was not ready to receive or it was not connected to A. So in the lossy setting one has to examine the origin state to find out if B had an enabled receive action or not. The concept of not being ready to receive is treated in the same way as a lossy communication. Since only the former may be due to a conceptual design in the protocol, finding design errors is not straightforward in the lossy setting. In general the lossy setting will produce a large number of possible error traces that all need to be examined exhaustively, while the reliable setting will produce no spurious error traces.
7.2 Protocol Analysis
The properties of wireless protocols, specially MANETs, tends to be weaker in comparison with wired protocols. For instance, the simple property of packet delivery from node A to B is specified as “if there is a path from A to B for a long enough period of time, any packet sent by A, will be received by B” [21]. The topology-dependent behavior of communication, and
consequently the need for multi-hop communication between nodes, make their properties preconditioned by the existence of some paths among nodes.
To investigate the topology-dependent properties of MANETs by equational reasoning, it is necessary to enrich our process theory RCNT to specify behaviors constrained by multi-hop constraints. To this aim, we extend the action prefix operator of RCNT with actions that are paired with multi-hop constraints, first introduced in [22] and here extended by negative multi-hop connectivity pairs. Viewing a network topology as a directed graph, a multi-hop
constraint is represented as a set of multi-hop (dis)connectivity pairs
⇢:Loc×Loc and ⇢:Loc×Loc. For instance, A⇢C
denotes there exists a multi-hop connection from A to C, and
consequently C can indirectly receive data from A. Let
M(Loc) denote the set of multi-hop constraints that
can be defined over network addresses in Loc, ranged over by
M. Term (M,ι).t, where ι∈IAct∪{τ}, denotes that the action ι is possible if the underlying topology satisfies the multi-hop network constraint M. Formally, a topology like γ satisfies the multi-hop network constraint M, denoted by γ⊨M iff for each
ℓ⇢ℓ′ in M, there is a multi-hop connection
from ℓ to ℓ′ in γ, and for each
ℓ⇢ℓ′ in M, there is no multi-hop connection
from ℓ to ℓ′ in γ. To define a well-formed RCNT term, the rule which restricts the application of the new prefixed-actions to sequential processes, is added to the previous ones. Furthermore, a term cannot have two summands such that one is prefixed by an action of the form (C,η) and the other by an action of the form (M,ι). So terms with an action of the form (M,ι) only contain action prefix (with multi-hop constraints), choice and recursion operators.
To reason about the correctness of a MANET protocol, its behavior can be abstractly specified by observable internal actions with the required conditions on the underlying topology, i.e., ι-actions with multi-hop constraints. Intuitively, each communication of a protocol implementation triggers an internal action. Such communications are abstracted away by τ-transitions. Therefore, we define a novel preorder relation to examine if a protocol refines its specification. To this aim, a sequence of τ-transitions is allowed to precede an action that is matched to an action of the specification, as long as the accumulated network constraints of the τ-transitions satisfy the multi-hop network constraint of the matched action. Hence our preorder relation is parametrized by a network constraint to reflect such accumulated network constraints.
To provide such a relation, we use the notation \ext@arrow0359\Rightarrowfill@C which is the reflexive and transitive closure of τ-relations while their network constraints are accumulated:
•
t\ext@arrow0359\Rightarrowfill@{}t;
•
if t(C,τ)(C,τ)t′ for some arbitrary network constraint C and
t′\ext@arrow0359\Rightarrowfill@C′t′′, then t\ext@arrow0359\Rightarrowfill@C′∪Ct′′, where C′∪C is well-formed.
Furthermore, the network constraint C satisfies the multi-hop constraint C, denoted by C⊨M iff
∃γ∈Γ(C)(γ⊨M). We remark that a network constraint like {A⇝B} may satisfy both {A⇢B} and {A⇢B}, but {A⇝B} only satisfies {A⇢B}.
Definition 7.1
A binary relation RC on RCNT terms is a refinement relation if tRCs implies:
•
if t(C′,η)(C′,η)t′, where C∪C′∈Cv(Loc), then
–
η=τ* and t′RC∪C′s with C∪C′⊨M, or*
–
there is an s′ such that s(C,η)(C,η)s′, and t′RC∪C′s′, and C∪C′⊨M, or
–
η=ι* for some ι∈IAct∪{τ} and there is an s′ such that s(M,ι)(M,ι)s′ with t′RC∪C′s′;*
•
if s(M,ι)(M,ι)s′, then there are t′′ and t′ such that t\ext@arrow0359\Rightarrowfill@C′t′′(C′′,ι)(C′′,ι)t′ with t′′RC∪C′s and t′RC∪C′∪C′′s′;
•
if s(C,η)(C,η)s′, then there is a t′ such that t(C′,η)(C′,η)t′ with t′RC∪C′s′.
The protocol t refines the specification s, denoted by t⊑s, if tR{}s for some refinement relation R{}.
Theorem 7.2
Refinement is a preorder relation and has the precongruence property.
See Section E for its proof. To analyze the correctness of our simple routing protocol, we investigate if it has the packet delivery property. To this end, we verify whether τMsg(∂Msg([[P]]A∥[[M]]C∥[[Q]]B)) refines S, where S=def({A⇢B,B⇢A},deliver).S+({A⇢B},τ).0+({A⇢B,B⇢A},τ).0.
To this aim, we match all the resulting terms of τ-transitions to S as long as their accumulated network constraints satisfy {A⇢B,B⇢A}. If a τ-transition violates {A⇢B,B⇢A} but satisfies {A⇢B}, then it will be matched to the transition ({A⇢B},τ). Otherwise, it will be matched to the transition ({A⇢B,B⇢A},τ). Therefore, we exploit the provided equations together with the precongruence property of our refinement for the choice operator and the rules of Proposition 7.3.
Proposition 7.3
Suppose ι∈IAct. The following rules holds
[TABLE]
These rules correspond to the transfer conditions of Definition 7.1, and their proofs are discussed in Section E.
To prove the refinement relation 3, we use the Equation 2 to show that
[TABLE]
This proof process stops when we reach to the predicate C⊳t⊑(M,ι).s to prove for which either we have previously examined C′⊳t⊑(M,ι).s where C≼C′, or it holds trivially. For instance, the refinement relation (4) trivially holds as it can be proved with the help of our axiomatization, especially the rules Fold and TRes1,2, that {A⇝B,A⇝C,C⇝B}⊳τMsg(∂Msg([[P1]]A∥[[M1]]C∥[[Q]]B)) is the answer to the equation Q=def({A⇝B,A⇝C,C⇝B},τ).Q, and trivially
[TABLE]
So, it can be easily proved that τMsg(∂Msg([[P]]A∥[[M]]C∥[[Q]]B))⊑S
.
8 Related Work
Related calculi to ours are CBS# [13], CWS [32],
CMAN [14, 15], CMN [16] and its timed version [33], bKlaim [17], ω-calculus [18], SCWN [19], CSDT [20],
AWN [21] and its timed extension [34], and the broadcast psi-calculi
[35]. These approaches have already been compared in [24] with regard to modeling issues, such as topology and mobility, as well as behavioral congruence relations, in particular observables and distinguishing power. As all these approaches, except [32], focus on protocols above the data like layer, we investigate their capabilities to faithfully support the properties of wireless communication at this layer, i.e., being non-blocking and asynchronous. Furthermore, we compare our behavioral equivalence relation to those with a reliable setting.
All these approaches, except [5], provide an algebraic framework. Among them only [17] is asynchronous, centered around the tuple space paradigm; broadcast messages are output into the tuple spaces of neighboring nodes to the sending node.
The non-blocking property is a consequence of either nodes being input-enabled or the communication primitives being lossy. In the former case, the asynchronous property is achieved through abstract data specifications [36] in line with the approach from [37, 38], in which the sum operator plays a pivotal role. Each process is then parametrized by a variable of the queue type with a summand which receives all possible messages (if the queue is empty). Among these approaches, CMN, CMAN, ω-calculus, SCWN, and the broadcast psi-calculi are lossy.
To make a process input-enabled while communication is synchronous, three approaches are followed. In the first approach, followed by AWN, the semantics is equipped with a rule similar to our Rcv2 with a negative premise which expresses that if a node is not ready to receive, the message is simply ignored [21]. Due to our implicit modeling of topology, the negative premise of our rule is more complicated to characterize the unreadiness of nodes regarding the underlying topology. In the second approach, followed by CDST, counterparts for the rules Bro and Recv are defined with negative premises to cover cases when a process cannot participate in the communication message [20]. The third approach, provided by CSB#, eliminates negative premises, to remain within the de Simone format of structural operational semantics [21], in favor of actions which discard messages [13]. Therefore, the semantics is augmented by rules that trigger the ignore actions for any sending node, receiving nodes for disconnected locations, and deadlock. Furthermore, the rules Bro and Recv are modified to cover cases when a process ignores a message.
Among the reliable settings, only CDST provides a behavioral equivalence relation, based on the notion of observational congruence: the receive and send actions are observable while transitions changing the underlying topology are treated as unobservable. However, due to implicit modeling of topology and mobility, our behavioral equivalence relation has been parametrized with network constraints while it considers the branching structure of MANETs.
9 Conclusion
We introduced the reliable framework RRBPT, suitable to specify and verify MANETs, with the aim to catch errors in design decisions. We discussed the required changes at the semantic model by extending the network constraints with negative connectivity links. Furthermore, we revised the equivalence relation of the lossy setting to preserve required behavior in the reliable framework. Then we demonstrated which axioms should be added to /removed from the reliable setting. We provided an analysis approach at the syntactic level, exploiting a precongruence relation and our axiomatization. We applied our analysis approach to a simple routing protocol to prove that it correctly finds routes among connected nodes.
Appendix A Branching Reliable Computed Network Bisimilarity is an Equivalence
To prove that branching reliable computed network bisimilarity
is an equivalence, we exploit semi-branching reliable computed network
bisimilarity, following [41].
Definition A.1
A binary relation
R on computed network terms is a semi-branching reliable computed
network simulation, if t1Rt2
implies whenever t1(C,η)(C,η)t1′:
•
either η=τ and there is a t2′ such that t2⇒t2′ with t1Rt2′ and t1′Rt2′; or
•
there are s1′′,…,sk′′ and s1′,…,sk′ for some k>0
such that ∀i≤k(t2⇒si′′⟨(Ci,η)⟩⟨(Ci,η)⟩si′, with t1Rsi′′ and t1′Rsi′), and ⟨C1⟩,…,⟨Ck⟩ constitute a partitioning of ⟨C⟩.
R* is a semi-branching reliable computed network bisimulation if R and R−1
are semi-branching reliable computed network simulations. Computed networks
t1 and t2 are semi-branching reliable computed
network bisimilar if t1Rt2, for
some semi-branching reliable computed network bisimulation relation
R.*
Lemma A.2
Let t1 and t2 be computed network terms,
and R a semi-branching reliable computed network bisimulation
such that t1Rt2.
•
If t1⇒t1′ then ∃t2′⋅t2⇒t2′∧t1′Rt2′
•
If t2⇒t2′ then ∃t1′⋅t1⇒t1′∧t1′Rt2′
Proof A.3
We only give the proof of the first property. The second
property can be proved in a similar fashion. The proof is by
induction on the number of ⇒ steps from t1
to t1′:
•
Base: Assume that the number of steps equals zero. Then
t1 and t1′ must be equal. Since
t1Rt2 and
t2⇒t2, the property is satisfied.
•
Induction step: Assume t1⇒t1′ in n steps, for some n≥1. Then there is t1′′ such that t1⇒t1′′
in n−1⇒ steps, and t1′′(C,τ)(C,τ)t1′. By the induction hypothesis, there is a t2′′ such that t2⇒t2′′ and t1′′Rt2′′.
Since t1′′(C,τ)(C,τ)t1′ and R is a semi-branching reliable computed network bisimulation,
there are two cases to consider:
–
there is a t2′ such that
t2′′⇒t2′,
t1′′Rt2′, and t1′Rt2′. So t2⇒t2′ such that t1′Rt2′.
–
or there are s1′′′,…,sk′′′ and s1′,…,sk′ for some k>0
such that ∀i≤k(t2′′⇒si′′′(Ci,τ)(Ci,τ)si′,
with t1′′Rsi′′′ and t1′Rsi′), and C1,…,Ck constitute a partitioning of C. By definition, si′′′(Ci,τ)(Ci,τ)si′ yields si′′′⇒si′. Consequently for any arbitrary i≤k, t2⇒si′ such that t1′Rsi′.
Proposition A.4
The relation composition of two semi-branching reliable computed network
bisimulations is again a semi-branching reliable computed network
bisimulation.
Proof A.5
Let R1 and R2 be
semi-branching reliable computed network bisimulations with t1R1t2 and t2R2t3. Let t1(C,η)(C,η)t1′.
It must be shown that
•
either η=τ and there is a t3′ such that t3⇒t3′ with t1R1∘R2t3′ and t1′R1∘R2t3′; or
•
∃s1′,…,sk′,s1′′,…,sk′′∀i≤k(t3⇒si′′⟨(Ci,η)⟩⟨(Ci,η)⟩si′∧t1R1∘R2si′′∧t1′R1∘R2si′), where ⟨C1⟩,…,⟨Ck⟩ constitute a partitioning of ⟨C⟩.
Since t1R1t2, two cases can be considered:
•
η=τ* and there is a t2′ such that t2⇒t2′ with t1R1t2′ and t1′R1t2′. Lemma A.2 yields that there is a t3′ that t3⇒t3′ with t2′R2t3′. It immediately follows that t1R1∘R2t3′ and t1′R1∘R2t3′.*
•
there exist
s1∗∗,…sj∗∗, s1∗…sj∗ for some j>0 such that
∀i≤j(t2⇒si∗∗⟨(Ci,η)⟩⟨(Ci,η)⟩si∗, t1R1si∗∗,
t1′R1si∗), and ⟨C1⟩,…,⟨Cj⟩ is a partitioning of ⟨C⟩. Since t2R2t3 and t2⇒si∗∗, Lemma A.2 yields that there are
s1′′′,…,sj′′′ such that ∀i≤j(t3⇒si′′′∧si∗∗R2si′′′). Two cases can be distinguished:
–
either η=τ and for some i≤j, si∗∗(Ci,τ)(Ci,τ)si∗ implies there is an si′′ such that si′′′⇒si′′ with si∗∗R2si′′ and si∗R2si′′. It follows immediately that there is an si′′ such that t3⇒si′′ with t1R1∘R2si′′ and t1′R1∘R2si′′; or
–
for all i≤j, si∗∗⟨(Ci,η)⟩⟨(Ci,η)⟩si∗ implies there are si1′′,…,siki′′ and si1′,…,siki′ for some ki>0 such that ∀o≤ki(si′′⇒sio′′⟨(Cio,η)⟩⟨(Cio,η)⟩sio′,
si∗∗R2sio′′, si∗R2sio′), and ⟨Ci1⟩,…,⟨Ciki⟩ is a partitioning of ⟨Ci⟩. Since t3⇒si′′, we have ∀i≤j,∀o≤ki(t3⇒sio′′⟨(Cio,η)⟩⟨(Cio,η)⟩sio′ with t1R1∘R2sio′′, t1′R1∘R2sio′), and {⟨Cio⟩∣i≤j,o<ki} is a partitioning of ⟨C⟩.
Corollary A.6
Semi-branching reliable computed network bisimilarity is an equivalence relation.
It is not hard to see that the union of semi-branching reliable computed network bisimulations is again a semi-branching reliable computed network bisimulation.
Proposition A.7
The largest semi-branching reliable computed network bisimulation is a branching reliable computed network bisimulation.
Proof A.8
Suppose R is the largest semi-branching reliable
computed network bisimulation for some given CLTS. Let t1Rt2,
t2⇒t2′, t1Rt2′ and t1′Rt2′. We show that
R′=R∪{(t1′,t2)}
is a semi-branching reliable computed network bisimulation.
If t1′(C,η)(C,η)t1′′, then it follows from (t1′,t2′)∈R that
•
either η=τ and there is a t2′′ such that t2′⇒t2′′ with t1′Rt2′′ and t1′′Rt2′′. Finally t2⇒t2′ results t1′R′t2′′ and t1′′R′t2′′; or
•
there are s1′′′,…,sk′′′ and s1′′,…,sk′′ for some k>0 such that
∀i≤k(t2′⇒si′′′⟨(Ci,η)⟩⟨(Ci,η)⟩si′′ with (t1′,si′′′),(t1′′,si′′)∈R) and ⟨C1⟩,…,⟨Ck⟩ is a partitioning of ⟨C⟩. And t2⇒t2′ yields ∀i≤k(t2⇒si′′′⟨(Ci,η)⟩⟨(Ci,η)⟩si′′, with (t1′,si′′′),(t1′′,si′′)∈R′).
2. 2.
If t2(C,η)(C,η)t2′′,
then it follows from (t1,t2)∈R that
•
either η=τ, and there is a t1′′ such that t1⇒t1′′ with t1′′Rt2 and t1′′Rt2′′. Furthermore, (t1,t2′)∈R, t1⇒t1′′, and Lemma A.2 imply there is a t2′′′ such that t2′⇒t2′′′ with (t1′′,t2′′′)∈R. Similarly (t1′,t2′)∈R, t2′⇒t2′′′, and Lemma A.2 imply there is a t1′′′ such that t1′⇒t1′′′ with (t1′′′,t2′′′)∈R. From (t1′′′,t2′′′)∈R, (t2′′′,t1′′)∈R−1, and (t1′′,t2)∈R, we conclude (t1′′′,t2)∈R∘R−1∘R. And from (t1′′′,t2′′′)∈R, (t2′′′,t1′′)∈R−1, and (t1′′,t2′′)∈R, we conclude (t1′′′,t2′′)∈R∘R−1∘R.
•
or there are s11′′′,…,s1k′′′
and s11′′,…,s1k′′ for some k>0 such that ∀i≤k(t1⇒s1i′′′⟨(Ci,η)⟩⟨(Ci,η)⟩s1i′′
with (s1i′′′,t2),(s1i′′,t2′′)∈R) and ⟨C1⟩,…,⟨Ck⟩ is a partitioning of ⟨C⟩. Since (t1,t2′)∈R and t1⇒s1i′′′, by Lemma A.2,
there are s21′′′,…,s2k′′′ such that
∀i≤k(t2′⇒s2i′′′ and (s1i′′′,s2i′′′)∈R). Since
s1i′′′⟨(Ci,η)⟩⟨(Ci,η)⟩s1i′′,
there are s2i1∗∗,…,s2iki∗∗ and
s2i1∗,…,s2iki∗ for some ki>0 such that
∀o≤ki(s2i′′′⇒s2io∗∗⟨(Cio,η)⟩⟨(Cio,η)⟩s2io∗ with (s1i′′′,s2io∗∗),(s1i′′,s2io∗)∈R) and ⟨Ci1⟩,…,⟨Ciki⟩ is a partitioning of ⟨Ci⟩. Since t2′⇒s2i′′′ and s2i′′′⇒s2io∗∗, we have
∀i≤k,o≤ki(t2′⇒s2io∗∗).
By assumption, (t1′,t2′)∈R, so by Lemma A.2 there are s11∗∗,…,s1K∗∗, where K=∑i=1kki, such that
∀z≤K(t1′⇒s1z∗∗ and (s1z∗∗,s2io∗∗)∈R, where z=(∑j=1i−1kj)+o). Since s2io∗∗⟨(Cio,η)⟩⟨(Cio,η)⟩s2io∗, there are
s1z1∗∗∗,…,s1zkz′∗∗∗ and s1z1′,…,s1zkz′′ for some kz′>0
such that ∀j≤kz′(s1z∗∗⇒s1zj∗∗∗⟨(Cioj,η)⟩⟨(Cioj,η)⟩s1zj′
with (s1zj∗∗∗,s2io∗∗),(s1zj′,s2io∗)∈R) and ⟨Cio1⟩,…,⟨Ciokz′⟩ is a partitioning of ⟨Cio⟩. And t1′⇒s1z∗∗ yields ∀i≤k,o≤ki,j≤kz′(t1′⇒s1zj∗∗∗⟨(Cioj,η)⟩⟨(Cioj,η)⟩s1zj′ with
[TABLE]
where z=(∑l=1i−1kl)+o), and {⟨Cioj⟩∣i≤k,o≤ki,j≤kz′} is a partitioning of ⟨C⟩.
*By Proposition A.4, R∘R−1∘R is a semi-branching reliable
computed network bisimulation. Since R is the largest semi-branching reliable computed network bisimulation, and clearly R⊆R∘R−1∘R, we have R=R∘R−1∘R.
*
So R′ is a semi-branching reliable computed network bisimulation. Since R is the largest semi-branching reliable
computed network bisimulation, R′=R.
We will now prove that R is a branching reliable computed network
bisimulation. Let t1Rt2, and
t1(C,η)(C,η)t1′. We only consider the
case when η=τ, because for other cases, the transfer condition of
Definition 5.3 and Definition A.1 are the
same.
Two cases can be
distinguished:
There is a t2′ such that t2⇒t2′ with t1Rt2′ and t1′Rt2′: we proved above that t1′Rt2. This agrees with the first case of
Definition 5.3.
2. 2.
There are s1′′,…,sk′′ and s1′,…,sk′ for some k>0 such that
∀i≤k(t2⇒si′′⟨(Ci,τ)⟩⟨(Ci,τ)⟩si′ with
t1Rsi′′ and t1′Rsi′) and ⟨C1⟩,…,⟨Ck⟩ constitute a partitioning of ⟨C⟩. This agrees with
the second case of Definition 5.1.
Consequently R is a branching reliable computed network
bisimulation.
Since any branching reliable computed network bisimulation is a
semi-branching reliable computed network bisimulation, this yields the
following corollary.
Corollary A.9
Two computed network terms are related by a branching reliable computed
network bisimulation if and only if they are related by a
semi-branching reliable computed network bisimulation.
Corollary A.10
Branching reliable computed network bisimilarity is an equivalence relation.
Corollary A.11
Rooted branching reliable computed network bisimilarity is an equivalence relation.
Proof A.12
It is easy to show that rooted branching reliable computed network
bisimilarity is reflexive and symmetric. To conclude the proof, we
show that rooted branching reliable computed network bisimilarity is
transitive. Let t1≃rbrt2 and
t2≃rbrt3. Since
t1≃rbrt2, if
t1(C,η)(C,η)t1′, then there is
t2′ such that
t2⟨(C,η)⟩⟨(C,η)⟩t2′ and
t1′≃brt2′. Since
t2≃rbrt3, there is a t3′
such that t3⟨(C,η)⟩⟨(C,η)⟩t3′ and
t2′≃brt3′. Equivalence of branching reliable
computed network bisimilarity yields
t3⟨(C,η)⟩⟨(C,η)⟩t3′ with
t1′≃brt3′. The same argumentation holds
when t3(C,η)(C,η)t3′. Consequently
the transfer conditions of Definition 5.5 holds and
t1≃rbrt3.
Appendix B Rooted Branching Reliable Computed Network Bisimilarity is a Congruence
Theorem B.1
Rooted branching reliable computed network bisimilarity is a congruence for
terms with
respect to RCNT operators.
Clearly, if t1≃rbrt2 then
t1≃brt2 is witnessed by the following
branching reliable computed network bisimulation relation:
[TABLE]
We prove the cases
1, 2, 4, 7, 10,
11, and 13 since the proof of the cases 3 and 6 are similar to the case 2, the case 5 is
similar to the case 1,
the cases 8 and 9 are
similar to the case 10,
and the case 12 is similar to the
case 11.
Case 1*. The first transitions of [[α.t1]]ℓ and [[α.t2]]ℓ are the same with application of the rule Snd (if α is a send action), Rcv1 (if α is a receive action), or Rcv2 (for receiving *(C,nrcv(m))which are not derivable from Rcv1), and
by assumption [[t1]]ℓ≃rbr[[t1]]ℓ implies [[t1]]ℓ≃br[[t1]]ℓ. Thus the transfer conditions
of Definition 5.5 hold.
Case 2. Every transition [[t1+t1′]]ℓ(C,η)(C,η)t owes to [[t1]]ℓ(C,η)(C,η)t or [[t1′]]ℓ(C,η)(C,η)t by application of Choice, or is implied by application of Rcv2, i.e., [[t1+t1′]]ℓ(C,nrcv(m))(C,nrcv(m))[[t1+t1′]]ℓ iff there exists no [[t1+t1′]]ℓ(C′,nrcv(m))(C′,nrcv(m))t for some t such that C≼C′. For the former case, [[t1]]ℓ≃rbr[[t2]]ℓ and [[t1′]]ℓ≃rbr[[t2′]]ℓ imply there is a t′
such that [[t2]]ℓ(⟨C,η)⟩(⟨C,η)⟩t′ or [[t2′]]ℓ⟨(C,η)⟩⟨(C,η)⟩t′ and
t≃brt′. Thus [[t2+t2′]]ℓ⟨(C,η)⟩⟨(C,η)⟩t′ with
t≃brt′. For the latter case by Choice, there exists no [[t1]]ℓ(C′,nrcv(m))(C′,nrcv(m))t and [[t1′]]ℓ(C′,nrcv(m))(C′,nrcv(m))t for some t such that C≼C′. Thus by Rcv2, [[t1]]ℓ(C,nrcv(m))(C,nrcv(m))[[t1]]ℓ and [[t1′]]ℓ(C,nrcv(m))(C,nrcv(m))[[t1′]]ℓ. We remark that transitions derived by application of Rcv2 are those that cannot be derived from Rcv1. The greatest value of the network constraints of such transitions either have the disconnectivity pair in the form of ?⇝ℓ or have no connectivity pair in the form of ?⇝ℓ. This implies that such transitions can not be mimicked by application of Rcv1 (since it will add constraints of the form ?⇝ℓ) .
Therefore, [[t1]]ℓ≃rbr[[t2]]ℓ and [[t1′]]ℓ≃rbr[[t2′]]ℓ imply that [[t2]]ℓ(C,nrcv(m))(C,nrcv(m))[[t2]]ℓ and [[t2′]]ℓ(C,nrcv(m))(C,nrcv(m))[[t2′]]ℓ which are derived by application of Rcv2. Consequently [[t2+t2′]]ℓ(C,nrcv(m))(C,nrcv(m))[[t2+t2′]]ℓ.
Case 4*
Suppose that ℓ:t:t1(C∗,η)(C∗,η)t∗, then three cases can be distinguished:*
•
It owes to t1(C,snd(m))(C,snd(m))t1′ by application of Inter1′, and C∗=C[ℓ/?], η=nsnd(m,ℓ) and t∗=[[t1′]]ℓ. By application of Snd, it implies that [[t1]]ℓ(C[ℓ/?],nsnd(m,ℓ))(C[ℓ/?],nsnd(m,ℓ))[[t1′]]ℓ. By assumption [[t1]]ℓ≃rbr[[t2]]ℓ implies that [[t2]]ℓ(C[ℓ/?],nsnd(m,ℓ))(C[ℓ/?],nsnd(m,ℓ))[[t2′]]ℓ and [[t1′]]ℓ≃br[[t2′]]ℓ. Therefore, by rule Snd, t2(C,snd(m))(C,snd(m))t2′, and hence by application of Inter1′, ℓ:t:t2(C[ℓ/?],nsnd(m,ℓ))(C[ℓ/?],nsnd(m,ℓ))[[t2′]]ℓ.
•
It owes to t1(C,rcv(m))(C,rcv(m))t1′ by application of either Inter2′ or Inter3′. This case is proved with the same argumentation as the previous case.
•
If t1 and t2 are of the form sense(ℓ′,t1∗,t1∗∗) and sense(ℓ′,t2∗,t2∗∗) respectively, and the transition owes to either Sen3 or Sen4. Assume it was derived by Sen3, as the other case can be proved with the same argumentation. Thus, t1∗rcv(m)rcv(m), t1∗∗(C,rcv(m))(C,rcv(m))t1∗∗′, C∗={ℓ′⇝ℓ}∪C[ℓ/?], η=nrcv(m) and t∗=t. Therefore, by application of Rcv2, [[t1]]ℓ(C∗,nrcv(m))(C∗,nrcv(m))[[t1]]ℓ, and by application of Sen2 and Rcv1, [[t1]]ℓ({ℓ′⇝ℓ}∪C[ℓ/?],nrcv(m))({ℓ′⇝ℓ}∪C[ℓ/?],nrcv(m))[[t1∗∗′]]ℓ. By assumption [[t1]]ℓ≃rbr[[t2]]ℓ implies that [[t2]]ℓ(C∗,nrcv(m))(C∗,nrcv(m))[[t2]]ℓ and [[t2]]ℓ({ℓ′⇝ℓ}∪C[ℓ/?],nrcv(m))({ℓ′⇝ℓ}∪C[ℓ/?],nrcv(m))[[t2∗∗′]]ℓ where [[t1∗∗′]]ℓ≃br[[t2∗∗′]]ℓ. Thus, t2∗rcv(m)rcv(m), t2∗∗(C,rcv(m))(C,rcv(m))t2∗∗′ (as the only way to generate the pair ℓ′⇝ℓ is through the sense operator) and ℓ:t:t2(C∗,nrcv(m))(C∗,nrcv(m))t by application of Sen3.
Case 7. We prove that if
t1≃brt2 then
(νℓ)t1≃br(νℓ)t2. Let
t1≃brt2 be witnessed by the
branching reliable computed network bisimulation relation R.
We define
R′={((νℓ)t1′,(νℓ)t2′)∣(t1′,t2′)∈R}. We prove that R′ is a branching reliable computed
network bisimulation relation. Suppose
(νℓ)t1′(C′,η′)(C′,η′)(νℓ)t1′′
results from the application of Hid on
t1′(C,η)(C,η)t1′′. Since
(t1′,t2′)∈R, there are two
cases; in the first case η is a τ action and
(t1′′,t2′)∈R, consequently
((νℓ)t1′′,(νℓ)t2′)∈R′. In second case there are s1′′′,…sk′′′ and
s1′′,…,sk′′ for some k>0 such that ∀i≤k(t2′⇒si′′′⟨(Ci,η)⟩⟨(Ci,η)⟩si′′ with
(t1′,si′′′),(t1′′,si′′)∈R), and ⟨C1⟩…,⟨Ck⟩ is a partitioning of ⟨C⟩. By application of Hid,
∀i≤k((νℓ)t2′⇒(νℓ)si′′′ with
((νℓ)t1′,(νℓ)si′′′)∈R′). There are two cases to consider:
•
⟨(Ci,η)⟩=(Ci,η): Consequently
(νℓ)si′′′(Ci′,η′)(Ci′,η′)(νℓ)si′′ where (Ci′,η′)=(Ci,η)[?/ℓ].
•
⟨(Ci,η)⟩=(Ci,η): in this case η is of the form
nsnd(m,?), η′=η, and Ci′=Ci[?/ℓ]. If
⟨(Ci,η)⟩=(Ci,η)[ℓ/?] then ⟨(Ci,η)⟩[?/ℓ]=(Ci′,η′) holds, otherwise ⟨(Ci,η)⟩=(Ci,η)[ℓ′/?], where ℓ′=ℓ, and hence ⟨(Ci,η)⟩[?/ℓ] is a counterpart of (Ci′,η′). Consequently (νℓ)si′′′⟨(Ci′,η′)⟩⟨(Ci′,η′)⟩(νℓ)si′′.
Owing to the fact that a subset of C1[?/ℓ],…,Ck[?/ℓ] constitutes a partitioning of C[ℓ/?], and according to the discussion above, there are s1′′′,…,sj′′′ and
s1′′,…,sj′′ for some j≤k such that ∀i≤j,(νℓ)t2′⇒(νℓ)si′′′⟨(Ci′,η′)⟩⟨(Ci′,η′)⟩(νℓ)si′′ with
((νℓ)t1′,(νℓ)si′′′),((νℓ)t1′′,(νℓ)si′′)∈R′), and ⟨C1′⟩,…,⟨Cj′⟩ is a partitioning of ⟨C′⟩.
Likewise we can prove that t1≃rbrt2
implies (νℓ)t1≃rbr(νℓ)t2.
To this aim we examine the root condition in
Definition 5.5. Suppose
(νℓ)t1(C′,η′)(C′,η′)(νℓ)t1′.
With the same argument as above,
(νℓ)t2⟨(C′,η′)⟩⟨(C′,η′)⟩(νℓ)t2′.
Since t1′≃brt2′, we proved that
(νℓ)t1′≃br(νℓ)t2′.
Concluding (νℓ)t1≃rbr(νℓ)t2.
Case 10. From the three remaining
cases, we focus on the most challenging case, which is the
communication merge operator ∣, as the other operators are proved
in a similar way.
First we prove that if t1≃brt2, then t1∥t≃brt2∥t. Let t1≃brt2 be witnessed by the branching reliable computed network
bisimulation relation R. We define
\mathcal{R}^{\prime}=\{(t_{1}^{\prime}\parallel t^{\prime},t_{2}^{\prime}\parallel t^{\prime})\mid(t_{1}^{\prime},t_{2}^{\prime})\in\mathcal{R},\mbox{
t^{\prime} any computed network term}\}. We prove that
R′ is a branching reliable computed network bisimulation
relation. Suppose t1′∥t(C∗,η)(C∗,η)t∗. There are
several cases to consider:
•
Suppose η is of the form nsnd(m,ℓ). First let it be performed by t1′, and t participated in the communication. That is, t1′(C1,nsnd(m,ℓ))(C1,nsnd(m,ℓ))t1′′ and t(C,nrcv(m))(C,nrcv(m))t′ give rise to the transition t1′∥t(C1∪C[ℓ/?],nsnd(m,ℓ))(C1∪C[ℓ/?],nsnd(m,ℓ))t1′′∥t′. As (t1′,t2′)∈R and
t1′(C1,nsnd(m,ℓ))(C1,nsnd(m,ℓ))t1′′, there
are s1′′′,…,sk′′′ and s1′′,…,sk′′ for some k>0 such that ∀i≤k(t2′⇒si′′′(C1i[ℓ′/ℓ],nsnd(m,ℓ′))(C1i[ℓ′/ℓ],nsnd(m,ℓ′))si′′,
where (ℓ=?∨ℓ=ℓ′), with (t1′,si′′′),(t1′′,si′′)∈R), and C11[ℓ′/ℓ],…,C1k[ℓ′/ℓ] is a partitioning of C1[ℓ′/ℓ]. Hence ∀i≤k(t2′∥t⇒si′′′∥t((C1i[ℓ′/ℓ]∪C)[ℓ′/?],nsnd(m,ℓ′))((C1i[ℓ′/ℓ]∪C)[ℓ′/?],nsnd(m,ℓ′))si′′∥t′ with (t1′∥t,si′′′∥t),(t1′′∥t′,si′′∥t′)∈R′), and (C11[ℓ′/ℓ]∪C)[ℓ′/?],…,(C1k[ℓ′/ℓ]∪C)[ℓ′/?] is a partitioning of (C1[ℓ′/ℓ]∪C)[ℓ′/?].
Now suppose that the send action was performed by t, and t1′ participated in the communication. That is, t1′(C1,nrcv(m))(C1,nrcv(m))t1′′ and t(C,nsnd(m,ℓ))(C,nsnd(m,ℓ))t′
give rise to the transition t1′∥t(C1∪C[ℓ/?],nsnd(m,ℓ))(C1∪C[ℓ/?],nsnd(m,ℓ))t1′′∥t′. Since (t1′,t2′)∈R and t1′(C1,nrcv(m))(C1,nrcv(m))t1′′, there are s1′′′,…,sk′′′ and s1′′,…,sk′′ for some k>0
such that
∀i≤k(t2′⇒si′′′(C1i,nrcv(m))(C1i,nrcv(m))si′′ with (t1′,si′′′),(t1′′,si′′)∈R), and C11,…,C1k is a partitioning of C1. Therefore, ∀i≤k(t2′∥t⇒si′′′∥t(C1i∪C[ℓ/?],nsnd(m,ℓ))(C1i∪C[ℓ/?],nsnd(m,ℓ))si′′∥t′, and (t1′∥t,si′′′∥t),(t1′′∥t′,si′′∥t′)∈R′) and C11∪C[ℓ/?],…,C1k∪C[ℓ/?] constitute a partitioning of C1∪C[ℓ/?].
•
The case where η is a receive action is proved in a similar way to the previous case.
•
Suppose η is a τ action. Assume it originates from t1 by application of Par. Thus t1′(C,τ)(C,τ)t1′′ and (t1′,t2′)∈R implies: either (t1′′,t2′)∈R and consequently (t1′′∥t,t2′∥t)∈R′, or there are s1′′′,…,sk′′′ and s1′′,…,sk′′ for some k>0
such that
∀i≤k(t2′⇒si′′′(Ci,τ)(Ci,τ)si′′ with (t1′,si′′′),(t1′′,si′′)∈R), and C1,…,Ck constitute a partitioning of C. Therefore, ∀i≤k(t2′∥t⇒si′′′∥t(Ci,τ)(Ci,τ)si′′∥t′, and (t1′∥t,si′′′∥t),(t1′′∥t′,si′′∥t′)∈R′). The case when t(C,τ)(C,τ)t′ implies t1′∥t(C,τ)(C,τ)t1′∥t′ by application of Par is straightforward.
•
The case when η is an internal action is easy to prove (similar to the second case of the previous case).
Likewise we can prove that t1≃rbrt2
implies
t∥t1≃rbrt∥t2.
Now let t1≃rbrt2. To prove
t1∣t≃rbrt2∣t,
we examine the root condition from Definition 5.5.
Suppose
t1∣t(C∗,nsnd(m,ℓ))(C∗,nsnd(m,ℓ))t∗. There are two cases to consider:
•
This send action was performed by t1 at node ℓ, and t participated in the communication. That is, t1(C1,nsnd(m,ℓ))(C1,nsnd(m,ℓ))t1′ and t(C,nrcv(m))(C,nrcv(m))t′, so that t1∣t(C1∪C[ℓ/?],nsnd(m,ℓ))(C1∪C[ℓ/?],nsnd(m,ℓ))t1′∥t′. Since t1≃rbrt2, there is a t2′ such that t2(C1,nsnd(m,ℓ′))(C1,nsnd(m,ℓ′))t2′ with (ℓ=?∨ℓ=ℓ′) and t1′≃brt2′. Then t2∣t(C1∪C[ℓ′/?],nsnd(m,ℓ))(C1∪C[ℓ′/?],nsnd(m,ℓ))t2′∥t′. Since t1′≃brt2′, we proved that t1′∥t′≃brt2′∥t′.
•
The send action was performed by t at node ℓ, and t1 participated in the communication. That is, t1(C1,nrcv(m))(C1,nrcv(m))t1′ and t(C,nsnd(m,ℓ))(C,nsnd(m,ℓ))t′, so that t1∣t(C1∪C[ℓ/?],nsnd(m,ℓ))(C1∪C[ℓ/?],nsnd(m,ℓ))t1′∥t′. Since t1≃rbrt2, there is a t2′ such that t2(C1,nrcv(m))(C1,nrcv(m))t2′ with t1′≃brt2′. Then t2∣t(C1∪C[ℓ/?],nsnd(m,ℓ))(C1∪C[ℓ/?],nsnd(m,ℓ))t2′∥t′. Since
t1′≃brt2′, we have
t1′∥t′≃brt2′∥t′.
Finally, the case where t1∣t(C∗,nrcv(m))(C∗,nrcv(m))t∗ can be easily dealt with. This receive action was performed by both t1 and t.
Concluding, t1∣t≃rbrt2∣t. Likewise it can be
argued that t∣t1≃rbrt∣t2.
Case 11. We prove that if
t1≃brt2, then
∂M(t1)≃br∂M(t2). Let
t1≃brt2 be witnessed by the
branching reliable computed network bisimulation relation R. We define
R′={(∂M(t1′),∂M(t2′))∣(t1′,t2′)∈R}. We prove that R′ is a branching reliable computed
network bisimulation relation. Suppose that
∂M(t1′)(C,η)(C,η)∂M(t1′′)
results from the application of Encap on
t1′(C,η)(C,η)t1′′ such that η=nrcv(m)∨isTypem(m)=F. Since
(t1′,t2′)∈R, two cases can be considered: either η is a τ action and (t1′′,t2′)∈R, or there are
s1′′′,…,sk′′′ and s1′′,…,sk′′ for some k>0 such that
∀i≤k(t2′⇒si′′′⟨(Ci,η)⟩⟨(Ci,η)⟩si′′ with
(t1′,si′′′),(t1′′,si′′)∈R) and ⟨C1⟩,…,⟨Ck⟩ is a partitioning of ⟨C⟩. In the former case, (∂M(t1′′),∂M(t2′))∈R′. In the latter case, by application of Par and Encap,
∀i≤k(∂M(t2′)⇒∂M(si′′′)⟨(Ci,η)⟩⟨(Ci,η)⟩∂M(t2′′) with
(∂M(t1′),∂M(si′′′)),(∂M(t1′′),∂M(si′′))∈R′).
Likewise we can prove that t1≃rbrt2
implies ∂M(t1)≃rbr∂M(t2). To this aim we examine the root condition
in Definition 5.5. Suppose
∂M(t1)(C,η)(C,η)∂M(t1′).
With the same argument as above,
∂M(t2)⟨(C,η)⟩⟨(C,η)⟩∂M(t2′).
Since t1′≃brt2′, we proved that
∂M(t1′)≃br∂M(t2′).
Concluding ∂M(t1)≃rbr∂M(t2).
Case 13* Suppose that C⊳t1(C′∪C,η)(C′∪C,η)t1′ by application of TR since t1(C′,η)(C′,η)t1′. By assumption t1≃rbrt2 implies that t2(C′,η)(C′,η)t2′ and t1′≃brt2′. Therefore, by application of TR, C⊳t2(C′∪C,η)(C′∪C,η)t2′, and t1′≃brt2′ concludes that C⊳t1≃rbrC⊳t2.*
Appendix C Soundness of RCNT axiomatization
As two rooted branching computed network bisimilar terms are also rooted branching reliable computed network bisimilar, the soundness of axioms which are in common with the lossy setting are established [24]. Thus, to prove Theorem 6.1, it suffices to prove the soundness of each new axiom in comparison with the lossy setting, i.e., Dep0−7, TRes1−5, LM1,2′, and T1, modulo rooted branching reliable computed network bisimilarity.
We focus on the soundness of Dep0 and T1, as the soundness of the remaining axioms can be argued in a similar fashion. To prove Dep0, we show that both sides of the axiom satisfy the transfer conditions of Definition 5.5. Three cases can be distinguished. In following cases, for the sake of brevity, we write X for recQ⋅∑m′∈Message(t,∅)({},nrcv(m′)).Q+ℓ:Q:t:
Assume [[t]]ℓ(C[ℓ/?],nsnd(m,ℓ))(C[ℓ/?],nsnd(m,ℓ))[[t′]]ℓ since tC,snd(m)C,snd(m)t′ by application of Snd. By application of Inter1′, ℓ:X:t(C[ℓ/?],nsnd(m,ℓ))(C[ℓ/?],nsnd(m,ℓ))[[t′]]ℓ. Then, by application of Rec and Choice, X(C[ℓ/?],nsnd(m,ℓ))(C[ℓ/?],nsnd(m,ℓ))[[t′]]ℓ.
2. 2.
Assume [[t]]ℓ(C[ℓ/?]∪{?⇝ℓ},nrcv(m))(C[ℓ/?]∪{?⇝ℓ},nrcv(m))[[t′]]ℓ since tC,rcv(m)C,rcv(m)t′ by application of Rcv1. Thus by application of Inter2′, ℓ:X:t(C[ℓ/?]∪{?⇝ℓ},nrcv(m))(C[ℓ/?]∪{?⇝ℓ},nrcv(m))[[t′]]ℓ. Then, by application of Rec and Choice, X(C[ℓ/?]∪{?⇝ℓ},nrcv(m))(C[ℓ/?]∪{?⇝ℓ},nrcv(m))[[t′]]ℓ.
3. 3.
Assume [[t]]ℓ(C,nrcv(m))(C,nrcv(m))[[t]]ℓ since [[t]]ℓ(C,rcv(m)(C,rcv(m) and ∄C′([[t]]ℓ(C′,nrcv(m))(C′,nrcv(m))∧C≼C′) by application of Rcv2. Two cases can be distinguished:
•
Assume trcv(m)rcv(m), and consequently m∈Message(t). Thus, by application of Rec, Choice and Prefix, X(C,nrcv(m)(C,nrcv(m)X, where C={}.
•
t(C′′,rcv(m))(C′′,rcv(m))t′ for some t′, and consequently m∈Message(t). Thus, the assumption [[t]]ℓ(C,rcv(m)(C,rcv(m) and ∄C′([[t]]ℓ(C′,nrcv(m))(C′,nrcv(m))∧C≼C′) imply that ?⇝ℓ∈C while ?⇝ℓ∈C′′ due to application of Rcv1. Then by application of Inter3′, ℓ:X:t(C[ℓ/?]∪{?⇝ℓ},nrcv(m))(C[ℓ/?]∪{?⇝ℓ},nrcv(m))[[t′]]ℓ. Hence, X(C[ℓ/?]∪{?⇝ℓ},nrcv(m))(C[ℓ/?]∪{?⇝ℓ},nrcv(m))[[t′]]ℓ by application of Rec and Choice.
We focus on the soundness of T1. The only transition that the terms (C′,η).((C1,η).t+(C2,η).t+t′) and (C′,η).((C,η).t+t′) in T1 can do is (C′,η)(C′,η) and the resulting terms (C1,η).t+(C2,η).t+t′ and (C,η).t+t′ are branching reliable computed network bisimilar, witnessed by the relation R constructed as follows:
[TABLE]
The pair ((C1,η).t+(C2,η).t+t′,(C,η).t+t′) satisfies the transfer conditions of Definition 5.3. Because every initial transition that (C1,η).t+(C2,η).t+t′ can perform owing to t′, (C,η).t+t′ can perform too. If (C1,η).t+(C2,η).t+t′ can perform a (C1,η) or (C2,η)-transition, (C,η).t+t′ can also perform it by application of Exe. Vice versa, if (C,η).t+t′ can perform a (C,η)-transition, then as C1 and C2 form a partitioning of C, (C1,η).t+(C2,η).t+t′ can perform a corresponding (C1,η)- or (C2,η)-transition.
Appendix D Completeness of RCNT axiomatization
To define RCNT terms with a finite-state behavior, we borrow the syntactical restriction of [24] on recursive terms recA⋅t, following the approach of [30]. We consider so-called finite-state Reliable Computed Network Theory (RCNTf), obtained by
restricting recursive terms recA⋅t to those that of which the bound network names do not occur in the scope of parallel, communication merge, left merge, hide, encapsulation and abstraction operators in t.
We follow the corresponding proof of [24] to prove Theorem 6.2 by performing the following steps:
first we show that each RCNTf term can be turned into a
normal form consisting of only 0,(C,η).t′,t′+t′′ and
recA⋅t′, where A is
guarded in t′;
2. 2.
next we define recursive network specifications and prove that each guarded recursive network specification has a
unique solution;
3. 3.
finally we show that our axiomatization is ground-complete for normal forms, by showing that equivalent normal forms are
solutions for the same guarded recursive network specification.
Completeness of our axiomatization for all RCNTf terms
results from the steps 1 and 3. We only discuss the first step, as others are exactly the same as in the lossy setting.
Proposition D.1
Each closed term t of RCNTf whose network names do not occur in the scope of one of the operators \parallel,\,\begin{picture}(1.0,1.75)\put(0.0,0.0){\line(1,0){1.0}}\put(0.0,0.0){\line(0,1){1.75}}\put(0.45,0.0){\line(0,1){1.75}}\end{picture}\,,\mid,(\nu\ell),\tau_{M} or
∂M for some ℓ∈Loc and M⊆Msg, can be turned into a normal form.
We prove this by structural induction over the syntax of terms t (possibly open). The base cases of induction for t≡0 or t≡A are trivial because they are in normal form already. The inductive cases of the induction are the following ones:
•
if t≡[[0]]ℓ, then by application of Dep0,4 and Ch1 we have t=recQ⋅∑m′∈Msg({},nrcv(m′)).Q, which is in normal form.
•
if t≡[[α.t′]]ℓ or t≡[[t′+t′′]]ℓ or [[sense(ℓ′,t′,t′′)]]ℓ or [[A]]ℓ, then t can be
turned into a normal form by application of
axioms Dep0−5,6,7 and induction over [[t′]]ℓ and
[[t′′]]ℓ.
•
if t≡(C,η).t′ or t≡t′+t′′, then t can be
turned into normal form by induction over t′ and t′′.
•
the other cases can be treated in the same way as in [24].
We first prove Theorem 7.2 which indicates that the refinement relation is a preorder relation and has the precongruence property, and then we discuss the proof of Proposition 7.3.
We first show that the refinement relation is a preorder relation and then discuss its precongruence property. To prove that refinement is a preorder, we must show that it is reflexive and transitive. As it is trivial that Definition 7.1 is reflexive, we focus on its transitivity property.
Regrading the well-formedness conditions imposed on RCNT terms, the transitivity property of our refinement relation, i.e., t1⊑t2 and t2⊑s implies that t1⊑s, can be only proved when t1 and t2 have no prefixed-actions with a multi-hop network constraint. For such terms, Definition 7.1 enforces they mimic the behavior of each other by the first and third conditions. In other words, for reliable computed network terms with no prefixed-actions with multi-hop network constraints, refinement and strong bisimulation of [51] coincide.
Lemma E.1** **(Transitive property)
t1⊑t2* and t2⊑s implies that t1⊑s.*
Proof E.2
Assume sets of refinement relations RC1 and RC2 witnessing t1⊑t2 and t2⊑s, respectively. We construct a set of refinement relations RC′={(t1′,s′)∣(t2′,s′)∈RC2∧t1′RC1t2} for any well-formed network constraint C. We show that t1′RC′s′ satisfies the transfer conditions of Definition 7.1.
Assume t1′(C′,η)(C′,η)t1′′. By assumption t1′RC1t2′ implies that t2′(C′,η)(C′,η)t2′′ such that t1′′RC∪C′1t2′′. By the assumption t2′RC2s′, there are three cases to consider:
•
η=τ* and t2′′RC∪C′2s′ with C∪C′⊨M. Thus by construction, t1′′RC∪C′′s′.*
•
There is an s′′ such that s′(C,η)(C,η)s′′, and t2′′RC∪C′2s′′, and C∪C′⊨M. Thus by construction, t1′′RC∪C′′s′.
•
η=ι* for some ι∈IAct∪{τ} and there is an s′′ such that s′(M,ι)(M,ι)s′′ with t2′′RC∪C′2s′′. Thus by construction, t1′′RC∪C′′s′′.*
Assume s′(C′,η)(C′,η)s′′. Hence t2′RC∪C′2s′ implies that there is a t2′′ such that t2′(C′,η)(C′,η)t2′′ with t2′′RC∪C′2s′′. By assumption t1′RC1t2′ implies that t1′(C′,η)(C′,η)t1′′ such that t1′′RC∪C′1t2′′, and consequently t1′′RC∪C′′s′′.
Assume s(M,ι)(M,ι)s′. Therefore t2′RC∪C′2s′ implies that there are t2′′′ and t2′′ such that t2′\ext@arrow0359\Rightarrowfill@C′t2′′′(C′′,ι)(C′′,ι)t2′′ with t2′′′RC∪C′2s′ and t2′′RC∪C′∪C′′2s′′. As every transition of t2′ is mimicked by t1′, there are t1′′′ and t1′′ such that t1′\ext@arrow0359\Rightarrowfill@C′t1′′′(C′′,ι)(C′′,ι)t1′′ with t1′′′RC∪C′1t2′′′ and t1′′RC∪C′∪C′′1t2′′. Concluding, there are t1′′′ and t1′′ such that t1′\ext@arrow0359\Rightarrowfill@C′t1′′′(C′′,ι)(C′′,ι)t1′′ with t1′′′RC∪C′′s′ and t1′′RC∪C′∪C′′′s′′.
Theorem E.3
Refinement is a precongruence for terms with respect to the RCNT operators.
Proof E.4
Assume that t1⊑s1 and t2⊑s2. We first show that t1+t2⊑s1+s2.
There are sets of refinement relations RC1 and RC2 witnessing t1⊑s1 and t2⊑s2, respectively. We construct a set of refinement relations RC=RC1∪RC2∪{(t1′,s1+s2)∣t1′RC1s1}∪{(t2′,s1+s2)∣t2′RC2s2} for any well-formed network constraint C. We show that R{}={(t1+t2,s1+s2)}∪R{}1∪R{}2 satisfies the transfer conditions of Definition 7.1.
Assume t1+t2(C′,η)(C′,η)t1′ owing to t1(C′,η)(C′,η)t1′. By assumption t1R{}1s1. Three cases can be considered:
•
η=τ* and t1′RC∪C′s1, with C∪C′⊨M. Thus by construction t1′RC∪C′s1+s2.*
•
There is an s1′ such that s1(C,η)(C,η)s1′, and t1′RC∪C′1s1′, and C∪C′⊨M. Thus by sos rule Choice, there is an s1′ such that s1+s2(M,ι)(M,ι)s1′ and by construction t1′RC∪C′s1′.
•
η=ι* for some ι∈IAct∪{τ} and there is an s1′ such that s1(M,ι)(M,ι)s1′ with t1′RC∪C′1s1′. Thus by the sos rule Choice, there is an s1′ such that s1+s2(M,ι)(M,ι)s1′ and by construction t1′RC∪C′s1′.*
The same discussion holds if t1+t2(C′,η)(C′,η)t2′ owing to t2(C′,η)(C′,η)t2′.
Assume s1+s2(M,ι)(M,ι)s1′ owing to s1(M,ι)(M,ι)s1′. By assumption t1RC1s1 implies there are t1′′ and t1′ such that t1\ext@arrow0359\Rightarrowfill@C′t1′′(C′′,ι)(C′′,ι)t1′ with t1′′RC∪C′1s1 and t1′RC∪C′∪C′′1s1′. Consequently t1+t2\ext@arrow0359\Rightarrowfill@C′t1′′(C′′,ι)(C′′,ι)t1′ with t1′′RC∪C′s1+s2 and t1′RC∪C′∪C′′s1′. The same discussion holds when s1+s2(M,ι)(M,ι)s2′ owing to s2(M,ι)(M,ι)s2′.
Assume s1+s2(C,η)(C,η)s1′ owing to s1(C,η)(C,η)s1′. By assumption t1RC1s1 implies there is a t1′ such that t1(C′,η)(C′,η)t1′ with t1′RC∪C′1s1′. Hence, there is a t1′ such that t1+t2(C′,η)(C′,η)t1′ with t1′RC∪C′s1′.
The above discussions together yield t1+t2⊑s1+s2.
If s1 and s2 have no prefixed-action with a multi-hop network constraint, then we must show the following cases:
First we show that (C,τ).t⊑(M,ι).s⇒C⊳t⊑(M,ι).s∧C⊨M. The only transition (C,τ).t can make is (C,τ).t(C,τ)(C,τ)t. As ι=τ, according to Definition 7.1, tRC(M,ι).s. We construct R{}′=RC and show that it induces C⊳t⊑(M,ι).s. This is trivial as any transition C⊳t(C∪C′,η)(C∪C′,η)t′ is the result of t(C′,η)(C′,η)t′. The reverse of the rule can be argued in a similar fashion.
Now, we show that (C,ι).t⊑(M,ι).s⇒C⊳t⊑s. The only transition (C,ι).t can make is (C,ι).t(C,τ)(C,τ)t. As ι=τ and ι∈IAct, according to Definition 7.1, tRCs. We construct R{}′=RC and show that it induces C⊳t⊑s. This is trivial as any transition C⊳t(C∪C′,η)(C∪C′,η)t′ is the result of t(C′,η)(C′,η)t′. The reverse of the rule can be argued in a similar fashion.
Bibliography51
The reference list from the paper itself. Each links out to its DOI / PubMed record.
1[1] Perkins CE, Belding-Royer EM. Ad-hoc on-demand distance vector routing. In: Proc. 2nd Workshop on Mobile Computing Systems and Applications. IEEE; 1999. p. 90–100.
2[2] Bhargavan K, Obradovid D, Gunter CA. Formal verification of standards for distance vector routing protocols. Journal of the ACM. 2002;49(4):538–576.
3[3] Namjoshi KS, Trefler RJ. Loop freedom in AOD Vv 2. In: Proc. 35th IFIP Conference on Formal Techniques for Distributed Objects, Components, and Systems. vol. 9039 of LNCS; 2015. p. 98–112.
4[4] Fehnker A, Van Glabbeek RJ, Höfner P, Mc Iver A, Portmann M, Tan WL. A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. ar Xiv preprint ar Xiv:13127645. 2013;.
5[5] Yousefi B, Ghassemi F, Khosravi R. Modeling and efficient verification of wireless ad hoc networks. Co RR. 2016;abs/1604.07179. Available from: http://arxiv.org/abs/1604.07179 .
6[6] de Renesse R, Aghvami AH. Formal verification of ad-hoc routing protocols using SPIN model checker. In: Proc. 12th Mediterranean Electrotechnical Conference. IEEE; 2004. p. 1177–1182.
7[7] Wibling O, Parrow J, Pears A. Automatized verification of ad hoc routing protocols. In: Proc. 24th IFIP Conference on Formal Techniques for Networked and Distributed Systems. vol. 3235 of LNCS. Springer; 2004. p. 343–358.
8[8] Wibling O, Parrow J, Pears A. Ad hoc routing protocol verification through broadcast abstraction. In: Proc. 25th IFIP Conference on Formal Techniques for Networked and Distributed Systems. vol. 3731 of LNCS. Springer; 2005. p. 128–142.
