{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,3]],"date-time":"2026-08-03T20:28:22Z","timestamp":1785788902516,"version":"3.56.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N68335-22-C-0411"],"award-info":[{"award-number":["N68335-22-C-0411"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["W912CG-23-C-0032"],"award-info":[{"award-number":["W912CG-23-C-0032"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101002697"],"award-info":[{"award-number":["101002697"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>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\u00fcchi, 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.<\/jats:p>","DOI":"10.1145\/3729295","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1119-1142","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Active Learning of Symbolic NetKAT Automata"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-9512-565X","authenticated-orcid":false,"given":"Mark","family":"Moeller","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6942-0228","authenticated-orcid":false,"given":"Tiago","family":"Ferreira","sequence":"additional","affiliation":[{"name":"University College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-3474-6263","authenticated-orcid":false,"given":"Thomas","family":"Lu","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6557-684X","authenticated-orcid":false,"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"},{"name":"Jane Street, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3544216.3544220"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040314"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Carolyn Jane Anderson Nate Foster Arjun Guha Jean-Baptiste Jeannin Dexter Kozen Cole Schlesinger and David Walker. 2014. NetKAT: Semantic Foundations for Networks. In Proceedings of the 41st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2014). doi:10.1145\/2535838.2535862","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90052-6"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_23"},{"key":"e_1_3_2_7_2","first-page":"1004","volume-title":"Proceedings of the 21st International Joint Conference on Artificial Intelligence (Pasadena, California, USA) (IJCAI\u201909)","author":"Bollig Benedikt","year":"2009","unstructured":"Benedikt Bollig, Peter Habermehl, Carsten Kern, and Martin Leucker. 2009. Angluin-style learning of NFA. In Proceedings of the 21st International Joint Conference on Artificial Intelligence (Pasadena, California, USA) (IJCAI\u201909). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1004\u20131009. http:\/\/ijcai.org\/papers09\/Papers\/IJCAI09-170.pdf"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10431-7_18"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_3"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"Samuel Drews and Loris D\u2019Antoni. 2017. Learning Symbolic Automata. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference TACAS 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2017 Uppsala Sweden April 22-29 2017 Proceedings Part I (Lecture Notes in Computer Science Vol. 10205) Axel Legay and Tiziana Margaria (Eds.). 173\u2013189. doi:10.1007\/978-3-662-54577-5_10","DOI":"10.1007\/978-3-662-54577-5_10"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472938"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-19(2:5)2023"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67113-0_12"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10702-8_6"},{"key":"e_1_3_2_15_2","first-page":"2523","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Fiterau-Brostean Paul","year":"2020","unstructured":"Paul Fiterau-Brostean, Bengt Jonsson, Robert Merget, Joeri de Ruiter, Konstantinos Sagonas, and Juraj Somorovsky. 2020. Analysis of DTLS Implementations Using Protocol State Fuzzing. In 29th USENIX Security Symposium (USENIX Security 20). USENIX Association, 2523\u20132540. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/fiterau-brostean"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Paul Fiterau-Brostean Toon Lenaerts Erik Poll Joeri de Ruiter Frits W. Vaandrager and Patrick Verleg. 2017. Model learning and model checking of SSH implementations. Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software (2017). doi:10.1145\/3092282.3092289","DOI":"10.1145\/3092282.3092289"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Nate Foster Dexter Kozen Mae Milano Alexandra Silva and Laure Thompson. 2015. A Coalgebraic Decision Procedure for NetKAT. In Proceedings of the 42nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2015). doi:10.1145\/2676726.2677011","DOI":"10.1145\/2676726.2677011"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.87284"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60454-5_41"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_26"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3897.001.0001"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2011.111002"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.5555\/867180"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57249-4_6"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Oded Maler and Irini-Eleftheria Mens. 2017. A Generic Algorithm for Learning Symbolic Automata from Membership Queries. 146\u2013169. doi:10.1007\/978-3-319-63121-9_8","DOI":"10.1007\/978-3-319-63121-9_8"},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","unstructured":"Mark Moeller Tiago Ferreira Thomas Lu Nate Foster and Alexandra Silva. 2025. Active Learning of Symbolic NetKAT Automata. arXiv:2504.13794 [cs.PL] https:\/\/arxiv.org\/pdf\/2504.13794","DOI":"10.1145\/3729295"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Mark Moeller Tiago Ferreira Thomas Lu Nate Foster and Alexandra Silva. 2025. Active Learning of Symbolic NetKAT Automata (Artifact). doi:10.5281\/zenodo.15230071","DOI":"10.5281\/zenodo.15230071"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656454"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Anil Nerode. 1958. Linear automaton transformations. doi:10.1090\/S0002-9939-1958-0135681-9","DOI":"10.1090\/S0002-9939-1958-0135681-9"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Spiridon Eliopoulos Nate Foster and Arjun Guha. 2015. A Fast Compiler for NetKAT. In ICFP. doi:10.1145\/2784731.2784761","DOI":"10.1145\/2784731.2784761"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39274-0_3"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386008"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.7298\/Y5X5-JR17"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Stefan Zetzsche Alexandra Silva and Matteo Sammartino. 2022. Guarded Kleene Algebra with Tests: Automata Learning. Electronic Notes in Theoretical Informatics and Computer Science (2022). doi:10.46298\/entics.10505","DOI":"10.46298\/entics.10505"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729295","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729295","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:03:45Z","timestamp":1784196225000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729295"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":33,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729295"],"URL":"https:\/\/doi.org\/10.1145\/3729295","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}