ICALP ARXIV

# DyNetKAT: An Algebra of Dynamic Networks ††thanks: The work of Georgiana
Caltais and Hünkar Can Tunç was supported by the DFG project “CRENKAT”, proj.
no. 398056821. The work of Mohammad Reza Mousavi was supported by the UKRI
Trustworthy Autonomous Systems Node in Verifiability, Grant Award Reference
EP/V026801/1.

Georgiana Caltais, Hünkar Can Tunç  University of Konstanz, Germany
$\\{$georgiana.caltais<EMAIL_ADDRESS>Hossein Hojjat
Tehran Inst. for Advanced Studies, Iran
<EMAIL_ADDRESS>Mohammad Reza Mousavi  King’s College London, UK
<EMAIL_ADDRESS>
###### Abstract

We introduce a formal language for specifying dynamic updates for Software
Defined Networks. Our language builds upon Network Kleene Algebra with Tests
(NetKAT) and adds constructs for synchronisations and multi-packet behaviour
to capture the interaction between the control- and data-plane in dynamic
updates. We provide a sound and ground-complete axiomatization of our
language. We exploit the equational theory to provide an efficient reasoning
method about safety properties for dynamic networks. We implement our
equational theory in DyNetiKAT – a tool prototype, based on the Maude
Rewriting Logic and the NetKAT tool, and apply it to a case study. We show
that we can analyse the case study for networks with hundreds of switches
using our initial tool prototype.

###### Index Terms:

Software Defined Networks, Dynamic Updates, Dynamic Network Reconfiguration,
NetKAT, Process Algebra, Equational Reasoning

##  I Introduction

Software defined networking (SDN) has gained immense popularity due to
simplicity in network management and offering network programmability. Many
programming languages have been designed for programming SDNs [26, 15]. They
range from industrial-scale, hardware-oriented and low-level programming
languages such as OpenFlow [18] to domain-specific, high-level and programmer-
centric languages such as Frenetic [10]. In recent years, there has been a
growing interest in analysable languages based on mathematical foundations
which provide a solid reasoning framework to prove correctness properties in
SDNs (e.g., safety).

There is a spectrum of mathematically inspired network programming languages
that varies between those with a small number of language constructs and those
with expressive language design which allow them to support more networking
features. Flowlog [21] and Kinetic [14] are points on the more expressive side
of the spectrum, which provide support for formal reasoning based on SAT-
solving and model checking, respectively. On the more expressive side of the
spectrum, Flowlog [21] is an example of a language that uses a powerful
formalism (first-order Horn clause logic) to program a Software Defined
Network (SDN). In order to keep the language decidable, Flowlog disallows
recursion in the clauses. For the purpose of formal analysis of a Flowlog
program, the authors of [21] provide a translator to the Alloy tool. As
another example of an expressive language, Kinetic [14] is a language based on
finite state machines that is mostly geared towards dynamic feature of SDNs.
Model checking is used to formally analyse the Kinetic programs. NetKAT [2, 9]
is an example of a minimalist language based on Kleene algebra with tests that
has a sound and complete equational theory. While the core of the language is
very simple with a few number of operators, the language has been extended in
various ways to support different aspects of networking such as congestion
control [8], history-based routing [5] and higher-order functions [27].

Our starting point is NetKAT, because it provides a clean and analysable
framework for specifying SDNs. The minimalist design of NetKAT does not cater
for some common (failure) patterns in SDNs, particularly those arising from
dynamic reconfiguration and the interaction between the data- and control-
plane flows. In [16], the authors have proposed an extension to NetKAT to
support stateful network updates. The extension embraces the notion of mutable
state in the language which is in contrast to its pure functional nature. The
purpose of this paper is to propose an extension to NetKAT to support dynamic
and stateful behaviours. On the one hand, we preserve the big-step
denotational semantics of NetKAT-specific constructs enabling, for instance,
handling flow table updates atomically, in the spirit of [22]. On the other
hand, we extend NetKAT in a modular fashion, to integrate concurrent SDN
behaviours such as dynamic updates, defined via a small-step operational
semantics. To this end, we pledge to keep the minimalist design of NetKAT by
adding only a few new operators. Furthermore, our extension does not
contradict the nature of the language.

A number of concurrent extensions of NetKAT have been introduced to date [23,
28, 13]. These extensions followed different design decisions than the present
paper and a comparison of their approaches with ours is provided in Section
II; however, the most important difference lies in the fact that inspired by
earlier abstractions in this domain [22], we were committed to create
different layers for data-plane flows and dynamic updates such that every
data-plane packet observes a single set of flow tables through its flight
through the network. This allowed us, unlike the earlier approaches, to build
a layer on top of NetKAT without modifying its semantics. Although our
presentation in this paper is based on NetKAT, we envisage that our
concurrency layer can be modularly (in the sense of Modular SOS [19]) used for
other network programming languages in the above-mentioned spectrum. We leave
a more careful investigation of the modularity on other network languages for
future work.

###  I-A Running Examples

Throughout the paper, we focus on modelling with DyNetKAT two examples that
involve dynamically updating the network configuration. In the first example,
stateful firewall, the data-plane initiates the update by allowing a
disallowed path in the network as a result of requests received from the
trusted intranet. In the second, distributed controller, the control-plane
initiates the update by modifying the forwarding route of a packet in a multi-
controller setting.

Running Example. To illustrate our language concepts, we focus on modelling
with DyNetKAT an example of a stateful firewall that involves dynamically
updating the flow table. The example is overly simplified for the purpose of
presentation. Towards the end of this paper and also in the extended version
[6], we treat more complex and larger-scale case studies to evaluate the
applicability and analysability of our language.

###### Example 1

A firewall is supposed to protect the intranet of an organization from
unauthorised access from the Internet. However, due to certain requests from
the intranet, it should be able to open up connections from the Internet to
intranet. An example is when a user within the intranet requests a secure
connection to a node on the Internet; in that case, the response from the node
should be allowed to enter the intranet. The behaviour of updating the flow
tables with respects to some events in the network such as receiving a
specific packet is a challenging phenomenon for languages such as NetKAT.

Figure 1 shows a simplified version of the stateful firewall network. Note
that we are not interested in the flow of packets but interested in the flow
update. In this version, the $\it{Switch}$ does not allow any packet from the
port $\it{ext}$ to $\it{int}$ at the beginning. When the $\it{Host}$ sends a
request to the $\it{Switch}$ it opens up the connection.

$\mathit{Switch}$$\mathit{Host}$$\mathit{int}$$\mathit{ext}$ Figure 1:
Stateful Firewall

###### Example 2

Another running example concerns a well-known challenge in SDNs, namely, race
conditions resulting from dynamic updates of flow-tables and in-flight packets
[17, 25]. Below we specify a typical scenario for such race conditions;
similar scenarios concerning actual bugs are abundant in the literature [25,
11, 12].

Consider the network topology depicted in Figure 2. The controller $C1$
controls the top part of the network (switches $S1$, $S3$ and $S5$) and the
controller $C2$ is responsible for the bottom part. Initially, the packets
from $H1$, which enter the network through switch $S1$ (port $2$), should be
routed through switches $S5$ (through ports $6$ and $7$), $S6$ (through ports
$8$ and $10$) and finally port $12$ of switch $S2$, to reach $H2$. Due to an
event, the controllers have to take down the previous route, and to install a
new route in the network that routes packets from $H3$ through $S3$ (ports $1$
to $3$), $S5$ (through ports $5$ to $7$), $S6$ (ports $8$ to $9$) to switch
$S4$ (port $11$) to finally reach $H4$. It is an important security property
that the traffic in these two routes should not mix. In particular, it will be
serious breach if packets from $H1$ arrive at $H4$ or vice versa, packets from
$H3$ arrive at $H2$.

$S3$13$S1$24$S4$1311$S2$1412$S5$675$S6$8910$H4$15$H2$16$H1$$H3$$C1$$C2$ Figure
2: Race Condition in a Distributed Controller

###  I-B Our Contributions

Our contributions. The contributions of this paper are summarized as follows:

  * •

we define the syntax and operational semantics of a dynamic extension of
NetKAT that allows for modelling and reasoning about control-plane updates and
their interaction with data-plane flows (Sections II-C, II-D);

  * •

we give a sound and ground-complete axiomatization of our language (Section
III); and

  * •

we devise analysis methods for reasoning about flow properties using our
axiomatization, apply them on examples from the domain and gather and analyze
evidence of applicability and efficiency for our approach ( Sections IV, V).

###  I-C Structure of Paper

Structure of Paper. In Section II, we provide a brief overview of NetKAT,
review our design decision and introduce the syntax and operational semantics
of DyNetKAT. In Section III, we investigate some semantic properties of
DyNetKAT by defining a notion of behavioural equivalence and providing a sound
and ground-complete axiomatization. We exploit this axiomatization in Section
IV in an analysis method. We implement and apply our analysis method in
Section V on a case study and report about its scalability on large examples
with hundreds of switches. We conclude the paper and present some avenues for
future work in Section VI.

##  II Language Design

In what follows, we provide a brief overview of the NetKAT syntax and
semantics [2]. Then, we motivate our language design decisions, we introduce
the syntax of DyNetKAT and its underlying semantics, and provide the
corresponding encoding of our running examples presented in Section I-A.

###  II-A Brief Overview of NetKAT

We proceed by first introducing some basic notions that are used throughout
the paper.

######  Definition 1 (Network Packets.)

Let $F=\\{f_{1},\ldots,f_{n}\\}$ be a set of field names $f_{i}$ with
$i\in\\{1,\ldots n\\}$. We call _network packet_ a function in
$F\rightarrow\mathbb{N}$ that maps field names in $F$ to values in
$\mathbb{N}$. We use $\sigma,\sigma^{\prime}$ to range over network packets.
We write, for instance, $\sigma(f_{i})=v_{i}$ to denote a test checking
whether the value of $f_{i}$ in $\sigma$ is $v_{i}$. Furthermore, we write
$\sigma[f_{i}:=n_{i}]$ to denote the assignment of $f_{i}$ to $v_{i}$ in
$\sigma$.

A (possibly empty) _list of packets_ is formally defined as a function from
natural numbers to packets, where the natural number in the domain denotes the
position of the packet in the list such that the domain of the function forms
an interval starting from $0$.

The _empty list_ is denoted by $\langle\rangle$ and is formally defined as the
empty function (the function with the empty set as its domain). Let $\sigma$
be a packet and $l$ be a list, then $\sigma::l$ is the list $l^{\prime}$ in
which $\sigma$ is at position $0$ in $l^{\prime}$, i.e.,
$l^{\prime}(0)=\sigma$, and $l^{\prime}(i+1)=l(i)$, for all $i$ in the domain
of $l$.

In Figure 3, we recall the NetKAT syntax and semantics [2].

$\small\begin{array}[]{rcl}\lx@intercol\textnormal{\bf{NetKAT
Syntax:}}\hfil\lx@intercol\\\
\mathit{Pr}&::=&\mathbf{0}\mid\mathbf{1}{}\mid\mathit{Pr}+\mathit{Pr}\mid\mathit{Pr}\cdot\mathit{Pr}\mid\neg\mathit{Pr}\\\
N&::=&\mathit{Pr}\mid f\leftarrow n\mid N+N\mid N\cdot N\mid
N^{*}\mid\textbf{dup}\end{array}$

$\small\begin{array}[]{cc}\begin{array}[]{rcl}\lx@intercol\textnormal{\bf{NetKAT
Semantics:}}\hfil\lx@intercol\\\
\llbracket\mathbf{1}\rrbracket(h)&\triangleq&\\{h\\}\\\
\llbracket\mathbf{0}\rrbracket(h)&\triangleq&\\{\\}\\\ \llbracket
f=n\rrbracket\;(\sigma{:}{:}h)&\triangleq&\;\left\\{\begin{array}[]{ll}\\{\sigma{:}{:}h\\}&\textnormal{if}\;\sigma(f)=n\\\
\\{\\}&\textnormal{otherwise}\end{array}\right.\\\ \llbracket\neg
a\rrbracket\;(h)&\triangleq&\;\\{h\\}\setminus\,\,\llbracket
a\rrbracket\;(h)\\\ \llbracket f\leftarrow
n\rrbracket\;(\sigma{:}{:}h)&\triangleq&\;\\{\sigma[f:=n]{:}{:}h\\}\\\
\llbracket p+q\rrbracket\;(h)&\triangleq&\;\llbracket
p\rrbracket\;(h)\cup\llbracket q\rrbracket\;(h)\\\ \llbracket p\cdot
q\rrbracket\;(h)&\triangleq&\;(\llbracket p\rrbracket\bullet\llbracket
q\rrbracket)\;(h)\\\ \llbracket
p^{*}\rrbracket\;(h)&\triangleq&\;\bigcup_{i\in N}F^{i}\;(h)\\\
F^{0}\;(h)&\triangleq&\;\\{h\\}\\\ F^{i+1}\;(h)&\triangleq&\;(\llbracket
p\rrbracket\bullet F^{i})\;(h)\\\ (f\bullet
g)(x)&\triangleq&\;\bigcup\\{g(y)\mid y\in f(x)\\}\\\
\llbracket\textbf{dup}\rrbracket\;(\sigma{:}{:}h)&\triangleq&\;\\{\sigma{:}{:}(\sigma{:}{:}h)\\}\par\end{array}\end{array}$

Figure 3: NetKAT: Syntax and Semantics [2]

The predicate for dropping a packet is denoted by $\mathbf{0}{}$, while
passing on a packet (without any modification) is denoted by $\mathbf{1}{}$.
The predicate checking whether the field $f$ of a packet has value $n$ is
denoted by $(f=n)$; if the predicate fails on the current packet it results on
dropping the packet, otherwise it will pass the packet on. Disjunction and
conjunction between predicates are denoted by $\mathit{Pr}+\mathit{Pr}$ and
$\mathit{Pr}\cdot\mathit{Pr}$, respectively. Negation is denoted by
$\neg\mathit{Pr}$. Predicates are the basic building blocks of NetKAT policies
and hence, a predicate is a policy by definition. The policy that modifies the
field $f$ of the current packet to take value $n$ is denoted by $(f\leftarrow
n)$. A multicast behaviour of policies is denoted by $N+N$, while sequencing
policies (to be applied on the same packet) are denoted by $N\cdot N$. The
repeated application of a policy is encoded as $N^{*}$. The construct dup
simply makes a copy of the current network packet.

In [2], lists of packets are referred to as _histories_. Let $H$ stand for the
set of packet histories, and ${\cal P}(H)$ denote the powerset of $H$. More
formally, the denotational semantics of NetKAT policies is inductively defined
via the semantic map $\llbracket-\rrbracket:N\rightarrow(H\rightarrow{\cal
P}(H))$ in Figure 3, where $N$ stands for the set of NetKAT policies, $h\in H$
is a packet history, $a\in{\textit{P}r}$ denotes a NetKAT predicate and
$\sigma\in F\rightarrow\mathbb{N}$ is a network packet.

For a reminder, the equational axioms of NetKAT include the Kleene Algebra
axioms, Boolean Algebra axioms and the so-called Packet Algebra axioms that
handle NetKAT networking specific constructs such as field assignments and
dup. In this paper, we write $E_{\textit{NK}}$ to denote the NetKAT
axiomatization [2].

For a reminder, the equational axioms of NetKAT, denoted by $E_{\textit{NK}}$,
are provided in Figure 4. $E_{\textit{NK}}$ includes the Kleene Algebra axioms
(KA-$\ldots$), Boolean Algebra axioms (BA-$\ldots$) and Packet Algebra axioms
(PA-$\ldots$). The novelty is the set of PA-axioms. In short, PA-MOD-MOD-COMM
states that the order in which two different packet fields are assigned does
not matter. PA-MOD-FILTER-COMM encodes a similar property, for the case of a
field assignment followed by a test of a different field’s value. PA-MOD-
FILTER ignores the test of a field preceded by an assignment of the same value
to the field. Orthogonaly, PA-FILTER-MOD ignores a field assignment preceded
by a test against the assigned value. PA-MOD-MOD states that a sequence of
assignments to the same field only takes into consideration the last
assignment. PA-CONTRA encodes the fact that a field cannot have two different
values at the same point. PA-MATCH-ALL identifies the policy accepting all the
packets with the sum of all possible tests of a field’s value. Intuitively,
PA-DUP-FILTER-COMM states that adding the current packet to the history is
independent of tests.

$\displaystyle\begin{array}[]{r@{}c@{}ll|r@{}c@{}ll}p+(q+r)&\,\equiv&(p+q)+r&\textnormal{\footnotesize
KA-PLUS-ASSOC}{}&~{}a+(b\cdot
c)&\,\equiv&\,(a+b)\cdot(a+c)&\textnormal{\footnotesize BA-PLUS-DIST}\\\
p+q&\,\equiv&q+p&\textnormal{\footnotesize KA-PLUS-
COMM}&a+1&\,\equiv&\,1&\textnormal{\footnotesize BA-PLUS-ONE}\\\
p+0&\,\equiv&p&\textnormal{\footnotesize KA-PLUS-ZERO}&a+\neg
a&\,\equiv&\,1&\textnormal{\footnotesize BA-EXCL-MID}\\\
p+p&\,\equiv&p&\textnormal{\footnotesize KA-PLUS-IDEM}&a\cdot
b&\,\equiv&\,b\cdot a&\textnormal{\footnotesize BA-SEQ-COMM}\\\ p\cdot(q\cdot
r)&\,\equiv&(p\cdot q)\cdot r&\textnormal{\footnotesize KA-SEQ-
ASSOC}{}&a\cdot\neg a&\,\equiv&\,0&\textnormal{\footnotesize BA-CONTRA}\\\
1\cdot p&\,\equiv&p&\textnormal{\footnotesize KA-ONE-SEQ}{}&a\cdot
a&\,\equiv&\,a&\textnormal{\footnotesize BA-SEQ-IDEM}\\\ p\cdot
1&\,\equiv&p&\textnormal{\footnotesize KA-SEQ-ONE}{}&&&&\\\
p\cdot(q+r)&\,\equiv&p\cdot q+p\cdot r&\textnormal{\footnotesize KA-SEQ-
DIST-L}{}&f\leftarrow n\cdot f^{\prime}\leftarrow
n^{\prime}&\,\equiv&f^{\prime}\leftarrow n^{\prime}\cdot f\leftarrow
n,\textnormal{if }f\not=f^{\prime}{}{}&\textnormal{\footnotesize PA-MOD-MOD-
COMM}\\\ (p+q)\cdot r&\,\equiv&p\cdot r+q\cdot r&\textnormal{\footnotesize KA-
SEQ-DIST-R}{}&f\leftarrow n\cdot
f^{\prime}=n^{\prime}&\,\equiv&f^{\prime}=n^{\prime}\cdot f\leftarrow
n,\textnormal{if }f\not=f^{\prime}&\textnormal{\footnotesize PA-MOD-FILTER-
COMM}\\\ 0\cdot p&\,\equiv&0&\textnormal{\footnotesize KA-ZERO-SEQ}{}&{\bf
dup}\cdot f=n&\,\equiv&f=n\cdot{\bf dup}&\textnormal{\footnotesize PA-DUP-
FILTER-COMM}\\\ p\cdot 0&\,\equiv&0&\textnormal{\footnotesize KA-ZERO-
SEQ}{}&f\leftarrow n\cdot f=n&\,\equiv&f\leftarrow n&\textnormal{\footnotesize
PA-MOD-FILTER}\\\ 1+p\cdot p^{*}&\,\equiv&p^{*}&\textnormal{\footnotesize KA-
UNROLL-L}{}&f=n\cdot f\leftarrow n&\,\equiv&f=n&\textnormal{\footnotesize PA-
FILTER-MOD}\\\ 1+p^{*}\cdot p&\,\equiv&p^{*}&\textnormal{\footnotesize KA-
UNROLL-R}{}&f\leftarrow n\cdot f\leftarrow n^{\prime}&\,\equiv&f\leftarrow
n^{\prime}&\textnormal{\footnotesize PA-MOD-MOD}\\\ q+p\cdot r\leq
r&\,\Rightarrow&p^{*}\cdot q\leq r&\textnormal{\footnotesize KA-
LFP-L}{}&f=n\cdot f=n^{\prime}&\,\equiv&\,0,\textnormal{if
}n\not=n^{\prime}&\textnormal{\footnotesize PA-CONTRA}\\\ p+q\cdot r\leq
q&\,\Rightarrow&p\cdot r^{*}\leq q&\textnormal{\footnotesize KA-
LFP-R}{}&\Sigma_{i}f=i&\,\equiv&\,1&\textnormal{\footnotesize PA-MATCH-
ALL}\end{array}$

Figure 4: $E_{\textit{NK}}$: NetKAT Equational Axioms [2]

###  II-B Design Decisions

Our main motivation behind DyNetKAT is to have a _minimalistic_ language that
can model _control-plane_ and _data-plane_ network traffic and their
interaction. Our choice for a minimal language is motivated by our desire to
use our language as a basis for scalable analysis. We would like to be able to
compile major practical languages into ours. Our minimal design helps us reuse
much of the well-known scalable analysis techniques. Regarding its modelling
capabilities, we are interested in modelling the stateful and dynamic
behaviour of networks emerging from these interactions. We would like to be
able to model control messages, connections between controllers and switches,
data packets, links among switches, and model and analyse their interaction in
a seamless manner.

Based on these motivations, we start off with NetKAT as a fundamental and
minimal network programming language, which allows us to model the basic
policies governing the network traffic. The choice of NetKAT, in addition to
its minimalist nature, is motivated by its rigorous semantics and equational
theory, and the existing techniques and tools for its analysis. This motivates
our next design constraint, namely, to build upon NetKAT in a hierarchical
manner and without redefining its semantics. This constraint should not be
taken lightly as the challenges in the recent concurrent extensions of NetKAT
demonstrated [23, 28, 13]. We will elaborate on this point, in the
presentation of our syntax and semantics. We can achieve this thanks to the
abstractions introduced in the domain [22] that allows for a neat layering of
data-plane and control-plan flows such that every data-plane flow sees one set
of flow-tables in its flight through the network.

We then introduce a few extensions and modifications to cater for the
phenomena we desire to model in our extension regarding control-plane and
dynamic and stateful behaviour:

  * •

Synchronisation: we introduce a basic mechanism of handshake synchronisation
with the possibility of communicating a network program (a flow table). This
construct allows for capturing the dynamicity and interaction between the
control and data planes.

  * •

Guarded recursion: we introduce the concept of recursion to model the
(persistent) dynamic changes that result from control messages and stateful
behaviour. In other words, recursion is used to model the new state of the
flow tables. An alternative modelling construct could have been using “global”
variables and guards, but we prefer recursion due to its neat algebraic
representation. We restrict the use of recursion to guarded recursion, that is
a policy should be applied before changing state to a new recursive
definition, in order to remain within a decidable and analyse-able realm. A
natural extension of our framework could introduce formal parameters and
parameterised recursive variables; this future extension is orthogonal to our
existing extensions and in this paper, we go for a minimal extension in which
the parameters are coded in variable names.

  * •

Multi-packet semantics: we introduce the semantics of treating a list of
packets, which is essential for studying the interaction between control- and
data plane packets. This is in contrast with NetKAT where a single-packet
semantics is introduced. The introduction of multi-packet semantics also
called for a new operator to denote the end of applying a flow-table to the
current packet and proceeding with the next packet (possibly with the modified
flow-table in place). This is our new sequential composition operator, denoted
by “;”.

###  II-C DyNetKAT Syntax

As already mentioned, NetKAT provides the possibility of recording the
individual “hops” that packets take as they go through the network by using
the so-called dup construct. The latter keeps track of the state of the packet
at each intermediate hop. As a brief reminder of the approach in [2]: assume a
NetKAT switch policy $p$ and a topology $t$, together with an ingress ${\it
in}$ and an egress ${\it out}$. Checking whether ${\it out}$ is reachable from
${\it in}$ reduces to checking: ${\it in}\cdot\textbf{dup}\cdot(p\cdot
t\cdot\textbf{dup})^{*}\cdot{\it out}\not\equiv\mathbf{0}$ (see Definition $2$
and Theorem $4$ in [2]). Furthermore, as shown in [9], dup plays a crucial
role in devising the NetKAT language semantics in a coalgebraic fashion, via
Brzozowski-like derivatives on top of NetKAT coalgebras (or NetKAT automata)
corresponding to NetKAT expressions.

We decided to depart from NetKAT in this respect, due to our important
constraint not to redefine the NetKAT semantics: the dup expression allows for
observable intermediate steps that result from incomplete application of flow-
tables and in concurrency scenarios, the same data packet may become subject
to more than one flow table due to the concurrent interactions with the
control plane. For this semantics to be compositional, one needs to define a
small step operational semantics in such a way that the small steps in
predicate evaluation also become visible (see our past work on
compositionality of SOS with data on such constraints [20]). This will first
break our constraint in building upon NetKAT semantics and secondly, due to
the huge number of possible interleavings, make the resulting state-space
intractable for analysis.

In addition to the argumentation above, note that similarly to the approach in
[2], we work with packet fields ranging over finite domains. Consequently, our
analyses can be formulated in terms of reachability properties, further
verifiable by means of dup-free expressions of shape: ${\it in}\cdot(p\cdot
t)^{*}\cdot{\it out}\not\equiv\mathbf{0}$. Hence, we chose to define DyNetKAT
synchronization, guarded recursion and multi-packet semantics on top of the
dup-free fragment of NetKAT, denoted by $\textnormal{NetKAT}^{-{\bf{dup}}}$.

The syntax of DyNetKAT is defined on top of the dup-free fragment of NetKAT
as:

$\begin{array}[]{ccl}\mathit{N}&::=&{\textnormal{NetKAT}^{-{\bf{dup}}}}\\\\[4.30554pt]
\mathit{D}&::=&{\bot}\mid\mathit{N}\mathop{;}\mathit{D}\mid
x?\mathit{N}\mathop{;}D\mid
x!\mathit{N}\mathop{;}D\mid\mathit{D}\mathop{||}\mathit{D}\mid D\oplus D\mid
X\\\ &&X\triangleq D\par\end{array}$ (1)

We sometimes write $p\in\textnormal{NetKAT}$,
$p\in{\textnormal{NetKAT}^{-{\bf{dup}}}}$ or, respectively,
$p\in\textnormal{{DyNetKAT}}$ in order to refer to a NetKAT,
${\textnormal{NetKAT}^{-{\bf{dup}}}}$ or, respectively, DyNetKAT policy $p$.

The DyNetKAT-specific constructs are as follows. By $\bot$ we denote a dummy
policy without behaviour. Our new sequential composition operator, denoted by
$\mathit{N}\mathop{;}\mathit{D}$, specifies when the
$\textnormal{NetKAT}^{-{\bf{dup}}}$ policy $N$ applicable to the current
packet has come to a successful end and, thus, the packet can be transmitted
further and the next packet can be fetched for processing according to the
rest of the policy $D$.

Communication in DyNetKAT, encoded via $x!\mathit{N};D$ and $x?\mathit{N};D$,
consists of two steps. In the first place, sending and receiving
$\textnormal{NetKAT}^{-{\bf{dup}}}$ policies through channel $x$ are denoted
by $x!\mathit{N}$, and $x?\mathit{N}$. Intuitively, these correspond to
updating the current network configuration according to $N$. Secondly, as soon
as the sending or receiving messages are successfully communicated, a new
packet is fetched and processed according to $D$. The parallel composition of
two DyNetKAT policies (to enable synchronization) is denoted by
$\mathit{D}\mathop{||}\mathit{D}$.

As it will become clearer in Section II-D (semantics), communication in
DyNetKAT guarantees preservation of well-defined behaviours when transitioning
between network configurations. This corresponds to the so-called per-packet
consistency in [22], and it guarantees that every packet traversing the
network is processed according to exactly one
$\textnormal{NetKAT}^{-{\bf{dup}}}$ policy.

Non-deterministic choice of DyNetKAT policies is denoted by $D\oplus D$. For a
non-determinstic choice over a finite domain $P$, we use the syntactic sugar
$\oplus_{p\in P}P^{\prime}$, where $p$ appears as “bound variable” in
$P^{\prime}$; this is interpreted as a sum of finite summand by replacing the
variable $p$ with all its possible values in $P$.

Finally, one can use recursive variables $X$ in the specification of DyNetKAT
policies, where each recursive variable should have a unique defining equation
$X\triangleq D$.

For the simplicity of notation, we do not explicitly specify the trailing
“$;\bot$” in our policy specifications, whenever clear from the context.

In Figure 6 we provide the DyNetKAT formalization of the firewall in Example
1. In the DyNetKAT encoding, we use the message channel $\it{secConReq}$ to
open up the connection and $\it{secConEnd}$ to close it. We model the behavior
of the switch using the two programs $\mathit{Switch}$ and
$\mathit{Switch^{\prime}}$.

$\footnotesize{\begin{array}[]{r@{}c@{}ll}\mathit{Switch}&\triangleq&\big{(}(port=int)\cdot(port\leftarrow
ext)\big{)}\mathop{;}\mathit{Switch}\oplus\\\
&&\big{(}(port=ext)\cdot\mathbf{0}\big{)}\mathop{;}\mathit{Switch}\oplus\\\
&&secConReq?\mathbf{1}\mathop{;}Switch^{\prime}\\\ \\\
\mathit{Switch}^{\prime}&\triangleq&\big{(}(port=int)\cdot(port\leftarrow
ext)\big{)}\mathop{;}\mathit{Switch}^{\prime}\oplus\\\
&&\big{(}(port=ext)\cdot(port\leftarrow
int)\big{)}\mathop{;}\mathit{Switch}^{\prime}\oplus\\\
&&secConEnd?\mathbf{1}\mathop{;}Switch\\\ \\\
\mathit{Host}&\triangleq&secConReq!\mathbf{1}\mathop{;}\mathit{Host}\oplus
secConEnd!\mathbf{1}\mathop{;}\mathit{Host}\\\ \\\
\mathit{Init}&\triangleq&\mathit{Host}\mathop{||}\mathit{Switch}\\\
\end{array}}$
Figure 5: Stateful Firewall in DyNetKAT

$\begin{array}[]{ccl}\mathit{Host}&\triangleq&secConReq!\mathbf{1}\mathop{;}\mathit{Host}\oplus\\\
&&secConEnd!\mathbf{1}\mathop{;}\mathit{Host}\\\ \\\
\mathit{Switch}&\triangleq&\big{(}(port=int)\cdot(port\leftarrow
ext)\big{)}\mathop{;}\mathit{Switch}\oplus\\\
&&\big{(}(port=ext)\cdot\mathbf{0}\big{)}\mathop{;}\mathit{Switch}\oplus\\\
&&secConReq?\mathbf{1}\mathop{;}Switch^{\prime}\\\ \\\
\mathit{Switch}^{\prime}&\triangleq&\big{(}(port=int)\cdot(port\leftarrow
ext)\big{)}\mathop{;}\mathit{Switch}^{\prime}\oplus\\\
&&\big{(}(port=ext)\cdot(port\leftarrow
int)\big{)}\mathop{;}\mathit{Switch}^{\prime}\oplus\\\
&&secConEnd?\mathbf{1}\mathop{;}Switch\\\ \\\
\mathit{Init}&\triangleq&\mathit{Host}\mathop{||}\mathit{Switch}\\\
\end{array}$ Figure 6: Stateful Firewall in DyNetKAT

In Figure 7 we provide the DyNetKAT formalization of the distributed
controllers in Example 2. In the code in Figure 7 the controllers work
independently to update the network (which can lead to security breach). The
specification $\mathit{SwitchX}_{ft}$ is a generic specification for the
behaviour of all switches in this example; the domain of $P$ in this example
is the set of all $5$ policies that are being communicated, such as
$\mathbf{0}$, $((port=11)\cdot(port\leftarrow 13))$, and
$((port=5)\cdot(port\leftarrow 7))$.

However, in the code in Figure 8 the controllers synchronise before updating
the rest of the switches.

$\begin{array}[]{lcl}\mathit{L}&\triangleq&(((port=3)\cdot(port\leftarrow
5))+\\\ &&((port=4)\cdot(port\leftarrow 6))+\\\
&&((port=7)\cdot(port\leftarrow 8))+\\\ &&((port=9)\cdot(port\leftarrow
11))+\\\ &&((port=10)\cdot(port\leftarrow 12))+\\\
&&((port=13)\cdot(port\leftarrow 15))+\\\ &&((port=14)\cdot(port\leftarrow
16)))\\\ \\\ S_{1}&\triangleq&(port=2)\cdot(port\leftarrow 4)\\\
S_{2}&\triangleq&(port=12)\cdot(port\leftarrow 14)\\\
S_{3}&\triangleq&\mathbf{0}\\\ S_{4}&\triangleq&\mathbf{0}\\\
S_{5}&\triangleq&(port=6)\cdot(port\leftarrow 7)\\\
S_{6}&\triangleq&(port=8)\cdot(port\leftarrow 10)\\\
\mathit{SDN}_{X_{1},\ldots,X_{6}}&\triangleq&((X_{1}+\ldots+X_{6})\cdot
L)^{*}\mathop{;}\mathit{SDN}_{X_{1},\ldots,X_{6}}\oplus\\\
&&\sum_{X^{\prime}_{i}\in\mathit{FT}}\mathit{upSi}?X^{\prime}_{i}\mathop{;}\mathit{SDN}_{X_{1},\ldots,X^{\prime}_{i},\ldots,X_{6}}\\\
\\\ \mathit{ft3}&\triangleq&(port=1)\cdot(port\leftarrow 3)\\\
\mathit{ft4}&\triangleq&(port=11)\cdot(port\leftarrow 13)\\\
\mathit{ft5}&\triangleq&(port=5)\cdot(port\leftarrow 7)\\\
\mathit{ft6}&\triangleq&(port=8)\cdot(port\leftarrow 9)\\\
\mathit{FT}&=&\\{\mathbf{0}{},\mathit{ft3},\mathit{ft4},\mathit{ft5},\mathit{ft6}\\}\\\
\\\
\mathit{SDN}&\triangleq&\mathit{SDN}_{S_{1},\ldots,S_{6}}\mathop{||}C_{1}\mathop{||}C_{2}\\\
\\\ \ \par
C_{1}&\triangleq&upS1!\mathbf{0}{}\mathop{||}upS3!\mathit{ft3}\mathop{||}upS5!\mathit{ft5}\\\
\\\
C_{2}&\triangleq&upS2!\mathbf{0}{}\mathop{||}upS4!\mathit{ft4}\mathop{||}upS6!\mathit{ft6}\end{array}$
Figure 7: Distributed Controller in DyNetKAT: Independent Controllers

$\begin{array}[]{ccl}C_{1}&\triangleq&upS1!\mathbf{0}{};\\\
&&syn!\mathbf{1}{};\\\ &&upS3!((port=1)\cdot(port\leftarrow 3));\\\
&&upS5!((port=5)\cdot(port\leftarrow 7))\\\ \\\ \end{array}$

$\begin{array}[]{ccl}C_{2}&\triangleq&upS2!\mathbf{0}{};\\\
&&syn?\mathbf{1}{};\\\ &&upS4!((port=11)\cdot(port\leftarrow 13));\\\
&&upS6!((port=8)\cdot(port\leftarrow 9))\end{array}$

Figure 8: Distributed Controller in DyNetKAT: Synchronizing Controllers

###  II-D DyNetKAT Semantics

The operational semantics of DyNetKAT in Figure 10 is provided over
configurations of shape $(d,H,H^{\prime})$, where $d$ stands for the current
DyNetKAT policy, $H$ is the list of packets to be processed by the network
according to $d$ and $H^{\prime}$ is the list of packets handled successfully
by the network. The rule labels $\gamma$ range over pairs of packets
$(\sigma,\sigma^{\prime})$ or communication/reconfiguration-like actions of
shape $x!q,\,x?q$ or $\mathbf{rcfg(x,q)}$, depending on the context.

Note that the DyNetKAT semantics is devised in a “layered” fashion. Rule
$\mathbf{(cpol_{\\_\mathop{;}}^{\checkmark})}$ in Figure 10 is the base rule
that makes the transition between the NetKAT denotations and DyNetKAT
operations. More precisely, whenever $\sigma^{\prime}$ is a packet resulted
from the successful evaluation of a NetKAT policy $p$ on $\sigma$, a
$(\sigma,\sigma^{\prime})$-labelled step is observed at the level of DyNetKAT.
This transition applies whenever the current configuration encapsulates a
DyNetKAT policy of shape $p;q$ and a list of packets to be processed starting
with $\sigma$. The resulting configuration continues with evaluating $q$ on
the next packet in the list, while $\sigma^{\prime}$ is marked as successfully
handled by the network.

The remaining rules in Figure 10 define non-deterministic choice $\oplus$,
synchronization $\mathop{||}$ and recursion $X$ in the standard fashion. Note
that synchronizations leave the packet lists unchanged. Due to space
limitation, we omitted the explicit definitions of the symmetric cases for
$\oplus$ and $\mathop{||}$. The full semantics is provided in [6].

$\begin{array}[]{|c|c|}\hline\cr&\\\
\mathbf{(cpol_{\\_\mathop{;}}^{\checkmark})}\frac{\raisebox{1.68776pt}{\normalsize{${\sigma^{\prime}\in\llbracket
p\rrbracket(\sigma\\!\\!::\\!\\!\langle\rangle)}$}}}{\raisebox{-2.4111pt}{\normalsize{$(p;q,\sigma::H,H^{\prime})\,\,{{\xrightarrow{(\sigma,\sigma^{\prime})}}}\,\,(q,H,\sigma^{\prime}::H^{\prime})$}}}&\mathbf{(cpol_{X})}\frac{\raisebox{1.68776pt}{\normalsize{$(p,{H_{0},H_{1}})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},{H^{\prime}_{0},H^{\prime}_{1}})$}}}{\raisebox{-2.4111pt}{\normalsize{$(X,H_{0},H_{1})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H^{\prime}_{0},H^{\prime}_{1})$}}}X\triangleq
p\\\ &\\\ \hline\cr&\\\
\mathbf{(cpol_{\\_\oplus})}\frac{\raisebox{1.68776pt}{\normalsize{$(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-2.4111pt}{\normalsize{$(p\oplus
q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}&\mathbf{(cpol_{\\_||})}\frac{\raisebox{1.68776pt}{\normalsize{$(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-2.4111pt}{\normalsize{$(p||q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime}||q,H_{1},H^{\prime}_{1})$}}}\\\
&\\\ \hline\cr\vrule\lx@intercol\hfil\hfil\lx@intercol\vrule\lx@intercol\\\
\vrule\lx@intercol\hfil\mathbf{(cpol_{\bullet})}\frac{\raisebox{1.68776pt}{\normalsize{$$}}}{\raisebox{-2.4111pt}{\normalsize{$(x\,\bullet\,p;q,H,H^{\prime})\,\,{{\xrightarrow{x\bullet
p}}}\,\,(q,H,H^{\prime})$}}}~{}~{}~{}\bullet\in\\{?,!\\}\hfil\lx@intercol\vrule\lx@intercol\\\
\vrule\lx@intercol\hfil\hfil\lx@intercol\vrule\lx@intercol\\\
\hline\cr\vrule\lx@intercol\hfil\hfil\lx@intercol\vrule\lx@intercol\\\
\vrule\lx@intercol\hfil\mathbf{(cpol_{\clubsuit\spadesuit})}\frac{\raisebox{1.68776pt}{\normalsize{$(q,{H,H^{\prime}})\,\,{{\xrightarrow{x\,\clubsuit\,p}}}\,\,(q^{\prime},H,H^{\prime})\quad(s,{H,H^{\prime}})\,\,{{\xrightarrow{x\,\spadesuit\,p}}}\,\,(s^{\prime},H,H^{\prime})$}}}{\raisebox{-2.4111pt}{\normalsize{$(q||s,H,H^{\prime})\,\,{{\xrightarrow{\mathbf{rcfg(x,p)}}}}\,\,(q^{\prime}||s^{\prime},H,H^{\prime})$}}}~{}~{}~{}\begin{array}[]{c}\clubsuit=?~{}~{}~{}\spadesuit=!\\\
\textnormal{or}\\\
\clubsuit=!~{}~{}~{}\spadesuit=?\end{array}\hfil\lx@intercol\vrule\lx@intercol\\\
\vrule\lx@intercol\hfil\hfil\lx@intercol\vrule\lx@intercol\\\
\hline\cr\end{array}$

$\gamma::=(\sigma,\sigma^{\prime})\mid x!q\mid x?q\mid{\mathbf{rcfg(x,q)}}$

Figure 9: DyNetKAT: Operational Semantics (relevant excerpt)

The operational semantics of DyNetKAT in Figure 10 is provided over
configurations of shape $(d,H,H^{\prime})$, where $d$ stands for the current
DyNetKAT policy, $H$ is the list of packets to be processed by the network
according to $d$ and $H^{\prime}$ is the list of packets handled successfully
by the network. The rule labels $\gamma$ range over pairs of packets
$(\sigma,\sigma^{\prime})$ or communication/reconfiguration-like actions of
shape $x!q,\,x?q$ or $\mathbf{rcfg(x,q)}$, depending on the context.

Note that the DyNetKAT semantics is devised in a “layered” fashion. Rule
$\mathbf{(cpol_{\\_\mathop{;}}^{\checkmark})}$ in Figure 10 is the base rule
that makes the transition between the NetKAT denotations and DyNetKAT
operations. More precisely, whenever $\sigma^{\prime}$ is a packet resulted
from the successful evaluation of a NetKAT policy $p$ on $\sigma$, a
$(\sigma,\sigma^{\prime})$-labelled step is observed at the level of DyNetKAT.
This transition applies whenever the current configuration encapsulates a
DyNetKAT policy of shape $p;q$ and a list of packets to be processed starting
with $\sigma$. The resulting configuration continues with evaluating $q$ on
the next packet in the list, while $\sigma^{\prime}$ is marked as successfully
handled by the network.

The remaining rules in Figure 10 define non-deterministic choice,
synchronization and recursion in the standard fashion.

Rules $\mathbf{(cpol_{\\_\oplus})}$ and $\mathbf{(cpol_{\\_\oplus})}$ define
non-deterministic behaviours. Assume $H_{0}$ is the list of packets to be
processed by the network according to $p$ (respectively, $q$) and
$H^{\prime}_{0}$ is the list of packets handled successfully by the network.
Whenever $p$ (respectively, $q$) determines a $\gamma$-labelled transition
into $(p^{\prime},H_{1},H^{\prime}_{1})$ (respectively,
$(q^{\prime},H_{1},H^{\prime}_{1})$), the policy $p\oplus q$ is able to mimic
the same behaviour. Rules $\mathbf{(cpol_{\\_||})}$ and
$\mathbf{(cpol_{||\\_})}$ follow a similar pattern; the only difference is
that the “inactive” operand is preserved by the target of the semantic rule.

Mere sending $\mathbf{(cpol_{!})}$ and receiving $\mathbf{(cpol_{?})}$ entail
transitions labelled accordingly, and continue with the DyNetKAT policy
following the ; operator. Note that the list of packets to be processed by the
network and the list of packets handled successfully by the network remain
unchanged.

DyNetKAT synchronization is defined by $\mathbf{(cpol_{!?})}$ and
$\mathbf{(cpol_{?!})}$. Intuitively, when both operands $q$ and, respectively,
$s$ “agree” on sending/receiving a policy $p$ on channel $x$ in the context of
the same packet lists $H$ and $H^{\prime}$, and behave like $q^{\prime}$,
respectively, $s^{\prime}$ afterwards, then a $\mathbf{rcfg(x,p)}$ step can be
observed. The system proceeds with the continuation behaviour
$q^{\prime}\mathop{||}s^{\prime}$.

As denoted by $\mathbf{(cpol_{X})}$, a recursive variable defined as
$X\triangleq p$ behaves according to $p$.

$\begin{array}[]{|c|c|}\hline\cr&\\\
\mathbf{(cpol_{\\_\mathop{;}}^{\checkmark})}\frac{\raisebox{2.1097pt}{\normalsize{${\sigma^{\prime}\in\llbracket
p\rrbracket(\sigma\\!\\!::\\!\\!\langle\rangle)}$}}}{\raisebox{-3.01389pt}{\normalsize{$(p;q,\sigma::H,H^{\prime})\,\,{{\xrightarrow{(\sigma,\sigma^{\prime})}}}\,\,(q,H,\sigma^{\prime}::H^{\prime})$}}}&\mathbf{(cpol_{X})}\frac{\raisebox{2.1097pt}{\normalsize{$(p,{H_{0},H_{1}})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},{H^{\prime}_{0},H^{\prime}_{1}})$}}}{\raisebox{-3.01389pt}{\normalsize{$(X,H_{0},H_{1})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H^{\prime}_{0},H^{\prime}_{1})$}}}X\triangleq
p\\\ &\\\ \hline\cr&\\\
\mathbf{(cpol_{\\_\oplus})}\frac{\raisebox{2.1097pt}{\normalsize{$(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(p\oplus
q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}&\mathbf{(cpol_{\oplus\\_})}\frac{\raisebox{2.1097pt}{\normalsize{$(q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(p\oplus
q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$}}}\\\
&\\\ \hline\cr&\\\
\mathbf{(cpol_{\\_||})}\frac{\raisebox{2.1097pt}{\normalsize{$(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(p||q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime}||q,H_{1},H^{\prime}_{1})$}}}&\mathbf{(cpol_{||\\_})}\frac{\raisebox{2.1097pt}{\normalsize{$(q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(p||q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p||q^{\prime},H_{1},H^{\prime}_{1})$}}}\\\
&\\\ \hline\cr&\\\
\mathbf{(cpol_{?})}\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$(x?p;q,H,H^{\prime})\,\,{{\xrightarrow{x?p}}}\,\,(q,H,H^{\prime})$}}}&\mathbf{(cpol_{!})}\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$(x!p;q,H,H^{\prime})\,\,{{\xrightarrow{x!p}}}\,\,(q,H,H^{\prime})$}}}\\\
&\\\ \hline\cr\vrule\lx@intercol\hfil\hfil\lx@intercol\vrule\lx@intercol\\\
\vrule\lx@intercol\hfil\mathbf{(cpol_{!?})}\frac{\raisebox{2.1097pt}{\normalsize{$(q,H,H^{\prime})\,\,{{\xrightarrow{x!p}}}\,\,(q^{\prime},H,H^{\prime})\quad(s,H,H^{\prime})\,\,{{\xrightarrow{x?p}}}\,\,(s^{\prime},H,H^{\prime})$}}}{\raisebox{-3.01389pt}{\normalsize{$(q||s,H,H^{\prime})\,\,{{\xrightarrow{\mathbf{rcfg(x,p)}}}}\,\,(q^{\prime}||s^{\prime},H,H^{\prime})$}}}\hfil\lx@intercol\vrule\lx@intercol\\\
\vrule\lx@intercol\hfil\hfil\lx@intercol\vrule\lx@intercol\\\
\hline\cr\vrule\lx@intercol\hfil\hfil\lx@intercol\vrule\lx@intercol\\\
\vrule\lx@intercol\hfil\mathbf{(cpol_{?!})}\frac{\raisebox{2.1097pt}{\normalsize{$(q,{H,H^{\prime}})\,\,{{\xrightarrow{x?p}}}\,\,(q^{\prime},H,H^{\prime})\quad(s,{H,H^{\prime}})\,\,{{\xrightarrow{x!p}}}\,\,(s^{\prime},H,H^{\prime})$}}}{\raisebox{-3.01389pt}{\normalsize{$(q||s,H,H^{\prime})\,\,{{\xrightarrow{\mathbf{rcfg(x,p)}}}}\,\,(q^{\prime}||s^{\prime},H,H^{\prime})$}}}\hfil\lx@intercol\vrule\lx@intercol\\\
\vrule\lx@intercol\hfil\hfil\lx@intercol\vrule\lx@intercol\\\
\hline\cr\end{array}$

$\gamma::=(\sigma,\sigma^{\prime})\mid x!q\mid x?q\mid{\mathbf{rcfg(x,q)}}$

Figure 10: DyNetKAT: Operational Semantics

In Figure 11 we depict a labelled transition system (LTS) encoding a possible
behaviour of the stateful firewall in Example 1. We assume the list of network
packets to be processed consists of a “safe” packet $\sigma_{i}$ travelling
from int to ext (i.e., $\sigma_{i}(\it{port})=\it{int}$) followed by a
potentially “dangerous” packet $\sigma_{e}$ travelling from ext to int (i.e.,
$\sigma_{e}(\it{port})=\it{ext}$). For the simplicity of notation, in Figure
11 we write H for Host, S for Switch, $\mathit{S}^{\prime}$ for
$\mathit{Switch}^{\prime}$, $\mathit{SCR}$ for $\mathit{secConReq}$ and
$\mathit{SCE}$ for $\mathit{secConEnd}$. Note that $\sigma_{e}$ can enter the
network only if a secure connection request was received. More precisely, the
transition labelled $(\sigma_{e},\sigma_{i})$ is preceded by a transition
labelled $\mathit{SCR}?1$ or $\mathbf{rcfg(\mathit{SCR},1)}$:
$n_{2}\xrightarrow{\mathit{SCR}?1,\,\,\mathbf{rcfg(\mathit{SCR},1)}}n_{3}\xrightarrow{(\sigma_{e},\sigma_{i})}n_{4}$.

$n_{1}:(H||S^{\prime},\sigma_{i}{::}\sigma_{e}{::}\langle\rangle,\langle\rangle)$$n_{0}:(H||S,\sigma_{i}{::}\sigma_{e}{::}\langle\rangle,\langle\rangle)$$n_{2}:(H||S,\sigma_{e}{::}\langle\rangle,\sigma_{e}{::}\langle\rangle$$n_{3}:(H||S^{\prime},\sigma_{e}{::}\langle\rangle,\sigma_{e}{::}\langle\rangle$$n_{4}:(H||S^{\prime},\langle\rangle,\sigma_{i}{::}\sigma_{e}{::}\langle\rangle$$n_{5}:(H||S,\langle\rangle,\sigma_{i}{::}\sigma_{e}{::}\langle\rangle$$\scriptstyle{SCE!\mathbf{1}{},SCR!\mathbf{1}{}}~{}~{}~{}$$\scriptstyle{SCE!\mathbf{1}{},\mathbf{rcfg(SCE,\mathbf{1}{})}}$$(\sigma_{i},\sigma_{e})$$\scriptstyle{SCE!\mathbf{1}{},SCR!\mathbf{1}{}}~{}~{}~{}$$\scriptstyle{SCR!\mathbf{1}{},\mathbf{rcfg(SCR,\mathbf{1}{})}}$$(\sigma_{i},\sigma_{e})$$\scriptstyle{SCE!\mathbf{1}{},SCR!\mathbf{1}{}}$$\scriptstyle{SCR!\mathbf{1}{},\mathbf{rcfg(SCR,\mathbf{1}{})}}$$\scriptstyle{SCE!\mathbf{1}{},\mathbf{rcfg(SCE,\mathbf{1}{})}}$$(\sigma_{e},\sigma_{i})$$\scriptstyle{SCE!\mathbf{1}{},SCR!\mathbf{1}{}}$$\scriptstyle{SCE!\mathbf{1}{},SCR!\mathbf{1}{}}$$\scriptstyle{SCE!\mathbf{1}{},\mathbf{rcfg(SCE,\mathbf{1}{})}}$$\scriptstyle{SCR!\mathbf{1}{},\mathbf{rcfg(SCR,\mathbf{1}{})}}$$\scriptstyle{SCE!\mathbf{1}{},SCR!\mathbf{1}{}}$
Figure 11: Stateful Firewall LTS

In Figure 12 we depict an excerpt of the LTS corresponding to the distributed
independent controllers in Example 2, given a network packet denoted by
$\sigma_{2}$. In Figure 12 we write $\sigma_{i}$ to denote a network packet
such that $\sigma_{i}(port)=i$. For instance, transitions of shape
$n_{0}\xrightarrow{(\sigma_{2},\sigma_{i})}\overline{n}_{i}$ encode forwarding
of the current packet from port $2$ to port $i$ based on the subsequent
unfoldings of the Kleene-star expression in the definition of
$\mathit{SDN}_{X_{1},\ldots,X_{6}}$. The transition
$n_{2}\xrightarrow{(\sigma_{2},\sigma_{15})}\overline{\overline{n}}_{15}$
reveals a breach in the network corresponding to the possibility of forwarding
the current packet from $H_{1}$ to $H_{4}$. This is possible due to two
consecutive reconfigurations of the flow tables of switches $S_{6}$ and
$S_{4}$, respectively, enabling traffic from port $8$ to $9$, and from port
$11$ to $13$.

$n_{0}:(SDN,\sigma_{2}{::}\langle\rangle,\langle\rangle)$$\ldots$$n_{1}:SDN_{S_{1},S_{2},S_{3},S_{4},S_{5},ft_{6}}\mathop{||}C1\mathop{||}(upS2!\mathbf{0}{}\mathop{||}upS4!ft_{4}),\sigma_{2}{::}\langle\rangle,\langle\rangle)$$n_{2}:SDN_{S_{1},S_{2},S_{3},S_{4},S_{5},ft_{6}}\mathop{||}C1\mathop{||}(upS2!\mathbf{0}{}),\sigma_{2}{::}\langle\rangle,\langle\rangle)$$\overline{\overline{n}}_{j}:SDN_{S_{1},S_{2},S_{3},S_{4},S_{5},ft_{6}}\mathop{||}C1\mathop{||}(upS2!\mathbf{0}{}\mathop{||}upS4!ft_{4}),\langle\rangle,\sigma_{j}{::}\langle\rangle)$$\overline{n}_{i}:SDN,\langle\rangle,\sigma_{j}{::}\langle\rangle)$$\mathbf{rcfg(upS6,ft_{6})}$$\mathbf{rcfg(upS4,ft_{4})}$pt$(\sigma_{2},\sigma_{j})$$j\in\\{2,6,8,11,15\\}$$(\sigma_{2},\sigma_{i})$$i\in\\{2,6,8,12,16\\}$
Figure 12: Independent Controllers LTS (excerpt)

$\footnotesize{\begin{array}[]{r@{}c@{}ll}\lx@intercol\textnormal{for
$p,q,r\in\textnormal{DyNetKAT}$ and
$z,y\in{\textnormal{NetKAT}^{-{\bf{dup}}}}$}\hfil\lx@intercol\\\
\lx@intercol\textnormal{for }a::=z\mid x?z\mid
x!z\mid\mathbf{rcfg}_{x,z}\hfil\lx@intercol\\\
\mathbf{0}{}\mathop{;}p&\,\equiv&\bot&(A0)\\\
(z+y)\mathop{;}p&\,\equiv&z\mathop{;}p\oplus y\mathop{;}p&(A1)\\\ p\oplus
q&\,\equiv&q\oplus p&(A2)\\\ (p\oplus q)\oplus r&\,\equiv&p\oplus(q\oplus
r)&(A3)\\\ p\oplus p&\,\equiv&p&(A4)\\\ p\oplus\bot&\,\equiv&p&(A5)\\\
p\mathop{||}q&\,\equiv&q\mathop{||}p&(A6)\\\
p\mathop{||}\bot&\,\equiv&p&(A7)\\\ p\mathop{||}q&\,\equiv&p\llfloor q\oplus
q\llfloor p\oplus p\mid q&(A8)\\\ \bot\llfloor p&\,\equiv&\bot&(A9)\\\
(a\mathop{;}p)\llfloor q&\,\equiv&a\mathop{;}(p\mathop{||}q)&(A10)\\\ (p\oplus
q)\llfloor r&\,\equiv&(p\llfloor r)\oplus(q\llfloor r)&(A11)\\\
(x?\mathit{z}\mathop{;}p)\mid(x!\mathit{z}\mathop{;}q)&\,\equiv&\mathbf{rcfg}_{x,z}\mathop{;}(p\mathop{||}q)&(A12)\\\
(p\oplus q)\mid r&\,\equiv&(p\mid r)\oplus(q\mid r)&(A13)\\\ p\mid
q&\,\equiv&q\mid p&(A14)\\\ p\mid q&\,\equiv&\bot~{}[owise]&(A15)\\\
\end{array}}$

$\footnotesize{\begin{array}[]{r@{}c@{}ll}&&&\\\ \lx@intercol\textnormal{for
$\mathit{at}::=\alpha\cdot\pi\mid x?\mathit{z}\mid
x!\mathit{z}\mid\mathbf{rcfg}_{x,z}$:}\hfil\lx@intercol\\\
\delta_{{\mathcal{L}}}(\bot)&\,\equiv&\bot&(\delta_{\bot})\\\
\delta_{{\mathcal{L}}}(\mathit{at}\mathop{;}p)&\,\equiv&\mathit{at}\mathop{;}\delta_{{\mathcal{L}}}(p)~{}{\textnormal{if}}~{}\mathit{at}\not\in{\mathcal{L}}&(\delta_{\mathop{;}})\\\
\delta_{{\mathcal{L}}}(\mathit{at}\mathop{;}p)&\,\equiv&\bot~{}{\textnormal{if}}~{}\mathit{at}\in{\mathcal{L}}&(\delta_{\mathop{;}}^{\bot})\\\
\delta_{{\mathcal{L}}}(p\oplus
q)&\,\equiv&\delta_{{\mathcal{L}}}(p)\oplus\delta_{{\mathcal{L}}}(q)&(\delta_{\oplus})\\\
&&&\\\ \lx@intercol\textnormal{for $n\in\mathbb{N}:$}\hfil\lx@intercol\\\
\pi_{0}(p)&\,\equiv&\bot&(\Pi_{0})\\\
\pi_{n}(\bot)&\,\equiv&\bot&(\Pi_{\bot})\\\
\pi_{n+1}(\mathit{at}\mathop{;}p)&\,\equiv&\mathit{at}\mathop{;}\pi_{n}(p)&(\Pi_{\mathop{;}})\\\
\pi_{n}(p\oplus q)&\,\equiv&\pi_{n}(p)\oplus\pi_{n}(q)&(\Pi_{\oplus})\\\
&&&\\\ p&\,\equiv&q\hfill~{}{\textnormal{if}}~{}\forall
n\in\mathbb{N}\,:\,\pi_{n}(p)\,\equiv\,\,\pi_{n}(q)&({\it AIP})\\\ \\\
E_{\textit{NK}}&&\\\ \end{array}}$

Figure 13: The axiom system $E_{\textit{DNK}}$ (including $E_{\textit{NK}}$)

##  III Semantic Results

In this section we define bisimilarity of DyNetKAT policies and provide a
corresponding sound and ground-complete axiomatization.

Bisimilarity of DyNetKAT terms is defined in the standard fashion:

######  Definition 2 (Bisimilarity ($\sim$))

A symmetric relation $R$ over DyNetKAT policies is a _bisimulation_ whenever
for $(p,q)\in R$ the following holds:
If
$(p,H_{0},H_{1})\xrightarrow{\gamma}(p^{\prime},H^{\prime}_{0},H^{\prime}_{1})$
then exists $q^{\prime}$ s.t.
$(q,H_{0},H_{1})\xrightarrow{\gamma}(q^{\prime},H^{\prime}_{0},H^{\prime}_{1})$
and $(p^{\prime},q^{\prime})\in R$, with
$\gamma::=(\sigma,\sigma^{\prime})\mid x?r\mid x!r\mid\mathbf{rcfg(x,r)}$.

We call _bisimilarity_ the largest bisimulation relation. Two policies $p$ and
$q$ are _bisimilar_ ($p\sim q$) if and only if there is a bisimulation
relation $R$ such that $(p,q)\in R$.

Semantic equivalence of $\textnormal{NetKAT}^{-{\bf{dup}}}$ policies is
preserved by DyNetKAT bisimilarity.

######  Proposition 1 (Semantic Layering)

Let $p$ and $q$ be two $\textnormal{NetKAT}^{-{\bf{dup}}}$ policies. The
following holds: $\llbracket p\rrbracket=\llbracket q\rrbracket\textnormal{
iff }(p;d)\sim(q;d)$ for any DyNetKAT policy $d$.

###### Proof 1

This follows according to the definition of bisimilarity and
$\mathbf{(cpol_{\\_\mathop{;}}^{\checkmark})}$ in Figure 10.

We further provide some additional ingredients needed to introduce the
DyNetKAT axiomatization in Figure 13. First, note that our notion of
bisimilarity identifies synchronization steps as in
$\mathbf{(cpol_{\clubsuit\spadesuit})}$ in Figure 10. At the axiomatization
level, this requires introducing corresponding constants $\mathbf{rcfg}_{x,z}$
defined as:

$\frac{\raisebox{3.01385pt}{\normalsize{$$}}}{\raisebox{-4.30554pt}{\normalsize{$(\mathbf{rcfg}_{x,z};p,H_{0},H_{1})\,\,{{\xrightarrow{\mathbf{rcfg(x,z)}}}}\,\,(p,H_{0},H_{1})$}}}.$

In accordance with standard approaches to process algebra (see, e.g., [1, 3])
we consider the restriction operator $\delta_{\mathcal{L}}(-)$ with
${\mathcal{L}}$ a set of forbidden actions ranging over $x?z$ and $x!z$ as in
(1). In practice, we use the restriction operator to force synchronous
communication. We also define a projection operator $\pi_{n}(-)$ that,
intuitively, captures the first $n$ steps of a DyNetKAT policy. $\pi_{n}(-)$
is crucial for defining the so-called “Approximation Induction Principle” that
enables reasoning about equivalence of recursive DyNetKAT specifications.
Last, but not least, in our axiomatization we employ the left-merge operator
($\llfloor$) and the communication-merge operator ($\mid$) utilised for
axiomatizing parallel composition. Intuitively, a process of shape $p\llfloor
q$ behaves like $p$ as a first step, and then continues as the parallel
composition between the remaining behaviour of $p$ and $q$. A process of shape
$p\mid q$ forces the synchronous communication between $p$ and $q$ in a first
step, and then continues as the parallel composition between the remaining
behaviours of $p$ and $q$. The full description of these auxiliary operators
is provided in [6].

In Figure 13, we introduce $E_{\textit{DNK}}$ – the axiom system of DyNetKAT,
including the NetKAT axiomatization $E_{\textit{NK}}$. Most of the axioms in
Figure 13 comply to the standard axioms of parallel and communicating
processes [3], where, intuitively, $\oplus$ plays the role of non-
deterministic choice, ; resembles sequential composition and $\bot$ is a
process that deadlocks. An interesting axiom is $(A7):\,p\mathop{||}\bot\equiv
p$ which, intuitively, states that if one network component fails, then the
whole system continues with the behaviour of the remaining components. This is
a departure from the approach in [13], where recovery is not possible in case
of a component’s failure; i.e., $e\mathop{||}0\equiv 0$. Additionally, $(A12)$
“pin-points” a communication step via the newly introduced constants of form
$\mathbf{rcfg}_{x,z}$. Axiom $(A0)$ states that if the current packet is
dropped as a result of the unsuccessful evaluation of a NetKAT policy, then
the continuation is deadlocked. $(A1)$ enables mapping the non-deterministic
choice at the level of NetKAT to the setting of DyNetKAT.

The axioms encoding the restriction operator $\delta_{\mathcal{L}}(-)$ and the
projection operator $\pi_{n}(-)$ are defined in the standard fashion, on top
of DyNetKAT normal forms. The latter are defined inductively, as sums of
complete tests and complete assignments $\alpha\cdot\pi$, or communication
steps $x?q,\,x!q$ and $\mathbf{rcfg}_{x,q}$, followed by arbitrary DyNetKAT
policies:

$\Sigma^{\oplus}_{i\in
I}(\alpha_{i}\cdot\pi_{i});d_{i}\,\oplus\,\Sigma^{\oplus}_{j\in
J}c_{j};d_{j}\,(\oplus\bot)$

where $d_{i},d_{j}$ range over DyNetKAT policies and $c_{j}::=x?q\mid
x!q\mid\mathbf{rcfg}_{x,q}$ with $q$ denoting terms in
$\textnormal{NetKAT}^{-{\bf{dup}}}$. Complete tests (typically denoted by
$\alpha$) and complete assignments (typically denoted by $\pi$) were
originally introduced in [2]. In short: let $F=\\{f_{1},\ldots,f_{n}\\}$ be a
set of fields names with values in $V_{i}$, for $i\in\\{1,\ldots,n\\}$. We
call _complete test_ (resp., _complete assignment_) an expression
$f_{1}=v_{1}\cdot\ldots\cdot f_{n}=v_{n}$ (resp., $f_{1}\leftarrow
v_{1}\cdot\ldots\cdot f_{n}\leftarrow v_{n}$), with $v_{i}\in V_{i}$, for
$i\in\\{1,\ldots,n\\}$.

######  Theorem 1 (Soundness & Completeness)

$E_{\textit{DNK}}$ is sound and ground-complete with respect to DyNetKAT
bisimilarity.

###### Proof 2

The proof of soundness follows in two steps. First, we show that axioms
$(A0)$-$(\Pi_{\oplus})$ together with the NetKAT axioms in $E_{\textit{NK}}$
are sound w.r.t. DyNetKAT bisimilarity. This is shown in a standard fashion,
by case analysis on transitions of shape
$(p,H_{0},H^{\prime}_{0})\xrightarrow{\gamma}(q,H_{1},H^{\prime}_{1})$ with
$\gamma::=(\sigma,\sigma^{\prime})\mid x?n\mid x!n\mid\mathbf{rcfg(x,n)}$.
Then, we show that $(AIP)$ holds; the proof is close to the one of Theorem
$2.5.8$ in [3] and uses the branching finiteness property of guarded DyNetKAT
policies.

Given two bisimilar DyNetKAT policies $p$ and $q$ in normal form, ground-
completeness reduces to showing that every summand of $p$ can be proven
syntactically equal to a summand of $q$. The reasoning is by structural
induction, and case analysis on the type of transitions that can be triggered
as a first step. For showing the existence of DyNetKAT normal forms, we
exploit the results of Lemma $4$ in [2] stating that the standard semantics of
every NetKAT expression is equal to the union of its minimal nonzero terms. In
the context of $\textnormal{NetKAT}^{-{\bf{dup}}}$ and packet values drawn
from finite domains (as is the case in [2]), this union can be equivalently
expressed as a sum of complete tests and complete assignments. I.e., $\vdash
r\equiv\Sigma_{i\in I}\alpha_{i}\cdot\pi_{i}$ for every
$\textnormal{NetKAT}^{-{\bf{dup}}}$ expression $r$. We refer to [6] for the
complete proof and additional details.

In this section we define bisimilarity of DyNetKAT policies, introduce some
necessary definitions and terminology, and provide a corresponding sound and
complete axiomatization.

###  III-A An Axiom System for DyNetKAT Bisimilarity

Bisimilarity of DyNetKAT terms is defined in the standard fashion:

######  Definition 3 (Bisimilarity ($\sim$))

A symmetric relation $R$ over DyNetKAT policies is a _bisimulation_ whenever
for $(p,q)\in R$ the following holds:
If
$(p,H_{0},H_{1})\xrightarrow{\gamma}(p^{\prime},H^{\prime}_{0},H^{\prime}_{1})$
then exists $q^{\prime}$ s.t.
$(q,H_{0},H_{1})\xrightarrow{\gamma}(q^{\prime},H^{\prime}_{0},H^{\prime}_{1})$
and $(p^{\prime},q^{\prime})\in R$, with
$\gamma::=(\sigma,\sigma^{\prime})\mid x?r\mid x!r\mid\mathbf{rcfg(x,r)}$.

We call _bisimilarity_ the largest bisimulation relation.

Two policies $p$ and $q$ are _bisimilar_ ($p\sim q$) if and only if there is a
bisimulation relation $R$ such that $(p,q)\in R$.

Semantic equivalence of $\textnormal{NetKAT}^{-{\bf{dup}}}$ policies is
preserved by DyNetKAT bisimilarity.

######  Proposition 2 (Semantic Layering)

Let $p$ and $q$ be two $\textnormal{NetKAT}^{-{\bf{dup}}}$ policies. The
following holds:

$\llbracket p\rrbracket=\llbracket q\rrbracket\textnormal{ iff
}(p;d)\sim(q;d)$

for any DyNetKAT policy $d$.

###### Proof 3

The result follows directly according to the definition of bisimilarity and
$\mathbf{(cpol_{\\_\mathop{;}}^{\checkmark})}$ in Figure 10.

Next, we introduce the restriction operator $\delta_{\mathcal{L}}(-)$ [1, 3],
with ${\mathcal{L}}$ a set of forbidden actions ranging over $x?z$ and $x!z$
as in (1). The semantics of $\delta_{\mathcal{L}}(-)$ is:

$\mathbf{({\delta})}\frac{\raisebox{3.01385pt}{\normalsize{$(p,H_{0},H_{1})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H^{\prime}_{0},H^{\prime}_{1})$}}}{\raisebox{-4.30554pt}{\normalsize{$(\delta_{\mathcal{L}}(p),H_{0},H_{1})\,\,{{\xrightarrow{\gamma}}}\,\,(\delta_{\mathcal{L}}(p^{\prime}),H^{\prime}_{0},H^{\prime}_{1})$}}}\gamma\not\in\mathcal{L}$
(2)

In practice, we use the restriction operator to force synchronous
communication. For an example, consider the synchronising controllers in
Figure 8. Let $\mathcal{L}$ be the set of restricted actions ranging over
elements of shape $upS_{i}?X$, $upS_{i}!X$, $syn?1$ and $syn!1$. The
restricted system
$\delta_{\mathcal{L}}(\mathit{SDN}_{S1,\ldots,S6}\mathop{||}C_{1}\mathop{||}C_{2})$
ensures that: (1) traffic through $S2$ and $S1$ is first disabled via
reconfigurations $\mathbf{rcfg(upS2,0)}$ and $\mathbf{rcfg(upS1,0)}$ and (2)
the controllers acknowledge this deactivation via a synchronization step
$\mathbf{rcfg(syn,1)}$ before installing further flow tables for $S4$ and
$S6$.

In the style of [3], we define a projection operator $\pi_{n}(-)$ that,
intuitively, captures the first $n$ steps of a DyNetKAT policy. Its formal
semantics is:

$\mathbf{({\pi})}\frac{\raisebox{3.01385pt}{\normalsize{$(p,H_{0},H_{1})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H^{\prime}_{0},H^{\prime}_{1})$}}}{\raisebox{-4.30554pt}{\normalsize{$(\pi_{n+1}(p),H_{0},H_{1})\,\,{{\xrightarrow{\gamma}}}\,\,(\pi_{n}(p^{\prime}),H^{\prime}_{0},H^{\prime}_{1})$}}}$
(3)

As we shall later see, $\pi_{n}(-)$ is crucial for defining the so-called
“Approximation Induction Principle” that enables reasoning about equivalence
of recursive DyNetKAT specifications.

We further provide some additional ingredients needed to introduce the
DyNetKAT axiomatization in Figure 13. First, note that our notion of
bisimilarity identifies synchronization steps as in $\mathbf{(cpol_{!?})}$ and
$\mathbf{(cpol_{?!})}$. At the axiomatization level, this requires introducing
corresponding constants $\mathbf{rcfg}_{x,z}$ defined as:

$\mathbf{(\mathbf{rcfg}_{x,z})}\frac{\raisebox{3.01385pt}{\normalsize{$$}}}{\raisebox{-4.30554pt}{\normalsize{$(\mathbf{rcfg}_{x,z};p,H_{0},H_{1})\,\,{{\xrightarrow{\mathbf{rcfg(x,z)}}}}\,\,(p,H_{0},H_{1})$}}}$
(4)

Last, but not least, we introduce the left-merge operator ($\llfloor$) and the
communication-merge operator ($\mid$) utilised for axiomatizing parallel
composition. Intuitively, a process of shape $p\llfloor q$ behaves like $p$ as
a first step, and then continues as the parallel composition between the
remaining behaviour of $p$ and $q$. A process of shape $p\mid q$ forces the
synchronous communication between $p$ and $q$ in a first step, and then
continues as the parallel composition between the remaining behaviours of $p$
and $q$. The corresponding semantic rules are:

$\begin{array}[]{l}\mathbf{(\llfloor)}\frac{\raisebox{2.1097pt}{\normalsize{$(p,{H_{0},H_{1}})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H^{\prime}_{0},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(p\llfloor
q,H_{0},H_{1}))\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime}\mathop{||}q,H^{\prime}_{0},H^{\prime}_{1})$}}}~{}~{}~{}~{}\gamma::=(\sigma,\sigma^{\prime})\mid
x!p\mid x?p\mid\mathbf{rcfg(x,p)}\\\\[12.91663pt]
\mathbf{(\mid^{?!})}\frac{\raisebox{2.1097pt}{\normalsize{$(p,H,H^{\prime})\,\,{{\xrightarrow{x?r}}}\,\,(p^{\prime},H,H^{\prime})\quad\quad(q,H,H^{\prime})\,\,{{\xrightarrow{x!r}}}\,\,(q^{\prime},H,H^{\prime})$}}}{\raisebox{-3.01389pt}{\normalsize{$(p\mid
q,H,H^{\prime})\,\,{{\xrightarrow{\mathbf{rcfg(x,p)}}}}\,\,(p^{\prime}\mathop{||}q^{\prime},H,H^{\prime})$}}}\\\\[12.91663pt]
\mathbf{(\mid^{!?})}\frac{\raisebox{2.1097pt}{\normalsize{$(p,H,H^{\prime})\,\,{{\xrightarrow{x!r}}}\,\,(p^{\prime},H,H^{\prime})\quad\quad(q,H,H^{\prime})\,\,{{\xrightarrow{x?r}}}\,\,(q^{\prime},H,H^{\prime})$}}}{\raisebox{-3.01389pt}{\normalsize{$(p\mid
q,H,H^{\prime})\,\,{{\xrightarrow{\mathbf{rcfg(x,p)}}}}\,\,(p^{\prime}\mathop{||}q^{\prime},H,H^{\prime})$}}}\end{array}$
(5)

From this point onward, we denote by DyNetKAT the extension with the operators
in (2), (3) and (4):

$\begin{array}[]{ccl}\mathit{N}&::=&{\textnormal{NetKAT}^{-{\bf{dup}}}}\\\\[4.30554pt]
\mathit{D}_{e}&::=&{\bot}\mid\mathit{N}\mathop{;}\mathit{D}\mid
x?\mathit{N}\mathop{;}D_{e}\mid
x!\mathit{N}\mathop{;}D_{e}\mid\mathbf{rcfg}_{x,N}\mathop{;}D_{e}\mid\\\
&&\mathit{D}_{e}\mathop{||}\mathit{D}_{e}\mid D_{e}\oplus
D_{e}\mid\delta_{\mathcal{L}}(D_{e})\mid\pi_{n}(D_{e})\mid D_{e}\llfloor
D_{e}\mid D_{e}\\!\\!\mid\\!\\!D_{e}\mid X\\\ &&X\triangleq
D_{e},\,n\in\mathbb{N},\,\mathcal{L}=\\{c\mid c::=x?N\mid
x!N\\}\par\end{array}$ (6)

Bisimilarity is defined for DyNetKAT terms as in (6) in the natural fashion,
according to the operational semantics of the new operators in (2), (3) and
(4).

###### Lemma 4

DyNetKAT bisimilarity is a _congruence_.

###### Proof 4

The result follows from the fact that the semantic rules defined in this paper
comply to the congruence formats proposed in [20].

######  Definition 5 (Complete Tests & Assignments [2])

Let $F=\\{f_{1},\ldots,f_{n}\\}$ be a set of fields names with values in
$V_{i}$, for $i\in\\{1,\ldots,n\\}$. We call _complete test_ (typically
denoted by $\alpha$) an expression $f_{1}=v_{1}\cdot\ldots\cdot f_{n}=v_{n}$,
with $v_{i}\in V_{i}$, for $i\in\\{1,\ldots,n\\}$. We call _complete
assignment_ (typically denoted by $\pi$) an expression $f_{1}\leftarrow
v_{1}\cdot\ldots\cdot f_{n}\leftarrow v_{n}$, with $v_{i}\in V_{i}$, for
$i\in\\{1,\ldots,n\\}$. We sometimes write $\alpha_{\pi}$ in order to denote
the complete test derived from the complete assignment $\pi$ by replacing all
$f_{i}\leftarrow v_{i}$ in $\pi$ with $f_{i}=v_{i}$; symmetrically for
$\pi_{\alpha}$. Additionally, we sometimes write $\sigma_{\alpha}$ to denote
the network packet whose fields are assigned the corresponding values in
$\alpha$; symmetrically for $\sigma_{\pi}$.

In Figure 13, we introduce $E_{\textit{DNK}}$ – the axiom system of DyNetKAT,
including the NetKAT axiomatization $E_{\textit{NK}}$. Most of the axioms in
Figure 13 comply to the standard axioms of parallel and communicating
processes [3], where, intuitively, $\oplus$ plays the role of non-
deterministic choice, ; resembles sequential composition and $\bot$ is a
process that deadlocks.

For instance, axioms $(A2)-(A5)$ encode the ACI properties of $\oplus$
together with the fact that $\bot$ is the neutral element.

Axioms $(A8)-(A15)$ define parallel composition ($\mathop{||}$) in terms of
left-merge ($\llfloor$) and communication-merge ($\,\mid\,$) in the standard
fashion. Additionally, $(A12)$ “pin-points” a communication step via the newly
introduced constants of form $\mathbf{rcfg}_{x,z}$. An interesting axiom is
$(A7):\,p\mathop{||}\bot\equiv p$ which, intuitively, states that if one
network component fails, then the whole system continues with the behaviour of
the remaining components. This is a departure from the approach in [13], where
recovery is not possible in case of a component’s failure; i.e.,
$e\mathop{||}0\equiv 0$.

Axiom $(A0)$ states that if the current packet is dropped as a result of the
unsuccessful evaluation of a NetKAT policy, then the continuation is
deadlocked. $(A1)$ enables mapping the non-deterministic choice at the level
of NetKAT to the setting of DyNetKAT.

The axioms encoding the restriction operator $\delta_{\mathcal{L}}(-)$ and the
projection operator $\pi_{n}(-)$ are defined in the standard fashion, on top
of DyNetKAT normal forms later defined in this section. Intuitively, normal
forms are defined inductively, as sums of complete tests and complete
assignments $\alpha\cdot\pi$, or communication steps $x?q,\,x!q$ and
$\mathbf{rcfg}_{x,q}$, followed by arbitrary DyNetKAT policies.

Last, but not least, $(AIP)$ corresponds to the so-called “Approximation
Induction Principle”, and it provides a mechanism for reasoning on the
equivalence of recursive behaviours, up to a certain limit denoted by $n$.

####  III-A1 Soundness and Completeness

In what follows, we show that the axiom system $E_{\textit{DNK}}$ is sound and
ground-complete with respect to DyNetKAT bisimilarity.

We proceed by first defining a notion of normal forms of DyNetKAT terms,
together with a notion of guardedness and a statement about the branching
finiteness of guarded DyNetKAT processes.

######  Lemma 6 ($\textnormal{NetKAT}^{-{\bf{dup}}}$ Normal Forms)

We call a $\textnormal{NetKAT}^{-{\bf{dup}}}$ policy $q$ in _normal form_
(n.f.) whenever $q$ is of shape
$\Sigma_{\alpha\cdot\pi\in\mathcal{A}}\alpha\cdot\pi$ with
$\mathcal{A}=\\{\alpha_{i}\cdot\pi_{i}\mid i\in I\\}$. For every
$\textnormal{NetKAT}^{-{\bf{dup}}}$ policy $p$ there exists a
$\textnormal{NetKAT}^{-{\bf{dup}}}$ policy $q$ in n.f. such that
$E_{\textit{NK}}\vdash p\equiv q$.

###### Proof 5

The result follows by Lemma $4$ in [2], stating that:

$\llbracket p\rrbracket=\bigcup_{x\in G(p)}\llbracket x\rrbracket$ (7)

where $G(p)$ defines the language model of NetKAT terms. Let $A$ be the set of
all complete tests, and $\Pi$ be the set of all complete assignments.
Similarly to [2], we consider network packets with values in finite domains.
Consequently, $A$ and $\Pi$ are finite. In [2], $G(p)$ is defined as a set
with elements in $A\cdot(\Pi\cdot\textbf{dup})^{*}\cdot\Pi$. Recall that, in
our setting, we work with the dup-free fragment of NetKAT. Hence, $G(p)$ is a
finite set of shape $G=\\{\alpha_{i}\cdot\pi_{i}\mid i\in I,\alpha_{i}\in
A,\pi_{i}\in\Pi\\}$. Based on the definition of $\llbracket-\rrbracket$ and
(7) it follows that:

$\llbracket p\rrbracket=\llbracket\Sigma_{\alpha\cdot\pi\in
G}\alpha\cdot\pi\rrbracket$ (8)

Therefore, by the completeness of NetKAT, it holds that:
$E_{\textit{NK}}\vdash p\equiv\Sigma_{\alpha\cdot\pi\in G}\alpha\cdot\pi$. In
other words, $p$ can be reduced to a term in n.f.

######  Definition 7 (DyNetKAT Normal Forms)

We call a DyNetKAT policy in _normal form_ (n.f.) if it is of shape

$\Sigma^{\oplus}_{i\in
I}(\alpha_{i}\cdot\pi_{i});d_{i}\oplus\Sigma^{\oplus}_{j\in
J}c_{j};d_{j}\,(\oplus\bot)$

where $d_{i},d_{j}$ range over DyNetKAT policies and $c_{j}::=x?q\mid
x!q\mid\mathbf{rcfg}_{x,q}$ with $q$ denoting terms in
$\textnormal{NetKAT}^{-{\bf{dup}}}$.

######  Definition 8 (Guardedness)

A DyNetKAT policy $p$ is _guarded_ if and only if all occurrences of all
variables $X$ in $p$ are _guarded_. An occurrence of a variable $X$ in a
policy $p$ is _guarded_ if and only if (i) $p$ has a subterm of shape
$p^{\prime};t$ such that either $p^{\prime}$ is variable-free, or all the
occurrences of variables $Y$ in $p^{\prime}$ are guarded, and $X$ occurs in
$t$, or (ii) if $p$ is of shape $y?X;t$, $y!X;t$ or $\mathbf{rcfg}_{X,t}$.

######  Lemma 9 (Branching Finiteness)

All guarded DyNetKAT policies are finitely branching.

######  Lemma 10 (DyNetKAT Normalization)

$E_{\textit{DNK}}$ is normalising for DyNetKAT. In other words, for every
guarded DyNetKAT policy $p$ there exists a DyNetKAT policy $q$ in n.f. such
that $E_{\textit{DNK}}\vdash p\equiv q$.

###### Proof 6

The proof follows from Lemma 6 and $(A1):\,(z+y);p\equiv z;p\oplus y;p$ in a
standard fashion, by structural induction.
_Base cases._

  * •

$p\triangleq\bot$ trivially holds

  * •

$p\triangleq q;d$ with $q$ a $\textnormal{NetKAT}^{-{\bf{dup}}}$ term holds by
Lemma 6 and $(A1)$

  * •

$p\triangleq c;d$ with $c::=x?q\mid x!q\mid\mathbf{rcfg}_{x,q}$ trivially
holds

_Induction step._

  * •

$p\triangleq p_{1}\oplus p_{2}$ $p\triangleq X$ \- case discarded, as $p$ is
not guarded

  * •

$p\triangleq p_{1}\llfloor p_{2}$ $p\triangleq\pi_{n}(^{\prime})$

  * •

$p\triangleq p_{1}\,\mid\,p_{2}$ $p\triangleq\delta_{\mathcal{L}}(p^{\prime})$

  * •

$p\triangleq p_{1}\mathop{||}p_{2}$

All items above follow by the axiom system $E_{\textit{DNK}}$ and the
induction hypothesis, under the assumption that $p_{1},p_{2}$ and $p^{\prime}$
are guarded.

For simplicity, in what follows, we assume that DyNetKAT policies are guarded.

######  Lemma 11 (Soundness of $E_{\textnormal{DyNetKAT}\setminus AIP}$)

Let $E_{\textnormal{DyNetKAT}\setminus AIP}$ stand for the axiom system
$E_{\textit{DNK}}$ in Figure 13, without the axiom $(AIP)$.
$E_{\textnormal{DyNetKAT}\setminus AIP}$ is sound for DyNetKAT bisimilarity.

###### Proof 7

The proof reduces to showing that for all $p$, $q$ DyNetKAT policies, the
following holds: If $E_{\textnormal{DyNetKAT}\setminus AIP}\vdash p\equiv q$
then $p\sim q$. This is proven in a standard fashion, by case analysis on
transitions of shape

$(p,H_{0},H^{\prime}_{0})\xrightarrow{\gamma}(q,H_{1},H^{\prime}_{1})$

with $\gamma::=(\sigma,\sigma^{\prime})\mid x?n\mid
x!n\mid\mathbf{rcfg(x,n)}$, according to the semantic rules in Figure 10, (2),
(3), (4) and (5).

For an example, consider $(A1)$ and $(A12)$ in Figure 13; the proof of
soundness for these axioms are given in the following. The soundness proofs
for the rest of the axioms are provided in Appendix -A.

  * •

Axiom under consideration:

$(z+y)\mathop{;}p\equiv z\mathop{;}p\oplus y\mathop{;}p\quad(A1)$ (9)

for $z,y\in{\textnormal{NetKAT}^{-{\bf{dup}}}}$ and
$p\in{\textnormal{DyNetKAT}}$. Consider an arbitrary but fixed network packet
$\sigma$, let $S_{z}\triangleq\llbracket
z\rrbracket(\sigma\\!\\!::\\!\\!\langle\rangle)$, $S_{y}\triangleq\llbracket
y\rrbracket(\sigma\\!\\!::\\!\\!\langle\rangle)$ and
$S_{zy}\triangleq\llbracket
z+y\rrbracket(\sigma\\!\\!::\\!\\!\langle\rangle)$. According to the semantic
rules of DyNetKAT, the derivations of the term $(z+y)\mathop{;}p$ are as
follows:

    1. (a)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\textnormal{For all
}\sigma^{\prime}\in
S_{zy}:\quad\mathbf{(cpol_{\\_\mathop{;}}^{\checkmark}{})}&\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$((z+y);p,\sigma::H,H^{\prime})\,\,{{\xrightarrow{(\sigma,\sigma^{\prime})}}}\,\,(p,H,\sigma^{\prime}::H^{\prime})$}}}\\\
\end{array}$

Accordingly, the derivations of the term $z\mathop{;}p\oplus y\mathop{;}p$ are
as follows:

    1. (b)

$\begin{array}[]{r@{}r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\textnormal{For all
}\sigma^{\prime}\in
S_{z}:&\mathbf{(cpol_{\\_\mathop{;}}^{\checkmark}{})}&\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$(z;p,\sigma::H,H^{\prime})\,\,{{\xrightarrow{(\sigma,\sigma^{\prime})}}}\,\,(p,H,\sigma^{\prime}::H^{\prime})$}}}\\\
&\mathbf{(cpol_{\\_\oplus})}&\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$(z;p\oplus
y;p,\sigma::H,H^{\prime})\,\,{{\xrightarrow{(\sigma,\sigma^{\prime})}}}\,\,(p,H,\sigma^{\prime}::H^{\prime})$}}}\end{array}$

    2. (c)

$\begin{array}[]{r@{}r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\textnormal{For all
}\sigma^{\prime}\in
S_{y}:&\mathbf{(cpol_{\\_\mathop{;}}^{\checkmark}{})}&\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$(y;p,\sigma::H,H^{\prime})\,\,{{\xrightarrow{(\sigma,\sigma^{\prime})}}}\,\,(p,H,\sigma^{\prime}::H^{\prime})$}}}\\\
&\mathbf{(cpol_{\oplus\\_})}&\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$(z;p\oplus
y;p,\sigma::H,H^{\prime})\,\,{{\xrightarrow{(\sigma,\sigma^{\prime})}}}\,\,(p,H,\sigma^{\prime}::H^{\prime})$}}}\end{array}$

As demonstrated in (a) and (b), (c), both of the terms $(z+y)\mathop{;}p$ and
$z\mathop{;}p\oplus y\mathop{;}p$ initially only afford a transition of shape
$(\sigma,\sigma^{\prime})$ and they converge into the same expression after
taking that transition:

$\displaystyle((z+y);p,\sigma::H,H^{\prime})\,\,{{\xrightarrow{(\sigma,\sigma^{\prime})}}}\,\,$
$\displaystyle(p,H,\sigma^{\prime}::H^{\prime})$ (10)
$\displaystyle(z\mathop{;}p\oplus
y\mathop{;}p,\sigma::H,H^{\prime})\,\,{{\xrightarrow{(\sigma,\sigma^{\prime})}}}\,\,$
$\displaystyle(p,H,\sigma^{\prime}::H^{\prime})$ (11)

In the case of the term $(z+y)\mathop{;}p$, the possible values for the
$\sigma^{\prime}$ ranges over $S_{zy}$. Whereas for the term
$(z+y)\mathop{;}p$, the possible values for the $\sigma^{\prime}$ ranges over
$S_{z}\cup S_{y}$. However, observe that $S_{zy}$ is equal to $S_{z}\cup
S_{y}$:

$\displaystyle S_{zy}$ $\displaystyle=\llbracket
z+y\rrbracket(\sigma\\!\\!::\\!\\!\langle\rangle)$
$\displaystyle(\textnormal{Definition of }S_{zy})$ (12)
$\displaystyle=\llbracket
z\rrbracket(\sigma\\!\\!::\\!\\!\langle\rangle)\cup\llbracket
y\rrbracket(\sigma\\!\\!::\\!\\!\langle\rangle)\quad$
$\displaystyle(\textnormal{Definition of }+)$ (13) $\displaystyle=S_{z}\cup
S_{y}$ $\displaystyle(\textnormal{Definition of }S_{z}\textnormal{ and
}S_{y})$ (14)

Hence, it is straightforward to conclude that the following holds:

$((z+y)\mathop{;}p)\sim(z\mathop{;}p\oplus y\mathop{;}p)$ (15)

  * •

Axiom under consideration:

$(x?\mathit{z}\mathop{;}p)\mid(x!\mathit{z}\mathop{;}q)\equiv\mathbf{rcfg}_{x,z}\mathop{;}(p\mathop{||}q)\quad(A12)$
(16)

for $p,q\in{\textnormal{DyNetKAT}}$. The derivations of the term
$(x?\mathit{z}\mathop{;}p)\mid(x!\mathit{z}\mathop{;}q)$ are as follows:

    1. (a)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\mathbf{(cpol_{?})}&\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$(x?z;p,H,H^{\prime})\,\,{{\xrightarrow{x?z}}}\,\,(p,H,H^{\prime})$}}}&&\mathbf{(cpol_{!})}&\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$(x!z;q,H,H^{\prime})\,\,{{\xrightarrow{x!z}}}\,\,(q,H,H^{\prime})$}}}\\\
<EMAIL_ADDRESS>300.00046pt\ignorespaces$}}}{\raisebox{-3.01389pt}{\normalsize{$((x?\mathit{z}\mathop{;}p)\mid(x!\mathit{z}\mathop{;}q),H,H^{\prime})\,\,{{\xrightarrow{\mathbf{rcfg(x,z)}}}}\,\,(p\mathop{||}q,H,H^{\prime})$}}}\hfil\end{array}$

The derivations of the term $\mathbf{rcfg}_{x,z}\mathop{;}(p\mathop{||}q)$ are
as follows:

    1. (b)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\mathbf{(\mathbf{rcfg}_{x,z})}&\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$(\mathbf{rcfg}_{x,z}\mathop{;}(p\mathop{||}q),H,H^{\prime})\,\,{{\xrightarrow{\mathbf{rcfg(x,z)}}}}\,\,(p\mathop{||}q,H,H^{\prime})$}}}\end{array}$

As demonstrated in (a) and (b), both of the terms
$(x?\mathit{z}\mathop{;}p)\mid(x!\mathit{z}\mathop{;}q)$ and
$\mathbf{rcfg}_{x,z}\mathop{;}(p\mathop{||}q)$ initially only afford the
transition $\mathbf{rcfg(x,z)}$ and they converge into the same expression
after taking that transition:

$\displaystyle((x?\mathit{z}\mathop{;}p)\mid(x!\mathit{z}\mathop{;}q),H,H^{\prime})\,\,{{\xrightarrow{\mathbf{rcfg(x,z)}}}}\,\,$
$\displaystyle(p\mathop{||}q,H,H^{\prime})$ (17)
$\displaystyle(\mathbf{rcfg}_{x,z}\mathop{;}(p\mathop{||}q),H,H^{\prime})\,\,{{\xrightarrow{\mathbf{rcfg(x,z)}}}}\,\,$
$\displaystyle(p\mathop{||}q,H,H^{\prime})$ (18)

Hence, it is straightforward to conclude that the following holds:

$((x?\mathit{z}\mathop{;}p)\mid(x!\mathit{z}\mathop{;}q))\sim(\mathbf{rcfg}_{x,z}\mathop{;}(p\mathop{||}q)).$
(19)

######  Lemma 12 (Soundness of $AIP$)

The Approximation Induction Principle $(AIP)$ is sound for DyNetKAT
bisimilarity.

###### Proof 8

The proof is close to the one of Theorem $2.5.8$ in [3] and uses the branching
finiteness property of DyNetKAT policies in Lemma 9. Assume two DyNetKAT
policies $p,p^{\prime}$ such that

$\forall n\in\mathbb{N}:\pi_{n}(p)\equiv\pi_{n}(p^{\prime})$ (20)

By Lemma 11 it follows that

$\forall n\in\mathbb{N}:\pi_{n}(p)\sim\pi_{n}(p^{\prime})$ (21)

We want to prove that $p\sim p^{\prime}$. The idea is to build a bisimulation
relation $R$ such that $(p,p^{\prime})\in R$. We define $R$ as follows:

$R=\\{(t,t^{\prime})\mid\forall
n\in\mathbb{N}:\pi_{n}(t)\sim\pi_{n}(t^{\prime})\\}$ (22)

Without loss of generality, assume that $p$ and $p^{\prime}$ are in n.f.
Assume $(p,p^{\prime})\in R$ and

$(p,H_{0},H^{\prime}_{0})\xrightarrow{\gamma}(p_{1},H_{1},H^{\prime}_{1})$
(23)

Next, for all $n>0$, define

$S_{n}=\\{p^{\prime}_{1}\mid(p^{\prime},H_{0},H^{\prime}_{0})\xrightarrow{\gamma}(p^{\prime}_{1},H_{1},H^{\prime}_{1})\textnormal{
and }\pi_{n}(p_{1})\sim\pi_{n}(p^{\prime}_{1})\\}$ (24)

The following hold:

  1. 1.

$S_{1}\supseteq S_{2}\ldots$ as if $\pi_{n+1}(p)\sim\pi_{n+1}(p^{\prime})$
then $\pi_{n}(p_{1})\sim\pi_{n}(p^{\prime}_{1})$. The latter is a
straightforward result derived according to the definition of $\sim$ and the
semantics of $\pi_{n}(-)$, under the assumption that $p,p^{\prime}$ are in
n.f.

  2. 2.

$S_{n}\not=\emptyset$ for all $n\geq 1$ since
$\pi_{n+1}(p)\sim\pi_{n+1}(p^{\prime})$ by (21) and
$(p,H_{0},H^{\prime}_{0})\xrightarrow{\gamma}(p_{1},H_{1},H^{\prime}_{1})$
according to (23)

  3. 3.

$S_{n}$ is finite, for all $n\in\mathbb{N}$, as $p^{\prime}$ is finitely
branching according to Lemma 9

Hence, the sequence $S_{1},S_{2},\ldots$ remains constant from some $n$ onward
and $\cap_{n\geq 0}S_{n}\not=\emptyset$. Let $p^{\prime}_{1}\in\cap_{n\geq
0}S_{n}$. It holds that:

  * •

$(p^{\prime},H_{0},H^{\prime}_{0})\xrightarrow{\gamma}(p^{\prime}_{1},H_{1},H^{\prime}_{1})$

  * •

$(p_{1},p^{\prime}_{1})\in R$ by the definition of $R$ and $S_{n}$

Symmetrically to (23), assume $(p,p^{\prime})\in R$ and
$(p^{\prime},H_{0},H^{\prime}_{0})\xrightarrow{\gamma}(p^{\prime}_{1},H_{1},H^{\prime}_{1})$.
By following a similar reasoning, we can show that:

  * •

$(p,H_{0},H^{\prime}_{0})\xrightarrow{\gamma}(p_{1},H_{1},H^{\prime}_{1})$

  * •

$(p_{1},p^{\prime}_{1})\in R$ by the definition of $R$ and $S_{n}$

Hence, $R$ is a bisimulation relation and $p\sim p^{\prime}$.

######  Theorem 2 (Soundness & Completeness)

$E_{\textit{DNK}}$ is sound and ground-complete for DyNetKAT bisimilarity.

###### Proof 9

Soundness: if $E_{\textit{DNK}}\vdash p\equiv q$ then $p\sim q$, follows from
Lemma 11 and Lemma 12.

Completeness: if $p\sim q$ then $E_{\textit{DNK}}\vdash p\equiv q$, is shown
as follows. Without loss of generality, assume $p$ and $q$ are in n.f.,
according to Lemma 10. We want to show that:

$\begin{array}[]{rcl}p&\equiv&q\oplus p\\\ q&\equiv&p\oplus q\end{array}$ (25)

which, by ACI of $\oplus$ implies $p\equiv q$. This reduces to showing that
every summand of $p$ is a summand of $q$ and vice-versa. We first argue that
every summand of $p$ is a summand of $q$. The reasoning is by structural
induction.
_Base case._

  * •

$p\triangleq\bot$. It holds by the hypothesis $p\sim q$ that
$q\triangleq\bot$.

_Induction step._

  * •

$p\triangleq((\alpha\cdot\pi);p^{\prime})\oplus p^{\prime\prime}$. Then,
$(p,\sigma_{\alpha}::H,H^{\prime})\xrightarrow{(\sigma_{\alpha},\sigma_{\pi})}(p^{\prime},H,\sigma_{\pi}::H^{\prime})$
implies by the hypothesis $p\sim q$ that
$(q,\sigma_{\alpha}::H,H^{\prime})\xrightarrow{(\sigma_{\alpha},\sigma_{\pi})}(q^{\prime},H,\sigma_{\pi}::H^{\prime})$
and $p^{\prime}\sim q^{\prime}$. Recall that $q$ is in n.f.; hence, by the
shape of the semantic rules in Figure 10 it holds that
$q\triangleq((\alpha\cdot\pi);q^{\prime})\oplus q^{\prime\prime}$. By the
induction hypothesis, it holds that $p^{\prime}\equiv q^{\prime}$ hence,
$(\alpha\cdot\pi);p^{\prime}$ is a summand of $q$ as well.

  * •

Cases $p\triangleq(c;p^{\prime})\oplus p^{\prime\prime}$ with $c::=x?n\mid
x!n\mid\mathbf{rcfg}_{x,n}$ follow in a similar fashion.

Hence, $p\equiv q\oplus p$ holds. The symmetric case $q\equiv p\oplus q$
follows the same reasoning.

##  IV A Framework for Safety

In this section we provide a language for specifying safety properties of
DyNetKAT networks, together with a procedure for reasoning about safety in an
equational fashion. Intuitively, safety properties enable specifying the
absence of undesired network behaviours.

######  Definition 13 (Safety Properties - Syntax)

Let $\mathcal{A}$ be an alphabet over letters of shape $\alpha\cdot\pi$ and
$\mathbf{rcfg}_{x,p}$, with $\alpha$ and $\pi$ ranging over complete tests and
assignments, and $\mathbf{rcfg}_{x,p}$ ranging over reconfiguration actions.
Safety properties are defined in the following fashion:

$\begin{array}[]{rcl}\mathit{act}&::=&\alpha\cdot\pi\mid\mathbf{rcfg}_{x,p}\mid\neg\mathit{act}~{}(\alpha\cdot\pi,\,\mathbf{rcfg}_{x,p}\in\mathcal{A})\\\
\mathit{regexp}&::=&\textit{true}\mid\mathit{act}\mid\mathit{regexp}+\mathit{regexp}\mid\mathit{regexp}\cdot\mathit{regexp}\mid\\\
&&(\mathit{regexp})^{n}~{}~{}(\textnormal{with }n\geq 1)\\\
\mathit{prop}&::=&[\mathit{regexp}]\mathit{false}\end{array}$

A safety property specification $\mathit{prop}$ is satisfied whenever the
behaviour encoded by regexp should not be observed within the network. Regular
expressions regexp are defined with respect to actions $\mathit{act}$: a flow
of shape $\alpha\cdot\pi$ is the observable behaviour of a
(${\textnormal{NetKAT}^{-{\bf{dup}}}}$) policy transforming a packet encoded
by $\alpha$ into $\alpha_{\pi}$, whereas $\mathbf{rcfg}_{x,p}$ corresponds to
a reconfiguration step in a network. Recursively, a sum of regular expressions
$\mathit{regexp}_{1}+\mathit{regexp}_{2}$ encodes the union of the two
behaviours, a concatenation of regular expressions
$\mathit{regexp}_{1}\cdot\mathit{regexp}_{2}$ encodes the behaviour of
$\mathit{regexp}_{1}$ followed by the behaviour of $\mathit{regexp}_{2}$. A
property of shape $[\neg a]\textit{false}$, with $a\in\mathcal{A}$, states
that the system cannot do anything apart from $a$ as a first step. The
property $[\textit{true}]\textit{false}$ states that no action can be observed
in the network, whereas $[\mathit{r}^{n}]\textit{false}$ encodes the repeated
application of $r$ for $n$ times.

The full semantics of safety property is provided in [6]. In short, the
semantic map
$\llbracket-\rrbracket:\mathit{Prop}\rightarrow\mathit{\textnormal{DyNetKAT}}$
associates to each property $[\textit{regexp}]\textit{false}$ as in Definition
20, a DyNetKAT process that can only execute sequences of actions outside the
scope of regexp. Typically, safety analysis is reduced to reachability
analysis. In our context, a safety property is violated whenever the network
system under analysis displays a (finite) execution that is not in the
behaviour of the property. Thus, the aforementioned semantic map is based on
traces (or words in $\mathcal{A}^{*}$) and is not sensitive to branching. This
paves the way to reasoning about the satisfiability of safety properties in an
equational fashion.

######  Definition 14 (Safe Network Systems)

Let $E_{\textit{DNK}}^{\textit{tr}}$ stand for the equational axioms in Figure
13, including the additional axiom that enables switching from the context of
bisimilarity to trace equivalence of DyNetKAT policies, namely: $p;(q\oplus
r)\equiv p;q\oplus p;r.$ Assume a specification given as the safety formula
$s$ and a network system implemented as the DyNetKAT policy $i$. We say that
the network is _safe_ whenever the following holds:
$E_{\textit{DNK}}^{\textit{tr}}\vdash\llbracket s\rrbracket\oplus
i\equiv\llbracket s\rrbracket.$ In words: checking whether $i$ satisfies $s$
reduces to checking whether the trace behaviour of $i$ is included into that
of $s$.

For an example, consider the firewall in Figure 1 and the corresponding
encoding in Figure 6. Recall that reaching int from ext without observing a
secure connection request is a faulty behaviour. This entails the safety
formula $s_{n}$ defined as
$[(\neg\mathbf{rcfg}_{\textit{secConReq},1})^{n}\cdot(\alpha\cdot\pi)]\textit{false}$,
for $n\in\mathbb{N}$, $\alpha\triangleq(\mathit{port}=\textit{ext})$ and
$\pi\triangleq(\mathit{port}\leftarrow\textit{int})$. Therefore, checking
whether the network is safe reduces to checking, for all $n\in\mathbb{N}$:
$E_{\textit{DNK}}^{\textit{tr}}\vdash\llbracket
s_{n}\rrbracket\oplus\mathit{Init}\equiv\llbracket s_{n}\rrbracket$. Note
that, for a fixed $n$, the verification procedure resembles bounded model
checking [4].

In this section we provide a language for specifying safety properties of
DyNetKAT networks, together with a procedure for reasoning about safety in an
equational fashion. Intuitively, safety properties enable specifying undesired
network behaviours.

######  Definition 15 (Safety Properties - Syntax)

Let $\mathcal{A}$ be an alphabet over letters of shape $\alpha\cdot\pi$ and
$\mathbf{rcfg(x,p)}$, with $\alpha$ and $\pi$ ranging over complete tests and
assignments as in Definition 5, and $\mathbf{rcfg(x,p)}$ ranging over
reconfiguration actions. A _safety property_ $\mathit{prop}$ is defined as:

$\begin{array}[]{rcl}\mathit{act}&::=&\alpha\cdot\pi\mid\mathbf{rcfg}_{x,p}~{}~{}~{}~{}~{}~{}~{}(\textnormal{where
}\alpha\cdot\pi,\,\mathbf{rcfg}_{x,p}\in\mathcal{A})\\\
\mathit{regexp}&::=&\mathit{act}\mid\mathit{regexp}+\mathit{regexp}\mid\mathit{regexp}\cdot\mathit{regexp}\\\
\mathit{prop}&::=&[\mathit{regexp}]\mathit{false}\end{array}$

The intuition behind Definition 15 is as follows. A safety property
specification $\mathit{prop}$ is satisfied whenever the behaviour encoded by
regexp cannot be observed within the network. Regular expressions regexp are
defined with respect to actions $\mathit{act}$: a flow of shape
$\alpha\cdot\pi$ is the observable behaviour of a
(${\textnormal{NetKAT}^{-{\bf{dup}}}}$) policy transforming a packet encoded
by $\alpha$ into $\alpha_{\pi}$, whereas $\mathbf{rcfg}_{x,p}$ corresponds to
a reconfiguration step in a network. Recursively, a sum of regular expressions
$\mathit{regexp}_{1}+\mathit{regexp}_{2}$ encodes the union of the two
behaviours, a concatenation of regular expressions
$\mathit{regexp}_{1}\cdot\mathit{regexp}_{2}$ encodes the behaviour of
$\mathit{regexp}_{1}$ followed by the behaviour of $\mathit{regexp}_{2}$.

######  Definition 16 (Head Normal Forms for Safety)

Let $\mathcal{A}$ be an alphabet over letters of shape $\alpha\cdot\pi$ and
$\mathbf{rcfg(x,p)}$, with $\alpha$ and $\pi$ ranging over complete tests and
assignments as in Definition 5, and $\mathbf{rcfg(x,p)}$ ranging over
reconfiguration actions. We write $w,w^{\prime}$ for (non-empty) words with
letters in $\mathcal{A}$ (i.e., $w,w^{\prime}\in\mathcal{A}^{*}$) and $\mid
w\mid$ for the length of $w$. We write $w^{\prime}\preceq w$ whenever
$w^{\prime}$ is a prefix of $w$ (including $w$).

Let $r$ be a regular expression (regexp) as in Definition 15. We call _head
normal form_ of $r$, denoted by ${\textit{hnf}(r)}$, the sum of words obtained
by distributing $\cdot$ over $+$ in $r$, in the standard fashion:

$\begin{array}[]{rcl}{\textit{hnf}(a)}&\triangleq&a~{}~{}~{}(a\in\mathcal{A})\\\
{\textit{hnf}(w)}&\triangleq&w~{}~{}~{}(w\in\mathcal{A^{*}})\\\
{\textit{hnf}(r_{1}+r_{2})}&\triangleq&{\textit{hnf}(r_{1})}+{\textit{hnf}(r_{2})}\\\
{\textit{hnf}(r_{1}\cdot(r_{2}+r_{3}))}&\triangleq&{\textit{hnf}(r_{1}\cdot
r_{2})}+{\textit{hnf}(r_{1}\cdot r_{3})}\\\ {\textit{hnf}((r_{1}+r_{2})\cdot
r_{3})}&\triangleq&{\textit{hnf}(r_{1}\cdot r_{3})}+{\textit{hnf}(r_{1}\cdot
r_{3})}\\\ {\textit{hnf}(r^{\prime}\cdot(r_{1}+r_{2})\cdot
r^{\prime\prime})}&\triangleq&{\textit{hnf}(r^{\prime}\cdot r_{1}\cdot
r^{\prime\prime})}+{\textit{hnf}(r^{\prime}\cdot r_{2}\cdot
r^{\prime\prime})}\end{array}$

Next, we give the formal semantics of safety properties.

######  Definition 17 (Safety Properties - Semantics)

Let $\mathit{Prop}$ stand for the set of all properties as in Definition 15.
The semantic map
$\llbracket-\rrbracket:\mathit{Prop}\rightarrow\mathit{\textnormal{DyNetKAT}}$
associates to each safety property in $\mathit{Prop}$ a DyNetKAT expression as
follows.

Let $\Theta$ be the DyNetKAT policy (in normal form) encoding all possible
behaviours over $\mathcal{A}$:

$\Theta\triangleq\Sigma^{\oplus}_{\alpha\cdot\pi\in\mathcal{A}}(\alpha\cdot\pi;\bot\oplus\alpha\cdot\pi;\Theta)\,\oplus\,\Sigma^{\oplus}_{\mathbf{rcfg}_{x,p}\in\mathcal{A}}(\mathbf{rcfg}_{x,p};\bot\oplus\mathbf{rcfg}_{x,p};\Theta)$

Then:

$\begin{array}[]{lrcl}(c_{1})&\llbracket\,[\Sigma_{\footnotesize\begin{array}[]{l}i\in
I\\\ w_{i}\in
A^{*}\end{array}}\\!\\!\\!\\!w_{i}]\mathit{false}\,\rrbracket&\triangleq&\Sigma^{\oplus}_{\footnotesize\begin{array}[]{l}w\in\mathcal{A}^{*}\\\
\mid w\mid<M\\\ \forall i\in I:w_{i}\not\preceq
w\end{array}}\overline{w};\bot~{}~{}~{}\oplus~{}~{}~{}\Sigma^{\oplus}_{\footnotesize\begin{array}[]{l}w\in\mathcal{A}^{*}\\\
\mid w\mid=M\\\ \forall i\in I:w_{i}\not\preceq
w\end{array}}(\overline{w};\bot\,\oplus\,\overline{w};\Theta)\\\
\\\\[4.30554pt]
(c_{2})&\llbracket[r]\textit{false}\rrbracket&\triangleq&\llbracket[{\textit{hnf}(r)}]\textit{false}\rrbracket~{}~{}~{}~{}\textnormal{[otherwise]}\par\end{array}$

such that $M$ is the length of the longest word $w_{i}$, with $i\in I$, and
$\overline{w}$ is a DyNetKAT-compatible term obtained from $w$ where all
letters have been separated by ; and inductively defined in the obvious way:

$\begin{array}[]{rcl}\overline{a}&\triangleq&a~{}~{}~{}~{}(a\in\mathcal{A})\\\
\overline{a\cdot
w}&\triangleq&a;\overline{w}~{}~{}~{}~{}(a\in\mathcal{A},w\in\mathcal{A^{*}})\end{array}$

The semantic map
$\llbracket-\rrbracket:\mathit{Prop}\rightarrow\mathit{\textnormal{DyNetKAT}}$
is defined in accordance with the intuition provided in the beginning of this
section. For instance, as shown in $(c_{1})$, if none of the sequences of
steps $w_{i}$ can be observed in the system, then the associated DyNetKAT term
prevents the immediate execution of all $w_{i}$. Typically, safety analysis is
reduced to reachability analysis. Intuitively, in our context, a safety
property is violated whenever the network system under analysis displays a
(finite) execution that is not in the behaviour of the property. Thus, the
semantic map in Definition 17 is based on traces (or words in
$\mathcal{A}^{*}$) and is not sensitive to branching; see the use of head
normal forms in $(c_{2})$.

With these ingredients at hand, we can reason about the satisfiability of
safety properties in an equational fashion.

######  Definition 18 ($E_{\textit{DNK}}^{\textit{tr}}$)

Let $E_{\textit{DNK}}^{\textit{tr}}$ stand for the equational axioms in Figure
13, including the additional axiom that enables switching from the context of
bisimilarity to trace equivalence of DyNetKAT policies, namely:

$p;(q\oplus r)\equiv p;q\oplus p;r~{}~{}~{}~{}(A_{16})$ (26)

######  Definition 19 (Safe Network Systems)

Assume a specification given as the safety formula $s$ and a network system
implemented as the DyNetKAT policy $i$. We say that the network is _safe_
whenever the following holds:

$E_{\textit{DNK}}^{\textit{tr}}\vdash\llbracket s\rrbracket\oplus
i\equiv\llbracket s\rrbracket$ (27)

In words: checking whether $i$ satisfies $s$ reduces to checking whether the
trace behaviour of $i$ is included into that of $s$.

###  IV-A Sugars for Safety

In this section we introduce a version of safety properties extended with
negated actions ($\neg(\alpha\cdot\pi)$ and, respectively,
$\neg\mathbf{rcfg}_{x,p}$), the true construct and repetitions ($r^{n}$),
equally expressive but enabling more concise property specifications.

######  Definition 20 (Safety Properties - Extended Syntax)

Let $\mathcal{A}$ be an alphabet over letters of shape $\alpha\cdot\pi$ and
$\mathbf{rcfg}_{x,p}$, with $\alpha$ and $\pi$ ranging over complete tests and
assignments as in Definition 5, and $\mathbf{rcfg}_{x,p}$ ranging over
reconfiguration actions. Safety properties are extended in the following
fashion:

$\begin{array}[]{rcl}\mathit{act}_{e}&::=&\alpha\cdot\pi\mid\mathbf{rcfg}_{x,p}\mid\neg\mathit{act}_{e}~{}~{}~{}~{}~{}~{}~{}(\textnormal{with
}\alpha\cdot\pi,\,\mathbf{rcfg}_{x,p}\in\mathcal{A})\\\
\mathit{regexp}_{e}&::=&\textit{true}\mid\mathit{act}_{e}\mid\mathit{regexp}_{e}+\mathit{regexp}_{e}\mid\mathit{regexp}_{e}\cdot\mathit{regexp}_{e}\mid(\mathit{regexp}_{e})^{n}~{}~{}(\textnormal{with
}n\geq 1)\\\
\mathit{prop}_{e}&::=&[\mathit{regexp}_{e}]\mathit{false}\end{array}$

Intuitively, a property of shape $[\neg a]\textit{false}$, with
$a\in\mathcal{A}$, states that the system cannot do anything apart from $a$ as
a first step. The property $[\textit{true}]\textit{false}$ states that no
action can be observed in the network, whereas
$[\mathit{r}^{n}]\textit{false}$ encodes the repeated application of $r$ for
$n$ times.

Let $\mathit{Reg}$ and, respectively, $\mathit{Reg}_{e}$ denote the set of
regular expressions $\mathit{regexp}$ in Definition 15 and, respectively, the
set of regular expressions $\mathit{regexp}_{e}$ in Definition 20. The
“desugaring” function defining the regular equivalent of the extended safety
properties is defined as follows:

$\begin{array}[]{rcl}\lx@intercol\hfil
ds:\mathit{Reg}_{e}\rightarrow\mathit{Reg}\hfil\lx@intercol\\\
ds(\textit{true})&\triangleq&\Sigma_{a\in\mathcal{A}}a\\\
ds(\neg(\alpha\cdot\pi))&\triangleq&\Sigma_{\footnotesize\begin{array}[]{c}\alpha_{i}\cdot\pi_{i}\in\mathcal{A}\\\
\alpha_{i}\not=\alpha\\\ or\\\
\pi_{i}\not=\pi\end{array}}\alpha_{i}\cdot\pi_{i}\\\
ds(\neg\mathbf{rcfg}_{x,p})&\triangleq&\Sigma_{\footnotesize\begin{array}[]{c}\mathbf{rcfg}_{y,q}\in\mathcal{A}\\\
\mathbf{rcfg}_{y,q}\not=\mathbf{rcfg}_{x,p}\end{array}}\\!\\!\\!\\!\mathbf{rcfg}_{y,q}\\\
ds(r^{n})&\triangleq&ds(\underbrace{r\cdot r\cdot\ldots\cdot r}_{\text{$n$
times}})\\\ ds(r_{1}\cdot r_{2})&\triangleq&ds(r_{1})\cdot
ds(r_{2})~{}~{}~{}\textnormal{if }r_{1}\cdot r_{2}\not\in\textit{Reg}\\\
ds(r_{1}+r_{2})&\triangleq&ds(r_{1})+ds(r_{2})~{}~{}\textnormal{if
}r_{1}+r_{2}\not\in\textit{Reg}\\\
ds(r)&\triangleq&r~{}~{}~{}\textnormal{[otherwise]}\end{array}$

The (overloaded) semantic map
$\llbracket-\rrbracket:\mathit{Prop}_{e}\rightarrow\mathit{\textnormal{DyNetKAT}}$
is defined as expected:

$\llbracket\,[r_{e}]\textit{false}\,\rrbracket\triangleq\llbracket\,[ds(r_{e})]\textit{false}\,\rrbracket$

For an example, consider the distributed controllers in Figure 2 and the
corresponding encoding in Figure 7. Recall that reaching $H4$ from $S2$ is
considered a breach in the system. This entails the safety formulae $s_{n}$
defined as $[(true)^{n}\cdot(\alpha\cdot\pi)]\textit{false}$, for
$n\in\mathbb{N}$, $\alpha\triangleq(\mathit{port}=2)$ and
$\pi\triangleq(\mathit{port}\leftarrow 15)$. In words: no matter what sequence
of events (of length $n$) is executed, $\alpha\cdot\pi$ cannot happen as the
next step. Therefore, checking whether the network is safe reduces to
checking, for all $n\in\mathbb{N}$:

$E_{\textit{DNK}}^{\textit{tr}}\vdash\llbracket
s_{n}\rrbracket\oplus\mathit{SDN}\equiv\llbracket s_{n}\rrbracket$ (28)

Note that, for a fixed $n$, the verification procedure resembles bounded model
checking [4].

##  V Implementation

In Section IV we introduced a notion of safety for DyNetKAT and provided a
mechanism for reasoning about safety in an equational fashion, by exploiting
DyNetKAT trace semantics. To this end, we search for traces that violate the
safety property, i.e., we turn the equational reasoning about safety into
checking for reachability properties of shape
$s\triangleq\langle\textit{regexp}\rangle\textit{true}$; for an implementation
$i$, this is achieved by checking the following equation using our
axiomatization: $E_{\textit{DNK}}^{\textit{tr}}\vdash i\oplus\llbracket
s\rrbracket\equiv i$.

We developed a prototype tool, called
DyNetiKAT111https://github.com/hcantunc/DyNetiKAT, based on Maude [7], NetKAT
decision procedure [9] and Python [24], for checking the aforementioned
equation. We build upon the reachability checking method in NetKAT [2]. For a
reminder: out is reachable from in, in the context of a switch policy $p$ and
topology $t$, whenever the following property is satisfied: $in\cdot(p\cdot
t)^{*}\cdot out\not\equiv\mathbf{0}$ (and vice-versa). Furthermore, we also
consider waypointing properties. An intermediate point $w$ between $in$ and
$out$ is considered a waypoint from $in$ to $out$ if all the packets from $in$
to $out$ go through $w$. Such a property is satisfied if the following
equivalence holds [2]:

$\displaystyle in\cdot(p\cdot t)^{*}\cdot out+in\cdot(\neg out\cdot p\cdot
t)^{*}\cdot w\cdot(\neg in\cdot p\cdot t)^{*}\cdot out$ $\displaystyle\equiv
in\cdot(\neg out\cdot p\cdot t)^{*}\cdot w\cdot(\neg in\cdot p\cdot
t)^{*}\cdot out$

The inputs to our tool are a DyNetKAT program $p$, an input predicate $in$, an
output predicate $out$, a waypoint predicate $w$ for waypointing properties,
and the equivalences that describe the desired properties. The checking of
properties is achieved by analyzing the step by step behaviour of DyNetKAT
terms in normal form via a set of operators $head(D)$, and $tail(D,R)$, where
$D$ is a DyNetKAT term and $R$ is a set of terms of shape
$\mathbf{rcfg}_{X,N}$. Intuitively, the operator $head(D)$ returns a NetKAT
policy which represents the current configuration in the input $D$ and the
operator $tail(D,R)$ returns a DyNetKAT policy which is the sum of DyNetKAT
policies inside $D$ that appear after the reconfiguration events in $R$. The
operators $head$ and $tail$ are defined as follows:

$\displaystyle head(\bot)$ $\displaystyle=\mathbf{0}{}$ $\displaystyle
tail(\bot,R)$ $\displaystyle=\bot$ (29) $\displaystyle head(N;D)$
$\displaystyle=N+head(D)$ $\displaystyle tail(N;D,R)$
$\displaystyle=tail(D,R)$ (30) $\displaystyle head(D\oplus Q)$
$\displaystyle=head(D)+head(Q)$ $\displaystyle tail(D\oplus Q,R)$
$\displaystyle=tail(D,R)\oplus tail(Q,R)$ (31) $\displaystyle
head(\mathbf{rcfg}_{X,N};D)$ $\displaystyle=\mathbf{0}{}$ $\displaystyle
tail(\mathbf{rcfg}_{X,N};D,R)$ $\displaystyle=D\oplus
tail(D,R)~{}\textnormal{if}~{}\mathbf{rcfg}_{X,Z}\in R$ (32)
$\displaystyle\quad\quad tail(\mathbf{rcfg}_{X,N};D,R)$
$\displaystyle=\bot~{}\textnormal{if}~{}\mathbf{rcfg}_{X,N}\not\in R$ (33)

Note that we assume the input $D$ to the operators $head$ and $tail$ do not
contain terms of shape $x?q$ and $x!q$. This can be ensured by always applying
the restriction operator $\delta$ on $D$. After extracting the desired
configurations by using the $head$ and $tail$ operators, we then utilize the
NetKAT decision procedure for checking properties. For an example, consider
the stateful firewall in Figure 1 and the corresponding encoding in Figure 6.
Assume that we would like to check if the packets at port $ext$ can arrive at
port $int$ only after a proper reconfiguration on the channel $secConReq$. For
this example, the analysis reduces to defining the input predicate
$in\triangleq port=ext$, the output predicate $out\triangleq port=int$,
$R=\\{\mathbf{rcfg}_{secConReq,\mathbf{1}{}}\\}$, and the following
properties:

$\displaystyle in\cdot head(Init)\cdot out\equiv\mathbf{0}{}$ (34)
$\displaystyle in\cdot head(tail(Init,R))\cdot out\not\equiv\mathbf{0}{}$ (35)

Intuitively, the equivalence in (34) expresses that packets at port $ext$ are
not able to reach to port $int$ in the initial configuration and (35)
expresses that the configuration after the synchronization on the channel
$secConReq$ allows this flow.

$A_{1}$$A_{2}$$A_{3}$$A_{4}$$A_{5}$$A_{6}$$A_{7}$$A_{8}$$C_{1}$$C_{2}$$C_{3}$$C_{4}$$T_{1}$$T_{2}$$T_{3}$$T_{4}$$T_{5}$$T_{6}$$T_{7}$$T_{8}$AggregationCoreTop-
of-RackPod 1Pod 2Pod 3Pod 4 Figure 14: A FatTree Topology

We performed experiments on the FatTree [29] topologies to evaluate the
performance of our implementation. FatTrees are hierarchical topologies which
are very commonly used in data centers. Figure 14 illustrates a FatTree with
$3$ levels: core, aggregation and top-of-rack (ToR). The switches at each
level contain a number of redundant links to the switches at the next upper
level. The groups of ToR switches and their corresponding aggregation switches
are called pods. For our experiments, we generated $6$ FatTrees that grow in
size and achieve a maximum size of $1344$ switches. For these networks we
computed a shortest path forwarding policy between all pairs of ToR switches.
The number of switches in the ToR layer is set to $k^{3}/4$ where $k$ is the
number of pods in the network. We check certain dynamic properties on these
networks and assess the time performance of our tool. We consider a scenario
which involves two ToR switches $T_{a}$ and $T_{b}$ that reside in different
pods. Initially, all the packets from $T_{a}$ to $T_{b}$ traverse through a
firewall $A_{x}$ in the aggregation layer which filters SSH packets. The
controller then decides to shift the firewall from $A_{x}$ to another switch
$A_{x^{\prime}}$ in the aggregation layer. For this purpose, the controller
updates the corresponding aggregation and core layer switches which results in
a total of $4$ updates. The properties that we check in this scenario are as
follows: (i) At any point while the controller is performing the updates, non-
SSH packets from $T_{a}$ can always reach to $T_{b}$. (ii) At any point while
the controller is performing the updates, SSH packets from $T_{a}$ can never
reach to $T_{b}$. (iii) After all the updates are performed, $A_{x^{\prime}}$
is a waypoint between $T_{a}$ and $T_{b}$. We conducted the experiments on a
computer running Ubuntu 20.04 LTS with 16 core 2.4GHz Intel i9-9980HK
processor and 64 GB RAM. The results of these experiments are displayed in
Figure 15. We report the preprocessing time, the time taken for checking
properties (i), (ii), and (iii) individually (referred to as Reachability-I,
Reachability-II, and Waypointing, respectively), and also time taken to check
all the properties in parallel (referred to as All Properties). The reported
times are the average of 10 runs. The results indicate that preprocessing step
is a non-negligible factor that contributes to overall time. However,
preprocessing is independent of the property that is being checked and this
procedure only needs to be done once for a given network. After the
preprocessing step, the individual properties can be checked in less than $2$
seconds for networks with less than $100$ switches. For larger networks with
sizes up to $931$ and $1344$ switches, the individual properties can be
checked in a maximum of $5$ minutes and $11$ minutes, respectively. It can be
observed that checking for the property (iii) can take more than twice as much
time as checking for the properties (i) and (ii). In the experiments where we
check all the properties in parallel, we allocated one thread for each
property. In this setting, checking all the properties in parallel introduced
$24\%$ overhead on average. An important observation in the results of these
experiments is that after the preprocessing is performed, on average $87\%$ of
the running times are spent in the NetKAT decision procedure and this step
becomes the bottleneck in analyzing larger networks.

In order to be able to compare our technique with another verification method,
we also aimed to perform an analysis based on explicit state model checking.
For this purpose, we devised an operational semantics for NetKAT and
implemented it in Maude along with the operational semantics of DyNetKAT.
However, this method immediately failed at scaling even for small networks,
hence, we did not perform further analysis by using this method.

Figure 15: Results of FatTree experiments. Light colored areas indicate the
time spent in the NetKAT decision procedure and solid colored areas indicate
the time spent in our equational reasoning framework.

##  VI Conclusions

We developed a language, called DyNetKAT for modelling and reasoning about
dynamic reconfigurations in Software Defined Networks. Our language builds
upon the concepts, syntax, and semantics of NetKAT and hence, provides a
modular extension and makes it possible to reuse the theory and tools of
NetKAT. We define a formal semantics for our language and provide a sound and
ground-complete axiomatization. We exploit our axiomatization to analyse
reachability properties of dynamic networks and show that our approach is
indeed scalable to networks with hundreds of switches.

Our language builds upon the assumption that control plane updates interleave
with data plane packet processing in such a way that each data plane packet
sees one set of flow tables throughout their flight in the network. This
assumption is inspired by the framework put forward by Reitblatt et al. [22]
and is motivated by the requirement to design a modular extension on top of
NetKAT. However, we have experimented with a much smaller-stepped semantics in
which the control plane updates can have a finer interleaving with in-flight
packet moves. This alternative language breaks the hierarchy with NetKAT and a
naive treatment of this alternative semantics will lead to much larger state-
spaces. We would like to investigate this small-step semantics and efficient
analysis techniques for it further.

## Acknowledgments.

The authors would like to thank Alexandra Silva and Tobias Kappé for their
useful insight into the NetKAT framework.

## References

  * [1] Luca Aceto, Bard Bloom, and Frits W. Vaandrager.  Turning SOS rules into equations.  Inf. Comput., 111(1):1–52, 1994.  doi:10.1006/inco.1994.1040.
  * [2] Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker.  NetKAT: semantic foundations for networks.  In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, pages 113–126. ACM, 2014\.  doi:10.1145/2535838.2535862.
  * [3] Jos C. M. Baeten and W. P. Weijland.  Process algebra, volume 18 of Cambridge tracts in theoretical computer science.  Cambridge University Press, 1990.
  * [4] Christel Baier and Joost-Pieter Katoen.  Principles of model checking.  MIT Press, 2008.
  * [5] Ryan Beckett, Michael Greenberg, and David Walker.  Temporal netkat.  In Chandra Krintz and Emery Berger, editors, Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 386–401. ACM, 2016.  doi:10.1145/2908080.2908108.
  * [6] G. Caltais, H. Hojjat, M. R. Mousavi, and H. C. Tunc.  DyNetKAT: An algebra of dynamic networks.  CoRR, abs/2102.10035, 2021.
  * [7] Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott.  Full Maude: Extending Core Maude.  In Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott, editors, All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science, pages 559–597. Springer, 2007.  doi:10.1007/978-3-540-71999-1\\_18.
  * [8] Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva.  Probabilistic NetKAT.  In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 282–309. Springer, 2016.  doi:10.1007/978-3-662-49498-1\\_12.
  * [9] Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva, and Laure Thompson.  A Coalgebraic Decision Procedure for NetKAT.  In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 343–355. ACM, 2015.  doi:10.1145/2676726.2677011.
  * [10] Nate Foster, Rob Harrison, Michael J. Freedman, Christopher Monsanto, Jennifer Rexford, Alec Story, and David Walker.  Frenetic: a network programming language.  In _Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming (ICFP 2011)_. pages 279–291, ACM, 2011.  .
  * [11] Ahmed El-Hassany, Ahmed Miserez, Pavol Bielik, Laurent Vanbever, and Martin T. Vechev.  SDNRacer: concurrency analysis for software-defined networks.  In Chandra Krintz and Emery Berger, Eds. , Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2016), 402–415, ACM, 2016.  .
  * [12] Maciej Kuzniar, Peter Peresíni, and Dejan Kostic. Providing Reliable FIB Update Acknowledgments in SDN. In Aruna Seneviratne, Christophe Diot, Jim Kurose, Augustin Chaintreau, and Luigi Rizzo, Eds. Proceedings of the 10th ACM International on Conference on emerging Networking Experiments and Technologies (CoNEXT 2014), 415–422, ACM, 2014.  .
  * [13] Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi.  Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness.  CoRR, abs/2002.09682, 2020.  URL: https://arxiv.org/abs/2002.09682, arXiv:2002.09682.
  * [14] Hyojoon Kim, Joshua Reich, Arpit Gupta, Muhammad Shahbaz, Nick Feamster, and Russell J. Clark.  Kinetic: Verifiable dynamic network control.  In 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4-6, 2015, pages 59–72. USENIX Association, 2015.  URL: https://www.usenix.org/conference/nsdi15/technical-sessions/presentation/kim.
  * [15] Zohaib Latif, Kashif Sharif, Fan Li , Md. Monjurul Karim, Sujit Biswas, and Yu Wang.  A comprehensive survey of interface protocols for software defined networks.  J. Netw. Comput. Appl. 156:102563, 2020\.  .
  * [16] Jedidiah McClurg, Hossein Hojjat, Nate Foster, and Pavol Cerný.  Event-driven network programming.  In Chandra Krintz and Emery Berger, editors, Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 369–385. ACM, 2016.  doi:10.1145/2908080.2908097.
  * [17] Jedidiah McClurg, Hossein Hojjat, and Pavol Cerný.  Synchronization Synthesis for Network Programs.  In Proceedings of the 29th International Conference on Computer Aided Verification (CAV 2017).  volume 10427 of Lecture Notes in Computer Science, pages 301–321, Springer, 2017.  .
  * [18] Nick McKeown, Thomas E. Anderson, Hari Balakrishnan, Guru M. Parulkar, Larry L. Peterson, Jennifer Rexford, Scott Shenker, and Jonathan S. Turner.  OpenFlow: enabling innovation in campus networks.  Computer Communication Review, 38(2):69–74, 2008. .
  * [19] Peter D. Mosses.  Modular structural operational semantics.  J. Log. Algebraic Methods Program. 60-61: 195-228, 2004.  doi:https://doi.org/10.1016/j.jlap.2004.03.008
  * [20] Mohammad Reza Mousavi, Michel A. Reniers, and Jan Friso Groote.  Notions of bisimulation and congruence formats for SOS with data.  Information and Computation, 200(1):107 – 147, 2005.  doi:https://doi.org/10.1016/j.ic.2005.03.002.
  * [21] Tim Nelson, Andrew D. Ferguson, Michael J. G. Scheer, and Shriram Krishnamurthi.  Tierless programming and reasoning for software-defined networks.  In Ratul Mahajan and Ion Stoica, editors, Proceedings of the 11th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2014, Seattle, WA, USA, April 2-4, 2014, pages 519–531. USENIX Association, 2014.  URL: https://www.usenix.org/conference/nsdi14/technical-sessions/presentation/nelson.
  * [22] Mark Reitblatt, Nate Foster, Jennifer Rexford, Cole Schlesinger, and David Walker.  Abstractions for network update.  In Lars Eggert, Jörg Ott, Venkata N. Padmanabhan, and George Varghese, editors, ACM SIGCOMM 2012 Conference, SIGCOMM ’12, Helsinki, Finland - August 13 - 17, 2012, pages 323–334. ACM, 2012.  doi:10.1145/2342356.2342427.
  * [23] Alexandra Silva.  Models of Concurrent Kleene Algebra.  In Elvira Albert and Laura Kovács, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, page 516. EasyChair, 2020.  URL: https://easychair.org/publications/paper/6C8R.
  * [24] Guido van Rossum.  Python programming language.  In Jeff Chase and Srinivasan Seshan, editors, Proceedings of the 2007 USENIX Annual Technical Conference, Santa Clara, CA, USA, June 17-22, 2007. USENIX, 2007.
  * [25] Teemu Koponen, Keith Amidon, Peter Balland, Martín Casado, Anupam Chanda, Bryan Fulton, Igor Ganichev, Jesse Gross, Paul Ingram, Ethan J. Jackson, Andrew Lambeth, Romain Lenglet, Shih-Hao Li, Amar Padmanabhan, Justin Pettit, Ben Pfaff, Rajiv Ramanathan, Scott Shenker, Alan Shieh, Jeremy Stribling, Pankaj Thakkar, Dan Wendlandt, Alexander Yip, and Ronghua Zhang.  Network Virtualization in Multi-tenant Datacenters.  In Ratul Mahajan and Ion Stoica, Eds., Proceedings of the 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2014), 203–216, USENIX Association, 2014.
  * [26] Celio Trois, Marcos Didonet Del Fabro, Luis Carlos Erpen De Bona, and Magnos Martinello.  A Survey on SDN Programming Languages: Toward a Taxonomy.  IEEE Commun. Surv. Tutorials 18(4): 2687–2712, 2016.  .
  * [27] Alexander Vandenbroucke and Tom Schrijvers.  P$\lambda$$\omega$nk: functional probabilistic netkat.  Proc. ACM Program. Lang., 4(POPL):39:1–39:27, 2020.  doi:10.1145/3371107.
  * [28] Jana Wagemaker, Paul Brunet, Simon Docherty, Tobias Kappé, Jurriaan Rot, and Alexandra Silva.  Partially Observable Concurrent Kleene Algebra.  In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 20:1–20:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020\.  doi:10.4230/LIPIcs.CONCUR.2020.20.
  * [29] Al-Fares, Mohammad and Loukissas, Alexander and Vahdat, Amin.  A Scalable, Commodity Data Center Network Architecture.  ACM SIGCOMM Comput. Commun. Rev. 38, 4, 63-74, 2008\.  doi:10.1145/1402946.1402967.

###  -A Soundness Proofs

  * •

Axiom under consideration:

$\mathbf{0}{}\mathop{;}p\equiv\bot\quad(A0)$ (36)

for $p\in{\textnormal{DyNetKAT}}$. According to the semantic rules of
DyNetKAT, the derivations of the term $\mathbf{0}{}\mathop{;}p$ are as
follows:

    1. (a)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\textnormal{For all
}\sigma^{\prime}\in\llbracket\mathbf{0}{}\rrbracket(\sigma\\!\\!::\\!\\!\langle\rangle):~{}\mathbf{(cpol_{\\_\mathop{;}}^{\checkmark}{})}&\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$(\mathbf{0}{}\mathop{;}p,\sigma::H,H^{\prime})\,\,{{\xrightarrow{(\sigma,\sigma^{\prime})}}}\,\,(p,H,\sigma^{\prime}::H^{\prime})$}}}\\\
\end{array}$

However, observe that
$\llbracket\mathbf{0}{}\rrbracket(\sigma\\!\\!::\\!\\!\langle\rangle)$ is
equal to empty set:

$\displaystyle\llbracket\mathbf{0}{}\rrbracket(\sigma\\!\\!::\\!\\!\langle\rangle)=\\{\\}\quad$
$\displaystyle(\textnormal{Definition of }\mathbf{0}{})$ (37)

Hence, the term $\mathbf{0}{}\mathop{;}p$ does not afford any transition.
Similarly, observe that according to the semantic rules of DyNetKAT, the term
$\bot$ does not afford any transition. Hence, the following trivially holds:

$(\mathbf{0}{}\mathop{;}p)\sim\bot$ (38)

  * •

Axiom under consideration:

$p\oplus q\equiv q\oplus p\quad(A2)$ (39)

for $p,q\in{\textnormal{DyNetKAT}}$. According to the semantic rules of
DyNetKAT, the following are the possible transitions that can initially occur
in the terms $p\oplus q$ and $q\oplus p$:

$\displaystyle\begin{cases}(1)\;(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})\\\
(2)\;(q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})\end{cases}$

$\gamma::=(\sigma,\sigma^{\prime})\mid x!z\mid x?z\mid{\mathbf{rcfg(x,z)}}$

Case (1):
$(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$

The derivations of $p\oplus q$ are as follows:

    1. (a)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\mathbf{(cpol_{\\_\oplus})}\frac{\raisebox{2.1097pt}{\normalsize{$(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(p\oplus
q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}\end{array}$

The derivations of $q\oplus p$ are as follows:

    1. (b)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\mathbf{(cpol_{\oplus\\_})}\frac{\raisebox{2.1097pt}{\normalsize{$(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(q\oplus
p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}\end{array}$

As demonstrated in (a) and (b), if
$(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$
holds then both of the terms $p\oplus q$ and $q\oplus p$ converge to the same
expression with the $\gamma$ transition:

$\displaystyle(p\oplus q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}$
$\displaystyle(p^{\prime},H_{1},H^{\prime}_{1})$ (40) $\displaystyle(q\oplus
p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}$
$\displaystyle(p^{\prime},H_{1},H^{\prime}_{1})$

Case (2):
$(q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$

The derivations of $p\oplus q$ are as follows:

    1. (c)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\mathbf{(cpol_{\oplus\\_})}\frac{\raisebox{2.1097pt}{\normalsize{$(q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(p\oplus
q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$}}}\end{array}$

The derivations of $q\oplus p$ are as follows:

    1. (d)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\mathbf{(cpol_{\\_\oplus})}\frac{\raisebox{2.1097pt}{\normalsize{$(q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(q\oplus
p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$}}}\end{array}$

As demonstrated in (c) and (d), if
$(q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$
holds then both of the terms $p\oplus q$ and $q\oplus p$ converge to the same
expression with the $\gamma$ transition:

$\displaystyle(p\oplus q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}$
$\displaystyle(q^{\prime},H_{1},H^{\prime}_{1})$ (41) $\displaystyle(q\oplus
p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}$
$\displaystyle(q^{\prime},H_{1},H^{\prime}_{1})$

Therefore, by (40) and (41) it is straightforward to conclude that the
following holds:

$(p\oplus q)\sim(q\oplus p)$ (42)

  * •

Axiom under consideration:

$(p\oplus q)\oplus r\equiv p\oplus(q\oplus r)\quad(A3)$ (43)

for $p,q,r\in{\textnormal{DyNetKAT}}$. According to the semantic rules of
DyNetKAT, the following are the possible transitions that can initially occur
in the terms $(p\oplus q)\oplus r$ and $p\oplus(q\oplus r)$:

$\displaystyle\begin{cases}(1)\;(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})\\\
(2)\;(q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})\\\
(3)\;(r,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(r^{\prime},H_{1},H^{\prime}_{1})\end{cases}$

$\gamma::=(\sigma,\sigma^{\prime})\mid x!z\mid x?z\mid{\mathbf{rcfg(x,z)}}$

Case (1):
$(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$

The derivations of $(p\oplus q)\oplus r$ are as follows:

    1. (a)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\mathbf{(cpol_{\\_\oplus})}&\frac{\raisebox{2.1097pt}{\normalsize{$(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(p\oplus
q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}\\\
\mathbf{(cpol_{\\_\oplus})}&\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$((p\oplus
q)\oplus
r,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}\end{array}$

The derivations of $p\oplus(q\oplus r)$ are as follows:

    1. (b)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\mathbf{(cpol_{\\_\oplus})}\frac{\raisebox{2.1097pt}{\normalsize{$(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(p\oplus(q\oplus
r),H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$}}}\end{array}$

As demonstrated in (a) and (b), if
$(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$
holds then both of the terms $(p\oplus q)\oplus r$ and $p\oplus(q\oplus r)$
converge to the same expression with the $\gamma$ transition:

$\displaystyle((p\oplus q)\oplus
r,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}$
$\displaystyle(p^{\prime},H_{1},H^{\prime}_{1})$ (44)
$\displaystyle(p\oplus(q\oplus
r),H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}$
$\displaystyle(p^{\prime},H_{1},H^{\prime}_{1})$

Case (2):
$(q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$

The derivations of $(p\oplus q)\oplus r$ are as follows:

    1. (c)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\mathbf{(cpol_{\oplus\\_})}&\frac{\raisebox{2.1097pt}{\normalsize{$(q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(p\oplus
q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$}}}\\\
\mathbf{(cpol_{\\_\oplus})}&\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$((p\oplus
q)\oplus
r,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$}}}\end{array}$

The derivations of $p\oplus(q\oplus r)$ are as follows:

    1. (d)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\mathbf{(cpol_{\\_\oplus})}&\frac{\raisebox{2.1097pt}{\normalsize{$(q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(q\oplus
r,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$}}}\\\
\mathbf{(cpol_{\oplus\\_})}&\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$(p\oplus(q\oplus
r),H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$}}}\end{array}$

As demonstrated in (c) and (d), if
$(q,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(q^{\prime},H_{1},H^{\prime}_{1})$
holds then both of the terms $(p\oplus q)\oplus r$ and $p\oplus(q\oplus r)$
converge to the same expression with the $\gamma$ transition:

$\displaystyle((p\oplus q)\oplus
r,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}$
$\displaystyle(q^{\prime},H_{1},H^{\prime}_{1})$ (45)
$\displaystyle(p\oplus(q\oplus
r),H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}$
$\displaystyle(q^{\prime},H_{1},H^{\prime}_{1})$

Case (3):
$(r,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(r^{\prime},H_{1},H^{\prime}_{1})$

The derivations of $(p\oplus q)\oplus r$ are as follows:

    1. (e)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\mathbf{(cpol_{\oplus\\_})}&\frac{\raisebox{2.1097pt}{\normalsize{$(r,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(r^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$((p\oplus
q)\oplus
r,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(r^{\prime},H_{1},H^{\prime}_{1})$}}}\end{array}$

The derivations of $p\oplus(q\oplus r)$ are as follows:

    1. (f)

$\begin{array}[]{r@{}l@{}c@{}r@{}l@{}c@{}r@{}l@{}}\mathbf{(cpol_{\oplus\\_})}&\frac{\raisebox{2.1097pt}{\normalsize{$(r,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(r^{\prime},H_{1},H^{\prime}_{1})$}}}{\raisebox{-3.01389pt}{\normalsize{$(q\oplus
r,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(r^{\prime},H_{1},H^{\prime}_{1})$}}}\\\
\mathbf{(cpol_{\oplus\\_})}&\frac{\raisebox{2.1097pt}{\normalsize{$$}}}{\raisebox{-3.01389pt}{\normalsize{$(p\oplus(q\oplus
r),H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(r^{\prime},H_{1},H^{\prime}_{1})$}}}\end{array}$

As demonstrated in (e) and (f), if
$(r,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(r^{\prime},H_{1},H^{\prime}_{1})$
holds then both of the terms $(p\oplus q)\oplus r$ and $p\oplus(q\oplus r)$
converge to the same expression with the $\gamma$ transition:

$\displaystyle((p\oplus q)\oplus
r,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}$
$\displaystyle(r^{\prime},H_{1},H^{\prime}_{1})$ (46)
$\displaystyle(p\oplus(q\oplus
r),H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}$
$\displaystyle(r^{\prime},H_{1},H^{\prime}_{1})$

Therefore, by (44), (45) and (46) it is straightforward to conclude that the
following holds:

$((p\oplus q)\oplus r)\sim(p\oplus(q\oplus r))$ (47)

  * •

Axiom under consideration:

$p\oplus p\equiv p\quad(A4)$ (48)

for $p\in{\textnormal{DyNetKAT}}$. According to the semantic rules of
DyNetKAT, the following are the possible transitions that can initially occur
in the terms $p\oplus p$ and $p$:

$\displaystyle\begin{cases}(1)\;(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})\end{cases}$

$\gamma::=(\sigma,\sigma^{\prime})\mid x!z\mid x?z\mid{\mathbf{rcfg(x,z)}}$

Case (1):
$(p,H_{0},H^{\prime}_{0})\,\,{{\xrightarrow{\gamma}}}\,\,(p^{\prime},H_{1},H^{\prime}_{1})$

The derivations of $p\oplus p$ are as follows:

    1. (a)