AI 中文总结
研究网络诊断和推理任务中的枚举问题，核心方法是使用参数化NetKAT语言，贡献为介绍其设计语义、编译方法、算法及正确性证明，并评估了在工业基准测试中的性能。
AI 中文摘要
网络工程师常需执行网络诊断和推理任务，常涉及枚举问题。参数化NetKAT是一种新的领域特定语言，融合了NetKAT、关系NetKAT和加权NetKAT的元素并扩展了参数，能让用户直接针对网络模型提出枚举问题。本文介绍了其设计与语义，通过示例展示效用，阐述编译方法、开发算法并证明正确性，最后评估了其在工业基准测试中的性能。
英文摘要
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.
