An Algebraic Approach to Automatic Reasoning for NetKAT Based on its Operational Semantics
Yuxin Deng, Min Zhang, and Guoqing Lei
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.