Markov Chain

Motivation

The M/G/1 queue is the single-server queue with Poisson arrivals and an arbitrary service-time distribution. It is the first queueing model beyond the birth–death family in which exact formulas survive. It is also the model a practitioner reaches for when service times are measured and visibly not exponential: repair times, transmission times of variable-length packets, machining times. Its central result is the Pollaczek–Khintchine formula, first obtained by Pollaczek (1930) and Khintchine (1932). It expresses the stationary queue in terms of the service distribution, and it shows that the mean wait grows linearly in the squared coefficient of variation of service. That makes variability, and not only load, a measurable driver of congestion.

The textbook treatment followed here is Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory, 4th ed. (Wiley 2008), §5.1. It derives the result through Kendall's (1953) imbedded Markov chain of system sizes at departure epochs. It then obtains the transforms of the waiting times and the busy-period functional equation of Takács (1962).

Setting

Customers arrive in a Poisson stream of rate $\lambda > 0$. Service times $S$ are independent with distribution $B$, a probability distribution on $[0,\infty)$ with mean $\mathrm E[S]$, and the discipline is first-come first-served. The traffic intensity is $\rho = \lambda\,\mathrm E[S]$.

Let $X_n$ be the number of customers the $n$th departing customer leaves behind. The number of arrivals during one service time equals $i$ with probability

$$k_i = \int_0^\infty \frac{e^{-\lambda t}(\lambda t)^i}{i!}\,dB(t),$$

and $(X_n)$ is a Markov chain on $\{0,1,2,\dots\}$ whose transition matrix $P$ has first row $(k_0,k_1,k_2,\dots)$ and, for $i \ge 1$, entries $p_{ij} = k_{j-i+1}$ for $j \ge i-1$ and $0$ otherwise. A stationary distribution is a probability vector $\pi$ with $\pi P = \pi$. Its generating function is $\Pi(z) = \sum_i \pi_i z^i$, and that of the arrivals per service is $K(z) = \sum_i k_i z^i$, for complex $|z| \le 1$. The Laplace–Stieltjes transform of a distribution $F$ on $[0,\infty)$ is $F^*(s) = \int_0^\infty e^{-st}\,dF(t)$. In the Lean development these are arrivalProb, transitionMatrix, IsStationaryDist, pgf, utilization and lst in the namespace QueueingFundamentals.MG1.

Formalization targets

Goal: the Pollaczek–Khintchine transform formula (5.15)–(5.16)

If $\mathrm E[S] < \infty$ and $\rho < 1$, the chain has a stationary distribution, and every stationary distribution satisfies $\pi_0 = 1-\rho$ and

$$\Pi(z) = \frac{(1-\rho)(1-z)K(z)}{K(z)-z}, \qquad |z| \le 1,\ z \ne 1,$$

with $K(z) \ne z$ at each such $z$. It leaves the service distribution completely general.

Milestones

1. The stationary equations (5.12): $\pi_i = \pi_0 k_i + \sum_{j=1}^{i+1}\pi_j k_{i-j+1}$.
2. The transform (5.14), $\Pi(z) = \pi_0(1-z)K(z)/(K(z)-z)$, with $\pi_0$ free and no condition on $\rho$.
3. Ergodicity (§5.1.4): a unique stationary distribution exists if and only if $\rho < 1$.
4. The departure-point mean (5.7): $L^{(D)} = \rho + (\rho^2+\lambda^2\sigma_B^2)/(2(1-\rho))$.
5. $K(z) = B^*[\lambda(1-z)]$ (5.32).
6. The system-wait transform (5.29), (5.33): $\Pi(z) = W^*[\lambda(1-z)]$ and $W^*(s) = (1-\rho)sB^*(s)/(s-\lambda[1-B^*(s)])$.
7. The line-wait transform (5.34): $W_q^*(s) = (1-\rho)s/(s-\lambda[1-B^*(s)])$.
8. The busy-period equation (5.37): $G^*(s) = B^*[s+\lambda-\lambda G^*(s)]$.
9. The mean busy period: $\mathrm E[X] = 1/(\mu-\lambda)$ with $\mu = 1/\mathrm E[S]$.

Significance

The transform formula determines the whole stationary departure-point distribution from the service distribution. Its derivatives at $z = 1$ give every moment of the system size, including the mean-value formula (5.7). Combined with the transform identity (5.32), it gives the waiting-time transforms (5.33)–(5.34). Those in turn give the classical geometric-series representation of the line-wait distribution through the residual service time. The busy-period equation is the starting point for busy-period moments and for the M/G/1 analysis of priority and vacation models later in the book.

All results here are classical and proved in the literature. As far as a search of the platform shows (2026-09-28), none is machine-checked: there is no M/G/1 queue, imbedded departure-point chain, Laplace–Stieltjes transform of a service distribution, or busy-period equation on Prove2Me. Mathlib has Poisson distributions and measure convolution but no generating-function theory for countable Markov chains, no Laplace–Stieltjes transform, and no identity theorem in the form these statements need. The mission produces a checked statement of the Pollaczek–Khintchine formulas that later queueing developments (vacations, priorities, M/G/1-type chains) can build on.

Difficulty

Turning the stationary equations into (5.14) is formal power-series algebra. The difficulties lie elsewhere. First, the formula must hold for complex $z$ on the closed disk, which needs the non-vanishing of $K(z)-z$ away from $z = 1$. That fact fails for $\rho > 1$, where $K$ has a fixed point inside the disk. Second, (5.15) evaluates $\pi_0$ from $\Pi(1) = 1$ by a limit at the point where the formula is $0/0$, and this uses $K'(1) = \rho$, an interchange of sum and integral. Third, the existence half of the goal requires positive recurrence of a chain with unbounded jumps. The book obtains it from Foster's criterion, which is not in Mathlib. Fourth, the waiting-time and busy-period transforms are stated for all real $s > 0$, while the generating-function route reaches only $s = \lambda(1-z) \in (0, 2\lambda]$. Extending the identity requires either analyticity arguments or a direct derivation. A formal proof of (5.14) alone does not touch any of these.

Formalization scope

The service distribution is a Measure ℝ with IsProbabilityMeasure B and B (Set.Iio 0) = 0; no density is assumed. The arrival rate is lam : ℝ with 0 < lam. Stationarity is IsStationaryDist P π: nonnegative entries, HasSum π 1, and HasSum (fun i => π i * P i j) (π j) for every j. That is global balance on ℕ, as the book writes it. Generating functions take a complex argument with ‖z‖ ≤ 1; transforms take a complex argument, and the waiting-time and busy-period statements use real s. The mean and variance of B are Bochner integrals, and every statement that uses them assumes Integrable. The mean busy period assumes 0 < E[S], so that $\mu = 1/\mathrm E[S]$ is the book's service rate.

Closed forms carried by the statements: $\pi_0 = 1-\rho$ (5.15); $(1-\rho)(1-z)K(z)/(K(z)-z)$ (5.16); $\pi_0(1-z)K(z)/(K(z)-z)$ (5.14); $\rho + (\rho^2+\lambda^2\sigma_B^2)/(2(1-\rho))$ (5.7); $B^*[\lambda(1-z)]$ (5.32); $(1-\rho)sB^*(s)/(s-\lambda[1-B^*(s)])$ (5.33); $(1-\rho)s/(s-\lambda[1-B^*(s)])$ (5.34); $B^*[s+\lambda-\lambda G^*(s)]$ (5.37); $1/(\mu-\lambda)$ for the mean busy period.

The waiting-time distribution $W$ enters through the book's FCFS relation $\pi_n = \frac1{n!}\int(\lambda t)^n e^{-\lambda t}\,dW(t)$, and $W_q$ through $W = W_q * B$; both are hypotheses, as in the book. The busy-period distribution $G$ enters through the equation (5.36) in CDF form, with $n$-fold convolutions built from Mathlib's Measure.conv.

The goal is not the algebraic consequence of (5.12) for an arbitrary sequence: $\pi$ must be a probability vector, $\pi_0$ is determined as $1-\rho$, and the existence of a stationary distribution is part of the conclusion, so the statement cannot hold vacuously. The departure-point/time-average equality (§5.1.3, via PASTA) is not formalized.

Useful infrastructure, reusable beyond this mission: generating functions of stationary distributions on ℕ, Poisson mixtures, Laplace–Stieltjes transforms of measures on $[0,\infty)$, and a Foster-type drift criterion for countable chains. Contributions proving any milestone, or those tools, are welcome.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.1. https://doi.org/10.1002/9781118625651
• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Annals of Mathematical Statistics 24 (1953) 338–354. https://doi.org/10.1214/aoms/1177728975
• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953) 355–360. https://doi.org/10.1214/aoms/1177728976
• L. Takács, Introduction to the Theory of Queues, Oxford University Press, 1962.
• F. Pollaczek, Über eine Aufgabe der Wahrscheinlichkeitstheorie, Mathematische Zeitschrift 32 (1930) 64–100. https://doi.org/10.1007/BF01194620

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

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.