We introduce weighted NetKAT, a domain-specific language for modeling and verifying 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.

翻译：我们提出加权NetKAT，这是一种用于建模和验证定量网络属性的领域特定语言。该语言以半环为参数，能够以统一的方式处理各种数量。我们提供了指称语义和等价的操作语义，其中操作语义基于加权NetKAT自动机（WNKA）的新模型，该模型捕捉了语言中的状态行为。借助WNKA，我们获得了一类通用决策过程，即使在可能存在无界迭代的情况下，也能以全自动的方式推理定量安全性和可达性。我们通过以Internet2的Abilene网络为底层拓扑的案例研究，展示了我们框架的适用性。