a probabilistic language for networks

Learn More »

State of the art languages and tools for network programming and verification are fundamtentally limited, because they are based on deterministic network models. But real-world networks have many important features that are inherently non-deterministic:

  • Efficient routing protocols distribute flows across multiple paths for better performance.
  • Link failures occur randomly in a network, and
  • Fault-tolerance mechanisms resort to backup paths when links fail.

Probabilistic NetKAT is a language and framework that allows modeling, programming, and reasoning about networks with such probabilistic fatures. It seeks to answer quantitative questions such as:

  • What is the expected congestion of a link, given some model of the network demand?
  • What is the probability of packet delivery, given some failure model of the links?
  • What is the expected latency, given some randomized routing algorithm?

Cornell Cornell



David M. Kahn. Undecidable Problems for Probabilistic Network Programming. In International Symposium on Mathematical Foundations of Computer Science (MFCS), Aalborg, Denmark, July 2017. [ full version ]

Robert Furber, Dexter Kozen, Kim Larsen, Radu Mardare, and Prakash Panangaden. Unrestricted Stone duality for Markov processes. In ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), June 2017. [ conference version ]

Dexter Kozen. On the coalgebraic theory of Kleene algebra with tests. In Can Başkent, Lawrence S. Moss, and Ramaswamy Ramanujam, editors, Rohit Parikh on Logic, Language and Society. March 2017. [ conference version ]

Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. Cantor Meets Scott: Semantic Foundations for Probabilistic Networks. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France, January 2017. [ conference version | full version | slides ]

Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. Probabilistic NetKAT. In European Symposium on Programming (ESOP), Eindhoven, Netherlands, April 2016. [ conference version ]

Probabilistic NetKAT is supported by ERC Starting Grant 679127; the National Security Agency; the National Science Foundation under grants CNS-1111698, CNS- 1413972, CCF-1422046, CCF-1253165, and CCF-1535952; the Office of Naval Research under grant N00014-15-1-2177; the Dutch Research Foundation (NWO) under project numbers 639.021.334 and 612.001.113; and gifts from Cisco, Facebook, Google, and Fujitsu.

  • ERC
  • NSA
  • NSF
  • ONR
  • NWO
  • Facebook
  • Google
  • Fujitsu