An Algebraic Approach to Automatic Reasoning for NetKAT Based on Its Operational Semantics.

NetKAT is a network programming language with a solid mathematical foundation. In this paper, we present an operational semantics and show that it is sound and complete with respect to its original axiomatic semantics. We achieve automatic reasoning for NetKAT such as reachability analysis and model checking of temporal properties, by formalizing the operational semantics in an algebraic executable specification language called Maude. In addition, as NetKAT policies are normalizable, two policies are operationally equivalent if and only if they can be converted into the same normal form. We provide a formal way of reasoning about network properties by turning the equivalence checking problem of NetKAT policies into the normalization problem that can be automated in Maude.