Motivation

Networks of queues model systems in which a job visits several service stations in turn: jobs in a computer system alternating between CPU and disks, machines cycling between operation and repair, parts routed through a job shop. In a closed network no job enters or leaves; a fixed population of $N$ customers circulates among $k$ nodes. Closed networks are the standard model of multiprogrammed computer systems and of machine-repair and finite-source systems, and they are the setting of chapter 4 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, doi:10.1002/9781118625651).

The chapter's results form a short line of computational ideas:

• Jackson (1957, 1963) showed that open networks of exponential servers with Markovian routing have a product-form steady state; Gordon and Newell (1967) gave the closed-network version, (4.15)–(4.18) of the book.
• Buzen (1973) gave a convolution recursion for the normalizing constant $G(N)$ and for marginal distributions, (4.19)–(4.22).
• Reiser and Lavenberg (1980) introduced mean-value analysis (MVA), which computes mean queue lengths, waiting times and throughputs population by population without ever forming $G(N)$, (4.23)–(4.25); the book presents it following Bruell and Balbo (1980).
• The book closes the section with a recursion for the full marginal distributions, (4.26), which it proves from the product form (pp.207–209).

This mission formalizes that line, ending at (4.26).

Setting

A closed Jackson network has nodes $i = 1, \dots, k$, each with a single server whose service times are exponential with rate $\mu_i > 0$. A customer finishing service at node $i$ moves to node $j$ with probability $r_{ij}$; the routing matrix $R = (r_{ij})$ has nonnegative entries and rows summing to one, and it is irreducible: every node can be reached from every other. The state is $\bar n = (n_1, \dots, n_k)$, the number of customers at each node, with $n_1 + \cdots + n_k = N$; this state space is finite.

The steady-state distribution $p_{\bar n}$ is the probability vector on the state space that solves the flow-balance equations (4.14),

$$\sum_{j=1}^{k}\sum_{\substack{i=1\\ i\ne j}}^{k} \mu_i r_{ij}\, p_{\bar n;i^+j^-} = \sum_{i=1}^{k}\mu_i(1-r_{ii})\,p_{\bar n},$$

where $\bar n;i^+j^-$ has one more customer at $i$ and one fewer at $j$, and terms with a negative subscript or with $\mu_i$ at an empty node vanish. The traffic equations (4.16) are $\mu_i\rho_i = \sum_j \mu_j r_{ji}\rho_j$; they determine $\rho = (\rho_1, \dots, \rho_k)$ up to a positive factor. The normalizing constant is

$$G(N) = \sum_{n_1+\cdots+n_k=N}\rho_1^{n_1}\cdots\rho_k^{n_k},$$

and more generally, with $f_i(n) = \rho_i^{\,n}/a_i(n)$ for $c_i$-server nodes ((4.13)), $G(N) = \sum \prod_i f_i(n_i)$ and Buzen's function $g_m(n) = \sum_{n_1+\cdots+n_m=n}\prod_{i\le m} f_i(n_i)$.

For each population $N$ write $p_i(n, N) = \Pr\{N_i = n\}$ for the marginal distribution at node $i$, $\bar P_i(n; N) = \Pr\{N_i \ge n\}$, $L_i(N)$ for the mean number at node $i$, and

$$\lambda_i(N) = \Pr\{\text{server busy at node } i\}\cdot\mu_i$$

for the throughput of node $i$.

Formalization targets

Goal: the marginal recursion (4.26)

For every node $i$,

$$p_i(0,0) = 1, \qquad p_i(n, N) = \frac{\lambda_i(N)}{\mu_i}\,p_i(n-1, N-1) \quad (n, N \ge 1).$$

It involves only the steady-state distributions and quantities computed from them; it holds for every irreducible routing matrix and every choice of rates.

Milestones

1. Product form (4.14)–(4.16). For any positive solution $\rho$ of (4.16), a probability distribution solves (4.14) if and only if $p_{\bar n} = G(N)^{-1}\rho_1^{n_1}\cdots\rho_k^{n_k}$.
2. Buzen's algorithm (4.19)–(4.21). $G(N) = g_k(N)$, $g_m(n) = \sum_{i=0}^{n} f_m(i)\,g_{m-1}(n-i)$, $g_1 = f_1$, $g_m(0) = 1$.
3. Marginal at the last node (4.22). $p_k(n) = f_k(n)\,g_{k-1}(N-n)/G(N)$ for $0 \le n \le N$.
4. Complementary marginal (p.208). $\bar P_i(n_i; N) = \rho_i^{\,n_i}G(N-n_i)/G(N)$.
5. Mean-value analysis (4.23)–(4.25). $L_i(0) = 0$; $L_i(N) = \lambda_i(N)W_i(N)$ with $W_i(N) = (1 + L_i(N-1))/\mu_i$; and for $v$ solving $v_i = \sum_j v_j r_{ji}$ with $v_l = 1$, $\lambda_l(N) = N/\sum_i v_iW_i(N)$ and $\lambda_i(N) = \lambda_l(N)v_i$.

Significance

The product form reduces a $\binom{N+k-1}{N}$-state Markov chain to the constants $G(0), \dots, G(N)$, and Buzen's recursion computes them in $O(kN^2)$ operations. Mean-value analysis goes further and avoids $G(N)$, whose magnitude can overflow or underflow for large populations; it is the method used in capacity planning of computer systems. The recursion (4.26) extends MVA from means to full marginal distributions, so a single pass over $N$ yields every nodal distribution.

All of these results are classical and proved in the literature; the book proves (4.26) itself. What the mission adds is a machine-checked development of them from the global balance equations: the product form with its uniqueness, the convolution identities, the marginal formulas, and the correctness of the MVA iteration as stated by the book, all over one shared definition layer. A search of the platform on 2026-09-28 found no formal statement of Buzen's algorithm or of MVA. The platform has Kelly's closed migration process theorem (KellyStochasticNetworks.closed_migration_equilibrium), which shows that the unnormalized product form satisfies the equilibrium equations under Kelly's conventions; the normalization, uniqueness and everything downstream of the product form are new here.

Difficulty

The combinatorial identities (Buzen's recursion, the tail marginal) are reindexings of finite sums over compositions of $N$; in Lean the work is in bijections between the state spaces $\{n_1+\cdots+n_k = N\}$ for different $k$ and $N$. The substantive step is uniqueness in the product-form theorem: the global balance equations have a one-dimensional solution space only because the chain on the $N$-customer states is irreducible on the population level, which is a property of the network chain and not of the routing matrix alone. The goal and MVA also need a positive solution of the traffic equations, which is not among the hypotheses and has to come from irreducibility of $R$. The book's own intuitive derivation of MVA via the arrival theorem is not the route the statements require; they are stated in terms of the steady-state distributions alone.

Formalization scope

Nodes are Fin k (book node $i$ is index $i-1$); states are n : Fin k → ℕ with ∑ i, n i = N, collected in a Finset, and all sums are finite. A distribution is a real function on $\mathbb N^k$ that is nonnegative, vanishes off the $N$-customer states and sums to one there. The balance equations are (4.14) verbatim with the book's boundary convention (p.188), not detailed balance. All results except Buzen's algorithm and (4.22) are for single-server nodes, as in the book; (4.13)'s multiserver factor $a_i(n)$ enters only (4.19)–(4.22).

Closed forms instantiated in the statements: the product form $G(N)^{-1}\prod_i\rho_i^{n_i}$ ((4.15)); $G(N)$ as the explicit sum (4.18)/(4.19); $a_i(n)$ from (4.13); $g_m$ from (4.20); $p_k(n) = f_k(n)g_{k-1}(N-n)/G(N)$ ((4.22)); $\bar P_i(n;N) = \rho_i^nG(N-n)/G(N)$ (p.208); $W_i(N) = (1+L_i(N-1))/\mu_i$ ((4.23)); $\lambda_l(N) = N/\sum_i v_iW_i(N)$ (MVA step (iii)(b)).

Two trivializing formalizations are ruled out: $\lambda_i(N)$ in (4.26) and (4.24) is the throughput computed from the steady-state distribution, not a free constant (which would make (4.26) a definition); and $g_m$ is defined by the sum (4.20), so the recursion (4.21) is a theorem rather than rfl. The product-form statement is an equivalence, so it asserts both that the product form is a steady state and that it is the only one.

Needed infrastructure: bijections between compositions of $N$ into $k$ and $k-1$ parts, uniqueness of stationary distributions of irreducible finite continuous-time chains (stated directly via the balance equations), and existence of positive solutions of $v = vR$ for irreducible stochastic $R$. The last two are reusable beyond this mission. Contributions welcome: proofs of the milestones in any order, and helper lemmas on these three points.

Not formalized: open Jackson networks (4.11) and Burke's theorem (4.5)–(4.6), multiclass networks (§4.2.1), the multiserver recursion (4.27) and cyclic queues (§4.4).

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §4.3, pp.195–209. https://doi.org/10.1002/9781118625651
• J. R. Jackson, "Jobshop-like queueing systems", Management Science 10(1), 1963. https://doi.org/10.1287/mnsc.10.1.131
• W. J. Gordon, G. F. Newell, "Closed queuing systems with exponential servers", Operations Research 15(2), 1967. https://doi.org/10.1287/opre.15.2.254
• J. P. Buzen, "Computational algorithms for closed queueing networks with exponential servers", Communications of the ACM 16(9), 1973. https://doi.org/10.1145/362342.362345
• M. Reiser, S. S. Lavenberg, "Mean-value analysis of closed multichain queuing networks", Journal of the ACM 27(2), 1980. https://doi.org/10.1145/322186.322195
• S. C. Bruell, G. Balbo, Computational Algorithms for Closed Queueing Networks, North-Holland, 1980.

Motivation

In many service systems a customer who finds every server busy does not join a queue. A caller who hears a busy signal hangs up and redials later; a request rejected by a saturated server is resent after a timeout; an aircraft that cannot land circles and tries again. These retrial queues are the subject of a substantial literature in telephone traffic engineering, computer networks and call-centre design, surveyed in the monograph of Falin and Templeton (1997) and the bibliography of Artalejo (1999). Their analysis is harder than that of ordinary queues: the blocked customers form an orbit whose size is part of the state, so even the simplest model is a two-dimensional Markov chain, and explicit stationary distributions are rare.

This mission is the fourth of a series formalizing Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008). Its goal is the explicit stationary distribution of the single-server retrial queue, Eq. (3.57) of §3.5.1, one of the few retrial models solvable in closed form. Chapter 3 of the book treats Markovian queues that are not birth–death processes: bulk arrivals, bulk service, Erlang phases, priority disciplines and retrials. The milestones also collect three capstone formulas from the chapter's other sections: the bulk-input queue, the partial-batch bulk-service queue, and Cobham's formula for nonpreemptive priorities (Cobham, 1954).

Setting

In the $M/M/1$ retrial queue customers arrive according to a Poisson process with rate $\lambda$ and are served one at a time by a single server, with exponential service times of mean $1/\mu$. An arrival that finds the server busy enters the orbit and stays there for an exponential time with mean $1/\gamma$, after which it tries again; each customer in orbit retries independently. No customer leaves because of impatience. With $N_s(t) \in \{0,1\}$ the number in service and $N_o(t)$ the number in orbit, the pair is a continuous-time Markov chain on states $\{i, n\}$, $i \in \{0,1\}$, $n \in \{0,1,2,\dots\}$. Writing $p_{i,n}$ for the steady-state probability of $\{i,n\}$, the rate-balance equations are

$$\begin{aligned} (\lambda + n\gamma)p_{0,n} &= \mu p_{1,n}, && n \ge 0, && (3.47)\\ (\lambda+\mu)p_{1,n} &= \lambda p_{0,n} + (n+1)\gamma p_{0,n+1} + \lambda p_{1,n-1}, && n \ge 1, && (3.48)\\ (\lambda+\mu)p_{1,0} &= \lambda p_{0,0} + \gamma p_{0,1}. && && (3.49) \end{aligned}$$

Following the book's convention (§1.9, and the footnote on p.118), a steady-state solution is a nonnegative solution of these equations whose total mass $\sum_n (p_{0,n} + p_{1,n})$ equals $1$. The traffic intensity is $\rho = \lambda/\mu$, and the partial generating functions are $P_0(z) = \sum_n z^n p_{0,n}$ and $P_1(z) = \sum_n z^n p_{1,n}$.

The other models of the mission use the same convention. In the bulk-input queue $M^{[X]}/M/1$, batches arrive at rate $\lambda$ with batch-size probabilities $c_n = \Pr\{X = n\}$, $n \ge 1$, and batch-size generating function $C(z) = \sum_n c_n z^n$. In the partial-batch bulk-service queue $M/M^{[K]}/1$, single arrivals come at rate $\lambda$ and the server serves up to $K$ customers together in an exponential time of mean $1/\mu$. In the nonpreemptive priority queue there are $r$ classes with rates $\lambda_k$ and $\mu_k$, loads $\rho_k = \lambda_k/\mu_k$ and cumulative loads $\sigma_k = \rho_1 + \cdots + \rho_k$.

Formalization targets

Goal: the stationary distribution (3.57)

For $\lambda, \mu, \gamma > 0$ and $\rho < 1$, the numbers

$$p_{0,n} = (1-\rho)^{(\lambda/\gamma)+1}\frac{\rho^n}{n!\,\gamma^n}\prod_{i=0}^{n-1}(\lambda+i\gamma), \qquad p_{1,n} = (1-\rho)^{(\lambda/\gamma)+1}\frac{\rho^{n+1}}{n!\,\gamma^n}\prod_{i=1}^{n}(\lambda+i\gamma)$$

form a steady-state solution of (3.47)–(3.49), and every steady-state solution equals them.

Milestones on the retrial queue

The generating functions satisfy (3.50)–(3.52) on $(-1,1)$, including the separable equation

$$P_0'(z) = \frac{\lambda\rho}{\gamma(1-\rho z)}P_0(z),$$

their closed form is (3.55),

$$P_0(z) = (1-\rho z)\left(\frac{1-\rho}{1-\rho z}\right)^{(\lambda/\gamma)+1}, \qquad P_1(z) = \rho\left(\frac{1-\rho}{1-\rho z}\right)^{(\lambda/\gamma)+1},$$

and the mean orbit size is (3.58), $L_o = \frac{\rho^2}{1-\rho}\cdot\frac{\mu+\gamma}{\gamma}$.

Milestones from the rest of Chapter 3

The bulk-input generating function (3.3), $p_0 = 1 - \rho$ with $\rho = \lambda\mathrm E[X]/\mu$, and the mean (3.4); the unique root $r_0 \in (0,1)$ of $\mu r^{K+1} - (\lambda+\mu)r + \lambda = 0$ and the geometric law $p_n = (1-r_0)r_0^n$ (3.9); and Cobham's formula (3.41)/(3.43), the unique solution of the linear system (3.40).

Significance

The closed form (3.57) makes every performance measure of the $M/M/1$ retrial queue explicit. The server is busy a fraction $\rho$ of the time, exactly as without retrials. The mean orbit size (3.58) is the $M/M/1$ mean queue length multiplied by $(\mu+\gamma)/\gamma$, and the mean time in orbit (3.59) follows from Little's law. These formulas quantify the cost of retrials against an ordinary queue and are the reference case against which approximations for multi-server retrial systems are checked.

The results are classical and proved in the book, partly through exercises (Problems 3.39–3.41). None of them is formalized in any proof assistant, as far as the platform's catalogue shows: there is no retrial, bulk or priority queue on Prove2Me. The mission produces machine-checked statements and, once solved, proofs of the chapter's main closed forms. It also produces a small reusable layer: generating functions of probability sequences on the closed unit disc, and the "probability solution of the balance equations" pattern for chains with countable state spaces.

Difficulty

The derivation in the book is formal. It differentiates power series term by term, divides by $1 - z$, integrates $\ln P_0$, and fixes the constant by setting $z = 1$, without justifying any of these steps. A formal proof has to show that the series converge and are differentiable on $(-1,1)$, that the differential equation determines $P_0$ up to a constant, and that the values at $z = 1$ are the limits of the values inside the disc (Abel's theorem). The uniqueness half of the goal is the hardest part. The book never proves it; it follows from the ODE argument only once every step is shown to hold for an arbitrary probability solution. Verifying that (3.57) solves (3.47)–(3.49) is only the easy half. The same pattern recurs in the bulk-input queue, where $z = 1$ is a removable singularity of (3.3). In the bulk-service queue the root $r_0$ is only characterized as the unique root in $(0,1)$, so existence and uniqueness of the root are part of the claim.

Formalization scope

A steady-state solution is a pair p0 p1 : ℕ → ℝ (resp. one sequence p : ℕ → ℝ) that is pointwise nonnegative, has total mass $1$ as a HasSum, and solves the book's balance equations exactly as printed, global balance and not detailed balance. Every "the steady-state solution is X" is stated with both halves: X is a steady-state solution, and every steady-state solution equals X. Stating only that (3.57) solves (3.47)–(3.49), without normalization or uniqueness, would be a trivializing formalization. So would taking $r_0$ as a given root in (3.9), or taking the $W_q^{(i)}$ in (3.41) as numbers assumed to satisfy it. None of these is used. The closed forms instantiated are (3.52), (3.55), (3.57), (3.58), (3.3), (3.4), (3.9), (3.41) and (3.43), each written out in full, with the real power $(1-\rho)^{(\lambda/\gamma)+1}$ as Real.rpow.

The conventions are as follows. The retrial generating functions take real arguments, on $(-1,1)$ for the differential equations and on $[-1,1]$ for the closed form. The bulk-input generating function takes complex arguments with $|z| \le 1$, $z \ne 1$, because (3.3) is $0/0$ at $z = 1$. The condition $\rho < 1$ is a hypothesis of every retrial statement. For the bulk-service queue the book's unnamed condition is stated as $\lambda < K\mu$. For bulk input, $\mathrm E[X] < \infty$ is assumed throughout, and the mean (3.4) is asserted under the further condition $\mathrm E[X^2] < \infty$, which it requires. For Cobham's formula only the algebraic content is formalized; the mean-value argument that yields (3.40) and (3.42) is not.

Needed infrastructure: power series of summable nonnegative sequences on the closed unit disc (convergence, term-by-term differentiation, Abel continuity), the binomial series $(1 - x)^{-a} = \sum_n \frac{a(a+1)\cdots(a+n-1)}{n!}x^n$ for real $a$, and uniqueness of invariant probability vectors for irreducible chains. All of this is reusable beyond the mission. Proofs of any milestone, of the easy half of the goal, or of the needed series facts are welcome contributions.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§3.1, 3.2.0.1, 3.4.2, 3.5.1. https://doi.org/10.1002/9781118625651
• G. I. Falin, J. G. C. Templeton, Retrial Queues, Chapman & Hall, 1997. https://doi.org/10.1007/978-1-4899-2977-8
• J. R. Artalejo, Accessible bibliography on retrial queues, Mathematical and Computer Modelling 30 (1999) 1–6. https://doi.org/10.1016/S0895-7177(99)00128-4
• A. Cobham, Priority assignment in waiting line problems, Journal of the Operations Research Society of America 2 (1954) 70–76. https://doi.org/10.1287/opre.2.1.70

Motivation

Steady-state formulas describe a queue that has been running forever. Many practical questions are about a queue that has not: a call centre just after opening, a server just after a reset, a system under a burst of load. For these, the relevant quantity is the transient distribution $p_n(t) = \Pr\{N(t) = n\}$ of the number $N(t)$ in the system at a finite time $t$. It is also what determines how fast the steady state is approached, and it is needed for the busy period: the length of time a server stays busy once a customer arrives at an idle server.

For the single-server Markovian queue M/M/1 the transient distribution has an explicit closed form in modified Bessel functions. Its history is short and well documented. Ledermann and Reuter (1954) obtained it by spectral analysis of the birth–death process. Bailey (1954) found it by generating functions and Laplace transforms, and Champernowne (1956) by combinatorial methods. Bailey's route is the standard textbook derivation, and it is the one Gross, Shortle, Thompson and Harris outline in §2.11 of Fundamentals of Queueing Theory (4th ed., 2008). Abate and Whitt (1989) showed that computing with the resulting series is numerically delicate, which is one reason for having the formula pinned down exactly.

This mission formalizes §§2.11–2.12 of that book: the transient laws of M/M/1/1, M/M/1 and M/M/∞, and the M/M/1 busy period.

Setting

Customers arrive in a Poisson stream of rate $\lambda > 0$. Each service takes an exponential time of rate $\mu > 0$, and $\rho = \lambda/\mu$. The number in the system is a continuous-time Markov chain on $\{0, 1, 2, \dots\}$, and its state probabilities $p_n(t)$ satisfy the forward (differential–difference) equations. For M/M/1 started with $N(0) = i$ they are, for $t \ge 0$,

$$p_n'(t) = -(\lambda+\mu)p_n(t) + \lambda p_{n-1}(t) + \mu p_{n+1}(t)\ (n > 0), \qquad p_0'(t) = -\lambda p_0(t) + \mu p_1(t), \tag{2.72}$$

with $p_n(0) = 1$ if $n = i$ and $0$ otherwise. The other systems are variants:

• M/M/1/1, no waiting room: two states and equations (2.70).
• M/M/∞, ample service: the death rate in state $n$ is $n\mu$, giving (2.76).
• The busy-period system: (2.72) with $0$ made absorbing ($\lambda_0 = 0$) and $N(0) = 1$. Its $p_0(t)$ is the distribution function of the busy period $T_{bp}$.

A family $(p_n)$ solves a system on $[0,\infty)$ when each $p_n$ has, at every $t \ge 0$, the prescribed derivative (a right derivative at $t = 0$). It is a probability solution when $p_n(t) \ge 0$ and $\sum_n p_n(t) = 1$ for every $t \ge 0$. The modified Bessel function of the first kind is

$$I_n(y) = \sum_{k=0}^{\infty} \frac{(y/2)^{n+2k}}{k!\,(n+k)!}, \qquad I_{-n} = I_n,$$

and the Laplace transform of $f$ is $\bar f(s) = \int_0^\infty e^{-st} f(t)\,dt$ for $\operatorname{Re} s > 0$.

Formalization targets

Goal: the transient M/M/1 law, (2.75)

With $y = 2t\sqrt{\lambda\mu}$,

$$p_n(t) = e^{-(\lambda+\mu)t}\Big[\rho^{(n-i)/2} I_{n-i}(y) + \rho^{(n-i-1)/2} I_{n+i+1}(y) + (1-\rho)\rho^n \sum_{j=n+i+2}^{\infty} \rho^{-j/2} I_j(y)\Big].$$

The goal asserts five things for every $\lambda, \mu > 0$ and every $i$, with no restriction on $\rho$:

1. the series converges;
2. these functions solve (2.72);
3. they meet the initial condition;
4. they form a probability distribution at every $t$;
5. they are the only probability solution.

Milestones

1. (2.71): the M/M/1/1 solution $p_1(t) = \frac{\lambda}{\lambda+\mu}(1-e^{-(\lambda+\mu)t}) + p_1(0)e^{-(\lambda+\mu)t}$, and the matching formula for $p_0$.
2. (2.74) and Rouché's theorem: for $\operatorname{Re} s > 0$, the quadratic $(\lambda+\mu+s)z - \mu - \lambda z^2$ has exactly one zero in $|z| < 1$, namely $z_1 = (\lambda+\mu+s-\sqrt{(\lambda+\mu+s)^2-4\lambda\mu})/(2\lambda)$.
3. The transform of $p_0$: $\bar p_0(s) = z_1^{i+1}/(\mu(1-z_1))$.
4. The limit of (2.75): $p_n(t) \to (1-\rho)\rho^n$ if $\rho < 1$, and $p_n(t) \to 0$ if $\rho \ge 1$.
5. (2.77), M/M/∞: started empty, $p_n(t) = a(t)^n e^{-a(t)}/n!$ with $a(t) = (1-e^{-\mu t})\lambda/\mu$. The statement says that this family solves (2.76), is the unique probability solution, and has generating function $\exp((z-1)a(t))$.
6. The busy-period transform: $\bar p_0(s) = 2\mu/(s[\lambda+\mu+s+\sqrt{(\lambda+\mu+s)^2-4\lambda\mu}])$.
7. The busy-period density: $p_0'(t) = \sqrt{\mu/\lambda}\,e^{-(\lambda+\mu)t} I_1(2\sqrt{\lambda\mu}\,t)/t$.
8. (2.79): for $\lambda < \mu$, $E[T_{bp}] = 1/(\mu-\lambda)$ and $E[T_{bc}] = 1/\lambda + 1/(\mu-\lambda)$.

Significance

The formula (2.75) is the exact finite-time law of the most basic queue. It gives the rate at which M/M/1 approaches equilibrium, and it gives the distribution of the queue under overload ($\rho \ge 1$), where no steady state exists. It is the reference against which numerical transient methods, such as the uniformization of Chapter 8 of the same book, are checked. The busy-period density and its mean (2.79) enter server-utilisation and vacation models, and the Laplace-transform method used here recurs in the M/G/1 analysis of Chapter 5.

All of these results are classical and proved in the literature. None of them is machine-checked, as far as the platform's catalogue and Mathlib show. The chain from a countable system of linear ODEs, through generating functions and a root-location argument, to a Bessel series is a standard pattern in applied probability, and a formal version of it is what this mission adds. The formal statements also make explicit what the book leaves implicit: the sense in which the equations hold at $t = 0$, and the class in which the solution is unique.

Difficulty

The forward equations (2.72) form an infinite linear system. The obvious approach is to treat it like a finite system of ODEs, whose solution is a matrix exponential, and read off (2.75). That fails for two reasons. The generator is an infinite matrix, so its exponential needs a functional-analytic setting. And uniqueness is not automatic for infinite systems: it needs a class, such as probability solutions, and an argument that works in that class.

The Bessel form is a second, independent difficulty. The transform $\bar p_0(s)$ is fixed by a root-location argument in the complex plane. Inverting the transform, or verifying (2.75) directly, requires manipulating the three-term Bessel recurrence and exchanging infinite sums. The tail sum $\sum_{j} \rho^{-j/2} I_j$ has to be controlled uniformly enough to be differentiated term by term. For $\rho \ge 1$ the factor $(1-\rho)$ is non-positive, so the nonnegativity of $p_n(t)$ is not visible from the formula.

Formalization scope

Conventions committed to:

• Parameters. Rates are real with $\lambda, \mu > 0$, and $\rho = \lambda/\mu$. States are ℕ (Fin 2 for M/M/1/1).
• Solutions. "Solves on $[0,\infty)$" is HasDerivWithinAt on Set.Ici 0 at every $t \ge 0$. Uniqueness is asserted among solutions that are probability distributions at every time.
• Special functions. Half-integer powers of $\rho$ are real powers, and $I_{-m} = I_m$ is part of the definition. Laplace transforms are complex Bochner integrals over $(0,\infty)$, and each statement also asserts the integrability it needs. Square roots with positive real part are hypotheses $r^2 = (\lambda+\mu+s)^2 - 4\lambda\mu$, $\operatorname{Re} r > 0$.

The closed forms stated exactly as in the book are:

• (2.71);
• $z_1$ and $z_2$ of (2.74);
• $\bar p_0(s) = z_1^{i+1}/(\mu(1-z_1))$;
• (2.75), with the Bessel series of p.101;
• the M/M/∞ law and (2.77);
• the busy-period transform and density of p.102;
• (2.79).

The book derives (2.79) by a steady-state ratio argument valid for M/G/1. Here it is stated for M/M/1, as the mean of the explicit density.

A statement of (2.75) that only asserts the right-hand side is well defined, or checks only $n = 0$, is ruled out: the goal requires the ODE system, the initial condition, the probability property and uniqueness. For the same reason, the M/M/∞ law is tied to the system (2.76) and does not reduce to a Taylor expansion.

Needed infrastructure that Mathlib lacks:

• modified Bessel functions of integer order;
• Laplace transforms;
• a Rouché-type zero count or a direct root-location lemma;
• uniqueness for countable linear ODE systems with bounded or linearly growing rates.

The Bessel and Laplace definitions, and the uniqueness lemma for birth–death forward equations, are reusable beyond this mission. Contributions of those as separate lemmas are welcome.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§2.11–2.12, pp.97–103. https://doi.org/10.1002/9781118625651
• N. T. J. Bailey, "A continuous time treatment of a simple queue using generating functions", J. Royal Statistical Society B 16 (1954) 288–291. https://doi.org/10.1111/j.2517-6161.1954.tb00172.x
• W. Ledermann, G. E. H. Reuter, "Spectral theory for the differential equations of simple birth and death processes", Phil. Trans. Royal Society A 246 (1954) 321–369. https://doi.org/10.1098/rsta.1954.0001
• D. G. Champernowne, "An elementary method of solution of the queueing problem with a single server and constant parameters", J. Royal Statistical Society B 18 (1956) 125–128. https://doi.org/10.1111/j.2517-6161.1956.tb00217.x
• J. Abate, W. Whitt, "Calculating time-dependent performance measures for the M/M/1 queue", IEEE Trans. Communications 37 (1989) 1102–1104. https://doi.org/10.1109/26.41165

Why birth–death queues and Erlang's formulas

Every call center, hospital ward, cloud server pool and telephone exchange that is sized by formula is sized by one of a handful of explicit expressions from Markovian queueing theory. The two oldest are A. K. Erlang's: the Erlang-B (loss) formula of 1917, which gives the fraction of calls lost when $c$ trunks carry an offered load of $r$ erlangs, and the Erlang-C formula, which gives the probability that a customer of a $c$-server queue must wait. Both are still the default dimensioning rules of telecommunications and call-center workforce management (Gans, Koole & Mandelbaum 2003).

This mission formalizes Chapter 2, §§2.1–2.10, of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory, 4th ed. (Wiley 2008), which derives these formulas from a single result about birth–death processes and closes with the modern answer to the staffing question.

Timeline. Erlang (1917) obtained the loss formula; Vaulot (1927), Pollaczek (1932), Palm (1938) and Kosten (1948) completed its proof for general service times. Halfin and Whitt (1981) showed that in the $M/M/n$ queue the delay probability converges to a limit strictly between $0$ and $1$ exactly when the number of servers exceeds the offered load by an amount of order $\sqrt n$. This is the quality-and-efficiency-driven (QED) regime on which square-root staffing rests.

Setting

A birth–death process is a continuous-time Markov chain on the states $n \in \{0, 1, 2, \dots\}$ that moves from $n$ to $n+1$ at rate $\lambda_n \ge 0$ (a birth, or arrival) and, for $n \ge 1$, from $n$ to $n-1$ at rate $\mu_n > 0$ (a death, or departure). A steady-state solution is a probability sequence $\{p_n\}$ ($p_n \ge 0$, $\sum_n p_n = 1$) solving the global balance equations (2.1):

$$(\lambda_n + \mu_n)p_n = \lambda_{n-1}p_{n-1} + \mu_{n+1}p_{n+1}\ (n \ge 1), \qquad \lambda_0 p_0 = \mu_1 p_1.$$

The queues of the chapter are birth–death processes with particular rates. The $M/M/1$ queue has $\lambda_n = \lambda$, $\mu_n = \mu$ and traffic intensity $\rho = \lambda/\mu$. The $M/M/c$ queue has $\lambda_n = \lambda$, $\mu_n = \min(n, c)\mu$ (2.30), offered load $r = \lambda/\mu$ and $\rho = r/c$. The $M/M/c/c$ loss system is the same with $\lambda_n = 0$ for $n \ge c$. The $M/M/\infty$ queue has $\mu_n = n\mu$.

The explicit functions are the Erlang-B formula

$$B(c, r) = \frac{r^c/c!}{\sum_{i=0}^{c} r^i/i!},$$

the Erlang-C formula, defined for $\rho = r/c < 1$,

$$C(c, r) = \frac{r^c/(c!(1-\rho))}{r^c/(c!(1-\rho)) + \sum_{n=0}^{c-1} r^n/n!},$$

and, with $\phi$, $\Phi$ the standard normal density and distribution function,

$$\alpha(\beta) = \frac{\phi(\beta)}{\phi(\beta) + \beta\Phi(\beta)}.$$

Formalization targets

Goal: the Halfin–Whitt theorem (§2.4, p.75)

For offered loads $0 < r_n < n$,

$$\lim_{n\to\infty} C(n, r_n) = \alpha \in (0,1) \iff \lim_{n\to\infty} \frac{n - r_n}{\sqrt n} = \beta > 0, \qquad \alpha = \alpha(\beta).$$

It is stated as three facts: $\alpha$ maps $(0, \infty)$ into $(0, 1)$; each $\alpha \in (0, 1)$ has exactly one preimage $\beta > 0$; and for every $\beta > 0$ the two limits are equivalent.

Milestones

1. (2.3)–(2.4): the steady-state solution of a general birth–death process, $p_n = p_0\prod_{i=1}^n \lambda_{i-1}/\mu_i$, and its existence if and only if $1 + \sum_{n\ge1}\prod_{i=1}^n \lambda_{i-1}/\mu_i < \infty$.
2. (2.9): $M/M/1$, $p_n = (1-\rho)\rho^n$, existing iff $\rho < 1$.
3. (2.31)–(2.32): the $M/M/c$ law, existing iff $\lambda/(c\mu) < 1$.
4. (2.33): $L_q = r^c\rho\,p_0/(c!(1-\rho)^2)$.
5. (2.37)–(2.38): $1 - \sum_{n<c} p_n = C(c, r)$.
6. (2.52)–(2.53): the $M/M/c/c$ law and $p_c = B(c, r)$.
7. (2.54): $B(c, r) = rB(c-1, r)/(c + rB(c-1, r))$, $B(0, r) = 1$.
8. (2.55): $C(c, r) = cB(c, r)/(c - r + rB(c, r))$.
9. (2.57): $M/M/\infty$, $p_n = r^n e^{-r}/n!$.

Significance

The results. Items 1–9 are the working formulas of Markovian capacity planning: a stationary law for each basic model and the measures read off from it. (2.54) and (2.55) are how $B$ and $C$ are computed in practice, since the factorials of the closed forms overflow for $c > 170$. The Halfin–Whitt theorem is the reason the rule $c \approx r + \beta\sqrt r$ holds a fixed service level, and it is the entry point to the QED heavy-traffic literature (diffusion limits of many-server queues, Garnett–Mandelbaum–Reiman, Gamarnik–Momčilović).

Formalizing them. All results are classical and proved in the literature. The book states the Halfin–Whitt theorem without proof, and (2.54)–(2.55) are left to exercises. The formalization would supply machine-checked versions of the Erlang identities and of the Halfin–Whitt limit theorem. No Lean development of either was found on the platform when this mission was drafted. A related Erlang-B statement from Kelly and Yudovina is on the platform, stated with detailed balance on a finite state space.

Difficulty

The stationary laws are induction plus geometric and exponential series, and the Erlang identities are finite algebra. The difficulty is concentrated in the goal. $C(n, r_n)$ is a ratio of a Poisson-type tail to a truncated exponential sum in which both $n$ and $r_n$ grow. The naive route, substituting Stirling's formula term by term, fails: the sums have $\Theta(\sqrt n)$ significant terms, each of relative size $\exp(-k^2/2n)$, and the error has to be controlled uniformly over them. The converse direction also requires showing that $\alpha(\cdot)$ is strictly monotone. Without that, convergence of $C(n, r_n)$ does not force convergence of $(n - r_n)/\sqrt n$.

Formalization scope

Rates are real sequences indexed by $\mathbb N$, and a steady-state solution is a real sequence with HasSum p 1, nonnegative entries, and the balance equations (2.1) exactly as printed (global balance, not detailed balance). Every "the steady-state solution is X" is stated in both halves: X is a steady-state solution, and every steady-state solution equals X; the book's existence conditions ($\rho < 1$, $\lambda/(c\mu) < 1$, convergence of the series) are part of the statements. The $M/M/c/c$ system is the $\mathbb N$-indexed process with $\lambda_n = 0$ for $n \ge c$, as §2.5 sets it up; the statement records that states above $c$ carry no mass.

The closed forms that are fixed in Lean: $\prod_{i=1}^n \lambda_{i-1}/\mu_i$ over Finset.Icc 1 n; $B(c, r)$ and $C(c, r)$ exactly as displayed above; $\phi$ = gaussianPDFReal 0 1, $\Phi$ = the CDF of gaussianReal 0 1; $W_q(0) = \sum_{n=0}^{c-1} p_n$, as evaluated on p.69; $L_q = \sum_{n > c}(n - c)p_n$ as a convergent series.

$C(c, r)$ is a total function in Lean, but its value for $r \ge c$ carries no meaning. The goal assumes $0 < r_n < n$ for $n \ge 1$, the book's standing condition $\rho < 1$. A statement about some other function with the same limiting behaviour, or with $B$ and $C$ left abstract, would not be this mission. Neither would one-directional or existence-only versions of the stationary laws.

Not included: the waiting-time distributions (2.28) and (2.39), which need an FCFS waiting-time model with arrival-point probabilities; the $M/M/c/K$ measures (2.45)–(2.48); finite-source and state-dependent models (§§2.8–2.10). Useful contributions beyond the milestones are Poisson tail estimates at the $\sqrt n$ scale and monotonicity of $\alpha(\beta)$. Both are reusable in other many-server heavy-traffic statements.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• N. Gans, G. Koole, A. Mandelbaum, Telephone call centers: tutorial, review, and research prospects, Manufacturing & Service Operations Management 5(2), 79–141, 2003. https://doi.org/10.1287/msom.5.2.79.16071
• A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektroteknikeren 13, 1917 (English translation in The Life and Works of A. K. Erlang, 1948).
• F. P. Kelly, E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781139565363

Strassen's Theorems and the Stochastic Ordering of Queues

Background

Chapters 1–3 of Baccelli and Brémaud's Elements of Queueing Theory compute exact quantities: Palm identities, stability criteria, PASTA, Pollaczek–Khinchin. Chapter 4 asks a different question. When you cannot compute a queue, can you at least say it is better than another one?

That requires an order on distributions. The chapter builds a family of them — integral orders — by choosing a class ℒ of test functions and declaring F ≤_ℒ G when ∫f dF ≤ ∫f dG for all f ∈ ℒ. Three matter: {i} the non-decreasing functions, giving the strong (stochastic) order; {cx} the convex functions, giving the convex order; and their intersection {icx}.

The goal

An integral order compares two distributions that need not live on the same probability space, and that is both its convenience and its difficulty. Strassen's theorems say each of these orders is secretly a statement about a coupling.

Theorem 4.2.2 (p.278), Strassen's ≤_cx theorem:

F ≤_cx G   ⟺   ∃ X ~ F, Y ~ G on one space with  E[Y | X] = X  a.s.
F ≤_icx G  ⟺   the same with  E[Y | X] ≥ X  a.s.

The convex order holds exactly when G is a martingale dilation of F — obtained by spreading each point out without moving its conditional mean. That is what makes the order usable: comparison results for queues become induction arguments on a coupling instead of analytic manipulations of convolutions of c.d.f.'s.

Its companion Theorem 4.2.1 is the ≤_st version, where the coupling is the simpler X ≤ Y a.s. In dimension one both are explicit — take X = F⁻¹(U), Y = G⁻¹(U) for a uniform U. In dimension n there is no such formula, and that is why these are Strassen's theorems. The book attributes both to Strassen (1965) and proves neither.

Why FIFO is optimal

§4.1 is a different kind of comparison: not between two queues, but between two service disciplines for the same queue. The order there is majorization ≺, which compares how spread out two vectors of the same total are.

The answer is that FIFO minimizes E⁰[f(V)] for every convex f (Property 4.1.3), and the proof is an interchange argument. Under any non-preemptive discipline that uses no information on the service times, customer k effectively receives service σ_{γ(k)} for some permutation γ; Lemma 4.1.3 shows the same queue is produced by FIFO fed with that reordered input, and that the reordering does not change the law of the input. Lemma 4.1.4 passes to the limit, which needs ρ < 1. Lemmas 4.1.1 and 4.1.2 then do the combinatorics: undoing one inversion of γ makes the waiting-time vector less spread out, so the identity permutation — FIFO — is extremal.

Feller's paradox, and what survives it

§4.4 compares time-stationary queues, and opens with a warning. T_n[P⁰] ≤_i T̃_n[P̃⁰] for every n does not imply T_n[P] ≤_i T̃_n[P̃]: Example 4.4.1, "Feller's paradox revisited", exhibits a Poisson process and a renewal process where the Palm order holds and the stationary one fails. The order does not pass from the Palm probability to the stationary one.

For ≤_cx it does. Lemma 4.4.1 is why: it expands E_P[f(N[0,x))] as a series of second differences of f against Palm expectations, and a convex f makes every coefficient non-negative. Lemma 4.4.2 handles the S-orders, built by dividing Palm integrals by the mean cycle length, and shows that the normalisation does not hide the comparison it normalises by.

Formalization scope

• Orders. ≤_i, ≤_cx, ≤_icx on distributions on ℝⁿ are integral orders over the book's test classes (§4.2.1), with the page's qualification that only test functions with well-defined integrals count. Majorization ≺ is (4.1.2) with increasing reorderings of both vectors.
• Strassen. Both theorems are stated as equivalences, with the coupling existential over the probability space. Theorem 4.2.2 carries both clauses — E[Y | X] = X for ≤_cx, E[Y | X] ≥ X for ≤_icx, as conditional expectations given σ(X) — and assumes both distributions integrable; Theorem 4.2.1 has no integrability hypothesis. A one-directional statement (the Jensen half) is not the theorem.
• The queue of §4.1.3 is constructed: a GI/GI input (i.i.d. inter-arrival and service times, independent), a single work-conserving server started empty, and any non-preemptive discipline whose choices are measurable in the information the book's σ-field 𝒢_t carries (arrivals, service times of customers already started) plus external randomisation. FIFO is one such discipline. The interchange permutations γ_n and their limit γ are built from the schedule as on pp.268–270; Lemma 4.1.4 assumes ρ = E[σ₀]/E[τ₀] < 1.
• Lemma 4.4.1 is stated with the exact second-difference series and assumes that series converges absolutely; the page states it for all f, which fails for heavy-tailed counts and sparse f.
• The S-orders test against {I-ℒ} — primitives ∫_0^t f(u, x) du of test functions — and apply only to distributions whose first coordinate is a.s. positive with a finite mean.

What this mission provides

None of it exists. Mathlib has no stochastic order, no convex order, no increasing-convex order, no majorization, no Schur-convexity and no Strassen theorem; the platform returns zero hits for q=stochastic ordering. Everything in this chapter is new substrate — and §§4.1–4.2 need nothing from Palm calculus, so this mission can be read on its own.

Motivation

Average cost control of queues rests on a small amount of Markov chain theory: when does a chain with costs have a well defined long-run average cost, and how can that be checked for a concrete model with an unbounded state space? Appendix C of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) collects this material for countable state spaces and packages it in one hypothesis, the $z$ standard chain. Chapters 7–10 of the book verify this hypothesis for the Markov chains induced by stationary policies in admission, routing and service-rate control models, and use its consequences to prove existence of average cost optimal policies.

The tools are Lyapunov functions in the sense of Foster (1953): a nonnegative function on the states whose expected one-step change is negative away from a finite set. Foster's criterion for positive recurrence, and its refinements bounding expected first passage times and costs, are the standard way to verify stability of queueing networks (Meyn and Tweedie, Markov Chains and Stochastic Stability, 1993/2009).

Setting

A Markov chain $\Gamma$ on a countable set $S$ is given by transition probabilities $P_{ij}\ge 0$ with $\sum_j P_{ij}=1$. $X_t$ is the state at time $t$ and $P^{(t)}_{ij}$ the $t$-step transition probability ($P^{(0)}_{ij}=\delta_{ij}$). State $i$ leads to $j$ if $P^{(t)}_{ij}>0$ for some $t\ge0$; states that lead to each other communicate, which partitions $S$ into communicating classes.

For a nonempty $G\subseteq S$ the first passage time from $i$ is $T_{iG}=\min\{t\ge1: X_t\in G\}$ given $X_0=i$, and $m_{iG}=E[T_{iG}]\in[0,\infty]$; $m_{ij}$ is the case $G=\{j\}$ and $m_{ii}$ the expected return time. The taboo probability $_G P^{(t)}_{ik}$ is the probability of going from $i$ to $k$ in $t$ steps without visiting $G$ at the intermediate times, and $_G u_{ik}$ is the expected number of visits to $k$ at times $0\le t<T_{iG}$. A state is transient if $P(T_{ii}<\infty)<1$ and positive recurrent if $m_{ii}<\infty$; a positive recurrent class is a communicating class of positive recurrent states. The steady state probability is $\pi_j=(m_{jj})^{-1}$ (zero when $m_{jj}=\infty$).

Each state carries a finite cost $C(i)\ge0$. The expected average cost over $[0,n-1]$ from $i$ is

$$J^{(n)}_i=\frac1n\,E\Big[\sum_{t=0}^{n-1}C(X_t)\,\Big|\,X_0=i\Big]=\frac1n\sum_{t=0}^{n-1}\sum_j P^{(t)}_{ij}C(j),$$

$c_{iG}$ is the expected cost $E[\sum_{t=0}^{T_{iG}-1}C(X_t)\mid X_0=i]$ of a first passage (defined when $m_{iG}<\infty$), and $J_R=\sum_{j\in R}\pi_jC(j)$ is the average cost on a positive recurrent class $R$. The chain is $z$ standard (Definition C.2.5) if for a distinguished state $z$

$$m_{iz}<\infty\quad\text{and}\quad c_{iz}<\infty\qquad\text{for all } i\in S.$$

Formalization targets

Goal: Proposition C.2.6

If $\Gamma$ is $z$ standard, then $S$ is the union of a positive recurrent class $R\ni z$ and a set of transient states, $J_R<\infty$, and

$$\lim_{n\to\infty}J^{(n)}_i=J_R\qquad\text{for every } i\in S.$$

The statement fixes no constants: it asserts that the average cost exists, is finite, and does not depend on the initial state.

Milestones

1. Proposition C.1.2: $\pi$ is the unique stationary distribution of a positive recurrent class, and $\pi_j=e_{ij}/m_{ii}=\pi_ie_{ij}$.
2. Proposition C.1.4: the first-step equations (C.2)–(C.4) for taboo probabilities, visit counts and $m_{iG}$; $\sum_{i\in G}\pi_im_{iG}=1$ for $G$ inside a positive recurrent class; $m_{ij}<\infty$ within such a class.
3. Proposition C.1.5: if $\sum_jP_{ij}[y(j)-y(i)]\le-\epsilon$ off $G$, then $m_{iG}\le y(i)/\epsilon$.
4. Corollary C.1.6: the same with $G=\{z\}$ and $\sum_jP_{zj}y(j)<\infty$ makes $z$ positive recurrent.
5. Proposition C.2.1: on a positive recurrent class, $J^{(n)}_i\to J_R=c_{ii}/m_{ii}$.
6. Proposition C.2.2: $c_{iG}=\sum_kC(k)\,{}_Gu_{ik}$, the first-step equation (C.13), and $J_R=\sum_{i\in G}\pi_ic_{iG}$.
7. Proposition C.2.3 and Corollary C.2.4: the cost drift condition $\sum_jP_{ij}[r(j)-r(i)]\le-C(i)$ off a finite set bounds $c_{iG}\le r(i)+Fm_{iG}$, and gives $c_{zz}<\infty$.
8. Remark C.2.7: the hypotheses of C.1.6 and C.2.4 together imply the chain is $z$ standard; so do irreducibility, positive recurrence and finite average cost.

Significance

Proposition C.2.6 is what makes the $z$ standard hypothesis useful: an average cost criterion that is a genuine limit, finite, and independent of the initial state, even for chains with transient states and unbounded state spaces. Every average cost optimality result of the book that works with a stationary policy's induced chain (the (SEN) and (BOR) assumption sets, the approximating-sequence method, the continuous-time chapter) calls on this proposition or on the Lyapunov criteria of Remark C.2.7 to establish its hypotheses for queueing models.

All results of the mission are classical and proved in the literature; parts are stated in the book without proof and referred to Chung (1967), Grassmann et al. (1985) and renewal theory. None of them has been machine-checked in this form as far as the platform and Mathlib show: Mathlib has kernels and Ionescu-Tulcea trajectories but no countable-state Markov chain classification, no first passage calculus, and no Foster–Lyapunov criterion. Existing platform results on countable chains (the Levin–Peres–Wilmer series) treat irreducible chains without costs. A complete development here produces a reusable library of first passage identities, Foster–Lyapunov bounds for times and costs, and average cost limits on reducible chains.

Difficulty

The Lyapunov bounds (C.1.5, C.2.3) are telescoping arguments, but they require a clean handling of truncated passages and of sums that may be infinite: (C.7) is an inequality between possibly divergent series, and the step "iterate $n$ times and let $n\to\infty$" must be made rigorous for $[0,\infty]$-valued expectations.

The central difficulty is part (iii) of the goal for transient initial states. On the class $R$, the limit of $J^{(n)}_i$ is a renewal reward theorem over successive returns to $z$; from a transient state the first cycle has a different law, so a delayed renewal reward argument is needed, and it has to cover the case where costs are unbounded. The obvious approach, bounding $J^{(n)}_i$ between $J_R$ and the average over the first $n$ steps of the chain started in $z$, fails because $P^{(t)}_{ij}$ need not converge (periodic classes) and because finite $c_{iz}$ does not bound individual cost terms. Proposition C.1.2's uniqueness and the Kac-type identity of C.1.4(iv) likewise need the full cycle decomposition of a positive recurrent class.

Formalization scope

The chain is a structure MC S with P : S → S → ℝ≥0∞ and ∑' j, P i j = 1, over a countable type S; costs are C : S → ℝ≥0. Probabilities and expectations are ℝ≥0∞-valued sums over finite paths Fin (t+1) → S, so every quantity is defined without summability side conditions and may be $\infty$. The first passage time is $T_{iG}\ge1$; $m_{iG}$ is the expectation of $T_{iG}$ from its law (and $\infty$ when $P(T_{iG}<\infty)<1$), not defined by the recursion (C.4), so that (C.4) is a theorem. $_Gu_{ik}$ counts visits at times $0\le t<T_{iG}$. $c_{iG}$ is computed over first passage paths and is used only when $m_{iG}<\infty$, as in the book. $\pi_j$ is $(m_{jj})^{-1}$, which the book states equals the Cesàro limit $\lim_nQ^{(n)}_{jj}$. $J^{(n)}_i$ is meaningful for $n\ge1$, and limits are taken in $[0,\infty]$. The drift conditions $\sum_jP_{ij}[y(j)-y(i)]\le-\epsilon$ and $\sum_jP_{ij}[r(j)-r(i)]\le-C(i)$ are written in the equivalent additive form $\sum_jP_{ij}y(j)+\epsilon\le y(i)$, which is equivalent for finite $y$ and makes the case $\sum_jP_{ij}y(j)=\infty$ fail, as it does in the book.

A trivializing formalization, such as defining $m_{iG}$ or $c_{iG}$ by the equations (C.4) or (C.13), defining $J_R$ as the limit of $J^{(n)}_i$, or allowing a $z$ standard chain whose return time or return cost to $z$ is infinite, is ruled out: $z$ standard requires $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$ including $z$, and each quantity is defined from path probabilities.

Needed infrastructure: path-sum manipulation in $[0,\infty]$ (first-step and last-step decompositions), the ratio limit / renewal reward theorem for a positive recurrent class, and the delayed version for transient starts. The first passage calculus and the Lyapunov bounds are reusable by the book's other chapters on average cost, which state the $z$ standard property for policy-induced chains. Contributions of lemmas on path sums and of an independent renewal reward library are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, pp. 292–302. doi:10.1002/9780470317037
• K. L. Chung, Markov Chains with Stationary Transition Probabilities, 2nd ed., Springer, 1967. doi:10.1007/978-3-642-62015-7
• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953), 355–360. doi:10.1214/aoms/1177728976
• S. P. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, 2nd ed., Cambridge University Press, 2009. doi:10.1017/CBO9780511626630
• D. P. Heyman and M. J. Sobel, Stochastic Models in Operations Research, Vol. I, McGraw-Hill, 1982.

Motivation

Many queueing systems evolve in continuous time: customers arrive according to a Poisson process, services take exponentially distributed times, and a controller may change the service rate, admit or reject customers, or route them whenever the state changes. Minimizing the long-run average cost of such a system is a standard problem in the control of queues (Lippman 1975; Puterman 1994, Ch. 11; Sennott 1999, Ch. 10). The continuous time model does not fit directly into the discrete time theory of Markov decision chains developed in the earlier chapters of Sennott's book, because time spent in a state now matters and the natural average cost is a ratio of expected cost to expected elapsed time.

This mission formalizes Sections 10.1–10.4 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999): the elementary properties of the exponential distribution, the continuous time Markov decision chain and its average cost, a reduction of the continuous time problem to an auxiliary discrete time Markov decision chain, and the theorem stating that finite state approximating sequences of the auxiliary chain compute optimal average costs and optimal stationary policies of the continuous time chain. The chapter closes with an explicit average cost computation for the M/M/1 queue with service rate control.

Setting

A random variable $X$ has the exponential distribution with rate $\mu>0$ if $P(X\le t)=1-e^{-\mu t}$ for $t\ge0$. A function $r(\delta)$ is $o(\delta)$ if $r(\delta)/\delta\to0$ as $\delta\to0^+$.

A continuous time Markov decision chain (CTMDC) $\Psi$ has a countable state space $S$ and, for each $i\in S$, a finite nonempty action set $A_i$. Choosing $a\in A_i$ in state $i$ incurs an instantaneous cost $G(i,a)\ge0$ and a cost rate $g(i,a)\ge0$ in effect until the next transition. The time until the next transition is exponential with rate $\nu(i,a)>0$, so its mean is $\tau(i,a)=1/\nu(i,a)$; the next state is $j$ with probability $P_{ij}(a)$, where $P_{ii}(a)=0$. A policy $\theta$ chooses, at each transition, an action (possibly at random) from the history of past states, actions and sojourn times; a stationary policy $e$ chooses $e(i)$ in state $i$. With $C_n$ the cost and $T_n$ the time of the first $n$ transition periods, the average cost and the minimum average cost are

$$J^\Psi_\theta(i)=\limsup_{n\to\infty}\frac{E_\theta[C_n\mid X_0=i]}{E_\theta[T_n\mid X_0=i]},\qquad J^\Psi(i)=\inf_\theta J^\Psi_\theta(i).$$

Assumption (CTB) requires constants $\tau$ and $B$ with $0<\tau<\inf_{i,a}\tau(i,a)\le\sup_{i,a}\tau(i,a)\le B<\infty$. The auxiliary MDC $\Delta$ has the same states and actions, costs $C(i,a)=G(i,a)\nu(i,a)+g(i,a)$, and transition probabilities $P^*_{ij}(a)=\tau\nu(i,a)P_{ij}(a)$ for $j\ne i$, $P^*_{ii}(a)=1-\tau\nu(i,a)$. Its average cost $J^\Delta_\theta(i)=\limsup_n n^{-1}\sum_{t<n}E_\theta[C(X_t,Y_t)]$ and minimum average cost $J^\Delta(i)$ are those of Chapter 2. Assumption (CTAC) is $J^\Delta(\cdot)\le J^\Psi(\cdot)$.

An approximating sequence $(\Delta_N)_{N\ge N_0}$ for $\Delta$ uses finite state spaces $S_N$ increasing to $S$ and transition probabilities $P^*_{ij}(a;N)$ on $S_N$ converging to $P^*_{ij}(a)$. The (AC) assumptions ask for constants $J^N$ and functions $r^N$ on $S_N$ solving

$$J^N+r^N(i)=\min_{a\in A_i}\Big\{C(i,a)+\sum_{j\in S_N}P^*_{ij}(a;N)\,r^N(j)\Big\},\qquad i\in S_N,\ N\ge N_0,\tag{10.21}$$

with $\limsup_N r^N(i)<\infty$, $\liminf_N r^N(i)\ge-Q$ for a constant $Q\ge0$, and $\limsup_N J^N=:J^*<\infty$, $J^*\le J^\Delta(i)$.

Formalization targets

Goal: Theorem 10.3.3

Under (CTB), (CTAC) and the (AC) assumptions for an approximating sequence of $\Delta$:

$$J^*=\lim_{N\to\infty}J^N\ \text{exists and}\ J^\Delta(i)=J^\Psi(i)=J^*\quad(i\in S),$$

and every limit point $e^*$ of a sequence $e^N$ of stationary policies realizing the minimum in (10.21) satisfies $J^\Delta_{e^*}=J^\Delta$ and $J^\Psi_{e^*}=J^\Psi$. The goal leaves the chain, the approximating sequence and the constants of (CTB) arbitrary.

Milestones

• Proposition 10.1.2: $P(X>x+y\mid X>y)=P(X>x)$ for $x,y>0$, and $P(X\le\delta)=\mu\delta+o(\delta)$.
• Proposition 10.1.3: for independent exponentials, $P(X_1\le\delta,X_2\le\delta)=o(\delta)$, $P(X_1<X_2)=\mu_1/(\mu_1+\mu_2)$, and $\min(X_1,X_2)$ is exponential with rate $\mu_1+\mu_2$.
• Lemma 10.3.1: if $z$ is bounded below and $Z\tau(i,e)+z(i)\ge G(i,e)+g(i,e)\tau(i,e)+\sum_jP_{ij}(e)z(j)$ for all $i$ (10.15), then $J^\Psi_e\le Z$.
• Lemma 10.3.2: $(Z,w)$ satisfies $Z+w(i)\ge C(i,e)+\sum_jP^*_{ij}(e)w(j)$ (10.20) if and only if $(Z,\tau w)$ satisfies (10.15).
• Proposition 10.4.1: in the M/M/1 queue with arrival rate $\lambda$, holding cost $H(i)=Hi$ and service cost rate $c(a)$, the policy that always serves at rate $a>\lambda$ has average cost $\rho_ac(a)+H\rho_a/(1-\rho_a)$, $\rho_a=\lambda/a$.

Significance

The goal theorem turns the average cost control of a continuous time chain on an infinite state space into a finite computation: solve the optimality equation (10.21) of a finite truncation of the auxiliary chain, let the truncation grow, and read off the optimal average cost and an optimal stationary policy of the original continuous time chain. The auxiliary chain is the book's form of uniformization, and the result is what licenses the numerical study of the M/M/1 service rate control problem in Section 10.4 and of the M/M/K and polling models in Sections 10.5–10.6. Proposition 10.4.1 gives the closed-form benchmark against which the computed optimal policy is compared.

The results are proved in the book, some with details left to the reader (Lemma 10.3.2(ii), Problem 10.10), and the goal rests on Theorem 8.1.1 and Lemma 7.2.1 of the same book. None of them has, as far as a search of Mathlib and the Prove2Me catalogue shows, a machine-checked proof: Mathlib provides the exponential law (ProbabilityTheory.expMeasure) and its distribution function, but not memorylessness or the minimum of independent exponentials, and no continuous time Markov decision model. A formalization would supply these, together with a checked average cost comparison between a continuous time chain and its discrete time auxiliary chain.

Difficulty

The obvious argument compares the two chains policy by policy, but the policy classes differ: a policy for $\Delta$ may change action in every time slot, including slots where the state does not change, while a policy for $\Psi$ acts only at transitions and may use the observed sojourn times. Only the stationary policies coincide. The lower bound $J^\Psi\ge J^*$ therefore cannot be obtained by transferring policies, and it is exactly what Assumption (CTAC) supplies. The upper bound requires passing from the discrete time inequality (10.20) for the limit point $e^*$ to a bound on a ratio of expected cost to expected time in continuous time, where the denominator depends on the policy; the uniform bounds of (CTB) on the mean sojourn times are what control it. Inside Lemma 10.3.1 the function $z$ is only bounded below, so the telescoping of expectations must be justified without integrability of $z$ from above.

Formalization scope

The state space is a countable type S, actions a type Act, and action sets A i : Finset Act; the CTMDC and MDC structures hold data, and their axioms (nonempty action sets, nonnegative costs, positive rates, stochastic transition rows with $P_{ii}(a)=0$) are separate predicates. Transition probabilities are ℝ≥0∞-valued; costs, rates and the functions $z,w,r^N$ are real. Expected costs, expected times and all average costs are ℝ≥0∞-valued, so $+\infty$ is a legitimate value, and they are compared with real constants in EReal; the limits superior and inferior of (AC) are taken in EReal. The expected cost of $n$ transition periods under a general policy is a recursion over the periods in which the sojourn time is integrated against expMeasure ν(i,a) and the next state is drawn independently from $P_{i\cdot}(a)$; policies are measurable in the past sojourn times. In (10.15) and (10.20) the convergence of the series is part of the inequality. The strict inequality $\tau<\inf\tau(i,a)$ of (CTB) is kept strict (as a positive margin); weakening it to $\le$ would make $P^*_{ii}(a)$ vanish or turn negative.

The average cost $J^\Psi_\theta$ is a ratio of expectations, not the expectation of a ratio, and the infimum $J^\Psi$ ranges over history dependent randomized policies that may use sojourn times; replacing either by a stationary-only class, or dropping (CTAC), gives a different theorem.

A complete development needs: expected rewards of a chain with exponential holding times, the average cost theory of Chapter 8 for the auxiliary chain (Theorem 8.1.1 and Lemma 7.2.1, restated here as needed), and renewal-reward reasoning for Proposition 10.4.1. The exponential-distribution lemmas are reusable beyond this mission and are welcome as independent contributions.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. https://doi.org/10.1002/9780470317037
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, John Wiley & Sons, 1994. https://doi.org/10.1002/9780470316887
• S. A. Lippman, Applying a new device in the optimization of exponential queuing systems, Operations Research 23(4), 687–710, 1975. https://doi.org/10.1287/opre.23.4.687
• D. Gross and C. M. Harris, Fundamentals of Queueing Theory, 3rd ed., John Wiley & Sons, 1998.