一句话：提出 Relational NetKAT 规格语言与转换器/自动机算法，以验证网络变更是否符合意图。
网络变更常因实现与意图不一致而引入错误。本文提出关系式 NetKAT（RN）规格语言：工程师给出迹关系 R，将变更前网络的包迹映射到变更后网络的预期包迹，再与实际迹比较以发现错误。迹关系由迹插入、删除、包变换等组合子及连接、并、迭代等正则算子复合而成。作者将迹关系编译为新型 NetKAT 转换器，并构造自动机识别 NetKAT 自动机在转换器下的像；结合已有 NetKAT 等价判定即可验证变更。文章给出指称语义、证明编译正确、实现工具，并在生产网络与 Amazon Batfish 基准上评估。
Relational NetKAT (RN) is a new specification language for network change validation. Engineers use RN to specify intended changes by providing a trace relation R , which maps existing packet traces in the pre-change network to intended packet traces in the post-change network. The intended set of traces may then be checked against the actual post-change traces to uncover errors in implementation. Trace relations are constructed compositionally from a language of combinators that include trace insertion, trace deletion, and packet transformation, as well as regular operators for concatenation, union, and iteration of relations. We provide algorithms for converting trace relations into a new form of NetKAT transducer and also for constructing an automaton that recognizes the image of a NetKAT automaton under a NetKAT transducer. These algorithms, together with existing decision procedures for NetKAT automaton equivalence, suffice for validating network changes. We provide a denotational semantics for our specification language, prove our compilation algorithms correct, implement a tool for network change validation, and evaluate it on a set of benchmarks drawn from a production network and Amazon’s Batfish toolkit.
@article{XuKMW26,
title = {Network Change Validation with Relational NetKAT},
author = {Han Xu and Zachary Kincaid and Ratul Mahajan and David Walker},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776656}
}