一句话：提出主动学习未知网络 NetKAT 模型（含符号自动机）的算法，并证明其健全性。
NetKAT 是用于指定和验证分组交换网络行为的领域特定语言与逻辑。本文研究如何通过主动学习自动获得未知网络的 NetKAT 模型。先前工作已对确定性、寄存器、Büchi、时间等多种自动机开展主动学习，并用于验证网络协议实现；作者在此基础上为不同类型的 NetKAT 自动机（包括近期提出的符号自动机）提出学习算法，证明算法健全性，构建原型实现，并在标准基准上评估。结果表明，符号 NetKAT 学习适用于现实的网络配置与拓扑。
NetKAT is a domain-specific programming language and logic that has been successfully used to specify and verify the behavior of packet-switched networks. This paper develops techniques for automatically learning NetKAT models of unknown networks using active learning. Prior work has explored active learning for a wide range of automata (e.g., deterministic, register, Büchi, timed etc.) and also developed applications, such as validating implementations of network protocols. We present algorithms for learning different types of NetKAT automata, including symbolic automata proposed in recent work. We prove the soundness of these algorithms, build a prototype implementation, and evaluate it on a standard benchmark. Our results highlight the applicability of symbolic NetKAT learning for realistic network configurations and topologies.
@article{paperbot3103,
title = {Active Learning of Symbolic NetKAT Automata},
author = {Mark Moeller and Tiago Ferreira and Thomas Lu and Nate Foster and Alexandra Silva},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729295}
}