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).


Dexter Campbell Kozen is an American theoretical computer scientist. He is Joseph Newton Pew, Jr. Professor in Engineering at Cornell University.

He is a Fellow of the Association for Computing Machinery,[2] 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.

Dexter Kozen was one of the first professors to receive the honor of a professorship at The Radboud Excellence Initiative at Radboud University Nijmegen in the Netherlands.[3]

He is known for his work at the intersection of logic and complexity. He is one of the fathers of dynamic logic[4] and developed the version of the mu calculus most used today.[5] Moreover, he has written several textbooks on the theory of computation,[6] automata theory, dynamic logic, and algorithms.

More info at:

Scientific host: Professor Fritz Henglein, DIKU