Concurrent NetKAT. Modeling and analyzing stateful, concurrent networks

DOI10.1007/978-3-030-99336-8_21MaRDI QIDQ6166804zbMATH OpenOpenAlexFDO

Authors Jana Wagemaker, Nate Foster, Tobias Kappé, Dexter Kozen, Jurriaan Rot, Alexandra Silva

Publication date 3 August 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2201.10485

zbMATH Keywords

completenessconcurrencyconcurrent Kleene algebraNetKAT

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We introduce Concurrent NetKAT (CNetKAT), an extension of NetKAT with operators for specifying and reasoning about concurrency in scenarios where multiple packets interact through state. We provide a model of the language based on partially-ordered multisets (pomsets), which are a well-established mathematical structure for defining the denotational semantics of concurrent languages. We provide a sound and complete axiomatization of this model, and we illustrate the use of CNetKAT through examples. More generally, CNetKAT can be understood as an algebraic framework for reasoning about programs with both local state (in packets) and global state (in a global store).

Recommendations

• Probabilistic NetKAT
• DyNetKAT: an algebra of dynamic networks
• A coalgebraic decision procedure for NetKAT
• Netkat, semantic foundations for networks
• Concurrent NetCore: from policies to pipelines

Cites work

• scientific article; zbMATH DE number 3735177 (Why is no real title available?)
• scientific article; zbMATH DE number 177804 (Why is no real title available?)
• scientific article; zbMATH DE number 7559476 (Why is no real title available?)
• scientific article; zbMATH DE number 7204945 (Why is no real title available?)
• scientific article; zbMATH DE number 3366846 (Why is no real title available?)
• A coalgebraic decision procedure for NetKAT
• A completeness theorem for Kleene algebras and the algebra of regular events
• Completeness theorems for bi-Kleene algebras and series-parallel rational pomset languages
• Concurrent Kleene Algebra
• Concurrent Kleene algebra with observations: from hypotheses to completeness
• Concurrent Kleene algebra with tests and branching automata
• Concurrent Kleene algebra: free model and completeness
• Concurrent NetCore: from policies to pipelines
• Netkat, semantic foundations for networks
• Petri automata
• Series-parallel languages and the bounded-width property
• The Böhm–Jacopini Theorem Is False, Propositionally
• The equational theory of pomsets
• Two Complete Axiom Systems for the Algebra of Regular Events

This page was built for publication: Concurrent NetKAT. Modeling and analyzing stateful, concurrent networks

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166804)