Queueing and Stochastic Networks

Motivation

The neutral theory of molecular evolution holds that much of the genetic variation observed at the molecular level is caused by selectively neutral mutations rather than by selection. To test it against data one needs the distribution of allele frequencies that a neutral model predicts, and in practice that distribution has to be compared with a sample from the population, never with the whole population. Ewens (Ewens 1972) derived the equilibrium distribution of allele counts under the infinite alleles model, now called the Ewens sampling formula; it underlies classical tests of neutrality and appears throughout combinatorics and probability as the law of the cycle type of an Ewens-distributed random permutation and of the Chinese restaurant process.

Chapter 7 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) obtains the infinite alleles model as a limit of the reversible migration processes of Chapters 2 and 6, and uses reversibility to answer questions about allele ages and fixation. The mission formalizes the finite, combinatorial results of that chapter.

Timeline. Kimura and Crow (1964) introduced the infinite alleles model. Ewens (1972) found its equilibrium sampling distribution (7.6). Kingman (1978, J. London Math. Soc.) characterized the consistency of random partitions under sampling, the property Theorem 7.1 asserts for the Ewens family. Kelly (1979, Chapter 7) derived (7.6) as a limit of reversible migration processes, and the consistency and the allele-age results from the reversibility of a labelled population process.

Setting

A population consists of $M\ge2$ individuals, each carrying an allelic type. Its description is $\mathbf M=(M_1,\dots,M_M)$, where $M_i$ is the number of allelic types carried by exactly $i$ individuals, so that

$$\sum_{i=1}^{M} iM_i=M. \qquad (7.3)$$

For a real parameter $\nu>0$, the Ewens distribution on descriptions is

$$\pi_M(\mathbf M)=\binom{\nu+M-1}{M}^{-1}\prod_{i=1}^{M}\Big(\frac{\nu}{i}\Big)^{M_i}\frac{1}{M_i!}, \qquad (7.6)$$

where $\binom{x}{k}=x(x-1)\cdots(x-k+1)/k!$ is the binomial coefficient for real $x$. In the infinite alleles model, individuals die at rate $\mu$, each death is followed by the birth of an offspring of a uniformly chosen survivor, and the offspring is a mutant of an entirely new type with probability $u$; then (7.6) is the equilibrium distribution with $\nu=(M-1)u/(1-u)$ (7.5).

A random sample of size $1\le m\le M$ without replacement is a uniformly random $m$-element subset of the $M$ labelled individuals, each of the $\binom Mm$ subsets being equally likely; the sample has a description in the same sense.

The number $j$ of individuals carrying one given allele performs a random walk on $\{0,\dots,M\}$ with intensities

$$q(j,j-1)=\mu\frac jM\Big(\frac{M-j}{M-1}+\frac{j-1}{M-1}u\Big),\qquad q(j,j+1)=\mu\frac{M-j}{M}\frac{j}{M-1}(1-u). \qquad (7.8)$$

An allele is quasi-fixed when it is the only allele present ($j=M$).

Formalization targets

Goal: consistency under sampling (Theorem 7.1)

If $M\ge2$ and the population description is distributed as $\pi_M$, then a random sample of size $1\le m\le M$ drawn without replacement has description $\mathbf m$ with probability $\pi_m(\mathbf m)$, the same $\nu$ being used for both sizes:

$$\sum_{\mathbf M}\pi_M(\mathbf M)\,P\big(\text{sample has description }\mathbf m\mid\text{population has description }\mathbf M\big)=\pi_m(\mathbf m).$$

Milestones

1. (7.6) is a distribution: $\pi_M(\mathbf M)>0$ and $\sum_{\mathbf M}\pi_M(\mathbf M)=1$ (Exercise 7.1.3).
2. Theorem 7.1 for $m=M-1$, the case the book's proof establishes first.
3. Corollary 7.5, the identity of its proof: the probability that a uniformly chosen individual's allele is carried by exactly $i$ individuals is

$$\sum_{\mathbf M}\frac{iM_i}{M}\pi_M(\mathbf M)=\frac{\nu}{M}\binom{\nu+M-1}{i}^{-1}\binom Mi. \qquad (7.9)$$

4. Theorem 7.9: the probability $Q$ that the walk (7.8) started at $1$ reaches $M$ before $0$ satisfies

$$Q^{-1}=\sum_{i=0}^{M-1}\binom{M-1}{i}^{-1}\binom{\nu+M-1}{i}.$$

Significance

The results. Consistency under sampling is what makes the Ewens formula usable as a statistical model: the predicted distribution for an observed sample does not depend on the unknown population size, only on $\nu$. Kelly deduces from it the sufficiency of the number of alleles in a sample for $\nu$ and the heterozygosity $\nu/(\nu+1)$ (Exercises 7.1.5, 7.1.8). The formula (7.9) gives the equilibrium frequency of the oldest allele, and Theorem 7.9 gives the quasi-fixation probability from which the mean time between quasi-fixations follows (Corollary 7.10).

Formalizing them. All four results are classical and proved; none has a machine-checked proof on the platform or in Mathlib as of this writing. The mission produces a reusable formal Ewens distribution over integer partitions, a definition of sampling without replacement by counting labelled subsets, and an absorption probability for an explicit birth–death walk. Proofs independent of Kelly's process argument are welcome.

Difficulty

The book's proof of Theorem 7.1 is a process argument: in a population whose size fluctuates between $M-1$ and $M$, a drop in size acts as a random deletion, and the truncated equilibrium (7.7) restricted to each size gives $\pi_{M-1}$ and $\pi_M$. Turning that into a statement about finite sets requires the equilibrium of a truncated reversible process, which is not available here, so a formal proof must either build that process or find a direct combinatorial route. A direct route has to relate, for each description of the sample, the number of $m$-subsets of a labelled population with a given description to products of binomial coefficients, and sum the result against (7.6); the bookkeeping over partitions is where the work lies. Theorem 7.9 needs a solution of the first-step equations of a non-symmetric walk and the identification of that solution with a hitting probability defined as a limit.

Formalization scope

• Descriptions of $n$ individuals are integer partitions Nat.Partition n, with $M_i$ the multiplicity of the part $i$; the product in (7.6) runs over $i=1,\dots,n$. The real binomial coefficient is the published definition AppliedComb.GenFun.binomReal.
• The population is Fin M with allelic types Fin M → ℕ; the description of a labelled set is computed from the labelling. The sampling probability is $\binom Mm^{-1}$ times the number of $m$-subsets whose restricted labelling has the given description. It is not defined by a formula on descriptions, and a definition that removed individuals one at a time in proportion to class sizes (the book's proof route) is ruled out as a definition because it presupposes the reduction the proof must supply.
• The goal and Corollary 7.5 quantify over an arbitrary choice of labelling for each population description. They assume $M\ge2$, as required by the chapter's rule that a parent is chosen among the other $M-1$ individuals; the goal also assumes $1\le m\le M$. Because $\pi_M>0$, this forces the conditional sampling law to depend on the population only through its description. Types are natural numbers, so every description is realized and the hypothesis is never vacuous.
• The quasi-fixation probability is defined through the jump chain of (7.8): the limit of the probabilities of reaching $M$ within $n$ jumps without reaching $0$. The theorem assumes $M\ge2$, $\mu>0$, $0<u<1$ and $\nu=(M-1)u/(1-u)$.
• Corollary 7.5 is formalized as the identity of its proof. The identification of the oldest allele's frequency with that of a randomly chosen individual uses allele ages and the reversibility of the labelled process (Theorem 7.2) and is not formalized. Theorem 7.2 itself, whose state space orders the allele labels within each class, and the allele-age results (Corollaries 7.3, 7.4, 7.7, 7.8, Theorem 7.6, Corollary 7.10, Theorem 7.11) are not part of the mission.

Contributions of general partition and sampling lemmas (counting subsets with a given description, the generating function identity $(1-x)^{-\nu}=\prod_j e^{\nu x^j/j}$) are reusable beyond this mission.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979, Chapter 7. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• W. J. Ewens, The sampling theory of selectively neutral alleles, Theoretical Population Biology 3 (1972), 87–112. https://doi.org/10.1016/0040-5809(72)90035-4
• J. F. C. Kingman, The representation of partition structures, Journal of the London Mathematical Society (2) 18 (1978), 374–380. https://doi.org/10.1112/jlms/s2-18.2.374
• M. Kimura and J. F. Crow, The number of alleles that can be maintained in a finite population, Genetics 49 (1964), 725–738. https://doi.org/10.1093/genetics/49.4.725

Why partial balance

Equilibrium distributions of Markov models of networks are rarely computed by solving the full equilibrium equations directly. In the classical product-form results (migration processes, Jackson and Kelly networks, loss networks, clustering processes) the equilibrium distribution satisfies a stronger, local family of equations, and that is what makes it computable. The strongest such family is detailed balance, which characterizes reversibility. Many models that are not reversible still satisfy an intermediate family, partial balance: the probability flux balances not pair by pair but across a chosen set of transitions. F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) uses partial balance throughout: quasi-reversibility in Chapter 3 is a form of it, and the models that display it tend to be insensitive, meaning their equilibrium distribution does not change when exponential holding times are replaced by general ones with the same mean.

Section 9.4 of the book collects what partial balance means in a single statement. Theorem 9.5 summarizes Exercises 1.6.2–1.6.4 and 1.7.7–1.7.8 and gives five operational characterizations of partial balance. Corollaries 9.6–9.8 translate them into the language of spatial processes, and Theorem 9.9 turns partial balance of a coarse description into a product-form equilibrium for a finer one. This last step is the mechanism behind insensitivity.

Setting

A Markov process on a state space $\mathcal S$ has transition rates $q(j,k)\ge0$ for $j\ne k$, with $q(j,j)=0$. It is irreducible: every state can be reached from every other through transitions of positive rate. An equilibrium distribution is a collection of positive numbers $\pi(j)$ summing to one that satisfies the equilibrium equations

$$\pi(j)\sum_{k\in\mathcal S}q(j,k)=\sum_{k\in\mathcal S}\pi(k)q(k,j),\qquad j\in\mathcal S.$$

For an irreducible process on a finite state space it exists and is unique.

Given a set $\mathcal A\subseteq\mathcal S$, $\pi$ satisfies partial balance with respect to $\mathcal A$ if

$$\pi(j)\sum_{k\in\mathcal A}q(j,k)=\sum_{k\in\mathcal A}\pi(k)q(k,j),\qquad j\in\mathcal A.$$

Truncating the process to $\mathcal A$ deletes every transition out of $\mathcal A$, and the result is required to be irreducible within $\mathcal A$. The time-reversed process of a process with equilibrium distribution $\pi$ has rates $\pi(k)q(k,j)/\pi(j)$.

A spatial process has $J$ sites, the vertices of a graph $G$. Site $j$ carries an attribute $n_j$ from a finite set $\mathcal N_j$, and the state space is $\mathcal S=\mathcal N_1\times\cdots\times\mathcal N_J$. Write $T_j^m\mathbf n$ for the state $\mathbf n$ with the attribute of site $j$ changed to $m$. The process must satisfy three conditions: only one site changes at a time; the rate $q(\mathbf n,T_j^m\mathbf n)$ depends on the other sites only through the neighbours of $j$; and any $T_j^m\mathbf n$ can be reached from $\mathbf n$ without changing the other sites. The conditional distribution of site $j$ given the rest is $P(n_j\mid\mathbf n_{G-j})=\pi(\mathbf n)/\sum_m\pi(T_j^m\mathbf n)$. A Markov field is a positive distribution whose conditional distributions depend only on the neighbours of $j$.

Formalization targets

Goal: Theorem 9.5

For an irreducible process on a finite $\mathcal S$ with equilibrium distribution $\pi$, a nonempty $\mathcal A$ within which the truncated process is irreducible, and a constant $c>0$, $c\ne1$, the following are equivalent:

1. partial balance with respect to $\mathcal A$;
2. the equilibrium distribution of the truncated process is $\pi(j)/\sum_{k\in\mathcal A}\pi(k)$;
3. multiplying the rates $q(j,k)$, $j,k\in\mathcal A$, by $c$ leaves the equilibrium distribution unchanged;
4. multiplying the rates $q(j,k)$, $j\in\mathcal A$, $k\notin\mathcal A$, by $c$ changes the equilibrium distribution to

$$B\pi(j)\ (j\in\mathcal A),\qquad Bc\pi(j)\ (j\notin\mathcal A),\qquad B^{-1}=\sum_{j\in\mathcal A}\pi(j)+c\sum_{j\notin\mathcal A}\pi(j);$$

5. time reversal and truncation to $\mathcal A$ commute.

When $\mathcal S-\mathcal A$ is nonempty, these are also equivalent to:

6. the chain observed just before each exit from $\mathcal A$ and the chain observed just after each entry into $\mathcal A$ have the same equilibrium distribution.

Milestones

• Corollary 9.6: the equivalences for the sets on which all sites but $j$ are frozen, i.e. partial balance (9.26) at a site.
• Corollary 9.7: on a state space with at least two states, partial balance at every site makes $\pi$ a Markov field, with $0<\pi(\mathbf n)<1$ as in the book's definition.
• Corollary 9.8: the equivalences for the set on which site $j$ is frozen at one attribute (9.27).
• Theorem 9.9: if a reduced description $\mathbf n=f(\mathbf x)$ has a distribution $\pi(\mathbf n)$ in partial balance for the rates (9.31), then the finer process has equilibrium distribution $\pi(\mathbf x)=\pi(\mathbf n)\prod_jP_j(x_j\mid n_j)$.

What the results give

Theorem 9.5 makes partial balance testable by operations on the process itself: truncation, speeding up or slowing down transitions, and time reversal. The book points to close relationships between statement (iv) and the product form of Section 2.3, and between statement (ii) and part (iii) of Theorem 3.12. Corollary 9.6 (iv) explains why the reversed migration process has such a simple form. Corollary 9.7 strengthens Theorem 9.3 by replacing reversibility with partial balance at each site. Theorem 9.9 is the step from partial balance to insensitivity: it is what the book uses to show that a spatial process keeps its equilibrium distribution when the lifetimes of attributes are mixtures of gamma distributions.

All of these results were proved in 1979. None has a machine-checked proof. The platform has the reversible special case of statement (ii) (KellyStochasticNetworks.truncated_reversible) and the rate-level objects for time reversal and truncation, which this mission reuses. Formalizing Theorem 9.5 also produces a reusable account of embedded exit and entry chains of a finite Markov process.

Difficulty

Most of the equivalences (i)–(v) are short manipulations of the equilibrium equations, but each direction from a property of an altered process back to partial balance needs uniqueness of equilibrium distributions for irreducible finite processes, and (v) ⇒ (i) also needs their existence. Mathlib has neither in the form needed here. Statement (vi) is a different kind of claim. The equilibrium distribution of the exit chain is proportional to the exit flux $\pi(j)\sum_{k\notin\mathcal A}q(j,k)$, and that of the entry chain to the entry flux. Proving this requires the hitting distributions and the Green's function of the jump chain killed on leaving a set, and the convergence of the series that define them. Corollary 9.8 (v) inherits that work. Theorem 9.9 requires uniqueness for the reduced frozen processes and careful bookkeeping of the fibres $\{x_j:f_j(x_j)=n_j\}$.

Formalization scope

State spaces are finite types, and every sum is an unconditional sum over a finite type. Because the state space is finite, the book's extra condition for (vi), a finite flux out of $\mathcal A$, holds automatically. Rates are real functions with $q(j,j)=0$ built into the hypotheses; the reduced rates of (9.31) also have zero self-rates. "The equilibrium distribution of a process is $X$" means: $X$ is positive, sums to one, satisfies the equilibrium equations, and every distribution with these properties equals $X$. The book's "$c\ne0$ or $1$" is read as $c>0$, $c\ne1$, so that altered rates remain rates. Truncation to $\mathcal A$ is the published truncatedRates, a process on the subtype $\mathcal A$, and the reversed rates are the published reversedRates. The exit and entry chains are defined from the jump chain through series of restricted matrix powers. Spatial processes live on $\prod_j\mathcal N_j$ with $T_j^m$ given by Function.update. In Theorem 9.9 the graph is complete, as the book assumes from p. 202 on.

The equilibrium distribution of the truncated process must be the unique positive normalized solution of the truncated equilibrium equations. It must not be defined as the conditional distribution, which would make (ii) a tautology. For the same reason (iii) and (iv) are stated through the equilibrium equations of the altered rates, not by assumption.

Theorem 9.10 (p. 207) is not a target. Its hypothesis, that a nominal lifetime "can have any distribution with unit mean", is not defined on the page, and the point-process and lifetime description it needs lies outside this rate-level development.

Contributions are welcome at every level: uniqueness and existence of equilibrium distributions for irreducible finite rate matrices (reusable across the series), convergence of the killed Green's function, and proofs of the corollaries from the goal.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, Chichester, 1979; reissued Cambridge University Press, 2011. https://doi.org/10.1017/CBO9781139171724 (§9.4, pp. 200–208; §1.6, pp. 25–27)
• F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781139565363

Motivation

Large call centers route several types of customers to a common pool of agents. When the pool is large and highly utilized, the relevant asymptotic regime is the quality-and-efficiency-driven (QED) or Halfin–Whitt regime (Halfin & Whitt 1981). The number of servers $n$ grows while the offered load stays within $O(\sqrt n)$ of $n$. Waiting is then neither negligible nor overwhelming (Gans, Koole & Mandelbaum 2003).

Which class should a freed agent serve next? Exact optimization of a multi-class many-server queue with abandonment is intractable. The standard route is to solve a limiting diffusion control problem and translate its optimal control back into a policy for the queue. Atar, Mandelbaum and Reiman (Ann. Appl. Probab. 2004) carried this out for $k$ customer classes, exponential service and abandonment, general renewal arrivals and general convex-type holding costs. They proved that the translated policy is asymptotically optimal. This mission formalizes that result for the preemptive policy.

Context:

• Harrison & Zeevi (2004) studied the same multi-class many-server problem.
• Bell & Williams (2001) proved asymptotic optimality of a threshold policy for a two-server system in conventional heavy traffic.
• The present paper is the first to cover the QED regime with general costs and abandonment.

Setting

There are $k\ge1$ customer classes and $n$ identical servers.

Primitives.

• Arrivals. Class-$i$ customers arrive according to a renewal process $A^n_i$ with interarrival times $\check U_i(j)/\lambda^n_i$. Here the $\check U_i(j)$ are i.i.d., positive, of mean one and squared coefficient of variation $C^2_{U,i}$.
• Service. Service times are exponential with rate $\mu^n_i$, represented by Poisson processes $S^n_i$.
• Abandonment. Waiting customers abandon at rate $\theta^n_i\ge0$, represented by Poisson processes $R^n_i$.

State. $X^n_i(t)$ is the number of class-$i$ customers in the system, $\Psi^n_i(t)$ the number in service and $\Phi^n_i=X^n_i-\Psi^n_i$ the number waiting. The dynamics are

$$X^n_i(t)=X^{0,n}_i+A^n_i(t)-R^n_i\Big(\int_0^t\Phi^n_i\Big)-S^n_i\Big(\int_0^t\Psi^n_i\Big),\qquad \Psi^n,\Phi^n\in\mathbb Z^k_+,\quad \textstyle\sum_i\Psi^n_i\le n .$$

Policies.

• A scheduling control policy (SCP) is the process $\Psi^n$.
• It is admissible if it does not anticipate the future beyond the time of the next arrival: past information is independent of future primitive increments.
• It is work-conserving if no server idles while customers wait: $(\mathbb 1\cdot X^n-n)^+=\mathbb 1\cdot\Phi^n$.

Scaling and cost. In the QED scaling $n^{-1}\lambda^n_i\to\lambda_i$ with $\sum_i\lambda_i/\mu_i=1$. With $\rho_i=\lambda_i/\mu_i$ the centred processes are $\hat X^n=n^{-1/2}(X^n-\rho n)$, $\hat\Phi^n=n^{-1/2}\Phi^n$ and $\hat\Psi^n=n^{-1/2}(\Psi^n-\rho n)$. The cost is

$$C^n=E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^n(t),\hat\Psi^n(t))\,dt .$$

The limiting control problem. It controls

$$X(t)=x+rW(t)+\int_0^t b(X(s),u(s))\,ds,\qquad b(x,u)=\ell+(\mu-\theta)(\mathbb 1\cdot x)^+u-\mu x,$$

where the control $u$ takes values in the simplex $\mathbb S^k$ and $W$ is a $k$-dimensional Brownian motion. The data are $r_i=(\lambda_iC^2_{U,i}+\lambda_i)^{1/2}$ and $\ell_i=\hat\lambda_i-\rho_i\hat\mu_i$. Its value $V(x)$ is the infimum of $E\int_0^\infty e^{-\gamma t}L(X,u)\,dt$, with $L(x,u)=\tilde L((\mathbb 1\cdot x)^+u,x-(\mathbb 1\cdot x)^+u)$.

HJB equation and the proposed policy. The HJB equation is $\tfrac12\sum_ir_i^2\partial_{ii}f+H(x,Df)-\gamma f=0$ with $H(x,p)=\inf_{u\in\mathbb S^k}[b(x,u)\cdot p+L(x,u)]$. Let $h$ be a measurable selection of its minimizers. The proposed preemptive policy (P-SCP) sets the queue vector to $\Theta[(\mathbb 1\cdot X^n-n)^+h(\hat X^n)]$, an integer rounding, and falls back to a static priority rule when that is infeasible.

Formalization targets

Goal: Theorem 2(i)

For a $C^2_{\mathrm{pol}}$ solution $f$ of the HJB equation, a measurable minimizer selection $h$, and initial states with $\hat X^{0,n}\to x$:

$$\lim_{n\to\infty}E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^{n,*}_t,\hat\Psi^{n,*}_t)\,dt\;\le\;\liminf_{n\to\infty}E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^n_t,\hat\Psi^n_t)\,dt$$

This holds for every sequence of work-conserving admissible SCPs, and the left-hand limit exists and is finite. No constants are hard-coded.

Milestones

The milestones follow the proof:

• on the diffusion side, Proposition 2 (well-posedness), Proposition 4 (stability and moment bounds), Proposition 5(i)–(ii) (growth and continuity of $V$) and Theorem 3 ($V$ is the unique $C^2_{\mathrm{pol}}$ HJB solution, and an optimal Markov policy exists);
• on the queueing side, Proposition 1 (feedback rules give admissible SCPs), Lemmas 2–3 (moment bounds), Lemma 4(i)–(ii) (FCLT for the primitives and the fluid limit $(\bar\Psi^n,\bar\Phi^n)\Rightarrow(\rho,0)$), and Theorem 4(i)–(ii): $\liminf\ge V(x)$ always, and $\limsup\le V(x)$ under condition (49).

Significance

The result. Theorem 2(i) justifies using the diffusion control problem as a design tool for multi-class many-server systems. The policy is explicit given $h$, and it is optimal in the limit against all non-anticipating work-conserving policies, including those that use the full history and the time of the next arrival. The proof also identifies the limit cost with $V(x)$.

Formalizing it. The result is proved on paper, with some steps (Proposition 1, the principle of optimality, the time-change and martingale limit theorems) given as sketches or citations. No part of it is machine-checked. A formalization requires:

• a counting-process model of the queue;
• a careful definition of non-anticipation;
• a pathwise controlled SDE;
• classical solvability of a semilinear elliptic HJB equation on $\mathbb R^k$;
• a weak-convergence argument in Skorokhod space.

Each of these is reusable well beyond this paper.

Difficulty

The obvious argument would show that $\hat X^n$ converges to the controlled diffusion and pass the costs to the limit. This fails for two reasons:

• the comparison class contains arbitrary non-Markov, history-dependent policies, so the queue does not converge to a single controlled diffusion;
• the optimal selector $h$ is in general discontinuous (for linear costs it is), so the proposed policy is not a continuous function of the state.

The proof instead compares every policy with the HJB solution through Itô's formula on the prelimit processes. This needs:

• uniform moment bounds;
• tightness of the integral processes;
• the convergence of stochastic integrals of Kurtz and Protter;
• and, for the proposed policy, the fact that the rounding $\Theta$ and the priority fallback perturb the minimizer by $O(n^{-1/2})$.

Existence of a classical HJB solution on all of $\mathbb R^k$, with only Hölder-continuous costs and polynomial growth, rests on a bounded-domain existence theorem for fully nonlinear elliptic equations.

Formalization scope

The Lean development commits to the following conventions.

• Indexing and norms. Classes are Fin k with $k\ge1$; paper class $i$ is index $i-1$, so "class $k$" (highest priority, rounding remainder of $\Theta$) is the last index. Vectors are Fin k → ℝ and $\|\cdot\|$ is the paper's $\ell^1$ norm; the paper's $|\cdot|$ on vectors is read the same way.
• Probability space and paths. All systems share one complete probability space. Time is real and every condition is for $t\ge0$. The paper's "without loss" path regularity (finite arrival counts, Poisson paths $\mathbb Z_+$-valued, nondecreasing and càdlàg) holds for every $\omega$.
• Poisson processes are defined by independent Poisson increments; rate $0$ gives the zero process.
• Policies. A policy is a pair of real processes $(\Psi^n,X^n)$ with integer values. Admissibility is Definition 2 verbatim, with the future $\sigma$-field built from the next arrival time $\tau^n_i(t)$. Work conservation is (18).
• Costs and value are lower Lebesgue integrals in $[0,\infty]$, and $\lim$/$\liminf$ are taken there. The integrands are nonnegative under work conservation.
• Admissible systems range over sample spaces Ω : Type (universe 0). "Complete filtered probability space" means $P$ complete with all null sets in $\mathcal F_0$. Brownian motion is Mathlib's IsBrownianReal per coordinate, with independence and the $(\mathcal F_t)$-Brownian property stated explicitly. $V$ is the infimum over systems and their controlled processes.
• Discount rate. $\gamma>0$ is a hypothesis; the paper leaves it implicit.
• Initial states are integer vectors $X^{0,n}\in\mathbb Z^k_+$ with $n^{-1/2}(X^{0,n}-\rho n)\to x$. The literal "$\hat X^{0,n}\in n^{-1/2}\mathbb Z^k$" would require $\rho_in\in\mathbb Z$. Assumption 1(ii) is not imposed: each policy chooses its own initial split.
• Lemma 3 is stated for all $n$ beyond a threshold that depends on the sequence, with constants $c,\bar m$ chosen before $x$ and the sequence. The printed all-$n$ bound with $c$ independent of $x$ fails when the early terms $\hat X^{0,n}$ are large.
• Weak convergence to a continuous limit uses the coupling form CouplingConverges of the published BellWilliams2001.ThresholdPolicy.Paths; convergence to a deterministic limit is UocInProb.

The goal hypothesizes $f$ and $h$ with the pointwise identity $b(x,h(x))\cdot Df(x)+L(x,h(x))=H(x,Df(x))$ for all $x$. An arbitrary "optimal Markov control policy" may differ from a minimizer selection on the Lebesgue-null lattice where $\hat X^n$ lives, and that formalization would make the goal false. Restricting the comparators to feedback, Markov or nonpreemptive policies, fixing $k$, dropping abandonment, specializing to Poisson arrivals or linear costs, or imposing a common initial split would each trivialize or weaken the statement and is ruled out.

Not formalized:

• Lemma 4(iii) (tightness);
• Lemma 5 (Kurtz–Protter, which needs semimartingale theory absent from Mathlib);
• Lemma 6 (convergence of Stieltjes integrals at limit points);
• Proposition 5(iii);
• the nonpreemptive results, Theorem 2(ii)–(iii).

Contributions are welcome on any milestone, and especially on infrastructure: Poisson and renewal processes, functional central limit theorems in Skorokhod space, classical solvability of elliptic HJB equations, and measurable selection of minimizers.

Selected references

• R. Atar, A. Mandelbaum, M. I. Reiman, Scheduling a multi class queue with many exponential servers: asymptotic optimality in heavy traffic, Ann. Appl. Probab. 14(3), 2004. https://arxiv.org/abs/math/0407058
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Oper. Res. 29(3), 1981. https://doi.org/10.1287/opre.29.3.567
• N. Gans, G. Koole, A. Mandelbaum, Telephone call centers: tutorial, review, and research prospects, Manuf. Serv. Oper. Manag. 5(2), 2003. https://doi.org/10.1287/msom.5.2.79.16071
• J. M. Harrison, A. Zeevi, Dynamic scheduling of a multiclass queue in the Halfin–Whitt heavy traffic regime, Oper. Res. 52(2), 2004. https://doi.org/10.1287/opre.1040.0109
• S. L. Bell, R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Ann. Appl. Probab. 11(3), 2001. https://doi.org/10.1214/aoap/1015345343
• T. G. Kurtz, P. Protter, Weak limit theorems for stochastic integrals and stochastic differential equations, Ann. Probab. 19(3), 1991. https://doi.org/10.1214/aop/1176990334

Why reentrant lines, and why this one

A reentrant line is a queueing network in which every job follows the same route and visits some stations more than once. It is the standard model of a semiconductor wafer fab, where a wafer returns to the same lithography station for each of its layers (Kumar, Re-entrant lines, Queueing Systems 13, 1993). Because jobs at different stages compete for the same server, a network can be unstable (queues grow without bound) even though every station has nominal load below one; the Lu–Kumar and Rybko–Stolyar examples of the early 1990s made this concrete. Deciding stability under the usual load condition therefore needs an argument specific to the network and to the scheduling policy.

Fluid models turn that question into one about deterministic dynamics. Dai (Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Ann. Appl. Probab. 5, 1995) showed that if the fluid model of a queueing discipline is stable, the queueing network under that discipline is positive Harris recurrent. Dai and Weiss (1996) then proved fluid stability, or instability, for several classes of reentrant lines. This mission formalizes their first result, about the smallest reentrant line that revisits a station after visiting another one.

Timeline:

• 1993: Kumar conjectured that the three-buffer line $1 \to 2 \to 1$ is stable under the first-in-first-out (FIFO) discipline whenever the load condition holds, for exponential distributions.
• 1993: Wang proved that the FIFO fluid model of this line is stable, which with Dai's theorem confirms the conjecture.
• 1996: Dai and Weiss (Theorem 3.1) proved stability of the fluid model for every work-conserving discipline, with an explicit emptying time.

Setting

A reentrant line has $I$ stations and $K$ classes. Fluid enters as class $1$ at rate one; class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$ and service rate $\mu_k = 1/m_k$, and on completion becomes class $k+1$ (class $K$ leaves). The constituency of station $i$ is $C_i = \{k : \sigma(k) = i\}$, and its nominal workload is $\rho_i = \sum_{k\in C_i} m_k$.

A fluid model solution is a pair of paths $Q(t) \in \mathbb R^K$ (fluid levels) and $T(t) \in \mathbb R^K$ (cumulative time spent serving each class) such that, for $t \ge 0$:

$$Q_k(t) = Q_k(0) + \mu_{k-1}T_{k-1}(t) - \mu_k T_k(t)\quad(\mu_0T_0(t) = t),\qquad Q_k(t) \ge 0,$$

each $T_k$ starts at $0$ and is nondecreasing, and the idle time $U_i(t) = t - B_i(t)$, with busy time $B_i(t) = \sum_{k \in C_i} T_k(t)$, is nondecreasing. These are the paper's equations (1.8)–(1.12). The solution is work conserving if, in addition, (1.13): $U_i$ increases only at times when station $i$ holds no fluid. The immediate volume of station $i$ is $W_i(t) = \sum_{k \in C_i} m_k Q_k(t)$.

A set of fluid model solutions is stable (Definition 1.3) if there is a $\delta > 0$ such that every solution with $|Q(0)| = \sum_k Q_k(0) = 1$ has $Q(t) = 0$ for all $t \ge \delta$.

The three-buffer line of Figure 1 has $I = 2$, $K = 3$ and route $1 \to 2 \to 1$: classes $1$ and $3$ at station $1$, class $2$ at station $2$. The load condition (3.1) is

$$\rho_1 = m_1 + m_3 < 1, \qquad \rho_2 = m_2 < 1 .$$

Formalization targets

Goal: Theorem 3.1

$$m_1, m_2, m_3 > 0,\ \ m_1 + m_3 < 1,\ \ m_2 < 1 \ \Longrightarrow\ \text{the work-conserving fluid model (1.8)–(1.13) of } 1 \to 2 \to 1 \text{ is stable.}$$

The goal fixes no emptying time: it asserts only that some $\delta > 0$ works, which is Definition 1.3.

Milestones, in attack order

1. Lemma 2.2 (ii): a nonnegative absolutely continuous $g$ with $\dot g(t) \le -\varepsilon$ almost everywhere where $g(t) > 0$ vanishes from $g(0)/\varepsilon$ on, and is nonincreasing.
2. Display (3.2) (already proved on the platform): at a regular point, the maximum of finitely many functions has the derivative of every component that attains it.
3. Lemma 3.2: for nonnegative linear functions $G_i$ of $Q$ with (a) $\dot G_i \le -\varepsilon_i$ while $W_i > 0$ and (b) $G_i \le \min_{j \ne i} G_j$ while $W_i = 0$, the maximum $G$ is absolutely continuous and nonnegative, and $\dot G(t) \le -\min_i \varepsilon_i$ at regular points with $G(t) > 0$.
4. Drift identity (proof of Theorem 3.1): with $\theta = m_1/(m_1+m_3)$, $G_1 = \theta Q_1^+ + (1-\theta)Q_3^+$ and $G_2 = Q_2^+$, where $Q_k^+ = \sum_{l \le k} Q_l$, one has $G_i(t) = G_i(0) + t - B_i(t)/\rho_i$.
5. Drift rate: $\dot G_i(t) = -(1/\rho_i - 1) < 0$ whenever $W_i(t) > 0$.
6. Condition (b): $W_1(t) = 0 \Rightarrow G_1(t) \le G_2(t)$ and $W_2(t) = 0 \Rightarrow G_2(t) \le G_1(t)$.
7. Emptying time: every work-conserving solution with $|Q(0)| = 1$ is empty from $\max\{\rho_1/(1-\rho_1), \rho_2/(1-\rho_2)\}$ on.

Significance

Theorem 3.1 settles stability of the three-buffer line for every work-conserving discipline at once, not only FIFO. Through Dai's 1995 theorem it gives positive Harris recurrence of the queueing network under any such discipline whose fluid limits satisfy (1.8)–(1.13), under that theorem's distributional assumptions. By the paper's remark after the proof, every other three-buffer reentrant line is feedforward, so with this theorem all three-buffer reentrant lines are stable under every work-conserving policy. The method, a Lyapunov function that is the maximum of linear functions of the fluid levels, recurs in the paper's later theorems (Lu–Kumar network, two-station Kelly-type lines) and in the wider fluid-stability literature.

The result is proved on paper; no machine-checked version exists. The mission's contribution is a formal fluid-model layer for reentrant lines (equations (1.8)–(1.13), Definition 1.3) shared with the other missions of this series, two reusable real-analysis lemmas (Lemma 2.2 (ii) and Lemma 3.2), and a complete formal proof of Theorem 3.1. The fluid-limit theorem linking fluid stability to the stochastic network is cited, not formalized.

Difficulty

The obvious approach is to split cases on the relative loads, as the paper notes ($m_1 + m_3/m_2 < 1$ or not), and track the fluid explicitly; this gives sharp emptying times but requires following solutions through regime changes, which is unwieldy when the discipline is arbitrary. The Lyapunov approach avoids this but moves the difficulty into analysis: the fluid paths are only Lipschitz, so derivatives exist only almost everywhere; the maximum of two Lyapunov components is not differentiable where they cross; and work conservation is a statement about where the idle time can increase, which has to be converted into "the busy time grows at rate one" at points where a station holds fluid. Lemma 2.2 (ii) itself needs the fundamental theorem of calculus for absolutely continuous functions.

Formalization scope

All declarations live in DaiWeissFluid.ThreeBuffer. Committed conventions:

• Classes and stations are 0-based (Fin 3, Fin 2). The paper's class $k$ is Lean k - 1; the line is threeBuffer m with station map ![0, 1, 0], and (3.1) reads m 0 + m 2 < 1, m 1 < 1.
• Paths are total functions ℝ → Fin K → ℝ; every equation is imposed only for $t \ge 0$, and derivatives are taken at $t > 0$ (HasDerivAt).
• Work conservation (1.13) is in interval form: $U_i$ is constant on every interval $[s,t] \subseteq [0,\infty)$ on which station $i$ holds fluid throughout. This is equivalent to the paper's integral condition for continuous paths.
• No Lipschitz continuity is assumed; it follows from (1.10)–(1.12).
• $m_k > 0$ is an explicit hypothesis (the paper takes it for granted). $|Q(0)| = \sum_k Q_k(0)$.
• Lemma 2.2 (ii) is stated with $\dot g(t) \le -\varepsilon$; the paper prints $<$, but every application uses $\le$, and the stated version is the stronger lemma.
• Lemma 3.2 is stated for any reentrant line with $I \ge 1$ stations, assuming only (1.8)–(1.12), as in the paper.

A trivializing formalization is ruled out: the work-conserving solution set of the three-buffer line is nonempty for every $m$ satisfying (3.1), with $|Q(0)| = 1$ (a sorry-free witness was checked), so the goal is not vacuous, and the goal quantifies over all work-conserving solutions rather than one discipline.

Needed infrastructure: Lipschitz and absolute continuity of the fluid paths, the a.e. fundamental theorem of calculus for absolutely continuous functions (in Mathlib), and the derivative of a finite maximum at a regular point (on the platform as display (3.2)). Lemma 2.2 (ii) and Lemma 3.2 are reusable for the other missions of the series. Proofs of any milestone are welcome independently.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 115–134, 1996. https://doi.org/10.1287/moor.21.1.115
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1), 49–77, 1995. https://doi.org/10.1214/aoap/1177004828
• P. R. Kumar, Re-entrant lines, Queueing Systems 13, 87–110, 1993. https://doi.org/10.1007/BF01158927
• A. N. Rybko and A. L. Stolyar, Ergodicity of stochastic processes describing the operation of open queueing networks, Problems of Information Transmission 28, 199–220, 1992.
• D. D. Botvich and A. A. Zamyatin, Ergodicity of conservative communication networks, Rapport de recherche 1772, INRIA, 1992.

Motivation

Stochastic processing networks (Harrison 2000) model manufacturing lines, data switches, call centers and multiclass queueing networks in one framework: jobs wait in buffers, activities process jobs from one or several buffers at once, each activity may need several processors simultaneously, and routing after service may depend on the activity used. A central control question is which dynamic policy keeps such a network stable whenever any policy can.

Dai and Lin (Oper. Res. 53(2), 2005) answer it with maximum pressure policies, a generalization of the back-pressure policy of Tassiulas and Ephremides (1992) for wireless networks. At each decision time the policy picks an extreme allocation maximizing a linear "network pressure" in the current buffer levels; it needs no arrival-rate information. Their main result (Theorem 2) is pathwise stability whenever Harrison's static planning LP has a feasible solution with $\rho\le1$. The proof goes through the fluid model: a deterministic, continuous analogue of the network whose stability implies stability of the stochastic system.

This mission formalizes Theorem 5 of the paper, the strong form of the fluid-level result: under a strict load condition $\rho<1$ and a mild structural assumption, every solution of the maximum pressure fluid model empties in finite time, uniformly over bounded initial states. Fluid stability in this sense (Definition 4) is the property that the standard fluid-limit machinery (Dai 1995) turns into positive Harris recurrence of the stochastic network.

Setting

The network has buffers $0,1,\dots,I$, where Buffer $0$ is the outside world and $\mathcal I=\{1,\dots,I\}$ are the internal buffers, activities $\mathcal J=\{1,\dots,J\}$ and processors $\mathcal K=\{1,\dots,K\}$.

• $A_{kj}\in\{0,1\}$ records whether activity $j$ needs processor $k$, and $B_{ji}\in\{0,1\}$ whether activity $j$ processes buffer $i$.
• An input activity processes only Buffer $0$; a service activity never processes Buffer $0$. Every activity is one or the other. Every processor serves only input activities (an input processor) or only service activities (a service processor).
• $m_j>0$ is the mean processing requirement of activity $j$, $\mu_j=1/m_j$, and $P^j$ is its routing matrix.

The input-output matrix is $R_{ij}=\mu_j\big(B_{ji}-\sum_{i'\in\mathcal I\cup\{0\}}B_{ji'}P^j_{i'i}\big)$. An allocation is $a\in\mathbb R^J_+$ with $\sum_jA_{kj}a_j\le1$ for every processor and $=1$ for every input processor; $\mathcal A$ is the set of allocations and $\mathcal E$ the set of its extreme points. The network pressure of $a$ at buffer level $z\in\mathbb R^I_+$ is $p(a,z)=z\cdot Ra$.

The static planning LP asks for $x\ge0$ and $\rho$ with $Rx=0$, $\sum_jA_{kj}x_j\le\rho$ for service processors and $=1$ for input processors. Assumption 1 (extreme-allocation-available, EAA) says that for every $z\in\mathbb R^I_+$ some maximizer of $p(\cdot,z)$ over $\mathcal E$ has $z_i>0$ on all its constituent buffers. Assumption 2 says there is $x\ge0$ with $Rx>0$ componentwise.

A fluid model solution is a pair of paths $(\bar Z,\bar T)$, buffer levels $\bar Z(t)\in\mathbb R^I$ and cumulative activity times $\bar T(t)\in\mathbb R^J$, satisfying (14)–(18): $\bar Z(t)=\bar Z(0)-R\bar T(t)$ (written out over buffers), $\bar Z\ge0$, input processors always busy, every processor's busy time at most elapsed time, and $\bar T$ nondecreasing with $\bar T(0)=0$. A time $t>0$ is regular if both paths are differentiable there. Under a maximum pressure policy the solution also satisfies (20): at each regular $t$,

$$R\dot{\bar T}(t)\cdot\bar Z(t)=\max_{a\in\mathcal E}Ra\cdot\bar Z(t).$$

Formalization targets

Goal: Theorem 5

$$\text{Assumptions 1, 2 and an LP solution with } \rho<1\ \Longrightarrow\ \exists\,\delta>0:\ |\bar Z(0)|\le1\Rightarrow \bar Z(t)=0\ \ \forall t\ge\delta,$$

for every solution of (14)–(18) and (20). The constant $\delta$ depends on the network only.

Milestones

1. For an input activity $j$, $R_{ij}=-\mu_jB_{j0}P^j_{0i}\le0$.
2. Assumption 2 yields $\hat x\ge0$ with $R\hat x>0$ that vanishes on input activities and loads no input processor.
3. After scaling $\hat x$, the vector $x^*=\tilde x+\hat x$ is an allocation and $Rx^*\ge\delta e$ for some $\delta>0$.
4. The maximum of $p(\cdot,z)$ over $\mathcal A$ is attained on $\mathcal E$ (p. 201).
5. The identities (22)–(23): $\dot f(t)=2\dot{\bar Z}(t)\cdot\bar Z(t)=-2R\dot{\bar T}(t)\cdot\bar Z(t)$ for $f=\sum_i\bar Z_i^2$.
6. $R\dot{\bar T}(t)\cdot\bar Z(t)\ge Rx^*\cdot\bar Z(t)\ge\delta\sum_i\bar Z_i(t)\ge\delta\|\bar Z(t)\|$.
7. $\dot f(t)\le-2\delta\sqrt{f(t)}$ at regular times.
8. The explicit emptying time: $\bar Z(t)=0$ for $t\ge\|\bar Z(0)\|/\delta$.

Significance

The result. Theorem 4 of the paper gives only weak stability (a fluid model started empty stays empty) under $\rho\le1$, which suffices for pathwise stability. Theorem 5 gives a uniform emptying time under $\rho<1$, the hypothesis that standard arguments (Dai 1995; Dai and Meyn 1995) need to conclude positive Harris recurrence and moment bounds for the stochastic network. The emptying-time bound is explicit and linear in the initial fluid level.

Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked proof exists. The closest formalized result on Prove2Me is ProcessingNetworks.BackPressure.bp_maximal_stability (Dai and Harrison's book, Theorem 9.12), which uses the same Lyapunov idea in a different model: exogenous arrival rates, the planning problem $Rx=\lambda$, no input activities and no Buffer 0. The present mission formalizes the Dai–Lin model with input processors, where the planning LP has $Rx=0$ and the equality constraints (2). The definitions file (network, $\mathcal A$, $\mathcal E$, pressure, fluid model, (20)) is shared in content with the other missions of this series.

Difficulty

Each algebraic step is short; the work is in the analysis. The obvious route reads $\dot f\le-2\delta\sqrt f$ as an ordinary differential inequality and integrates it. That requires the inequality almost everywhere, but it is only available at regular points. So one needs: Lipschitz continuity of $\bar T$ and $\bar Z$ on $[0,\infty)$ from (16)–(18), almost-everywhere differentiability (Rademacher), and a comparison argument for an absolutely continuous function, $\sqrt f=\|\bar Z\|$, whose derivative bound holds only where $f>0$. The step "by (20)" also needs the maximum over $\mathcal E$ to dominate every allocation in $\mathcal A$. That is the vertex property of a bounded polyhedron, which in Lean means compactness of $\mathcal A$ plus a Krein–Milman type argument. The published Dini-derivative extinction criterion ProcessingNetworks.LyapunovCriteria.dini_extinction_criterion (Dai–Harrison Lemma 8.11) is a possible tool for the last step, applied to $\|\bar Z\|$.

Formalization scope

• Indices are 0-based: internal buffers Fin I, buffers $0..I$ as Fin (I+1) with Buffer 0 the index 0 and internal buffer i the index i.succ, activities Fin J, processors Fin K.
• Paths are functions ℝ → (Fin n → ℝ) constrained only at $t\ge0$. Derivatives are deriv, used only at regular points.
• (20) is encoded as IsGreatest of the set of pressures over $\mathcal E$, so the maximum is attained and an empty $\mathcal E$ cannot pass through a junk supremum. $\mathcal E$ is Mathlib's Set.extremePoints.
• The fluid model of the theorem is the predicate "(14)–(18) and (20)". Solutions are not required to be fluid limits.
• The standing assumptions of §2 are one predicate, Network.Standing. Two disclosed additions are needed for the objects to make sense: every input processor has an activity, and $m_j>0$. The row sums of $P^j$ are not imposed.
• The theorem's text cites "the LP (9)–(12)". The proof needs $x\ge0$, so the LP used is (9)–(13), as in Theorems 1, 2 and 4.
• The norm in Definition 4 is Euclidean, as in the proof.
• Assumption 1 is a hypothesis of the goal because the page states it. The fluid-level argument does not use it.
• Ruled out: a vacuous goal. A sorry-free sanity file shows a one-buffer network (one input activity, one service activity) that satisfies every hypothesis of the goal and has a maximum pressure fluid solution. The milestone on the maximum over $\mathcal A$ carries the hypothesis $\mathcal A\neq\emptyset$, because the standing assumptions alone do not imply it.

Contributions of reusable lemmas are welcome, in particular almost-everywhere differentiability of Lipschitz paths on $[0,\infty)$, the vertex property of bounded polyhedra, and extinction of nonnegative absolutely continuous functions with $\dot g\le-\varepsilon$ on $\{g>0\}$.

Selected references

• J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. https://doi.org/10.1287/opre.1040.0170
• J. M. Harrison, Brownian models of open processing networks: canonical representation of workload, Annals of Applied Probability 10(1):75–103, 2000. https://doi.org/10.1214/aoap/1019737665
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1):49–77, 1995. https://doi.org/10.1214/aoap/1177004828
• L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Transactions on Automatic Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479
• J. G. Dai and J. M. Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press, 2020. https://doi.org/10.1017/9781108772662

Motivation

A stochastic processing network (Harrison 2000) models a system in which processors carry out activities and each activity draws jobs from one or more buffers. Manufacturing lines, call centers with cross-trained agents, and data switches all fit this model. A central question is which scheduling policies are throughput optimal, meaning they stabilize the network whenever any policy can.

Dai and Lin (Oper. Res. 53(2), 2005) show that maximum pressure policies are throughput optimal. These policies generalize the back-pressure rule of Tassiulas and Ephremides (1992) for wireless and switch networks, and at each moment they choose the allocation that maximizes a linear "network pressure". Their main theorem (Theorem 2) has one structural hypothesis, the extreme-allocation-available (EAA) assumption (Assumption 1). It holds for many familiar networks and fails for some (§6.2 gives a counterexample). Theorem 6 identifies a broad class where it always holds: strict Leontief networks, in the sense of Bramson and Williams (2003). This mission formalizes that theorem.

Setting

A network has internal buffers $\mathcal I=\{1,\dots,I\}$, an outside Buffer $0$, activities $\mathcal J=\{1,\dots,J\}$ and processors $\mathcal K=\{1,\dots,K\}$.

• $A_{kj}=1$ if activity $j$ needs processor $k$, and $0$ otherwise.
• $B_{ji}=1$ if activity $j$ processes buffer $i\in\mathcal I\cup\{0\}$, and $0$ otherwise. The set $\mathcal B_j=\{i:B_{ji}=1\}$ is the constituency of $j$.
• An input activity has $\mathcal B_j=\{0\}$; a service activity has $0\notin\mathcal B_j$. Every activity is one of the two.
• Each processor serves input activities only (an input processor) or service activities only.
• Activity $j$ has processing rate $\mu_j=1/m_j$ and a nonnegative routing matrix $P^j$.

The input-output matrix is

$$R_{ij}=\mu_j\Big(B_{ji}-\sum_{i'\in\mathcal I\cup\{0\}}B_{ji'}P^j_{i'i}\Big),\qquad i\in\mathcal I,\ j\in\mathcal J.$$

An allocation $a\in\mathbb R^J_+$ gives the level at which each activity runs. The allocation set $\mathcal A$ consists of the allocations with $\sum_jA_{kj}a_j\le1$ for every processor and $\sum_jA_{kj}a_j=1$ for every input processor. Write $\mathcal E$ for the set of its extreme points, the extreme allocations. For a buffer-level vector $z\in\mathbb R^I_+$ the network pressure is $p(a,z)=z\cdot Ra$. Buffer $i$ is a constituent buffer of $a$ if $\sum_ja_jB_{ji}>0$.

Assumption 1 (EAA). For every $z\in\mathbb R^I_+$ there is $a^*\in\mathcal E$ with $p(a^*,z)=\max_{a\in\mathcal E}p(a,z)$ such that $z_i>0$ for every constituent buffer $i$ of $a^*$.

A network is strict Leontief if every service activity has exactly one buffer in its constituency, denoted $i(j)$.

Formalization targets

Goal: Theorem 6 (p. 204)

$$\text{strict Leontief}\ \Longrightarrow\ \forall z\in\mathbb R^I_+\ \exists a^*\in\mathcal E:\ p(a^*,z)=\max_{a\in\mathcal E}p(a,z)\ \text{ and }\ z_i>0\ \text{for every constituent buffer } i \text{ of } a^*.$$

Milestones

1. (§3, p. 201) For every $z\in\mathbb R^I_+$, $\max_{a\in\mathcal A}p(a,z)$ is attained at an extreme allocation.
2. (p. 204) $B_{ji}=0$ and $R_{ij}\le0$ whenever $i\in\mathcal I$, $i\ne i(j)$.
3. (p. 204) Let $\mathcal J_0$ be the set of service activities $j$ with $z_{i(j)}=0$. Setting the coordinates of $\hat a\in\mathcal A$ in $\mathcal J_0$ to zero gives $\tilde a\in\mathcal A$ with $z'R\tilde a\ge z'R\hat a$.
4. (p. 204) It suffices to find $a^*\in\arg\max_{a\in\mathcal E}z'Ra$ with $a^*_j=0$ on $\mathcal J_0$.
5. (p. 204) If $\tilde a\in\mathcal A$ maximizes $z'Ra$ over $\mathcal A$ and vanishes on $\mathcal J_0$, some extreme allocation does both.

Significance

The result. Theorem 2 of the paper states that, under EAA, a maximum pressure policy is pathwise stable whenever the static planning problem has a feasible solution with $\rho\le1$. Theorem 6 removes the EAA hypothesis for strict Leontief networks. In that class maximum pressure is therefore throughput optimal with no further structural condition. The class includes multiclass queueing networks with alternate routes and networks of input-queued data switches (§9), so Theorem 6 is the step that turns the abstract main theorem into a statement about these concrete systems.

Formalizing it. The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. Formalizing it fixes the exact standing assumptions of the model, several of which the paper uses without stating (see below). It also yields a reusable Lean vocabulary for stochastic processing networks with input activities: $R$ from (5), the allocation polytope with the input-processor equality (2), extreme allocations, network pressure and EAA. The companion missions of this series on maximum pressure policies build on the same vocabulary.

Difficulty

The naive argument stops at "take a maximizing extreme allocation". A maximizer $\hat a$ may run a service activity whose buffer is empty, in which case EAA fails at $\hat a$. Removing such activities gives $\tilde a$, which has the right support and pressure but is in general not extreme. The pressure inequality depends on the sign pattern of $R$, which holds only because every service activity has a single buffer. In the network of §6.2 this sign pattern fails and so does EAA. Returning from $\tilde a$ to an extreme allocation without losing the support property needs a convex-geometry argument about the polytope $\mathcal A$. In Lean this means relating Set.extremePoints of a compact polyhedron to maximizers of a linear functional and to supports.

Formalization scope

• Indexing. Internal buffers are Fin I. Buffers including Buffer 0 are Fin (I+1), with Buffer $0$ as 0 and internal buffer $i$ as i.succ. Activities and processors are 0-based.

• Standing assumptions (§2), one predicate Network.Standing.

  • $A$ and $B$ are $0$–$1$ matrices.
  • Every constituency is nonempty, and every activity is an input or a service activity.
  • Every activity needs a processor.
  • Each processor serves input activities only or service activities only.
  • There is an input activity.
  • $P^j\ge0$ and $P^j_{00}=0$.

• Disclosed additions to the page.

  1. Every input processor has an activity. "The input processors are never idle" presupposes it.
  2. $m_j>0$. The page writes "nonnegative" but sets $\mu_j=1/m_j$.
  3. $\mathcal A\neq\emptyset$, an explicit hypothesis of the goal and of milestone 1. The paper presupposes it by listing $\mathcal E=\{a^1,\dots,a^E\}$. It does not follow from the standing assumptions: two input activities needing input processors $\{1,2\}$ and $\{2,3\}$ make (2) infeasible, so $\mathcal E=\emptyset$ and EAA fails in a network that is vacuously strict Leontief. A verification file checks this example in Lean.

• Conventions.

  • $\mathcal E$ is Mathlib's Set.extremePoints ℝ 𝒜.
  • Every "max" and "argmax" is in domination form ($p(a',z)\le p(a^*,z)$ for all $a'$), never sSup. Without attainment the statement would be vacuous.
  • Constituent buffers are internal buffers only. Buffer $0$ has no level.
  • $i(j)$ is written relationally.
  • Row sums of $P^j$ are not imposed.

• Trivializing formalizations ruled out. EAA must not be weakened to a supremum over a possibly empty $\mathcal E$, and Buffer $0$ must not be counted as a constituent buffer. Either change would make the goal trivially true or impossible.

• Infrastructure. Solvers need two results:

  • attainment of a linear maximum on extreme points of a compact convex polyhedron, via IsCompact.extremePoints_nonempty and Krein–Milman;
  • the fact that every extreme point in a convex decomposition of a maximizer with positive weight is a maximizer.

  Both are reusable beyond this mission. Contributions proving them as general Mathlib-style lemmas are welcome.

Selected references

• J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. https://doi.org/10.1287/opre.1040.0170
• J. M. Harrison, Brownian models of open processing networks: canonical representation of workload, Annals of Applied Probability 10(1):75–103, 2000. https://doi.org/10.1214/aoap/1019737665
• M. Bramson and R. J. Williams, Two workload properties for Brownian networks, Queueing Systems 45(3):191–221, 2003. (no link verified; see the reference list of Dai & Lin 2005)
• L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Transactions on Automatic Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479

Why throughput matters

A processing network must decide which activities receive scarce processor capacity while jobs move among buffers. Such decisions matter in manufacturing, service systems, and switches: one activity can consume several processors at once, and a job can be routed to another buffer after processing. A policy that sees current buffer levels but does not need to know arrival or routing rates is easier to operate when those rates are difficult to estimate. Dai and Lin's 2005 paper studies whether a maximum pressure policy, which uses the buffer vector and an input-output matrix, can stabilize every network that is stabilizable in their model. Their Theorems 1 and 2 give, respectively, a necessary planning condition for any stabilizing policy and a sufficient condition for maximum pressure under the extreme-allocation-available assumption. Dai and Lin (2005)

Here pathwise stability means that each internal buffer grows sublinearly in time almost surely. This is a rate statement about sample paths. It does not assert positive recurrence of a Markov chain, nor does it require a stationary distribution. The paper allows general primitive processing and routing processes with almost-sure long-run averages. Dai and Lin (2005), §§2–4

Network and allocations

There are $I$ internal buffers, $J$ activities, and $K$ processors. Buffer $0$ represents the outside world. The $K\times J$ matrix $A$ records resource use: $A_{kj}=1$ when activity $j$ requires processor $k$. The $J\times(I+1)$ matrix $B$ records which buffers an activity processes. An input activity processes Buffer $0$; a service activity does not. Input processors serve only input activities and must be fully used, while all processors have at most unit capacity.

For activity $j$, the processing requirements have mean $m_j$ and the routing counts have long-run matrix $P^j$. Write $\mu_j=1/m_j$. The input-output matrix is

$$R_{ij}=\mu_j\left(B_{ji}-\sum_{i'=0}^{I}B_{ji'}P^j_{i'i}\right),\qquad i=1,\ldots,I.$$

Positive $R_{ij}$ means activity $j$ consumes net material from internal buffer $i$; negative means it produces net material there. An allocation $a\in\mathcal A$ assigns nonnegative activity levels subject to the processor capacity bounds and the equality for every input processor. The finite set $\mathcal E$ consists of the extreme points of this allocation set. At buffer vector $z$, allocation $a$ has network pressure $p(a,z)=z\cdot Ra$. The maximum pressure rule chooses an allocation of greatest pressure among the currently feasible members of $\mathcal E$. Feasibility depends on jobs actually available to each constituent buffer. Dai and Lin (2005), §§2–3

The extreme-allocation-available assumption (EAA) says that for every nonnegative $z$, a pressure maximizer in $\mathcal E$ can be chosen whose constituent buffers all have positive levels. It links the static pressure maximization to the jobs that a policy can process. The static planning LP asks for activity fractions $x\ge0$ and a service-processor load $\rho$ such that $Rx=0$, every input processor has load one, and every service processor has load at most $\rho$. Dai and Lin (2005), p. 202

Formalization targets

The goal is Theorem 2. For a network satisfying EAA and run by a preemptive, processor-splitting maximum pressure policy, LP feasibility with $\rho\le1$ implies

$$\mathbb P\!\left(\forall i\in\{1,\ldots,I\},\ \lim_{t\to\infty}\frac{Z_i(t)}{t}=0\right)=1.$$

The milestones follow the paper's route from stochastic paths to deterministic fluid limits. A fluid limit is a uniform-on-compact limit of $(Z(rt),T(rt))/r$ along positive scales $r\to\infty$. The milestones state that fluid limits satisfy (14)–(18), weak stability of the corresponding fluid model transfers to pathwise stability (Theorem 3), maximum pressure adds (52)–(55) and (20) (Lemmas 5 and 4), quadratic fluid energy obeys (22)–(23), and LP feasibility with EAA makes the maximum-pressure fluid model weakly stable (Theorem 4). Dai and Lin (2005), pp. 203, 213–214

What the result gives

Theorem 2 identifies a policy whose almost-sure buffer growth rate vanishes whenever the planning LP permits load at most one and EAA holds. Together with the paper's necessary condition in Theorem 1, it characterizes the feasibility boundary for this policy class under EAA. Its scope includes networks in which an activity uses multiple processors and processes multiple buffers simultaneously. It does not claim that all such networks satisfy EAA. Dai and Lin (2005), Theorems 1–2

The result is proved in the 2005 article. This mission asks for a machine-checked proof of that known theorem and its selected intermediate claims. The Lean statements are open draft targets. Reusable outcomes include a model of cumulative routing and service counts, a uniform-on-compact fluid-limit interface, and the weak-fluid-stability transfer theorem for networks without a Markov assumption.

Why the proof is difficult

Maximizing pressure over the static allocation polytope does not by itself describe an executable service policy. An allocation can demand work from an empty buffer. EAA addresses the existence of a maximizing allocation supported by positive buffer levels, but the stochastic policy acts on actual jobs and completion times. The proof must connect those discrete, pathwise decisions to the limiting differential equation (20). At a regular fluid time, the maximum-pressure equation is decisive; away from regular times, derivatives need not exist. The fluid model therefore carries a time qualifier that cannot simply be dropped. Dai and Lin (2005), pp. 201–203, 214

Formalization scope

The Lean model uses finite index types for buffers, activities, and processors. Internal buffers are Fin I; Buffer 0 is the zero index of Fin (I+1), and an internal buffer maps to its successor index. Activity and processor labels use zero-based Fin. Time is real but all network equations are asserted for nonnegative time. The shared Bell–Williams Paths definition supplies the renewal count in $\mathbb N\cup\{\infty\}$ and uniform-on-compact distance using the $\ell^1$ norm. The completion count is required finite wherever the network equations convert it to a natural number; this prevents infinity from becoming a zero count. Bell and Williams (2001)

The network standing assumptions record binary incidence matrices, nonempty constituencies, processor coverage, activity types, and an input activity. Two refinements are explicit: each input processor has an activity, so its mandatory unit allocation is feasible, and $m_j>0$, so $\mu_j=1/m_j$ is defined as the intended positive rate. Routing counts are cumulative and nonnegative. Their row sums are constrained only for buffers an activity processes: the printed sentence requiring the same sum for every buffer conflicts with its immediately preceding statement that the count vanishes when the activity does not process that buffer. The corresponding rows of $P^j$ sum to one for processed buffers and vanish for unprocessed buffers, as follows from (4). Dai and Lin (2005), pp. 199–200

The policy predicate records allocation-time decomposition (49)–(51) and the non-employment consequence of Definition 1 used in (56)–(58). It checks feasibility of a competing extreme allocation through the paper's threshold $J$ at every time of the interval. Individual job states and tie breaking are outside the pathwise interface. The goal retains EAA, the exact $\rho\le1$ bound, and all network and policy equations, so an empty allocation set or an unconstrained service path cannot make the target automatic. Contributions formalizing the finite extreme-point set, fluid-limit compactness, Lemmas 4–5, and the weak-stability transfer are welcome.

Selected references

• J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. DOI.
• S. L. Bell and R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Annals of Applied Probability 11(3):608–649, 2001. DOI.