AI 中文总结
本文提出基于加权NetKAT的定量网络属性快速分析器，设计加权符号分组程序等，符号化计算策略构造，开发带迹帕累托半环，在Lean中形式化并提供Rust实现，在经典和定量分析上有优势，支持多目标设计时分析。
AI 中文摘要
在设计网络时，工程师必须权衡各种因素，这需要对定量属性进行推理。我们提出了一种基于加权NetKAT（wNetKAT）的定量网络属性快速分析器，wNetKAT是一种领域特定语言，通过使用半环中的权重对网络行为进行建模，为定量推理提供语义基础。我们设计了加权符号分组程序（wSPPs）这一符号数据结构来紧凑表示加权策略的语义。展示了如何符号化计算所有策略构造，关键在于为Kleene star设计了定制算法。还开发了带迹帕累托半环来计算多目标前沿及实现它们的网络路径。在Lean中进行了形式化并提供了优化的Rust实现。该实现涵盖经典和定量分析，在概率分析中比McNetKAT和Storm快几个数量级，与KATch具有竞争力。一个比较Fat-tree和Jellyfish数据中心拓扑的案例研究表明该框架支持多目标设计时分析。
英文摘要
When designing a network, engineers must navigate trade-offs (e.g., one topology offers more aggregate bandwidth, another lower latency or better resilience) that demand reasoning about quantitative properties. We present a fast analyzer for quantitative network properties based on weighted NetKAT (wNetKAT), a domain-specific language that provides a semantic foundation for quantitative reasoning by modeling network behavior using weights drawn from a semiring. At the core of our development is the design of a symbolic data structure -- weighted symbolic packet programs (wSPPs) -- that compactly represent the semantics of weighted policies, for which a direct implementation would be intractable. We show how to compute all policy constructs symbolically; unsurprisingly, the crux is Kleene star, for which we design a tailored algorithm. We further develop trace-carrying Pareto semirings, which compute multi-objective frontiers together with the network paths that realize them. We formalize the development in Lean and provide an optimized Rust implementation. Being parametric on a semiring, our implementation covers both classical and quantitative analyses: we show that it is competitive with KATch, a heavily optimized Boolean-reachability verifier, and orders of magnitude faster than McNetKAT and Storm on probabilistic analyses. A case study comparing Fat-tree and Jellyfish data-center topologies shows the framework supports multi-objective design-time analysis.
