Over the past decade, formal methods have found successful application in the verification of computer networks and various network verification tools have been developed in academia and industry. These tools are all based on deterministic network models, and as such cannot reason about network features involving uncertainty: faulty links, randomized routing algorithms, fault-tolerance mechanism, etc. This is a serious limitation as such features are pervasive in real-world networks.
NetKAT is one such framework. In NetKAT, verification questions such as waypointing, reachability, and isolation can be naturally phrased as questions about program equivalence, and then be answered by a symbolic (worst-case PSPACE) decision procedure that scales well in practise.
This work studies the equivalence problem for Probabilistic NetKAT, i.e. NetKAT extended with a probabilistic choice operator. We show that the problem is decidable for the history-free fragment of the language and use the system to study resilient routing algorithms.
It remains open whether the equivalence problem for the full language is decidable. The problem is technically challenging because ProbNetKATs semantics is defined over the uncountable space of packet history sets and the calculus is powerful enough to encode continuous (i.e., atomless) distributions.