22 Verification bandwidth and audit queues
On this page · Permalink · Source line 1995
Let \(a_t\geq0\) be candidate arrivals during audit cycle \(t\), let \(s_t\geq0\) be service capacity, and let \(B_t\geq0\) be the unresolved backlog. Suppose arrivals in a cycle are available to that cycle's service. The basic deterministic queue is
Theorem 22.1: Constant-rate audit regimes
Suppose \(a_t\equiv\lambda\) and \(s_t\equiv\mu\).
If \(\lambda<\mu\), every finite initial backlog reaches zero after finitely many cycles.
If \(\lambda=\mu\), the backlog remains constant.
If \(\lambda>\mu\), the backlog grows linearly with slope \(\lambda-\mu\).
Proof
Before the truncation at zero, each cycle adds \(\lambda-\mu\). When this quantity is negative, the backlog decreases by a fixed amount until it reaches zero. When it is zero, the backlog is unchanged. When it is positive, the truncation is never active after a nonnegative start, and the backlog is \(B_0+t(\lambda-\mu)\).
A simple audit priority score is
Here \(p_{\mathrm{err}}(x)\in[0,1]\), the consequence and dependency factors are nonnegative, and \(c_{\mathrm{audit}}(x)>0\). Zero-cost checks can be handled separately. This is a declared priority heuristic, not a probability of truth or a proved optimal scheduling rule.