Queueing and Stochastic Networks

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.

Motivation

Maximum pressure policies schedule a stochastic processing network by choosing, at each decision time, an allocation of processors to activities that maximizes a linear "pressure" built from the current buffer levels and the network's input-output matrix. Dai and Lin (Oper. Res. 53(2), 2005) prove that such policies are throughput optimal: they stabilize the network whenever any policy can. The policies descend from the back-pressure rule of Tassiulas and Ephremides (IEEE TAC 37(12), 1992) for wireless networks and are now standard in switching, manufacturing and data-center scheduling.

The general theory lets a processor split its capacity among several activities at once. In many systems this is impossible: a machine works on one job type at a time. Section 7 of the paper shows that with this restriction Harrison's static planning LP no longer characterizes stability, and Section 8 shows that forbidding preemption can make a maximum pressure policy unstable. Both difficulties disappear for one structural class, the reversed Leontief networks, in which every activity needs exactly one processor. This mission formalizes the two lemmas that make that class work: extreme allocations are integral (Lemma 1), and a maximum pressure allocation is found processor by processor (Lemma 3).

Setting

A 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\}$. The resource consumption matrix $A$ has $A_{kj}=1$ if activity $j$ requires processor $k$ and $0$ otherwise. The constituency indicator $B_{ji}=1$ records that activity $j$ processes buffer $i$. An input activity processes only Buffer $0$; a service activity never processes Buffer $0$. Each processor runs input activities only (an input processor) or service activities only (a service processor). Each activity $j$ has a mean processing requirement $m_j$, rate $\mu_j=1/m_j$, and a 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 is $a\in\mathbb R^J_+$ with $\sum_j A_{kj}a_j\le1$ for every processor and $\sum_j A_{kj}a_j=1$ for every input processor; $\mathcal A$ is the set of allocations, $\mathcal E$ its set of extreme points, and $\mathcal N\subseteq\mathcal A$ the allocations with integer coordinates. For a buffer-level vector $z\in\mathbb R^I_+$, the network pressure is $p(a,z)=z\cdot Ra$ and the activity pressure is $p(j,z)=\sum_{i\in\mathcal I}R_{ij}z_i$, with $p(0,z)=0$ for the idle Activity $0$.

The network is reversed Leontief if each activity requires exactly one processor. The possible activities of processor $k$ are $\mathcal J(k)=\{j:A_{kj}=1\}$ for an input processor and $\mathcal J(k)=\{0\}\cup\{j:A_{kj}=1\}$ for a service processor. Under an integer allocation $a$, $j_k(a)$ is the activity processor $k$ works on, or $0$ if $k$ is idle.

Formalization targets

Goal: Lemma 3 (p. 208)

For a reversed Leontief network, $z\in\mathbb R^I_+$ and $a\in\mathcal E$,

$$p(a,z)=\max_{a'\in\mathcal E}p(a',z)\iff j_k(a)\in\operatorname*{arg\,max}_{j\in\mathcal J(k)}p(j,z)\ \text{ for all }k\in\mathcal K.$$

Milestones

• the pressure identity $p(a,z)=\sum_j a_j\,p(j,z)$ (§8, p. 208);
• $\mathcal N\subseteq\mathcal E$ (proof of Lemma 1, p. 215);
• Lemma 1 (p. 207): for a reversed Leontief network, $\mathcal E=\mathcal N$;
• for $a\in\mathcal E$: $j_k(a)\in\mathcal J(k)$ and $p(a,z)=\sum_k p(j_k(a),z)$ (proof of Lemma 3);
• the single-processor exchange $\tilde a=a-e_{j_k(a)}+e_j$ stays in $\mathcal E$ and shifts the pressure by $p(j,z)-p(j_k(a),z)$ (proof of Lemma 3).

A further supporting item, not a milestone, states the decomposition $a=\sum_{j\in\mathcal J(\tilde k)}a_j b^j$ of an allocation along one processor (proof of Lemma 1, p. 215).

Significance

The result. Lemma 1 says that, in a reversed Leontief network, the maximum pressure policies of the processor-splitting theory are automatically non-processor-splitting, so the paper's throughput optimality theorem holds in the setting where machines cannot be shared. Lemma 3 says that the maximization over the (exponentially large) set $\mathcal E$ decouples into one small maximization per processor: each processor picks an activity of largest activity pressure among its own options. This separability is what makes the nonpreemptive version of the policy well defined and is the key step towards Theorem 9 (throughput optimality of nonpreemptive maximum pressure policies). It also covers multiclass queueing networks with alternate routes (§9.1), which are reversed Leontief.

Formalizing it. Both lemmas are proved in the paper; to our knowledge neither is machine-checked. The mission produces a reusable Lean model of the allocation polytope of a processing network with input processors, its integer and extreme points, and the activity and network pressures. The integrality of $\mathcal E$ is a total-unimodularity-type fact for a block structure that is not available in Mathlib in this form.

Difficulty

The pressure is linear, so maximizing over $\mathcal E$ equals maximizing over $\mathcal A$; the substance is the description of $\mathcal E$. The polytope $\mathcal A$ is not a box: input processors carry equality constraints and service processors inequality constraints, and in general networks (an activity needing several processors) $\mathcal E$ contains fractional points, as the paper's example in §7 shows. The step that fails for general networks is the decomposition of a fractional allocation along a single processor: it needs every activity of that processor to use no other processor. In Lean, extreme points must be handled through Mathlib's Set.extremePoints, and the argmax over $\mathcal J(k)$ must keep track of the idle option, which exists for service processors and not for input processors.

Formalization scope

Indices are 0-based: internal buffers Fin I, buffers with Buffer $0$ Fin (I+1) (Buffer $0$ is 0, internal buffer $i$ is i.succ), activities Fin J, processors Fin K. The idle Activity $0$ is none : Option (Fin J), with activity pressure $0$ and unit vector $e_0=0$. $\mathcal E$ is Set.extremePoints ℝ 𝒜. "Maximizes the pressure over $\mathcal E$" is stated by domination ($p(a',z)\le p(a,z)$ for all $a'\in\mathcal E$), never through a supremum. $j_k(a)$ is defined by choice of an activity of $k$ at level $1$; it is used only for $a\in\mathcal E$, where it is unique.

The standing assumptions of §2 are carried as one hypothesis: $A$ and $B$ are $0$–$1$, constituencies are nonempty, every activity is an input or service activity and needs a processor, processors are input-only or service-only, at least one input activity exists, $P^j\ge0$ and $P^j_{00}=0$. Two disclosed additions: every input processor has at least one activity (otherwise (2) is infeasible and $\mathcal A=\emptyset$), and $m_j>0$ (needed for $\mu_j=1/m_j$). The goal keeps $z\ge0$ as on the page; two milestones drop it, which strengthens them.

A trivializing formalization would make $\mathcal E$ empty or give input processors an idle option; both are excluded: $\mathcal E$ is the extreme-point set of the real polytope $\mathcal A$, which is nonempty for a reversed Leontief network under the standing assumptions, and the idle option belongs to $\mathcal J(k)$ only for service processors, as in (60).

Contributions welcome: proofs of the milestones, a general lemma that $0$–$1$ points of a subset of the unit cube are extreme, and the separable description of extreme points of products of simplices, which is reusable beyond this mission.

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
• 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 priority rules in reentrant lines matter

Semiconductor wafer fabrication is the standard example of a reentrant line: every wafer follows the same long route through a set of machines, and visits several machines many times. Each visit is a separate processing step, and a machine with work waiting from several steps must choose which step to serve. Kumar (1993) proposed studying such lines through their buffer priority rules, and Lu and Kumar (1991) showed that a priority rule can make a line unstable even though every machine has spare capacity. The question is therefore not academic: a scheduling rule that looks reasonable can let queues grow without bound.

Dai (1995) reduced the positive Harris recurrence of a multiclass queueing network to the stability of a deterministic fluid model, and Dai and Weiss (1996) used this reduction to prove stability results for several reentrant lines. This mission formalizes their Theorem 4.3: under the First-Buffer-First-Served (FBFS) discipline, the fluid model of every reentrant line is stable whenever each station's nominal workload is below one. Kumar (1993) had proved the analogous statement for discrete deterministic systems.

Timeline:

• 1991. Lu and Kumar exhibit a two-station reentrant line that is unstable under a static priority rule with every workload below one.
• 1993. Kumar proves stability of FBFS and LBFS for discrete deterministic reentrant lines.
• 1995. Dai shows that stability of the fluid model implies positive Harris recurrence of the stochastic network.
• 1996. Dai and Weiss prove that the FBFS and LBFS fluid models of every reentrant line are stable (Theorems 4.3 and 4.4), and with Dai's theorem obtain stability of the stochastic networks.

Setting

A reentrant line has $I$ stations and $K$ classes. All fluid follows one route: it enters as class $1$, becomes class $k+1$ when class $k$ is completed, and leaves after class $K$. Class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$, and $\mu_k = 1/m_k$. 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$. The exogenous arrival rate is $1$. The standing assumption of the paper is

$$\rho_i < 1 \qquad (i = 1,\dots,I). \tag{1.7}$$

A fluid model solution is a pair of paths $Q(t) = (Q_k(t))_k$, the fluid levels, and $T(t) = (T_k(t))_k$, the cumulative service time given to 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), \qquad Q_k(t) \ge 0,$$

with $\mu_0T_0(t) = t$; each $T_k$ starts at $0$ and is nondecreasing; and the idle time $U_i(t) = t - \sum_{k\in C_i}T_k(t)$ of each station is nondecreasing.

A buffer priority discipline is a permutation $\pi$ of the classes; a class $k$ has priority over a class $l$ at the same station when $\pi(k) < \pi(l)$. Write $H_k = \{l \in C_{\sigma(k)} : \pi(l) \le \pi(k)\}$, $T_k^+ = \sum_{l\in H_k}T_l$, $U_k^+(t) = t - T_k^+(t)$ and $W_k^+ = \sum_{l\in H_k} m_l Q_l$. Under preemptive resume, $U_k^+$ may increase only at times when $W_k^+ = 0$ (condition (4.4)): a station never idles toward the classes of priority at least that of $k$ while any of them holds fluid. FBFS is $\pi(k) = k$, so earlier steps of the route have priority.

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

Formalization targets

Goal: Theorem 4.3

For every reentrant line with $m_k > 0$ and (1.7),

$$\text{the fluid model (1.8)–(1.12), (4.4) with } \pi(k) = k \text{ is stable.}$$

The goal asserts existence of an emptying time; it does not fix the value.

Milestones

1. Lemma 2.2 (i): a nonnegative function has zero derivative wherever it vanishes and is differentiable.
2. Lemma 2.2 (ii): an absolutely continuous nonnegative $g$ whose derivative is at most $-\varepsilon$ wherever $g > 0$ vanishes from $g(0)/\varepsilon$ on, and is nonincreasing.
3. Proposition 4.2: at a regular time of a priority fluid model, an empty buffer has equal in- and out-flow rates, and at each station the highest-priority nonempty class satisfies $\sum_{k\in H_{k_0}} m_kd_k = 1$ while lower-priority classes have zero out-flow.
4. Inductive step (proof of Theorem 4.3): once buffers $1,\dots,k-1$ stay empty from $t_{k-1}$ on, buffer $k$ is empty from $t_k = t_{k-1} + Q_k(t_{k-1})m_k/(1 - \sum_{l\in H_k} m_l)$ on.
5. Emptying time (proof of Theorem 4.3): every solution with $|Q(0)| = 1$ is empty from

$$\delta = \sum_{k=1}^K m_k\frac{\prod_{l=1}^{k-1}(1-\sum_{j\in H_l\setminus\{l\}}m_j)}{\prod_{l=1}^{k}(1-\sum_{j\in H_l}m_j)}$$

on, which gives the goal with an explicit constant.

Significance

Combined with Dai's theorem (Theorem 1.1 of the paper), Theorem 4.3 gives positive Harris recurrence of every multiclass reentrant line operated under FBFS, under the distributional assumptions of that theorem, whenever (1.7) holds. Since Lu–Kumar-type examples show that priority rules can destabilize a network with spare capacity, a rule that is provably stable on every reentrant line is a meaningful guarantee. FBFS, together with LBFS, is the basic positive case against which the instability examples in the same paper (Theorem 5.1) are compared.

Formalizing the result adds a machine-checked version of the fluid model with priority constraints, stated for an arbitrary line rather than a fixed network, and a checked explicit emptying time. The result is proved in the paper; no machine-checked proof is known. The rate identities of Proposition 4.2 and the extinction lemma are reused by the LBFS mission of this series.

Difficulty

The fluid model gives the paths only as nondecreasing functions subject to equations; nothing says they are differentiable. Every argument about rates holds only at regular times, and the conclusion must be integrated back through absolute continuity, which itself must be derived from the monotonicity conditions. The priority condition (4.4) is an "increases only when empty" condition; turning it into the rate identity (4.6) at a regular point requires continuity of the fluid levels and a careful local argument. The induction over classes needs uniform control of every earlier buffer for all later times, not only at one instant, so a pointwise reading of "buffer $k-1$ is empty" is not enough. Finally, the explicit constant $\delta$ requires bounding the content of buffer $k$ at time $t_{k-1}$ by the total content, which may have grown since time $0$.

Formalization scope

• Classes and stations are Fin K and Fin I, 0-based: the paper's class $k$ is Lean index $k-1$.
• Paths are total functions ℝ → Fin K → ℝ; every equation is imposed on $t \ge 0$ only, and derivatives are taken at $t > 0$.
• Conditions (1.13) and (4.4) are in interval form (ConstantWhile): the idle process is constant on every interval of $[0,\infty)$ on which the content stays positive. This is equivalent to the paper's Stieltjes integral form for continuous paths.
• Lipschitz continuity of the paths is not assumed; it follows from the monotonicity conditions.
• $m_k > 0$ is an explicit hypothesis; the paper takes it for granted.
• Priorities are Equiv.Perm (Fin K), FBFS is the identity; $|Q(0)|$ is $\sum_k Q_k(0)$.
• In Lemma 2.2 (ii) the printed strict "$\dot g(t) < -\varepsilon$" is relaxed to "$\le -\varepsilon$", as every application requires; absolute continuity is dropped from Lemma 2.2 (i), where it is not needed. Both changes strengthen the lemma.
• In the inductive step, "stay empty for $t > t_{k-1}$" is read as $t \ge t_{k-1}$, and the case $Q_k(t_{k-1}) = 0$ is included.
• The stochastic network is not formalized; only the fluid model is.

A trivializing formalization is ruled out: the goal uses the priority fluid model, not the work-conserving one alone (which would claim that every work-conserving fluid model is stable, false by Theorem 5.1), and a sorry-free witness shows that the FBFS solution predicate has solutions with $|Q(0)| = 1$, so stability is not vacuous.

Contributions welcome: the extinction lemma for absolutely continuous functions, the derivation of Lipschitz continuity from (1.10)–(1.12), and the rate identities of Proposition 4.2 are reusable beyond this mission.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1) (1996) 115–134. 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) (1995) 49–77. https://doi.org/10.1214/aoap/1177004828
• P. R. Kumar, Re-entrant lines, Queueing Systems 13 (1993) 87–110. https://doi.org/10.1007/BF01149327
• S. H. Lu and P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Transactions on Automatic Control 36(12) (1991) 1406–1416. https://doi.org/10.1109/9.106159

Motivation

A manufacturing line can send the same job through several stations and return it to a station it visited earlier. Semiconductor fabrication is one example. Such a reentrant line has several customer classes at one server, and the server must choose which class to work on. A station may have enough capacity on average yet the line can still accumulate an unbounded queue under an unfortunate service rule. Dai and Weiss use deterministic fluid models to study this question: fluid represents large queues, and its motion exposes the long-run effect of the service rule. Their paper proves that two simple buffer priority disciplines have stable fluid models for every reentrant line satisfying the usual station load condition. This mission concerns Last-Buffer-First-Served, abbreviated LBFS. Dai and Weiss (1996).

The distinction between fluid and stochastic queue stability matters. Dai and Weiss cite an earlier theorem connecting stable fluid models to stable queueing disciplines under the stochastic assumptions of their introduction. The target here is their fluid theorem, Theorem 4.4, rather than a separate formalization of that stochastic implication. Dai and Weiss (1996), pp. 115, 119, 124.

Setting

There are $K$ classes, numbered in route order, and $I$ stations. Every unit of fluid enters class $1$ at rate one. On completing service in class $k$, it becomes class $k+1$; after class $K$, it leaves. The station serving class $k$ is $\sigma(k)$. Different classes may share a station. The constituency of station $i$ is $C_i=\{k:\sigma(k)=i\}$, and class $k$ has positive mean service requirement $m_k$, so its service rate is $\mu_k=1/m_k$. The nominal workload at station $i$ is $\rho_i=\sum_{k\in C_i}m_k$. The paper assumes $\rho_i<1$ at every station. Dai and Weiss (1996), pp. 115–117.

For time $t\ge0$, $Q_k(t)$ is the amount of fluid in class $k$, and $T_k(t)$ is the cumulative server time spent on that class. The flow equations say that class content equals its initial content plus completed service from the preceding class minus its own completed service. The first class receives the external unit-rate flow. Each $Q_k$ remains nonnegative, each $T_k$ starts at zero and is nondecreasing, and the cumulative idle time of every station is nondecreasing. A priority rule adds a condition on when a server may reserve capacity for lower-ranked classes. These are the fluid equations of Definition 1.2 and §4. Dai and Weiss (1996), pp. 118, 122–123.

A priority ranking $\pi$ assigns a distinct rank to every class, with smaller rank meaning higher priority. For class $k$, let $H_k$ contain the classes at the same station whose rank is at least as high as $k$'s. In a preemptive-resume priority fluid model, capacity unused by $H_k$ may increase only when the fluid workload in $H_k$ is zero. Under LBFS, $\pi(k)=K+1-k$: a class later in the route has higher priority. Priority is compared within each station, even though the ranking is written globally. Dai and Weiss (1996), pp. 122–123, Definition 4.1.

Formalization targets

Theorem 4.4 asks for stability of the LBFS fluid model for every reentrant line with positive service requirements and $\rho_i<1$:

$$\exists\delta>0\;\forall (Q,T),\quad \bigl[(Q,T)\text{ is an LBFS fluid solution and }|Q(0)|=1\bigr] \Longrightarrow \forall t\ge\delta,\;Q(t)=0,$$

where $|Q(0)|=\sum_{k=1}^K Q_k(0)$. The same $\delta$ must work for every solution and every normalized initial configuration. This is exactly the fluid stability definition used by the paper. Dai and Weiss (1996), pp. 118–119, 124.

The milestones follow the paper's own intermediate statements. Lemma 2.2 treats a nonnegative absolutely continuous function whose derivative is negative whenever the function is positive. Proposition 4.2 identifies flow-rate relations at a regular point under a buffer priority rule. The proof of Theorem 4.4 records a uniform negative drift for total content and the explicit emptying time

$$\delta=\frac{|Q(0)|}{\widehat\lambda-1},\qquad \widehat\lambda=\frac{1}{\max_{1\le i\le I}\rho_i}>1.$$

The explicit time is stated for every initial fluid amount; normalization to one belongs only to the final stability theorem. Dai and Weiss (1996), pp. 120, 123–125.

Significance

The theorem gives a uniform finite clearing time for the LBFS fluid model whenever each station's nominal workload is below its capacity. It applies to any number of stations, any finite route, and any assignment of route stages to stations. This is stronger than checking a particular factory layout. The conclusion concerns every fluid solution, which matters because the defining equations need not determine a unique path. Dai and Weiss (1996), pp. 118–119, 124–125.

Formalizing the result requires a reusable interface for reentrant lines, service allocation, station workloads, and the priority complementarity condition, plus separate statements for the extinction criterion and priority flow rates. The theorem is proved in the 1996 paper; the remaining work in this mission is a machine-checked Lean proof of its fluid-model statement and of the listed milestones. The stochastic queueing theorem cited by Dai and Weiss is outside this mission's scope.

Difficulty

The load inequalities $\rho_i<1$ compare average work with available server time, but by themselves they do not specify which class receives service at an instant. Under other service rules, reentrant lines can amplify queued fluid despite every station being nominally underloaded; the same paper gives such an example. A formal proof therefore has to use the precise LBFS priority condition, not only the flow equations and the load inequalities. The regular-time argument must then yield a single bound valid across every possible fluid path. Dai and Weiss (1996), §§4–5.

Formalization scope

Lean represents classes and stations by finite index types. Their indices start at zero: Lean class $k-1$ corresponds to paper class $k$, and LBFS is Fin.revPerm. The paths $Q$ and $T$ are functions on all real times, while the fluid equations and conclusions are imposed only for $t\ge0$. The external arrival rate is one, as in the paper's normalization. The conditions that station idle capacity and priority-set unused capacity increase only when their relevant content is zero are expressed by constancy on each interval where that content stays positive. Service and fluid paths are not given extra continuity hypotheses; the fluid equations and monotonicity conditions provide the regularity used in the paper. Dai and Weiss (1996), pp. 116–119, 122–123.

The service requirements $m_k>0$ are explicit so $\mu_k=1/m_k$ has its intended value. The drift and emptying-time milestones explicitly assume $K>0$, since their formula divides by the maximum station workload. The main theorem retains the universal quantification over lines; when $K=0$, its normalization $|Q(0)|=1$ is impossible. A faithful solution predicate must include the priority condition (4.4), whose omission would change Theorem 4.4 into a false claim about all work-conserving policies. The definition layer, elementary real-analysis extinction lemma, and priority flow-rate relations are useful beyond this single stability theorem. Dai and Weiss (1996), pp. 117–125.

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. DOI: 10.1287/moor.21.1.115.

Motivation

A multiclass queueing network can be unstable even when every station has enough capacity on average: the queue lengths grow without bound although each server's nominal load is below one. Kumar and Seidman, Lu and Kumar (1991) and Rybko and Stolyar (1992) exhibited such networks under simple priority disciplines. This raised the question of which networks are stable under every reasonable policy, and which policies are stable in every network. Dai (1995) reduced the stability of a queueing network to the stability of its deterministic fluid model, so that the question becomes one about solutions of a system of linear equations and inequalities.

Dai and Weiss (1996) use this reduction to study reentrant lines, the model of semiconductor wafer fabrication in which a single route visits the same machines many times. Section 6 of their paper treats Kelly-type lines, in which every visit to a station has the same mean service time. Kelly (1979) showed that such networks with exponential service times are stable under FIFO and have a product-form stationary distribution. Theorem 6.1 shows that with two stations, and a route that never visits the same station twice in a row, stability holds under every work-conserving policy, not only FIFO. This mission formalizes that theorem.

Setting

A reentrant line has stations $1,\dots,I$ and classes $1,\dots,K$. Fluid enters class $1$ at rate $1$, moves from class $k$ to class $k+1$ on service, and leaves after class $K$. Class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$ and rate $\mu_k = 1/m_k$. 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$. The traffic condition (1.7) is $\rho_i < 1$ for every $i$.

A fluid model solution is a pair $(Q, T)$: $Q_k(t) \ge 0$ is the fluid in class $k$ at time $t$ and $T_k(t)$ the cumulative service time given to class $k$ by time $t$. They satisfy, for $t \ge 0$,

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

$T_k(0) = 0$ with $T_k$ nondecreasing, and the idle time $U_i(t) = t - B_i(t)$, where $B_i(t) = \sum_{k\in C_i} T_k(t)$, is nondecreasing. The solution is work-conserving if $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)$.

The line is of Kelly type with station means $\beta_1, \dots, \beta_I$ if $m_k = \beta_{\sigma(k)}$ for every class $k$. Its routing has no immediate feedback if $\sigma(k+1) \ne \sigma(k)$ for every $k < K$. A set of fluid solutions is stable (Definition 1.3) if there is a $\delta > 0$ such that every solution in the set with $|Q(0)| = \sum_k Q_k(0) = 1$ is empty from time $\delta$ on.

Formalization targets

Goal: Theorem 6.1

For a two-station Kelly-type reentrant line without immediate feedback that satisfies (1.7), the work-conserving fluid model is stable: there is $\delta > 0$ with

$$\sum_k Q_k(0) = 1 \ \Longrightarrow\ Q_k(t) = 0 \quad \text{for all } t \ge \delta,\ k = 1,\dots,K,$$

for every work-conserving fluid solution $(Q,T)$. The number of classes $K$ is arbitrary, of either parity, and the route may start at either station.

Milestones

The milestones follow the proof on p. 130 and the two general lemmas it uses: the extinction criterion of Lemma 2.2 (ii); the derivative of a maximum at an active index, display (3.2), already proved on the platform; the piecewise-linear Lyapunov Lemma 3.2; the drift identity $G_i(t) = G_i(0) + |C_i|t - B_i(t)/\beta_i$ for $G_i = \sum_{k\in C_i} Q_k^+$, with $Q_k^+ = \sum_{l\le k} Q_l$; the comparison $W_i(t) = 0 \Rightarrow G_i(t) \le G_j(t)$; and the verification that $G_1, G_2$ meet the hypotheses of Lemma 3.2 with $\varepsilon_i = 1/\beta_i - |C_i|$.

Significance

The result. Theorem 6.1 gives a class of networks in which stability needs no knowledge of the scheduling policy: any policy that never idles a server with work waiting is stable whenever the nominal loads are below one. For queueing networks this is the property usually called global stability. Through Theorem 1.1 of the paper (Dai 1995, Theorem 4.3) the fluid statement implies positive Harris recurrence of the corresponding multiclass queueing network under every work-conserving head-of-the-line policy. The paper's Remarks 2 and 3 show the boundary: with immediate feedback (the line $1,2,2,2,1,1$ with all means $0.3$), or with three stations, a Kelly-type line can be unstable. A two-station Kelly-type line without immediate feedback is a unidirectional ring with one customer type, so the theorem is a special case of the ring-network result the paper proves as Theorem 6.2. That result is an open goal on the platform (ProcessingNetworks.GlobalStability.ring_globally_stable, Dai and Harrison's Theorem 8.24) in a different encoding of the fluid model.

Formalizing it. The theorem is proved in the paper, and the mission formalizes that proof. No machine-checked proof of the result, or of the Lyapunov lemmas it uses, is known to exist. The mission also produces reusable pieces: a fluid model of reentrant lines in the paper's own formulation, an extinction lemma for absolutely continuous functions, and the max-of-linear Lyapunov lemma, which the paper uses again in §§3 and 5.

Difficulty

The obvious Lyapunov function, the total workload, does not work: a work-conserving policy may starve a station while the other one is busy, so the total content need not decrease. The paper's components $G_i = \sum_{k\in C_i}Q_k^+$ each decrease at the constant rate $1/\beta_i - |C_i|$ while station $i$ is busy. When station $i$ is idle, $G_i$ can grow, and the argument then needs the comparison $G_i \le G_j$, which requires the alternating route. The analytic difficulty is the passage from these pointwise statements to extinction. Fluid paths are only Lipschitz. The maximum $G = \max(G_1, G_2)$ need not be differentiable where the maximum switches, and the drift statements hold only almost everywhere. Lemma 2.2 (ii) and the derivative-of-a-maximum fact (3.2) make this step rigorous. The proof for odd $K$ is not printed ("can be proved similarly"), and the formal goal covers it.

Formalization scope

All objects live in the namespace DaiWeissFluid.KellyType. The conventions are fixed as follows.

• Classes and stations are 0-based (Fin K, Fin I). The paper's class $k$ is Lean k - 1.
• Paths are total functions ℝ → Fin K → ℝ, and every equation is imposed for $t \ge 0$ only. Derivatives are taken at $t > 0$ via HasDerivAt.
• Work conservation (1.13) is stated in interval form: $U_i$ is constant on every interval $[s,t] \subseteq [0,\infty)$ on which station $i$ holds fluid throughout. For the continuous nondecreasing $U_i$ this is equivalent to the paper's Stieltjes condition. Lipschitz continuity of the paths is not assumed, because it follows from the model.
• $m_k > 0$ is an explicit hypothesis. $|Q(0)|$ is $\sum_k Q_k(0)$.
• Stability is Definition 1.3, which constrains only solutions with $|Q(0)| = 1$.
• The paper's Theorem 6.1 says "any work-conserving policy is stable", which is stability of the queueing network (Definition 1.1). Its proof establishes stability of the work-conserving fluid model, and the queueing-level conclusion follows from the cited Theorem 1.1 (Dai 1995). The goal is the fluid statement. Theorem 1.1 and the stochastic model are not formalized.
• Lemma 2.2 (ii) is stated with the hypothesis $\dot g \le -\varepsilon$, where the page prints $<$. This is the form in which every application uses it, and it gives a stronger lemma.
• The drift identity is stated for every Kelly-type line, which implies the printed $K = 2n$ display. The printed "$G_2(t) = G_2(t) + nt - \dots$" is read as $G_2(0) + nt - \dots$.
• Condition (b) and the Lemma 3.2 check are stated for both parities of $K$ and both starting stations. A station with no classes has its $\varepsilon_i$ left free.

The goal must not be trivialized. It quantifies over all work-conserving solutions with $|Q(0)| = 1$, and this set is nonempty: a sorry-free witness with $K = 2$ is checked locally. Neither the Kelly-type hypothesis nor the absence of immediate feedback may be dropped (Remark 2), nor may the goal be generalized beyond two stations (Remark 3). Restricting it to even $K$, or to a route starting at station 1, would weaken it.

Contributions welcome: proofs of the general Lemmas 2.2 (ii) and 3.2, which apply across the whole series; the drift identity, which is pure algebra from (1.8); the continuity facts for fluid paths (Lipschitz bounds from (1.10)–(1.12)); and the final assembly.

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
• S. H. Lu and P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Transactions on Automatic Control 36(12), 1406–1416, 1991. https://doi.org/10.1109/9.106156
• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979.
• 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 reentrant line is a queueing network in which every customer follows one fixed route but may return to a station after visiting another one. A manufacturing line can have this pattern when a product revisits the same machine at different processing stages. A station can then have little nominal workload and still face unstable queues under an unfortunate service order. Dai and Weiss studied this gap between nominal capacity and fluid stability for reentrant lines in their 1996 paper. The four-class line associated with Lu and Kumar is their sharp example: its behavior changes at a simple cross-station inequality that is different from either station's ordinary workload constraint.

The paper establishes several positive stability results for other disciplines and networks, then gives an exact boundary for the Lu–Kumar line. Here the exact boundary is the focus. The result concerns fluid models, deterministic large-scale approximations of queue trajectories. It does not assert positive Harris recurrence or transience of the underlying stochastic network in both directions. The paper cites Dai's earlier implication from a stable fluid model to a stable stochastic discipline, but the converse was still open in its concluding discussion (Dai and Weiss 1996, pp. 119 and 133).

Setting

There are four customer classes, encountered in order $1\to2\to3\to4$. Classes $1$ and $4$ use station $1$; classes $2$ and $3$ use station $2$. Each class $k$ has a positive mean service time $m_k$ and service rate $\mu_k=1/m_k$. The external arrival rate is normalized to one. The nominal workloads are $\rho_1=m_1+m_4$ and $\rho_2=m_2+m_3$, both assumed strictly below one. These assumptions say that each station has enough average capacity for its own stages, but they leave the scheduling decision unresolved.

At time $t$, $Q_k(t)\ge0$ is the amount of class-$k$ fluid, and $T_k(t)$ is the cumulative service time devoted to that class. The fluid equations balance the inflow and outflow of each class. Outside fluid enters class $1$ at unit rate; completion of class $k$ feeds class $k+1$ until class $4$ exits. Service times and idle times are nondecreasing, and a station's idle time can increase only when its total queue content is zero. A pair $(Q,T)$ with these properties is a work-conserving fluid solution.

The Lu–Kumar priority discipline gives class $4$ priority over class $1$ at station $1$, and class $2$ priority over class $3$ at station $2$. Its fluid model adds the priority complementarity condition: service capacity available to a priority prefix can be unused only when that prefix has no immediate workload. For either model, fluid stability means that some common time $\delta>0$ empties every admissible solution with $\sum_kQ_k(0)=1$, with all queues remaining zero for $t\ge\delta$. Instability is the negation of this statement; it does not require every solution to diverge.

Formalization targets

Exact threshold

Theorem 5.1 and Remark 1 give two connected classifications, under $m_k>0$, $\rho_1<1$, and $\rho_2<1$:

$$\neg\operatorname{FluidStable}(\text{all work-conserving solutions}) \quad\Longleftrightarrow\quad m_2+m_4\ge1,$$ $$\neg\operatorname{FluidStable}(\text{Lu–Kumar priority solutions}) \quad\Longleftrightarrow\quad m_2+m_4\ge1.$$

The first clause captures the paper's existence of an unstable work-conserving policy: on the unstable side, the named priority discipline supplies one; on the other side, every work-conserving fluid model is stable. The second clause records the particular policy classification stated in Remark 1. Equality belongs to the unstable side: the paper exhibits a periodic nonempty solution there (Dai and Weiss 1996, pp. 125–127).

Supporting targets

The milestones follow the paper's own statements and proof claims. The real-analysis extinction criterion of Lemma 2.2(ii) and the maximum-of-components criterion of Lemma 3.2 provide the stability language. Display (3.2), already available as a proved platform theorem, identifies the derivative of an attained maximum at a regular point. The priority condition (4.4) implies the ordinary work-conserving condition (1.13). The unstable half records one first cycle, one solution with every scaled cycle, and instability of the priority model. The stable half records the authors' explicit parameter choice, the two linear Lyapunov conditions, and stability of every work-conserving fluid solution.

Significance

The threshold says that the two station-load inequalities alone do not characterize stability of all work-conserving service orders. The extra inequality $m_2+m_4<1$ determines when the entire work-conserving fluid class is stable; its failure admits a concrete priority discipline with a nonempty trajectory. At the boundary $m_2+m_4=1$, growth need not be strict: periodic fluid behavior already defeats finite-time stability. The result therefore distinguishes the paper's global stability region from the larger parameter region in which both stations are nominally underloaded (Dai and Weiss 1996, Remark 1, p. 125).

A machine-checked development would give reusable definitions for a four-stage reentrant fluid model, its priority complementarity condition, and the precise unit-initial-state notion of stability. The local Lean statements in this proposal compile, but their proofs remain open. The published maximum-derivative fact is the one already proved platform component used by this mission. The other milestones identify the mathematical work needed to formalize the known 1996 result, rather than presenting the result as a new open conjecture.

Difficulty

The ordinary load test $\rho_i<1$ controls how much service each station needs on average, but it does not control which class receives service when several buffers at a station are nonempty. In the Lu–Kumar priority discipline, serving a high-priority downstream class changes the future arrival pattern seen by the other station. Thus a direct argument from $\rho_1<1$ and $\rho_2<1$ to queue extinction fails. On the stable side, checking a single station's workload is also insufficient: its content may fall while earlier-stage fluid continues to feed it. The paper formulates two linear components and a finite maximum; the challenge is to obtain a uniform negative drift whenever that maximum is positive, including times when one station is empty and the other determines the active component (Dai and Weiss 1996, pp. 126–128).

Formalization scope

Classes and stations are Fin 4 and Fin 2, with zero-based Lean indices: paper class $k$ is Lean index $k-1$. The fixed station map is $(0,1,1,0)$. Service times remain real parameters with explicit positivity hypotheses. Paths are total functions of real time, while equations and conclusions apply only on $t\ge0$. The external arrival rate is one, and initial size is the sum $\sum_kQ_k(0)$, since class contents are nonnegative. The nominal-load assumptions are the two strict inequalities in (5.1). The named priority ranking is a permutation; it encodes only the station-local comparisons that matter.

Conditions (1.13) and (4.4), printed as complementarity or “increases only when empty,” use an equivalent interval-constancy condition in Lean. No extra Lipschitz or continuity assumption is placed on solutions: the fluid equations and monotone capacity constraints are intended to supply that regularity. Derivatives at regular points are represented with HasDerivAt. Lemma 2.2(ii) uses the non-strict bound $\dot g\le-\varepsilon$, the version used by the paper's applications, although its displayed hypothesis prints $\dot g<-\varepsilon$. The p. 127 line involving $G_1$ prints $(1-\theta_2)Q_4$; (5.3) fixes the intended coefficient as $(1-\theta_1)Q_4$.

The goal uses Definition 1.3 exactly: one uniform emptying time for all solutions of unit initial content. An impossible solution predicate, or an instability claim that only asks for a nonzero state at time zero, would not represent the paper's theorem. The mission needs finite-index sum and maximum infrastructure, absolute continuity and almost-everywhere differentiation on nonnegative time, plus elementary algebra of service rates and the cycle scaling. These components can be reused in later fluid-network missions. Contributions that preserve the source's hypotheses and boundary case are welcome.

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. DOI: 10.1287/moor.21.1.115.

Motivation

Queueing results often relate an average accumulated over customers to an average accumulated over time. In the familiar relation $L=\lambda W$, the long-run average number in a system equals the arrival rate times the average time spent there. Glynn and Whitt study a broader relation, $H=\lambda G$, that can represent queue lengths and waiting times but also costs, work, and other cumulative inputs. Their framework is deterministic: a stochastic model may supply a sample path, yet the central comparison is a statement about functions on that path. This lets the same theorem apply to different queueing models without choosing a probability law for each one. Glynn and Whitt (1989)

The paper asks for more than the usual forward implication from a customer average to a time average. Its main theorem identifies conditions under which either average has a finite limit exactly when the other does. It also compares lim inf and lim sup when ordinary limits fail to exist. Both questions matter when sample paths fluctuate: convergence of one average cannot simply be inferred from a visual similarity between the two ways of indexing the input. Glynn and Whitt (1989), §§1–2

Setting

A cumulative input is a real-valued function $F(s,t)$ on $[0,\infty)\times[0,\infty)$, nondecreasing separately in the customer coordinate $s$ and the time coordinate $t$. Its marginal limits $F(s,\infty)$ and $F(\infty,t)$ are finite for every fixed argument. The first counts all eventual input associated with customers through index $s$; the second counts all input accumulated through time $t$. The marginal averages are

$$G(s)=\frac{F(s,\infty)}{s},\qquad H(t)=\frac{F(\infty,t)}{t}.$$

The paper permits cumulative inputs that are not distribution functions of measures on rectangles. In particular, it does not require a rectangle-increment inequality or nonnegative values of $F$. The finite marginal limits and monotonicity are the actual assumptions of its general framework. Glynn and Whitt (1989), p. 635, (1)

A time change $T_i(s)$, for $i=1,2$, is finite, nonnegative, nondecreasing, and right-continuous, and tends to infinity with $s$. Its right-continuous inverse is $S_i(t)=\inf\{s\geq0:T_i(s)>t\}$. The two time changes may differ. Both have the same asymptotic rate $T_i(s)/s\to\lambda^{-1}$ for a positive finite $\lambda$. The paper's two approximation conditions are

$$\frac{F(s,T_1(s-))-F(\infty,T_1(s-))}{s}\longrightarrow0 \quad(14), \qquad \frac{F(s,\infty)-F(s,T_2(s))}{s}\longrightarrow0 \quad(15),$$

as $s\to\infty$, where $T_1(s-)$ is the left limit. Condition (14) concerns input already present by a left-limit time; condition (15) concerns input not yet present by a right-limit time. Glynn and Whitt (1989), p. 638, (3), (14)–(15)

Formalization targets

One-sided asymptotic bounds

With only (14) and the rate for $T_1$, the corrected upper bounds are

$$\liminf H\leq\liminf \lambda G,\qquad \limsup H\leq\limsup \lambda G.$$

With only (15) and the rate for $T_2$, the corrected lower bounds reverse both inequalities. The two bounds remain useful separately when only one approximation condition holds. Their lim inf and lim sup may be infinite. Glynn and Whitt (1989), p. 639, Theorem 1(a)–(b) and Remark 2

Equality of asymptotic bounds and finite limits

Under both conditions, Theorem 1(c) asserts equality of the respective lim inf and lim sup. The mission goal is Theorem 1(f): for finite real limits,

$$H(t)\to h\quad\Longleftrightarrow\quad G(s)\to g, \qquad\text{and whenever these limits exist, }h=\lambda g.$$

Here the equivalence means existence of finite limits, with the second clause identifying their values. The lim inf and lim sup statement is retained as a milestone because it also covers nonconvergent paths. Glynn and Whitt (1989), p. 639, Theorem 1(c), (f)

Significance

The goal gives a two-way transfer between customer-indexed and time-indexed long-run averages. If an application establishes one finite average, the theorem supplies the other and fixes its value. The one-sided milestones give meaningful bounds when only one approximation condition is available; the lim inf and lim sup milestone retains information when neither average converges. These outcomes are stated for a general cumulative input, so applications can supply their own $F$, $T_1$, and $T_2$ without changing the theorem. Glynn and Whitt (1989), §§2–4

The paper proves these results on paper. The formalization target is a machine-checked interface for the paper's deterministic framework, its inversion lemmas, its asymptotic inequalities, and the two-way limit theorem. At this drafting stage the Lean theorem statements compile with proof placeholders; no machine-checked proofs of these new statements are claimed. The definitions and inverse-rate lemma can be reused in other sample-path results.

Difficulty

The two marginal averages examine different slices of $F$, and a time change may jump or have flat intervals. A direct substitution of $t=T_i(s)$ does not give an equality between $F(s,\infty)$ and $F(\infty,t)$ under the paper's assumptions. The left limit in (14) and the value in (15) also behave differently at jumps. The inverse $S_i$ connects the coordinates, but its boundary behavior and rate must be handled before comparing the averages. These issues are present even without stochastic randomness. Glynn and Whitt (1989), pp. 638–639

Formalization scope

Lean represents $s,t$ by nonnegative real numbers and $F$ by a real-valued function with separate monotonicity and bounded marginal ranges. Real suprema represent $F(s,\infty)$ and $F(\infty,t)$; the boundedness fields ensure those suprema are the paper's finite limits. The inverse is an infimum of a nonempty set because $T_i\to\infty$. The left limit is the supremum over earlier nonnegative arguments, with $T(0-)=0$. Ratios at zero use Lean's total division convention, but every ratio assertion is asymptotic at infinity.

Lim inf and lim sup are taken in the extended reals so an unbounded average retains an infinite limit. Multiplication by $\lambda$ happens in the reals before conversion. Ordinary limits in Theorem 1(f) are finite real limits. The two time changes are independent and share only the positive rate $\lambda$. The goal assumes only (14), (15), and the stated time-change rates; it does not assume its own inverse-rate or asymptotic conclusions. No nonnegativity or rectangle inequality is imposed on $F$.

Theorem 1(a) and (b) have their hypothesis pairing reversed in print. The formalized one-sided bounds use the corrected pairing, and the milestone text preserves the printed source for audit. The intermediate expressions involving $G(S_i(t))$ are excluded from the corrected statements because the framework does not assume customer-coordinate right continuity. Theorem 1(c) and (f) use both conditions and are true as printed. The scope includes the definitions, Lemmas 1–2, corrected parts (a)–(b), and parts (c) and (f). Contributions toward their proofs and reusable time-change lemmas are welcome. Glynn and Whitt (1989), p. 639, Theorem 1

Selected references

• P. W. Glynn and W. Whitt, Extensions of the Queueing Relations L = λW and H = λG, Operations Research 37(4):634–644, 1989. DOI: 10.1287/opre.37.4.634

Motivation

Little's law $L = \lambda W$ says that the long-run average number of customers in a system equals the arrival rate times the average time a customer spends there. It is one of the most used identities in queueing theory, and it holds on individual sample paths under weak conditions (Little 1961; Stidham 1974). Many quantities of interest are not head counts, however: the work in the system, the cost accumulated by customers in progress, the number of tokens a customer holds in some state. For these a more general relation is needed, between a time average $H$ and a customer average $G$, of the form $H = \lambda G$.

Heyman and Stidham (Oper. Res. 28 (1980)) prove such a relation on each sample path, for an arbitrary real-valued function attached to each customer, under a support condition that is much weaker than the continuous-sojourn assumption of the $L = \lambda W$ theorem. They then show by a counterexample that the support condition cannot simply be dropped, even when every customer function is an indicator.

Timeline.

• 1961: Little proves $L = \lambda W$ under stationarity assumptions (Little 1961).
• 1971: Brumelle proves $H = \lambda G$ under conditions (v.a), (v.b) on the tails of the $f_n$ (J. Appl. Prob. 8, 508–520).
• 1972: Stidham gives a new proof of $L = \lambda W$, including the lemma relating $N(t)/t$ and $t_n/n$ (Stidham 1972).
• 1974: Stidham proves $L = \lambda W$ on each sample path, assuming each sojourn is one uninterrupted interval (Stidham 1974).
• 1980: Heyman and Stidham prove $H = \lambda G$ on every sample path under the support condition below, and give the counterexample. The paper notes that its Theorem 1 is weaker than the sample-path version of Brumelle's theorem, with hypotheses stated directly on the sample path.

Setting

Fix one sample path. Customers $n = 1, 2, \ldots$ arrive at epochs $0 \le t_1 \le t_2 \le \cdots$; ties are allowed. The arrival count $N(t)$ is the number of $n$ with $t_n \le t$, and the arrival rate is $\lambda = \lim_{t\to\infty} N(t)/t$ when the limit exists.

Customer $n$ carries a real-valued function $f_n$ on $[0,\infty)$. Its total is $g_n = \int_0^\infty f_n(t)\,dt$, and the rate is $h(t) = \sum_{n=1}^\infty f_n(t)$. The customer average and time average are

$$G = \lim_{N\to\infty} \frac1N \sum_{n=1}^N g_n, \qquad H = \lim_{T\to\infty} \frac1T \int_0^T h(t)\,dt .$$

When $f_n$ is the indicator of $[t_n, t_n + W_n)$, $g_n = W_n$ is the sojourn time and $h(t)$ is the number in system, so $H = \lambda G$ is $L = \lambda W$.

The ASSUMPTION of the paper is that for each $n$ there is $s_n \in [0,\infty)$ with

1. (i) $f_n(t) = 0$ for $t \notin [t_n, t_n + s_n]$;
2. (ii) $s_n / n \to 0$.

For signed $f_n$ write $f_n^+ = \max[0, f_n]$, $f_n^- = \max[0, -f_n]$, and let $g_n^\pm$, $h^\pm$, $G^\pm$, $H^\pm$ be the corresponding totals, rates and averages.

Formalization targets

Goal: Theorem 2 (p. 986)

Assume (i), (ii) and (v) $\int_0^\infty |f_n(t)|\,dt < \infty$ for every $n$. If $\lambda$, $G^+$ and $G^-$ exist with $0 < \lambda < \infty$ and $G^\pm < \infty$, then $G$ exists, equals $G^+ - G^-$, $H$ exists, and

$$H = \lambda G. \tag{1}$$

Milestones

• (2): for $0 < \lambda < \infty$, $N(t)/t \to \lambda$ if and only if $t_n / n \to \lambda^{-1}$.
• (3): for $f_n \ge 0$, $V(T) \le \int_0^T h(t)\,dt \le U(T)$, where $U(T)$ sums $g_n$ over arrived customers and $V(T)$ over customers with $t_n + s_n \le T$.
• (4): $\lambda G = \lim_{t\to\infty} U(t)/t$.
• $s_n / t_n \to 0$, and $\lim U(t)/t = \lim V(t)/t$.
• Theorem 1 (p. 985): for $f_n \ge 0$ under (i)–(iv), $H = \lambda G$.
• The identity $\int_0^T h^+ - \int_0^T h^- = \int_0^T h$ and (6): $G = G^+ - G^-$, $H = H^+ - H^-$.

Companion results

• The §3 counterexample: $t_n = n$, indicator $f_n$ with $g_n = 1$, so $\lambda = G = 1$, but $H = \log 2$; its support span $s_n = n$ satisfies (i) and fails (ii).
• Corollary 3 (p. 988): if $\lambda(\omega) = \lambda$ is constant, the ensemble averages satisfy $\int H\,dP = \lambda \int G\,dP$.
• $G = W < \infty$ implies $W_n / n \to 0$ (p. 986), the step by which Theorem 1 contains $L = \lambda W$.

Significance

The result. $H = \lambda G$ converts between a time average, which is what a system designer measures, and a customer average, which is what a customer experiences. Applied to different $f_n$ it yields $L = \lambda W$, the relation between average work in system and average customer work, and relations between time-stationary and embedded-chain probabilities; §2 of the paper derives the GI/M/c/K relation this way. Because the support condition (i)–(ii) allows a customer's contribution to be interrupted (leaving and re-entering the system), it covers preemptive priority queues and nodes of networks, which the continuous-sojourn $L = \lambda W$ theorem does not. The counterexample marks the boundary: with interrupted sojourns, indicator functions and finite $\lambda$, $G$ alone do not suffice.

Formalizing it. The result is proved on paper, with two steps delegated to earlier work "by mimicking" Lemma 1 and Theorem 2 of Stidham 1974. The indicator special case $L = \lambda W$ (with strictly increasing arrivals) is already proved on Prove2Me as queueing_general_littles_law (wenxinzhang). This mission asks for the general, signed, pathwise statement and its proof steps, a counterexample with an exactly computed time average $\log 2$, and the ensemble corollary.

Difficulty

The obvious argument, exchanging the time integral of $h$ with the sum over customers, gives $\int_0^T h = \sum_n \int_0^T f_n$, but a customer that has arrived by $T$ may contribute only part of its total $g_n$ by $T$. The sandwich $V(T) \le \int_0^T h \le U(T)$ only bounds this loss; the hard step is showing that $U(t)/t$ and $V(t)/t$ have the same limit, which needs $s_n / t_n \to 0$ to compare $V$ at time $t$ with $U$ at a slightly earlier time. Without (ii) this fails, as the counterexample shows: customers there remain "open" for a window proportional to their index.

For signed $f_n$ the sandwich is not available directly, and the proof splits $f_n$ into positive and negative parts; the exchange of sum and integral then needs the finiteness of the parts on every $[0,T]$.

Formalization scope

All statements except Corollary 3 are about one fixed sample path; the paper's "with probability one" is the pathwise statement applied to almost every path, and Corollary 3 states this explicitly with a probability measure and almost-sure hypotheses.

Conventions:

• Customers are indexed from $0$ in Lean; index $n$ is the paper's customer $n+1$, so $s_n/n \to 0$ is written $s_n/(n+1) \to 0$.
• Arrival epochs are Monotone with $t_0 \ge 0$; ties are allowed.
• $f_n : \mathbb R \to \mathbb R$, but only values on $[0,\infty)$ enter: (i) is required only for $t \ge 0$, $g_n$ integrates over $[0,\infty)$, and time averages integrate over $[0,T]$.
• (iv) and (v) are stated as integrability of $f_n$ on $[0,\infty)$; the page prints (iv) as "$\le \infty$", a misprint for "$< \infty$".
• $N(t)$ is the cardinality of $\{n : t_n \le t\}$; $h$, $U$, $V$ are infinite sums over all customers.
• "$H$ exists" includes integrability of $h$ on every $[0,T]$.
• The page prints (6) as "$G = G^+ - G^+$"; the stated identity is $G = G^+ - G^-$, as the proof shows.

Added hypotheses: milestones (3), the $h^\pm$ identity and (6) assume $t_n \to \infty$, which the paper derives from (2); Corollary 3 assumes $G(\omega)$ is integrable, which its definition of the ensemble average presupposes.

A formalization in which $h$ sums only over arrived customers, or in which a non-integrable $h$ or $f_n$ has integral $0$, would make the statements trivial or different; the definitions rule this out by summing over all customers and requiring integrability.

Needed infrastructure: Cesàro averages and counting functions of nondecreasing sequences, interchange of countable sums and integrals for locally finite families, and harmonic sums $\sum_{m=\lceil (k+1)/2\rceil}^{k} 1/m \to \log 2$. The counting-function lemma (2) and the squeeze for $U$ and $V$ are reusable well beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• D. P. Heyman and S. Stidham, Jr., The relation between customer and time averages in queues, Operations Research 28(4):983–994, 1980. https://doi.org/10.1287/opre.28.4.983
• J. D. C. Little, A proof for the queuing formula: L = λW, Operations Research 9(3):383–387, 1961. https://doi.org/10.1287/opre.9.3.383
• S. Stidham, Jr., L = λW: a discounted analogue and a new proof, Operations Research 20(6):1115–1126, 1972. https://doi.org/10.1287/opre.20.6.1115
• S. Stidham, Jr., A last word on L = λW, Operations Research 22(2):417–421, 1974. https://doi.org/10.1287/opre.22.2.417
• S. L. Brumelle, On the relation between customer and time averages in queues, Journal of Applied Probability 8:508–520, 1971.

Motivation

A loss network is a model of a circuit-switched network: telephone networks, and more generally any system in which a request seizes several resources at once and is lost if any of them is unavailable. Exact loss probabilities in such networks are given by a product-form distribution over a state space whose size grows exponentially with the number of routes, so practitioners compute an approximation instead: the Erlang fixed point, also called the reduced-load approximation. It pretends that links block independently, computes the traffic offered to each link after thinning by the other links, and applies Erlang's single-link formula link by link. Reduced-load approximations of this kind recur throughout §§3–4 of Kelly 1991, where they appear as limits of networks with fixed and with alternative routing.

An approximation defined by a fixed point equation raises an immediate question: does the equation have exactly one solution? Under fixed routing it does, and Kelly's Theorem 3.7 (Ann. Appl. Probab. 1991, p. 338, citing Kelly 1986, reference [33] of the paper) proves it by identifying the fixed point with the optimum of a strictly convex program, the revised dual problem. The convex characterization is specific to fixed routing; the paper notes (p. 337) that for networks with dynamic routing and control nonuniquely determined behaviour can occur.

Setting

There are $J$ links, link $j$ having $C_j \ge 1$ circuits, and a finite set of routes $r$. A call on route $r$ uses $A_{jr} \in \mathbb Z_+$ circuits of link $j$, and calls on route $r$ arrive as a Poisson stream of rate $\nu_r > 0$.

Erlang's formula (1.1) gives the blocking probability of a single link with $C$ circuits offered Poisson traffic of intensity $\nu$:

$$E(\nu, C) = \frac{\nu^C}{C!}\Big[\sum_{n=0}^{C} \frac{\nu^n}{n!}\Big]^{-1}.$$

The Erlang fixed point equations (3.1)–(3.2) for the vector of link blocking probabilities $(E_1, \dots, E_J)$ are

$$E_j = E(\rho_j, C_j), \qquad \rho_j = (1 - E_j)^{-1} \sum_r A_{jr}\,\nu_r \prod_i (1 - E_i)^{A_{ir}}, \qquad j = 1, \dots, J.$$

The utilization function $U(y, C)$ is defined by the implicit relation (3.4),

$$U\big(-\log(1 - E(\nu, C)),\, C\big) = \nu\,\big(1 - E(\nu, C)\big), \qquad \nu \ge 0:$$

the mean number of busy circuits on a single link whose blocking probability is $1 - e^{-y}$.

The revised dual problem (3.5) is

$$\text{minimize} \quad \sum_r \nu_r \exp\Big(-\sum_j y_j A_{jr}\Big) + \sum_j \int_0^{y_j} U(z, C_j)\,dz \qquad \text{subject to } y \ge 0,$$

and its stationarity conditions (3.6) are

$$\sum_r A_{jr}\,\nu_r \exp\Big(-\sum_i y_i A_{ir}\Big) = U(y_j, C_j), \qquad j = 1, \dots, J.$$

The revised dual differs from the dual problem (2.3) of §2, whose optimum gives the limiting blocking probabilities of a large network, only in its last term: $\sum_j y_j C_j$ becomes $\sum_j \int_0^{y_j} U(z, C_j)\,dz$.

Formalization targets

Goal: Theorem 3.7

The revised dual problem (3.5) has an optimum $y$, every optimum equals $y$, and

$$E \in [0,1]^J \text{ solves (3.1)–(3.2)} \iff E_j = 1 - \exp(-y_j) \text{ for every } j.$$

The goal states the characterization, not only the existence and uniqueness of the fixed point: the solution is $1 - e^{-y}$ for the optimum $y$ of (3.5).

Milestones (p. 338, in the order the argument uses them)

1. (3.4) defines a function: $\nu \mapsto -\log(1 - E(\nu, C))$ is a continuous strictly increasing bijection of $[0,\infty)$ onto itself for $C \ge 1$, $U$ satisfies (3.4), and $U \ge 0$.
2. $y \mapsto U(y, C)$ is strictly increasing on $[0, \infty)$.
3. $y \mapsto \int_0^y U(z, C)\,dz$ is strictly convex, and so is the objective of (3.5) on $y \ge 0$.
4. (3.5) has exactly one optimum.
5. A vector $y \ge 0$ is optimal for (3.5) if and only if it satisfies (3.6).
6. A solution of (3.1)–(3.2) in $[0,1]^J$ has all $E_j < 1$; and for $y \ge 0$, $E_j = 1 - e^{-y_j}$ solves (3.1)–(3.2) if and only if $y$ satisfies (3.6).

Significance

The theorem turns a nonlinear system of $J$ equations into a smooth strictly convex minimization over the nonnegative orthant. Uniqueness of the fixed point follows at once, and the program gives a computational handle: any convex-minimization method computes the Erlang fixed point, without relying on the convergence of repeated substitution. The comparison with the dual problem (2.3) also explains the approximation: (3.6) relaxes the conditions (2.7), which force a link's carried traffic to equal its capacity before it can block, into a smooth relation in which blocking grows with carried traffic as Erlang's formula prescribes (Remark 3.8).

On Prove2Me, existence and uniqueness of the fixed point alone is already the Proved theorem KellyStochasticNetworks.erlang_fixed_point_unique (Kelly–Yudovina, Stochastic Networks, Theorem 3.20), referenced by this mission. Also referenced: KellyStochasticNetworks.erlang_strictMono (Proved: $\nu \mapsto E(\nu, C)$ and $\nu \mapsto \nu(1 - E(\nu, C))$ are strictly increasing for $C \ge 1$) and KellyStochasticNetworks.erlang_mean_busy_circuits (Proved: the mean number of busy circuits is $\nu(1 - E(\nu, C))$, the reading of $U$ as a utilization). What this mission adds is the revised dual problem itself, the utilization function $U$, and the identification of the fixed point with the optimum of (3.5); none of these is formalized on the platform.

Difficulty

The function $U$ is defined only implicitly, through the inverse of $\nu \mapsto -\log(1 - E(\nu, C))$, so every property of the objective of (3.5) passes through properties of Erlang's formula: monotonicity, continuity, and the limit $E(\nu, C) \to 1$ as $\nu \to \infty$. Differentiating $\int_0^{y} U$ needs continuity of $U$, which must be derived from the inverse.

The paper's sentence "strictly convex: it thus has a unique minimum" covers only uniqueness. Existence of a minimizer on the unbounded set $y \ge 0$ is a separate fact, a growth estimate for the integral terms, and it is part of milestone 4. The first term of (3.5) is not strictly convex when $A$ has rank less than $J$, so strict convexity must come from the separable integral terms. Finally, optimality over $y \ge 0$ yields only one-sided conditions at coordinates with $y_j = 0$; that (3.6) is an equality there uses $U(0, C) = 0$.

Formalization scope

Lean namespace KellyLossNetworks.RevisedDual. Links are Fin J, routes Fin R, the incidence matrix is A : Fin J → Fin R → ℕ, rates ν : Fin R → ℝ, capacities C : Fin J → ℕ, following the published Kelly–Yudovina definitions. Every statement assumes $\nu_r > 0$ and $C_j \ge 1$; the paper uses both without stating them, and a link with $C_j = 0$ makes (3.4) meaningless, since $E(\nu, 0) = 1$.

Erlang's formula is the published KellyStochasticNetworks.erlang and the fixed point equations (3.1)–(3.2) are the published KellyStochasticNetworks.ErlangFixedPoint, whose factor $(1 - E_j)^{-1}$ is Lean's total inverse; milestone 6 shows that no solution in $[0,1]^J$ reaches $E_j = 1$. Solutions are sought in $[0,1]^J$, as on p. 338.

$U$ is defined by choice: $U(y, C) = \nu(1 - E(\nu, C))$ for a $\nu \ge 0$ with $-\log(1 - E(\nu, C)) = y$, and $0$ if none exists. For $C \ge 1$, $y \ge 0$ the $\nu$ is unique, and that (3.4) holds is milestone 1, a theorem, not an axiom built into the definition. Values at $y < 0$ or $C = 0$ are placeholders that no statement uses. The integral in (3.5) is the interval integral $\int_0^{y_j}$. An optimum of (3.5) is a $y \ge 0$ whose objective value is at most that of every $z \ge 0$.

A trivializing formalization is ruled out: replacing $U$ by any closed form other than the one fixed by (3.4) (for instance $U(z, C) = C$, the fluid utilization of Remark 3.8) would change the problem and reduce (3.5) to the dual (2.3); and the goal asserts the identification $E = 1 - e^{-y}$ rather than restating the existence and uniqueness that is already Proved.

A complete development needs: inverse-function arguments for a strictly increasing continuous map of $[0, \infty)$, derivatives of interval integrals with continuous integrands, strict convexity of separable sums, and first-order optimality conditions for convex functions on the nonnegative orthant. The facts about Erlang's formula and about $U$ are reusable in any reduced-load analysis. Proofs of individual milestones are welcome independently.

Selected references

• F. P. Kelly, Loss networks, The Annals of Applied Probability 1(3):319–378, 1991. https://doi.org/10.1214/aoap/1177005872
• F. P. Kelly, Blocking probabilities in large circuit-switched networks, Advances in Applied Probability 18:473–505, 1986 (reference [33] of Kelly 1991; DOI not verified offline).
• F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014 (the source of the Proved platform items referenced here; DOI not verified offline).