{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:10:36Z","timestamp":1768000236189,"version":"3.49.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030992521","type":"print"},{"value":"9783030992538","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce a formal language for specifying dynamic updates for Software Defined Networks. Our language builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs for synchronisations and multi-packet behaviour to capture the interaction between the control- and data-plane in dynamic updates. We provide a sound and ground-complete axiomatisation of our language. We exploit the equational theory and provide an efficient method for reasoning about safety properties. We implement our equational theory in DyNetiKAT \u2013 a tool prototype, based on the Maude Rewriting Logic and the NetKAT tool, and apply it to a case study. We show that we can analyse the case study for networks with hundreds of switches using our tool prototype.<\/jats:p>","DOI":"10.1007\/978-3-030-99253-8_10","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"184-204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["DyNetKAT: An Algebra of Dynamic Networks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8653-2299","authenticated-orcid":false,"given":"Georgiana","family":"Caltais","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4743-8750","authenticated-orcid":false,"given":"Hossein","family":"Hojjat","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4869-6794","authenticated-orcid":false,"given":"Mohammad Reza","family":"Mousavi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9125-8506","authenticated-orcid":false,"given":"H\u00fcnkar Can","family":"Tun\u00e7","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","unstructured":"Luca Aceto, Bard Bloom, and Frits\u00a0W. Vaandrager. Turning SOS rules into equations. Inf. Comput., 111(1):1\u201352, 1994. https:\/\/doi.org\/10.1006\/inco.1994.1040.","DOI":"10.1006\/inco.1994.1040"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"L.\u00a0Aceto, W.\u00a0J. Fokkink, and C.\u00a0Verhoef. Conservative extension in structural operational semantics. Bull. EATCS, 69:110\u2013132, 1999.","DOI":"10.7146\/brics.v6i24.20093"},{"key":"10_CR3","doi-asserted-by":"publisher","unstructured":"Carolyn\u00a0Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. NetKAT: semantic foundations for networks. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, January 20-21, 2014, pages 113\u2013126. ACM, 2014. https:\/\/doi.org\/10.1145\/2535838.2535862.","DOI":"10.1145\/2535838.2535862"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Jos C.\u00a0M. Baeten and W.\u00a0P. Weijland. Process algebra, volume\u00a018 of Cambridge tracts in theoretical computer science. Cambridge University Press, 1990.","DOI":"10.1017\/CBO9780511624193"},{"key":"10_CR5","unstructured":"Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008."},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"Ryan Beckett, Michael Greenberg, and David Walker. Temporal netkat. In Chandra Krintz and Emery Berger, editors, Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 386\u2013401. ACM, 2016. https:\/\/doi.org\/10.1145\/2908080.2908108.","DOI":"10.1145\/2908080.2908108"},{"key":"10_CR7","unstructured":"G.\u00a0Caltais, H.\u00a0Hojjat, M.\u00a0R. Mousavi, and H.\u00a0C. Tunc. DyNetKAT: An algebra of dynamic networks. CoRR, abs\/2102.10035, 2021."},{"key":"10_CR8","doi-asserted-by":"publisher","unstructured":"Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet, Jos\u00e9 Meseguer, and Carolyn\u00a0L. Talcott. Full Maude: Extending Core Maude. In Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet, Jos\u00e9 Meseguer, and arolyn\u00a0L. Talcott, editors, All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science, pages 559\u2013597. Springer, 2007. https:\/\/doi.org\/10.1007\/978-3-540-71999-1_18.","DOI":"10.1007\/978-3-540-71999-1_18"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. Probabilistic NetKAT. In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 282\u2013309. Springer, 2016. https:\/\/doi.org\/10.1007\/978-3-662-49498-1_12.","DOI":"10.1007\/978-3-662-49498-1_12"},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva, and Laure Thompson. A Coalgebraic Decision Procedure for NetKAT. In Sriram\u00a0K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 343\u2013355. ACM, 2015. https:\/\/doi.org\/10.1145\/2676726.2677011.","DOI":"10.1145\/2676726.2677011"},{"key":"10_CR11","unstructured":"Tobias Kapp\u00e9, Paul Brunet, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness. CoRR, abs\/2002.09682, 2020. URL: https:\/\/arxiv.org\/abs\/2002.09682, http:\/\/arxiv.org\/abs\/2002.09682."},{"key":"10_CR12","unstructured":"Hyojoon Kim, Joshua Reich, Arpit Gupta, Muhammad Shahbaz, Nick Feamster, and Russell\u00a0J. Clark. Kinetic: Verifiable dynamic network control. In 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4-6, 2015, pages 59\u201372. USENIX Association, 2015. URL: https:\/\/www.usenix.org\/conference\/nsdi15\/technical-sessions\/presentation\/kim."},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"Jedidiah McClurg, Hossein Hojjat, Nate Foster, and Pavol Cern\u00fd. Event-driven network programming. In Chandra Krintz and Emery Berger, editors, Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 369\u2013385. ACM, 2016. https:\/\/doi.org\/10.1145\/2908080.2908097.","DOI":"10.1145\/2908080.2908097"},{"key":"10_CR14","doi-asserted-by":"publisher","unstructured":"Peter D. Mosses. Modular structural operational semantics. J. Log. Algebraic Methods Program. 60-61: 195-228, 2004. https:\/\/doi.org\/10.1016\/j.jlap.2004.03.008","DOI":"10.1016\/j.jlap.2004.03.008"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Mohammad\u00a0Reza Mousavi, Michel\u00a0A. Reniers, and Jan\u00a0Friso Groote. Notions of bisimulation and congruence formats for SOS with data. Information and Computation, 200(1):107 \u2013 147, 2005. https:\/\/doi.org\/10.1016\/j.ic.2005.03.002.","DOI":"10.1016\/j.ic.2005.03.002"},{"key":"10_CR16","unstructured":"Tim Nelson, Andrew\u00a0D. Ferguson, Michael J.\u00a0G. Scheer, and Shriram Krishnamurthi. Tierless programming and reasoning for software-defined networks. In Ratul Mahajan and Ion Stoica, editors, Proceedings of the 11th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2014, Seattle, WA, USA, April 2-4, 2014, pages 519\u2013531. USENIX Association, 2014. URL: https:\/\/www.usenix.org\/conference\/nsdi14\/technical-sessions\/presentation\/nelson."},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Mark Reitblatt, Nate Foster, Jennifer Rexford, Cole Schlesinger, and David Walker. Abstractions for network update. In Lars Eggert, J\u00f6rg Ott, Venkata\u00a0N. Padmanabhan, and George Varghese, editors, ACM SIGCOMM 2012 Conference, SIGCOMM \u201912, Helsinki, Finland - August 13 - 17, 2012, pages 323\u2013334. ACM, 2012. https:\/\/doi.org\/10.1145\/2342356.2342427.","DOI":"10.1145\/2342356.2342427"},{"key":"10_CR18","unstructured":"Alexandra Silva. Models of Concurrent Kleene Algebra. In Elvira Albert and Laura Kov\u00e1cs, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume\u00a073 of EPiC Series in Computing, page 516. EasyChair, 2020. URL: https:\/\/easychair.org\/publications\/paper\/6C8R."},{"key":"10_CR19","unstructured":"Guido van Rossum. Python programming language. In Jeff Chase and Srinivasan Seshan, editors, Proceedings of the 2007 USENIX Annual Technical Conference, Santa Clara, CA, USA, June 17-22, 2007. USENIX, 2007."},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Alexander Vandenbroucke and Tom Schrijvers. P$$\\lambda $$$$\\omega $$nk: functional probabilistic netkat. Proc. ACM Program. Lang., 4(POPL):39:1\u201339:27, 2020. https:\/\/doi.org\/10.1145\/3371107.","DOI":"10.1145\/3371107"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Jana Wagemaker, Paul Brunet, Simon Docherty, Tobias Kapp\u00e9, Jurriaan Rot, and Alexandra Silva. Partially Observable Concurrent Kleene Algebra. In Igor Konnov and Laura Kov\u00e1cs, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 20:1\u201320:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2020. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.20.","DOI":"10.4230\/LIPIcs.CONCUR.2020.20"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"Al-Fares, Mohammad and Loukissas, Alexander and Vahdat, Amin. A Scalable, Commodity Data Center Network Architecture. ACM SIGCOMM Comput. Commun. Rev. 38, 4, 63-74, 2008. https:\/\/doi.org\/10.1145\/1402946.1402967.","DOI":"10.1145\/1402946.1402967"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99253-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:05:54Z","timestamp":1648497954000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99253-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030992521","9783030992538"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99253-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}