论文标题
并发Netkat：建模和分析状态，并发网络
Concurrent NetKAT: Modeling and analyzing stateful, concurrent networks
论文作者
论文摘要
我们介绍了并发Netkat（CNETKAT），这是Netkat与运营商的扩展程序，用于在各个数据包通过状态相互作用的方案中指定和推理有关并发的推理。我们提供了基于部分订购的多键（Pomset）的语言模型，该模型是定义并发语言的示范语义的完善的数学结构。我们提供了该模型的声音和完整的公理化，并通过示例说明了CNETKAT的使用。更笼统地，CNETKAT可以理解为用于与本地状态（包装）和全球状态（在全球商店中）（全球商店）的程序进行推理的代数框架。
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).
