Stochastic Systems

Motivation

Control problems for queueing systems (admission control, routing, service rate selection, inventory replenishment) are naturally modelled as Markov decision chains with a countable state space, such as the number of customers in a buffer, and with costs that grow without bound in the state, such as holding costs proportional to queue length. The expected discounted cost criterion is the first infinite horizon criterion applied to such models, and it is also the tool through which the average cost criterion is treated later in the same book (Chapters 6–8 of Sennott's text reach average cost optimal policies through limits of discounted problems as the discount factor tends to one).

Classical treatments of discounted dynamic programming assume bounded costs, under which the dynamic programming operator is a contraction and has a unique bounded fixed point. That assumption fails for queueing models. This mission formalizes Chapter 4, Sections 4.1–4.4, of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999), which develops the discounted theory for nonnegative, possibly unbounded costs, where value functions may be infinite.

Timeline of the underlying theory:

• 1965. Blackwell (Ann. Math. Statist. 36) establishes the discounted theory with bounded rewards.
• 1966. Strauch (Ann. Math. Statist. 37) treats "negative" dynamic programming, the case of nonpositive rewards (equivalently nonnegative costs), with no boundedness assumption.
• 1977–1978. Bertsekas (SIAM J. Control Optim. 15) and Bertsekas and Shreve (Stochastic Optimal Control: The Discrete-Time Case) give the abstract monotone-mapping framework covering both cases.
• 1999. Sennott's text states the countable-state, finite-action, nonnegative-cost discounted theory in the form used for queueing control, with general history-dependent randomized policies.

Setting

A Markov decision chain $\Delta$ has a countable state space $S$; for each state $i$ a finite nonempty action set $A_i$; for each $a \in A_i$ a nonnegative finite cost $C(i,a)$ and a probability distribution $(P_{ij}(a))_{j \in S}$ of the next state. A policy $\theta$ chooses the action at time $n$ at random from a distribution $\theta(\cdot \mid h_n)$ on $A_{i_n}$ that may depend on the entire history $h_n = (i_0, a_0, \dots, a_{n-1}, i_n)$. A stationary policy $f$ always chooses $f(i) \in A_i$ in state $i$; for it one writes $C(i,f) = C(i,f(i))$ and $P_{ij}(f) = P_{ij}(f(i))$.

Fix a discount factor $\alpha \in (0,1)$. For an initial state $i$ and a policy $\theta$, the $n$-horizon cost with terminal cost zero and the infinite horizon discounted cost are

$$v_{\theta,\alpha,n}(i) = \sum_{t=0}^{n-1} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i], \qquad V_{\theta,\alpha}(i) = \sum_{t=0}^{\infty} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i],$$

and the value functions are $v_{\alpha,n}(i) = \inf_\theta v_{\theta,\alpha,n}(i)$ and $V_\alpha(i) = \inf_\theta V_{\theta,\alpha}(i)$, infima over all policies. All of these lie in $[0,\infty]$. A policy is discount optimal if $V_{\theta,\alpha} = V_\alpha$. The discount optimality equation is

$$W(i) = \min_{a \in A_i} \Big\{ C(i,a) + \alpha \sum_j P_{ij}(a) W(j) \Big\}, \qquad i \in S. \tag{4.9}$$

With $W = V_\alpha$, $B_i(\alpha)$ denotes the set of actions attaining the minimum at $i$.

Formalization targets

Goal: Theorem 4.1.4

$V_\alpha$ solves (4.9); every $W : S \to [0,\infty]$ solving (4.9) satisfies $V_\alpha \le W$; and every stationary policy $f_\alpha$ with

$$C(i,f_\alpha) + \alpha \sum_j P_{ij}(f_\alpha) V_\alpha(j) = \min_a \Big\{ C(i,a) + \alpha \sum_j P_{ij}(a) V_\alpha(j) \Big\} \quad \text{for all } i$$

is discount optimal. No boundedness of costs and no finiteness of $V_\alpha$ is assumed.

Milestones

In attack order: Lemma 4.1.1 ($v_{\theta,\alpha,n} \uparrow V_{\theta,\alpha}$); Proposition 4.1.2 (a supersolution of the one-policy equation dominates $v_{e,\alpha,n} + \alpha^n E_e[W(X_n)]$ and $V_{e,\alpha}$); Corollary 4.1.3 (a supersolution of the optimality inequality dominates $V_{f,\alpha} \ge V_\alpha$); then, beyond the goal, Corollary 4.1.5 ($\alpha^n E_{f_\alpha}[V_\alpha(X_n) \mid X_0 = i] \to 0$ where $V_\alpha(i) < \infty$), Proposition 4.2.2 and Corollary 4.2.4 (conditions under which a solution of (4.9) equals $V_\alpha$), Proposition 4.3.1 ($v_{\alpha,n} \uparrow V_\alpha$, and limit points of finite horizon optimal stationary policies are discount optimal) and Proposition 4.4.1 (optimal policies are exactly those concentrated on the sets $B_{i}(\alpha)$ along histories of positive probability).

Significance

Theorem 4.1.4 is the foundation for everything in the book that concerns discounted costs: it produces an optimal stationary deterministic policy, identifies $V_\alpha$ among the many solutions of (4.9) (Example 4.2.1 of the book gives a one-parameter family of finite solutions), and underlies value iteration (Proposition 4.3.1) and the approximating-sequence method of Sections 4.6–4.7. The average cost results of Chapters 6–8 are proved from it by letting $\alpha \to 1$. Proposition 4.4.1 describes the full set of optimal policies, including randomized and history-dependent ones.

These are known results with published proofs. The contribution of this mission is a machine-checked development of the discounted theory for countable state spaces with unbounded costs and infinite values, over the general policy class. Related statements on the platform (the monotone-mapping propositions of Bertsekas 1977 in the MonotoneDP missions, and bounded-cost or finite-state discounted results) use different models and are open; no machine-checked proof of the present statements is known to this mission.

Difficulty

The contraction argument that settles the bounded case is unavailable: with unbounded costs the operator in (4.9) has many fixed points, and $V_\alpha$ can equal $+\infty$ at some states, so neither uniqueness of fixed points nor subtraction of values is available. The optimality equation compares the infimum over all history-dependent randomized policies with a one-step minimum, so the general policy class and the law of the process under it must be handled directly; restricting attention to Markov or stationary policies begs the question. Every limit exchange (monotone limits of finite horizon costs, the passage to limit points of policies in Proposition 4.3.1) takes place in $[0,\infty]$, where finite-valued arguments do not transfer verbatim.

Formalization scope

The Lean development lives in the namespace SennottDP.Discounted. Conventions:

• The state space is a type S with [Countable S]; actions form a type Act and A i : Finset Act is nonempty. Costs are ℝ≥0; transition probabilities are ℝ≥0∞ with ∑' j, P i a j = 1 for a ∈ A i.
• A history at time $n$ is a pair Fin (n+1) → S, Fin n → Act; a policy assigns to every history a distribution on the action set of its last state. The probability of a history is the product of the policy and transition probabilities; expectations are ℝ≥0∞ sums over histories, so no integrability conditions arise.
• All values ($v_{\theta,\alpha,n}$, $V_{\theta,\alpha}$, $v_{\alpha,n}$, $V_\alpha$, and the competing solutions $W$) are ℝ≥0∞-valued; $0 \cdot \infty = 0$. The discount factor is α : ℝ≥0 with 0 < α and α < 1. Terminal costs are zero.
• $V_\alpha$ and $v_{\alpha,n}$ are infima over the type of all general policies. Defining them over stationary policies only would make the optimality of $f_\alpha$ a tautology; that formalization is ruled out.
• Proposition 4.4.1: the book states the equivalence without a finiteness assumption, but its necessity argument needs $V_\alpha < \infty$, and necessity fails otherwise. Sufficiency is stated in general and necessity under $V_\alpha < \infty$ everywhere.

Useful infrastructure, reusable by the later missions of this series (approximating sequences, average cost): the shift of a general policy after its first step, the Chapman–Kolmogorov identity for the history law, and the computation $E_f[W(X_{n+1})] = E_f[\sum_j P_{X_n j}(f) W(j)]$ for stationary policies. Contributions of such lemmas, and proofs of any milestone, are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Chapter 4. https://doi.org/10.1002/9780470317037
• D. Blackwell, Discounted dynamic programming, Annals of Mathematical Statistics 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
• R. E. Strauch, Negative dynamic programming, Annals of Mathematical Statistics 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM Journal on Control and Optimization 15 (1977), 438–464. https://doi.org/10.1137/0315031
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Controlled queueing systems (admission control, routing, service-rate selection) are naturally modelled as Markov decision chains whose state is a buffer content and therefore ranges over a countably infinite set. Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, DOI 10.1002/9780470317037) develops the dynamic programming theory for exactly this setting: countable state space, finite action sets, nonnegative and possibly unbounded costs, and value functions that are allowed to be infinite. The book's computational method, the approximating sequence method (ASM), replaces the infinite chain by a sequence of finite truncations and asks when optimal values and policies of the truncations converge to those of the original chain.

This mission is the first of a series on the book. It covers Chapter 3, finite horizon optimization, together with the model of Chapter 2 and three results from Appendices A and B that the chapter uses. The finite horizon theory is the entry point: it is where the book's general policy class, its extended-valued cost criteria and its approximating sequences are first used together.

Setting

A Markov decision chain $\Delta$ has a countable state space $S$; for each $i \in S$ a finite nonempty action set $A_i$; a finite cost $C(i,a) \ge 0$; and for each $a \in A_i$ a transition distribution $(P_{ij}(a))_{j \in S}$. A history at time $t$ is $h_t = (i_0, a_0, \dots, i_{t-1}, a_{t-1}, i_t)$, and a general policy $\theta$ chooses the action at time $t$ from a distribution $\theta(\cdot \mid h_t)$ on $A_{i_t}$: it may use the whole history and may randomize. Stationary policies $f$ ($f(i) \in A_i$) and deterministic Markov policies (a stationary policy for each time) are special cases.

Fix a finite terminal cost $F \ge 0$ and a discount factor $0 < \alpha \le 1$ ($\alpha = 1$ is the undiscounted case). The $n$ horizon expected discounted cost of $\theta$ from initial state $i$ is

$$v_{\theta,\alpha,n}(i) = \sum_{t=0}^{n-1} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i] + \alpha^n E_\theta[F(X_n) \mid X_0 = i],$$

and the value function is $v_{\alpha,n}(i) = \inf_\theta v_{\theta,\alpha,n}(i)$ over all general policies. Both may be $+\infty$. A policy is optimal for the $n$ horizon if it attains $v_{\alpha,n}(i)$ at every $i$. For $n \ge 1$ put $u_{\alpha,n}(i,a) = C(i,a) + \alpha \sum_j P_{ij}(a) v_{\alpha,n-1}(j)$ and let $B_i(\alpha,n)$ be the set of $a \in A_i$ minimizing it.

An approximating sequence $(\Delta_N)_{N \ge N_0}$ has finite nonempty state spaces $S_N$ increasing to $S$, the same actions and costs, and transition distributions $P_{ij}(a;N)$ on $S_N$ converging to $P_{ij}(a)$ as $N \to \infty$. Its value functions are $v^N_{\alpha,n}$. In an augmentation type approximating sequence, the probability $P_{ir}(a)$ of leaving $S_N$ to $r$ is redistributed over $S_N$ by an augmentation distribution $q_j(i,a,r,N)$. Assumption FH($\alpha$, $n$) requires $\limsup_N v^N_{\alpha,n}(i)$ to be finite and at most $v_{\alpha,n}(i)$ for every $i$. A stationary policy $e$ is a limit point of stationary policies $e^N$ if, along a subsequence, $e^{N_r}(i) = e(i)$ eventually for each $i$.

Formalization targets

Goal: Theorem 3.2.3

For fixed $n \ge 1$,

$$\Big(\forall i:\ \lim_{N\to\infty} v^N_{\alpha,n}(i) = v_{\alpha,n}(i) < \infty\Big) \iff \mathrm{FH}(\alpha,n),$$

and under either condition every limit point $e_n$ of stationary policies $e^N_n$ with $e^N_n(i) \in B^N_i(\alpha,n)$ satisfies $e_n(i) \in B_i(\alpha,n)$ for all $i \in S$.

Milestones

1. Proposition A.1.1: a probability average of $u$ is at least $\min u$, with equality iff the distribution is concentrated on the minimizers.
2. Theorem 3.1.2: the finite horizon optimality equation $v_{\alpha,n}(i) = \min_a u_{\alpha,n}(i,a)$, and the characterization of all optimal general policies.
3. Corollary 3.1.4: choosing $f_{n-t}(i) \in B_i(\alpha,n-t)$ yields an optimal deterministic Markov policy.
4. Proposition 2.5.6: the augmentation (2.19) defines an approximating distribution.
5. Lemma 3.2.2: $v^N_{\alpha,0} \to v_{\alpha,0}$ and $\liminf_N v^N_{\alpha,n} \ge v_{\alpha,n}$.
6. Propositions B.3 and B.5: sequences of stationary policies, for $\Delta$ or for $(\Delta_N)$, have limit points.
7. Propositions 3.3.1, 3.3.2 and 3.3.4: three sufficient conditions for FH($\alpha$, $n$), namely bounded costs, an augmentation sending excess probability to a finite set, and the augmentation inequality (3.20).

Significance

Theorem 3.1.2 is the finite horizon dynamic programming equation in the generality the rest of the book needs: the value function is an infimum over history-dependent randomized policies, and the equation holds with infinite values allowed. Its characterization of optimal policies is Bellman's principle of optimality in necessary-and-sufficient form. Corollary 3.1.4 shows that deterministic Markov policies suffice. The discounted chapter builds on these results, since its value function is the limit of finite horizon ones, and so does the value iteration algorithm of the average cost chapters.

Theorem 3.2.3 is the finite horizon case of the approximating sequence method. It says exactly when finite truncations give the right answer, and it reduces the question to Assumption FH, for which Section 3.3 gives checkable conditions. The same structure (a lim inf inequality, a lim sup assumption, a limit point of optimal truncated policies) recurs for the discounted and the average cost criteria in later chapters.

The results are proved in the book. None of them is formalized: the platform has finite horizon dynamic programming only for Markov policies, abstract monotone mappings or finite reward-maximizing MDPs, and nothing on approximating sequences. A formalization contributes a Lean model of Markov decision chains with general policies and extended-valued criteria, which the later missions of the series restate and can merge with this one.

Difficulty

The obvious proof of the optimality equation conditions on the first action and state and then applies the induction hypothesis to the rest of the trajectory. With general policies the rest of the trajectory is governed by a continuation policy that depends on the first state and action, and the decomposition of the path law into a first step and a continuation must be proved from the definition of the process, not assumed. Infinite values also make the "only if" direction delicate: a strict inequality between expected costs becomes an equality once both sides are infinite.

For approximating sequences, the natural idea is to pass to the limit in the optimality equation of $\Delta_N$. This fails in general. Example 3.2.1 of the book has $\lim_N v^N_{1,2}(0) = 2 > 1 = v_{1,2}(0)$, because truncation moves probability onto states of high cost and dominated convergence is not available. Only the lim inf inequality holds for free, through a generalized Fatou lemma for approximating distributions. The lim sup side is exactly what Assumption FH supplies. The limit point argument then needs the compactness statement of Appendix B and the fact that a lim inf can be passed through a minimum over a finite set.

Formalization scope

The state space is a type S with [Countable S], the actions a type Act, and A i : Finset Act is nonempty. Costs are ℝ≥0, transition probabilities ℝ≥0∞ summing to 1 over S, and all values and expectations are in ℝ≥0∞, so infima over policies are lattice infima and +∞ is a genuine value. A history is the list of past state–action pairs, most recent first, with the current state, and a policy gives a distribution on A i for every history. Expectations are sums over histories of the path probabilities $\prod \theta(a_s \mid h_s) P_{i_s i_{s+1}}(a_s)$, which is the book's (2.6) and (2.9), not the dynamic programming recursion. The discount factor satisfies $0 < \alpha \le 1$ in every statement. An approximating sequence is indexed by $N \in \mathbb N$ with a start level $N_0$; its value functions are set to $0$ for the finitely many $N$ at which a given state is not yet in $S_N$, which does not affect limits.

The optimality equation must not be made definitional by defining $v_{\theta,\alpha,n}$ or $v_{\alpha,n}$ through the recursion (3.2). The policy class must not be restricted to deterministic Markov policies either, since that would make the characterization in Theorem 3.1.2 a different statement. Theorem 3.1.2(ii)(2) is stated with the guard $v_{\alpha,n}(i) < \infty$; the book omits it, and without it the "only if" direction is false (see the item's note).

A complete development needs the first-step decomposition of the path law under a general policy, the generalized Fatou lemma for approximating distributions (Proposition A.2.5, a milestone of the Appendix A mission of this series), and lim inf / lim sup manipulations in ℝ≥0∞. The model definitions are reusable by every later mission of the series. Contributions are welcome at every milestone, including proofs of the definitional sanity facts (for instance $v_{\theta,\alpha,0} = F$).

Selected references

• Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. https://doi.org/10.1002/9780470317037
• Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994 (the standard reference for finite horizon dynamic programming with history-dependent randomized policies).
• Richard Bellman, Dynamic Programming, Princeton University Press, 1957.

Motivation

Service parts (spare engines, avionics modules, repairable components) are usually managed one unit at a time: whenever a customer order removes a unit from stock, a replacement is ordered at once, from a repair shop or an outside supplier. This is the (s–1, s) policy, under which the inventory position (on hand plus on order minus backorders) stays constant at the stock level $s$. Every performance measure of such a system (fill rate, expected backorders, availability) is a function of one random variable: the number of units in resupply, i.e. ordered but not yet returned. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005) computes its distribution, and the rest of the book (the METRIC-type multi-echelon models of Chapters 4 and 5, the stock-level optimization of Section 3.4) is built on that computation.

Timeline. C. Palm (1938) showed, in the setting of telephone traffic, that in an infinite-server system with Poisson arrivals the number of busy servers has, in steady state, a Poisson law whose mean is the arrival rate times the mean service time, whatever the service-time distribution. Feeney and Sherbrooke (1966) carried the result to (s–1, s) inventory systems with compound Poisson demand, and treated the lost-sales case. Sherbrooke's METRIC model (1968) made the Poisson law of units in resupply the basis of multi-echelon spare-parts planning.

Setting

A single item is stocked at one location. Customer orders arrive at epochs $T_0 < T_1 < \cdots$ of a Poisson process with rate $\lambda > 0$, started empty at time $0$: the interarrival times $A_k$ are independent and exponential with rate $\lambda$, and $T_k = A_0 + \cdots + A_k$. The $k$-th order triggers a resupply order with resupply time $L_k \ge 0$. The resupply times are independent and identically distributed, independent of the arrival process, with a density $g$, distribution function $G(u) = P[L \le u]$ and finite mean

$$\bar\tau = E[L] = \int_0^\infty [1 - G(u)]\,du .$$

With backorders allowed, the number of units in resupply at time $t$ is

$$X(t) = \#\{k : T_k \le t < T_k + L_k\},$$

and $N(t) = \#\{k : T_k \le t\}$ counts the orders placed in $[0,t]$. On-hand stock and backorders at time $t$ are $(s - X(t))^+$ and $(X(t) - s)^+$.

In the compound Poisson version the $k$-th order asks for $X_k \ge 1$ units, the sizes are i.i.d. with $u_j = P[X_k = j]$, independent of arrivals and resupply times, and all units of one order share its resupply time $L_k$. The units in resupply are $Y(t) = \sum_{k : T_k \le t < T_k + L_k} X_k$. Writing $u^{(y)}_n$ for the probability that $y$ orders ask for $n$ units in total, the compound Poisson probabilities with parameter $\mu$ are

$$p(n \mid \mu) = \sum_{y=0}^{n} \frac{\mu^y e^{-\mu}}{y!}\,u^{(y)}_n .$$

In the lost-sales version an order that finds no stock on hand is lost, so at most $s$ units are ever in resupply.

Formalization targets

Goal: Palm's theorem (Theorem 6, p. 39)

For every $x \ge 0$,

$$\lim_{t\to\infty} P[X(t) = x] = e^{-\lambda\bar\tau}\frac{(\lambda\bar\tau)^x}{x!}.$$

The resupply-time law enters only through its mean. This is the statement the book's proof establishes and every later chapter uses.

The proof's milestones (pp. 38–41)

1. Eq. (3.5): $P[N(t) = n] = e^{-\lambda t}(\lambda t)^n/n!$.
2. Eq. (3.3): given $N(t) = n$, the epochs $(T_0, \dots, T_{n-1})$ have density $n!/t^n$ on $0 < t_1 < \cdots < t_n < t$.
3. Eq. (3.7): given $N(t) = n$, $X(t)$ is binomial with parameters $n$ and $p = \frac1t\int_0^t[1-G(u)]\,du$.
4. Eq. (3.8): for every $t > 0$, $X(t)$ is Poisson with mean $\lambda\int_0^t[1-G(u)]\,du$.
5. Eq. (3.10): $\int_0^t[1-G(u)]\,du \to \bar\tau$.

Extensions in Section 3.1

6. Theorem 7 (pp. 43–44): with compound Poisson demand, $\lim_{t\to\infty}P[Y(t) = n] = p(n \mid \lambda\bar\tau)$.
7. Theorem 8 (p. 44): in the lost-sales system with exponential resupply times of rate $\beta$, the probability vectors solving the balance equations are exactly the truncated Poisson law $\pi_x \propto (\lambda/\beta)^x/x!$, $0 \le x \le s$.
8. Theorem 9 (pp. 46–47): for a due-date delay $T \ge 0$, the units in resupply that have been there for at least $T$ satisfy $\lim_{t\to\infty}P[Y_T(t) = n] = p(n \mid \lambda\bar\tau\alpha)$ with $\alpha = \frac1{\bar\tau}\int_T^\infty[1-G(t)]\,dt$.

Significance

The result. Palm's theorem turns an infinite-dimensional object (the whole resupply-time distribution) into one number, $\bar\tau$. This insensitivity is what makes spare-parts planning computable: the expected backorders at stock level $s$ are $\sum_{x > s}(x - s)\,p(x \mid \lambda\bar\tau)$, the fill rate is $P[X \le s - 1]$, and both can be optimized over $s$ with only the demand rate and mean repair time as data. Theorem 7 extends this to batch demand, Theorem 9 to systems allowed a response time, and Theorem 8 gives the exact law when shortages are lost instead of backordered.

Formalizing it. All of these results are classical and proved. None of them is formalized on the platform, and Mathlib has Poisson and exponential distributions but no Poisson process, no thinning theorem and no infinite-server queue. The mission produces a Poisson arrival stream built from i.i.d. exponential gaps, the conditional-uniformity property of its epochs, independent thinning, and the M/G/∞ transient law, all reusable in queueing and inventory missions.

Difficulty

The algebra of the proof (summing the binomial against the Poisson law of $N(t)$) is short. The work is in the probabilistic step the book treats in a sentence: that, given $N(t) = n$, the $n$ orders behave like independent uniform epochs, each of which independently is still in resupply at time $t$ with the same probability $p$. This needs the joint law of the partial sums of exponential variables (Eq. (3.3)), and then a symmetrization argument, since the epochs are ordered while the resupply times are attached to order indices. The naive route of computing $P[X(t) = x]$ by conditioning on individual epochs does not go through without that exchangeability step. The limit $t \to \infty$ is then elementary; stating a stationary version directly is not a substitute, since the book's "steady state" is exactly this limit.

Formalization scope

The model is a structure on a probability space $(\Omega, P)$: exponential interarrival times with rate $\lambda > 0$, nonnegative resupply times with a density and an integrable first coordinate, and mutual independence of the whole family. Orders are indexed from $0$, so the book's $X_1, \dots, X_n$ are $T_0, \dots, T_{n-1}$. Counts are cardinalities of sets of order indices, with value $0$ on the probability-zero event where infinitely many orders fall in a bounded interval.

Commitments and pinnings:

• "Steady state probability" (Theorems 6, 7, 9) is $\lim_{t\to\infty}P[\cdot(t) = x]$ for the system empty at time $0$, which is what the proofs compute via (3.8)–(3.11).
• Independence of resupply times from arrivals is not written in Theorem 6 but is used on p. 40; it is part of the model.
• The stock level $s$ does not enter the backorder model; it matters only in Theorem 8.
• Theorem 8 is stated algebraically: a vector on $\{0, \dots, s\}$ solves the balance equations (3.26), (3.25) for $0 < j < s$ and (3.32), and sums to one, if and only if it is the truncated Poisson law. The book obtains these equations by letting $t \to \infty$ in the forward equations under the unproved assumption $P_j'(t) \to 0$. The book writes (3.25) "for $0 \le j \le s$", which at $j = s$ contradicts its own (3.32); the boundary equation (3.32) is used. The sentence on p. 46 extending Theorem 8 to arbitrary resupply densities is asserted without proof and is not stated.
• Theorem 7 identifies the limit law by its probabilities (3.22)–(3.23); its mean $\lambda\bar\tau\bar u$ is a property of that law. Theorem 9 is stated for compound demand as the book states it, although the book's proof covers only the Poisson case.

A model in which $X(t)$ is postulated through its law, or in which resupply times may depend on the arrival epochs, makes the goal empty or false; here $X(t)$ is computed from the primitive arrival and resupply times, whose joint law is fully specified.

Welcome contributions: a general Poisson-process library (construction from exponential gaps, Poisson marginals, order-statistics property), independent thinning, and proofs of the milestones in the listed order.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, 2005, Chapter 3. https://doi.org/10.1007/b138879
• C. Palm, "Analysis of the Erlang traffic formula for busy-signal arrangements", Ericsson Technics 5, 1938, 39–58.
• G. J. Feeney and C. C. Sherbrooke, "The (s–1, s) inventory policy under compound Poisson demand", Management Science 12(5), 1966, 391–411. https://doi.org/10.1287/mnsc.12.5.391
• C. C. Sherbrooke, "METRIC: A multi-echelon technique for recoverable item control", Operations Research 16(1), 1968, 122–141. https://doi.org/10.1287/opre.16.1.122
• S. M. Ross, Stochastic Processes, 2nd ed., Wiley, 1996, Section 2.3 (conditional distribution of arrival times) and Section 2.4 (the M/G/∞ queue).

Motivation

Fictitious play is the oldest model of learning in games: players repeatedly play a fixed normal form game, and each round every player best-responds to the empirical frequencies of the opponents' past play. Brown (1951) proposed it as an algorithm for computing the value of a zero-sum game, and Robinson (1951) proved that the empirical frequencies converge to the set of equilibria in that case. In stochastic fictitious play (Fudenberg and Kreps 1993) each player's payoffs are perturbed by fresh random shocks before every choice. The shocks make best responses single-valued and smooth in beliefs, which puts the process within reach of stochastic approximation theory: its long-run behaviour is governed by a deterministic perturbed best response dynamic.

Before Hofbauer and Sandholm (2002), convergence of stochastic fictitious play was known only for 2×2 games (Fudenberg and Kreps 1993; Kaniovski and Young 1995) and for certain games with two strategies per player (Benaïm and Hirsch 1999). The difficulty was the perturbed dynamic itself, whose vector field involves choice probabilities with no closed form for general noise distributions. Hofbauer and Sandholm showed that every such dynamic can be rewritten with a deterministic payoff perturbation (their Theorem 2.1), and used that to carry Lyapunov functions over to arbitrary noise distributions. This mission covers the first two classes of games in their main convergence theorem: symmetric games with an interior evolutionarily stable strategy, and two player zero-sum games.

Setting

A two player normal form game has strategy sets $S^1 = \{1,\dots,n^1\}$ and $S^2 = \{1,\dots,n^2\}$ and utilities $u^\alpha : S^1 \times S^2 \to \mathbb R$. Player $\alpha$'s mixed strategies form the simplex $\Delta S^\alpha$, and $\Sigma = \Delta S^1 \times \Delta S^2$. The payoff vector $U^\alpha(x^{-\alpha}) \in \mathbb R^{n^\alpha}$ lists the expected payoff of each pure strategy of $\alpha$ against the opponent's mixed strategy. The game is zero-sum if $u^1(s) = -u^2(s)$ for every profile $s$.

Each player $\alpha$ has a shock density $f^\alpha$ on $\mathbb R^{n^\alpha}$. The choice function $C^\alpha(\pi)_i = P(\operatorname{argmax}_j \pi_j + \varepsilon_j = i)$, for $\varepsilon$ with density $f^\alpha$, gives the perturbed best response $\tilde B^\alpha(x^{-\alpha}) = C^\alpha(U^\alpha(x^{-\alpha}))$. The densities are required to be strictly positive with continuously differentiable choice functions ("the conditions of Theorem 2.1").

Standard stochastic fictitious play. Pure strategies are identified with basis vectors $e_i$. Choices $\zeta_1$ are arbitrary. At every time $t \ge 1$ each player $\alpha$ draws a shock $\varepsilon^\alpha_t$ with density $f^\alpha$ and plays at time $t+1$ the pure strategy maximizing $U^\alpha_k(Z^{-\alpha}_t) + (\varepsilon^\alpha_t)_k$, where the beliefs are the time averages

$$Z_t = \frac1t \sum_{u=1}^t \zeta_u \in \Sigma .$$

The shocks are independent over time and across players. The expected motion of $Z_t$ is the perturbed best response dynamic

$$\text{(P)}\qquad \dot x^\alpha = \tilde B^\alpha(x^{-\alpha}) - x^\alpha \quad\text{on } \Sigma .$$

Symmetric games. A two player game is symmetric if $S^1 = S^2 = \{1,\dots,m\}$ and $u^1(i,j) = u^2(j,i)$; it is described by the matrix $A_{ij} = u^1(i,j)$, and $U^1(z) = Az$. In symmetric stochastic fictitious play two players in roles 1 and 2 play at every time, their shocks are independent and identically distributed with one density $f$, and the state is the average of all past plays in both roles,

$$\hat Z_t = \frac1{2t}\sum_{u=1}^t \big(\hat\zeta^1_u + \hat\zeta^2_u\big) \in \Delta S^1 .$$

Its mean dynamic is $\text{(SP)}\ \dot x = C(Ax) - x$ on $\Delta S^1$. A mixed strategy $x^*$ in the interior of $\Delta S^1$ is an interior evolutionarily stable strategy (ESS) if $x^*\cdot Ax > x\cdot Ax$ for all mixed $x \ne x^*$ near $x^*$.

Rest points and chain recurrence. For a dynamic $\dot x = F(x)$ on a compact set $X$, the rest points are the zeros of $F$ in $X$. A point $x$ is chain recurrent if for every $\varepsilon > 0$ one can return from $x$ to $x$ by following solution segments of length at least $1$, with jumps of size less than $\varepsilon$ between segments.

Formalization targets

Goal: Theorem 6.1 (i) and (ii)

(i) If $A$ has an interior ESS, then (SP) has a unique rest point $\hat x$ and

$$P\Big(\lim_{t\to\infty} \hat Z_t = \hat x\Big) = 1 .$$

(ii) If the two player game is zero-sum, then (P) has a unique rest point $x^*$ and

$$P\Big(\lim_{t\to\infty} Z_t = x^*\Big) = 1 .$$

Both hold for all shock densities meeting the conditions of Theorem 2.1, all probability spaces carrying the shocks, and all initial choices.

Milestones

1. Theorem 2.1: for such a density, the choice function $C$ is the unique maximizer $C(\pi) = \operatorname{argmax}_{y \in \operatorname{int}\Delta}(y\cdot\pi - V(y))$ for one admissible deterministic perturbation $V$.
2. With an interior ESS, $\hat\Lambda(x) = x\cdot Ax - V(x) - W(Ax)$, where $W(\pi) = \max_y (y\cdot\pi - V(y))$, is strictly concave and a strict Lyapunov function for the deterministically perturbed dynamic (SPV).
3. Its maximizer is the unique chain recurrent point of (SPV).
4. In zero-sum games, $\Lambda(x^1,x^2) = -V^1(x^1) - W^1(U^1(x^2)) - V^2(x^2) - W^2(U^2(x^1))$ is strictly concave and a strict Lyapunov function for (PV).
5. Its maximizer is the unique chain recurrent point of (P).
6. The maximizer of $\hat\Lambda$ is the unique chain recurrent point of (SP).

Significance

The theorem gives global, almost sure convergence of a learning process for arbitrary noise distributions, not only for the logit (Gumbel) noise under which the perturbed dynamic has a closed form. For zero-sum games it is the stochastic counterpart of Robinson's theorem. For symmetric games with an interior ESS it shows that a population learning by stochastic fictitious play settles at a single mixed state. Since the choice functions are continuous, the players' choice probabilities converge as well. The limit is the rest point of the perturbed dynamic, which approximates a Nash equilibrium (in case (i), the ESS) as the noise vanishes.

On the formal side, the paper's results are proved, but no part of them is machine-checked, and the platform has no model of learning in games, of chain recurrence, or of stochastic approximation. The mission produces a formal model of stochastic fictitious play as a random process, formal statements of the Hofbauer and Hofbauer–Hopkins Lyapunov functions, and the chain recurrence characterizations that connect them to the process.

Difficulty

The obvious route replaces the process $Z_t$ by the ODE (P) and argues that (P) converges. That step is where the argument is incomplete: convergence of every solution of (P) does not give convergence of the stochastic process, because a stochastic approximation can in principle circulate near a set of orbits the ODE never follows. The right invariant is the chain recurrent set, and the limit sets of the process lie in a connected component of it (Benaïm and Hirsch 1999; Benaïm 1999). The characterization therefore has to be of chain recurrence, which is strictly weaker than asymptotic stability of individual orbits.

The second obstacle is that (P) itself is defined through the noise distribution and admits no useful Lyapunov function in general. The Lyapunov functions exist for the deterministic form (PV)/(SPV), and moving between the two forms requires the representation of Theorem 2.1, whose perturbation $V$ has no closed form either.

Formalization scope

Players and strategies are indexed from $0$. Mixed profiles live in $\prod_\alpha \mathbb R^{n^\alpha}$ and every vector field is defined on that ambient space. The processes are defined pathwise from a family of shock vectors on an arbitrary probability space. Ties in the argmax are broken by the smallest index, an event of probability zero because the shocks have densities. The shock drawn at time $t$ produces the choice at time $t+1$. Shock densities are arbitrary strictly positive densities with continuously differentiable choice functions; no noise law is fixed, and the two players' densities in (ii) may differ. Independence is joint over times and players (and roles in (i)). The symmetric process has its own state in one simplex and is not the standard process applied to a symmetric game.

Deterministic perturbations are functions defined on the whole space whose values off the open simplex are ignored; derivatives are taken of their composition with the projection onto the affine plane $\{\sum_i y_i = 1\}$. Perturbed best responses in (PV) and (SPV) are supplied as maps together with the hypothesis that they are the unique maximizers. A strict Lyapunov function must increase strictly along every non-constant solution on $(0,\infty)$. The ESS definition includes $x \ne x^*$, which the source omits.

The conclusions assert existence and uniqueness of the rest point; they are not hypotheses. A statement for the ODE (P) in place of the process $Z_t$, for one fixed noise law, or with the ESS as the limit point would be a different theorem.

A complete development needs Theorem 2.1 (convex duality and the Legendre transform on the simplex), existence and uniqueness of solutions of (P), basic chain recurrence theory, and the stochastic approximation results of Benaïm and Hirsch, which are not restated here and are welcome as independent contributions. The model layer (games, payoff vectors, choice functions, stochastic fictitious play) is shared with the other missions of this series.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2265–2294, 2002. https://doi.org/10.1111/1468-0262.00376 (theorem numbers and pages here follow the authors' manuscript of February 21, 2002).
• D. Fudenberg and D. M. Kreps, Learning Mixed Equilibria, Games and Economic Behavior 5, 320–367, 1993. https://doi.org/10.1006/game.1993.1021
• Y. M. Kaniovski and H. P. Young, Learning Dynamics in Games with Stochastic Perturbations, Games and Economic Behavior 11, 330–363, 1995. https://doi.org/10.1006/game.1995.1054
• M. Benaïm and M. W. Hirsch, Mixed Equilibria and Dynamical Systems Arising from Fictitious Play in Perturbed Games, Games and Economic Behavior 29, 36–72, 1999. https://doi.org/10.1006/game.1999.0717
• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, 1–68, 1999. https://doi.org/10.1007/BFb0096509
• J. Robinson, An Iterative Method of Solving a Game, Annals of Mathematics 54, 296–301, 1951. https://doi.org/10.2307/1969530
• J. Hofbauer and E. Hopkins, Learning in Perturbed Asymmetric Games, Games and Economic Behavior 52, 133–152, 2005. https://doi.org/10.1016/j.geb.2004.06.006