Active Learning of Symbolic NetKAT Automata
summary
Presents algorithms that learn symbolic NetKAT automata from active queries, proves soundness and termination, and ships a prototype implementation with reusable artifacts. Uses a subordinate symbolic transition learner and a generalization step to avoid DFA blowup, evaluates on the Internet Topology Zoo benchmark (≈260 topologies) and learns complete forwarding policies for about half to two‑thirds of networks within a 30‑minute timeout. Artifact and paper links (DOI, Zenodo) are provided.
AI-written summary · about
chapters (14)
- 0:00Active learning of NetKAT automata
- 2:07Unknown network implementations
- 5:18Adapting L* to NetKAT automata
- 6:19Symbolic packet transitions
- 7:25Update behavior challenge
- 9:33Naive DFA and state blowup
- 10:37Partial automata from observations
- 11:19Verification with learned automata
- 11:40Benchmarking on topologies
- 13:06Uniquely minimal correctness
- 13:48Subordinate transition learner
- 14:29Future work on automata
- 14:50Incomplete network telemetry
- 15:10Q&A
related talks
17mKATch: A Fast Symbolic Verifier for NetKAT
25mNetwork Change Validation with Relational NetKAT
47mDeep Programmability: A New Lens on Networking
01h 02mTheory and Control
20mAlgebras for Deterministic Computation are Inherently Incomplete
18mMaking Logic a First-Class Citizen in Generative ML for Networking
24mAutomatically Correcting Networks with NEAt
16mKatra: Realtime Verification for Multilayer Networks