Markov Chain

Motivation

Controlled Markov processes with the average cost criterion model systems that run indefinitely, such as queues, inventories, maintenance and communication networks, where only the long-run cost per unit time matters. The standard route to an optimal stationary policy goes through the average cost optimality equation (ACOE). The ACOE is usually obtained by the vanishing discount method: solve the discounted problem for each discount factor $\beta<1$ and let $\beta\to1$. The method works only when the differences of discounted values stay bounded as $\beta\to1$. Conditions that guarantee this are therefore central in the survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993), §5).

This mission formalizes one such condition, due to Ross: if the mean return time to a fixed state is bounded uniformly over all stationary policies and initial states, the differential discounted value functions are bounded uniformly in the discount factor and the state.

Timeline. Derman (Management Sci. 9 (1962); survey reference [38]) and Derman–Veinott (Ann. Math. Statist. 38 (1967); survey reference [43]) introduced recurrence conditions of this kind for countable-state processes. Ross (Ann. Math. Statist. 39 (1968), survey reference [147]; Introduction to Stochastic Dynamic Programming, 1983, survey reference [150]) showed, for bounded costs, that under a Derman–Veinott type recurrence condition $h_\beta$ is bounded uniformly in $\beta$, and obtained a bounded solution of the ACOE by letting $\beta\uparrow1$ (survey, pp. 291 and 301). Later work replaced the condition with weaker ones (survey Assumptions 5.1–5.3) and with Sennott's conditions (survey Theorem 5.9).

Setting

The state space is $S=\{0,1,2,\dots\}$. In each state $i$, an action $a$ is chosen from a nonempty compact set $U(i)$ of a metric space $A$. The one-stage cost $c(i,a)$ is nonnegative and the next state is drawn from the transition law $P(\cdot\mid i,a)$. For fixed $i,j$, the maps $a\mapsto c(i,a)$ and $a\mapsto P(j\mid i,a)$ are continuous on $U(i)$. A policy $\pi\in\Pi$ chooses the action at time $t$ at random, given the whole history, and must choose from $U(X_t)$. A stationary deterministic policy $f\in\Pi_{SD}$ is a map $f:S\to A$ with $f(i)\in U(i)$. $P^\pi_i$ and $E^\pi_i$ denote the law and the expectation of the controlled process $(X_t,A_t)$ started at $i$.

For a discount factor $\beta\in(0,1)$, the discounted cost and the optimal discounted cost are

$$J_\beta(i,\pi)=E^\pi_i\Big[\sum_{t=0}^\infty\beta^t c(X_t,A_t)\Big],\qquad J^*_\beta(i)=\inf_{\pi\in\Pi}J_\beta(i,\pi).$$

A policy $f\in\Pi_{SD}$ is $\beta$-discount optimal if $J_\beta(i,f)=J^*_\beta(i)$ for all $i$. The differential discounted value function is

$$h_\beta(i)=J^*_\beta(i)-J^*_\beta(0),$$

measured relative to the fixed state $0$. The return time to $0$ is

$$\tau=\min\{t\ge1:\ X_t=0\},$$

with $\tau=\infty$ if the process never returns. Throughout, as in §5.1 of the survey, the cost is bounded: $c(i,a)\le M$ on admissible pairs.

Formalization targets

Goal: Theorem 5.3

If there is a constant $K>0$ with

$$E^f_i[\tau]<K\qquad\text{for all } f\in\Pi_{SD},\ i\in S, \tag{5.7}$$

then there is a constant $B$ such that

$$|h_\beta(i)|\le B\qquad\text{for all }\beta\in(0,1),\ i\in S.$$

This is the theorem as printed: it asserts only uniform boundedness and fixes no constant.

Milestones

1. Theorem 2.1 (iii): for every $\beta\in(0,1)$, a $\beta$-discount optimal $f_\beta\in\Pi_{SD}$ exists.
2. (5.8): for such an $f_\beta$, $J^*_\beta(i)\le M\,E^{f_\beta}_i[\tau]+J^*_\beta(0)\,E^{f_\beta}_i[\beta^\tau]$.
3. (5.9): $J^*_\beta(i)-\beta J^*_\beta(0)\le MK$.
4. Jensen step: $J^*_\beta(i)\ge J^*_\beta(0)\,E^{f_\beta}_i[\beta^\tau]\ge J^*_\beta(0)\,\beta^K$.
5. (5.10): $J^*_\beta(0)-J^*_\beta(i)\le(1-\beta^K)J^*_\beta(0)\le(1-\beta^K)\frac{M}{1-\beta}\le MK$.
6. Explicit bound: $|h_\beta(i)|\le MK$. This is stronger than the goal and is the constant the survey's argument yields.

Significance

The result. Theorem 5.3 verifies the hypothesis of the vanishing discount theorem (Theorem 5.2 of the survey) from a condition on the uncontrolled dynamics of stationary policies. Theorem 5.2 then gives a bounded solution $(\rho,h)$ of the ACOE, an average optimal stationary policy, and the limit $\lim_{\beta\to1}(1-\beta)J^*_\beta(i)=\rho$. Mean return times can often be estimated directly, for instance through Foster–Lyapunov drift arguments on queues, which makes (5.7) checkable in applications. The explicit bound $MK$ also controls the span of the relative value function.

Formalizing it. The result is proved in the literature; to our knowledge it has not been machine-checked. A formal proof needs discounted dynamic programming on a countable state space with compact action sets, the existence of optimal stationary policies (Theorem 2.1 (iii), which the survey cites without proof), and the strong Markov property of the controlled chain at a return time. All of these are reusable well beyond this mission.

Difficulty

The estimates (5.9) and (5.10) are elementary once (5.8) and the existence of $f_\beta$ are available. The weight lies elsewhere.

• Optimal stationary policies. The infimum defining $J^*_\beta$ ranges over all history-dependent randomized policies. Bringing it down to a single stationary deterministic policy requires the discounted optimality equation, a measurable selection of minimizers on compact action sets, and a verification argument against arbitrary policies.
• Restarting at $\tau$. (5.8) splits the discounted cost at the random time $\tau$. The tail must be identified with $\beta^\tau$ times the discounted cost from state $0$. This is the strong Markov property for the process built by the Ionescu-Tulcea theorem, applied at a stopping time that may be infinite.

Formalization scope

• The state space is ℕ; the action space is a metric space with its Borel $\sigma$-algebra. The model CMP carries compact nonempty $U(i)$, a nonnegative measurable cost, and continuity of $c(i,\cdot)$ and $P(j\mid i,\cdot)$ on $U(i)$, the standing assumptions of §5.
• Policies are history-dependent, randomized and admissible. The path measure is Mathlib's Kernel.trajMeasure. $J^*_\beta$ is an infimum over all such policies, not over Markov or stationary policies only.
• Costs are lower Lebesgue integrals in $[0,\infty]$. $h_\beta$ is the difference of the real parts of $J^*_\beta(i)$ and $J^*_\beta(0)$. This is exact here because bounded cost gives $J^*_\beta\le M/(1-\beta)<\infty$.
• Explicit choices:
  • The bounded-cost hypothesis $c\le M$ on admissible pairs is a binder of every §5.1 statement. It is the section's standing assumption, and without it the theorem is false.
  • $\tau$ counts from $t\ge1$ and takes values in $\mathbb N\cup\{\infty\}$, so (5.7) applies from $i=0$ and forces $\tau<\infty$ almost surely; $\beta^\tau=0$ on $\{\tau=\infty\}$.
  • The typo $\beta^n$ in (5.8) is read as $\beta^t$.
  • $K\ge1$ in (5.10) is not assumed; it follows from (5.7).
• Theorem 2.1 is stated in the survey for Borel models under Assumptions 2.1–2.3. Here it is posed in the countable model, where those assumptions follow from the §5 continuity and compactness assumptions.
• The goal's bound $B$ is quantified before $\beta$ and $i$. A per-$\beta$ or per-state bound would be trivial, since every $h_\beta(i)$ is a finite number.
• Welcome contributions include discounted dynamic programming on countable state spaces, the strong Markov property for trajMeasure, and return-time estimates.

Selected references

• A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993) 282–344. https://doi.org/10.1137/0331018
• C. Derman, On sequential decisions and Markov chains, Management Sci. 9 (1962) 16–24. https://doi.org/10.1287/mnsc.9.1.16
• C. Derman, A. F. Veinott Jr., A solution to a countable system of equations arising in Markovian decision processes, Ann. Math. Statist. 38 (1967) 582–584 (cited as [43] in the survey, https://doi.org/10.1137/0331018).
• S. M. Ross, Non-discounted denumerable Markovian decision models, Ann. Math. Statist. 39 (1968) 412–423 (cited as [147] in the survey, https://doi.org/10.1137/0331018).
• S. M. Ross, Introduction to Stochastic Dynamic Programming, Academic Press, 1983 (cited as [150] in the survey, https://doi.org/10.1137/0331018).

Why average cost is a control problem

A controller acting over an indefinite horizon must decide whether a lower cost today is worth a higher cost later. Average cost measures the expected expenditure per stage as the horizon grows. It is appropriate when operation has no natural terminal date, but its limiting definition makes it difficult to compute an optimal policy directly. Discounted cost assigns less weight to distant stages and has a more direct optimality equation. Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus survey these criteria for controlled Markov processes and state a condition under which solving one discounted problem yields a solution to an average-cost problem (Arapostathis et al., 1993, §5.1).

The condition is a common lower bound on the one-step probability of moving to a distinguished state. Ross's reduction, reported as Theorem 5.6 of the survey, uses that bound to define a new transition law and a specific discount factor. The survey's theorem states the reduction informally; its proof specifies the transformed law, the optimality equation and the resulting average-cost policy. Those claims are the targets of this mission (Arapostathis et al., 1993, pp. 303–304).

Controlled process and criteria

The state space is $S=\{0,1,2,\ldots\}$. In state $i$, the controller may choose an action $a$ from a nonempty compact set $U(i)$ in a metric action space. Choosing $a$ incurs the one-stage cost $c(i,a)\ge0$ and moves the state to $j$ with probability $P(j\mid i,a)$. The cost is measurable, and for each fixed $i,j$ its value and $P(j\mid i,a)$ vary continuously with $a$ on $U(i)$. Section 5 imposes these state and continuity conventions; §5.1 additionally assumes the costs are bounded (Arapostathis et al., 1993, pp. 284–288, 299, 301).

An admissible policy $\pi$ chooses a probability law for the next action from the entire observed history, and assigns probability one to admissible actions. A stationary deterministic policy is a map $f$ with $f(i)\in U(i)$; it always takes action $f(i)$ in state $i$. These are distinct classes. Let $J_N(i,\pi)$ be expected cost over the first $N$ stages from $i$, and let $J_\beta(i,\pi)$ be expected cost when stage $t$ is weighted by $\beta^t$, where $0<\beta<1$. The average-cost criterion is $J(i,\pi)=\limsup_{N\to\infty}J_N(i,\pi)/N$. The optimal values $J^*(i)$ and $J_\beta^*(i)$ are infima over all admissible policies, including randomized and history-dependent ones (Arapostathis et al., 1993, pp. 285–287).

The average cost optimality equation, or ACOE, asks for a scalar $\rho$ and a real function $h$ such that, for each state $i$,

$$\rho+h(i)=\min_{a\in U(i)}\left\{c(i,a)+\sum_{j\in S}P(j\mid i,a)h(j)\right\}.$$

The minimum is attained. The survey's verification theorem identifies $\rho$ with the optimal average cost when the terminal contribution of $h(X_t)$ vanishes after division by $t$ (Arapostathis et al., 1993, p. 299, (5.1), Theorem 5.1).

Formalization targets

The reduction

Assume that $P(0\mid i,a)\ge\alpha$ on every admissible state-action pair for a single constant $0<\alpha<1$. The transformed process $\widetilde M$ has the same admissible actions and costs and has transition probabilities

$$\widetilde P(j\mid i,a)=\frac{P(j\mid i,a)-\alpha\mathbf1_{\{j=0\}}}{1-\alpha}.$$

Write $\widetilde J^*_{1-\alpha}$ for its discounted value at discount factor $1-\alpha$. The goal states that this value is finite, a stationary deterministic discounted-optimal policy exists, and every such policy is average-cost optimal for the original process. It also identifies a constant optimal average cost for every initial state:

$$J^*(i)=\alpha\widetilde J^*_{1-\alpha}(0),\qquad i\in S.$$

The goal does not assume the average optimality that it asserts. It requires the transformed law to satisfy the displayed formula at every admissible state-action pair (Arapostathis et al., 1993, Theorem 5.6 and proof, pp. 303–304).

Supporting targets

The milestones establish that the transformed law gives a controlled Markov process, that the discounted problem has an optimal stationary deterministic policy, and that the transformed discounted value satisfies the original ACOE with $\rho=\alpha\widetilde J^*_{1-\alpha}(0)$. The final milestone is the ACOE verification theorem needed to identify the average cost. The source gives the first two discounted claims through Theorem 2.1 and writes out the transformed equation in the proof of Theorem 5.6 (Arapostathis et al., 1993, pp. 289, 299, 304).

What the result supplies

The theorem replaces an average-cost optimization problem by one discounted problem with a prescribed discount factor and transition law. It yields a stationary deterministic policy that is optimal even when compared with every history-dependent randomized policy, and it shows that the optimal average cost is independent of the initial state. Without the common return probability, neither this particular law nor this fixed discount factor follows from the survey's argument (Arapostathis et al., 1993, Theorem 5.6).

The survey reports this as a known result of Ross rather than an open conjecture. The formalization work is to give the path measures, value functions, transformed process and verification result machine-checkable meanings. The Lean declarations here are open theorem statements awaiting proofs; compiling a statement with sorry does not establish the mathematical theorem. The policy and cost definitions can also support the other countable-state missions drawn from §5.

Difficulty

The transformed probabilities have to form a measurable stochastic kernel, preserve the action continuity assumptions and yield a controlled process with the original feasible actions and costs. The discounted value must be finite and uniformly bounded before its real form can enter the ACOE. A simple comparison of numerical optimal values is insufficient: a policy chosen in the transformed model must be shown optimal for the original model against the full policy class. The verification theorem also requires control of the terminal expectation of $h(X_t)$ for arbitrary admissible policies, rather than only the stationary policies named in its printed condition (Arapostathis et al., 1993, pp. 299–300, 304).

Formalization scope

Lean uses $\mathbb N$ for the countable state space and Mathlib probability kernels for the transition and randomized decision rules. Strategic path measures are constructed from those kernels. Nonnegative expected costs and their infima live in $[0,\infty]$, so an unbounded integral cannot silently become a finite real value. The transformed discounted value is converted to a real only in conclusions that also assert its finiteness. The ACOE uses real sums with explicit summability and an attained minimum. The model requires a Borel metric action space, nonempty compact action sets, measurable costs, and coordinatewise action continuity of the transition probabilities.

The source's §5.1 bounded-cost assumption is explicit in the goal and its discounted milestones. The displayed transformation needs $\alpha<1$; the paper's theorem sentence gives only $\alpha>0$, so the case $\alpha=1$ is excluded from this version. The paper prints (5.2) for stationary deterministic policies, but the proof uses it for all admissible policies to compare with $J^*$; the verification milestone takes the stronger, proof-supported hypothesis. Expectations in that condition are explicitly integrable. The converse part of Theorem 5.1 is not used and is outside this mission.

The transformed process is represented by another CMP constrained to have exactly the source's action sets, admissible costs and transition formula. A milestone poses its existence. This representation keeps the definition layer free of an unproved stochastic-kernel construction. The discount-optimal policy conclusion ranges over every stationary deterministic policy attaining the transformed discounted value, while the values themselves take infima over all admissible policies. Definitions of admissible path laws and the verification theorem are reusable contributions; proofs of the transformed kernel, stationary discounted existence and ACOE identity are welcome.

Selected references

• A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh and S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM Journal on Control and Optimization 31(2), 282–344, 1993. DOI: 10.1137/0331018.

Motivation

A single-server queue in which customers arrive according to a renewal process and are served in exponentially distributed times is the system GI/M/1. Observed just before successive arrivals, its queue length is a Markov chain on $\{0, 1, 2, \dots\}$, the imbedded chain introduced by D. G. Kendall (Kendall 1953, Ann. Math. Statist. 24, pp. 338–354). Whether this chain settles into a statistical equilibrium, keeps returning to the empty state without one, or drifts off to infinity is the first question asked about the queue, and every later quantity (stationary queue lengths, waiting-time distributions) presupposes the answer.

F. G. Foster's 1953 paper (Foster 1953) answers it for GI/M/1 and for M/G/1 by a different route from Kendall's direct analysis: it first proves general criteria, stated in terms of solutions of linear equations and inequalities in the transition matrix, for a countable Markov chain to be ergodic, recurrent or transient, and then checks them on the two queueing matrices. The criteria are of independent use; one of them (Theorem 2 of the paper) is now known as Foster's criterion, the starting point of the drift (Lyapunov-function) method for stability of Markov chains and queueing networks.

Timeline. Kendall (1951, J. Roy. Statist. Soc. B 13) studied queue-length processes directly, including a recurrence argument for M/G/1 that Foster's §3 reproduces; Kendall (1953) introduced the imbedded-chain method and, for GI/M/1, proved by it that $\rho < 1$ is sufficient for ergodicity (Foster 1953, p. 359); Foster (1953) proved the full classification, ergodic iff $\rho < 1$ and recurrent iff $\rho \le 1$, by the general criteria. This mission treats the GI/M/1 half; a companion mission treats M/G/1.

Setting

A transition matrix on the states $\{0, 1, 2, \dots\}$ is an array $[p_{ij}]$ of nonnegative reals whose rows sum to $1$. For a state $j$, $f_{jj}$ is the probability that the chain started at $j$ returns to $j$ at some later step. The chain is recurrent if $f_{jj} = 1$ for every $j$, transient if $f_{jj} < 1$ for every $j$, and ergodic (recurrent-nonnull, positive recurrent) if moreover every mean recurrence time $\sum_n n f^{(n)}_{jj}$ is finite. Foster's general theorems concern an irreducible chain (every state reachable from every state), assumed aperiodic for simplicity.

The GI/M/1 chain is described by a sequence $a = (a_n)_{n \ge 0}$ of positive numbers with $\sum_n a_n = 1$: $a_n$ is the probability that exactly $n$ services are completed between two arrivals. With the tails $\alpha_i = \sum_{j \ge i+1} a_j$,

$$[p_{ij}] = \begin{bmatrix} \alpha_0 & a_0 & 0 & 0 & \cdots \\ \alpha_1 & a_1 & a_0 & 0 & \cdots \\ \alpha_2 & a_2 & a_1 & a_0 & \cdots \\ \vdots & \vdots & \vdots & \vdots & \end{bmatrix},$$

that is $p_{i0} = \alpha_i$, $p_{ij} = a_{i+1-j}$ for $1 \le j \le i+1$, and $p_{ij} = 0$ for $j > i+1$. In Lean this matrix is gim1Matrix a. The traffic parameter $\rho$ is defined through its inverse,

$$\rho^{-1} = \sum_{n=1}^{\infty} n\, a_n \in (0, \infty],$$

the mean number of service completions per interarrival interval (rhoInv a, and rho a $= \rho$).

Formalization targets

Goal: the classification of GI/M/1 (§4, p. 359)

$$\text{the chain is ergodic} \iff \rho < 1, \qquad \text{the chain is recurrent} \iff \rho \le 1 .$$

Together: ergodic for $\rho < 1$, recurrent-null for $\rho = 1$, transient for $\rho > 1$. The statement carries no constants and leaves the sequence $a$ free apart from positivity and normalization.

Milestones

1. Theorem 7 (p. 358): for a probability distribution $\{p_n\}$ with $p_0 > 0$, the equation $\sum_{n \ge 0} z^n p_n = z$ has a root in $(0, 1)$ iff $\sum_{n\ge1} n p_n > 1$.
2. Theorem 1, sufficiency (p. 355): a nonnull solution of $\sum_i x_i p_{ij} = x_j$ with $\sum_i |x_i| < \infty$ makes the system ergodic.
3. Theorem 1, necessity (p. 355): in an ergodic system every nonnegative solution of $\sum_i x_i p_{ij} \le x_j$ has $\sum_i x_i < \infty$.
4. Theorem 4 (pp. 356–357): the system is transient iff $\sum_j p_{ij} y_j = y_i$ ($i \ne 0$) has a bounded nonconstant solution.

Milestones 2–4 are stated for a general irreducible aperiodic chain.

Significance

The classification tells exactly when the GI/M/1 queue is stable: the stationary distribution of the imbedded chain, which is geometric, exists precisely in the ergodic case $\rho < 1$, and for $\rho > 1$ the queue grows without bound. Theorems 1 and 4 are general tools, reusable for any countable chain: Theorem 1 characterizes ergodicity by summable invariant vectors, Theorem 4 characterizes transience by bounded harmonic functions off one state. Theorem 7 is the extinction criterion of branching processes and recurs throughout applied probability.

All of these results are proved in the literature (Foster 1953; Feller's textbook for Theorem 7 and a version of Theorem 4). As far as a search of the platform shows, none of them has a machine-checked proof; the platform holds related special cases for the G/M/1 queue with a specific interarrival law (QueueingFundamentals.GM1.unique_root_unit_interval, open), but not the general lemma or the classification. A formalization would provide the general criteria as reusable library results and the first verified stability classification of a non-Markovian queue's imbedded chain.

Difficulty

The matrix is explicit, but none of the three properties is a finite computation: ergodicity and recurrence are statements about return times over all horizons, so each direction must go through an existence or nonexistence statement about infinite systems of equations. For the converse directions the obvious argument fails: exhibiting a candidate solution such as $x_i \equiv 1$ shows nothing until it is known that ergodicity forces every such solution to be summable, and showing that no bounded nonconstant solution of (7) exists when $\rho < 1$ requires control of all solutions, not of one. The general criteria themselves rest on limit theorems for $p_{ij}^{(n)}$ and on interchanging infinite sums, and the infinite-mean case $\sum n a_n = \infty$ has to be carried along everywhere.

Formalization scope

• The Markov-chain vocabulary is the published definition QueueingFundamentals_Foundations_MarkovChain: TransitionMatrix (entries p, nonnegativity, rows summing to $1$ via HasSum), returnProb, meanRecurrenceTime, Irreducible, Aperiodic, PositiveRecurrent. "Ergodic" is PositiveRecurrent. IsRecurrent and IsTransient are defined state by state from returnProb; their complementarity for irreducible chains is a theorem, not a definition.
• States are indexed from $0$, as in the paper. The goal quantifies over every TransitionMatrix whose entries equal gim1Matrix a; such a matrix exists for every admissible $a$ (rows sum to $1$), so the statement is not vacuous.
• $\rho^{-1}$ and $\rho$ live in $[0, \infty]$ (ℝ≥0∞), with $\infty^{-1} = 0$: an infinite mean gives $\rho = 0$, and that chain is ergodic.
• The goal does not assume irreducibility or aperiodicity: they follow from $a_n > 0$. Milestones 2–4 carry them, as the paper's standing assumptions (§1).
• Every infinite series appearing in a hypothesis is required to converge (HasSum or Summable), so that a divergent series cannot satisfy an equation or inequality vacuously. In Theorem 1's sufficiency half the $x_i$ may be of either sign. In Theorem 7 the distribution is renamed $q$ to avoid a clash with $p_{ij}$.
• Ruled out as trivializing: defining $\rho$ by a real inverse of a real series, defining "ergodic" as the existence of a summable invariant vector (which is Theorem 1's condition), or stating the goal over a matrix that need not exist.
• Not included: the paper's explicit description of the solutions of (7) for $\rho \ge 1$ via the generating function $(1 - z)\{A(z) - z\}^{-1}$, and the M/G/1 half (Theorems 2, 3, 5), which is the companion mission. Contributions welcome: proofs of the general criteria (reusable for any countable chain), of Theorem 7, and lemmas on the GI/M/1 matrix such as irreducibility and aperiodicity.

Selected references

• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24 (1953), 355–360. https://doi.org/10.1214/aoms/1177728976
• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Ann. Math. Statist. 24 (1953), 338–354 (the paper immediately preceding Foster's in the same issue).
• D. G. Kendall, Some problems in the theory of queues, J. Roy. Statist. Soc. B 13 (1951), 151–185.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, Wiley, 1950.

Motivation

Average cost Markov decision chains model systems that run indefinitely and are judged by their long-run cost per step: admission and routing control in queues, inventory replenishment, machine maintenance. For a finite state space the classical tool is the average cost optimality equation (ACOE)

$$J + h(i) = \min_{a \in A_i}\Big\{C(i,a) + \sum_j P_{ij}(a)\,h(j)\Big\},$$

whose solution gives both the minimum average cost $J$ and an optimal stationary policy. To be useful the equation has to be solved numerically, and the method used in practice is value iteration: compute the minimum $n$-horizon costs $v_n$ and extract $J$ and $h$ from their growth. This mission formalizes Sections 6.4–6.6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037): when the minimum average cost is constant, the ACOE holds, any solution of it is optimal, and value iteration converges, provided the optimal policies are aperiodic. When they are not, a transformation of the model makes them so.

Related classical work includes Blackwell's discrete dynamic programming (1962) and Schweitzer–Federgruen's analysis of undiscounted value iteration (1977); Sennott's treatment derives the ACOE from the discounted value function $V_\alpha$ as $\alpha \to 1^-$, which is the route that extends to countable state spaces in later chapters of the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a finite state space $S$; in each state $i$ a finite nonempty action set $A_i$; nonnegative costs $C(i,a)$; and transition probabilities $P_{ij}(a)$. A policy $\theta$ may use the whole history and randomize; a stationary policy $e$ always chooses $e(i) \in A_i$ in state $i$ and induces a Markov chain with transitions $P_{ij}(e) = P_{ij}(e(i))$.

For a policy $\theta$ and initial state $i$: $v_{\theta,n}(i)$ is the expected cost of the first $n$ steps, $V_{\theta,\alpha}(i)$ the expected $\alpha$-discounted cost, and $J_\theta(i) = \limsup_n v_{\theta,n}(i)/n$ the average cost. The value functions are the infima over all policies: $v_n$, $V_\alpha$ and the minimum average cost $J(i)$. A policy is average cost optimal if $J_\theta \equiv J$.

Section 6.2 of the book provides a stationary policy $f$ that is $\alpha$ discount optimal for all $\alpha$ close to $1$ (a Blackwell optimal policy), and Section 6.3 builds from it a relative value function $w^*$. For a distinguished state $z$ put

$$h_\alpha(i) = V_\alpha(i) - V_\alpha(z), \qquad h(i) = \lim_{\alpha\to1^-} h_\alpha(i), \qquad d_n(i) = h(i) + nJ - v_n(i).$$

For a distinguished state $x$ the finite horizon relative value function is $r_n(i) = v_n(i) - v_n(x)$.

A positive recurrent class $R$ of a Markov chain is aperiodic if $P^{(n)}_{ij} \to \pi_j$ for $i, j \in R$, where $\pi$ is the steady state distribution. Assumption OPA ("optimal policies are aperiodic") requires every positive recurrent class of every average cost optimal stationary policy to be aperiodic. The aperiodicity transformation $\Delta^*$ with $0<\tau<1$ keeps states and actions, scales costs by $\tau$, and sets $P^*_{ij}(a) = \tau P_{ij}(a)$ for $j \ne i$, $P^*_{ii}(a) = \tau P_{ii}(a) + (1-\tau)$.

Formalization targets

Goal: convergence of value iteration (Proposition 6.6.3)

If $J(i) \equiv J$ and Assumption OPA holds, then for any distinguished state $x$

$$\lim_{n\to\infty}[v_n(x) - v_{n-1}(x)] = J, \qquad \lim_{n\to\infty} r_n(i) =: r(i) \text{ exists},$$

$(J, r)$ solves the ACOE, and every limit point of the finite horizon optimal stationary policies is average cost optimal.

Milestones

1. Proposition 6.4.1: unichain structure, bounded $|V_\alpha(i) - V_\alpha(z)|$, or pairwise reachability imply $J(i) \equiv J$, with the implication diagram (6.26).
2. Theorem 6.4.2: under $J(i) \equiv J$, $h$ exists, solves the ACOE (6.31), yields optimal policies, $|d_n| \le L$ and $v_n/n \to J$.
3. Proposition 6.5.1: any finite solution $(F, r)$ of the ACOE (or of the inequality (6.36)) gives $J \equiv F$ and optimal policies, and differs from $h$ by constants on recurrent classes.
4. Lemma 6.6.2: on an aperiodic positive recurrent class of an optimal policy, $d_n$ converges to a constant.
5. Lemma 6.6.5 and Proposition 6.6.6: $\Delta^*$ has the same recurrent classes and steady states, all of them aperiodic, costs scaled by $\tau$; value iteration on $\Delta^*$ produces a solution $(J^*/\tau, r^*)$ of the ACOE of $\Delta$.

Significance

The ACOE with constant $J$ is the standard certificate of optimality for finite average cost models, and Proposition 6.5.1 is what allows any numerical solution of it to be trusted. Proposition 6.6.3 is the correctness theorem of the value iteration algorithm (VIA 6.6.4 of the book), and Proposition 6.6.6 removes its one extra hypothesis at the price of a model transformation. Chapter 8 of the book runs this algorithm on a sequence of finite truncations to compute optimal policies for countable-state queueing models, so these results are the base of the book's computational method.

All results in this mission are proved in the book; none has a machine-checked proof. Existing formalizations on the platform treat average reward models under a unichain hypothesis with a single action set type; this mission assumes only a constant minimum average cost (multichain models allowed) and uses the general policy class throughout.

Difficulty

The ACOE itself is not the obstacle; convergence of $v_n(x) - v_{n-1}(x)$ is. Theorem 6.4.2 bounds $d_n$ but does not make it converge, and Example 6.6.1 of the book (a two-state periodic chain) shows that without aperiodicity $v_n(x) - v_{n-1}(x)$ oscillates. The naive argument, passing to the limit in the finite horizon optimality equation, assumes the limits exist, which is exactly what is in question. Chain structure is the obstruction: a multichain optimal policy has several recurrent classes, and the Cesàro-type convergence that suffices for the ACOE itself is weaker than the pointwise convergence value iteration needs. The policy statement is also delicate, since the finite horizon minimizers $f_n$ need not converge.

Formalization scope

• The state type S is finite ([Fintype S]); actions are a type Act with per-state nonempty Finset action sets. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞, and all value functions are defined in [0,∞] as infima over all history-dependent randomized policies, then converted to ℝ (they are finite for finite $S$).
• $J$ constant is stated as $J(i) = J$ for all $i$, with $J \in \mathbb R_{\ge 0}$. The relative value $h$ is defined as the limit $\alpha \to 1^-$ of $h_\alpha$, not taken as an arbitrary solution of the ACOE; Theorem 6.4.2(i) asserts the limit exists. The Blackwell optimal policy $f$ enters as a hypothesis: any stationary policy discount optimal on an interval $(\alpha_0,1)$.
• min_a is Finset.inf' over $A_i$. Limit points of policy sequences follow Definition B.1 (a subsequence agreeing eventually in every state). Finite horizon optimal policies $f_n$ are any minimizers of $v_n(i) = \min_a\{C(i,a) + \sum_j P_{ij}(a) v_{n-1}(j)\}$.
• Aperiodicity of a class is the book's definition ($P^{(n)}_{ij} \to \pi_j$ on the class), with $\pi_j = 1/m_{jj}$. Assumption OPA quantifies over average cost optimal stationary policies only, not over all stationary policies.
• A trivializing formalization is ruled out: $h$, $r_n$, $d_n$ and $v_n$ are computed from the model, not free functions constrained by the ACOE, and the ACOE conclusions are equalities of real numbers with the minimum over the actual action sets.
• The model, criteria and Markov chain definitions restate those of mission IV of this series in their own namespace; they are reusable for any finite average cost result. Contributions of general Markov chain facts (convergence of $P^{(n)}$ on aperiodic classes, Cesàro limits $\frac1n\sum_t P^{(t)}$) are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, Wiley, 1999. https://doi.org/10.1002/9780470317037
• D. Blackwell, Discrete dynamic programming, Annals of Mathematical Statistics 33 (1962), 719–726. https://doi.org/10.1214/aoms/1177704593
• P. J. Schweitzer and A. Federgruen, The asymptotic behavior of undiscounted value iteration in Markov decision problems, Mathematics of Operations Research 2 (1977), 360–381. https://doi.org/10.1287/moor.2.4.360
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887