  This work introduces a concept of explanations with respect to the violation
of safe behaviours within software defined networks (SDNs) expressible in
NetKAT. The latter is a network programming language that is based on a
well-studied mathematical structure, namely, Kleene Algebra with Tests (KAT).
Amongst others, the mathematical foundation of NetKAT gave rise to a sound and
complete equational theory. In our setting, a safe behaviour is characterised
by a NetKAT policy which does not enable forwarding packets from ingress to an
undesirable egress. Explanations for safety violations are derived in an
equational fashion, based on a modification of the existing NetKAT
axiomatisation.
