The OR Formalization Drive

Motivation

Periodic-review inventory control with backorders is one of the basic models of operations research: in each period a manager decides how much to order, orders arrive after a lead time, unmet demand is backlogged at a penalty, and stock left over is charged a holding cost. When demands in different periods are independent, dynamic programming yields an optimal base-stock policy and computing it is tractable. In practice demands are correlated and forecasts evolve over time, for example under the martingale model of forecast evolution (Heath and Jackson, 1994, doi:10.1080/07408179408966604). The dynamic program then has to range over all possible information states, whose number is typically exponential in the input (Zipkin, 2000), so optimal policies are out of reach and the heuristics in use came without performance guarantees.

Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2):284–302, 2007) gave the first policy for this model with a worst-case guarantee that holds for arbitrary correlated, nonstationary demand distributions: the dual-balancing policy costs at most twice the optimum in expectation. The analysis rests on a marginal cost accounting that charges each order, at the time it is placed, all the holding cost its units will ever incur. This mission formalizes that guarantee.

Setting

There are $T$ periods $t = 1, \dots, T$ and a known lead time $L \ge 0$: an order placed in period $t$ arrives in period $t + L$. Period $t$ has a per-unit holding cost $h_t \ge 0$ and a per-unit backlogging penalty $p_t \ge 0$. Ordering costs are zero ($c_t = 0$), which is the standing assumption of the paper's §4. The initial data are the net inventory $ni_0$ and the pipeline orders $q_{1-L}, \dots, q_0 \ge 0$.

Demands $D_1, \dots, D_T$ are nonnegative random variables on a probability space with a filtration $(\mathcal F_t)$; $\mathcal F_t$ is the information at the beginning of period $t$, and $D_t$ is $\mathcal F_{t+1}$-measurable. A feasible policy $P$ places orders $Q^P_t \ge 0$ that are $\mathcal F_t$-measurable. Write $D_{[s,t]} = \sum_{j=s}^t D_j$ (with $D_j = 0$ for $j \le 0$), $X_t = ni_0 + \sum_{j=1-L}^{t-1} Q_j - D_{[1,t-1]}$ for the inventory position before ordering and $Y_t = X_t + Q_t$ after ordering.

The marginal holding cost of period $t$ is the holding cost that the units ordered in $t$ incur until the end of the horizon, and the marginal backlogging cost is the penalty incurred one lead time later:

The cost of $P$ is $\mathcal C(P) = \sum_{t=1}^{T-L}(H^P_t + \Pi^P_t)$; by Eq. (3) it differs from the total holding and backlogging cost only by a policy-independent nonnegative term.

A dual-balancing policy $B$ orders nothing after period $T - L$, and in each period $t \le T - L$ orders the quantity that balances the two conditional expected marginal costs:

Formalization targets

Goal: Theorem 4.1

For every dual-balancing policy $B$ and every feasible policy $P$,

The paper writes $P = OPT$; quantifying over all feasible $P$ is the same statement whenever an optimum exists and needs no existence assumption.

Milestones

1. Lemma 4.1. $E[\mathcal C(B)] = 2\sum_{t=1}^{T-L}E[Z_t]$ with $Z_t = E[H^B_t \mid \mathcal F_t]$.
2. Lemma 4.2. With $\mathcal T_H = \{t : Y^B_t < Y^P_t\}$, $\sum_{t\in\mathcal T_H} H^B_t \le \sum_{t=1}^{T-L} H^P_t$ on every realization.
3. Lemma 4.3. With $\mathcal T_\Pi = \{t : Y^B_t \ge Y^P_t\}$, $\sum_{t\in\mathcal T_\Pi} \Pi^B_t \le \sum_{t=1}^{T-L} \Pi^P_t$ on every realization.

Two further items are not milestones. Eq. (3) states that, along every realization, the period-by-period holding and backlogging cost equals $\sum_{t=1-L}^{0}\Pi_t + H_{(-\infty,0]} + \sum_{t=1}^{T-L}(H_t + \Pi_t)$, which is why the cost of Eq. (4) is the right objective. The other states that a dual-balancing policy exists when $h_T > 0$ and the demands are integrable, so the goal is not about an empty class.

Significance

The theorem gives a policy that is computable period by period, by a one-dimensional search, with a factor-two guarantee that holds for every joint demand distribution, including correlated, nonstationary and forecast-driven ones, where the optimal policy cannot be computed. The constant is tight: the paper exhibits instances where the ratio tends to two. The second mission of this series treats the stochastic lot-sizing problem of the same paper, which uses the same marginal cost accounting.

The result is proved in the paper; no machine-checked proof of it is known. Formalizing it produces a reusable model of the periodic-review backlogging system with lead times and adapted policies, a verified marginal cost identity, and a formal approximation guarantee for a stochastic inventory policy. The pathwise comparison lemmas are stated for arbitrary pairs of order sequences and so apply to other balancing-type policies.

Difficulty

The obvious attempt compares the two policies period by period. That fails: in a given period the dual-balancing policy may hold far more or far less inventory than the comparison policy, and neither the holding nor the backlogging cost of one period is bounded by the comparator's cost in that period. The comparison only works after re-charging holding costs to the period in which the units were ordered, which requires the identity Eq. (3) to be established exactly, including the pipeline units, the initial stock and the lead-time shift. The probabilistic step then needs the random index sets $\mathcal T_H$ and $\mathcal T_\Pi$ to be determined by the information of period $t$, so that conditioning on $\mathcal F_t$ commutes with the indicators; this is where the nonanticipativity of both policies enters. The existence of a balancing quantity needs a measurable selection from conditional laws, and it fails without a positive late holding cost.

Formalization scope

• Periods are integers (ℤ). Orders and demands are functions ℤ → Ω → ℝ; only periods $1, \dots, T$ are read, and the pipeline $q_t$ is substituted for $t \le 0$.
• Ordering costs are $c_t = 0$ and there is no discounting, as in the paper's §4; the reduction of §4.6 from general instances is not formalized. The lead time $L$ is general.
• Information is an arbitrary Filtration ℤ to which demands are adapted with a one-period lag; the paper's information vectors are a special case, and randomized policies are covered when their randomness is part of the information.
• Expected costs are lower Lebesgue integrals in $[0,\infty]$, so an infinite expected cost is never read as $0$.
• The balancing condition carries integrability of $H^B_t$ and $\Pi^B_t$, so a conditional expectation of a non-integrable cost (which Mathlib sets to $0$) cannot satisfy it vacuously. The existence item rules out an empty policy class.
• Lemmas 4.2 and 4.3 are pathwise and do not use the balancing rule. The comparator totals are the marginal totals of Eq. (4), which is the stronger reading.
• Eq. (2) prints $X_{t+L}$ and its restatement on p. 292 prints $p_t$; both are typos, and the formalization uses $X_t$ and $p_{t+L}$.

A complete development needs finite-sum manipulations for Eq. (3) and Lemma 4.2, conditional expectation (tower property, pulling out bounded $\mathcal F_t$-measurable factors) for Lemma 4.1 and the goal, and regular conditional distributions with a measurable selection for the existence item. Theorem 4.2 (the randomized policy for integer demands) is outside this mission.

Selected references

• R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2):284–302, 2007. doi:10.1287/moor.1060.0205
• D. C. Heath, P. L. Jackson, Modeling the evolution of demand forecasts with application to safety stock analysis in production/distribution systems, IIE Transactions 26(3):17–30, 1994. doi:10.1080/07408179408966604
• P. H. Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000. ISBN 978-0-256-11379-7.

Motivation

In a multi-armed bandit problem a learner chooses one of $K$ actions in each of $n$ rounds and observes only the reward of the chosen action. Two models of the rewards have separate theories. In the stochastic model, each arm pays independent draws from a fixed distribution; algorithms such as UCB1 (Auer, Cesa-Bianchi & Fischer 2002) have regret of order $\sum_i \log(n)/\Delta_i$, logarithmic in $n$. In the adversarial model, an adversary chooses the rewards; Exp3 and its variants (Auer, Cesa-Bianchi, Freund & Schapire 2002) have regret of order $\sqrt{nK}$, which is optimal there. An algorithm tuned for one model fails in the other: stochastic algorithms can suffer linear regret against an adversary, and adversarial algorithms pay $\sqrt n$ even when the rewards are i.i.d.

Bubeck and Slivkins (arXiv:1202.4473, COLT 2012) asked whether one algorithm can be near-optimal in both models without knowing which one it faces. They answered yes with the algorithm SAO. This result started the "best of both worlds" line of work on bandits. Later contributions include EXP3++ (Seldin & Slivkins 2014) and Tsallis-INF (Zimmert & Seldin 2021).

Setting

There are $K\ge2$ arms and $n\ge K$ rounds. On round $t$ the algorithm draws an arm $I_t$ from a probability vector $p_t=(p_{1,t},\dots,p_{K,t})$ computed from the history it has observed. At the same time a reward vector $g_t\in[0,1]^K$ is fixed, and the algorithm observes only $g_{I_t,t}$.

• Adversarial model. The vector $g_t$ is chosen by an adaptive adversary: a function of the arms $I_1,\dots,I_{t-1}$ played earlier, but not of $I_t$. The regret is $R_n=\max_i\sum_{t=1}^n g_{i,t}-\sum_{t=1}^n g_{I_t,t}$.
• Stochastic model. There are distributions $\nu_1,\dots,\nu_K$ on $[0,1]$ with means $\mu_i$, and all $g_{i,t}\sim\nu_i$ are independent. The pseudo-regret is $\overline R_n=\sum_{t=1}^n(\max_i\mu_i-\mu_{I_t})$. The gap of arm $i$ is $\Delta_i=\max_j\mu_j-\mu_i$, and the minimal gap is $\Delta=\min_{i:\Delta_i>0}\Delta_i$.

The analysis uses importance-weighted estimates $\widetilde H_{i,t}=\frac1t\sum_{s\le t}g_{i,s}\mathbb 1_{\{I_s=i\}}/p_{i,s}$, the sample means $\widehat H_{i,t}$, the averages $H_{i,t}=\frac1t\sum_{s\le t}g_{i,s}$, and the play counts $T_i(t)$.

SAO (Algorithm 1 of the paper) takes a parameter $\beta>1$. It keeps a set of active arms, initially all arms, and samples them uniformly at first. On each round it applies a test, (12), that deactivates an arm whose estimate $\widetilde H_{i,t}$ falls far below the best active one. The probability of a deactivated arm then decays as $q_i\tau_i/t$, where $\tau_i$ is the deactivation time and $q_i$ the arm's probability at that moment. Three further tests, (13)–(15), check that the observations stay consistent with stochastic rewards. If any of them fails on round $\tau_0$, SAO switches permanently to the adversarial algorithm Exp3.P (Bubeck & Cesa-Bianchi 2012, Fig. 3.1) for the remaining rounds.

Formalization targets

Goal: Theorem 4.1, high-probability form

For every $\delta\in(0,1)$ let $\beta=10Kn^3\delta^{-1}$. With probability at least $1-\delta$, SAO with parameter $\beta$ satisfies, in the stochastic model (whenever some arm has $\Delta_i>0$),

and, against every adaptive adversary with rewards in $[0,1]$,

Milestones

The milestones follow the paper's proof in order:

• Freedman's inequality (Theorem 4.3) in the paper's two-sided form, and its variance-adaptive form, Lemma 4.4.
• The concentration lemmas for SAO's estimates (Lemmas 4.5, 4.6, 4.7) and the Exp3.P phase (Lemma 4.8).
• The two good events of §4.1, (21)–(25).
• The deterministic consequences on those events: Exp3.P is never started in the stochastic model; suboptimal arms are deactivated by time $260K\log(\beta)/\Delta_i^2$; $\sum_iq_i\le1+\log K$, (27); and the adversarial regret bound of §4.3.
• The two halves of Theorem 4.1.

Significance

The theorem shows that the stochastic and adversarial regret rates are not in conflict. A single algorithm, with no information about the model, gets $O(K\log K\log^2(n/\delta)/\Delta)$ pseudo-regret on stochastic rewards and $\tilde O(\sqrt{nK})$ regret against adaptive adversaries. Each rate is within polylogarithmic factors of optimal for its model. Later algorithms improved the logarithmic factors and removed the explicit switching, but they are compared against this result.

The theorem is proved in the paper. It is not known to have a machine-checked proof. Formalizing it requires a precise model of an adaptive adversary interacting with a randomized algorithm, martingale concentration with random variance (Lemma 4.4), and an exact statement of SAO including its boundary cases. The pieces are reusable: the interaction model, the estimators, Exp3.P and its high-probability guarantee all apply to other adversarial bandit results.

Difficulty

Neither standard analysis carries over. In the stochastic model, SAO's sampling probabilities are random and depend on the past, and a deactivated arm's probability keeps changing. Hoeffding-type bounds for a fixed sampling scheme therefore do not apply to $\widetilde H_{i,t}$. The variance of the importance-weighted estimate grows like $\sum_s1/p_{i,s}$, which is controlled only through the algorithm's own schedule (16). This is why Lemma 4.5 has the two-part radius with $\max(t-\tau_i,0)/(q_i\tau_it)$. In the adversarial model, the deterministic argument has to show that whenever the consistency tests pass, the regret accumulated before the switch is already small, for an adversary that adapts to the arms played. A union bound over all quantities, all arms and all times (§4.1) is needed before any deterministic reasoning, so every constant in the event matters.

Formalization scope

All declarations live in the namespace BestBothWorlds.SAO.

• Arms and paths. Arms are Fin K and rounds are $1,\dots,n$. An arm path is Fin n → Fin K.
• Algorithms and adversaries. An algorithm is a deterministic map from the observed history to a probability vector. A deterministic adaptive adversary is a map from the list of earlier arms to a reward vector; randomized adversaries are mixtures of these.
• Probabilities. For a fixed adversary, the probability of an event is $\sum_{I\in E}\prod_tp_{I_t,t}$. In the stochastic model this is integrated against the product law of the reward table.
• Logarithms and constants. Real.log is the natural logarithm. All constants of Theorem 4.1 are explicit, with $\beta=10Kn^3\delta^{-1}$.
• SAO. It is defined exactly as Algorithm 1. Arms are tested in order within a round, and the active set changes during the loop. Test (13) is false when $T_i(t)=0$, and test (14) is false when $\tau_i=1$.
• Exp3.P. After the switch, Exp3.P runs from scratch for $n-\tau_0$ rounds. Its parameters are those of Bubeck–Cesa-Bianchi Theorem 3.2 with confidence $K/\beta$, and $\gamma$ and $\beta_{\mathrm P}$ are clipped at $1$.
• §4 notation. $\tau_0$, $\tau_i\leftarrow\min(\tau_i,\tau_0)$ and $q_i=p_{i,\min(\tau_i,\tau_0)}$ are computed from the run, never assumed.

A trivializing formalization is ruled out. The goal's hypotheses concern only the instance ($K$, $n$, $\delta$, the distributions or the adversary). The algorithm's quantities ($\tau_0$, $\tau_i$, $q_i$, the sampling probabilities) are computed by the definition of SAO and are never free variables or hypotheses. The adversarial half covers adaptive adversaries, not only oblivious reward tables.

The expectation form of Theorem 4.1 ($O(\cdot)$ bounds with $\beta=n^4$), Theorem 1.1 and the two-armed warm-up of §3 are out of scope. Proofs of any milestone are welcome, as are alternative proofs of the concentration lemmas from Mathlib's martingale library.

Selected references

• S. Bubeck and A. Slivkins, The best of both worlds: stochastic and adversarial bandits, COLT 2012; arXiv:1202.4473v1. https://arxiv.org/abs/1202.4473
• S. Bubeck and N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://doi.org/10.1561/2200000024
• D. A. Freedman, On tail probabilities for martingales, Annals of Probability 3(1), 1975. https://doi.org/10.1214/aop/1176996452
• P. Auer, N. Cesa-Bianchi and P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• P. Auer, N. Cesa-Bianchi, Y. Freund and R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• Y. Seldin and A. Slivkins, One practical algorithm for both stochastic and adversarial bandits, ICML 2014. https://proceedings.mlr.press/v32/seldinb14.html
• J. Zimmert and Y. Seldin, Tsallis-INF: an optimal algorithm for stochastic and adversarial bandits, JMLR 22, 2021. https://jmlr.org/papers/v22/19-753.html

Why symmetric queues

The classical product-form results for queueing networks (Jackson, Kelly, Baskett–Chandy–Muntz–Palacios) assume exponentially distributed service requirements, because then the state of a queue need not record how much service each customer has received. Real service times are rarely exponential: telephone call lengths, job sizes in time-shared computers and web transfers are far from it. Symmetric queues, introduced in §3.3 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), form the class of single queues for which the stationary distribution of the number of customers, and of their classes, depends on the service requirement distribution only through its mean. This property, insensitivity, is what makes Erlang's loss formula valid for arbitrarily distributed call lengths (Kelly, p. 79), and it is the reason processor-sharing, last-come-first-served preemptive and infinite-server stations may appear with general service in product-form networks.

Timeline. Sevastyanov (1957) proved that Erlang's loss formula holds for arbitrarily distributed call lengths. Kelly (1975, 1976) introduced queues with customers of different types whose effort and arrival-position functions coincide, and showed product form for networks of them with non-exponential service built from exponential stages; Barbour (1976) extended the method of stages; Baskett, Chandy, Muntz and Palacios (1975) gave product form for networks containing processor-sharing, LCFS-preemptive and infinite-server stations with phase-type service. Kelly's 1979 book presents the symmetric queue in the form formalized here.

Setting

A symmetric queue holds customers in positions $1, 2, \dots, n$, where $n$ is the number present. It operates as follows (Kelly, p. 72):

1. the service requirement of a customer is a random variable whose distribution may depend on the class of the customer;
2. a total service effort is supplied at rate $\phi(n)$, with $\phi(n) > 0$ for $n > 0$;
3. a proportion $\gamma(l, n)$ of this effort, $\sum_{l=1}^n \gamma(l, n) = 1$, goes to the customer in position $l$; when he leaves, the customers in positions $l+1, \dots, n$ move down by one;
4. an arriving customer moves into position $l \in \{1, \dots, n+1\}$ with probability $\gamma(l, n+1)$ — the same function — and the customers in positions $l, \dots, n$ move up by one.

Server-sharing ($\gamma(l, n) = 1/n$), the stack ($\gamma(n, n) = 1$, last come first served preemptive), the queue with no waiting room and the infinite-server queue are examples (pp. 73–74).

Customers of class $c$ arrive in a Poisson stream of rate $\nu(c)$. On arrival a class-$c$ customer receives a refined class $(c, z)$ with probability $p(c, z)$, $\sum_z p(c, z) = 1$, and then needs $w(c, z) \ge 1$ independent stages of service, each exponentially distributed with mean $d(c, z) > 0$. The class-$c$ service requirement is therefore a mixture of gamma distributions with mean

and the work arriving per unit time is $a = \sum_c \nu(c) a(c)$. The record of the customer in position $l$ is $\mathbf c(l) = (c(l), z(l), u(l))$, $u(l)$ the stage in progress, and $\mathbf c = (\mathbf c(1), \dots, \mathbf c(n))$ is a Markov process. Its transitions are: an arrival of class $(c,z)$ into position $l$ at stage $1$, at rate $\nu(c)p(c,z)\gamma(l, n+1)$; and, at rate $\phi(n)\gamma(l,n)/d(c(l),z(l))$, completion of the current stage of the customer in position $l$, which moves him to the next stage or, after stage $w(c(l), z(l))$, out of the queue. The normalizing constant is

Formalization targets

Goal: Theorem 3.8

When (3.15) converges, the distribution

is the equilibrium distribution of $\mathbf c$, and under it

and the queue is quasi-reversible with respect to the classification $c$ and to $(c, z)$: from every state, the rate of arrivals of each class does not depend on the state, both for the process and its time reversal (relations (3.8) and (3.10) of p. 67).

Milestones

• Eqs. (3.14)–(3.15): the case of one refinement per class, $\pi(\mathbf c) = b\prod_l \nu(c(l))d(c(l))/\phi(l)$ with $a = \sum_c \nu(c)d(c)w(c)$.
• Eqs. (3.16)–(3.17): in that case, the law of $n$, and given $n$ independent positions of class $c$ with probability $\nu(c)d(c)w(c)/a$ and uniform stage.
• Eq. (3.18): the equilibrium distribution under gamma-mixture service.
• Lemma 3.9: mixtures of gamma distributions approximate, at continuity points, the distribution function of any positive random variable.

Significance

Theorem 3.8 gives the stationary law of a symmetric queue in closed form and shows that it depends on the service requirement distributions only through their means $a(c)$. Quasi-reversibility (part (iii)) is the property that lets symmetric queues be placed in networks: Kelly's §3.2 shows that a network of quasi-reversible queues has a product-form equilibrium, so Theorem 3.8 is the single-queue input to product-form networks with processor-sharing, LCFS-preemptive and infinite-server stations and class-dependent, non-exponential service. Lemma 3.9 is the approximation step behind the extension to arbitrary service distributions (Theorem 3.10).

These results are classical and proved in the book. To our knowledge none of them is machine-checked; Mathlib has the gamma distribution and distribution functions but no queueing theory. The mission produces a formal model of the symmetric queue as a countable-state Markov process, its equilibrium distribution, the insensitive marginals and the rate characterization of quasi-reversibility, all reusable by the chapter on networks of quasi-reversible queues.

Difficulty

The obvious first attempt, detailed balance, fails: the stage process is not reversible in general, since an intermediate stage completion has no transition back. The equilibrium equations must be verified in full, over a countable state space in which a single state is reached from infinitely many others. The symmetry condition $\gamma \equiv \delta$ is essential and must enter the argument: without it (for first-come-first-served, say) the distribution (3.18) is false for non-exponential service. Positions shift on every arrival and departure, so the bookkeeping of which list results from which event, including coincidences when neighbouring customers have identical records, is the main formal burden. The marginal computations sum (3.18) over lists of records, where convergence must be tracked, and Lemma 3.9 needs an explicit construction of approximating gamma mixtures.

Formalization scope

• The state is a List of customer records (class, refined class, stage); list index $i$ is position $l = i + 1$, and $\gamma(l, n)$, $\phi(n)$ keep the book's $1$-based indexing. The state space consists of the lists whose records have $\nu(c)p(c,z) > 0$ and $1 \le u \le w(c, z)$: records of a refined class arriving at rate zero are unreachable and excluded.
• Classes $\mathcal C$ and refinements $\mathcal Z$ are arbitrary countable types. All infinite sums are HasSum or tsum with explicit convergence hypotheses: $\sum_c \nu(c) < \infty$ (finite exit rates, the book's standing assumption of §1.1), convergence of $a(c)$, of $a$, and of (3.15). "Equilibrium distribution" means positive, summing to one, and satisfying the equilibrium equations with convergent series.
• The statement is rate level: (3.18) is shown to satisfy the equilibrium equations of the stage process, and quasi-reversibility is its rate characterization (3.8), (3.10). That these describe the stationary process and its time reversal is the book's Chapter 1 and is not reformalized.
• Trivializing readings ruled out: the goal keeps $p$, $w$ and $d$ general (not $w \equiv 1$, which would make the result Section 3.1's exponential case); the arrival position uses the same $\gamma$ as the service split; and in Lemma 3.9 the approximants must be genuine gamma mixtures with integer shapes, which a point mass is not.
• Not planned: Theorem 3.10 (arbitrary service distributions; only an outline of proof and a continuous state space the book does not construct) and Theorem 3.11 (reversibility of the number in queue, a non-Markov process).

Welcome contributions: proofs of the milestones, lemmas about List.insertIdx/List.eraseIdx bookkeeping for queues with positions, and summation over lists of records.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, Chichester, 1979, §3.3, pp. 72–82. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• F. P. Kelly, Networks of queues with customers of different types, Journal of Applied Probability 12 (1975), 542–554. https://www.jstor.org/journal/japplprob
• F. P. Kelly, Networks of queues, Advances in Applied Probability 8 (1976), 416–432. https://www.jstor.org/journal/advaapplprob
• A. D. Barbour, Networks of queues and the method of stages, Advances in Applied Probability 8 (1976), 584–591. https://www.jstor.org/journal/advaapplprob
• B. A. Sevastyanov, An ergodic theorem for Markov processes and its application to telephone systems with refusals, Theory of Probability and its Applications 2 (1957), 104–112.
• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, closed, and mixed networks of queues with different classes of customers, Journal of the ACM 22 (1975), 248–260. https://doi.org/10.1145/321879.321887

Motivation

Networks of queues model systems in which jobs visit a sequence of service stations: items in a manufacturing job-shop, packets in a communication network, patients moving between hospital departments. The open migration process of Chapter 2 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), and the job-shop networks of Jackson (Jackson 1963) route a customer leaving a queue at random, independently of where he has been. That rules out the most common situation in practice: an item that has passed machines 1 and 3 must next go to machine 4, while an item that has passed machines 2 and 3 must go to machine 5.

Section 3.1 of the book removes this restriction. Customers are divided into types, a type fixes a deterministic route through the queues, and a stochastic routing rule is recovered by using one type per possible route. Within each queue, the order of service is described by two position-dependent functions, which cover first-come first-served $K$-server queues, last-come first-served, processor sharing and service in random order. Theorem 3.1 states that, for every such network, the equilibrium distribution is a product of explicit single-queue factors. This is the result behind the "Kelly network" and "Kelly-type queue" terminology of later work (Kelly 1975; Baskett, Chandy, Muntz, Palacios 1975).

Setting

There are $I$ customer types and $J$ queues. Customers of type $i$ enter the system in a Poisson stream of rate $\nu(i)>0$ and visit the queues $r(i,1),r(i,2),\dots,r(i,S(i))$ in that order before leaving; two successive stages of a route are at different queues.

Queue $j$ holds its $n_j$ customers in positions $1,\dots,n_j$. Each customer needs an exponentially distributed amount of service with unit mean. The queue supplies total service effort at rate $\phi_j(n_j)$, with $\phi_j(n)>0$ for $n>0$; a proportion $\gamma_j(l,n_j)$ goes to the customer in position $l$. An arriving customer takes position $l$ with probability $\delta_j(l,n_j+1)$. For each $n\ge1$, $\gamma_j(\cdot,n)$ and $\delta_j(\cdot,n)$ are probability vectors on $\{1,\dots,n\}$.

The class of the customer in position $l$ of queue $j$ is $c_j(l)=(t_j(l),s_j(l))$, his type and the stage of his route. The state of queue $j$ is $\mathbf c_j=(c_j(1),\dots,c_j(n_j))$ and the state of the network is $\mathbf C=(\mathbf c_1,\dots,\mathbf c_J)$. Its transition rates $q(\mathbf C,\mathbf D)$, displays (3.1)–(3.6), are the sums of the intensities of all events taking $\mathbf C$ to $\mathbf D$: a departure from the system (intensity $\phi_j(n_j)\gamma_j(l,n_j)$), a move from position $l$ of queue $j$ to position $m$ of the next queue $k$ (intensity $\phi_j(n_j)\gamma_j(l,n_j)\delta_k(m,n_k+1)$), and an arrival into position $m$ of the first queue $k$ of a route (intensity $\nu(i)\delta_k(m,n_k+1)$).

With $\alpha_j(i,s)=\nu(i)$ if $r(i,s)=j$ and $0$ otherwise, set

Formalization targets

Goal: Theorem 3.1 (p. 61)

If every series defining $b_j^{-1}$ converges, then

is positive, sums to $1$ over all network states, and satisfies the equilibrium equations

Milestones

• Theorem 3.2 (p. 62). The time-reversed rates $\pi(\mathbf D)q(\mathbf D,\mathbf C)/\pi(\mathbf C)$ are the rates of the reversed network: routes traversed backwards, $\gamma_j$ and $\delta_j$ interchanged.
• Corollary 3.4 (p. 63). Queue $j$ is independent of the rest of the network, is in state $\mathbf c_j$ with probability $\pi_j(\mathbf c_j)$, holds $n$ customers with probability $b_ja_j^n/\prod_{l=1}^n\phi_j(l)$ (3.7), and a customer in position $l$ is of class $(i,s)$ with probability $\alpha_j(i,s)/a_j$.
• Corollary 3.5 (p. 63). A type-$i$ customer reaching queue $j$ at stage $s$ finds it in state $\mathbf c_j$ with probability $\pi_j(\mathbf c_j)$.
• Lemma 3.13 (p. 89). For a multiclass queue with Poisson arrivals of rate $\nu(c)$ and departure intensities $\nu(c)\phi_c(\mathbf n)$: reversible $\Leftrightarrow$ quasi-reversible $\Leftrightarrow$ $\Phi(\mathbf n)=\phi_c(\mathbf n)\Phi(\mathbf n-\mathbf e_c)$ for some positive $\Phi$ (3.26).

Significance

Theorem 3.1 gives the full joint law of a network in which routes carry memory, and its corollaries turn it into usable performance formulas: each queue behaves, in its marginal law and as seen by arriving customers, like an isolated queue fed by a Poisson stream of rate $a_j$, even though the actual arrival stream at queue $j$ is not Poisson. Mean sojourn times along a route then follow from Little's result. Theorem 3.2 identifies the reversed process as a network of the same kind; it is the source of the departure-stream results (Corollary 3.3) and of the arrival theorem (Corollary 3.5). Lemma 3.13 isolates the condition (3.26) under which state-dependent arrival rates preserve the product form (Theorem 3.14).

The results are classical and proved in the book. None of them has a machine-checked proof: the Prove2Me catalogue holds the rate-level theorems for migration processes (Chapter 2 of Kelly–Yudovina), and open targets for the BCMP and Jackson models, which have different state descriptions. This mission adds a formal model of the position-structured multiclass network itself, with the summation over coinciding transitions that (3.2), (3.4) and (3.6) require, and product-form, reversal and arrival-theorem statements over it.

Difficulty

The obvious first attempt, detailed balance, fails: $\pi(\mathbf C)q(\mathbf C,\mathbf D)$ and $\pi(\mathbf D)q(\mathbf D,\mathbf C)$ differ in general, because a customer's route cannot be run backwards inside the same network ($q(\mathbf D,\mathbf C)$ is usually $0$ when $q(\mathbf C,\mathbf D)>0$). The equilibrium equations therefore involve, for each state, all its predecessors at once. The rates are themselves sums over coinciding transitions, so a statement about individual events does not transfer to the rates without accounting for which positions lead to the same successor state. In Lean this brings in insertion into and deletion from position lists, the relabelling of stages, and the normalization of a product over a countable space of $J$-tuples of lists, reorganized by queue length together with the identity $\sum_{\text{classes at } j}\alpha_j=a_j$.

Formalization scope

• Finite types and queues. Types are Fin I, queues Fin J; the book allows countably many types with $\sum_i\nu(i)<\infty$. A network state is a function assigning to each queue a list of classes $(i,s)$ with $r(i,s)=j$; the state space is countable and all sums over it are tsum/HasSum.
• Indexing. Stages and list positions are $0$-based in Lean; $\gamma_j(l,n)$ and $\delta_j(l,n)$ keep the book's $1$-based position argument.
• Rate level. Equilibrium means: positive, summing to $1$, and satisfying the equilibrium equations (the published KellyStochasticNetworks.FullBalance). The existence of the Markov process, irreducibility and non-explosion are not formalized. "The reversed process" (Theorem 3.2) is read through the reversed rates $\pi(\mathbf D)q(\mathbf D,\mathbf C)/\pi(\mathbf C)$; "the probability he finds" (Corollary 3.5) is read as a ratio of equilibrium arrival fluxes; quasi-reversibility is its rate characterization (3.8), (3.10).
• Normalizing constants. $b_j$ is defined through a tsum, which Lean sets to $0$ for a divergent series; every theorem assumes the series converges, the book's "none of $b_1,\dots,b_J$ is zero".
• No trivial instance. The goal holds for arbitrary $I$, $J$, $\nu$, routes, $\phi_j$, $\gamma_j$, $\delta_j$ subject only to the book's constraints; a proof for a single queue, or for fixed $\gamma=\delta$ disciplines, does not prove it. In Lemma 3.13 the function $\Phi$ is required to be positive, since $\Phi\equiv0$ satisfies (3.26) for every queue.

Infrastructure that a complete development needs: list insertion/deletion lemmas for position bookkeeping, sums of products over $\prod_j \mathrm{List}(\cdot)$, and a bijection-of-events argument for summed rates. The quasi-reversibility predicate and the reversed-rate apparatus are reusable for the closed networks of §3.4 and the symmetric queues of §3.3. Contributions are welcome on any milestone, in any order.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, John Wiley & Sons, 1979. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• F. P. Kelly, Networks of queues with customers of different types, Journal of Applied Probability 12 (1975), 542–554. https://doi.org/10.2307/3212785
• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, closed, and mixed networks of queues with different classes of customers, Journal of the ACM 22 (1975), 248–260. https://doi.org/10.1145/321879.321887
• J. R. Jackson, Jobshop-like queueing systems, Management Science 10 (1963), 131–142. https://doi.org/10.1287/mnsc.10.1.131
• F. P. Kelly, E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781139565363

Motivation

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

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

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

Setting

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