Applications of Automata and Concurrency Theory in Networks (Invited Paper)

Author Alexandra Silva



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.42.pdf
  • Filesize: 261 kB
  • 2 pages

Document Identifiers

Author Details

Alexandra Silva

Cite AsGet BibTex

Alexandra Silva. Applications of Automata and Concurrency Theory in Networks (Invited Paper). In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 42-43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CONCUR.2015.42

Abstract

Networks have received widespread attention in recent years as a target for domain-specific language design. The emergence of software-defined networking (SDN) as a popular paradigm for network programming has led to the appearance of a number of SDN programming languages seeking to provide high-level abstractions to simplify the task of specifying the packet-processing behavior of a network. Previous work by Anderson et al. [Anderson et al.,POPL'14,2014] introduced NetKAT, a language and logic for specifying and verifying the packet-processing behavior of networks. NetKAT provides general-purpose programming constructs such as parallel and sequential composition, conditional tests, and iteration, as well as special-purpose primitives for querying and modifying packet headers and encoding network topologies. In contrast to competing approaches, NetKAT has a formal mathematical semantics and an equational deductive system that is sound and complete over that semantics, as well as a PSPACE decision procedure. It is based on Kleene algebra with tests (KAT), an algebraic system for propositional program verification that has been extensively studied for nearly two decades [Kozen,ACM Trans. Program. Lang. Syst.,1997]. Several practical applications of NetKAT have been developed, including algorithms for testing reachability and non-interference and a syntactic correctness proof for a compiler that translates programs to hardware instructions for SDN switches. In a follow-up paper [Foster et al.,POPL'15,2015], the coalgebraic theory of NetKAT was developed and a bisimulation-based algorithm for deciding equivalence was devised. The new algorithm was shown to be significantly more efficient than the previous naive algorithm [Anderson et al.,POPL'14,2014], which was PSPACE in the best case and the worst case, as it was based on the determinization of a nondeterministic algorithm. Along with the coalgebraic model of NetKAT, the authors presented a specialized version of the Brzozowski derivative in both semantic and syntactic forms. They also also proved a version of Kleene's theorem for NetKAT that shows that the coalgebraic model is equivalent to the standard packet-processing and language models introduced previously [Anderson et al.,POPL'14,2014]. They demonstrated the real-world applicability of the tool by using it to decide common network verification questions such as all-pairs connectivity, loop-freedom, and translation validation - all pressing questions in modern networks. This talk will survey applications of automata theory, concurrency theory and coalgebra to problems in networking. We will suggest directions for exploring the bridge between the two communities and ways to deliver new synergies. On the one hand, this will lead to new insights and techniques that will enable the development of rigorous semantic foundations for networks. On the other hand, the idysiocransies of networks will provide new challenges for the automata and concurrency community.
Keywords
  • Automata
  • network programming
  • coalgebra

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Carolyn Jane 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'14, San Diego, CA, USA, January 20-21, 2014, pages 113-126. ACM, 2014. Google Scholar
  2. Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva, and Laure Thompson. A coalgebraic decision procedure for netkat. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'15, Mumbai, India, January 15-17, 2015, pages 343-355. ACM, 2015. Google Scholar
  3. Dexter Kozen. Kleene algebra with tests. ACM Trans. Program. Lang. Syst., 19(3):427-443, 1997. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail