Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
ProbNetKAT is a probabilistic extension of NetKAT with a denotational semantics based on Markov kernels. The language is expressive enough to generate continuous distributions, which raises the question of how to effectively compute in the language. This paper gives an alternative characterization of ProbNetKAT’s semantics using domain theory, which provides the foundations needed to build a practical implementation. The new semantics demonstrates that it is possible to analyze ProbNetKAT programs precisely using approximations of fixpoints and distributions with finite support. We develop an implementation and show how to solve a variety of practical problems including characterizing the expected performance of traffic engineering schemes based on randomized routing and reasoning probabilistically about properties such as loop freedom.
slides (2017-01-POPL.pdf) | 4.13MiB |
Thu 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:30 - 17:20 | |||
16:30 25mTalk | A Semantic Account of Metric Preservation POPL Arthur Azevedo de Amorim University of Pennsylvania, USA, Ikram Cherigui ENS Paris, Marco Gaboardi SUNY Buffalo, USA, Justin Hsu , Shin-ya Katsumata Kyoto University | ||
16:55 25mTalk | Cantor Meets Scott: Semantic Foundations for Probabilistic Networks POPL Steffen Smolka Cornell University, Praveen Kumar Cornell University, Nate Foster Cornell University, Dexter Kozen Cornell University, Alexandra Silva University College London DOI File Attached |