Certified Closed-Loop Control for Packet Networks: A Compositional Certification Framework
2026-06-01 • Networking and Internet Architecture
Networking and Internet Architecture
AI summaryⓘ
The authors treat network packet control like a safety check system, where a special operator verifies proposed actions from a controller before they're carried out. If the proposed action is unsafe, the operator either adjusts it to a safe one or switches to a backup action that has guaranteed limits. They provide mathematical guarantees that these certified actions prevent problems like delays or unstable queues under certain conditions. The paper also discusses how this approach handles real-world issues like delayed feedback and system overload, and they test their design at a detailed packet level but leave large-scale deployment experiments for future work.
packet networksdynamical systemsqueue stabilityLyapunov driftaction certificationbacklog boundsservice guaranteesdelayed telemetrycompositional contractssmall-gain theorem
Authors
Muhammad Bilal, Jon Crowcroft, Xiaolong Xu, Huaming Wu
Abstract
Packet networks are controlled dynamical systems with discontinuities, delayed observations, and partial state information. Adaptive or learning-driven proposers can improve performance, but an unsafe proposal may still cause starvation, tail-delay spikes, or unstable queue behaviour. This paper treats packet-network control as an executed-action certification problem. A certified operator sits between any proposer and the dataplane. At each control tick, the proposer emits an arbitrary candidate action $\tilde u(t)$. The operator either projects it to an executable action $u(t)$ that satisfies a configuration-compiled certificate, or reports INFEASIBLE and executes an always-defined fallback with quantified slack. The certificate also exports an auditable envelope $\bar z(t)$ for downstream composition. The guarantees are conditional and explicit. They apply on ticks where the operator reports CERTIFIED, the declared arrival envelope and backlog bound are valid, and the platform realises the assumed service lower bound. Under these conditions, one mechanism covers backlog caps, service floors, mitigation caps, Foster--Lyapunov drift constraints, and compositional envelope contracts. We prove operator-level safety, feed-forward compositional safety and stability using exported envelopes, and a cyclic closure result under a small-gain condition. We also define breach and infeasibility semantics, discuss calibration of the service-tracking factor that links certified targets to realised scheduler behaviour, and evaluate the design under delayed telemetry, delayed actuation, weak proposers, envelope mismatch, overload, and millisecond-scale certification. The present evaluation validates the certified execution boundary in a byte-level closed-loop backend; deployment-level scheduler tracking is left to future Linux or hardware experiments.