Markov Chain

Why average cost on finite state spaces

Controlled queues, inventories and communication links are run for a long time, and the quantity an operator usually cares about is the long-run average cost per period rather than a discounted total. The average cost criterion is harder to work with than the discounted one: its value is a $\limsup$ of Cesàro means, it is not given by a contraction, and for general (history dependent, randomized) policies the limit need not exist. Chapter 6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) treats the case of a finite state space, where the strongest results hold: an average cost optimal policy exists, can be taken stationary, and can be obtained as a limit of discount optimal policies as the discount factor tends to one.

The results go back to D. Blackwell, "Discrete dynamic programming", Ann. Math. Statist. 33 (1962), who showed that for finite states and actions some stationary policy is discount optimal for all discount factors close to one. Such a policy is now called Blackwell optimal. Sennott's Chapter 6 derives average cost optimality of this policy and the multichain average cost optimality equation from it, in the notation used throughout the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$, a finite nonempty action set $A_i$ in each state $i$, nonnegative finite costs $C(i,a)$, and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a) = 1$. A policy $\theta$ chooses the action at time $t$ from a distribution $\theta(\cdot \mid h_t)$ on $A_{i_t}$ that may depend on the whole history $h_t = (i_0,a_0,\ldots,i_t)$. A stationary policy $f$ always chooses a fixed action $f(i) \in A_i$ in state $i$.

With $X_t, A_t$ the state and action at time $t$ and $X_0 = i$, define

• the discounted cost $V_{\theta,\alpha}(i) = \sum_{t \ge 0} \alpha^t E_\theta[C(X_t,A_t)]$ for $0<\alpha<1$, and the discounted value function $V_\alpha(i) = \inf_\theta V_{\theta,\alpha}(i)$;
• the $n$ horizon cost $v_{\theta,n}(i) = \sum_{t=0}^{n-1} E_\theta[C(X_t,A_t)]$;
• the average cost $J_\theta(i) = \limsup_n v_{\theta,n}(i)/n$, its $\liminf$ version $J^*_\theta(i)$, and the minimum average cost $J(i) = \inf_\theta J_\theta(i)$.

All infima range over all general policies, and every quantity may equal $+\infty$. A policy is $\alpha$ discount optimal if $V_{\theta,\alpha} = V_\alpha$, and average cost optimal if $J_\theta = J$.

For a stationary policy $f$ on a finite state space, the induced Markov chain splits into positive recurrent classes $R_1,\ldots,R_K$ and transient states. With $p_k(i)$ the probability of reaching $R_k$ from $i$, distinguished states $z_k \in R_k$, and $W_\alpha(i) = \sum_k p_k(i) V_\alpha(z_k)$, the relative value function is $w_\alpha(i) = V_\alpha(i) - W_\alpha(i)$.

Formalization targets

Goal: Proposition 6.2.3

For an MDC with a finite state space there are $\alpha_0 \in (0,1)$ and one stationary policy $f$ such that $f$ is $\alpha$ discount optimal for every $\alpha \in (\alpha_0,1)$, $f$ is average cost optimal, and

$$J(i) = \lim_{\alpha\to 1^-} (1-\alpha) V_\alpha(i) = \lim_{n\to\infty} \frac{v_{f,n}(i)}{n}, \qquad i \in S.$$

Milestones

1. Proposition 4.5.3. For finite $S$ and stationary $e$, $\alpha \mapsto V_{e,\alpha}(i)$ is a finite, continuous, rational function on $(0,1)$.
2. Proposition 6.1.1. For every policy on a countable state space,

$$J^*_\theta(i) \le \liminf_{\alpha\to1^-}(1-\alpha)V_{\theta,\alpha}(i) \le \limsup_{\alpha\to1^-}(1-\alpha)V_{\theta,\alpha}(i) \le J_\theta(i),$$

with three equivalent conditions for equality. 3. Proposition 6.2.2. For finite $S$ and stationary $e$, $J_e(i) = \lim_{\alpha\to1^-}(1-\alpha)V_{e,\alpha}(i) = \lim_n v_{e,n}(i)/n$. 4. Proposition 4.5.1, Proposition 4.5.4, Corollary 4.5.5. The power series structure of $V_{\theta,\alpha}$ in $\alpha$; monotonicity and left continuity of $V_\alpha$; continuity under bounded costs. 5. Theorem 6.3.1. For the policy $f$ of the goal, $\lim_{\alpha \to 1^-} w_\alpha(i) = w(i)$ exists, and

$$J(i) + w(i) = C(i,f) + \sum_j P_{ij}(f) w(j) \ \ge\ \min_{a} \Big\{C(i,a) + \sum_j P_{ij}(a) w(j)\Big\},$$

together with the limit identities (i)–(iii) and the optimality criterion (v). 6. Proposition 6.3.3. $V_\alpha(i) = J(i)/(1-\alpha) + w^*(i) + \varepsilon_\alpha(i)$ with $\varepsilon_\alpha(i) \to 0$ as $\alpha \to 1^-$.

Significance

The goal says that on a finite state space nothing is gained by randomizing or by remembering the past when minimizing average cost, and that the minimum average cost is the vanishing-discount limit of the discounted value function. This justifies computing average cost optimal policies through discounted problems and value iteration, the route taken in the rest of Chapter 6 and, via approximating sequences, for countable state spaces in Chapters 7 and 8. Theorem 6.3.1 supplies an optimality equation without any unichain or communication assumption. The book's Example 6.3.2 shows that the inequality in that equation can be strict, and that a stationary policy attaining the minimum need not be optimal.

The results are classical and proved in the book. No machine-checked version of them is known to exist. The platform has average-reward results for unichain finite MDPs with Markov policies (the Puterman series) and an average-cost optimality equation under recurrence assumptions (the Bertsekas series). Neither covers existence of a Blackwell optimal policy against the class of all history dependent randomized policies, or the multichain equation. A formal development also yields reusable infrastructure: the law of a controlled process under a general policy, first passage quantities of finite chains, and the Abelian inequality between Abel and Cesàro means of a nonnegative sequence.

Difficulty

The obvious argument picks, for each $\alpha$, a stationary discount optimal policy $f_\alpha$ and lets $\alpha \to 1$. Finiteness of the set of stationary policies gives one policy that is optimal along some sequence $\alpha_n \to 1$, but not on an interval. Excluding infinite switching between two policies requires the analytic structure of $\alpha \mapsto V_{f,\alpha}(i)$ (Proposition 4.5.3), which in turn rests on matrix inversion of $I - \alpha P$. Passing from the discounted criterion to the average one requires an Abelian inequality for nonnegative series whose terms may be infinite (Proposition 6.1.1), and comparison against general policies rules out any argument that works only within stationary or Markov policies. For Theorem 6.3.1 the difficulty is the multichain structure: the relative value function has to be assembled class by class from first passage times and costs, and its limit must be identified.

Formalization scope

• States form a type S; [Countable S] for Section 4.5 and Proposition 6.1.1, [Fintype S] from Section 6.2 on, as in the book. Actions form a type Act with A i : Finset Act nonempty. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞.
• A general policy is a function of the list of past state-action pairs (most recent first) and the current state, giving a distribution on A i. Stationary policies embed as degenerate policies. The law of the process is built from this data, and every infimum ranges over all general policies.
• $V_{\theta,\alpha}$, $V_\alpha$, $v_{\theta,n}$, $J_\theta$, $J^*_\theta$, $J$ are in ℝ≥0∞, so $+\infty$ is represented. $\alpha \to 1^-$ is the filter 𝓝[<] 1. On a finite state space these quantities are finite. The real valued objects of Section 6.3 ($w_\alpha$, $w$, $w^*$, equation (6.6)) are therefore formed with toReal, and this switch from ℝ≥0∞ to ℝ happens only in Theorem 6.3.1 and Proposition 6.3.3.
• The objects of Section 6.3 ($p_k$, $m_{i|k}$, $c_{i|k}$, $\pi_s$, $W_\alpha$) are defined from $f$. The distinguished states are a hypothesis quantified over.
• A trivializing formalization would take the infimum over stationary policies only, let the optimal policy depend on $\alpha$, or state rationality as an equation p/q without requiring $q \ne 0$. Each is excluded here: $J$ and $V_\alpha$ are infima over all general policies, one pair $(\alpha_0,f)$ is quantified before all $\alpha$, and the denominator is required to be nonzero on $(0,1)$.

Useful infrastructure includes rational functions of one real variable and their finitely many sign changes, the resolvent $(I-\alpha P)^{-1}$ of a stochastic matrix, the Abelian inequality for $[0,\infty]$-valued sequences, and renewal-reward identities for finite chains. Contributions of general lemmas on these topics are welcome, as are proofs of individual milestones.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, 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
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Many operational systems move between a finite number of states at random times: a machine alternates between working and repair, a queue between occupancy levels, an inventory between stock positions. When the time spent in a state is not exponential and not a fixed period, neither discrete-time Markov decision processes nor continuous-time Markov chains describe the system faithfully. William S. Jewell's 1963 paper Markov-Renewal Programming. I extends Howard's Markov decision processes to Markov-renewal processes (also called semi-Markov processes), in which the time between transitions is a random variable whose law depends on the current state, the next state, and the decision taken. The resulting model, now called a semi-Markov decision process, is standard in maintenance, queueing control and reliability.

Timeline:

• 1954: Lévy, Smith and Takács independently introduce Markov-renewal and semi-Markov processes; Pyke later surveys them.
• 1960: Howard, Dynamic Programming and Markov Processes, introduces policy iteration for finite discrete-time Markov decision processes.
• 1962: Blackwell, Discrete Dynamic Programming, shows that for the discounted discrete-time problem a stationary policy is optimal among all policies.
• 1963: Jewell formulates Markov-renewal programming, with a continuous discount factor α, and carries Howard's algorithm and Blackwell's stationarity result over to it. Part II of the paper treats the undiscounted (infinite-return) models.

Setting

A Markov-renewal program has a finite set of states $S$ (the paper's $i = 1, \dots, N$) and a finite, nonempty set of alternatives (the paper's $z = 1, \dots, Z$), each available in every state. For each alternative $z$ and states $i, j$ it specifies:

• a transition probability $p^z_{ij} \ge 0$, with $\sum_j p^z_{ij} = 1$;
• a sojourn-time distribution $F^z_{ij}$, the law of the time $\tau$ between entering $i$ and moving to $j$, with $\tau \ge 0$ and $F^z_{ij}(0) = 0$;
• for each continuous discount factor $\alpha > 0$, a real number $\rho^z_{ij}(\alpha)$, the expected discounted return earned during that transition.

The Laplace–Stieltjes transform $\tilde f^z_{ij}(s) = \int_0^\infty e^{-st}\,dF^z_{ij}(t)$ is the expected discount $\mathbb E[e^{-s\tau}]$ over one interval. The average one-step return is $\rho^z_i(\alpha) = \sum_j p^z_{ij}\rho^z_{ij}(\alpha)$, and for a vector of returns $v$ the test quantity is

$$\rho^z_i(\alpha) + \sum_j p^z_{ij}\,\tilde f^z_{ij}(\alpha)\,v_j .$$

A stationary policy is a map $d : S \to A$; a nonstationary policy is a sequence $\pi = (\pi_0, \pi_1, \dots)$ of such maps, $\pi_k$ being used at the $k$-th transition. The $n$-step return $V^\pi_i(n)$ of a policy, with boundary rewards $V_i(0,\alpha)$, is the test quantity of $\pi_0(i)$ applied to the $(n-1)$-step return of the shifted policy; the optimal $n$-step return $V_i(n,\alpha)$ of equation (6) replaces $\pi_0(i)$ by a maximum over $z$. The value-determination equations (15) of a stationary policy $d$ are $v_i = \rho^{d(i)}_i(\alpha) + \sum_j p^{d(i)}_{ij}\tilde f^{d(i)}_{ij}(\alpha) v_j$.

The algorithm of Fig. 1 alternates two steps: solve (15) for the current policy, then in every state pick an alternative maximizing the test quantity, keeping the old alternative if it still attains the maximum. It stops when two successive policies are identical.

Formalization targets

Goal (p. 947)

For every $\alpha > 0$: (15) has a unique solution for every stationary policy, and every run $(d_k, v_k)$ of Fig. 1 reaches $d_{K+1} = d_K$ with $K < Z^N$, where

$$\lim_{n\to\infty} V^{d_K}_i(n) = (v_K)_i,\qquad \lim_{n\to\infty} V^\pi_i(n) \le (v_K)_i \ \ \forall \pi,\qquad \lim_{n\to\infty} V_i(n,\alpha) = (v_K)_i ,$$

for every state $i$ and all boundary rewards, every limit existing. This is the paper's "the algorithm of Fig. 1 produces an optimal, stationary policy that is as good as any optimal, nonstationary policy".

Milestones

1. p. 945: $0 \le p^z_{ij}\tilde f^z_{ij}(s) < 1$ for $s > 0$.
2. Claim (a): (15) has exactly one solution for each stationary policy.
3. Eq. (15): the $n$-step return of a stationary policy converges to a solution of (15).
4. p. 946: $I - \tilde q(\alpha)$ is invertible and $([I-\tilde q(\alpha)]^{-1})_{ii} \ge 1$.
5. Claim (b): a change of policy raises the return of some state and lowers none.
6. Claim (c): a policy reproduced by the improvement step is optimal among stationary policies.
7. Claim (d): a run of Fig. 1 terminates within $Z^N$ cycles.
8. Eq. (14): $V_i(n,\alpha)$ converges, independently of the boundary rewards, to a solution of $v_i = \max_z\{\rho^z_i(\alpha) + \sum_j p^z_{ij}\tilde f^z_{ij}(\alpha) v_j\}$.
9. p. 946: some stationary policy's return dominates the limiting return of every nonstationary policy.

Significance

The result says that the infinite-step discounted Markov-renewal program is solved exactly, in finitely many cycles, by a finite-dimensional algorithm, and that the answer is a stationary policy. As the paper notes, this matters operationally because a nonstationary policy is hard to follow. The sojourn distributions enter only through the numbers $\tilde f^z_{ij}(\alpha)$, so the same algorithm serves any sojourn-time law. For fixed $\alpha$ the model is a discounted Markov decision process whose discount factor depends on the transition, which contains Howard's and Blackwell's constant-discount problem as the case of intervals of fixed length (p. 943).

The results are classical and proved in the literature. The paper itself refers the proofs to Howard and Blackwell. Machine-checked versions exist on this platform for finite stochastic shortest path and constant-discount problems (Bertsekas, Dynamic Programming and Optimal Control, Prop. 7.2.2 and 7.3.1, mission Dynamic Programming and Optimal Control VII). No formal treatment of Markov-renewal programs, of transition-dependent discounting, or of the retention rule of Fig. 1 is known to exist. The mission produces a verified policy-iteration theorem for semi-Markov decision processes, with an explicit termination bound and the comparison against nonstationary policies.

Difficulty

The discount over one transition, $\tilde f^z_{ij}(\alpha)$, varies with $i$, $j$ and $z$, so the problem is not a constant-$\gamma$ contraction of textbook form; the relevant bound is that every row of $\tilde q(\alpha)$ sums to less than one, which rests on $F^z_{ij}(0) = 0$. Entries in $[0, 1)$ alone, the paper's stated justification of Claim (a), do not make $I - \tilde q(\alpha)$ invertible: the $2 \times 2$ matrix with every entry $1/2$ has entries in $[0,1)$, yet $I$ minus it is singular.

Finite termination is not automatic either. If the improvement step may switch between tied maximizers, the iterates can cycle forever between two policies with equal returns; the retention rule of Fig. 1 excludes this, and Claim (b) must deliver a strict increase in some state, with no decrease anywhere, to rule out revisiting a policy. Comparing with nonstationary policies requires controlling returns of arbitrary policy sequences, whose limits must be shown to exist, not assumed.

Formalization scope

• States and alternatives are finite types; alternatives are nonempty. Every alternative is available in every state.
• $F^z_{ij}$ is a probability measure on $\mathbb R$ with no mass on $(-\infty, 0]$. The transform is integrated over $(0, \infty)$, which carries all the mass.
• The one-transition returns $\rho^z_{ij}(\alpha)$ are arbitrary real numbers, a generalization of the paper's Stieltjes integral (4), which is not formalized. The reward functions $R^z_{ij}(t\mid\tau)$ do not appear.
• Returns of policies are defined by the one-step recursion (the policy form of (6)); the Markov-renewal process is not built as a stochastic process.
• Policies are the paper's: deterministic and Markov, nonstationary ones indexed by the number of transitions made. Randomized and history-dependent policies are not in the comparison class.
• The following informal words are read as follows. "Solve the set of simultaneous equations": (15) has exactly one solution. "Strictly increases the expected return of at least one state": no state's return decreases and one strictly increases, under the hypothesis that the policy changed. "No other policy can lead to higher expected returns" in Claim (c): no stationary policy. "Terminates in a finite number of cycles": two successive policies coincide at some cycle $K < Z^N$. "If there is no improvement in the test quantity, retain the same alternative": the old alternative is kept whenever it attains the maximum. "Optimal" and "as good as any nonstationary policy": the limiting return of the returned policy dominates that of every policy from every state, for all boundary rewards. "$\lim_{n\to\infty} V_i(n,\alpha)$": the limit is proved to exist. "$\max_z$": a maximum over the finite nonempty set of alternatives.
• Eq. (14) is printed with $v_i(\alpha)$ inside the sum over $j$; the formalization uses $v_j(\alpha)$, as (6), (15) and Fig. 1 do.
• Every statement fixes one $\alpha > 0$. The undiscounted models (16)–(19), the finite-time and mixed-horizon models (9)–(13), and the infinite-time case of the stationarity result are out of scope.
• The return of a policy is never defined through a matrix inverse, whose Mathlib value for a singular matrix is $0$; (15) is a predicate, and the goal asserts unique solvability, so a vacuous reading through junk inverses or assumed limits is excluded.

Reusable infrastructure: bounds for substochastic matrices with row sums below one (invertibility, Neumann series, nonnegative inverse), convergence of iterated Bellman operators with transition-dependent discount, and the policy-iteration termination argument with a tie-breaking rule. Proofs of any milestone and alternative arguments are welcome.

Selected references

• W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6), 938–948, 1963. https://doi.org/10.1287/opre.11.6.938
• W. S. Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Operations Research 11(6), 949–971, 1963. https://doi.org/10.1287/opre.11.6.949
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2), 719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• R. Pyke, Markov Renewal Processes: Definitions and Preliminary Properties, Annals of Mathematical Statistics 32(4), 1231–1242, 1961. https://doi.org/10.1214/aoms/1177704863
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Section 7.2–7.3.

Motivation

A Markov decision process (MDP) is evaluated with a transition kernel that, in practice, is estimated from data. The expected total reward of a policy can be very sensitive to small errors in that estimate (Mannor, Simester, Sun and Tsitsiklis, 2007). Robust MDPs address this by letting the kernel range over an ambiguity set and optimizing the worst-case expected reward. Iyengar (2005) and Nilim and El Ghaoui (2005) showed that when the ambiguity set is (s, a)-rectangular (the transition law of each state–action pair varies independently of all others), the robust problem is solved by a robust Bellman recursion and a deterministic stationary policy is optimal.

Wiesemann, Kuhn and Rustem (Robust Markov Decision Processes, Mathematics of Operations Research 38(1), 2013) widen this to s-rectangular ambiguity sets, in which the transition laws of different actions in the same state may be coupled. Their Theorem 4.1 shows that robust policy improvement over such sets is still solved by a robust Bellman fixed point, but the optimal stationary policy may need to randomize. This mission formalizes that theorem and the chain of results its proof uses.

Timeline:

• 2005: Iyengar; Nilim and El Ghaoui — robust dynamic programming over (s, a)-rectangular sets, deterministic stationary optimal policies.
• 2010–2013: Wiesemann, Kuhn and Rustem — s-rectangular sets with affinely parametrized kernels; robust value iteration for evaluation (Theorem 3.2) and improvement (Theorem 4.1); randomization needed in general.

Setting

States form a finite set $\mathcal S$, actions a finite set $\mathcal A$. Choosing action $a$ in state $s$ and moving to $s'$ pays a reward $r(s,a,s')\ge 0$; rewards are discounted by $\lambda\in(0,1)$ and the initial state has a known law $p_0$ in the probability simplex $\mathcal M(\mathcal S)$.

The uncertain parameter $\xi$ lies in

$$\Xi=\{\xi\in\mathbb R^q:\ \xi^\top O_l\xi+o_l^\top\xi+\omega_l\ge 0,\ l=1,\dots,L\},$$

with $O_l$ symmetric negative semidefinite, $\Xi$ bounded and containing a Slater point. Transition probabilities are affine in the parameter, $p^\xi(\cdot\mid s,a)=k_{sa}+K_{sa}\xi\in\mathcal M(\mathcal S)$ for $\xi\in\Xi$. The ambiguity set $\mathcal P$ is the set of kernels $(p^\xi(\cdot\mid s,a))_{s,a}$, $\xi\in\Xi$. It is s-rectangular if $\mathcal P=\times_{s}\mathcal P_s$, where $\mathcal P_s$ collects the blocks $(P_{s1},\dots,P_{sA})$ of members of $\mathcal P$: the parameter may be chosen separately in each state.

A stationary randomized policy $\pi\in\Pi$ assigns to each state a distribution $\pi(\cdot\mid s)$ over actions. It induces the Markov reward process

$$\widehat P_{ss'}(\pi;\xi)=\sum_a\pi(a\mid s)p^\xi(s'\mid s,a),\qquad \widehat r_s(\pi;\xi)=\sum_a\pi(a\mid s)\sum_{s'}p^\xi(s'\mid s,a)r(s,a,s'),$$

and the reward to-go $v(\pi;\xi)=\sum_{t\ge0}[\lambda\widehat P(\pi;\xi)]^t\widehat r(\pi;\xi)$. The worst-case expected total reward of $\pi$ is $\inf_{\xi\in\Xi}p_0^\top v(\pi;\xi)$.

Two robust Bellman maps on $\mathbb R^S$ carry the results:

$$\phi_s(\pi;w)=\min_{\xi\in\Xi}\Big\{\widehat r_s(\pi;\xi)+\lambda\sum_{s'}\widehat P_{ss'}(\pi;\xi)w_{s'}\Big\},\qquad \varphi_s(w)=\max_{\pi\in\Pi}\phi_s(\pi;w).$$

In Lean these are phiEval and phiImprove, in the namespace WiesemannRMDP.SRect.

Formalization targets

Goal: Theorem 4.1 (robust policy improvement)

For an s-rectangular $\mathcal P$, $\varphi$ has a unique fixed point $w^*$, per-state maximizers $\pi^s\in\arg\max_{\pi\in\Pi}\phi_s(\pi;w^*)$ exist, and the glued policy $\pi^*(a\mid s)=\pi^s(a\mid s)$ together with the constant function $\vartheta^*\equiv w^*$ attains

$$\sup_{\pi\in\Pi}\ \sup_{\vartheta:\Xi\overset{c}{\to}\mathbb R^S}\Big\{\inf_{\xi\in\Xi}p_0^\top\vartheta(\xi):\ \vartheta(\xi)\le\widehat r(\pi;\xi)+\lambda\widehat P(\pi;\xi)\vartheta(\xi)\ \forall\xi\in\Xi\Big\}=p_0^\top w^*.$$

Milestones

1. Proposition 3.1 (b), (c), (a): $v(\pi;\xi)$ is the unique solution of $w=\widehat r+\lambda\widehat Pw$; every sub-solution lies below it; $v$ is Lipschitz on $\Pi\times\Xi$.
2. Reformulation (10): for fixed $\pi$, $\inf_\xi p_0^\top v(\pi;\xi)$ equals the inner supremum above, over all and over continuous $\vartheta$.
3. $\phi(\pi;\cdot)$ is a contraction (proof of Theorem 3.2).
4. Theorem 3.2: for s-rectangular $\mathcal P$ and fixed $\pi$, the constant fixed point of $\phi(\pi;\cdot)$ solves the evaluation problem (10).
5. From the proof of Theorem 4.1: the glued policy satisfies $w^*=\phi(\pi^*;w^*)$, and $\varphi$ is a contraction.

Significance

Theorem 4.1 reduces robust policy improvement over s-rectangular sets to computing the fixed point of one map on $\mathbb R^S$, each evaluation of which is a finite convex program; the paper derives a polynomial-time method from it (Corollary 4.2). It also shows that the optimal policy is stationary but generally randomized, which separates s-rectangular from (s, a)-rectangular robust MDPs. Theorem 3.2 is the evaluation counterpart and is used again when the paper compares s-rectangular and general ambiguity sets (Proposition 3.10).

The results are proved in the paper; none is formalized. On the platform, the (s, a)-rectangular analogue with deterministic policies and costs (Nilim and El Ghaoui) and a related robust linear-programming characterization in another model (Derman, Geist and Mannor) exist, but neither covers coupled actions, randomized policies or rewards depending on the next state. A complete development would give machine-checked robust value iteration for s-rectangular sets and reusable facts on the reward to-go of a finite Markov reward process.

Difficulty

The obvious argument copies the nominal proof: the optimum of the constant-$\vartheta$ restriction is the fixed point $w^*$, so the constant function is optimal. That only solves the restriction to constant $\vartheta$; the problems optimize over all continuous reward to-go functions $\vartheta:\Xi\to\mathbb R^S$, and showing that no non-constant $\vartheta$ does better is where s-rectangularity enters. Without it the claim is false: the paper's Example 3.11 gives a non-rectangular set where the constant bound is strictly below the worst-case reward. A second subtlety is that $\phi_s(\pi;w)$ depends on $\pi$ only through the row $\pi(\cdot\mid s)$, which is what lets per-state maximizers be assembled into a single policy; the maximizers are in general not deterministic.

Formalization scope

States and actions are finite nonempty types; policies are functions $\pi(a\mid s)$ satisfying the published IsPolicy, and the simplex condition on $p^\xi(\cdot\mid s,a)$ is the published IsTransitionKernel. $\widehat P$ and $\widehat r$ are built from the published InducedTransition and InducedReward. The model is a structure Model with the standing assumptions in Model.Standing. The reward to-go is defined by the series $\sum_t[\lambda\widehat P]^t\widehat r$, not as the solution of the evaluation equation, so Proposition 3.1 (b) is not definitional. The minimum over $\Xi$ and the maximum over $\Pi$ are infima and suprema over subtypes, attained under the standing assumptions; the objective $\inf_\xi p_0^\top\vartheta(\xi)$ is used only for $\vartheta$ continuous on $\Xi$, and where arbitrary $\vartheta$ appear (the middle line of (10)) the infimum is taken in the extended reals. Inequalities on $\mathbb R^S$ are componentwise; contractions are with respect to the sup norm. The paper's $\omega$ in (3b) carries the index $l$, as elsewhere in the paper.

A statement that compares the fixed point only with constant reward to-go functions, or that takes $w^*$ and $\pi^*$ as hypotheses satisfying the conclusion, is not Theorem 4.1; the goal asserts existence and uniqueness of $w^*$, existence of the maximizers, and optimality against every policy and every continuous feasible $\vartheta$.

Useful infrastructure: Neumann series for $\lambda$ times a row-stochastic matrix, continuity of infima over compact parameter sets, and contraction properties of min/max Bellman operators. Proofs of the milestones, and of nonvacuity of richer instances, are welcome.

Selected references

• W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov Decision Processes, Mathematics of Operations Research 38(1):153–183, 2013. https://doi.org/10.1287/moor.1120.0566 (formalized from the Optimization Online revision of February 9, 2012: https://optimization-online.org/wp-content/uploads/2010/05/2610.pdf)
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• S. Mannor, D. Simester, P. Sun, J. N. Tsitsiklis, Bias and Variance Approximation in Value Function Estimates, Management Science 53(2):308–322, 2007. https://doi.org/10.1287/mnsc.1060.0614
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

A production process deteriorates over time, and the state it is in cannot be observed directly. Each period the operator chooses among three actions: produce without looking, produce and inspect the item (which reveals the current state at a cost), or revise the process back to its good state. This is one of the earliest partially observed Markov decision problems with a costly observation action, and it is the prototype of the inspection and machine-replacement models that followed in operations research and maintenance theory. Ross (Management Science 17(9), 1971) set it up for a countable state space, reduced it to a fully observed problem on beliefs, and determined the structure of an optimal policy for two states.

Intuition suggests a three-region policy for two states: produce while the probability of the bad state is small, inspect at intermediate probabilities, revise when it is large. Ross showed that the true structure has up to four regions: produce, inspect, produce again, revise. This mission formalizes that structure theorem and the general results it rests on.

Setting

The underlying process has a countable set of states $0,1,2,\dots$, with transition probabilities $P_{ij}$ from state $i$ at the end of a period to state $j$ at the beginning of the next. In state $i$, producing without inspection costs $C_i$, producing with inspection costs $I_i$, and revising costs $R_i$; costs are bounded, and future costs are discounted by $\beta\in(0,1)$. A revision puts the process in state $0$.

The decision maker tracks a belief $P=(P_0,P_1,\dots)$, a probability vector on the states, ranging over

$$S=\Big\{P: P_i\ge0,\ \sum_iP_i=1\Big\}.$$

Producing without inspection moves the belief to $TP$, with $(TP)_i=\sum_jP_jP_{ji}$. Inspecting reveals the state; if it is $i$, the next belief is the row $e^i=(P_{i0},P_{i1},\dots)$. Revising leads to $e^0$.

The $\beta$-discounted optimal cost $V_\beta$ is the limit of value iteration: $V^0=0$ and

$$V^{n+1}(P)=\min\Big\{\sum_iP_iC_i+\beta V^n(TP);\ \sum_iP_iI_i+\beta\sum_iP_iV^n(e^i);\ \sum_iP_iR_i+\beta V^n(e^0)\Big\}.$$

The three terms with $V^n$ replaced by $V_\beta$ form the right side of the optimality equation (1). The $\beta$-optimal produce, inspect and revise regions are the sets of beliefs at which the corresponding term equals $V_\beta(P)$, and a stationary rule is $\beta$-optimal when it always selects an action attaining the minimum.

In the two-state process of §3, state $0$ is good and state $1$ is bad: $P_{00}=1-\pi$, $P_{11}=1$, $C_0=0$, $C_1=C$, $I_0=I_1=I$, $R_0=R_1=R$, with $C<I<R$. The belief is a number $P\in[0,1]$, the probability of the bad state, $TP=P+\pi-\pi P$, and the optimality equation becomes

$$V_\beta(P)=\min\{CP+\beta V_\beta(TP);\ I+\beta PV_\beta(1)+\beta(1-P)V_\beta(\pi);\ R+\beta V_\beta(\pi)\}.\tag{3}$$

Formalization targets

Goal: Theorem 3.3, the four-region structure

There are thresholds $\pi\le P_1\le P_2\le P_3$ with $P_2\le1$ such that the rule

$$\text{produce on }[0,P_1),\quad\text{inspect on }[P_1,P_2),\quad\text{produce on }[P_2,P_3),\quad\text{revise on }[P_3,1]$$

is $\beta$-optimal, and $P_3\le1$ whenever revising is $\beta$-optimal at some belief. Degenerate thresholds (empty intervals) are allowed, so the statement fixes only the order of the regions, not their number.

Milestones

1. (1): value iteration converges on $S$, $V_\beta$ is bounded, solves (1), and is its unique bounded solution.
2. Lemma 2.1: $V_\beta$ is concave on $S$.
3. Theorem 2.2: the $\beta$-optimal inspect and revise regions are convex.
4. (3): the two-state optimality equation, as an instance of (1).
5. Lemma 3.1: in the two-state model $V_\beta$ is nondecreasing on $[0,1]$.
6. Lemma 3.2: for $0\le P\le\pi$, producing is strictly better than inspecting and than revising.

Significance

Theorem 3.3 reduces the search for an optimal policy in the two-state problem to the choice of three numbers, and it fixes the order of the regions: there is never a revise region below an inspect region, and inspection never occurs below the deterioration probability $\pi$. Together with Theorems 3.4 and 3.7 of the same paper (separate missions in this series), it is the basis for computing optimal inspection policies by searching over thresholds. Theorem 2.2 holds for any countable state space and is the general form of the observation that, in partially observed problems with linear-in-belief action costs, the regions of the "information" and "reset" actions are convex while the region of the passive action need not be.

The results are proved in the paper. As far as a search of the Prove2Me library shows (October 2026), none of them is formalized. Related formal work treats other models: belief-state reductions of finite POMDPs, and abstract contraction models for discounted dynamic programming. The mission produces machine-checked versions of the general model's optimality equation, the concavity of its value function, the convexity of two of its regions, and the two-state structure theorem.

Difficulty

The paper's proofs are short and lean on facts quoted from the literature. Theorem 3.3's proof is two sentences long. Filling it in requires several facts that the paper leaves implicit. The revise region of the two-state model is a closed right-hand interval. The inspect region meets $[0,1]$ in an interval, through the affine embedding $P\mapsto(1-P,P)$ of $[0,1]$ into $S$. The half-open endpoints of the rule select optimal actions. That last point needs continuity of $V_\beta$ inside $(0,1)$, a consequence of concavity, and Lemma 3.2 at the left end. The naive reading of the printed theorem, with all three thresholds in $[0,1]$, is false in general (see below), so the threshold bookkeeping cannot be skipped.

On the general side, the optimality equation (1) is quoted from Blackwell. Here it must be proved for value iteration on the belief simplex of a countable state space, where the inspect term is an infinite series of values at the rows $e^i$. Its convergence and the contraction estimates use the boundedness of the costs.

Formalization scope

The general model is a structure over a type ι with [Countable ι], a distinguished state i₀, a transition matrix Pm, costs C I R : ι → ℝ and β. A separate predicate Model.Valid requires nonnegative entries, rows with HasSum (Pm i) 1, bounded costs and 0 < β < 1. The simplex uses HasSum P 1, never tsum, so it consists of genuine probability vectors. $V_\beta$ is defined as limUnder atTop of value iteration from $V^0=0$, which is the paper's own characterization in the proof of Lemma 2.1. It is not an arbitrary function assumed to satisfy (1). The paper's definition as an infimum over measurable policies is not formalized; the policy class would be a separate mission. Regions are subsets of $S$.

The two-state model is the instance ι = Fin 2 with $P_{00}=1-\pi$, $P_{01}=\pi$, $P_{10}=0$, $P_{11}=1$, and its value at the scalar belief $P$ is the general $V_\beta$ at $(1-P,P)$. The general Lemma 2.1 and Theorem 2.2 therefore apply to it without restatement. Standing hypotheses of §3 are $0<\beta<1$, $0\le\pi\le1$ and $0<C<I<R$. $0<C$ is implicit in the paper, where the good state costs $0$ and the bad state $C$. "$\beta$-optimal rule" means a rule selecting a minimizer of the right side of (3) at every $P\in[0,1]$, the criterion the paper quotes on p. 588. "Every $\beta$-optimal policy produces" (Lemma 3.2) means that producing is the unique minimizer.

Threshold repair. The paper prints $\pi\le P_1\le P_2\le P_3\le1$. This is false when revising is never optimal, for instance when $R>C/(1-\beta(1-\pi))$: then always producing is optimal and revising at $P=1$ is strictly worse, so no rule revising on a nonempty $[P_3,1]$ is optimal. The goal keeps $P_3\le1$ exactly when the $\beta$-optimal revise region is nonempty and otherwise allows $P_3>1$; the rest of the printed chain, $\pi\le P_1\le P_2\le1$, is kept. Adding the hypothesis $R<C/(1-\beta(1-\pi))$ instead would drop a case the paper covers.

The statement admits no trivializing reading. The thresholds are quantified existentially, but the rule must be optimal at every belief in $[0,1]$, $V_\beta$ is pinned down by its definition, and the paper's numbers ($C=4$, $\pi=0.1$, $I=6$, $R=10$, $\beta=0.9$) satisfy all hypotheses.

Infrastructure needed: tsum manipulations on the belief simplex (linearity of $T$, summability of $\sum_iP_iV(e^i)$ for bounded $V$), a sup-norm contraction argument for value iteration, and closure of concavity under minima and pointwise limits. The value-iteration and contraction lemmas are reusable for any discounted model with bounded costs. Contributions of intermediate lemmas, such as continuity of the two-state $V_\beta$ on $(0,1]$ or the bridge identities $T(1-P,P)=(1-TP,TP)$, are welcome.

Selected references

• S. M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9):587–596, 1971. https://doi.org/10.1287/mnsc.17.9.587
• D. Blackwell, Discounted Dynamic Programming, Annals of Mathematical Statistics 36(1):226–235, 1965. https://doi.org/10.1214/aoms/1177700285
• K. J. Åström, Optimal Control of Markov Processes with Incomplete State Information, Journal of Mathematical Analysis and Applications 10(1):174–205, 1965. https://doi.org/10.1016/0022-247X(65)90154-X

Motivation

Temporal-difference (TD) methods learn to predict an eventual outcome from the differences between successive predictions rather than from the difference between each prediction and the final outcome. Sutton's 1988 paper Learning to predict by the methods of temporal differences introduced the TD($\lambda$) family and gave the first convergence proof for a TD method; before it, as the paper notes (p. 23), "no TD method has ever been proved stable or convergent to the correct predictions". TD learning is now the core of policy evaluation in reinforcement learning, and later analyses (Dayan 1992, Tsitsiklis and Van Roy 1997) start from the setting fixed here.

Timeline:

• 1960 — Widrow and Hoff introduce the LMS (Widrow–Hoff) rule; its predictions converge in expected value to the ideal predictions for small step sizes (Widrow and Stearns 1985).
• 1977 — Witten sketches a convergence proof for a TD-like procedure on discounted costs; many steps were left out, and Sutton (footnote 4) writes that it "now appears that the theorem he proposed is not true".
• 1988 — Sutton proves Theorem 2 (linear TD(0), expected-value convergence on absorbing chains) and Theorem 3 (convergence of batch linear TD(0) to the maximum-likelihood predictions).
• 1992–1997 — Dayan extends expected convergence to TD($\lambda$); Tsitsiklis and Van Roy prove almost-sure convergence of linear TD($\lambda$) under decreasing step sizes.

Setting

An absorbing Markov chain has a finite set $N$ of nonterminal states, a finite set $T$ of terminal states and transition probabilities $p_{ij}\ge0$ ($i\in N$, $j\in N\cup T$) with $\sum_{j\in N\cup T}p_{ij}=1$. Let $Q$ be the $N\times N$ matrix $[Q]_{ij}=p_{ij}$. "Absorbing" means that every sequence terminates with probability one; for a finite chain this is $Q^k\to0$.

A sequence starts in a nonterminal state drawn from a distribution $\mu$, follows the chain through nonterminal states $q_1,\dots,q_m$ until it enters a terminal state $q_{m+1}=j$, and then produces a scalar outcome $z$ drawn from a distribution $\nu_j$ with finite mean $\bar z_j$. Let $[h]_i=\sum_{j\in T}p_{ij}\bar z_j$. The ideal prediction of state $i$ is the expected outcome from $i$,

$$E\{z\mid i\}=\Bigl[\sum_{k\ge0}Q^kh\Bigr]_i=\bigl[(I-Q)^{-1}h\bigr]_i .$$

The learner does not see states, only an observation vector $x_i\in\mathbb R^K$ for each $i\in N$, and predicts linearly, $P_t=w^\top x_{q_t}$. Linear TD(0) with weight updates after each sequence keeps $w$ fixed during a sequence and then sets, with $P_{m+1}=z$,

$$w\leftarrow w+\sum_{t=1}^m\alpha\,(P_{t+1}-P_t)\,x_{q_t}.$$

Sequences are experienced independently; $w_n$ is the weight vector after $n$ sequences. Let $d_i$ be the expected number of visits to $i$ in one sequence, $D=\operatorname{diag}(d)$, and $X$ the matrix with columns $x_i$.

Formalization targets

Goal: Theorem 2

For every absorbing chain, start distribution $\mu$, outcome laws with finite means and linearly independent $\{x_i\}$, with every $d_i>0$, there is $\varepsilon>0$ such that for $0<\alpha<\varepsilon$ and every $w_0$,

$$\lim_{n\to\infty}E\{x_i^\top w_n\}=\bigl[(I-Q)^{-1}h\bigr]_i\qquad\forall i\in N .$$

The threshold $\varepsilon$ is existential, as in the paper; no explicit value is fixed.

Milestones on the goal's path

Theorem A.1 (Neumann series under $A^n\to0$); (5) the ideal predictions; (7) $d^\top=\mu^\top(I-Q)^{-1}$; the mean recursion $\bar w_{n+1}=\bar w_n+\alpha XD(h+QX^\top\bar w_n-X^\top\bar w_n)$; Theorem A.2 ($A^\top A$ nonsingular); Theorem A.3 ($A\succ0\iff A+A^\top\succ0$); the Lemma of p. 27; $D(I-Q)$ positive definite; the eigenvalues of $X^\top XD(I-Q)$ have positive real parts; and $(I-\alpha X^\top XD(I-Q))^n\to0$ for small $\alpha$.

Further results

Theorem 3: under repeated presentations of a finite training set, batch linear TD(0) converges (deterministically) to the maximum-likelihood predictions $[(I-\hat Q)^{-1}\hat h]_i$, with its two supporting steps ($\hat Q^n\to0$ and $\hat d^\top=\hat\mu^\top(I-\hat Q)^{-1}$). Theorem 1: linear TD(1) and Widrow–Hoff produce the same per-sequence weight changes.

Significance

Theorem 2 shows that a bootstrapping method, which learns from its own earlier predictions, is not biased by them in the limit: in expectation it reaches the same predictions as supervised (Widrow–Hoff) learning. Theorem 3 says more: on a fixed data set, TD(0) converges to the predictions that would be exact if the maximum-likelihood model of the process were correct, which differs from the least-squares answer Widrow–Hoff converges to. Together they are the formal basis for preferring TD to Monte-Carlo targets in multi-step prediction.

The results are proved on paper, and not formalized in Lean. A formalization adds a precise model of the experience (i.i.d. sequences of an absorbing chain with terminal-dependent outcome laws), the integrability facts the paper leaves implicit, and a correct proof of the positive definiteness of $D(I-Q)$, whose printed argument has a gap (see below). The matrix lemmas (Neumann series under $A^n\to0$; real-part positivity of eigenvalues of $GM$ for $G\succ0$ symmetric and $M$ positive definite in the non-symmetric sense; the step-size threshold) are reusable for other linear stochastic-approximation analyses.

Difficulty

The obvious argument writes $E\{w_{n+1}\}$ as a linear function of $E\{w_n\}$ and observes that the iteration matrix $I-\alpha X^\top XD(I-Q)$ is a contraction for small $\alpha$. Two steps of this fail as printed. First, the paper proves that $D(I-Q)$ is positive definite through the Lemma of p. 27 with a weakened notion of diagonal dominance (weak in every row, strict in one), under which the Lemma is false; with the standard notion, $D(I-Q)+(D(I-Q))^\top$ is in general not strictly diagonally dominant (a row with $\mu_i=0$ that cannot leave $N$ in one step has row sum $0$). A correct proof combines weak dominance with reachability of every state from the support of $\mu$, which is where $d_i>0$ enters. Second, $X^\top XD(I-Q)$ is not symmetric, so a small $\alpha$ does not make $I-\alpha X^\top XD(I-Q)$ a contraction in the Euclidean norm; the argument goes through its eigenvalues, and turning eigenvalues of modulus below one into $(I-\alpha X^\top XD(I-Q))^n\to0$ is a spectral-radius argument. The probabilistic step is also not free: $w_n$ is a polynomial in $n$ random sequences of unbounded length, and its integrability and the factorization $E\{\eta_{ij}w_n\}=d_ip_{ij}E\{w_n\}$ need independence across sequences.

Formalization scope

States are finite types N (nonempty) and T; the chain is the structure AbsorbingChain with blocks pN, pT and the field $Q^k\to0$. Observation vectors are x : N → Fin K → ℝ with LinearIndependent ℝ x; $X$ is Matrix (Fin K) N ℝ. A sequence is an Episode (list of nonterminal states, terminal state, outcome); IsEpisodeStream states measurability, mutual independence (iIndepFun) and the law $P(\text{path}=s,\text{term}=j,\text{out}\in B)=\mu_{s_1}p_{s_1s_2}\cdots p_{s_mj}\,\nu_j(B)$. Expectations are Bochner integrals, and the goal asserts integrability of $x_i^\top w_n$, so a non-integrable junk value $0$ cannot satisfy it. $d_i$ is defined as an expectation (a sum over sequences), not as $[\mu^\top(I-Q)^{-1}]_i$, so (7) is not circular. "Positive definite" is the paper's footnote 6 ($y^\top Ay>0$ for real $y\ne0$, no symmetry), not Mathlib's Matrix.PosDef.

Trivializations ruled out: the hypothesis $d_i>0$ is the paper's own discarding of never-visited states (without it the goal is false: an unvisited state's weight never moves); N is nonempty and $\mu$ sums to one, so the hypotheses are satisfiable and the goal is not vacuous; the sequences cannot be arbitrary random variables or a fixed sequence, since their law is pinned to $\mu$, $p$ and $\nu$; $\varepsilon$ is chosen before $\alpha$, $w_0$ and the probability space; and the update is per sequence, not the intra-sequence variant of §5.

Corrected slips: "For each nonterminal state $j$" (p. 24) means terminal; the diagonal-dominance definition of p. 27 is replaced by the standard one; $I-\alpha XD(I-Q)X^\top$ (p. 28) means $I-\alpha X^\top XD(I-Q)$. Not formalized: the variance and TD($\lambda$) conjectures of p. 29, §4.3, and the extension claims of §5.

Related open goals on this platform (different models, credited, not re-posed): SuttonBartoRL.BatchTD.batch_td_converges_to_certainty_equivalence (tabular, discounted analogue of Theorem 3), and SuttonBartoRL.LinearTD.keyMatrix_posDef, posDef_of_row_col_sums, expected_td_update (continuing discounted chain with stationary $D$, where every row sum of $D(I-\gamma P)$ is positive). Contributions of any milestone, of general matrix lemmas, and of reusable infrastructure for i.i.d. episode streams are welcome.

Selected references

• R. S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3(1), 9–44, 1988. https://doi.org/10.1023/A:1022633531479
• B. Widrow and M. E. Hoff, Adaptive switching circuits, IRE WESCON Convention Record, 96–104, 1960.
• B. Widrow and S. D. Stearns, Adaptive Signal Processing, Prentice-Hall, 1985.
• J. G. Kemeny and J. L. Snell, Finite Markov Chains, Springer, 1976. https://link.springer.com/book/9780387901923
• R. S. Varga, Matrix Iterative Analysis, Prentice-Hall, 1962 (2nd ed., Springer, 2000: https://doi.org/10.1007/978-3-642-05156-2).
• P. Dayan, The convergence of TD(λ) for general λ, Machine Learning 8, 341–362, 1992. https://doi.org/10.1007/BF00992701
• J. N. Tsitsiklis and B. Van Roy, An analysis of temporal-difference learning with function approximation, IEEE Transactions on Automatic Control 42(5), 674–690, 1997. https://doi.org/10.1109/9.580874

Motivation

A shortest path problem asks how to reach a destination at minimum cost. In a stochastic shortest path problem, a decision at a state selects a probability distribution over successor states, so both the route and its total cost are random. Costs may have either sign. This makes the problem relevant to finite-state control models where rewards and expenses occur before eventual termination. Bertsekas and Tsitsiklis analyze this setting without requiring all one-stage costs to be nonnegative or all to be nonpositive. Their condition instead rules out an improper stationary policy whose costs stay finite from every initial state. Bertsekas and Tsitsiklis (1991), pp. 580–583.

Earlier treatments established Bellman-equation and algorithmic conclusions under positive or nonnegative costs. The 1991 paper traces the finite-control development from Eaton and Zadeh and the compact-control extension from Kushner, then removes the sign restriction while retaining finite state space. It also explains why the Bellman mapping need not contract when an improper policy is available. Bertsekas and Tsitsiklis (1991), pp. 581, 585. A separate, proved Prove2Me theorem from Bertsekas's textbook treats the special case in which every policy is proper and controls are finite; the result here permits improper policies and compact control spaces.

Setting

There are $n\ge1$ states. State $1$ is the destination. At state $i$, a control $u\in U(i)$ incurs a real cost $c_i(u)$ and moves the process to state $j$ with probability $p_{ij}(u)$. A selector $\mu$ chooses one control $\mu(i)$ at every state. A policy $\pi=(\mu_0,\mu_1,\ldots)$ may change selectors over time; a stationary policy repeats one selector. The matrix $P(\mu)$ has entries $p_{ij}(\mu(i))$, and $c(\mu)$ is the vector of one-stage costs. Bertsekas and Tsitsiklis (1991), p. 582.

The cost vector $x(\pi)$ is the coordinatewise limit inferior of expected partial costs, including the possibility of infinite values. The optimal cost $x_i^*$ is the infimum of $x_i(\pi)$ over all policies, including nonstationary ones. Optimality of a policy means it attains that infimum from every initial state. The fixed-selector operator is $T_\mu(x)=c(\mu)+P(\mu)x$; the Bellman operator $T$ takes the coordinatewise infimum of these vectors over selectors. Bertsekas and Tsitsiklis (1991), pp. 582–583, equations (2)–(6).

A stationary policy is proper when its probability of reaching state $1$ tends to one from every starting state. Assumption 1 says state $1$ is absorbing and cost-free, at least one proper stationary policy exists, and every improper stationary policy has a partial-cost coordinate tending to $+\infty$. Assumption 2 makes each control space compact, each cost function lower semicontinuous, and each transition-probability coordinate continuous. Work takes place in $X=\{x\in\mathbb R^n:x_1=0\}$. Bertsekas and Tsitsiklis (1991), pp. 583–584.

Formalization targets

Proposition 2: Bellman's equation and value iteration

Under Assumptions 1 and 2, the optimal cost is finite and is the unique fixed point of $T$ in $X$. Every initial $x\in X$ has

$$\lim_{t\to\infty}T^t(x)=x^*.$$

A stationary selector $\mu$ is optimal exactly when $T_\mu(x^*)=T(x^*)$; an optimal proper stationary selector exists. These are all clauses of Proposition 2, rather than separate targets selected from it. Bertsekas and Tsitsiklis (1991), p. 586, Proposition 2.

Supporting results

The milestone list follows the source's Proposition 1, Lemmas 1–3, and the numbered equations used by their proof. Proposition 1 supplies a weighted maximum-norm contraction when every stationary policy is proper. Lemma 1 describes fixed costs of a proper policy and characterizes properness through a Bellman inequality. Lemma 2 gives continuity of $T$. Lemma 3 controls limits of proper policies; its second part detects a limit that becomes improper through diverging costs. Appendix equations (22) and (24), and the policy-improvement equation (15), provide the paper's intermediate targets. Bertsekas and Tsitsiklis (1991), pp. 585–587, 591–592.

Significance

Proposition 2 identifies the cost of the best policy by a finite-dimensional Bellman equation even though the definition of optimal cost ranges over all, possibly nonstationary, policies. Its convergence clause justifies value iteration from any vector whose destination coordinate is zero. Its policy criterion and existence clause connect a fixed point to an implementable stationary decision rule. The paper applies these conclusions to successive approximation and policy iteration in §4. Bertsekas and Tsitsiklis (1991), pp. 586, 590–591.

The paper proves these statements. This mission seeks machine-checked proofs of their exact finite-state formulation and of the listed intermediate results. The resulting finite stochastic-matrix, hitting, and policy-cost infrastructure can also support other undiscounted control problems. The related proved Prove2Me result for the all-proper finite-control case does not settle this mission's compact-control or improper-policy cases.

Difficulty

When every stationary policy is proper, a common weighted maximum norm makes the Bellman mapping contract. An improper policy can destroy this route: Figure 2 has an absorbing destination and satisfies both assumptions, yet $T(0,x_2)=(0,\min\{1+x_2,2\})$ is not a contraction in any norm on $X$. The main result therefore needs a way to retain fixed-point uniqueness and convergence without a uniform contraction rate. Compactness matters because a sequence of proper selectors may converge to an improper selector; Lemma 3 explains the associated cost behavior. Bertsekas and Tsitsiklis (1991), pp. 585–586, 591–595.

Formalization scope

States are Fin n, with the paper's state $1$ represented by 0; the model requires $n\ge1$. A control set $U(i)$ is a type with a metric, with compactness asserted for its whole carrier. Transition rows explicitly have nonnegative entries summing to one. These are the probability-vector conditions implicit in the word “probability.” Assumption 1 supplies a selector and therefore nonempty control sets. The paper writes $T:\mathbb R^n\to\mathbb R^n$; where a theorem uses only Assumption 1, finite real Bellman infima are made explicit through TRealValued. Under Assumption 2, compactness and lower semicontinuity give real attained minima. Bertsekas and Tsitsiklis (1991), pp. 582–584.

Policy costs and their infimum use extended reals so that an improper policy's $+\infty$ cost is represented without a default finite value. Proposition 2 concludes, rather than assumes, that $x^*$ has real coordinates. Its policy infimum ranges over every sequence of selectors. Matrix products use the identity at time zero; $T^0$ is the identity. The destination-zero restriction is retained in every fixed-point and iteration claim. Defining optimal cost as a Bellman fixed point, or restricting the infimum to stationary policies, would remove the result the paper proves. Solvers can contribute the finite-chain, matrix-inverse, semicontinuity, and convergence arguments needed by these targets.

Selected references

• Dimitri P. Bertsekas and John N. Tsitsiklis, An Analysis of Stochastic Shortest Path Problems, Mathematics of Operations Research 16(3), 580–595, 1991. DOI.

Motivation

A controller often cannot see the state of the system it steers. It sees only measurements that are noisy functions of that state. In operations research this happens in machine maintenance and inspection, in queues observed only partially, and in inventory systems with inexact stock records. In control engineering it is the usual case. The question is what the controller should base its decisions on. The full record of past measurements is the obvious choice, but that record grows with time, so a law that uses it is a function on a space whose dimension grows with the horizon.

K. J. Åström's 1965 paper Optimal Control of Markov Processes with Incomplete State Information answered this question for finite Markov chains. The answer is that the conditional distribution of the hidden state given the measurements is a sufficient statistic. The problem with incomplete information is equivalent to a problem with complete information whose state is that distribution. This is the model now called a partially observable Markov decision process (POMDP), and the conditional distribution is now called the belief state.

Timeline. For linear systems with quadratic cost and Gaussian noise, the separation theorem of Joseph and Tou (1961) and Gunckel and Franklin (1963) says that the optimal control is a fixed function of the conditional mean of the state. Åström (1965) proved the reduction for finite-state Markov chains with arbitrary costs, with the conditional distribution as the new state. Smallwood and Sondik (1973) showed that for finite horizons the value function is piecewise linear and concave in the belief, which made exact computation possible. Bertsekas and Shreve (1978) and Bäuerle and Rieder (2011) gave the reduction for general Borel models.

Setting

The hidden state $x_t$, $t = 1, \dots, N$, takes values in a finite set $S$. The controls $u = (u_1, \dots, u_r)$ range over a compact nonempty set $U \subset \mathbb R^r$. The state moves by the transition probabilities $p_{ij}(u, t) = P\{x_t = j \mid x_{t-1} = i\}$, which are continuous in $u$. The state is observed through outputs $y_t$ in a finite set $Y$, with $q_{ij} = P\{y_t = j \mid x_t = i\}$, conditionally independent given the states. The law of $x_1$ is $p^1$. An instantaneous cost $g(u, i, t)$, continuous in $u$, is paid at each time.

A control law chooses $u(t) = c(\eta_1, \dots, \eta_t, t) \in U$ from the outputs observed so far, $\eta(t) = (\eta_1, \dots, \eta_t)$. With $u(t)$ moving $x_t$ to $x_{t+1}$, a law determines the joint law of $(x_1, \dots, x_N, y_1, \dots, y_N)$ and the expected cost

$$EL = E \sum_{t=1}^N g(u(t), x_t, t). \tag{2.6}$$

Problem P.1 is to find an admissible law minimizing (2.6).

The conditional state distribution is $w_i(t) = P\{x_t = i \mid \eta(t)\}$. It is updated by Bayes' rule: with $z^j(u, w)_i = \sum_s q_{ij}\, p_{si}(u, t+1)\, w_s$ and $\|z\| = \sum_i |z_i|$, the output $\eta_{t+1} = j$ gives $w(t+1) = z^j(u(t), w(t)) / \|z^j(u(t), w(t))\|$, and $\|z^j\|$ is the probability of that output. The cost-to-go $V_k(w)$ is the minimal expected cost of the steps $k, \dots, N$ when $x_k$ has distribution $w$, with $V_{N+1} = 0$. Problem P.2 controls the process $w(t)$ directly: a law chooses $u(t)$ from $w(1), \dots, w(t)$ to minimize $E\sum_{t=1}^N \sum_i g(u(t), i, t)\, w_i(t)$.

Formalization targets

Goal: Theorem 3

P.1 has a solution if and only if P.2 has one. For every solution $(V, c^0)$ of the functional equation

$$V_k(w) = \min_{u \in U} \Big\{ \sum_i g(u, i, k)\, w_i + \sum_j V_{k+1}\Big(\frac{z^j(u, w)}{\|z^j(u, w)\|}\Big) \|z^j(u, w)\| \Big\}, \qquad V_{N+1} = 0, \tag{3.28}$$

with $c^0(w, k)$ attaining the minimum, the law

$$u(t) = c^0(w(t), t)$$

is optimal for P.1 and for P.2, among all admissible laws of each, and both minimal values equal $E_{\eta_1} V_1(w(1))$.

Milestones

1. (3.20)–(3.25): the conditional distributions obey the Bayes recursion, and $\|z^j\| = P[y_{t+1} = j \mid \eta(t)]$.
2. Theorem 1: the cost-to-go satisfies (3.28) with the minimum attained, and an optimal Markov law attains it.
3. Theorem 2: a solution of (3.28) gives an optimal law for P.1 with value (3.29).
4. Lemma 1: under $u(t) = c(w(t), t)$, $\{w(t)\}$ is a Markov process with transition probabilities $P(y, \Gamma, u) = \sum_{k \in K} \|z^k(u, y)\|$.
5. Proof of Theorem 3: the integral against this kernel is the sum in (3.28).

Significance

The result. Theorem 3 replaces a minimization over functions of ever longer measurement records with a recursion over a fixed space, the probability simplex over the states. Every exact and approximate POMDP algorithm starts from it: value iteration on beliefs, the piecewise-linear representation of Smallwood and Sondik, point-based methods. It also splits the controller in two. A filter computes $w(t)$ in real time, and the function $c^0$ can be computed off-line. This is the decomposition the paper draws on p. 189, and it extends the linear-quadratic separation theorem to arbitrary finite chains.

Formalizing it. The theorem is proved. The platform has the reduction in Bäuerle and Rieder's discounted Borel model with an observable state component and rewards in extended reals. It does not have Åström's model: finite chains, time-dependent transition matrices, an unobservable state, costs, and laws of the raw output history. This mission formalizes Åström's statements as he gives them. The cost (2.6) is defined from the joint law of states and outputs, and the comparison classes are all laws of the outputs (P.1) and all laws of the distribution history (P.2). The finite setting makes every expectation a finite sum, so a complete development needs no measure theory.

Difficulty

The obvious argument is backward induction on the conditional distributions. The difficulty is that $w(t)$ depends on the controls already used, so it is not given in advance: the state of the reduced problem is produced by the law being optimized. It has to be shown that the expected cost of an arbitrary law of the outputs, computed from the joint law, splits as the reduced recursion says. In particular, laws that use more of the record than $w(t)$ must gain nothing. Restricting the comparison class to laws of the form $c(w(t), t)$ assumes this conclusion.

A second difficulty is attainment. "Min" in (3.28) and "has a solution" presuppose that minima over $U$ are attained, which needs continuity of $V_{k+1}$ on the simplex. The weights $\|z^j(u, w)\|$ can vanish, and then the update $z^j/\|z^j\|$ is undefined.

Formalization scope

States and outputs are finite types, St and Obs, with the chain given by the structure Model. Controls are Fin r → ℝ, and $U$ is compact and nonempty. The law $p^1$ of $x_1$ is the datum in place of the paper's law of $x_0$, since no control $u(0)$ exists. The transition from $x_t$ to $x_{t+1}$ uses $u(t)$ and the matrix $p(u(t), t+1)$. Times $1, \dots, N$ are indexed by Fin N as $0, \dots, N-1$.

The norm $\|\cdot\|$ is the $\ell^1$ norm l1, not Mathlib's sup norm. Conditional distributions are ratios of path sums, condState, and are claimed only on output histories of positive probability. When $\|z^j\| = 0$ the update is the zero vector and is always multiplied by $0$.

The cost-to-go costToGo is an infimum over admissible tail laws. Its index set is nonempty and the costs are bounded below, so the real infimum is a true infimum. It is never defined through (3.28), since that would make Theorem 1 circular. The P.2 functional sums branch by branch over the outputs, with weights $\|z^j\|$. "Given by Theorem 1" is read as "$c^0(w, k) \in U$ attains the minimum in (3.28)" (IsSolution328).

The goal is not the bare equivalence of solvability. In this compact, continuous, finite setting both problems always have solutions, so that sentence alone is trivially true. The goal also requires the law $c^0(w(t), t)$ to be optimal in both problems, against every admissible law, with equal minimal values.

Reusable beyond this mission are the finite POMDP model, the joint path law, the Bayes filter and the belief-MDP kernel. Welcome contributions include proofs of the milestones, the continuity of $V_k$ on the simplex, and existence of solutions of (3.28).

Selected references

• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10(1):174–205, 1965. https://doi.org/10.1016/0022-247X(65)90154-X
• R. D. Smallwood and E. J. Sondik, The optimal control of partially observable Markov processes over a finite horizon, Operations Research 21(5):1071–1088, 1973. https://doi.org/10.1287/opre.21.5.1071
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978, Chapter 10. https://web.mit.edu/dimitrib/www/soc.html
• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5. https://doi.org/10.1007/978-3-642-18324-9
• P. D. Joseph and J. T. Tou, On linear control theory, Transactions of the AIEE, Part II 80(4):193–196, 1961. https://doi.org/10.1109/TAI.1961.6371743