Weighted NetKAT: A Programming Language for Quantitative Network Verification
Abstract
We introduce weighted NetKAT, a domain-specific language for modeling and verifying quantitative quantitative network properties. The language is parametric on a semiring , enabling the treatment of a wide range of quantities in a uniform way. We provide a denotational semantics and an equivalent operational semantics, the latter based on a novel model of weighted NetKAT automata ( WNKA ) capturing the stateful behavior of our language. With WNKA , we obtain a class of generic decision procedures for reasoning about quantitative safety and reachability in a fully automatic way, even in the presence of possibly unbounded iteration. We demonstrate the applicability of our framework in a case study using Internet2’s Abilene network as the underlying topology.
Fields of Study & Subjects
Formal Methods in Verification
Gene Regulatory Network Analysis
Petri Nets in System Modeling
Publication details
- Journal / source
- Proceedings of the ACM on Programming Languages
- Publisher
- Association for Computing Machinery (ACM)
- Volume
- 10
- Issue
- PLDI
- Pages
- 1788–1811
- Publication date
- 8 June 2026
- Language
- EN