Discussing "Scalable Verification of Probabilistic Networks"

(Link)

Authors: Steffen Smolka (Cornell University), Praveen Kumar (Cornell University), David M. Kahn (Carnegie Mellon University), Nate Foster (Cornell University), Justin Hsu (University of Wisconsin), Dexter Kozen (Cornell University), and Alexandra Silva (University College London)

Reference: Smolka, Steffen, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva. "Scalable verification of probabilistic networks." In PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 190-203. 2019.

Why this paper? Cited by A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests and Lilac: a Modal Separation Logic for Conditional Probability

I built this blog around the idea of discoverability via Google Scholar both of new papers and, via their citations, influential older papers. Google Scholar generally does an excellent job of this (far better than the new wave of AIs with their tendency to hallucinate literature) but nothing is perfect, and the recommendations from this week are perhaps partly caused by misunderstanding that the word ‘guarded’, which is used a lot in some of my papers, is also used, but in a completely different way, in certain other papers. Still, the paper I got served by my self-imposed algorithm, while not exactly in my wheelhouse, is interesting enough so long as I don’t dive too deep into the technicalities.

This paper describes a system call McNetKAT, which is a grand pileup of acronyms: Mc for ‘Markov chain’, Net for ‘Network’, KA for ‘Kleen Algebra’, and ‘T’ for ‘(with) Tests’. The basic idea is to build capability for automatic verification on top of the programming language ProbNetKAT (Prob for ‘Probabilistic’), a small imperative language that allows one to specify the topology of a network and the policy for moving packets through it. The support for probability helps capture cases “from uncertainty about the inputs, to expected loads, to likelihood of device and link failures” that might effect networks. One can attempt to prove that the network program is fully correct, by showing that is equivalent to a magic network that teleports each packet to its correct destination, but the probabilities really come into play when you show a certain network program improves on another, in the sense that where both succeed they agree on their treatment of packets, but one is less likely to fail than another according to a given failure model on links or switches.

The ‘Mc’ comes into play because a new semantics is presented based on stochastic matrices / Markov chains, a notion of probabilistic transition system. These semantics are proved to be equal to the existing semantics in the literature, but are more amenable to automation. Programs are compiled into their semantics, and then passed to the linear algebra solver UMFPACK. It is shown that this treatment performs well against an alternative route involving compilation into the language of the probabilistic model checker PRISM, and against the (admittedly, more expressive) system Bayonet.