Network Analysis with Parametric NetKAT
2026-07-10 • Programming Languages
Programming Languages
AI summaryⓘ
The authors introduce Parametric NetKAT, a new language that helps network engineers ask detailed questions about how data packets move or how failures affect a network. This language combines features from earlier tools and adds parameters to make these questions easier to express. They explain how Parametric NetKAT works, show examples, and create methods to efficiently find answers while proving these methods are correct. Finally, they test its performance using real-world network data.
NetKATParametric NetKATnetwork diagnosisnetwork inferenceautomataenumeration queriesnetwork modelinglink failurescompilationvaluation algorithms
Authors
Han Xu, Zachary Kincaid, David Walker
Abstract
Network engineers often need to perform network diagnosis and inference tasks, which frequently require answers to enumeration questions such as "Which packets from the Internet arrive at host C?" or "Which single-link failures disconnect my network?" Parametric NetKAT is a new domain-specific language that combines elements of NetKAT, Relational NetKAT, and Weighted NetKAT into a single system and extends them with parameters, allowing users to pose such enumeration questions directly over network models. This paper presents the design and semantics of Parametric NetKAT and illustrates its utility through a series of examples. It shows how to compile Parametric NetKAT into NetKAT automata, develops new algorithms for efficiently collecting satisfying valuations, and proves the correctness of these procedures. Finally, it evaluates the performance of Parametric NetKAT on a collection of benchmarks drawn from industrial sources.