NetKAT Automata

In this lecture we present NetKAT automata. Intuitively, these automata recognize the guarded strings in the language model. However, before presenting NetKAT automata, we’ll introduce a technique for converting ordinary regular expressions into deterministic finite automata.

Regular Expressions

Recall the syntax of regular expressions:

R ::= 0
    | c
    | R1 + R2
    | R1 . R2
    | R*

Define 1 to be 0* – i.e., the regular expression that describes the language containing just the empty string.

The (left) derivatives of a language L with respect to a character c is defined as:

δ_c(L) = { w | c . w in L }

It turns out that we can characterize the derivative of a regular expressions syntactically, via a simple inductive definition:

D_c(0) = 0
D_c(c') = { 1 if c = c'
          { 0 otherwise
D_c(R1 + R2) = D_c(R1) + D_c(R2)
D_c(R1 . R2) = D_c(R1) . R2 + E(R1) . D_c(R2)
D_c(R*) = D_c(R) . R*

where

E(0) = 0
E(c) = 0
E(R1 + R2) = E(R1) + E(R2)
E(R1 . R2) = E(R1) . E(R2)
E(R*) = 1

Intuitively, E(R) is equivalent to 1 if the language described by R contains the empty string, and 0 otherwise.

Every regular expression has a finite number of syntactically distinct derivatives, up to a simple equivalence relation that includes associativity, commutativity, and idempotence. Hence, we can build a finite automaton from a regular expression R by taking:

  • Q = derivatives of R,
  • q0 = R
  • delta R c = D_c(R)
  • R in F <=> E(R) == 1

NetKAT Automata

Formally, a NetKAT automaton consists of:

  • A finite set of states Q
  • An initial state q_0
  • An observation function epsilon : Q -> Packet -> Packet Set
  • A transition function delta : Q -> Packet -> (Q * Packet) Set

Just as with standard automata, we can construct NetKAT automata using derivatives. Assume that each occurrence of dup is annotated with a distinct label. We will write L for the set of labels and dup^l to indicate an occurrence of dup labeled with l.

We can define the derivatives of a NetKAT program as follows:

First we define a syntactic version of observations:

E(p) : Program
E(a) = a
E(f := n) = f := n
E(dup^l) = 0
E(p1 + p2) = E(p1) + E(p2)
E(p1 ; p2) = E(p1) ; E(p2)
E(p*) = E(p)*

Note that unlike standard automata, where the notion of observation is just acceptance, and can be represented by a boolean, here we need a (dup-free) NetKAT program to represent the observation at each state – intuitively, the processing done at the final hop.

Next we define a syntactic version of derivatives:

D(p) : (Program * L * Program) Set
D(a) = 0
D(f := n) = 0
D(dup^l) = { (1, l, 1) }
D(p1 + p2) = D(p1) U D(p2)
D(p1 ; p2) = D(p1) ; p2 + E(p1) ; D(p2)
D(p*) = E(p*) ; D(p); p*

Note that we lift operators to sets in the obvious way. For example,

D(p1) ; p2 = { (d,l,k ; p2) | (d,l,k) in D(p1) }

Intuitively D(p) returns a set of triples (d,l,k) where d represents the packet-processing up to the next occurrence of dup, which is labeled by l, and k represents the packet-processing after the next occurrence of dup.

Lemma: p == E(p) + Sum_{(d,l,k) in D(p)} d ; dup; k

Lemma: for each label l occurring in p, there exists a unique triple (d,l,k) in D(p). We write k_l for the k associated with l in D(p).

Using these derivatives, we can build a NetKAT automaton as follows:

  • Q = L U { 0 }
  • q0 = 0
  • epsilon l pk = U { [[ E(k_l) ]] pk }
  • delta l pk = { (l', pk') | (d,l',k) in D(k_l) and <pk'> in [[ d ]] <pk> }

Reading

An excellent introduction to regular expression derivatives can be found in the following paper:

The NetKAT material in this lecture was originally published in the following papers: