Concurrent NetKAT. Modeling and analyzing stateful, concurrent networks

DOI10.1007/978-3-030-99336-8_21zbMATH Open1528.68259arXiv2201.10485OpenAlexW4226090351MaRDI QIDQ6166804FDOQ6166804

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

Publication date: 3 August 2023

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

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).

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)

Cites Work

• NetKAT
• Title not available (Why is that?)
• Two Complete Axiom Systems for the Algebra of Regular Events
• The equational theory of pomsets
• A completeness theorem for Kleene algebras and the algebra of regular events
• Series-parallel languages and the bounded-width property
• Concurrent Kleene algebra with tests and branching automata
• Concurrent Kleene Algebra
• Title not available (Why is that?)
• Title not available (Why is that?)
• Completeness Theorems for Bi-Kleene Algebras and Series-Parallel Rational Pomset Languages
• A coalgebraic decision procedure for NetKAT
• Concurrent Kleene algebra: free model and completeness
• Title not available (Why is that?)
• Title not available (Why is that?)
• Concurrent Kleene algebra with observations: from hypotheses to completeness
• The Böhm–Jacopini Theorem Is False, Propositionally
• Concurrent NetCore: from policies to pipelines
• Title not available (Why is that?)

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)