GUARDED NETKAT: SOUNDNESS, PARTIAL-COMPLETENESS, DECIDABILITY

Other Titles
Abstract
The equational theory of Kleene Algebra with Tests (KAT) provides an algebraic framework to manipulate uninterpreted programs along with a PSPACE-complete procedure for deciding program equivalence. One of the most successful applications of the KAT theory is found in NetKAT, which instantiates the KAT metatheory to an interpreted language with primitives that support reasoning about packets in a network. NetKAT has found wide applications in reasoning about network correctness, with original applications to reachability, traffic isolation, and more. The power of KAT lies in its compact, expressive, and elegant signature - it describes a wide array of imperative programming paradigms, in particular ones which support nondeterminism at the level of programs.Recent research has focused on the guarded fragment of KAT, known in the literature as Guarded Kleene Algebra with Tests (GKAT). This fragment of the KAT language trades expressivity for algorithmic performance. In particular, while remaining uninterpreted, guarded KAT programs have deterministic control flow: given a particular state the next action is completely determined, which differs from KAT in that the latter can compose programs non-deterministically. The upshot is that, even though GKAT can only encode a proper subset of valid KAT programs, the accompanying decision procedure for GKAT is nearly linear compared to the exponential worst-case in KAT. Furthermore, the loss of expressivity is mitigated by the fact that GKAT’s control flow corresponds more closely with traditional programming constructs, such as if-then-else and while-loops. Unfortunately, there have not yet been robust instantiations of the abstract GKAT theory in the same spirit as NetKAT for KAT. This is our present purpose: we aim to combine the primitive semantics and language model from NetKAT with the operations and metatheory from (abstract) GKAT. We offer a limited axiomatization for what we call guarded NetKAT (GNetKAT) and prove soundness and partial-completeness over this fragment. As we discover, it is deceptively difficult to adapt GKAT’s uninterpreted theory to an interpreted setting, as the inclusion of extra axioms and commutativity conditions greatly complicates the metatheory. We proceed to develop a coalgebraic decision procedure to verify GNetKAT semantic program equivalence in nearly linear time, similar to but more elementary than that in the original GKAT setting. We conclude with discussion of applications in the vein of NetKAT. It is our hope that a proper understanding of how GKAT instantiates to its concrete models will motivate further developments in GKAT’s theory, in particular towards resolving its non-algebraic axiomatization.
Journal / Series
Volume & Issue
Description
Sponsorship
Date Issued
2023-05
Publisher
Keywords
Algorithms; Formal methods; Program reasoning
Location
Effective Date
Expiration Date
Sector
Employer
Union
Union Local
NAICS
Number of Workers
Committee Chair
Martins da Silva, Alexandra
Committee Co-Chair
Committee Member
Levine, Lionel
Degree Discipline
Computer Science
Degree Name
M.S., Computer Science
Degree Level
Master of Science
Related Version
Related DOI
Related To
Related Part
Based on Related Item
Has Other Format(s)
Part of Related Item
Related To
Related Publication(s)
Link(s) to Related Publication(s)
References
Link(s) to Reference(s)
Previously Published As
Government Document
ISBN
ISMN
ISSN
Other Identifiers
Rights
Attribution 4.0 International
Types
dissertation or thesis
Accessibility Feature
Accessibility Hazard
Accessibility Summary
Link(s) to Catalog Record