Cantor Meets Scott: Semantic Foundations for Probabilistic Networks - By Dexter Kozen
A DIKU/MATH Talk by Dexter Kozen, Cornell University
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).
He is a Fellow of the Association for Computing Machinery, a Guggenheim Fellow, and has received an Outstanding Innovation Award from IBM Corporation. He has also been named Faculty of the Year by the Association of Computer Science Undergraduates at Cornell.
He is known for his work at the intersection of logic and complexity. He is one of the fathers of dynamic logic and developed the version of the mu calculus most used today. Moreover, he has written several textbooks on the theory of computation, automata theory, dynamic logic, and algorithms.
More info at: https://en.wikipedia.org/wiki/Dexter_Kozen
Scientific host: Professor Fritz Henglein, DIKU