{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T14:29:16Z","timestamp":1754144956447,"version":"3.41.2"},"reference-count":32,"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":0,"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"}]},{"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"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-3474-6263","authenticated-orcid":false,"given":"Thomas","family":"Lu","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}]},{"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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544216.3544220"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040314"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90052-6"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_23"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1661445.1661605"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10431-7_18"},{"volume-title":"Computer Aided Verification","author":"D\u2019Antoni Loris","key":"e_1_2_2_8_1","unstructured":"Loris D\u2019Antoni and Margus Veanes. 2017. The Power of Symbolic Automata and Transducers. In Computer Aided Verification. Springer International Publishing, Cham. 47\u201367. isbn:978-3-319-63387-9"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_10"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472938"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-19(2:5)2023"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67113-0_12"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10702-8_6"},{"key":"e_1_2_2_14_1","volume-title":"Analysis of DTLS Implementations Using Protocol State Fuzzing. In 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. isbn:978-1-939133-17-5 https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/fiterau-brostean"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092282.3092289"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677011"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.87284"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60454-5_41"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_26"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3897.001.0001"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2011.111002"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57249-4_6"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","unstructured":"Oded Maler and Irini-Eleftheria Mens. 2017. A Generic Algorithm for Learning Symbolic Automata from Membership Queries. 146\u2013169. isbn:978-3-319-63120-2 https:\/\/doi.org\/10.1007\/978-3-319-63121-9_8 10.1007\/978-3-319-63121-9_8","DOI":"10.1007\/978-3-319-63121-9_8"},{"key":"e_1_2_2_24_1","unstructured":"Mark Moeller Tiago Ferreira Thomas Lu Nate Foster and Alexandra Silva. 2025. Active Learning of Symbolic NetKAT Automata. arxiv:2504.13794. arxiv:2504.13794"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","unstructured":"Mark Moeller Tiago Ferreira Thomas Lu Nate Foster and Alexandra Silva. 2025. Active Learning of Symbolic NetKAT Automata (Artifact). https:\/\/doi.org\/10.5281\/zenodo.15230071 10.5281\/zenodo.15230071","DOI":"10.5281\/zenodo.15230071"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656454"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","unstructured":"Anil Nerode. 1958. Linear automaton transformations. https:\/\/doi.org\/10.1090\/S0002-9939-1958-0135681-9 10.1090\/S0002-9939-1958-0135681-9","DOI":"10.1090\/S0002-9939-1958-0135681-9"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Spiridon Eliopoulos Nate Foster and Arjun Guha. 2015. A Fast Compiler for NetKAT. In ICFP. https:\/\/doi.org\/10.1145\/2784731.2784761 10.1145\/2784731.2784761","DOI":"10.1145\/2784731.2784761"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39274-0_3"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386008"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.7298\/Y5X5-JR17"},{"key":"e_1_2_2_32_1","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 https:\/\/doi.org\/10.46298\/entics.10505 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":[[2025,7,16]],"date-time":"2025-07-16T06:04:50Z","timestamp":1752645890000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729295"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":32,"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":[{"type":"electronic","value":"2475-1421"}],"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"}}]}}