The OR Formalization Drive

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

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

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

Most queueing models with a closed-form answer assume Poisson arrivals. In practice the times between arrivals are often far from exponential: scheduled appointments, batch releases from an upstream process, or arrivals timed by a machine cycle. The G/M/1 queue keeps the service side exponential and makes no assumption about the arrival stream beyond independent, identically distributed interarrival times. It is the standard counterpart of the M/G/1 queue, and its solution is the one used in teaching and in practice whenever the input is not Poisson (Gross, Shortle, Thompson & Harris, Fundamentals of Queueing Theory, 4th ed., Wiley 2008, §5.3.1, DOI 10.1002/9781118625651).

The answer has an unusually clean form. The number of customers that an arriving customer finds in the system is geometric, exactly as in the M/M/1 queue, with the traffic intensity $\rho$ replaced by a number $r_0$ that depends on the whole interarrival distribution through a single scalar equation. This mission is the seventh of a series formalizing the book chapter by chapter; it covers the G/M/1 half of §5.3 (printed pp.259–263).

Setting

Customers arrive at a single server. The interarrival times are independent with common law $A$, a probability distribution on $[0,\infty)$ with CDF $A(t)$ and finite mean $E[T] = 1/\lambda$, $\lambda > 0$. Service times are independent exponential random variables with rate $\mu > 0$, and the discipline is first come, first served.

Let $X_n$ be the number of customers in the system just before the $n$th arrival. Between two arrivals the server completes a Poisson number of services (truncated by the number present), so $\{X_n\}$ is a Markov chain on $\{0,1,2,\dots\}$. Its transition probabilities are built from

$$b_k = \int_0^\infty \frac{e^{-\mu t}(\mu t)^k}{k!}\,dA(t) \qquad (k \ge 0),$$

the probability of exactly $k$ completions during one interarrival time (Eq. (5.50)): $p_{i0} = 1 - \sum_{k=0}^{i} b_k$, $p_{ij} = b_{i+1-j}$ for $1 \le j \le i+1$, and $p_{ij} = 0$ otherwise (Eq. (5.51)). A stationary arrival-point distribution is a probability vector $q = \{q_n\}$ with $qP = q$ and $qe = 1$ (Eq. (5.52)); $q_n$ is the long-run probability that an arrival finds $n$ customers present.

The characteristic equation of the chain is

$$z = \beta(z), \qquad \beta(z) = \sum_{n \ge 0} b_n z^n ,$$

where $\beta$ is the probability generating function of $\{b_n\}$ (Eq. (5.55)). Equivalently $z = A^*[\mu(1-z)]$ (Eq. (5.56)), where $A^*(s) = \int_0^\infty e^{-sx}\,dA(x)$ is the Laplace–Stieltjes transform of the interarrival law. The traffic intensity is $\rho = \lambda/\mu$.

Formalization targets

Goal: Eq. (5.60), the geometric arrival-point law

If $\rho = \lambda/\mu < 1$, there is a number $r_0$ with $0 < r_0 < 1$ and $r_0 = \beta(r_0)$, it is the only complex root of $z = \beta(z)$ in the open unit disk, and

$$q_n = (1 - r_0)\, r_0^{\,n} \qquad (n \ge 0)$$

is a stationary arrival-point distribution and the only one. The root is part of the conclusion, not an assumption.

Milestones

1. Eqs. (5.51)–(5.53): for a probability vector $q$, $qP = q$ is equivalent to $q_i = \sum_{k\ge0} q_{i+k-1}b_k$ ($i \ge 1$) and $q_0 = \sum_{j\ge0} q_j\bigl(1 - \sum_{k=0}^{j} b_k\bigr)$.
2. p.261: $0 < b_0 < 1$, $b_n > 0$ for all $n$, $\beta(1) = 1$, and $\beta'(1) = \sum_n n b_n = \mu/\lambda$.
3. Eq. (5.56): $\beta(z) = A^*[\mu(1-z)]$ for $|z| \le 1$.
4. Eq. (5.58), Figure 5.2: $z = \beta(z)$ has at most one root in $(0,1)$, and one exists if and only if $\lambda/\mu < 1$.
5. p.262: when $\lambda/\mu < 1$, $z = \beta(z)$ has exactly one root with $|z| < 1$.
6. Eq. (5.59): successive substitution $z^{(k+1)} = \beta(z^{(k)})$ from any $0 < z^{(0)} < 1$ converges to $r_0$.
7. Eq. (5.61): $L^{(A)} = r_0/(1-r_0)$ and $L_q^{(A)} = r_0^2/(1-r_0)$.
8. Eq. (5.62): $W_q(t) = 1 - r_0 e^{-\mu(1-r_0)t}$ and $W(t) = 1 - e^{-\mu(1-r_0)t}$ for $t \ge 0$.
9. Eq. (5.63): $W_q = r_0/(\mu(1-r_0))$ and $W = 1/(\mu(1-r_0))$.

Significance

The result. Equation (5.60) reduces the analysis of a queue with arbitrary renewal input to one scalar root. Every arrival-point performance measure of the M/M/1 queue then carries over with $\rho$ replaced by $r_0$: the mean number found by an arrival, the mean queue found by an arrival, and the full distributions of line delay and system time seen by arrivals (Eqs. (5.61)–(5.63)). The same root drives the multiserver G/M/c analysis later in §5.3 and the relation between arrival-point and time-average probabilities in §6.3. The result also illustrates a point the book stresses: $q_n$ is the distribution seen by arrivals, and it equals the time-average distribution $p_n$ only when the input is Poisson.

Formalizing it. The mathematics is classical (the embedded-chain method goes back to Kendall, 1953) and fully proved in the textbook literature; nothing here is open. To our knowledge none of it has a machine-checked proof: the platform had no G/M/1, embedded-chain, or Rouché-type statement when this mission was drafted. The work is to formalize the known argument, which touches analytic facts about power series with nonnegative coefficients, a mixture-of-Poisson computation, a counting of roots in the unit disk, and the uniqueness of the stationary law of an irreducible countable chain.

Difficulty

Locating a real root in $(0,1)$ is a one-variable question. The hard step is excluding every other complex root inside the unit disk: a real-variable argument says nothing about complex roots, and the book's route relies on Rouché's theorem, which Mathlib does not have. A second point is uniqueness of the stationary vector: showing that the geometric vector solves $qP = q$ does not show that no other probability vector does, and the goal asserts both. Computing $\sum_n n b_n = \mu/\lambda$ requires interchanging a sum with the integral against $A$, which is where the finite mean of the interarrival law enters.

Formalization scope

The interarrival law is a measure A : Measure ℝ with IsProbabilityMeasure A, A (Set.Iio 0) = 0, integrable identity, and ∫ x ∂A = 1/λ (the structure IsInterarrivalLaw). Every theorem also assumes $\lambda > 0$ and $\mu > 0$. The integrals defining $b_k$ and $A^*$ are over $[0,\infty)$, closed at $0$. The generating function $\beta$ takes complex arguments; real roots are written with the real-to-complex coercion. A stationary vector is a function q : ℕ → ℝ with $q_n \ge 0$, HasSum q 1, and HasSum (fun i => q i * p i j) (q j) for every $j$.

The explicit closed forms the statements carry are: the transition matrix (5.51); the equations (5.53); $\beta(z) = A^*[\mu(1-z)]$ (5.56); $\beta'(1) = \mu/\lambda$; $q_n = (1-r_0)r_0^n$ (5.60); $r_0/(1-r_0)$ and $r_0^2/(1-r_0)$ (5.61); $1 - r_0e^{-\mu(1-r_0)t}$ and $1 - e^{-\mu(1-r_0)t}$ (5.62); $r_0/(\mu(1-r_0))$ and $1/(\mu(1-r_0))$ (5.63). The waiting-time CDFs are defined as in §2.2.5 of the book: $W_q(t) = q_0 + \sum_{n\ge1} q_n \Pr\{n \text{ completions in} \le t\}$ with the Erlang type-$n$ CDF, and $W(t)$ likewise with $n+1$ completions. The means in (5.63) are $\int_0^\infty [1 - W_q(t)]\,dt$ and $\int_0^\infty [1 - W(t)]\,dt$.

A trivializing formalization would take "$r_0 \in (0,1)$ solves $z = \beta(z)$" as a hypothesis of the goal, which turns (5.60) into a geometric-series check; here existence, location and uniqueness of the root, and uniqueness of the stationary vector, are all conclusions.

Out of scope for this mission: the M/G/c and M/G/∞ results of §5.2 and the multiserver G/M/c analysis of §5.3.2. Reusable pieces include a Rouché-type or fixed-point counting lemma for power series with nonnegative coefficients summing to one, and the uniqueness of stationary laws for irreducible chains on $\mathbb N$. Contributions of either kind are welcome.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.3.1, pp.259–263. 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(3), 1953, 338–354. https://doi.org/10.1214/aoms/1177728975

Motivation

Resource-constrained project scheduling asks for start times of the activities of a project so that prescribed time lags between activities are respected and, at every moment, the activities in progress do not require more of any renewable resource (staff, machines, reactors) than is available. When the time lags include maximum time lags (deadlines relative to other activities), even finding a feasible schedule is NP-hard, and the feasible region is in general neither convex nor connected. Branch-and-bound methods for this problem (the problem $PS|temp|C_{\max}$ in the notation of Neumann, Schwindt & Zimmermann) do not search over schedules directly. They search over strict orders of the activities, that is, over sets of precedence constraints "$j$ starts after $i$ has finished".

This mission formalizes the theory behind that search, as developed by Bartusch, Möhring & Radermacher (1988) and presented in §2.3 of Neumann, Schwindt & Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003). Its goal, Theorem 2.3.10, says when a strict order resolves every resource conflict.

Setting

A project has activities $V = \{0, 1, \dots, n+1\}$, where $0$ and $n+1$ are fictitious activities marking the project's start and completion and $1, \dots, n$ are the real activities ($n \ge 1$). Activity $i$ has duration $p_i \in \mathbb Z_{\ge 0}$, with $p_0 = p_{n+1} = 0$ and $p_i > 0$ for real activities. Time lags are encoded in the project network $N$: an arc $\langle i, j\rangle \in E$ with integer weight $\delta_{ij}$ imposes $S_j - S_i \ge \delta_{ij}$. The book's standing assumptions give, for every node $i$, a path from $0$ to $i$ of nonnegative length and a path from $i$ to $n+1$ of length at least $p_i$.

A schedule is a vector $S \in \mathbb R^{n+2}$ with $S_0 = 0$ and $S_i \ge 0$. It is time-feasible if $S_j - S_i \ge \delta_{ij}$ for all arcs. The set of time-feasible schedules is $\mathcal S_T$.

Each renewable resource $k \in \mathcal R$ has a capacity $R_k$, and activity $i$ uses $r_{ik} \le R_k$ units of it while in progress, with $r_{0k} = r_{n+1,k} = 0$. The active set at time $t$ is $\mathcal A(S,t) = \{ i \mid S_i \le t < S_i + p_i\}$, and $S$ is resource-feasible if $\sum_{i \in \mathcal A(S,t)} r_{ik} \le R_k$ for all $k$ and all $t \ge 0$. The feasible region $\mathcal S$ consists of the schedules that are both time-feasible and resource-feasible.

A strict order $O \subseteq V \times V$ is an asymmetric, transitive relation. Its order polyhedron is

$$\mathcal S_T(O) = \{ S \in \mathcal S_T \mid S_j \ge S_i + p_i \ \text{for all } (i,j) \in O\}.$$

$O$ is time-feasible if $\mathcal S_T(O) \ne \emptyset$, and feasible if moreover $\mathcal S_T(O) \subseteq \mathcal S$. The order network $N(O)$ adds to $N$, for each $(i,j) \in O$, an arc $\langle i,j\rangle$ of weight $p_i$, or raises the weight of an existing arc to $\max(\delta_{ij}, p_i)$. A schedule $S$ induces the strict order $O(S) = \{(i,j) \mid i \ne j,\ S_j \ge S_i + p_i\}$.

A set $F \subseteq V$ is forbidden if $\sum_{i \in F} r_{ik} > R_k$ for some resource $k$. It is a minimal forbidden set if no proper subset of it is forbidden. $\mathcal F$ denotes the set of minimal forbidden sets.

Formalization targets

Goal: Theorem 2.3.10 (Bartusch et al. 1988)

For every time-feasible strict order $O$,

$$O \text{ feasible} \iff \forall F \in \mathcal F\ \exists\, i, j \in F:\ N(O) \text{ has a path from } i \text{ to } j \text{ of length} \ge p_i .$$

Milestones

1. Proposition 2.3.3. A strict order $O$ is time-feasible if and only if $N(O)$ has no cycle of positive length.
2. Bartusch et al.'s criterion (quoted in the proof of Theorem 2.3.10). A schedule $S$ is resource-feasible if and only if every $F \in \mathcal F$ contains distinct $i, j$ with $S_j \ge S_i + p_i$.
3. Proposition 2.3.6. For time-feasible $S$, the strict order $O(S)$ is feasible if and only if $S \in \mathcal S$.
4. Theorem 2.3.7. $\mathcal S = \bigcup_{O \in \mathcal O} \mathcal S_T(O)$, where $\mathcal O$ is the finite set of inclusion-minimal feasible strict orders.
5. Remark 2.3.11. A time-feasible schedule partitions $F$ if and only if every $\mathcal A(S,t) \cap F$, $t \ge 0$, is feasible. A time-feasible order is feasible if and only if it breaks up all (equivalently, all minimal) forbidden sets. A time-feasible schedule is feasible if and only if it partitions all forbidden sets.

Significance

Theorem 2.3.10 turns the feasibility of a strict order, which is a statement about infinitely many schedules and all times $t$, into a finite check: one longest-path computation in $N(O)$ for each minimal forbidden set. Together with Proposition 2.3.3 and the structural Theorem 2.3.7, it shows that $\mathcal S$ is a finite union of polyhedra indexed by feasible strict orders. This justifies the enumeration schemes of Chapter 2 of the book (branching on the pairs that break up a minimal forbidden set) and the notions of active and stable schedules developed in later sections.

All results in this mission are proved in the literature. For the resource-feasibility criterion, the book cites Bartusch et al. (1988) instead of proving it. To our knowledge, none of these results has been machine-checked. A formal development would give a verified foundation for the order-based description of the feasible region, on which later missions of this series (active schedules, delaying modes, stable schedules) build.

Difficulty

The sufficiency half of the goal is short once the criterion is available: a path of length $\ge p_i$ in $N(O)$ forces $S_j \ge S_i + p_i$ on the whole order polyhedron. The necessity half carries the content. If for some minimal forbidden set $F$ no path in $N(O)$ between elements of $F$ reaches the required length, one must construct a schedule in $\mathcal S_T(O)$ in which all activities of $F$ are simultaneously in progress. This means adding the reverse constraints $S_j - S_i < p_i$ for all $i, j \in F$ to the temporal system without creating a cycle of positive length, while keeping $S_0 = 0$ and $S \ge 0$. The obvious reading "no single arc gives a precedence, so they can overlap" fails because maximum time lags combine into long paths through activities outside $F$. The standing assumption that every node is reachable from $0$ by a path of nonnegative length is needed here: without it the equivalence is false.

Formalization scope

• The activity set is Fin (n + 2): 0 is the project start and Fin.last (n + 1) the project completion. Durations and resource data are natural numbers, arc weights are integers, and start times are real numbers.
• Strict orders are finite sets of pairs, Finset (Fin (n+2) × Fin (n+2)), required to be asymmetric and transitive.
• Resource constraints hold for every $t \ge 0$. The book's (2.1.4) writes $0 \le t \le \bar d$. In Chapter 2 schedules are not bounded by $\bar d$, and the book's proofs and Remark 2.3.11 use all $t \ge 0$. This is a convention of the whole series, not a strengthening.
• A path is a walk (nodes may repeat) and its length is the sum of its arc weights. A cycle of positive length is a closed walk with at least one arc and positive length. For a time-feasible order, $N(O)$ has no cycle of positive length. In that case "some path of length $\ge p_i$" coincides with the book's "longest path length $\ge p_i$", so no supremum over paths appears.
• The standing assumptions of the book form a single predicate Project.StandingAssumptions, which is a hypothesis of every theorem: $n \ge 1$; $p_0 = p_{n+1} = 0$ and $p_i > 0$ otherwise; no loops; $r_{0k} = r_{n+1,k} = 0$ and $r_{ik} \le R_k$; and the two path conditions of p. 8.
• Minimal forbidden sets and inclusion-minimal feasible orders use Mathlib's Minimal, taken among forbidden sets and among feasible strict orders respectively.
• The goal is an equivalence, and both directions are required. Weakening it to sufficiency, or dropping the time-feasibility of $O$ or the minimality of $F$, would change the theorem. Keeping the book's cut-off $t \le \bar d$ would also change it, because a schedule could then have an unresolved conflict after $\bar d$ and still be called feasible.
• Theorem 1.3.3 of Chapter 1 (a time-feasible schedule exists if and only if the network has no cycle of positive length) is needed for Proposition 2.3.3 and is restated here for $N(O)$. Chapter 1's mission is drafted separately.
• Useful infrastructure beyond this mission: longest-path potentials on integer-weighted digraphs without positive cycles (feasibility of difference constraints), and the walk and cycle API on Network. Contributions of this general lemma layer are welcome.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. https://doi.org/10.1007/978-3-540-24800-2
• M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988), 201–240. https://doi.org/10.1007/BF02283745

Why the G/G/1 queue

The single-server queue with general interarrival times and general service times, written G/G/1 in Kendall's notation, is the model left when every distributional assumption is removed from the classical single-server queue. Customers arrive one at a time, wait in line in first-come, first-served order, and are served one at a time. Almost nothing about it can be computed in closed form. What survives is a recursion for the waiting times of successive customers and the integral equation of its steady state, due to Lindley (Lindley, 1952). Every exact and approximate treatment of the G/G/1 waiting time, including the bounds of the next chapter of the book, starts from that equation.

This mission is the eighth of a series formalizing Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651). It covers Chapter 6, "General Models and Theoretical Topics". The chapter also treats the G/E_k/1 characteristic equation (§6.1), the M/D/c queue (§6.3) and maximum-likelihood estimation for M/M/1 (§6.7), which appear here as further milestones.

Timeline. Lindley (1952) derived the recursion and the integral equation and showed that a limiting waiting-time distribution exists when the mean service time is smaller than the mean interarrival time. Loynes (1962) gave the stationary solution as a supremum over the past of a random walk, for stationary rather than independent inputs. Clarke (1957) derived the maximum-likelihood estimators for M/M/1, and Crommelin (1932) the M/D/c generating function. Chaudhry, Harris and Marchal (1990) located the roots of the G/E_k/1 characteristic equation.

Setting

The interarrival times $T^{(n)}$ are independent with common distribution $A$, the service times $S^{(n)}$ are independent with common distribution $B$, and the two sequences are independent. Both $A$ and $B$ are lifetime laws: probability distributions on $[0,\infty)$. The means are $\mathrm E[T]=1/\lambda$ and $\mathrm E[S]=1/\mu$, and the traffic intensity is $\rho=\lambda/\mu=\mathrm E[S]/\mathrm E[T]$.

The line delay $W_q^{(n)}$ of the $n$th customer satisfies Lindley's recursion

$$W_q^{(n+1)}=\max\bigl(0,\;W_q^{(n)}+S^{(n)}-T^{(n)}\bigr).$$

Write $U$ for the distribution of $S-T$ with $S\sim B$ and $T\sim A$ independent. Since $W_q^{(n)}$ is independent of $(S^{(n)},T^{(n)})$, one step of the recursion sends the distribution $\nu$ of $W_q^{(n)}$ to the distribution of $\max(0,W+U)$ with $W\sim\nu$ independent of $U$. A stationary delay distribution is a probability distribution $\nu$ that this step maps to itself; its CDF is $W_q(t)=\nu((-\infty,t])$.

Formalization targets

Goal: Lindley's equation (6.8)

If $\mathrm E[T]$ and $\mathrm E[S]$ are finite and $\rho<1$, then a stationary delay distribution exists, and the CDF of every stationary delay distribution satisfies

$$W_q(t)=\begin{cases}\displaystyle\int_{-\infty}^{t}W_q(t-x)\,dU(x) & (0\le t<\infty),\\ 0 & (t<0),\end{cases} \qquad U(x)=\int_{\max(0,x)}^{\infty}B(y)\,dA(y-x).$$

The goal consists of the existence statement and the equation together. The equation alone is close to unfolding one step of the recursion. Existence is what ties it to a queue in steady state.

Milestones

• (6.9), the CDF of $U=S-T$ as a convolution of $B$ and $A$.
• The one-step convolution (p.285): $W_q^{(n+1)}(t)=\int_{-\infty}^{t}W_q^{(n)}(t-x)\,dU(x)$ for $t\ge0$.
• (6.10)–(6.12), the Wiener–Hopf form: $W_q^-(t)+W_q(t)=\int_{-\infty}^t W_q(t-x)\,dU(x)$ for all $t$, and $\bar W_q(s)=\bar W_q^-(s)/(A^*(-s)B^*(s)-1)$ for two-sided Laplace transforms.
• The G/E_k/1 root result (p.278): the characteristic equation $z^k=A^*[k\mu(1-z)]$ has exactly one root in $(0,1)$, one in $(-1,0)$ exactly when $k$ is even, and, when $A^*=[A_1^*]^k$, exactly $k$ distinct roots in the open unit disk.
• (6.18)–(6.20), the M/D/c generating function and $p_0$ in terms of the roots of $z^c=e^{-\lambda(1-z)}$.
• (6.33), the maximum-likelihood estimators $\hat\lambda=n_a/t$, $\hat\mu=n_c/t_b$ for M/M/1.

Significance

Lindley's equation characterizes the stationary G/G/1 waiting time without any distributional assumption. The M/M/1, M/G/1 and G/M/1 waiting-time distributions of earlier chapters are its special cases. The transform relation (6.12) reduces the G/G/1 delay to a factorization problem for $A^*(-s)B^*(s)-1$. The recursion and the equation are the starting point of Kingman's bound, of heavy-traffic approximations and of simulation of single-server systems.

All of these results are classical and proved. As far as a search of the platform shows, none of them is formalized. The platform's forward-coupling mission proves convergence to a stationary workload of a continuous-time queue that it assumes to exist. It proves neither the existence of a stationary law of Lindley's discrete recursion nor Lindley's equation. The mission therefore produces a machine-checked account of the G/G/1 recursion on distributions, a Loynes-type existence theorem for it, and the Wiener–Hopf transform identity. Its definitions (lifetime laws, the law of $S-T$, the law map of the recursion, two-sided transforms) are reusable for Kingman's bound in the next mission of the series.

Difficulty

The obvious route to existence is to iterate the recursion from $W_q^{(0)}=0$ and take a limit. The distributions of $W_q^{(n)}$ from zero increase stochastically, but a limit of CDFs need not be a probability distribution: mass can escape to infinity, and it does when $\rho>1$. Ruling this out under $\rho<1$ is the whole content of the existence half. It is a statement about the entire past of the input sequences, not about one step of the recursion, and the book asserts it without argument ("In the steady state ($\rho<1$) …", p.285).

The transform identity (6.12) needs the right strip of convergence, which the book does not state. $A^*(-s)$ is finite only where the interarrival time has an exponential moment.

Formalization scope

Distributions are Mathlib measures on $\mathbb R$. $A$ and $B$ are probability measures with no mass on $(-\infty,0)$, with integrable identity where means are used. $\rho<1$ is stated as $\mathrm E[S]/\mathrm E[T]<1$ with $\mathrm E[T]>0$. Independence is encoded by product measures: $U$ is the image of $B\otimes A$ under $(s,t)\mapsto s-t$, and one step of the recursion is the image of $\nu\otimes U$ under $(w,u)\mapsto\max(0,w+u)$. Stieltjes integrals over $(-\infty,t]$ are Lebesgue integrals over the closed half-line, so the atom $W_q(0)=q_0$ is counted. Transforms take complex arguments.

The closed forms carried by the statements are the following.

• (6.8), in both of the book's forms, $\int_{-\infty}^t W_q(t-x)\,dU(x)$ and $-\int_0^\infty W_q(y)\,dU(t-y)$.
• (6.9) as an integral against the law of $T+x$.
• $U^*(s)=A^*(-s)B^*(s)$ and (6.12), for $0<\operatorname{Re}s$ with $\int e^{(\operatorname{Re}s)x}\,dA(x)<\infty$. The division is stated only where $A^*(-s)B^*(s)\ne1$.
• (6.18) and (6.19) with the denominator $1-z^ce^{\lambda(1-z)}$ cleared on $|z|\le1$, and (6.20) for $c\ge2$. The roots $z_1,\dots,z_{c-1}$ are hypotheses: distinct, $\ne1$, and exhausting the roots in the closed disk.
• (6.33) as the unique maximizer of $-\lambda t-\mu t_b+n_a\ln\lambda+n_c\ln\mu$ over $\lambda,\mu>0$.

A stationary delay distribution is a fixed point of the law map of the recursion, not an arbitrary CDF assumed to satisfy (6.8). A statement of (6.8) for "any CDF with $W_q=W_q*U$ on $[0,\infty)$" would assume its own conclusion, and is excluded. The statement for M/D/c includes existence of a steady state under $\lambda<c$ as well as the formula for every steady state.

Not formalized: §6.1.1–6.1.2 (G/PH_k/1, quasi-birth–death processes), §6.4 (semi-Markov processes, whose limit theorems the book quotes without hypotheses), §6.5 (random-order and last-come service, series representations), §6.6 (design and control), and the rest of §6.7.

Contributions are welcome on the random-walk representation of the recursion, on the existence theorem under $\rho<1$, and on the transform identities. The first two are reusable for any single-server or storage model driven by a reflected random walk.

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
• D. V. Lindley, "The theory of queues with a single server", Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 1952. https://doi.org/10.1017/S0305004100027638
• R. M. Loynes, "The stability of a queue with non-independent inter-arrival and service times", Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 1962. https://doi.org/10.1017/S0305004100036094
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.
• A. B. Clarke, "Maximum likelihood estimates in a simple queue", Annals of Mathematical Statistics 28(4), 1957. https://doi.org/10.1214/aoms/1177706796
• M. L. Chaudhry, C. M. Harris, W. G. Marchal, "Robustness of rootfinding in single-server queueing models", ORSA Journal on Computing 2(3), 1990. https://doi.org/10.1287/ijoc.2.3.273