Cantor Meets Scott: Semantic Foundations for Probabilistic Networks

Speaker: Dexter Kozen, Professor at Cornell University

Abstract: NetKAT is a language/logic for specifying, programming, and reasoning about packet-switching networks. ProbNetKAT is a probabilistic extension of NetKAT with a compositional denotational semantics based on Markov kernels. The language is expressive enough to generate continuous distributions, which raises the question of how to compute effectively in the language. In this talk I will describe a new domain-theoretic characterization of the semantics, which provides the foundation needed to build a practical implementation. The new semantics allows the behavior of an arbitrary ProbNetKAT program to be approximated to arbitrary precision with distributions of finite support. There is a prototype implementation, which can be used to solve a variety of problems, including the calculation of the expected congestion induced by different routing schemes and reasoning probabilistically about reachability. (joint work with Steffen Smolka, Nate Foster, Praveen Kumar, and Alexandra Silva)