Queueing and Stochastic Networks

Motivation

The single-server queue with general independent interarrival and service times, the G/G/1 queue, is the basic model of a congested resource: a machine, a link, a checkout. For Markovian arrivals or services the mean wait has a closed form (the Pollaczek–Khintchine formula for M/G/1, the geometric law for G/M/1). For general distributions it has none, and the mean wait depends on the whole distributions of the interarrival and service times, not only on their moments. Capacity planning still needs numbers. Bounds that use only the first two moments are therefore the practical tool. They say how bad congestion can be for any queue with a given arrival rate, service rate and variabilities, and they become exact as the traffic intensity approaches one.

This mission formalizes Chapter 7, §7.1 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), together with the heavy-traffic Theorem 7.1 of §7.2.3.

Timeline. Lindley (Proc. Cambridge Philos. Soc., 1952) derived the recursion for successive waiting times and characterized the stationary law. Kingman (Proc. Cambridge Philos. Soc., 1961, 1962) proved the heavy-traffic exponential limit. In "Some inequalities for the queue GI/G/1" (Biometrika, 1962) he proved the two-moment upper bound. Marshall (1968) derived further moment relations and bounds (Operations Research, 1968). Marchal (Operations Research, 1978) gave the lower bound (7.14).

Setting

A G/G/1 queue is specified by two probability laws on $[0,\infty)$: the law $A$ of an interarrival time $T$ and the law $B$ of a service time $S$. Both have finite second moments, and

$$E[T] = \frac1\lambda,\quad E[S] = \frac1\mu,\quad \sigma_A^2 = \mathrm{Var}[T],\quad \sigma_B^2 = \mathrm{Var}[S],\quad \rho = \frac{\lambda}{\mu}.$$

The pairs $(S^{(n)}, T^{(n)})$ are independent and identically distributed, and $S^{(n)}$ is independent of $T^{(n)}$. Customers are served first come, first served. The line delay $W_q^{(n)}$ of the $n$th customer obeys Lindley's recursion

$$W_q^{(n+1)} = \max\bigl(0,\ W_q^{(n)} + U^{(n)}\bigr), \qquad U^{(n)} = S^{(n)} - T^{(n)}, \tag{7.1}$$

and $W_q^{(n)}$ is independent of $(S^{(n)}, T^{(n)})$. The idle gap $X^{(n)} = -\min(0, W_q^{(n)} + U^{(n)})$ is the time between the $n$th departure and the next start of service.

The queue is stationary when the law $\nu$ of $W_q^{(n)}$ does not depend on $n$, that is, when one step of (7.1) maps $\nu$ to itself. The mean stationary line delay is $W_q = E[W_q^{(n)}] = \int w\,d\nu(w)$. In the Lean development these objects are IsGG1Input A B lam mu, lindley, idleX, IsStationaryWaitLaw A B ν and meanWait ν, in the namespace QueueingFundamentals.Bounds.

Formalization targets

Goal: Kingman's upper bound (7.13)

For every stationary G/G/1 queue with $\rho < 1$, $W_q$ is finite and

$$W_q \le \frac{\lambda(\sigma_A^2 + \sigma_B^2)}{2(1-\rho)}.$$

Milestones

• the idle-gap identity $E[X] = -E[U] = 1/\lambda - 1/\mu$ (7.4), and the mean-wait formula (7.7)

$$W_q = \frac{E[X^2] - E[U^2]}{2E[U]};$$

• the variance of the interdeparture time $D = S^{(n+1)} + X^{(n)}$ (7.12): $\mathrm{Var}[D] = 2\sigma_B^2 + \sigma_A^2 - 2W_q(1/\lambda - 1/\mu)$;
• Marchal's lower bound (7.14), $W_q \ge (\lambda^2\sigma_B^2 + \rho(\rho-2))/(2\lambda(1-\rho))$;
• the distributional lower bound $W_q \ge r_0$, with $r_0$ the unique nonnegative root of $f(z) = z - \int_{-z}^\infty [1 - U(t)]\,dt$ and $U(t)$ the CDF of $S - T$ ((7.15), (7.16));
• the two-sided estimate (7.17), $\max\bigl(0, r_0, \tfrac{\lambda^2\sigma_B^2 + \rho(\rho-2)}{2\lambda(1-\rho)}\bigr) \le W_q \le \tfrac{\lambda(\sigma_A^2+\sigma_B^2)}{2(1-\rho)}$;
• Theorem 7.1 (heavy traffic): for a sequence of G/G/1 queues with $\rho_j \to 1$, $\alpha_j = -E[S_j - T_j]$ and $\beta_j^2 = \mathrm{Var}[S_j - T_j]$, under convergence of the input laws, $\mathrm{Var}[S - T] > 0$ and uniformly bounded $(2+\delta)$-moments,

$$\frac{2\alpha_j}{\beta_j^2}\,W_{q,j} \xrightarrow{d} \mathrm{Exp}(1).$$

The goal is (7.13) rather than the stronger (7.17) because it depends only on the first two moments of the input.

Significance

Kingman's bound is the most widely used performance estimate for single-server queues. It needs no distributional form, only two means and two variances. It yields the "Kingman formula" approximation used across manufacturing and service operations, and it is asymptotically exact as $\rho \to 1$ (Theorem 7.1). The departure variance (7.12) drives the decomposition approximations for networks of §7.3. The heavy-traffic theorem is the entry point to diffusion approximations of queues.

All results here are proved in the literature (Theorem 7.1 is stated in the book without proof). This mission produces the first machine-checked versions. As far as a search of the platform shows, none of these statements, and no stationary Lindley recursion, has been formalized. The substrate it needs is reusable for any mission on G/G/1, G/G/c or random walks: stationary laws of a recursion on distributions, moment identities for $\max(0,\cdot)$, and convergence in distribution.

Difficulty

The book's derivation squares (7.3) and takes expectations, using $E[(W_q^{(n+1)})^2] = E[(W_q^{(n)})^2]$. That step is valid only if the stationary wait has a finite second moment. It is not assumed here and fails in general: with finite second moments of $S$ and $T$ the stationary wait has a finite mean, but its second moment is finite only if $E[S^3] < \infty$. So the moment identity (7.7) cannot be obtained by cancelling second moments. A truncation or limiting argument is needed, and even the finiteness of $W_q$ has to be proved rather than assumed. The lower bound $W_q \ge r_0$ further needs a Jensen argument for the conditional mean of one Lindley step. Theorem 7.1 needs a uniform-integrability argument across a sequence of queues.

Formalization scope

Conventions committed to in Lean:

• laws, not random variables: $A$, $B$ and the stationary law $\nu$ are Measure ℝ; independence of $W_q^{(n)}, S^{(n)}, T^{(n)}$ (and $S^{(n+1)}$ for $D$) is the product measure;
• the input laws are probability measures on $[0,\infty)$ with finite second moments (MemLp id 2), $E[T] = 1/\lambda$, $E[S] = 1/\mu$, $\lambda, \mu > 0$, $\rho = \lambda/\mu < 1$;
• stationarity is invariance of the whole law $\nu$ under one step of (7.1), not equality of means;
• $W_q$, the variances (Mathlib variance) and $f_1$ are Lebesgue integrals. Every theorem therefore asserts, as part of its conclusion, that $\nu$ has a finite mean, and none assumes a finite second moment of $\nu$;
• $U(t)$ is Mathlib's cdf of the law of $S - T$;
• convergence in distribution is convergence of $\int g$ for all bounded continuous $g$, and $\mathrm{Exp}(1)$ is expMeasure 1.

Closed forms carried by the statements: (7.4), (7.7), (7.12), (7.13), (7.14) and (7.17) exactly as printed, and the scaling $2\alpha_j/\beta_j^2$ of Theorem 7.1.

Stating (7.13) with $W_q$, $E[X^2]$ or the idle probability as free real numbers constrained by (7.7) would reduce it to algebra. Here $W_q$ is always the mean of a stationary law of the queue.

Not formalized: (7.5) and (7.8), which need the idle-period law $I$ and the arrival-point probability $q_0$ as separate objects, and the multiserver bounds of §7.1.3. Proofs of any milestone are welcome, as are reusable lemmas on stationary laws of Lindley's recursion (existence, uniqueness, and finiteness of the mean under $E[S^2] < \infty$).

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
• D. V. Lindley, The theory of queues with a single server, Math. Proc. Cambridge Philos. Soc. 48 (1952)
• J. F. C. Kingman, The single server queue in heavy traffic, Math. Proc. Cambridge Philos. Soc. 57 (1961)
• J. F. C. Kingman, Some inequalities for the queue GI/G/1, Biometrika 49 (1962)
• K. T. Marshall, Some inequalities in queuing, Operations Research 16 (1968)
• W. G. Marchal, Some simpler bounds on the mean queuing time, Operations Research 26 (1978)

Motivation

A call center with $N$ agents facing Poisson arrivals at rate $\lambda$ and exponential service at rate $\mu$ is the M/M/N (Erlang-C) queue. Choosing $N$ trades the cost of agents against the cost of customers waiting, and in practice it is done with the square-root safety-staffing rule $N \approx R + y\sqrt R$, where $R = \lambda/\mu$ is the offered load. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) turned that rule of thumb into an optimization result: for a general convex staffing cost and a general waiting-cost function, they identify the safety factor $y$ that makes the rule asymptotically optimal as the arrival rate grows.

Timeline of the asymptotic regime the paper builds on:

• 1917. Erlang's delay formula $\pi(N,\nu)$ for the M/M/N queue.
• 1981. Halfin and Whitt (Oper. Res. 29(3)) show that with $N = R + \beta\sqrt R$ servers the probability of waiting converges to a limit $P(\beta) \in (0,1)$, the quality-and-efficiency-driven regime.
• 2000/2004. Borst, Mandelbaum and Reiman classify cost structures into a rationalized, an efficiency-driven and a quality-driven regime, and prove asymptotic optimality of an explicit staffing rule in each.

This mission is the first of a series of four on that paper and covers the rationalized regime (Section 5), where staffing and waiting costs are of the same order.

Setting

The service rate $\mu > 0$ is fixed and the arrival rate $\lambda$ grows. A staffing cost $F$, defined on $(0,\infty)$, is convex and strictly increasing; it does not depend on $\lambda$. For each $\lambda > 0$ a waiting-cost function $D_\lambda$ satisfies $D_\lambda(0)=0$, is strictly increasing on $[0,\infty)$, and makes

$$G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)\,e^{-(N\mu-\lambda)t}\,dt$$

finite for every $N > \lambda/\mu$. With the Erlang-C formula

$$\pi(N,\nu) = \frac{\nu^N}{N!}\Big\{\big(1-\tfrac{\nu}{N}\big)\sum_{n=0}^{N-1}\frac{\nu^n}{n!}+\frac{\nu^N}{N!}\Big\}^{-1},$$

the expected total cost of staffing $N > \lambda/\mu$ agents is $C(N,\lambda) = F(N) + \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda)$, and $N^*_\lambda$ is any integer $N > \lambda/\mu$ minimizing it (7).

In normalized units $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$ the paper defines $F_\lambda(x) = F(N_\lambda(x)) - F(\lambda/\mu)$, $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$, the continuous delay probability $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$ with

$$H(M,\alpha) = \Big\{\alpha\int_0^\infty e^{-\alpha t}\,t\,(1+t)^{M-1}\,dt\Big\}^{-1},$$

and $C_\lambda(x) = F_\lambda(x) + \pi_\lambda(x)G_\lambda(x)$, minimized at $x^*_\lambda$ (8). A surrogate $C[z;\hat F,\hat\pi,\hat G] = \hat F(z)+\hat\pi(z)\hat G(z)$ approximates it. Rounding is measured by

$$S_\lambda(x) = \min\{C(\lfloor N_\lambda(x)\rfloor,\lambda),\,C(\lceil N_\lambda(x)\rceil,\lambda)\}. \tag{10}$$

The Halfin–Whitt delay function is $P(x) = \big(1 + x/h(-x)\big)^{-1}$, with $h = \phi/(1-\Phi)$ the standard normal hazard rate (11). Asymptotic equality $a_\lambda \stackrel{\infty}{\approx} b_\lambda$ means $a_\lambda/b_\lambda \to 1$ as $\lambda\to\infty$.

Formalization targets

Goal: Theorem 5.1

Assume the rationalized condition (18): for some $\kappa > 0$, $F_\lambda(\kappa)/G_\lambda(\kappa) \to \gamma \in (0,\infty)$. Let $y^*_\lambda$ minimize $F_\lambda(y) + P(y)G_\lambda(y)$ over $y>0$ (19). Then

$$\lim_{\lambda\to\infty}\frac{S_\lambda(y^*_\lambda) - F(\lambda/\mu)}{C(N^*_\lambda,\lambda) - F(\lambda/\mu)} = 1.$$

The goal fixes no constant and no rate: it asserts only that the excess cost of the explicit rule is asymptotically the optimal excess cost.

Milestones

• Lemma C.1: $G_\lambda$ is strictly convex and strictly decreasing on $(0,\infty)$.
• Section 3, p. 12: $H(N,\nu) = \pi(N,\nu)$ at integers $N > \nu > 0$.
• Lemma 3.1, Lemma 3.2, Corollary 3.3: the approximation principle. If the surrogate approximates $C_\lambda$ at both $x^*_\lambda$ and its own minimizer $z^*_\lambda$, then rounding $N_\lambda(z^*_\lambda)$ is asymptotically optimal.
• Eqs. (13)–(14): $F_\lambda$ preserves $\limsup$-separation of ratios.
• Lemma 4.1 (Halfin & Whitt): for bounded $x_\lambda$, $\pi_\lambda(x_\lambda)/P(x_\lambda) \to 1$.

Significance

The theorem justifies the square-root staffing rule from first principles for a broad cost class. In Example 5.3 of the paper (linear staffing cost $c$ per agent, linear waiting cost $a$ per unit time) it gives $N^* \approx R + y^*(a/c)\sqrt R$, with $y^*(r)$ the minimizer of $y + rP(y)/y$, a one-dimensional rule computable once for all loads. Corollary 3.3 is reused verbatim by the efficiency-driven and quality-driven theorems of the paper (missions II and III of this series), and Lemma 4.1 is the analytic input of all three.

The result has been proved since 2000; no machine-checked proof of it, or of the Halfin–Whitt limit for the continuous extension $\pi_\lambda$, is known to exist. The mission produces a formal proof of the regime theorem together with reusable formal statements of the Erlang-C function, its integral representation, and the Halfin–Whitt limit.

Difficulty

The reduction from discrete to continuous staffing (Lemmas 3.1–3.2) is elementary once unimodality of $C_\lambda$ is available, but unimodality rests on convexity of $\pi_\lambda$, which the paper cites rather than proves, and on Lemma C.1, which needs differentiation under an improper integral. The central difficulty is Lemma 4.1: the paper derives it from Halfin and Whitt's limit theorem, which is stated for integer server counts, while $\pi_\lambda$ is evaluated at non-integer $N_\lambda(x_\lambda)$; a proof needs a uniform Laplace-type asymptotic for the integral defining $H$. A further obstacle is bounding $x^*_\lambda$: the obvious route through continuity of the optimizer fails because nothing converges, and the paper instead argues by contradiction via (14).

Formalization scope

All objects live in DimCallCenters.Rationalized. The arrival rate is a real lam, and every limit is Filter.atTop on $\mathbb R$ with $\mu$ fixed. The queue itself is not modelled; the paper's theorems are statements about the closed-form cost $C(N,\lambda)$, and so are these. Committed conventions:

1. The standing assumptions are a structure WaitModel ($\mu>0$; $D_\lambda(0)=0$; $D_\lambda$ strictly increasing on $[0,\infty)$; $t\mapsto D_\lambda(t)e^{-\theta t}$ integrable on $(0,\infty)$ for every $\theta>0$, which is the paper's finiteness of $G$). $F$ is convex and strictly increasing on $(0,\infty)$.
2. Staffing levels in $C(N,\lambda)$ are natural numbers; $G$ and $H$ take real $N$.
3. Argmins ($N^*_\lambda$, $x^*_\lambda$, $z^*_\lambda$, $y^*_\lambda$) are hypotheses that a given function is a minimizer, for every $\lambda>0$; ties are allowed and the theorems hold for every choice.
4. In $S_\lambda$ the floor term is omitted when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$, where $C$ is undefined.
5. $\limsup$ and $\liminf$ relations are written with ∃ᶠ/∀ᶠ, not Filter.limsup on $\mathbb R$.
6. Added hypothesis. The goal assumes $G(N,\lambda)\to\infty$ as $N\downarrow\lambda/\mu$. The paper asserts this limit on p. 12, but it does not follow from its assumptions (it fails for bounded $D_\lambda$); it is equivalent to $D_\lambda$ being unbounded and is what makes the continuous optimum exist.

The hypotheses are met by linear staffing and waiting costs ($F(N)=cN$, $D_\lambda(t)=at$), for which (18) holds with $\gamma = c\kappa^2/a$, so the goal is not vacuous. It is not trivialized by junk values either: the ratio's denominator is positive at every $\lambda>0$, and $S_\lambda$ never evaluates $C$ at an unstable level.

Needed infrastructure: Laplace asymptotics for $\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt$, differentiation under the integral sign for $G$, and convexity of $\pi_\lambda$. All of these are reusable for missions II–IV. Proofs of the milestones in any order are welcome, as are proofs of the convexity facts the paper cites from its references [9], [10].

Selected references

• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000; Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
• S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektroteknikeren 13, 1917.

Motivation

Open networks of single-server queues with general interarrival and service distributions are the standard model of job shops, communication networks and service systems. Outside the product-form (Jackson) case their queue-length distributions are not known in closed form. When every station is close to saturation, a heavy-traffic limit replaces the network by a diffusion process. Martin I. Reiman's paper Open Queueing Networks in Heavy Traffic (Mathematics of Operations Research 9(3), 1984) proves such a limit for the vector of queue lengths of a general open network. The limit is a reflected Brownian motion on the nonnegative orthant. That process has since become the default diffusion approximation for open networks, and it is the starting point of later work on its stationary distribution and on control of networks in heavy traffic.

Timeline:

• Iglehart and Whitt (1970a,b) proved heavy-traffic limits for a single multiple-server station and for acyclic networks, in which no customer visits a station twice.
• Harrison (1973, 1978) treated tandem queues; the 1978 paper introduced reflected Brownian motion on the nonnegative orthant as the diffusion limit.
• Harrison and Reiman (1981a, Ann. Probab. 9:302–308) constructed reflected Brownian motion on the orthant through a continuous reflection mapping. That paper is the source of Lemma 1 here.

(These attributions follow Reiman's own account, pp. 441–442 of the 1984 paper.)

• Reiman (1984) proved the limit for general open networks with Markovian routing (Theorem 1). The paper also proves a limit for sojourn times along fixed routes (Theorem 2).

Setting

There are $K$ single-server stations and a nonempty set $\mathcal J\subseteq\{1,\dots,K\}$ of stations that receive customers from outside. The primitives are mutually independent sequences of IID random variables: interarrival times $u_k^i>0$ ($k\in\mathcal J$), service times $v_k^i>0$, and routing indicators $\phi_k^i\in\{0,1,\dots,K\}$. When the $i$th customer served at station $k$ finishes, it moves to station $\phi_k^i$, or leaves if $\phi_k^i=0$. The parameters are the service rates $\mu_k=(E v_k^1)^{-1}$, the service-time variances $s_k=\operatorname{var} v_k^1$, the arrival rates $\lambda_k=(E u_k^1)^{-1}$ (with $\lambda_k=0$ for $k\notin\mathcal J$), and the interarrival variances $a_k=\operatorname{var} u_k^1$. The routing matrix $P=(p_{kj})$, $p_{kj}=P\{\phi_k^1=j\}$, has spectral radius strictly less than one, so every customer eventually leaves.

Let $A_k(t)$ be the number of exogenous arrivals to station $k$ by time $t$, and $S_k(t)$ the number of service completions at $k$ in $t$ units of busy time. Let $\hat S_k(t)=\sum_{i\le S_k(t)}e_{\phi_k^i}-S_k(t)e_k$, with $e_0=0$. The queue length $Q(t)\in\mathbb Z_+^K$ and the busy time $B(t)$ are the unique solution of

$$Q(t)=A(t)+\sum_{k=1}^K\hat S_k(B_k(t)),\qquad B_k(t)=\int_0^t1_{\{Q_k(s)>0\}}\,ds,\qquad B(0)=0 .$$

A sequence of such networks, indexed by $n$, shares $K$, $\mathcal J$ and $P$. Its parameters $\mu(n),s(n),\lambda(n),a(n)$ converge to finite limits $\mu,s,\lambda,a$. With $\nu(n)=\lambda(n)+\mu(n)P$, the heavy-traffic condition is

$$c_k(n)=\sqrt n\,(\nu_k(n)-\mu_k(n))\to c_k .$$

Moments of order $2+\epsilon$ of the interarrival and service times are bounded uniformly in $n$. The scaled queue length is $Z^n(t)=n^{-1/2}Q^n(nt)$, $0\le t\le1$.

Formalization targets

Goal: Theorem 1

Let $\xi$ be a Brownian motion with drift $c$ and covariance matrix $\mathcal A$, where

$$\mathcal A_{ii}=\lambda_i^3a_i+\mu_i^3s_i(1-2p_{ii})+\sum_j\mu_jp_{ji}(1-p_{ji}+p_{ji}\mu_j^2s_j),$$ $$\mathcal A_{ij}=-\Big[\mu_i^3s_ip_{ij}+\mu_j^3s_jp_{ji}+\sum_k\mu_kp_{ki}p_{kj}(1-\mu_k^2s_k)\Big]\quad(i\ne j).$$

Let $Z=\phi(\xi)$ be its reflection with reflection matrix $I-P$. Then

$$Z^n\Rightarrow Z\quad\text{in } D[0,1]\text{ (Skorohod topology)}.$$

The goal fixes no constants beyond the parameters' limits. It is stated for every network sequence satisfying (20)–(26).

Milestones

The milestones follow the paper's proof, in order:

• the existence and uniqueness claim for (1)–(3);
• the representation $Q=\tilde X+Y(I-P)$ (Eq. (13));
• the least-element map $f$ (Proposition 1);
• the reflection mapping $\phi$ (Lemma 1) and $f=\phi$ on continuous paths (Proposition 2);
• the netput limit $\zeta^n\Rightarrow\zeta$ (Proposition 3);
• stochastic boundedness of $Z^n$ (Lemma 6);
• vanishing scaled idleness $n^{-1}I^n_k(n)\to0$ (Proposition 4);
• the centred limit $\tilde\zeta^n\Rightarrow\zeta$ (Proposition 5).

Significance

Theorem 1 justifies the diffusion approximation of a heavily loaded open network. Writing $Q^n(t)\approx\sqrt n\,Z(t/n)$ reduces questions about the network to questions about one reflected Brownian motion, whose data are explicit functions of the first two moments of the primitives and of the routing matrix. The same limit, with Lemma 2, gives the paper's Theorem 2 on sojourn times. It is the model case for the multiclass heavy-traffic theory that followed.

The result has been proved since 1984. No machine-checked version exists. The mission's contributions would be:

• a formal statement of the network, of its Harrison representation, and of weak convergence in $D$;
• a formal proof of the reflection-mapping facts (Proposition 1, Lemma 1, Proposition 2), which are deterministic and reusable;
• eventually, a formal proof of the full limit theorem.

Difficulty

The obvious route applies a functional central limit theorem to $Q^n$ directly. That fails because $Q^n$ is not a sum of independent terms: each station serves only while its queue is nonempty, so the service process is evaluated at the random busy time $B_k(t)$, which depends on the whole network. The proof therefore has to separate the netput process, which obeys a central limit theorem, from the regulator $Y$. It then has to show that the random time change $B^n_k(nt)/n$ converges to the identity, i.e. that idleness vanishes on the diffusion scale. Weak convergence must also be transported through a reflection map that is defined on all of $D$ but is known to be continuous only at continuous paths.

Formalization scope

The Lean development uses the following conventions:

• Stations are Fin K, vectors are row vectors Fin K → ℝ, and a row vector times a matrix is Matrix.vecMul.
• A routing indicator lives in Fin (K+1), with 0 meaning "leaves" and j.succ meaning station $j$.
• The primitives are mutually independent (iIndep of their σ-algebras), IID within each sequence, everywhere positive and square integrable.
• "Spectral radius $<1$" is stated as $P^m\to0$.
• $(Q^n,B^n)$ is any pair solving (1)–(3) almost surely, with measurable paths so that (2) is a Lebesgue integral.
• The networks are indexed by ℕ; (25)–(26) are imposed for $n\ge1$, (22) and (26) over $k\in\mathcal J$, and $\mathcal J$ is the same for all $n$.
• Brownian motion with drift $c$ and covariance $\mathcal A$ lives on $[0,\infty)$. It is defined by continuity, $\xi(0)=0$, independent increments, and the Gaussian characteristic function of increments.
• $Z$ is the reflection of $\xi$ in the sense of (14)–(17).
• Weak convergence in $D$ is stated in Skorohod-representation form: a coupling with almost-sure J$_1$ convergence on $[0,1]$. This form accommodates a separate probability space for each $n$.

Added hypotheses, each implicit on the page:

1. The existence item assumes $U_k(l),V_k(l)\to\infty$ at the sample point; without it the maxima defining $A_k(t)$ and $S_k(t)$ need not exist.
2. Solutions of (1)–(3) have measurable paths.

No positivity hypothesis on the limits $\mu_k$ is added: (25) and (26) bound the means of the service and interarrival times, so the limits are positive.

The statement is not to be weakened. Ruled out are:

• convergence of finite-dimensional distributions only;
• a single network without the index $n$;
• uniform convergence used in place of the Skorohod topology without the coupling;
• a Brownian motion that is not required to have independent Gaussian increments.

Each of these is a different theorem.

Useful contributions, all reusable beyond this mission:

• the deterministic reflection-map results;
• Donsker-type theorems for renewal counting processes in $D$;
• the random time-change lemma (Billingsley);
• the continuous mapping theorem in coupling form.

Selected references

• M. I. Reiman, Open Queueing Networks in Heavy Traffic, Mathematics of Operations Research 9(3):441–458, 1984. https://doi.org/10.1287/moor.9.3.441
• J. M. Harrison and M. I. Reiman, Reflected Brownian Motion on an Orthant, Annals of Probability 9:302–308, 1981 (cited in Reiman 1984 as [6]).
• J. M. Harrison, The Diffusion Approximation for Tandem Queues in Heavy Traffic, Advances in Applied Probability 10:886–905, 1978 (Reiman 1984, [5]).
• J. M. Harrison, The Heavy Traffic Approximation for Single Server Queues in Series, Journal of Applied Probability 10:613–629, 1973 (Reiman 1984, [4]).
• D. L. Iglehart and W. Whitt, Multiple Channel Queues in Heavy Traffic, I and II: Sequences, Networks, and Batches, Advances in Applied Probability 2:150–177 and 355–364, 1970 (Reiman 1984, [8], [9]).
• P. Billingsley, Convergence of Probability Measures, Wiley, New York, 1968 (Reiman 1984, [1]).

Why staffing large call centers is a mathematical question

A call center must choose enough servers to limit waiting while paying for every server it staffs. When arrivals are heavy, small changes in the number of servers can change the probability of delay substantially. Borst, Mandelbaum, and Reiman study how to make this choice when the arrival rate grows and the costs of staffing and waiting need not grow at the same rate. Their CWI report treats several regimes within one queueing model. This mission concerns the efficiency-driven regime, where the incremental staffing cost eventually dominates the conditional waiting cost at every fixed positive square-root staffing offset. The resulting rule chooses an offset by optimizing a simpler cost that treats the probability of waiting as one.

The result is useful when the staffing-cost and waiting-cost primitives change with system scale. It says that the simplified choice still attains the optimal total cost asymptotically, even though the actual staffing decision is an integer and the simplified problem uses a real variable. The report states this as Theorem 6.1 on printed page 19, with its interpretation of asymptotic optimality supplied by Corollary 3.3 on printed page 14.

The Erlang-C cost model

Customers arrive at rate $\lambda>0$ and receive exponential service at rate $\mu>0$ per server. The service rate $\mu$ is fixed as $\lambda$ grows. For an integer number of servers $N>\lambda/\mu$, the Erlang-C delay probability $\pi(N,\lambda/\mu)$ is the explicit finite-sum expression in Section 2 of the report. A customer who waits has an exponential waiting time with rate $N\mu-\lambda$. Let $D_\lambda(t)$ be the cost of a wait of length $t$. It is strictly increasing on $t\ge0$, satisfies $D_\lambda(0)=0$, and has finite exponential expectation at every positive rate. The resulting conditional waiting cost is

$$G(N,\lambda)=(N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt.$$

The staffing cost $F(N)$ is one fixed, convex, strictly increasing function of the server count. Its continuous extension is evaluated at real $N>0$. Total cost per unit of time at a stable integer level is

$$C(N,\lambda)=F(N)+\lambda\pi(N,\lambda/\mu)G(N,\lambda).$$

Write $N^*_\lambda$ for any minimizing stable integer level. Ties are permitted. For a positive real offset $x$, define $N_\lambda(x)=\lambda/\mu+x\sqrt{\lambda/\mu}$, $F_\lambda(x)=F(N_\lambda(x))-F(\lambda/\mu)$, and $G_\lambda(x)=\lambda G(N_\lambda(x),\lambda)$. The report extends Erlang-C continuously to $\pi_\lambda(x)$ and writes the incremental continuous objective as $C_\lambda(x)=F_\lambda(x)+\pi_\lambda(x)G_\lambda(x)$. These definitions and the integer-extension identity are from Section 3, printed pages 11–12.

Formalization targets

The report defines the efficiency-driven regime by

$$\text{for every }\kappa>0,\qquad \lim_{\lambda\to\infty}\frac{F_\lambda(\kappa)}{G_\lambda(\kappa)}=+\infty.$$

For each $\lambda>0$, choose $y^*_\lambda>0$ to minimize $F_\lambda(y)+G_\lambda(y)$ over $y>0$. Let $S_\lambda(y)$ be the smaller cost of the stable integer levels immediately below and above $N_\lambda(y)$; if the lower one is unstable, use the upper one. The goal, Theorem 6.1 together with Corollary 3.3, is

$$\lim_{\lambda\to\infty} \frac{S_\lambda(y^*_\lambda)-F(\lambda/\mu)} {C(N^*_\lambda,\lambda)-F(\lambda/\mu)}=1.$$

The milestone path includes the convexity of the conditional waiting cost (Lemma C.1), the agreement of the continuous Erlang-C extension with its integer formula, the two approximation lemmas and their corollary (Lemmas 3.1–3.2 and Corollary 3.3), the convex staffing-cost comparison of equation (13), and all three clauses of the Halfin–Whitt limit in Lemma 4.1. This ordering follows the objects each later statement uses.

What the result gives

The theorem certifies a staffing rule defined by a one-variable surrogate rather than the exact Erlang-C probability in the objective. Its guarantee concerns the incremental total cost above the unavoidable baseline $F(\lambda/\mu)$, which is the economically relevant quantity when comparing two near-minimal stable staffing levels. The ratio tends to one, so the theorem is stronger than a claim that the two costs merely have the same growth order. The source also presents other regimes with different surrogates; their conclusions are separate targets in this series.

The paper proves the mathematical theorem. This mission asks for a Lean proof of its closed-form model and the surrounding lemmas. The complete development would make the report's approximation framework reusable for later results that combine a continuous queueing approximation, a surrogate minimizer, and integer rounding. It would also expose the exact assumptions needed to pass between real and integer staffing levels. No machine-checked proof of this report's Theorem 6.1 is claimed here.

Where the difficulty lies

The simple objective replaces the delay probability $\pi_\lambda(y)$ by one. That replacement is accurate near zero offset, but the minimizing offset itself changes with $\lambda$. Pointwise asymptotics at a fixed positive offset do not directly control the value of an objective at its moving minimizer. The proof therefore has to relate the regime assumption to the location of the relevant minimizers before using the Halfin–Whitt limit. Integer rounding introduces another boundary issue: when $N_\lambda(y)$ is just above $\lambda/\mu$, its floor need not be stable, so evaluating the ordinary Erlang-C formula there would compare the target against a meaningless cost. These difficulties are visible already in the statements of Theorem 6.1 and Lemma 3.2.

Formalization scope and conventions

Lean represents $\lambda$, $\mu$, offsets, and costs as real numbers; arrival-rate limits use the real filter at $+\infty$. Staffing counts are natural numbers. The service rate is positive and fixed. A WaitModel packages strict increase and normalization of $D_\lambda$ on nonnegative waits together with integrability against every positive exponential rate. This integrability expresses the report's finiteness assumption for $G$ and prevents a nonintegrable real integral from silently evaluating to zero. The hypotheses on $F$ are convexity and strict increase on positive real staffing levels; $F$ does not depend on $\lambda$.

The report asserts that $G(N,\lambda)$ diverges as $N$ decreases to $\lambda/\mu$, although the stated assumptions permit bounded increasing waiting penalties for which that assertion fails. The goal therefore includes this explicit divergence hypothesis, which also supports existence of the continuous minimizer used in the report's argument. The integer optimum and the surrogate optimum are functions constrained to be minimizers at every positive arrival rate. They cannot be arbitrary choices that make the conclusion vacuous. The continuous optimum appears only in the framework milestones; it is not a hypothesis of Theorem 6.1.

All formulas are total Lean functions. Their values at $\lambda\le0$, unstable integer counts, nonpositive offsets, or invalid parameters to the continuous Erlang-C integral have no queueing interpretation. Every theorem using them constrains its relevant inputs. The definition of $S_\lambda$ ignores an unstable floor and uses the stable ceiling. At a positive offset and arrival rate this ceiling is above offered load. The Gaussian density, its cumulative integral, the hazard rate, and the delay function use the explicit formulas of Section 4; the value of the delay function at zero is the continuous extension needed by Lemma 4.1.

The queue's stochastic construction is outside this mission. The formal objects are the report's cost formulas and asymptotic comparisons, not a continuous-time Markov chain. Useful contributions include proofs of the special-function limit, convexity of conditional waiting cost, the integer-extension identity, and the reusable approximation lemmas. The regime condition is the full limit in equation (23); weakening it to an unrelated boundedness condition would change the theorem.

Selected references

• Sem Borst, Avi Mandelbaum, and Martin I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000. Report PDF. Theorem 6.1, printed p. 19; Corollary 3.3, printed p. 14; Lemma 4.1, printed p. 15; Lemma C.1, printed p. 40.

Motivation

How many agents should a call center staff? Telephone call centers employ millions of people, and staffing is their largest cost, so the question is asked every half hour of every day (Gans, Koole & Mandelbaum, 2003). The classical model is the M/M/N (Erlang-C) queue: calls arrive at rate $\lambda$, service times are exponential with mean $1/\mu$, and $N$ agents serve in parallel. Practitioners use the square-root safety staffing rule $N \approx \lambda/\mu + y\sqrt{\lambda/\mu}$, which Halfin and Whitt (1981) justified in the regime where the probability of waiting stays bounded away from $0$ and $1$.

Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published as Operations Research 52(1), 2004) asked when such a rule is actually optimal: given a staffing cost and a waiting cost, which staffing level minimizes total cost as the arrival rate grows? They identified three regimes according to how the two costs compare. This mission formalizes their third case, the quality-driven regime, in which waiting is so expensive relative to staffing that the optimal number of agents exceeds the offered load by more than any fixed multiple of its square root.

Setting

Fix a service rate $\mu > 0$. For every arrival rate $\lambda > 0$ a waiting-cost function $D_\lambda$ assigns cost $D_\lambda(t)$ to a wait of $t$ time units; it satisfies $D_\lambda(0) = 0$, is strictly increasing, and $t \mapsto D_\lambda(t)e^{-\theta t}$ is integrable on $(0,\infty)$ for every $\theta > 0$. A staffing cost $F$, defined for real $N > 0$, is convex and strictly increasing.

For an integer $N > \lambda/\mu$ the probability of waiting is the Erlang-C formula

$$\pi(N,\nu) = \frac{\nu^N}{N!}\Bigl\{(1-\nu/N)\sum_{n=0}^{N-1}\frac{\nu^n}{n!} + \frac{\nu^N}{N!}\Bigr\}^{-1},\qquad \nu = \lambda/\mu,$$

the expected waiting cost of a delayed customer is $G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt$, and the total cost per unit time is $C(N,\lambda) = F(N) + \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda)$. An optimal staffing level $N^*_\lambda$ minimizes $C(\cdot,\lambda)$ over the integers $N > \lambda/\mu$.

Write $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$, and for $x > 0$ put $F_\lambda(x) = F(N_\lambda(x)) - F(\lambda/\mu)$, $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$, and $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$, where $H(M,\alpha) = \{\alpha\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt\}^{-1}$ extends the Erlang-C formula to real $M$. The normalized cost is $C_\lambda(x) = F_\lambda(x) + \pi_\lambda(x)G_\lambda(x)$, and a surrogate cost is $C[z;\hat F,\hat\pi,\hat G] = \hat F(z) + \hat\pi(z)\hat G(z)$. Rounding is measured by $S_\lambda(x) = \min\{C(\lfloor N_\lambda(x)\rfloor,\lambda), C(\lceil N_\lambda(x)\rceil,\lambda)\}$.

Two special functions appear. The Halfin–Whitt delay function is $P(x) = 1/(1 + x/h(-x))$ with $h = \phi/(1-\Phi)$ the standard normal hazard rate. The Stirling-type approximation is

$$Q_\lambda(x) = \frac{\exp\{N_\lambda(x)[1 - r_\lambda(x) + \log r_\lambda(x)]\}}{\sqrt{2\pi N_\lambda(x)}\,(1-r_\lambda(x))},\qquad r_\lambda(x) = \frac{\lambda/\mu}{N_\lambda(x)}.$$

Asymptotic relations are limits of ratios as $\lambda\to\infty$: $a_\lambda \stackrel{\infty}{\approx} b_\lambda$ means $a_\lambda/b_\lambda \to 1$, and $a_\lambda \stackrel{\infty}{\ll} b_\lambda$ means $a_\lambda/b_\lambda \to 0$.

Formalization targets

Goal: Theorem 7.1

Assume the regime is quality-driven, display (27): $F_\lambda(\kappa) \stackrel{\infty}{\ll} G_\lambda(\kappa)$ for every $\kappa > 0$. Let $y^*_\lambda$ minimize $F_\lambda(y) + Q_\lambda(y)G_\lambda(y)$ over $y > 0$. Then

$$\lim_{\lambda\to\infty}\frac{S_\lambda(y^*_\lambda) - F(\lambda/\mu)}{C(N^*_\lambda,\lambda) - F(\lambda/\mu)} = 1.$$

The statement fixes no constants and no rate; it asserts only that rounding the surrogate optimum loses a vanishing fraction of the excess cost.

Milestones

In attack order: Lemma C.1 ($G_\lambda$ strictly convex decreasing); the identity $H(N,\nu) = \pi(N,\nu)$ at integer $N$ (Section 3, p. 12); Lemma 3.1 and Lemma 3.2; Corollary 3.3 (the asymptotic optimality criterion); Lemma B.1 ($P$ strictly convex decreasing); display (15); Lemma 4.1 (Halfin and Whitt); and the first statement of Lemma 4.2, $\pi_\lambda(x_\lambda) \stackrel{\infty}{\approx} Q_\lambda(x_\lambda)$ whenever $x_\lambda\to\infty$.

Significance

Theorem 7.1 completes the paper's picture of optimal staffing. In the rationalized regime the square-root rule with the Halfin–Whitt function $P$ is optimal; in the efficiency-driven regime staffing barely exceeds the load; in the quality-driven regime the staffing excess outgrows $\sqrt{\lambda/\mu}$ and $P$ must be replaced by the Stirling-type expression $Q_\lambda$. The theorem gives a one-dimensional minimization whose solution is asymptotically optimal, which turns a discrete optimization over $N$ into a smooth problem, and it marks the boundary of validity of square-root staffing.

The result is proved in the paper; it is not formalized anywhere to our knowledge. A complete development formalizes the Section 3 framework (shared with the other regimes of the same paper), the convexity of $G_\lambda$ and of $P$, the Halfin–Whitt limit for the continuous extension $\pi_\lambda$, and the Stirling-type asymptotics of the Erlang-C formula. Each of these is a reusable piece of queueing theory in Lean.

Difficulty

The regime theorem itself is short once the framework is in place; the weight lies in the analytic lemmas. Lemma 4.2 requires uniform asymptotics of $\pi_\lambda$ at a staffing excess $x_\lambda$ that may grow at any rate, from barely faster than a constant to faster than $\sqrt{\lambda}$, where neither the central-limit picture of Halfin and Whitt nor a single Stirling expansion covers all cases. Lemma 4.1 concerns the continuous extension $\pi_\lambda$ at non-integer server counts, whereas Halfin and Whitt's theorem is about integer ones. The natural first idea, that the goal follows from Corollary 3.3 by plugging in Lemma 4.2, does not apply directly: Lemma 4.2 only covers staffing excesses that tend to infinity, and nothing in the definition of the true optimum $x^*_\lambda$ or the surrogate optimum $y^*_\lambda$ says that they do.

Formalization scope

Lean represents $\lambda$ as a positive real, and $\lambda\to\infty$ is the filter atTop on $\mathbb{R}$ with $\mu$ fixed. The standing assumptions on $\mu$ and $D_\lambda$ are the structure WaitModel; $F$ is a function argument with hypotheses ConvexOn and StrictMonoOn on $(0,\infty)$. Staffing levels $N$ are natural numbers. Minimizers ($N^*_\lambda$, $x^*_\lambda$, $z^*_\lambda$, $y^*_\lambda$) are function arguments with minimality hypotheses at every $\lambda > 0$, so every statement holds for every choice among ties. Liminf and limsup relations are stated through Filter.Frequently, avoiding boundedness side conditions.

The queue itself (Poisson arrivals, waiting-time law) is not formalized: the paper's analysis and all its theorems concern the closed-form cost $C(N,\lambda)$ with the Erlang-C formula.

Conventions committed to: (i) the goal adds the hypothesis $G(N,\lambda)\to\infty$ as $N\downarrow\lambda/\mu$, which the paper asserts on p. 12 to show the continuous optimum exists but which does not follow from its standing assumptions (it holds exactly when $D_\lambda$ is unbounded); (ii) in $S_\lambda$ the floor term is omitted when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$, since the cost is undefined at unstable levels; (iii) the integrability of $D_\lambda(t)e^{-\theta t}$ is explicit, because a Lean integral of a non-integrable function is $0$; (iv) $P(0) = 1$, the value of formula (11) at $0$; (v) display (15) is stated for $b > 0$, since the ratio $a_\lambda/b$ is undefined at $b = 0$. The instance $\mu = 1$, $F(N) = cN$, $D_\lambda(t) = a\sqrt{\lambda}\,t$ (Section 9) satisfies every hypothesis of the goal, so the goal is not vacuous; taking $\pi_\lambda$ or $G_\lambda$ at Lean default values is ruled out by these explicit domain conditions.

Only the first statement of Lemma 4.2 is a milestone: the second, $\pi_\lambda(x_\lambda)\approx Q(x_\lambda)$ under $x_\lambda \stackrel{\sup}{\le} \lambda^{1/6}$, fails as printed at $x_\lambda = \lambda^{1/6}$. Contributions on the Erlang-C asymptotics, the normal hazard rate, and Laplace transforms of increasing functions are welcome and reusable beyond this mission.

Selected references

• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000 (the version formalized here; every index and page cited in this mission is the report's).
• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
• S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• N. Gans, G. Koole, A. Mandelbaum, Telephone Call Centers: Tutorial, Review, and Research Prospects, Manufacturing & Service Operations Management 5(2):79–141, 2003. https://doi.org/10.1287/msom.5.2.79.16071