概率网络的可扩展验证
Scalable Verification of Probabilistic Networks
摘要：
本文介绍了McNetKAT，一个可扩展的工具，用于验证概率网络程序。McNetKAT是基于一个新的语义的保护和历史自由片段的概率NetKAT的有限状态，吸收马尔可夫链。该视图允许精确计算所有程序的语义，从而能够构建自动验证工具。特定于域的优化和并行后端使McNetKAT能够分析具有数千个节点的网络，自动推理诸如概率程序等价和细化等一般属性，以及诸如故障恢复等网络属性。我们评估McNetKAT的可扩展性，使用现实世界的拓扑结构，比较其性能对国家的最先进的工具，并开发一个扩展的案例研究最近提出的数据中心网络设计。
英文摘要：
This paper presents McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the guarded and history-free fragment of Probabilistic NetKAT in terms of finite-state, absorbing Markov chains. This view allows the semantics of all programs to be computed exactly, enabling construction of an automatic verification tool. Domain-specific optimizations and a parallelizing backend enable McNetKAT to analyze networks with thousands of nodes, automatically reasoning about general properties such as probabilistic program equivalence and refinement, as well as networking properties such as resilience to failures. We evaluate McNetKAT's scalability using real-world topologies, compare its performance against state-of-the-art tools, and develop an extended case study on a recently proposed data center network design.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
