Probabilistic Program Equivalence for NetKAT
We study the problem of deciding program equivalence in the context of Probabilistic NetKAT, a formal language for reasoning about the behavior of packet-switched networks. We show that the problem is decidable for the history-free fragment of the language, and discuss a path toward a decision procedure for the full language. The main challenge lies in reasoning about iteration, which we address by a reduction to finite-state absorbing Markov chains. We also describe an OCaml prototype that we have used to reason about probabilistic network programs.