Stochastic Systems

Motivation

Multistage stochastic programs model decisions taken over time while uncertain data are revealed: generation scheduling in hydro-thermal power systems, capacity expansion, unit commitment, portfolio management. When the uncertainty is represented by a finite scenario tree, the problem becomes one very large deterministic program, and decomposition algorithms solve it stage by stage. For linear problems the standard methods are nested Benders decomposition and its sampling variant, stochastic dual dynamic programming (SDDP), introduced by Pereira and Pinto (1991). Both rely on the convexity of the value functions, which they approximate from below by linear cuts.

Many applications need integer decisions (on/off status of generators, investment choices), and integer variables destroy convexity. Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) observed that when the state variables passed between stages are binary, exact convex polyhedral representations still exist on the binary points. They proposed stochastic nested decomposition (SND) and its stage-wise independent special case SDDiP, and identified three properties of cuts (valid, tight, finite) under which the algorithms converge. This mission formalizes that convergence theorem, Theorem 2 of the paper.

Timeline. Birge (1985) gave nested decomposition for multistage linear programs; Pereira and Pinto (1991) introduced SDDP. Philpott and Guan (2008) proved almost sure finite convergence of SDDP-type methods for linear problems, and Girardeau, Leclère and Philpott (2015) extended convergence to convex problems. Zou, Ahmed and Sun (2019) proved finite convergence with probability one for mixed integer problems with binary states and abstract valid, tight and finite cuts, and showed that their Lagrangian cuts have the first two properties.

Setting

Let $\mathcal T$ be a scenario tree with stages $1,\dots,T$, root $1$, parent map $a(n)$ and children $\mathcal C(n)$. The nodes of the last stage are the scenarios. Node probabilities satisfy $p_n>0$, $p_1=1$, and $p_n=\sum_{m\in\mathcal C(n)}p_m$ before the last stage, and $q_{nm}=p_m/p_n$. Each node has a linear cost $f_n(x_n,y_n)$ and a nonempty compact mixed integer polyhedral set $X_n$ (assumption (A1)). The state $x_n\in\{0,1\}^d$ is binary, the local variables $y_n$ are general, and the root's parent state $\bar x_0$ is fixed. The problem in local-copy form (2.1) is

$$\min\sum_{n\in\mathcal T}p_nf_n(x_n,y_n)\quad\text{s.t.}\quad(z_n,x_n,y_n)\in X_n,\ z_n=x_{a(n)},\ x_n\in\{0,1\}^d .$$

Its value functions satisfy the recursion (2.3): $Q_n(x_{a(n)})=\min\{f_n(x_n,y_n)+\mathcal Q_n(x_n)\}$ over the nodal feasible set, with the expected cost-to-go function $\mathcal Q_n(x)=\sum_{m\in\mathcal C(n)}q_{nm}Q_m(x)$.

The SND algorithm keeps an under-approximation $\psi^i_n$ of each $\mathcal Q_n$: the maximum of a lower bound $L_n$ and the aggregated cuts $\sum_{m\in\mathcal C(n)}q_{nm}(v^\ell_m+(\pi^\ell_m)^\top x)$ collected so far (3.2). Each iteration $i$ samples $M$ scenarios with replacement. In the forward step it solves the nodal problems $P^i_n(x^i_{a(n)},\psi^i_n)$ from the root down, which yields the forward tree solution $\{(x^i_n,y^i_n)\}$ of (3.6). In the backward step, at every sampled node it generates one cut per child at the state $x^i_n$ and adds their aggregate to $\psi_n$. Cuts are valid if $Q_m(x)\ge v^i_m+(\pi^i_m)^\top x$ on $\{0,1\}^d$ (3.4). They are tight if they equal the value $\underline Q^i_m(x^i_n,\psi^{i+1}_m)$ of the child's updated nodal problem at $x^i_n$ (3.5). They are finite if only finitely many distinct cuts occur. Assumption (A3) requires the nodal solver to return the same optimal solution whenever it is given the same problem.

Formalization targets

Goal: Theorem 2 (p. 474)

With sampling with replacement, valid, tight and finite cuts, and a solver satisfying (A3), the following holds with probability one:

$$\exists\, i_0\ \ \forall i\ge i_0:\quad \{(x^i_n,y^i_n)\}_{n\in\mathcal T}\ \text{is an optimal solution of (2.1)}.$$

Milestones, in the order the proof uses them

1. Valid cuts give under-approximations, $\psi^i_n\le\mathcal Q_n$ and $\underline Q^i_n\le Q_n$ (proof of Claim 1, p. 475).
2. Claim 1: if $\psi^i_n(x^i_n)=\mathcal Q_n(x^i_n)$ for all $n$, the forward solution is optimal for (2.1) (p. 475).
3. With finitely many possible cuts, the approximations $\{\psi^i_n\}$ change only in finitely many iterations (pp. 474–475).
4. (3.8a)–(3.8f): a sampled node whose children are exact becomes exact after its backward step (p. 476).
5. Under sampling with replacement, every scenario is sampled in infinitely many iterations, almost surely (p. 476).
6. Claim 2: almost surely, no infinite block of unchanged approximations has a non-optimal forward solution (p. 475).

Significance

Theorem 2 separates the convergence of nested decomposition from the choice of cuts. Any cut family with the three properties yields an exact algorithm for multistage stochastic integer programs with binary states. The paper verifies the properties for integer optimality cuts and, through its Theorem 3, shows that Lagrangian cuts from the local-copy reformulation are valid and tight. The convergence of SDDiP, the variant used in computations, follows from the same theorem, and binary expansion of general integer states extends the reach to mixed integer state spaces.

The result is proved in the paper; no machine-checked proof exists. A formal development would turn its informal points into checked statements: that the minima are attained, that the DP recursion is equivalent to the extensive form, and that the finiteness of cuts is global. It would also supply a reusable framework (scenario trees with node probabilities, cut-based approximations, sampled runs) for the convergence theory of SDDP-type methods.

Difficulty

No single step is deep; the difficulty is the interaction of the pieces. A tempting argument says the approximations stop changing, so the algorithm stops at an optimum. But a stalled run need not be optimal: if a node at which $\psi_n$ is inexact is never sampled again, nothing changes and the forward solution stays suboptimal. The proof must therefore combine three things: the deterministic finiteness of changes, an almost sure statement about sampling, and the exactness chain (3.8). That chain depends on tightness with respect to the updated approximation of the child, and it fails if tightness refers to the approximation from before the backward step. The equivalence between optimality for the DP recursion and for the extensive form (2.1), used without proof in Claim 1, also requires a backward induction over the tree.

Formalization scope

The tree is the platform definition StochasticProg.Multistage.Tree H, with stage $t$ of the paper equal to stage = t − 1. Binary vectors are Fin d → Bool, embedded in $\mathbb R^d$. The copy variable $z_n$ is eliminated through $z_n=x_{a(n)}$. Minima are written as infima over sets that the standing assumptions make nonempty, bounded below and attained. Lean iterations are numbered from $0$, and the run is infinite (stopping criteria and bounds play no role).

Readings of informal words. "Optimal solution of (2.1)" means a feasible tree solution of least cost $\sum_np_nf_n$ among all feasible tree solutions. "After a finite number of iterations" means from some iteration on, in every iteration (∀ᶠ i in atTop). "With probability one" refers to a probability space carrying independent draws, $M\ge1$ per iteration, each with law $\{p_n:n\in S_T\}$. "Finite" cuts means one finite set for the whole run, as the proof uses it, not a different finite set per iteration. (A3) means the solver is a function of the node, the parent state and the approximation, and returns an optimal solution.

Added hypotheses, which the paper uses without stating them: $p_n>0$; every nodal problem is feasible for every binary parent state, which replaces (A2) (not used by Theorem 2); and the lower bounds under-estimate, $L_n\le\mathcal Q_n$, which is Algorithm 1's "initial under-approximation".

Trivializing formalizations are ruled out: tightness refers to the child's approximation after its own update, optimality is for the true extensive form and not relative to $\psi$, and the probability statement is over independent sampling, not over a fixed sample sequence assumed to visit every scenario.

Contributions welcome: the attainment lemmas for nodal minima, the DP/extensive-form equivalence on trees, and the second Borel–Cantelli argument for repeated sampling. All of these are reusable for other SDDP-type convergence results.

Selected references

• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Math. Program. 175 (2019) 461–502. https://doi.org/10.1007/s10107-018-1249-5
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52 (1991) 359–375. https://doi.org/10.1007/BF01582895
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Oper. Res. Lett. 36 (2008) 450–455. https://doi.org/10.1016/j.orl.2008.01.013
• P. Girardeau, V. Leclère, A. B. Philpott, On the convergence of decomposition methods for multistage stochastic convex programs, Math. Oper. Res. 40 (2015) 130–145. https://doi.org/10.1287/moor.2014.0664
• J. R. Birge, Decomposition and partitioning methods for multistage stochastic linear programs, Oper. Res. 33 (1985) 989–1007. https://doi.org/10.1287/opre.33.5.989

Motivation

A data center or cloud platform routes each incoming task to one of $N$ parallel servers. Sending each task to a server with the shortest queue, the join-the-shortest-queue (JSQ) policy, minimizes waiting in a strong sense, but the dispatcher must learn all $N$ queue lengths for every arrival. The power-of-d schemes cut this communication: the dispatcher samples $d$ servers and joins the shortest of them. Mukherjee, Borst, van Leeuwaarden and Whiting ask how large $d=d(N)$ must be for the sampled scheme to perform as well as JSQ as $N\to\infty$. They answer at two scales. At the fluid scale (mission 1 of this series) $d(N)\to\infty$ suffices. At the diffusion scale of the Halfin–Whitt regime, the subject of this mission, $d(N)/(\sqrt N\log N)\to\infty$ suffices, and $d(N)/(\sqrt N\log N)\to 0$ does not.

Timeline:

• Halfin and Whitt (1981) introduced the heavy-traffic regime $(N-\lambda(N))/\sqrt N\to\beta>0$ for many-server systems.
• Eschenfeldt and Gamarnik (2018, arXiv:1502.00999) proved the diffusion limit of ordinary JSQ in this regime, the system (2.4) below.
• Mukherjee, Borst, van Leeuwaarden and Whiting (Stochastic Systems 8(4), 2018; arXiv:1612.00723v2) proved that JSQ(d(N)) has the same diffusion limit when $d(N)/(\sqrt N\log N)\to\infty$ (Theorem 2.4), and that the limit differs when $d(N)/(\sqrt N\log N)\to 0$ (Theorem 2.5).

Setting

There are $N$ servers, each with a buffer of size $b\in\{2,3,\dots\}\cup\{\infty\}$ that counts the task in service. Tasks arrive as a Poisson process of rate $\lambda(N)$, and each needs a unit-mean exponential amount of work, served at unit rate. A task sent to a full server is discarded. Under JSQ(d) the dispatcher samples $d$ servers without replacement ($1\le d\le N$) and sends the task to a server with the shortest queue among them. For $d=N$ this is JSQ.

The state is the occupancy vector $Q=(Q_1,\dots,Q_b)$, where $Q_i$ is the number of servers with at least $i$ tasks. The conventions are $Q_0=N$ and $Q_i=0$ for $i>b$. With the servers ordered by nondecreasing queue length, the $c$-th ordered server has queue length $I(c)=\max\{i\ge0:Q_i\ge N-c+1\}$. An arrival at position $c$ raises $Q_{I(c)+1}$ by one when $I(c)<b$. A departure at position $k$ lowers $Q_{I(k)}$ by one when $I(k)\ge1$. JSQ(d) routes to the smallest position in a uniform $d$-subset of $\{1,\dots,N\}$.

In the Halfin–Whitt regime $(N-\lambda(N))/\sqrt N\to\beta>0$, the diffusion-scaled state is

$$\bar Q_1=-\frac{N-Q_1}{\sqrt N},\qquad \bar Q_i=\frac{Q_i}{\sqrt N}\quad(i\ge2).$$

Here $-\bar Q_1$ is the scaled number of idle servers.

Formalization targets

Goal: Theorem 2.4 (pp. 7–8)

Let $\beta>0$, $b\ge2$ and $k\ge2$. Assume $\bar Q_{k+1}(0)=0$ for large $N$ and $(\bar Q_1(0),\dots,\bar Q_k(0))\Rightarrow\nu$. If $d(N)/(\sqrt N\log N)\to\infty$, then $\bar Q^{d(N)}\Rightarrow\bar Q$ in $D_{\ell_1}[0,\infty)$, where $\bar Q_i\equiv 0$ for $i\ge k+1$ and

$$\begin{aligned}\bar Q_1(t)&=\bar Q_1(0)+\sqrt2W(t)-\beta t+\int_0^t(-\bar Q_1+\bar Q_2)\,ds-U_1(t),\\ \bar Q_2(t)&=\bar Q_2(0)+U_1(t)-\int_0^t(\bar Q_2-\bar Q_3)\,ds,\\ \bar Q_i(t)&=\bar Q_i(0)-\int_0^t(\bar Q_i-\bar Q_{i+1})\,ds,\quad 3\le i\le k.\end{aligned}$$

Here $W$ is a standard Brownian motion and $U_1$ is the nonnegative nondecreasing regulator with $\int_0^\infty\mathbb 1_{[\bar Q_1<0]}\,dU_1=0$. The goal also asserts that this solution is unique.

Milestones

1. Uniqueness clause of Theorem 2.4: (2.4), with the constraint $\bar Q_1\le0$, has at most one solution for every driving path.
2. Theorem 2.4 for $d(N)=N$: the JSQ diffusion limit of [8, Theorem 2], stated along an arbitrary sequence of server counts $N_j\to\infty$.
3. Proposition 5.1 (p. 32): if JSQ has the diffusion limit along every such sequence, then so does JSQ(d(N)) with $d(N)/(\sqrt N\log N)\to\infty$.

The goal follows from 1–3.

Significance

The result. Theorem 2.4 shows that $O(\sqrt N\log N)$ queue-length queries per arrival already achieve diffusion-level optimality: over any finite horizon only $O_P(\sqrt N)$ servers are idle and only $O_P(\sqrt N)$ hold two or more tasks, exactly as under JSQ. With Theorem 2.5 it identifies $\sqrt N\log N$ as the minimal order of $d(N)$. The diffusion limit is also the input for the steady-state analyses of JSQ in this regime (Braverman; Banerjee and Mukherjee).

Formalizing it. The result is proved on paper; nothing in it is machine-checked. A formalization needs:

• a rigorous construction of the many-server JSQ(d) process;
• the stochastic-coupling comparison of §3;
• weak convergence of $\ell_1$-valued processes;
• a reflected integral equation of Skorokhod type.

The Eschenfeldt–Gamarnik limit (milestone 2) is cited by the paper, not proved in it, so its formalization is a separate, substantial contribution.

Difficulty

JSQ(d(N)) cannot be compared with JSQ path by path. The same arrival is routed to different servers under the two schemes, so their occupancy vectors drift apart and do not stay ordered. The obvious generator-based diffusion argument for JSQ(d(N)) itself does not close either. The routing probabilities depend on the whole ordered queue-length profile through $\binom{\cdot}{d}/\binom{N}{d}$-type terms, and these do not reduce to a function of $\bar Q_1,\bar Q_2$ at scale $\sqrt N$ unless $d(N)$ is large enough.

The threshold is sharp: for $d(N)\ll\sqrt N\log N$ the limit is different (Theorem 2.5). Any argument therefore has to use the growth rate quantitatively, controlling at scale $o_P(\sqrt N)$ over a finite horizon how often JSQ(d(N)) fails to make a near-shortest choice. A qualitative fluid-type argument cannot do this. A second difficulty is the limit itself: (2.4) is a reflected equation whose regulator enters two coordinates, so even its well-posedness needs a Skorokhod-type argument with feedback.

Formalization scope

Lean conventions:

• Levels and positions use the paper's index base: Q i is $Q_i$ for $i\ge1$, with Q 0 = N, and positions are $1,\dots,N$. The initial vector Fin k → ℝ lists levels $1,\dots,k$.
• Buffer b : ℕ∞ with 2 ≤ b; ⊤ is an infinite buffer.
• Process construction is by uniformization. A Poisson clock of rate $\lambda+N$ is built from i.i.d. expMeasure (λ + N) interarrival times through the published renewalCount/partialSum. Its i.i.d. marks are arrivals, with probability $\lambda/(\lambda+N)$ and a uniform $d$-subset, or departures at a uniform position. Marks are independent of the clock and of a random initial state. The model is therefore the paper's in law. Sampling is without replacement, so JSQ(N) is JSQ.
• Path space. $D_{\mathbb S}[0,\infty)$ is read as $\ell_1$-valued càdlàg paths, as the proof controls $\ell_1$ distances. Weak convergence to the continuous limit is stated in coupling form: a common probability space with copies of the laws and almost sure uniform convergence in $\ell_1$ on compacts.
• Initial convergence is joint convergence in law of $(\bar Q_1(0),\dots,\bar Q_k(0))$, via bounded continuous test functions. The page's coordinatewise convergence does not determine the limit. The limit's initial value is independent of $W$.
• Solution concept of (2.4) includes $\bar Q_1\le0$, implicit in the paper; without it $U_1\equiv0$ satisfies the complementarity condition and uniqueness fails. $\int\mathbb 1_{[\bar Q_1<0]}dU_1=0$ is a Lebesgue–Stieltjes measure condition. $W$ is Mathlib's IsBrownianReal.
• "Same diffusion limit" in Proposition 5.1 is the paper's reduction: the JSQ result, for all server-count sequences, implies the JSQ(d(N)) result.

Trivializing formalizations are ruled out. The goal asserts the existence of the limit (Brownian motion, initial value and solution), not merely that every limit point solves (2.4). The system hypotheses are satisfiable: the mark law has total mass one, which is checked in Lean. The convergence is of the whole $\ell_1$ path, including the tail above level $k$.

Infrastructure needed and welcome:

• a library for $\ell_1$-valued càdlàg processes;
• the one-sided Skorokhod map with Lipschitz feedback, reusable for many reflected limits;
• the S-coupling of §3, posed as milestones in mission 1 of this series;
• a formal proof of the Eschenfeldt–Gamarnik JSQ limit.

Selected references

• D. Mukherjee, S. C. Borst, J. S. H. van Leeuwaarden, P. A. Whiting, Universality of power-of-d load balancing in many-server systems, Stochastic Systems 8(4), 2018. arXiv:1612.00723v2, doi:10.1287/stsy.2018.0016
• P. Eschenfeldt, D. Gamarnik, Join the shortest queue with many servers. The heavy-traffic asymptotics, Mathematics of Operations Research 43(3), 2018. arXiv:1502.00999
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 1981. doi:10.1287/opre.29.3.567
• A. Braverman, Steady-state analysis of the join-the-shortest-queue model in the Halfin–Whitt regime, Mathematics of Operations Research 45(3), 2020. arXiv:1801.05121

Motivation

An agent whose preferences change over time cannot simply optimize once: a plan that is optimal today may be abandoned tomorrow by the agent's own "future selves". This is time inconsistency, and its standard source is non-exponential discounting, studied since Strotz (1955). The usual response, going back to Strotz and made rigorous in continuous time by Ekeland and Lazrak (2006), is to look for an equilibrium strategy: a strategy from which no future self wants to deviate. In continuous time "no incentive to deviate" is encoded through a first-order condition, which Huang and Zhou call a weak equilibrium.

Björk, Khapko and Murgoci (2017, Remark 3.5) observed that this first-order condition need not express the absence of an incentive to deviate: it only says that a derivative vanishes or is nonnegative, and a stationary point need not be a maximum. Huang and Zhou (Math. Oper. Res. 46(2), 2021; read here as arXiv:1809.09243v3) introduce a strong equilibrium, which requires the agent's payoff to be no better after any short deviation, and study the two notions for continuous-time Markov chains with controlled generators. This mission formalizes their main example (Example 4.3): a concrete two-state model in which a weak equilibrium fails to be strong, so that an agent in one state strictly gains from deviating on every short interval.

Setting

The state space is $S=\{1,\dots,N\}$. A generator is a matrix $Q\in\mathbb R^{N\times N}$ whose $i$-th row $Q_i$ lies in $E_i=\{q: q_j\ge0\ (j\ne i),\ q_i=-\sum_{j\ne i}q_j\}$. Admissible rows form sets $D_i\subseteq E_i$, and the control space is $\mathcal Q=\{Q: Q_i\in D_i\ \forall i\}$. A payoff function $f(t,i,q)$ gives the payment rate at time difference $t$ in state $i$ when row $q$ is in force. The expected payoff of using $Q$ from state $i$ is

$$F(i,Q)=\mathbb E_{i,Q}\Big[\int_0^\infty f(t,X_t,Q_{X_t})\,dt\Big]=\int_0^\infty\sum_j (e^{tQ})_{ij}\,f(t,j,Q_j)\,dt .$$

The concatenation $Q\otimes_\varepsilon Q^*$ uses $Q$ on $[0,\varepsilon]$ and $Q^*$ afterwards. A generator $Q^*\in\mathcal Q$ is a weak equilibrium if $\liminf_{\varepsilon\downarrow0}[F(i,Q^*)-F(i,Q\otimes_\varepsilon Q^*)]/\varepsilon\ge0$ for all $i\in S$, $Q\in\mathcal Q$, and a strong equilibrium if for all $i,Q$ there is $\varepsilon>0$ with $F(i,Q^*)\ge F(i,Q\otimes_{\varepsilon'}Q^*)$ for every $\varepsilon'\in(0,\varepsilon]$.

The paper's first-order and second-order quantities are

$$\Gamma^{Q^*}(Q_i)=f(0,i,Q_i)+Q_i\cdot F(Q^*),\qquad \Lambda^{Q^*}(i,Q)=f_t(0,i,Q_i)+Q_i\cdot\big(2G(Q^*)+\Gamma^{Q^*}(Q)\big),$$

with $G$ the payoff computed with the time derivative $f_t$ in place of $f$.

In the two-state model of §4, $S=\{1,2\}$, $D_i=E_i$, every generator is $Q\sim(a,b)=\begin{bmatrix}-a&a\\ b&-b\end{bmatrix}$ with $a,b\ge0$, and $f(t,1,(-a,a))=\delta(t)g_1(a)$, $f(t,2,(b,-b))=\delta(t)g_2(b)$ with the pseudo-exponential discount $\delta(t)=\lambda e^{-\rho t}+(1-\lambda)e^{-\rho't}$. Example 4.3 takes $\lambda=\tfrac12$, $\rho=1$, $\rho'=2$, $g_1(a)=-a^2$, and $g_2(b)=\tfrac{193}{144}+\tfrac56b$ for $b<\tfrac7{12}$, $g_2(b)=2-(1-b)^2$ for $b\ge\tfrac7{12}$.

Formalization targets

Goal: Example 4.3

$$Q^*\sim\Big(\frac5{12},\frac7{12}\Big)\ \text{is a weak equilibrium and not a strong equilibrium.}$$

The statement is fully explicit and has no hypotheses.

Milestones

1. (4.3)–(4.4): closed forms of $F_1-F_2$ and $G_1-G_2$ for $Q\sim(a,b)$ under pseudo-exponential discounting.
2. (4.5), (4.6), (4.8): $\Gamma^{Q^*}(Q_1)$, $\Gamma^{Q^*}(Q_2)$ and $\Lambda^{Q^*}(2,Q)$ in the two-state model.
3. Theorem 3.1: under (2.3) and (3.3), $Q^*$ is weak iff $\Gamma^{Q^*}(Q^*_i)\ge\Gamma^{Q^*}(Q_i)$ for all $(i,Q)$.
4. (4.11): at $Q^*$, $\Gamma_1$ is maximized uniquely at $a^*$ and $\operatorname{arg\,max}_{b\ge0}\Gamma_2(b)=[0,7/12]$.
5. Proposition 3.3: the second-order test on the set $R$ of equality cases.
6. (4.12): $\Lambda_2(a^*,b)=-b/12-579/288$ on $[0,7/12]$, so $\Lambda_2(a^*,b^*)<\Lambda_2(a^*,b)$ for $b\in[0,7/12)$.

Further statements

Remark 4.1: for $Q\sim(5/12,b)$, $b\in[0,7/12)$, $F(2,Q^*)<F(2,Q\otimes_\varepsilon Q^*)$ for all small $\varepsilon>0$. And (4.13): the equation $\tfrac56\le2a=\tfrac12(\tfrac1{1+a}+\tfrac1{2+a})(a^2+\tfrac{193}{144})$ has a unique solution $\bar a\ge0$, and $\bar Q^*\sim(\bar a,0)$ is a strong equilibrium.

Significance

The example shows that the weak equilibrium concept, the standard one in the time-inconsistency literature since Ekeland and Lazrak, admits strategies that an agent would abandon: Remark 4.1 exhibits a deviation that strictly increases the payoff on every short interval. Together with (4.13), it shows that in one and the same model a weak-but-not-strong equilibrium and a strong equilibrium coexist, so the choice of equilibrium concept changes which strategies are predicted. The example is the paper's justification for introducing strong equilibria.

The result is proved in the paper, through the first-order characterization (Theorem 3.1), the second-order test (Proposition 3.3, resting on the second-order expansion Lemma 3.2) and explicit computations in the two-state model. None of it has been machine-checked. A formal proof would provide checked versions of Theorem 3.1 and Proposition 3.3 for finite-state chains, reusable for any other example, and an independent check of the arithmetic of Example 4.3, where the source contains at least one misprinted formula.

Difficulty

Both conjuncts of the goal concern the small-$\varepsilon$ behaviour of $F(2,Q\otimes_\varepsilon Q^*)$, an integral of products of matrix exponentials. Weakness reduces to a first-order comparison by Theorem 3.1, but its proof needs the expansion (3.6) with an $o(\varepsilon)$ remainder controlled uniformly enough to pass under the integral over $[0,\infty)$. Failure of strong equilibrium cannot be read off the first-order term: at $b^*=7/12$ the maximizer of $\Gamma_2$ is not unique, every $b\in[0,7/12)$ ties at first order, and the decision moves to the second-order coefficient $\Lambda$ of Lemma 3.2, whose derivation needs a second-order expansion of the concatenated payoff. The regularity hypotheses of Lemma 3.2 and of (3.3) must also be verified for the example's discount function.

Formalization scope

States are Fin N; the paper's state $k$ is index $k-1$, so in the two-state model state 1 is 0 : Fin 2 and state 2 is 1 : Fin 2. Expectations are written through the transition matrices $e^{tQ}$ (NormedSpace.exp (t • Q)) and Fubini, exactly as the paper computes on p. 23; no Markov process is constructed. Payoffs are Bochner integrals over $(0,\infty)$. The weak-equilibrium condition is written as "for every $\eta>0$, eventually as $\varepsilon\downarrow0$ the quotient is $\ge-\eta$", which is $\liminf\ge0$ without a real-valued liminf. The norm in (2.3) is the sup norm, equivalent to the paper's Euclidean norm because (2.3) quantifies over every $c>0$.

Standing assumptions: $D_i\subseteq E_i$, continuity of $f$ in $t$ (2.2) and the integrability condition (2.3). Theorem 3.1 adds the shift bound (3.3)–(3.5); Proposition 3.3 assumes the conditions of Lemma 3.2, with the derivative $f_t$ tied to $f$. The closed forms (4.3)–(4.4) assume $\rho,\rho'>0$ (the page allows $\rho,\rho'\ge0$, but with a zero rate the payoff integral diverges); the algebraic identities (4.5)–(4.8) keep the page's $\rho,\rho'\ge0$; Example 4.3 has $\rho=1$, $\rho'=2$. Statement (4.11) gives $\Gamma_2(b)=g_2(b)-\tfrac56b$ and the argmax; the page's case formula for $b\ge7/12$ contains a misprint and is not used.

No trivializing reading is available: the goal has no hypotheses, $F$ is built from $e^{tQ}$ and the concatenation uses $Q$ before and $Q^*$ after $\varepsilon$, so neither conjunct holds by a junk value. Integrability of every payoff follows from (2.3) and is never assumed.

Theorem 3.1 and the second-order package are also drafted in the companion mission on existence of equilibria; they are restated here in the sub-namespace StrongWeakEq.TwoState. The goal needs the verification of (2.3), (3.3) and the Lemma 3.2 conditions for the example (convexity of $\delta$ gives (3.15)), the closed forms of $e^{tQ}$ for two-state generators, and the expansions of the paper. Contributions of proofs of the general results (Theorem 3.1, Proposition 3.3) are welcome independently of the example.

Selected references

• Y.-J. Huang and Z. Zhou, Strong and Weak Equilibria for Time-Inconsistent Stochastic Control in Continuous Time, Math. Oper. Res. 46(2), 2021; arXiv:1809.09243v3. https://arxiv.org/abs/1809.09243, https://doi.org/10.1287/moor.2020.1066
• I. Ekeland and A. Lazrak, Being serious about non-commitment: subgame perfect equilibrium in continuous time, 2006. https://arxiv.org/abs/math/0604264
• T. Björk, M. Khapko and A. Murgoci, On time-inconsistent stochastic control in continuous time, Finance Stoch. 21 (2017), pp. 331–360.
• R. H. Strotz, Myopia and inconsistency in dynamic utility maximization, Rev. Econ. Stud. 23 (1955), pp. 165–180.

Motivation

A decision maker is time-inconsistent when the plan that is optimal today stops being optimal tomorrow. The standard source is non-exponential discounting: a reward $t$ units of time ahead is weighted by $\delta(t)$, and unless $\delta$ is exponential the relative weight of two future dates changes as time passes. Hyperbolic and pseudo-exponential discount functions, which fit experimental and group-decision data better than exponential ones, all have this property. For such an agent "optimal control" is not a meaningful target, and the literature instead looks for equilibrium policies: plans that no current self wants to deviate from, given that all future selves follow the plan.

In discrete time the definition is unambiguous: a policy is an equilibrium if deviating at the current step alone does not help. In continuous time there is no "current step", and the usual definition, due to Ekeland and Lazrak (2006), compares the payoff of the plan with that of a deviation on a short interval $[0,\varepsilon]$ through a first-order condition as $\varepsilon\downarrow0$. Huang and Zhou (arXiv:1809.09243, Math. Oper. Res. 2021) call this a weak equilibrium, introduce a strong equilibrium that requires the deviation to be unprofitable for every small $\varepsilon$, and study both for a controlled finite-state Markov chain.

A natural question is whether continuous-time equilibria are the limits of the discrete-time ones as the time step shrinks. This mission formalizes the paper's answer (§5.1): limits of discrete equilibria are always weak equilibria. The paper's Example 5.1 shows they need not be strong.

Setting

The state space is $S=\{1,\dots,N\}$. A continuous-time Markov chain on $S$ is controlled through its generator $Q=(q_{ij})$: in state $i$ the row $Q_i$ is chosen from an admissible set $D_i\subseteq E_i=\{q: q_j\ge0\ (j\ne i),\ q_i=-\sum_{j\ne i}q_j\}$, and the control space is $\mathcal Q=\{Q: Q_i\in D_i\ \forall i\}$. A payoff function $f(t,i,q)$ gives the reward at time-distance $t$ from now, in state $i$, under row $q$. The standing assumptions are continuity of $t\mapsto f(t,i,q)$ on $[0,\infty)$ and, for each $c>0$, integrability over $[0,\infty)$ of $\sup_{i,\,q\in D_i,\,\|q\|\le c}|f(t,i,q)|$ (condition (2.3)). The expected payoff from state $i$ is

$$F(i,Q)=\mathbb E_{i,Q}\Big[\int_0^\infty f(t,X_t,Q_{X_t})\,dt\Big]=\int_0^\infty\sum_j(e^{tQ})_{ij}f(t,j,Q_j)\,dt,$$

and $F(Q)=(F(1,Q),\dots,F(N,Q))$. With $Q\otimes_\varepsilon Q^*$ the generator that uses $Q$ on $[0,\varepsilon]$ and $Q^*$ afterwards, $Q^*\in\mathcal Q$ is a weak equilibrium if $\liminf_{\varepsilon\downarrow0}\big(F(i,Q^*)-F(i,Q\otimes_\varepsilon Q^*)\big)/\varepsilon\ge0$ for all $i$ and $Q\in\mathcal Q$. The first-order quantity is $\Gamma^{Q^*}(q)=f(0,i,q)+q\cdot F(Q^*)$.

Discretization. Fix a mesh $\delta_n>0$. A transition matrix $u$ (rows in the probability simplex $\mathfrak P$) has generator $Q^{u,n}=(u-I)/\delta_n$, the admissible matrices are $\mathcal A^n=\{u: Q^{u,n}\in\mathcal Q\}$, and the discrete payoff is $\kappa^n(k,i,\alpha)=f\big(k\delta_n,i,(\alpha-e_i)/\delta_n\big)\,\delta_n$. The discrete value is $V^n(i,u)=\mathbb E_{i,u}\big[\sum_{k\ge0}\kappa^n(k,X_k,u_{X_k})\big]$, and $u^n\in\mathcal A^n$ is a discrete equilibrium if $V^n(i,u^n)\ge V^n(i,u\otimes_1u^n)$ for all $i$ and $u\in\mathcal A^n$, where $u\otimes_1u^n$ uses $u$ at time $0$ and $u^n$ afterwards. The continuation values are $H^n_i(u^n)=\mathbb E_{i,u^n}\big[\sum_{k\ge0}\kappa^n(k+1,X_k,u^n_{X_k})\big]$. Theorem 5.2 additionally assumes (5.8): for some $T>0$, $t\mapsto|f(t,i,q)|$ is nonincreasing on $[T,\infty)$.

Formalization targets

Goal: Theorem 5.2

Let $\delta_n\downarrow0$, let $u^n$ be an equilibrium of the problem with mesh $\delta_n$, $Q^n=Q^{u^n,n}$, and suppose $f(\cdot,i,\cdot)$ is continuous on $[0,\infty)\times D_i$. If $Q^{n_k}\to Q^*\in\mathcal Q$ along a subsequence, then

$$\Gamma^{Q^*}(Q^*_i)\ge\Gamma^{Q^*}(Q_i)\quad\text{for all }(i,Q)\in S\times\mathcal Q,\qquad\text{and } Q^* \text{ is a weak equilibrium.}$$

Milestones

1. (5.12): an equilibrium $u^n$ satisfies $\kappa^n(0,i,u^n_i)+H^n(u^n)\cdot u^n_i\ge\kappa^n(0,i,u_i)+H^n(u^n)\cdot u_i$ for all $u\in\mathcal A^n$.
2. Generator form (proof of Theorem 5.2): dividing by $\delta_n$, the same inequality reads $f(0,i,Q^n_i)+H\cdot Q^n_i\ge f(0,i,Q^{u,n}_i)+H\cdot Q^{u,n}_i$.
3. Continuity of $Q\mapsto F(Q)$ on $\mathcal Q$ (proof of Theorem 3.3).
4. Lemma 5.1: $H^{n_k}_i(u^{n_k})\to F(i,Q^*)$ along the subsequence.

Significance

The theorem justifies the weak-equilibrium notion from discrete time: whatever a time-inconsistent agent does on a fine time grid, the continuous-time limit satisfies the first-order condition (3.10). Combined with the paper's discrete existence result (Theorem 5.1) and compactness of $\mathcal Q$, it yields weak equilibria by approximation (Remark 5.3). It also locates the gap between the two notions: the limit is weak but in general not strong.

The result is proved in the paper; nothing about it is open. No part of it has a machine-checked proof. A formal development adds a checked Euler-scheme comparison between $(I+\delta Q)^k$ and $e^{k\delta Q}$ for generator matrices, a dominated passage to the limit for Riemann sums of the payoff, and continuity of the payoff in the generator, each reusable for other finite-state continuous-time control problems.

Difficulty

The obvious argument is to divide the discrete one-step inequality (5.12) by $\delta_n$ and let $n\to\infty$. Its algebraic part is immediate. The difficulty is the convergence of the discrete continuation values $H^n(u^n)$, which are infinite sums along a discrete chain with transition matrix $u^n$, to the continuous payoff $F(Q^*)$, an integral along the continuous chain with generator $Q^*$. Three errors must be controlled at once: the discrete chain against the chain sampled from $e^{tQ^n}$ (the difference of $k$-th powers grows with $k\approx M/\delta_n$), the Riemann sum against the integral (needs uniform continuity of $f$ jointly in $t$ and $q$), and $F(Q^n)$ against $F(Q^*)$. The tail of the infinite sums is not controlled by (2.3) alone: integrability of a majorant does not make its samples on a grid summable, which is why (5.8) is assumed. A second subtlety concerns the last step: the paper passes from (3.10) to the weak-equilibrium property through Theorem 3.1, which assumes a condition (3.3) that Theorem 5.2 does not. The conclusion is still true without (3.3), but no numbered statement of the paper provides that step.

Formalization scope

• States are Fin N; rows are Fin N → ℝ with the sup norm, generators and transition matrices are Matrix (Fin N) (Fin N) ℝ with the product topology.
• Expectations are written through marginals: $F(i,Q)=\int_0^\infty\sum_j(e^{tQ})_{ij}f(t,j,Q_j)\,dt$ (Bochner integral) and $H^n_i(u)=\sum_k\sum_j(u^k)_{ij}\kappa^n(k+1,j,u_j)$ (tsum). No Markov process is constructed.
• The weak-equilibrium liminf is encoded as "for every $\eta>0$, eventually as $\varepsilon\downarrow0$ the quotient is $\ge-\eta$".
• "$f(\cdot,i,\cdot)$ is continuous" is joint continuity on $[0,\infty)\times D_i$; (5.8) is required for $q\in D_i$; $\delta_n\downarrow0$ is positivity, monotonicity and convergence to $0$; the subsequence is a strictly increasing $\varphi:\mathbb N\to\mathbb N$.
• Not assumed: integrability of $F$, summability of $H^n$ or (5.2) for $\kappa^n$ (they follow from (2.3) and (5.8)), compactness of $D_i$, and condition (3.3).
• The equilibria $u^n$, the generators $Q^n=(u^n-I)/\delta_n$ and the subsequence are part of the goal's data. A version that only assumes "$Q^n\to Q^*$" for arbitrary $Q^n\in\mathcal Q$ would be false and is ruled out.
• The continuity milestone is proved in the paper for compact $D_i$; it is stated here without compactness, since only convergent sequences in $\mathcal Q$ matter.
• Needed infrastructure: bounds on $\|(I+\delta Q)^k-e^{k\delta Q}\|$ for generator matrices, stochasticity of $e^{tQ}$ for generator $Q$, dominated convergence for the payoff integral and for the discrete series. Contributions of these general lemmas are welcome.

Selected references

• Y.-J. Huang and Z. Zhou, Strong and Weak Equilibria for Time-Inconsistent Stochastic Control in Continuous Time, Math. Oper. Res. 46(2), 2021; read as arXiv:1809.09243v3. https://arxiv.org/abs/1809.09243 , https://doi.org/10.1287/moor.2020.1066
• I. Ekeland and A. Lazrak, Being serious about non-commitment: subgame perfect equilibrium in continuous time, tech. rep., University of British Columbia, 2006. http://arxiv.org/abs/math/0604264
• S. N. Ethier and T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658

Motivation

Many service systems must match jobs to servers whose quality is not known in advance: crowdsourcing platforms routing tasks to worker types, wireless schedulers assigning users to channels, and switches in data networks. The scheduler learns server quality only by trying servers, and every poor assignment lets work pile up. The natural performance measure is therefore not the cumulative reward loss of classical bandits but the queue-regret: the expected excess backlog compared with a genie that knows the best assignment.

Krishnasamy, Sen, Johari and Shakkottai, Learning Unknown Service Rates in Queues: A Multiarmed Bandit Approach (Operations Research, 2021; arXiv:1604.06377), show that queue-regret has two regimes. In an early stage it grows like the regret of a bandit. In a late stage, once the queue regularly empties, past mistakes are forgotten at every empty instant and the queue-regret decays. This mission formalizes their upper bound for the late stage: a UCB scheduler with forced exploration, Q-UCB, has queue-regret of order $\log^3 t/t$.

Setting

A discrete-time switch has $U$ queues and $K\ge U$ servers. In every slot $t\ge1$, queue $u$ receives an arrival $A_u(t)\sim\mathrm{Bernoulli}(\lambda_u)$ and link $(u,k)$ offers a potential service $R_{uk}(t)\sim\mathrm{Bernoulli}(\mu_{uk})$, all independent and i.i.d. over slots. The scheduler picks a matching $\kappa(t)$, an injective assignment of a server $\kappa_u(t)$ to every queue, and queue $u$ evolves as

$$Q_u(t)=\big(Q_u(t-1)+A_u(t)-S_u(t)\big)^+,\qquad S_u(t)=R_{u\kappa_u(t)}(t).$$

The scheduler observes only past schedules and the services offered on scheduled links.

Write $\mu^*_u=\max_k\mu_{uk}$, $k^*_u$ for its maximizer, $\epsilon_u=\mu^*_u-\lambda_u$, and $\Delta=\min_{u,\,k\ne k^*_u}(\mu^*_u-\mu_{uk})$. Assumption 1: each queue has a unique best server and the best servers are distinct, so $k^*$ is the unique optimal matching. Assumption 2: $\epsilon_u>0$ for all $u$. The genie queue $Q^*_u$ always uses $k^*_u$. Assumption 3: the system starts from the stationary law of $Q^*$. The queue-regret is

$$\Psi_u(t)=\mathbb E\big[Q_u(t)-Q^*_u(t)\big].$$

Q-UCB (Algorithm 1) explores in slot $t$ with probability $\min\{1,3K\log^2t/t\}$, scheduling a uniformly random member of a fixed family $\mathcal X$ of $K$ matchings that together cover all $UK$ links. Otherwise it exploits: for each queue it picks the server with the largest index $\hat\mu_{uk}(t)+\sqrt{\log^2t/(2N_{uk}(t))}$, with $\hat\mu_{uk}$ the empirical mean and $N_{uk}$ the number of past assignments of link $(u,k)$, and schedules a matching closest in Hamming distance to these choices. Fix $\beta>1$ and set

$$w(t)=t^{1-1/\beta},\qquad v'_u(t)=\frac{6K}{\epsilon_u}w(t),\qquad v_u(t)=\frac{24}{\epsilon_u^2}\log t+\frac{60K}{\epsilon_u}\frac{v'_u(t)\log^2t}{t}.$$

Formalization targets

Goal: Theorem 5 for Q-UCB (p. 16)

For every $t\ge5800$ with $t\ge\exp\big(4/(\Delta^2(1-1/\beta)^3)\big)$, $w(t)/\log t\ge2/\epsilon_u$ and $v_u(t)+v'_u(t)\le t/2$,

$$\Psi_u(t)\le 6K\frac{v_u(t)\log^2t}{t}+\frac{24.004+UK}{6t^2}.$$

The constants are the paper's, stated exactly.

Milestones (§8.2, pp. 24–34)

• Lemma 10: the number of forced-exploration slots in a window exceeds $5\max(\log t,K(\log^3t_2-\log^3t_1))$ with probability at most $t^{-4}$. Over $[1,t]$ it exceeds $Kw(t)$ with probability at most $t^{-2K}$.
• Lemma 11: with probability at least $1-UK/(6t^3)$, no exploit slot in $(w(t),t]$ schedules a sub-optimal link (event $\mathcal E_1$).
• Lemma 12: pathwise, $Q_u(t)-Q^*_u(t)$ is at most the number of sub-optimal schedules since queue $u$ was last empty, at time $t-B_u(t)$.
• Lemmas 13–17: on $\mathcal E_1\cap\mathcal E_2$, a coarse queue bound $2Kw(t)$ (13), a first bound on the regenerative cycle (14), a maximal inequality for the arrival-minus-service walk (15), a refined polylogarithmic queue bound (16), and the refined cycle bound $B_u(t)\le v_u(t)$ (17), each failing with probability $O(t^{-3})$.

Significance

The theorem shows that a simple learning scheduler loses only $O(K\log^3t/(\epsilon_u^2t))$ in expected backlog in the late stage. Together with the paper's $\Omega(1/t)$ lower bound for consistent policies (Theorem 3), this places the optimal late-stage queue-regret within a polylogarithmic factor. The analysis method has two parts: a high-probability statement that the learner has locked onto the optimal matching, and a regenerative argument that converts it into a bound on queue length. It applies to other learning-in-queues problems in the same way.

All results are proved in the paper (§8.2). None of them has a machine-checked proof. The mission produces a formal model of the learning switch, including the algorithm with arbitrary tie-breaking, the coupled genie and the stationary start, and checks the explicit constants. These constants rely on numerical facts stated in the proofs, for example a positivity check for $x\ge\log5800$ in Lemma 10(b) and the absorption of lower-order terms into $24.004$, which a formal proof must verify.

Difficulty

The obvious argument says that UCB eventually identifies the best server, so the queue behaves like the genie's. This fails for two reasons. First, the regret is an expectation of a queue length, and a queue remembers every early mistake until it next empties. So one must bound the current regenerative cycle, and that bound itself depends on the queue length, which forces the recursion of Lemmas 13, 14, 16 and 17. Second, UCB's standard logarithmic-regret analysis bounds the expected number of sub-optimal pulls. It says nothing about whether a sub-optimal pull happens in a specific late window. Forced exploration at rate $\log^2t/t$ is what makes all indices concentrate at once, and Lemma 11 requires a union bound over every link, slot and sample count with explicit exponents.

Formalization scope

• Probability space. One canonical space: the initial queue vector together with an i.i.d. sequence of slot seeds, namely uniforms for arrivals, links and the explore coin, and a uniform explore index.
  • Arrivals and services are threshold events of the uniforms.
  • $Q(0)$ has the product geometric law $\mathbb P(Q_u(0)=n)=(1-\rho_u)\rho_u^n$ with $\rho_u=\lambda_u(1-\mu^*_u)/((1-\lambda_u)\mu^*_u)$, the stationary law of the genie chain under the printed recursion.
• Indexing and coupling. Queues and servers are Fin U and Fin K, and slots are $t\ge1$. The genie shares arrivals, services and $Q(0)$ with the system. This coupling is implicit in the paper's proofs and does not change $\Psi_u$.
• Algorithm. Q-UCB is formalized for every covering family $\mathcal X$ and every tie-breaking rule, deterministic in the slot and history, for the UCB argmax and the Hamming projection.
  • $N_{uk}(t)$ counts slots $1,\dots,t-1$.
  • An unsampled link has index $+\infty$.
  • $B_u(t)=t$ when queue $u$ never emptied on $[0,t]$.
• Disclosed additions.
  • $K\ge2$ in every statement; $K=1$ is trivial, and the constants fail there.
  • $t,t_1\ge1$ in Lemma 10(a).
  • $\log w(t)\ge(2\log t)^{2/3}$ in Lemma 10(b); the printed statement is false without it, and its proof uses it.
  • Lemmas 14 and 16 take the "arbitrary function" $v_u$ natural-valued.
• Excluded trivializations. Theorem 5 also asserts that $Q_u(t)-Q^*_u(t)$ is integrable, so $\Psi_u(t)$ cannot be a default value of a non-integrable integral. Every probability bound concerns the actual events, and every hypothesis set is satisfiable. For example, with $U=1$, $K=2$, $\lambda=0.5$, $\mu=(0.9,0.1)$, $\beta=2$, the range of Theorem 5 contains $t=\lceil e^{50}\rceil$.
• Out of scope. Theorem 5 and Lemma 11 for Q-ThS (Algorithm 2) are not formalized, and neither is Corollary 6.
• Infrastructure needed and welcome. Chernoff bounds for sums of independent non-identically distributed Bernoulli variables (Lemma 10), Hoeffding's inequality and a maximal suffix-sum bound (Lemmas 14, 15), measurability of the algorithm's trajectory in the seeds, and regenerative-cycle arguments for the reflected random walk. The Chernoff and stationary-queue lemmas are reusable well beyond this mission.

The source is the arXiv v4 preprint; the paper's proofs are in its §8 and §9.

Selected references

• S. Krishnasamy, R. Sen, R. Johari, S. Shakkottai, Learning Unknown Service Rates in Queues: A Multiarmed Bandit Approach, Operations Research 69(1), 2021. Preprint arXiv:1604.06377v4. https://arxiv.org/abs/1604.06377 ; https://doi.org/10.1287/opre.2020.1995
• P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time Analysis of the Multiarmed Bandit Problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• M. J. Neely, Stochastic Network Optimization with Application to Communication and Queueing Systems, Morgan & Claypool, 2010. https://doi.org/10.2200/S00271ED1V01Y201006CNT007

Motivation

Large data centers and cloud platforms route each incoming job to one of $N$ parallel servers through a single dispatcher. The join-the-shortest-queue (JSQ) policy, which sends each job to a server with the fewest jobs, has strong optimality properties for identical exponential servers, but it needs the queue length of every server at every arrival, which is costly when $N$ is in the thousands. The power-of-$d$ scheme JSQ($d$) polls only $d$ servers chosen at random and joins the shortest among them. For fixed $d\ge2$ it improves dramatically over random routing, which is the supermarket model of Mitzenmacher and of Vvedenskaya, Dobrushin and Karpelevich, but it does not match JSQ.

Mukherjee, Borst, van Leeuwaarden and Whiting (arXiv:1612.00723, Stochastic Systems 2018) ask how fast $d=d(N)$ must grow for JSQ($d(N)$) to behave like JSQ in the large-$N$ limit. This mission concerns their fluid-scale answer: any growth $d(N)\to\infty$ suffices.

Timeline.

• 1996–2001: Vvedenskaya–Dobrushin–Karpelevich and Mitzenmacher derive the fluid limit of JSQ($d$) for fixed $d$ (the supermarket ODE).
• 2015–2018: Eschenfeldt and Gamarnik obtain the Halfin–Whitt diffusion limit of ordinary JSQ (arXiv:1502.00999).
• 2016–2018: Mukherjee et al. prove the first transient fluid limit of ordinary JSQ in $\ell_1$ (their Theorem 4.1). They show that JSQ($d(N)$) has the same fluid limit whenever $d(N)\to\infty$ (Theorem 2.1) and the same diffusion limit whenever $d(N)/(\sqrt N\log N)\to\infty$ (Theorem 2.4, a separate mission).

Setting

There are $N$ identical servers, each with a buffer of size $b\in\{1,2,\dots\}\cup\{\infty\}$ counting the job in service. Jobs arrive as a Poisson process of rate $\lambda(N)$ and need independent unit-mean exponential service. A job sent to a full server is discarded. The occupancy vector is $\mathbf Q(t)=(Q_1(t),Q_2(t),\dots)$, where $Q_i(t)$ is the number of servers with at least $i$ jobs, with the convention $Q_0\equiv N$. If the servers are listed in nondecreasing order of queue length, the $c$-th ordered server holds $I(c)=\max\{i\ge0:Q_i\ge N-c+1\}$ jobs. A dispatch scheme picks an ordered position $c\in\{1,\dots,N\}$ for each arrival, and the arrival raises $Q_{I(c)+1}$ by one (or is discarded if $I(c)=b$).

The schemes are:

• JSQ picks $c=1$;
• JSQ($d$) picks the lowest position among $d$ positions sampled uniformly without replacement, so JSQ($N$) is JSQ;
• MJSQ($n$) picks $c=n+1$;
• CJSQ($n$) is the class of all rules that pick some $c\le n+1$;
• JSQ($n,d$) keeps the JSQ($d$) choice when it is at most $n+1$ and otherwise picks uniformly among the first $n+1$ positions.

Two systems are S-coupled when they share the arrival clock and the departure clock of the $k$-th ordered server for every $k$.

The fluid-scaled state is $\mathbf q(t)=\mathbf Q(t)/N$. It lives in

$$\mathcal S=\Big\{\mathbf q\in[0,1]^b:\ q_i\le q_{i-1}\ (i\ge2),\ \sum_{i\ge1}q_i<\infty\Big\},$$

which carries the $\ell_1$ distance. For $\mathbf q\in\mathcal S$ let $m(\mathbf q)=\min\{i:q_{i+1}<1\}$. The coefficients $p_i(\mathbf q)$ of (4.4) send all incoming work to level $m(\mathbf q)-1$ while the rate $\lambda$ can be absorbed there, and the excess to level $m(\mathbf q)$: if $m(\mathbf q)=0$ then $p_0=1$; otherwise $p_{m-1}=\min\{(1-q_{m+1})/\lambda,1\}$, $p_m=1-p_{m-1}$, and all other $p_i$ vanish.

Formalization targets

Goal: Theorem 2.1

Assume $\lambda(N)/N\to\lambda<1$, $d(N)\to\infty$ and $\mathbf q^{d(N)}(0)\to\mathbf q^\infty$ in $\mathcal S$. Then every subsequence of $\{\mathbf q^{d(N)}(t)\}_{t\ge0}$ has a further subsequence converging weakly (Skorohod $J_1$) to a limit satisfying

$$q_i(t)=q^\infty_i+\lambda\int_0^t p_{i-1}(\mathbf q(s))\,ds-\int_0^t\big(q_i(s)-q_{i+1}(s)\big)\,ds,\qquad i=1,\dots,b. \tag{2.1}$$

The statement fixes no rate for $d(N)$, which is what makes it the right goal.

Milestones

The milestones follow the paper's proof.

• §3, coupling. Proposition 3.1 is a deterministic stack ordering. Proposition 3.2 and Corollary 3.3 sandwich any CJSQ($n$) scheme between JSQ and MJSQ($n$). Proposition 3.5 bounds the $\ell_1$ distance of two S-coupled systems by $2\Delta(t)$, and Proposition 3.6 bounds $\Delta$ for JSQ($d$) against JSQ($n,d$).
• §4.1, JSQ fluid limit. Proposition 4.3 makes the martingales negligible, Lemmas 4.6 and 4.7 characterize compactness and tightness in $\ell_1$, Lemma 4.8 gives level confinement, and Theorem 4.1 is the fluid limit of JSQ itself.
• §4.2. Proposition 4.9 is the reduction "JSQ fluid limit $\Rightarrow$ JSQ($d(N)$) fluid limit".

Significance

The result. Theorem 2.1 shows that on the fluid scale the optimality of JSQ costs nothing beyond $d(N)\to\infty$ queue inquiries per job, far fewer than $N$. In particular the fluid limit is the same as that of JSQ, which is fluid-optimal. The coupling framework of §3 (the class CJSQ($n$), stack orderings, S-coupling) is not tied to JSQ($d$). The paper uses the same tools for the diffusion-scale Theorem 2.4, for batch arrivals and for the interchange of limits, Proposition 2.2.

Formalizing it. Proofs of the paper's results exist; no machine-checked version does. The mission produces:

• a reusable model of many-server systems with ordered-position dispatch;
• a formal stack-ordering and S-coupling toolkit;
• compactness and tightness criteria for $\ell_1$-valued random sequences;
• a complete fluid-limit theorem for a load-balancing policy.

The proof of Theorem 4.1 in the paper is sketched in places (the time-scale separation is argued "analogously" to Hunt and Kurtz), so a formal proof would also settle those steps.

Difficulty

The obvious argument would compare JSQ($d(N)$) directly with JSQ: the two disagree whenever the $d(N)$ sampled servers miss every shortest queue. When a constant fraction of servers is idle this is rare, but when few servers share the minimum queue length the disagreement rate does not vanish, and a direct coupling fails. The paper instead passes through CJSQ($n(N)$) with $n(N)/N\to0$, which is close to JSQ($d(N)$) for a suitable $n(N)$ and sandwiched between JSQ and MJSQ($n(N)$).

The second difficulty is the topology. The sandwich controls tail sums $\sum_{i\ge m}Q_i$, so the fluid limit of JSQ is needed in $\ell_1$, not coordinatewise. With $b=\infty$ the state space is infinite-dimensional, and tightness requires uniform control of tails. Finally, the JSQ fluid limit itself involves a separation of time scales: the drift $p_i(\mathbf q)$ is discontinuous in $\mathbf q$ and arises as an averaged stationary behaviour of a fast process.

Formalization scope

• Occupancy. Occupancy vectors are finitely supported functions ℕ →₀ ℕ with the paper's level index; coordinate $0$ holds $Q_0=N$. The buffer is $b\in\mathbb N_\infty$ with $b\ge1$; both finite and infinite $b$ are covered.
• Construction. Systems are built by uniformization: a Poisson clock of rate $\lambda+N$ with i.i.d. Uniform$[0,1]$ marks. A mark decides arrival versus departure, the departure position, the random $d$-subset (sampling without replacement) and the uniform choice of JSQ($n,d$). S-coupled systems share the clock and the marks.
• Schemes. A scheme maps the event index, the current state and the current mark to a position. CJSQ($n$) rules must be measurable in the mark.
• Fluid states. Fluid states are functions ℕ → ℝ with $q_0=1$. $\mathcal S$ carries the $\ell_1$ distance, computed in $[0,\infty]$.
• Coefficients. $p_{m-1}$ is written as "$1$ if $\lambda\le1-q_{m+1}$, else $(1-q_{m+1})/\lambda$", which equals (4.4) for $\lambda>0$ and never divides by zero.
• Limit equation. A solution of (2.1) must take values in $\mathcal S$, have integrable integrands, and satisfy every equation $i=1,\dots,b$.
• Weak convergence. Weak $J_1$ convergence to a continuous limit is stated in coupling form: copies of the processes on one probability space converge almost surely uniformly on compacts in $\ell_1$. "Any subsequence has a further subsequence" asserts the existence of the limit.
• Initial states. Theorem 2.1 has deterministic initial states with $\ell_1$ convergence and allows $\lambda=0$. Theorem 4.1, Proposition 4.3 and Lemma 4.8 have random initial states converging in probability, and $\lambda>0$.
• Stochastic order. $\le_{st}$ for processes means the existence of an ordered coupling with the right path laws. Proposition 3.6's conditional probability is stated for each value of the integer $A(T)$.
• Correction. Proposition 3.1 as printed quantifies over $m\le b$. For finite $b$ the proof also needs the ordering of the discarded counts, $m=b+1$, and the formal statement orders every level $m\ge1$.

A formalization that states only "every limit point solves (2.1)", or that measures convergence coordinatewise, would be vacuous or weaker: it is ruled out by requiring the limit's existence and $\ell_1$ convergence.

Needed infrastructure. The development needs Poisson clocks and thinning, martingale bounds for counting processes, compactness in $\ell^1$, tightness and Prokhorov's theorem on Polish spaces, and the Skorohod representation. The $\ell_1$ compactness and tightness criteria (Lemmas 4.6, 4.7) and the stack ordering (Proposition 3.1) are reusable on their own. Proofs of any milestone are welcome, as are proofs of Theorem 2.1 that bypass Theorem 4.1.

Selected references

• D. Mukherjee, S. C. Borst, J. S. H. van Leeuwaarden, P. A. Whiting, Universality of Power-of-d Load Balancing in Many-Server Systems, Stochastic Systems 8(4), 2018. arXiv:1612.00723v2, https://arxiv.org/abs/1612.00723
• P. Eschenfeldt, D. Gamarnik, Join the Shortest Queue with Many Servers. The Heavy-Traffic Asymptotics, Mathematics of Operations Research 43(3), 2018. https://arxiv.org/abs/1502.00999
• M. Mitzenmacher, The Power of Two Choices in Randomized Load Balancing, IEEE Transactions on Parallel and Distributed Systems 12(10), 2001. https://doi.org/10.1109/71.963420
• N. D. Vvedenskaya, R. L. Dobrushin, F. I. Karpelevich, Queueing System with Selection of the Shortest of Two Queues: An Asymptotic Approach, Problems of Information Transmission 32(1), 1996.
• P. J. Hunt, T. G. Kurtz, Large Loss Networks, Stochastic Processes and their Applications 53(2), 1994. https://doi.org/10.1016/0304-4149(94)90063-9
• S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658