Based on vidoes of lectures by Alexandra Silva at OPLSS-2021.

Mistakes my own.

l1

NetKAT
Program can be made to leave a trace.
Kleene's theorem
- Class of languages accepted by a DFA is same as regular languages.
Fun fact: (a|b)* = (a*)(b(a*))*

Exercise:

regex for L = {w ∈ Σ* | w contains aba at least once} where Σ = {a,b}
- (a|b)*aba(a|b)*

—

DFA = (S, <o,t>)

S: set of states
o: Function telling whether a state is a final state
- o: S -> 𝔹
t: transition function
- t: (S,Σ) -> S
- She wrote it like S->S^Σ

t*(s)(ε) = s t*(s)(aw) = t*[t(s)(a)][w]

where t* is like the big-step form of t.

Notations:

s_w = t*(s)(w)

Languages accepted by a state:

w ∈ L(s) ↔︎ o(s_w)==true

Coalgebra in category theory

              L
  S ---------->----------> 2^(Σ*)
  |                        |
  |                        |
  |                        |
  V <o_S,t_S>              V <o_L,t_L>
  |                        |
  |                        |
(𝔹,S) --------->---------> (𝔹,[2^(Σ*)]ᴬ)
            id*Lᴬ

S = set of states of a DFA
L = functor from S to 2^Σ*, which is the set of all languages with Σ.

2^(Σ*) = Lᴬ This is defined by a characteristic function: Σ* → 2

Equip a state s:S with a transition function and output function and you get a DFA (ie, type (𝔹,S)).

Brzozowski derivatives

Uₐ = {u | au ∈ U}

—

Notation: Lᴬ

It's like:

f: X → Y
fᴬ: Xᴬ → Yᴬ

φ: A → X
fᴬ(φ)(a:A) = f (φ a)

ie, it's just function composition.

fᴬ means f ∘ φ where φ:A → dom(f)

Kleene algebra

We can give an ordering as

e ≤ f if e + f = f

Brzozowski derivatives

regex → DFA

(x + y)_a = x_a + y_a
(x ; y)_a
  | o x == 0  => x_a ; y
  | otherwise => x_a;y + y_a

output function: o. 1 if final state possibly reached, else 0.

o(∅) = 0
o(ε) = 1
o(a) = 0
o(r*) = 1
o(r1+r2) = o(r1) ∨ o(r2)
o(r1;r2) = o(r1) ∧ o(r2)

where the semantics for ; is made out as if 0 and 1 form a lattice like

   1
   |
   |
   0

where:
 - 0 ∨ 1 is 1
 - 0 ∧ 1 is 0 

But still... how does that explain it ????
o(r1) ∧ o(r2) means both r1 and r2 got to accept. Only end of r2 got to be accepting, right?

'a-derivative' is like removing 'a' from the string.

∅_a = 0	we can't take 'a' from nothingness
ε_a = 0	we can't take 'a' from empty string
r_a = r_a;r

Antimirov derivatives

regex → NFA

Sets unlike in the case of Brzozowski derivatives.

Every time you see a 'plus' (ie, an alternative path), we add a new set (corresponds to spawning a new thread of execution).

Comma instead of plus when translating Brzozowski derivatives to Antimirov derivatives.

NFAs from Antimirov derivatives are usually smaller than the one built via Brzozowski derivatives.

(x + y)_a = {x_a, y_a}
(x ; y)_a
  | o x == 0  => {x_a ; y}
  | otherwise => {x_a;y, y_a}

Antimirov implicitly does ACI (associativity, commutativity, identity) resolution by virtue of the set operation.

dₐ(∅) = ∅
dₐ(ε) = ∅
dₐ(.) = ε

dₐ(c) = {ε} if a=c
      | ∅   if a≠c

dₐ(r1;r2) = {r;r2 | r ∈ dₐ(r1)}           if r1 cannot derive ε
          | dₐ(r2) ∪ {r;r2 | r ∈ dₐ(r1)}  otherwise

dₐ(r1+r2) = dₐ(r1) ∪ dₐ(r2)

dₐ(r*) = {rr;r* | rr ∈ dₐ(r)}

Examples:

r + r => {r, r} = {r}
r + (s + t) => {r, s, t}
(r + s) + t => {r, s, t}

Glushkov automata or position automata: Another way to convert regex to DFA/NFA (mostly used for NFAs though).

Glushkov automata or position automata: another way of building NFA out of regex.

Used by Esterel. A language used for formal verification. Predominantly for embedded system verification.
https://en.wikipedia.org/wiki/Esterel

Esteral

l4

KAT: Kleene Algebra with Tests
- A Kleene algebra (K, +, ⋅, *, 0, 1)
- A boolean algebra (B, +, ⋅, neg, 0, 1) is embedded in this KA
- ie, The boolean algebra is a sub-algebra of the KA.

Notations:

p,q,r,.. ranges over K (actions)
a,b,c,.. ranges over B
α,β,γ,.. ranges over strings

Strings are guarded by tests/actions.

KAT subsumes Propositional Hoare Logic!

{a} p {b}

is equivalent to

 ap ≤ pb      ??
 ap ≤ apb
apb̅ = 0

(Think of {bc} p {c} like an loop. b is the exit condition.)

Another example:

      {bc} p {c}
───────────────────────
 {c} while b do p {b̅c}


This is same as saying

bcpc̅ = 0
implies
c(bp)*b̅(b̅c)' = 0

NetKAT

First presented at POPL'14.
Can be used for verifying networks.
Packet (π): Essentially an assignment to a finite set of fields
Packet history: non-empty sequence of packet.
- Captures the life of the packet. The changes it underwent.
- π1::π2::…..:πn
Head packet: First packet in the packet history. This is what we manipulate.

NetKAT is a Kleene algebra where the tests and actions are both pairs.

assignment (action): x ← n
test: x = n (check if x is equal to n)
dup: duplicate the head packet.
- dup (π1::π2) is π1::π1::π2

An example:

sw=6;pt=8; dst←A;pt←5

Test: if switch number is 6 and port is 8,
Action: make destination A and port 5

policy
(policy; topo); policy

The final 'policy' is to flush final values.

Encoding network topology

+---+                  +---+
|   | n              m |   |
| A |------------------| B |                  
|   |                  |   |
+---+                  +---+
switch                 switch

This link could be written as:

sw=A;pt=n; sw←B;pt←m

Coming to swtiches, they are like little networks themselves. Switches generally consist of match-action tables.

Applications using NetKAT:

openflow
p4

KA ⊂ KAT ⊂ NetKAT

Dbts

Final closure of a functor f: Ω_f
Meet, joins, lattice, semi-lattice, join semi-lattice