Dynamic Programming

Motivation

Finite Markov decision models are often described by policies that choose an action from the current state. The admissible class in a total reward problem is wider: a randomized decision may use the complete history of observed states and chosen actions. For an undiscounted infinite horizon, the expected number of visits to a state may be infinite, and the total reward may be an extended real number. It matters whether a test carried out on finitely many pure stationary policies really controls this wider class. Kallenberg's Section 3.2 answers that question for finite models whose transition rows may lose probability mass when the process terminates.

The chapter is part of a 1983 account of linear programming methods for finite Markovian control. Its Theorem 3.2.4 collects earlier characterizations of transience and relates them to a finite linear program. The historical attribution in Kallenberg's Remark 3.2.2 is precise: Veinott (1969) established the equivalence of the first three conditions for nonrandomized policies, Hordijk (1976, course notes) extended the first four to general policies, and Denardo and Rothblum (1979) established the link between pure stationary transience and the LP condition. The mission targets Kallenberg's combined five-way statement, rather than treating those partial precedents as separate conclusions. Kallenberg, pp. 42–43.

Setting

Let $E$ be a finite nonempty state space of size $N$. For every state $i$, let $A(i)$ be a nonempty finite set of actions. Choosing $a\in A(i)$ gives the transition number $p_{iaj}\ge0$ to state $j$, with $\sum_jp_{iaj}\le1$. The missing mass is the probability that the system terminates before another decision epoch. This is a substochastic model; replacing the inequality by equality would change the question. Kallenberg, §2.2.

A policy $R$ specifies, at each epoch $t\ge1$, a probability distribution on $A(i_t)$ after the full history $(i_1,a_1,\ldots,a_{t-1},i_t)$. It may be randomized and may depend on all preceding states and actions. A memoryless policy depends only on the epoch and current state. A pure stationary policy $f^\infty$ chooses a single admissible action $f(i)$ in state $i$ at every epoch. Write $P_R(X_t=j\mid X_1=i)$ for the probability of state $j$ at epoch $t$ from initial state $i$. The policy is transient when $\sum_{t\ge1}P_R(X_t=j\mid X_1=i)<\infty$ for every pair $i,j$. Kallenberg, pp. 20–23.

The finite-horizon survival recursion starts from $y_i^0=1$ and sets $y_i^t=\max_{a\in A(i)}\sum_jp_{iaj}y_j^{t-1}$ for $t\ge1$. A model is contracting if there is a strictly positive vector $\mu$ and a scalar $0\le c<1$ for which $\sum_jp_{iaj}\mu_j\le c\mu_i$ for every admissible $(i,a)$. These objects are determined by the transition system; rewards do not enter the five-way characterization. Kallenberg, p. 23 and pp. 41–43.

Formalization targets

Five equivalent conditions

For any fixed $\beta_j>0$, Theorem 3.2.4 states the equivalence of: transience of every pure stationary policy; transience of every policy; $\max_i y_i^N<1$; contraction; and existence of a finite solution of

$$\max\left\{\sum_{i\in E}\sum_{a\in A(i)}x_{ia}:\ \sum_{i\in E}\sum_{a\in A(i)}(\delta_{ij}-p_{iaj})x_{ia}\le\beta_j\ (j\in E),\quad x_{ia}\ge0\right\}.$$

“Finite solution” means an attained finite optimum. The $\beta_j$ are arbitrary positive right-hand sides, not a choice that the theorem is allowed to make after seeing the model. The state count $N$ is the exponent in $y^N$, and the inequality is strict. Kallenberg, Theorem 3.2.4, pp. 42–43.

Supporting targets

The milestones follow the results the chapter uses on the way to Theorem 3.2.4, in attack order:

1. Theorem 2.5.1 (Derman–Strauch) and its Corollary 2.5.1: for a fixed initial distribution, a memoryless policy reproduces the state-action probabilities $P_R(X_t=j,Y_t=a\mid X_1=i)$ of any policy or of any countable mixture of policies.
2. Lemma 3.2.1: under Assumption 3.2.1, $\lim_{\alpha\uparrow1}v_i^\alpha(R)=v_i(R)$ in $[-\infty,+\infty]$.
3. Theorem 3.2.1: under Assumption 3.2.1 there is a pure stationary policy $f^\infty$ with $v(f^\infty)=v$, where $v_i=\sup_Rv_i(R)$.
4. Theorem 3.2.2: if $v$ is p-summable, then $v_i=\max_{a\in A(i)}\{r_{ia}+\sum_jp_{iaj}v_j\}$.
5. Theorem 3.2.3: if some policy is transient, some pure stationary policy is transient.
6. Lemma 3.2.2: $y_i^t=\sup_R\sum_jP_R(X_{t+1}=j\mid X_1=i)$, attained by the policy $(f_t,f_{t-1},\dots,f_1,f_1,\dots)$ built from maximizers of the recursion.

Assumption 3.2.1 says that every policy's expected total reward $v_i(R)=\lim_T\sum_{t\le T}v^t_i(R)$ exists in $[-\infty,+\infty]$; it is a hypothesis of items 2–4 only. Kallenberg, pp. 32–33, 37–42.

Significance

The theorem gives four finite or structured ways to recognize a property quantified over all policies. The survival condition uses only $N$ recursion steps, and the contraction condition supplies a weighted geometric bound on continuation. The LP links the same property to a finite-dimensional optimization problem. Each characterization can serve a different later argument without assuming the policy class has been reduced to stationary rules. Kallenberg, Theorem 3.2.4.

The five-way theorem and its supporting results are proved in the book; this mission asks for machine-checked proofs of their stated finite-model versions. The Derman–Strauch policy result is quoted by Kallenberg without proof, so its formal proof is a separate substantial contribution. None of these results has a machine-checked proof yet. The general history and occupancy definitions can be reused by later total-reward and constrained-control missions.

Difficulty

Checking only the finitely many pure stationary transition matrices does not directly bound the occupation counts of a history-dependent policy. Such a policy can change its action distribution after each observed path, and it need not be a mixture of stationary policies chosen once at the start. Likewise, $y_i^N<1$ is a finite-horizon bound, whereas transience is a statement about an infinite series of visit probabilities. The main difficulty is connecting these different quantifiers without changing the policy class. The LP condition adds a second boundary: its constraints use $\le\beta_j$, and finite value includes attainment. Kallenberg, pp. 41–45.

Formalization scope

States are Fin N with $N>0$, and actions form one finite ambient type with a nonempty admissible subset $A(i)$ at each state. Transitions are real nonnegative numbers with row sums at most one. Epoch $t=1$ is Lean index zero. A history records states and earlier actions; policy decision rules are normalized and supported on the current state's admissible actions. Occupancies are finite sums of transition products, so the definition of transience is summability of a nonnegative real sequence, not a bound on an individual term.

The reward layer is separate from the transition system. It uses extended real limits under Assumption 3.2.1, while the five-way goal needs no reward hypothesis. Sums $\sum_jp_{iaj}x_j$ of extended reals are only asserted for p-summable $x$, where no $+\infty$ and $-\infty$ meet with positive coefficients; the convention $0\cdot(\pm\infty)=0$ is the book's. The LP objective and constraints range only over admissible state-action pairs. Its finite-solution predicate includes a feasible optimizer. Contraction allows an arbitrary componentwise positive weight $\mu$ and requires $0\le c<1$; it does not normalize $\mu$ to the all-ones vector. The $N$-step test uses the cardinality of the original state space.

All-policy transience means every history-dependent randomized policy. Restricting that quantifier to Markov or stationary policies would remove the central content of the theorem. Useful contributions include finite-history probability identities, the Derman–Strauch occupancy theorem, the maximal-survival recursion, the stationary total-optimality result, and the finite LP characterization. The occupancy and policy definitions are reusable beyond this mission.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. https://ir.cwi.nl/pub/13008
• C. Derman and R. E. Strauch, A note on memoryless rules for controlling sequential control processes, Annals of Mathematical Statistics 37 (1966), 276–278. https://doi.org/10.1214/aoms/1177699618
• A. F. Veinott Jr., Discrete dynamic programming with sensitive discount optimality criteria, Annals of Mathematical Statistics 40 (1969), 1635–1660. https://doi.org/10.1214/aoms/1177697379
• E. V. Denardo and U. G. Rothblum, Optimal stopping, exponential utility, and linear programming, Mathematical Programming 16 (1979), 228–244. https://doi.org/10.1007/BF01582110
• A. Hordijk and L. C. M. Kallenberg, Linear programming and Markov decision chains, Management Science 25 (1979), 352–362. https://doi.org/10.1287/mnsc.25.4.352

Motivation

Finite Markov decision models describe repeated choices whose consequences depend on the present state. They are used when a planner needs one rule that works from every starting state, yet the rule may in principle respond to the entire observed history. Linear programming offers a different description: it records how often each state and action are used, without representing the order of decisions. Kallenberg's account connects these two descriptions for a contracting total-reward model, in which the system may terminate after a transition and all policies have finite expected occupation counts (Kallenberg 1983, §§2.2 and 3.4).

The question is whether the frequency vectors attainable by general randomized policies are already attainable through the simpler stationary classes. This matters for constrained planning: restrictions on expected total resource use are linear in frequencies, while a direct search over every history-dependent policy has no comparable finite parameterization. Kallenberg's Theorem 3.4.8 makes the exact comparison, including initial distributions that assign zero probability to some states (Kallenberg 1983, pp. 72–74).

Setting

Let $E$ be a nonempty finite set of states. Each $i\in E$ has a nonempty finite action set $A(i)$. Taking $a\in A(i)$ earns a real reward $r_{ia}$ and moves to $j$ with probability $p_{iaj}\ge 0$. A row may sum to less than one; the missing probability is termination. A policy $R$ specifies a probability distribution over $A(i)$ after every finite history ending in $i$. A Markov policy uses only time and current state, a stationary policy uses only current state, and a pure stationary policy chooses a single action $f(i)$ in each state. These are the classes $C$, $C_M$, $C_S$, and $C_D$ of §2.2 (Kallenberg 1983, pp. 19–21).

The standing contraction assumption supplies weights $\mu_i>0$ and $0\le\alpha<1$ with

$$\sum_{j\in E}p_{iaj}\mu_j\le\alpha\mu_i \qquad(i\in E,\ a\in A(i)).$$

It is weaker in form than fixing a common discount factor: the weights may differ across states. The assumption makes every policy transient, so expected total rewards and state-action frequencies are finite (Kallenberg 1983, Assumption 3.4.1 and Theorem 3.2.4).

For an initial probability distribution $\beta$, with $\beta_i\ge0$ and $\sum_i\beta_i=1$, write $x_{ja}(R)$ for the expected total number of visits to state $j$ at which action $a$ is chosen, averaged over the initial state. Let $K$, $K(M)$, $K(S)$, and $K(D)$ collect these frequency vectors for the four policy classes. The frequency polytope $P$ consists of nonnegative vectors $x$ satisfying conservation of expected flow at each state:

$$\sum_{a\in A(j)}x_{ja} -\sum_{i\in E}\sum_{a\in A(i)}p_{iaj}x_{ia}=\beta_j \qquad(j\in E).$$

These equalities are those of the dual linear program (3.3.7), and the set names follow Notation 3.3.1 (Kallenberg 1983, pp. 53–55).

Formalization targets

The first milestones identify the total-reward value vector as the smallest TMD-superharmonic vector, establish a bijection between stationary policies and feasible frequencies when every $\beta_i>0$, and show that an optimal linear-programming solution yields a pure stationary policy optimal from every state (Kallenberg 1983, Theorems 3.4.1–3.4.3).

The mission goal allows zero entries in the initial distribution and compares all four policy classes:

$$\overline{K(D)}=K(S)=K(M)=K=P.$$

The overbar is Kallenberg's notation for the closed convex hull, rather than topological closure alone. Since there are finitely many pure stationary policies, $K(D)$ is finite and its convex hull is already closed (Kallenberg 1983, Definition 1.2.1(i) and Theorem 3.4.8).

Significance

The goal says that the finite LP flow constraints characterize exactly the frequencies of arbitrary history-dependent randomized policies. It also says that every such vector is a convex combination of frequencies from pure stationary policies. A resource-constrained objective that depends linearly on expected state-action use can therefore be expressed over $P$ without losing feasible frequency vectors. Kallenberg states this constrained consequence in Theorem 3.4.9; that theorem is beyond this mission's selected milestones (Kallenberg 1983, pp. 73–74).

The results are proved in the book. The remaining work here is a machine-checked development of their definitions and proofs, including the passage from arbitrary histories to finite flow equations. The history and frequency interfaces can also be reused for other finite, terminating control models. A proof of the goal would make explicit which uses of contraction and finite action sets justify the infinite sums and the closed convex hull.

Difficulty

For a stationary policy, the frequency equation can be written with a finite transition matrix. A general policy has a separate decision distribution after each possible history, so there is no single stationary transition matrix to substitute into that formula. A direct identification of $K$ with $P$ therefore skips the main issue. Moreover, the stationary-policy correspondence is one-to-one only when every initial weight is positive. When $\beta_j=0$, different rules at never-visited states may have identical frequencies; the set equality must survive this loss of injectivity (Kallenberg 1983, Theorem 3.4.2 and Remark 3.4.3).

Formalization scope

States and their action sets are finite and nonempty. Actions are indexed by their state, so an illegal state-action pair cannot occur. Transition rows are substochastic; rewards, values, and frequencies are real. Histories contain the past state-action pairs and current state, and time index $n=0$ represents the book's period $t=1$. The four frequency sets range over genuinely different policy classes. In particular, the general set permits every legal history-dependent randomized policy; defining it through stationary policies would erase the goal's content.

The initial distribution in the goal may have zero coordinates. The strictly positive weights in the bijection and LP-optimality milestones are the different convention of §3.3. Frequencies and rewards use infinite sums; contraction supplies their convergence. The value vector is a coordinatewise supremum over legal policies, bounded under contraction. The LP uses equalities, not relaxed inequalities, and the pure-policy set is convexified only in the goal's first equality. Needed infrastructure includes finite history probabilities, stationary transition matrices, inverse stationary flows, superharmonic vectors, and finite-dimensional convex geometry. Contributions that establish these interfaces and the three stated milestones are in scope.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. Publisher repository copy.

Motivation

A Markov decision process describes repeated choices whose costs and subsequent states depend on the current state. Such models are used when a decision affects both today's expense and the options available tomorrow. Papadimitriou and Tsitsiklis studied how the computational difficulty of finding an optimal policy changes between stochastic and deterministic transitions. Their general finite-state problems are P-complete, while their deterministic cases admit highly parallel algorithms Papadimitriou and Tsitsiklis, 1987. The contrast makes the deterministic case a useful setting in which to isolate the precise graph problem hidden inside long-run optimization.

This mission concerns their infinite-horizon average-cost case. When transitions are certain, every decision is an arc in a directed graph. The long-run cost of a policy can be related to the mean cost of a cycle reachable from the initial state. That relation is the mathematical claim supporting the algorithm in the paper's Theorem 3, whose headline says that the deterministic average-cost problem is in NC Papadimitriou and Tsitsiklis, p. 446.

Setting

Let $S$ be a finite set of states and $s_0\in S$ the initial state. At each $s\in S$ there is a finite, nonempty decision set $D_s$. A decision $d\in D_s$ has a real cost $c(s,d)$ and moves the process with certainty to $\operatorname{next}(s,d)\in S$. All of these data are stationary: they do not change with time. A policy $\delta(s,t)$ chooses a decision for each state and each time $t=0,1,2,\ldots$. It generates a trajectory by $s_{t+1}=\operatorname{next}(s_t,\delta(s_t,t))$. The corresponding directed graph has a state for each node and a decision for each arc. It may contain loops and parallel arcs, since different decisions can lead to the same next state.

The paper prints the finite average with $T+1$ cost terms and denominator $T$:

$$a_T^\delta(s_0)=\frac{1}{T}\sum_{t=0}^{T}c(s_t,\delta(s_t,t)).$$

A time-dependent policy's averages may fail to converge. We use the upper limit $g^\delta(s_0)=\limsup_{T\to\infty}a_T^\delta(s_0)$ and optimize over all policies, $g^*(s_0)=\inf_\delta g^\delta(s_0)$. A state $u$ is reachable if some finite walk of decision arcs goes from $s_0$ to $u$. A simple cycle $C$ is a positive-length closed sequence of decision arcs with distinct states before it returns to its start; its mean cost is $\operatorname{mean}(C)=c(C)/|C|$. A loop is a one-arc simple cycle.

For states $u,v$, the min-plus adjacency entry $A_{uv}$ is the least cost of a decision arc from $u$ to $v$, or $+\infty$ when no such arc exists. A min-plus product uses addition in place of multiplication and minimum in place of addition. Thus $(A^k)_{uv}$ represents the least cost of a $k$-arc walk from $u$ to $v$, when such a walk exists Papadimitriou and Tsitsiklis, pp. 445–446.

Formalization targets

Reachable cycles

The first target identifies the value of the original policy optimization problem:

$$g^*(s_0)=\min_{\substack{C\text{ simple cycle}\\C\text{ reachable from }s_0}}\operatorname{mean}(C).$$

It also states that a policy attains this value with convergent finite averages. The milestone for following a reachable cycle gives the attainable direction; the milestone saying that no policy can improve the least mean gives the reverse direction. The latter is formulated with $\liminf$, so it applies even when a policy's averages oscillate.

Min-plus calculation

The second target identifies the finite graph calculation used in the paper:

$$g^*(s_0)=\min_{\substack{u\text{ reachable from }s_0\\1\leq k\leq |S|\\(A^k)_{uu}<+\infty}}\frac{(A^k)_{uu}}{k}.$$

The milestones establish what a min-plus power says about decision walks and why closed walks of lengths from $1$ through $|S|$ recover the least simple-cycle mean. The restriction to reachable $u$ is essential: a cheap cycle in a disconnected component cannot be used from $s_0$.

Significance

The result reduces optimization over infinitely many decision times and all state-and-time policies to finitely many closed-walk calculations. It also guarantees that an optimal long-run value is realized by a trajectory with a genuine limiting average, despite the nonconvergence possible for other policies. The finite formula lets one determine the value by comparing graph quantities indexed by states and lengths; it is the correctness statement beneath the paper's parallel algorithm Papadimitriou and Tsitsiklis, p. 446.

Formalizing the identity creates a reusable bridge between deterministic decision processes, weighted directed walks and min-plus powers. Related proved tropical-algebra results on maximum cycle means use dense matrices and a max-plus convention, rather than the reachable, possibly missing-arc, minimum-cost process here; for example, the platform's TropicalLA.tpow_isGreatest concerns greatest walk weights. The present mission keeps the policy optimum and reachability explicit. The paper proves the result mathematically; these Lean statements are open proof targets in the proposal.

Difficulty

An arbitrary policy can keep changing its choices at repeated visits to the same state. Its averages can oscillate, so one cannot simply assume that its infinite trajectory becomes periodic or that its printed limit exists. The lower-bound claim must apply to every such trajectory. There is a second distinction between a closed walk and a simple cycle: a diagonal min-plus entry allows repeated states, whereas the cycle characterization is stated using simple cycles. Finally, an unrestricted matrix calculation would include cycles unreachable from the chosen initial state.

Formalization scope

Lean represents the general finite stationary deterministic process in its own definition, then defines policies, finite walks, simple cycles, average costs and min-plus powers on top of it. Decisions are arcs, so parallel arcs remain distinguishable; $A_{uv}$ takes their least cost and uses WithTop ℝ for a missing arc. Decision sets are explicitly nonempty because a policy has to make a choice at every state. The finite state set is automatically nonempty once $s_0$ is supplied. Policy time starts at zero. The printed $T+1$ terms divided by $T$ are retained; Lean's $T=0$ quotient is zero and has no effect on the limit. The optimum is the infimum over all policies $\delta(s,t)$, not a quantity defined by cycles or by stationary policies. Finite states and finite decision sets bound the one-step costs and hence the averages; this gives real limsup and infimum their intended values.

The paper's Theorem 3 asserts membership in NC. This mission formalizes the exact optimization identity that makes that algorithm correct. Its processor count and parallel-time bound are outside the scope, as are membership in P, log-space computability of reductions, PSPACE membership and the paper's Corollaries 1–2. Contributions to the finite-walk and min-plus lemmas, the lower bound for arbitrary policy paths, and the cycle-attainment statement are all needed; the graph definitions can be reused in other deterministic control problems.

Selected references

• Christos H. Papadimitriou and John N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 1987, pp. 441–450. DOI.

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

Finding the quickest route between two points of a road network is among the oldest problems of operations research. It is the subproblem inside vehicle routing, network flow and many dynamic programs. Richard Bellman's four-page note On a routing problem (Quarterly of Applied Mathematics, 1958) treats it as a dynamic program. The minimal travel times satisfy a nonlinear system of equations, and that system can be solved by successive approximations that terminate after a number of steps bounded in advance. The iteration is now known as the Bellman–Ford method. A footnote added in proof records that Max Woodbury and George Dantzig had obtained the same scheme independently, and Ford's RAND report of 1956 describes a closely related labelling procedure.

Timeline.

• 1956. L. R. Ford Jr., Network flow theory (RAND P-923): a label-improving procedure for shortest paths.
• 1957. Bellman's Dynamic Programming (Princeton) states the principle of optimality used here.
• 1958. Bellman's note: the routing equation, its uniqueness, approximation in policy space with an (N − 1)-step bound, and a second, monotone increasing scheme.
• 1959. Dijkstra gives a label-setting method for nonnegative lengths.
• 1962. Floyd's Algorithm 97 computes all pairs of shortest distances.

Setting

There are $N$ cities, numbered $1, \dots, N$. Every two of them are linked by a direct road, and city $N$ is the destination. The travel time from $i$ to $j$ is a real number $t_{ij}$; the matrix $T = (t_{ij})$ need not be symmetric. Throughout, $t_{ij} > 0$ for $i \ne j$.

A route from $i$ to $N$ is a sequence of cities $i = c_0, c_1, \dots, c_m = N$ in which consecutive cities differ. Its stops are $c_1, \dots, c_{m-1}$, and its time is $\sum_{r<m} t_{c_r c_{r+1}}$. The minimal time $f_i$ (3.1) is the least time of a route from $i$ to $N$, and $f_N = 0$.

The routing equation (3.2) is the system

$$F_i = \min_{j \ne i}\,[t_{ij} + F_j]\quad (i = 1, \dots, N-1), \qquad F_N = 0 .$$

Approximation in policy space (§5) starts from the direct-route policy (5.2), $f_i^{(0)} = t_{iN}$, and iterates (5.1):

$$f_i^{(k+1)} = \min_{j \ne i}\,[t_{ij} + f_j^{(k)}]\quad (i \ne N), \qquad f_N^{(k+1)} = 0 .$$

The second scheme (§7, (7.1)) starts instead from $\underline f_i^{(0)} = \min_{j\ne i} t_{ij}$ and uses the same step.

Formalization targets

Goal: convergence within $N - 1$ iterations

For every $k \ge N - 1$ the following hold. Each $f_i^{(k)}$ is the minimal time from $i$ to $N$, attained by a route. The vector $f^{(k)}$ solves (3.2). Every real solution of (3.2) equals $f^{(k)}$:

$$k \ge N-1 \;\Longrightarrow\; f^{(k)} = f = \text{the unique solution of (3.2)}.$$

This is the claim of the Summary ("converges after at most $(N-1)$ iterations") and of the last sentence of §5. The paper's bound $N - 1$ is kept, although $N - 2$ also suffices.

Milestones

1. (3.2): the minimal times exist and satisfy the routing equation.
2. §4: (3.2) has at most one solution.
3. (5.4): $f^{(1)} \le f^{(0)}$.
4. §5, the sentence after (5.4): $f_i^{(k)}$ is the minimal time over routes with at most $k$ stops.
5. (5.5): $f^{(k+1)} \le f^{(k)}$ for all $k$.
6. §7: the scheme (7.1) increases, stays below the solution of (3.2) (7.2), and equals it from some index on.

Significance

The result. The note turns an enumeration over exponentially many paths into $N - 1$ rounds of $N$ minimisations each, with a bound fixed before the computation starts. The uniqueness theorem makes the routing equation a characterisation of the minimal times, not merely a property of them. This is the template for later correctness proofs of shortest-path and value-iteration algorithms. The monotone decrease (5.5) is the first instance of policy improvement: every iterate is the value of an actual routing policy.

Formalizing it. The results are classical and proved. What this mission adds is a machine-checked development against the paper's own objects. Routes, their times and minimal times are defined from scratch. The iteration is stated exactly as printed, apart from the corrected initial value at the destination. The (N − 1)-step termination is asserted as an equality, not a limit. Related platform items treat other methods and do not cover these statements. One is the label-correcting method (BertsekasDP.label_correcting_correctness_of_nonneg_arcs, BertsekasDP.label_correcting_terminates). Another is the stochastic shortest path problem under a termination assumption that fails for deterministic routing (BertsekasDP.ssp_main_theorem). There are also the generic candidate-list algorithm (BertsekasNetwork.generic_shortest_path_algorithm), Floyd's Algorithm 97 and Dijkstra's method.

Difficulty

The minimum in (3.2) may be attained at a $j$ whose own optimal route passes back through $i$. The routing equation is a fixed-point equation for an operator that is monotone but not a contraction in any fixed norm. The standard contraction argument for discounted dynamic programs therefore does not apply. Uniqueness has to use $t_{ij} > 0$ to exclude zero-time cycles: with $t_{12} = t_{21} = 0$, the system (3.2) has infinitely many solutions. The $N - 1$ bound depends on the at-most-$k$-stops reading of $f^{(k)}$ and on the fact that an optimal route never needs to revisit a city. Neither is visible from the recursion alone. For the scheme of §7, the page gives no bound on the number of iterations, and none holds uniformly in $t$.

Formalization scope

Cities are Fin (n + 1), so $N = n + 1$, with standing hypothesis $n \ge 1$. City $N$ is Fin.last n, and travel times are t : Fin (n + 1) → Fin (n + 1) → ℝ with $t_{ij} > 0$ for $i \ne j$. Diagonal entries are unconstrained and never used. No symmetry, triangle inequality or integrality is assumed. A route is a list of cities with distinct consecutive entries ending at $N$. Repeated cities are allowed; with positive times this changes no minimum. Minimal times are attained minima over routes (IsMinTime, IsMinTimeWithin), not real infima. The minimum in (3.2) is a Finset.inf' over all $j \ne i$, the destination included.

The paper's loose phrases are made explicit as follows.

• "Using an optimal policy" (3.1) becomes a minimum attained by a route and below every route.
• "Represents the minimum time for a path with at most one stop" becomes, for every $k$, a minimum over routes with at most $k + 1$ roads.
• "Converges after at most $(N - 1)$ iterations" becomes $f^{(k)} = f$ for every $k \ge N - 1$.
• "Only a finite number of iterations will be required" (§7) becomes $\exists K, \forall k \ge K$, $\underline f^{(k)} = f$.
• "The solution of (3.2)" in §7 becomes an arbitrary solution of (3.2), which milestones 1–2 show is the vector of minimal times.

Two printed slips are corrected. (5.2) is printed for $i = 1, \dots, N$, which would set $f_N^{(0)} = t_{NN}$, and with $t_{NN} > 0$ statements (5.4), (5.5) and the goal would be false. The formalization uses $f_N^{(0)} = 0$, the value the paper's own justification needs. (7.1) prints "$N = 1$" for $N - 1$. Section 6 (computational aspects) and the closing expectation of §7 that the first method converges faster are not formalized.

The goal cannot be satisfied trivially. The minimal times are defined from routes, not as a solution of (3.2) or as a limit of the iteration, so the goal connects the recursion to the routing problem itself.

The development needs only finite minima, lists and induction; nothing beyond core Mathlib. The route and minimal-time layer is reusable for other deterministic shortest-path results. Proofs of any milestone are welcome, as are proofs of the sharper bound $N - 2$.

Selected references

• R. Bellman, On a routing problem, Quarterly of Applied Mathematics 16(1) (1958), 87–90. https://doi.org/10.1090/qam/102435
• R. Bellman, Dynamic Programming, Princeton University Press, 1957.
• R. Bellman, The theory of dynamic programming, Bull. Amer. Math. Soc. 60 (1954), 503–515. https://doi.org/10.1090/S0002-9904-1954-09848-8
• L. R. Ford Jr., Network flow theory, RAND Corporation P-923, 1956. https://www.rand.org/pubs/papers/P923.html
• E. W. Dijkstra, A note on two problems in connexion with graphs, Numerische Mathematik 1 (1959), 269–271. https://doi.org/10.1007/BF01386390
• R. W. Floyd, Algorithm 97: Shortest path, Communications of the ACM 5(6) (1962), 345. https://doi.org/10.1145/367766.368168

Motivation

Multistage robust optimization chooses decisions over time while an adversary picks the uncertain data from a known set; every later decision may react to what has been observed. The exact problem is a nested min-max over functions of the past, and is intractable in general. The standard workaround, proposed by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 2004), restricts every decision to an affine function of the observed disturbances. The restricted problem is a single convex (often linear) program, which is why disturbance-affine policies are used throughout robust control, inventory management and model predictive control. The price is suboptimality, and before this paper there was no nontrivial multistage problem in which that price was known to be zero.

Bertsimas, Iancu and Parrilo (arXiv:0904.3986, 2009; Math. Oper. Res. 35(2), 2010) proved that for one-dimensional linear dynamics with box constraints on controls and disturbances, linear control costs and convex state costs, disturbance-affine policies are exactly optimal. Their companion paper (Bertsimas & Goyal, Math. Program. 2012) shows how poorly affine policies can perform in other settings, so the one-dimensional result marks one side of the boundary between models where affine policies are exact and models where they are not.

Setting

Fix a horizon $T$ and an initial state $x_1\in\mathbb R$. For each stage $k=1,\dots,T$ there are a per-unit control cost $c_k\ge0$, control bounds $L_k\le U_k$, disturbance bounds $\underline w_k\le\overline w_k$, and a state cost $h_k:\mathbb R\to\mathbb R$ that is convex and coercive. The state evolves as

$$x_{k+1}=x_k+u_k+w_k,\qquad u_k\in[L_k,U_k],\qquad w_k\in\mathcal W_k=[\underline w_k,\overline w_k].$$

The controller chooses $u_k$ after seeing $x_k$; the adversary then chooses $w_k$. The min-max value $J_{mM}$ is the value of the nested problem $\min_{u_1}[c_1u_1+\max_{w_1}[h_1(x_2)+\min_{u_2}[\cdots]]]$, computed by the Bellman recursion with $J^*_{T+1}\equiv0$:

$$g_k(y)=\max_{w\in\mathcal W_k}\big[h_k(y+w)+J^*_{k+1}(y+w)\big],\qquad J^*_k(x)=\min_{L_k\le u\le U_k}\big[c_ku+g_k(x+u)\big],\qquad J_{mM}=J^*_1(x_1).$$

An affine control policy and an affine running cost at stage $k$ are

$$q_k(w)=q_{k,0}+\sum_{t=1}^{k-1}q_{k,t}w_t,\qquad z_k(w)=z_{k,0}+\sum_{t=1}^{k}z_{k,t}w_t,$$

so $q_k$ sees the disturbances before stage $k$ and $z_k$ those up to stage $k$. Under these policies the state after stage $k$ is $x_1+\sum_{t\le k}(q_t(w)+w_t)$.

Formalization targets

Goal: Theorem 3.1

There exist affine policies $q_k$ and affine costs $z_k$ such that, for every $k=1,\dots,T$,

$$L_k\le q_k(w)\le U_k\quad\forall w\in\mathcal W_1\times\dots\times\mathcal W_{k-1},$$ $$z_k(w)\ge h_k\Big(x_1+\sum_{t=1}^k(q_t(w)+w_t)\Big)\quad\forall w\in\mathcal W_1\times\dots\times\mathcal W_k,$$ $$J_{mM}=\max_{w_1,\dots,w_k}\Big[\sum_{t=1}^k\big(c_tq_t(w)+z_t(w)\big)+J^*_{k+1}\Big(x_1+\sum_{t=1}^k(q_t(w)+w_t)\Big)\Big].$$

At $k=T$ this says that affine policies are robustly feasible and attain the min-max value.

Milestones

1. Lemma 7.1 (with (8)–(9), P2): $J^*_k$ and $g_k$ are convex, and the optimal control is the clamp $\max(L_k,\min(U_k,y^*-x))$ for a minimizer $y^*$ of $c_ky+g_k(y)$.
2. P3: the clamp is non-increasing and 1-Lipschitz.
3. Lemma 4.1: the maximum of $\theta_1+f(\theta_2)$, $f$ convex, over a planar zonogon $\Theta=\pi([0,1]^k)$ is attained at one of the $k+1$ vertices on its right side.
4. Corollary 4.1: the maximum of $\theta_1+f(\theta_2)$ is unchanged when a polygon is replaced by its convex hull, its vertex set, its right side, or the zonogon hull of its vertices.
5. Lemma 4.2: after the optimal control is applied, the worst case is reached on the right side of $\operatorname{conv}\{\tilde v_0,\dots,\tilde v_k\}$.
6. Lemma 4.4: the matching-and-alignment system (37) defining the affine controller is feasible, and its solutions satisfy $-b_i\le q_i\le0$ and $L\le q(w)\le U$.
7. Lemma 4.8 and Lemma 4.9: the affine cost defined by system (51)–(53) dominates the convex cost, first at the hypercube vertices, then on the whole hypercube.

Significance

The theorem is one of the few exact optimality results for affine policies in multistage robust optimization. Combined with linear programming duality it has a computational corollary: when the $h_k$ are piecewise affine, an optimal policy for the full min-max problem is obtained from a single linear program (the affinely adjustable robust counterpart, p. 5), instead of a dynamic program over a continuous state. The construction also shows what is special about one dimension: the relevant uncertainty enters only through a planar zonogon, whose right side has at most $k+1$ vertices, matching the $k+1$ coefficients of an affine policy.

The result is proved in the literature, not formalized; no machine-checked proof of it, or of the zonogon lemmas it uses, is known. The formalization adds a checked proof of the main theorem and of the planar convexity facts (Lemma 4.1, Corollary 4.1) that are reusable for other zonotope arguments. It also closes the gaps the preprint leaves to the reader: Assumption 2 is removed by an infinitesimal perturbation argument, footnote 4 assumes a unique minimizer of $c_ky+g_k(y)$, and Lemma 4.3 is proved in one sub-case only.

Difficulty

Dynamic programming gives the optimal control as a function of the current state, $u^*_k(x_k)$, which is piecewise affine in $x_k$ with up to three pieces. Since $x_k$ is affine in past disturbances, the obvious idea is to substitute; but the composition is piecewise affine, not affine, in the disturbances, and no single affine function reproduces it. An affine policy is necessarily suboptimal at some disturbance sequences. The theorem asserts only that it is never suboptimal at the worst case, and that the excess cost it causes can be absorbed into an affine cost $z_k$ that still dominates $h_k$. Establishing this requires controlling where a convex objective is maximized over a zonogon, and showing that the affine controller and the affine cost can be chosen to reproduce exactly the right-side vertices that matter, at every stage, while staying feasible. A naive matching of all $2^k$ vertices of the disturbance box is overdetermined.

Formalization scope

Stages are indexed by Fin T (0-based). The model is the reduced form (DP) of §2, with dynamics coefficients equal to 1; the paper notes that this is without loss of generality. The standing hypotheses are those of Problem 1.1 ($c_k\ge0$, $h_k$ convex and coercive) plus two disclosed additions, $L_k\le U_k$ and $\underline w_k\le\overline w_k$: the page writes both as intervals but does not say they are nonempty. $J^*_k$ is defined by the Bellman recursion with sSup/sInf over images of nonempty compact intervals of continuous functions, so the values are attained maxima and minima. The max in (14) is stated with IsGreatest, which asserts attainment.

The goal carries none of the proof's normalizations (Assumptions 1–3 of p. 10, the unique minimizer of footnote 4). The milestones of §4 are stated in the paper's simplified notation: the unit hypercube, generators ordered as in (32) (cross-multiplied), the clamp form of the optimal control law (the printed (8) has misprinted thresholds), and, where the paper divides by $b_i$, the hypothesis $b_i>0$. Lemma 4.4 takes Lemma 4.3's conclusions as hypotheses; Lemmas 4.8–4.9 take system (51)–(53) (with two misprints of (53) corrected) as hypotheses instead of "computed by Algorithm 2". Every fraction in a system is cross-multiplied.

Trivializing formalizations are ruled out. (14) uses a maximum over a nonempty box of a continuous function, with the true $J^*_{k+1}$. The policies read only past disturbances (sums over $t<k$, resp. $t\le k$). $J_{mM}$ is the Bellman value over all state-feedback controls, not the value of the affine problem.

The development needs convexity of value functions under partial minimization and maximization, extreme points of planar polygons, and maxima of convex functions over polytopes. Contributions of independent planar-geometry lemmas are welcome, as are proofs of Lemma 4.3 (not stated here) and of the remaining construction lemmas 4.5–4.7.

Selected references

• D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of Affine Policies in Multi-stage Robust Optimization, arXiv:0904.3986v1, 2009; Mathematics of Operations Research 35(2):363–394, 2010. https://arxiv.org/abs/0904.3986, https://doi.org/10.1287/moor.1100.0444
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99(2):351–376, 2004. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming 134(2):491–531, 2012. https://doi.org/10.1007/s10107-011-0444-4
• G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995 (Chapter 7, zonotopes). https://doi.org/10.1007/978-1-4613-8431-1

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

Motivation

A controlled Markov process (CMP), or Markov decision process, models a system that moves randomly between states while a controller chooses actions that influence both the cost incurred and the next state. When the planning horizon is long and no discounting is natural (queueing control, inventory, communication networks, maintenance), the criterion of interest is the long-run average cost. Average-cost problems are harder than discounted ones: the dynamic programming operator is no longer a contraction, and an optimal policy need not exist without structure.

The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993)) organizes the theory by state space. For Borel state spaces and bounded costs, §6.1 follows Dynkin and Yushkevich and works with canonical triplets: a pair of bounded functions and a policy that make the policy optimal for every finite horizon with a fixed terminal cost. Theorem 6.3 is the statement that explains why this notion is the right one: a canonical triplet solves the average-cost problem.

Timeline. The notion of a canonical policy was introduced by Yushkevich (1973) and developed in Dynkin and Yushkevich's Controlled Markov Processes (1979, Chap. 7), which contains the substance of Theorem 6.3 (i)–(iii). Mandl (1974) introduced the discrepancy function that bears his name. The almost-sure statements (v)–(vi) are due to Georgin (1978). Coupled optimality equations for the multichain case go back to Howard (1960).

Setting

The model is a five-tuple $(S, A, U, P, c)$. The state space $S$ and the action space $A$ are Borel spaces. For each state $x$, $U(x)\subseteq A$ is a nonempty compact set of admissible actions, and $K = \{(x,a): a\in U(x)\}$ is measurable. $P(dy\mid x,a)$ is a transition kernel and $c$ a measurable one-stage cost, nonnegative on $K$.

A policy $\pi = (\pi_t)$ chooses the action at time $t$ at random from a kernel $\pi_t(da\mid h_t)$ that may depend on the whole history $h_t = (x_0,a_0,\dots,x_t)$ and charges only $U(x_t)$. The class of all such policies is $\Pi$. Each policy and initial state $x$ determine a law $\mathcal P^\pi_x$ of the state–action process $(X_t, A_t)$, with expectation $E^\pi_x$.

For a horizon $N$ and a terminal cost $h$,

$$J_N(x,\pi,h) = E^\pi_x\Big[\sum_{t=0}^{N-1}c(X_t,A_t) + h(X_N)\Big],\qquad J_N(x,\pi)=J_N(x,\pi,0),\qquad J^*_N(x,h)=\inf_{\pi\in\Pi}J_N(x,\pi,h).$$

The average cost is $J(x,\pi)=\limsup_N \frac1N J_N(x,\pi)$ and the optimal average cost is $J^*(x)=\inf_{\pi\in\Pi}J(x,\pi)$. The span of a bounded function is $\operatorname{span}(h)=\sup h-\inf h$.

With $\mathcal M_b(S)$ the bounded measurable functions, a triplet $(\rho,h,\pi^*)$ with $\rho,h\in\mathcal M_b(S)$ and $\pi^*\in\Pi$ is canonical if

$$J_N(x,\pi^*,h) = J^*_N(x,h) = h(x)+N\rho(x)\qquad\forall N\in\mathbb N_0,\ x\in S. \tag{6.4}$$

A policy $\pi^*$ is strong average optimal if

$$\limsup_{N\to\infty}\frac1N J_N(x,\pi^*)\le\liminf_{N\to\infty}\frac1N J_N(x,\pi)\qquad\forall x\in S,\ \pi\in\Pi. \tag{6.5}$$

Formalization targets

Goal: Theorem 6.3 (i)–(iii)

Let $(\rho,h,\pi^*)$ be a canonical triplet and let $c$ be bounded on $K$. Then for each $x\in S$:

$$\text{(i)}\quad J_N(x,\pi^*)\le J_N(x,\pi)+\operatorname{span}(h)\quad\forall N,\ \forall\pi\in\Pi;$$ $$\text{(ii)}\quad \pi^* \text{ is strong average optimal};\qquad \text{(iii)}\quad J(x,\pi^*)=J^*(x)=\rho(x).$$

Steps toward the goal

The proof's milestones are: $J_N(x,\pi^*,h)\le J_N(x,\pi,h)$; the decomposition $J_N(x,\pi,h)=J_N(x,\pi)+E^\pi_x[h(X_N)]$; part (i) on its own; and $\rho(x)=\lim_N\frac1N J_N(x,\pi^*)$.

Further targets: Theorem 6.3 (v)–(vi)

If $\rho\equiv\rho^*$ is constant and $\Phi(x,a)=c(x,a)+\int h(y)P(dy\mid x,a)-\rho^*-h(x)$ is Mandl's discrepancy function, then for every $\pi\in\Pi$ and $x$,

$$\limsup_{N\to\infty}\frac1N\sum_{t=0}^{N-1}c(X_t,A_t)\ge\rho^*\quad\mathcal P^\pi_x\text{-a.s.},$$

and the running average converges to $\rho^*$ almost surely if and only if $\frac1N\sum_{t<N}\Phi(X_t,A_t)\to0$ almost surely. Moreover $\pi^*$ is sample path average cost optimal. The intermediate milestones are $\Phi\ge0$ on $K$, the almost-sure limit $\frac1N\sum c-\rho^*-\frac1N\sum\Phi\to0$ under every policy, and $\Phi(X_t,A_t)=0$ almost surely under $\pi^*$.

Significance

The result. Theorem 6.3 reduces the average-cost problem on a general Borel space to finding a canonical triplet. Once one is found, $\rho$ is the optimal average cost from every initial state, possibly state-dependent as in multichain models, and the canonical policy is optimal in a strong sense: its worst-case long-run performance is no worse than the best-case long-run performance of any competitor, at every finite horizon up to the additive constant $\operatorname{span}(h)$. With constant $\rho$, optimality also holds path by path. The rest of §6 of the survey looks for conditions on $c$ and $P$ that produce a canonical triplet, and those results rely on this theorem.

Formalizing it. The result is classical and proved; it has no machine-checked proof that we know of. Formalization requires measure-theoretic infrastructure for history-dependent policies on Borel spaces (Ionescu-Tulcea path measures, finite-horizon costs, infima over all admissible policies) together with a strong law for bounded martingale differences for parts (v)–(vi). Both are reusable for any average-cost result on general state spaces.

Difficulty

Parts (i)–(iii) are short on paper; the work is in making every quantity genuine. The infimum $J^*_N$ ranges over a class of kernels, and turning (6.4) into a usable inequality needs the family bounded below. The decomposition of $J_N(x,\pi,h)$ needs integrability, which comes from the almost-sure confinement of the trajectory to $K$, a consequence of admissibility under the path measure. Parts (v)–(vi) need the conditional expectation identity $E^\pi_x[c(X_t,A_t)+h(X_{t+1})-\rho^*-h(X_t)\mid H_t,A_t]=\Phi(X_t,A_t)$ from the Markov structure of the path measure, and a martingale strong law. The tempting shortcut of restricting to stationary or Markov policies is not available: $\pi^*$ and every competitor are arbitrary history-dependent randomized policies.

Formalization scope

• $S$ is a standard Borel space and $A$ a Borel space; $U(x)$ is nonempty and compact with measurable graph $K$; $c\ge0$ on $K$ (Assumption 2.1, which the paper assumes throughout). $c$ and $P$ are defined on $S\times A$ and only their values on $K$ enter.
• $\Pi$ is the class of history-dependent randomized admissible policies (p. 285). Neither $\pi^*$ nor the competitors are restricted.
• $\mathcal P^\pi_x$ is Mathlib's Kernel.trajMeasure. $J_N$ is a Bochner integral and $J^*_N$ a real infimum; every theorem assumes $c$ bounded on $K$, which makes both genuine.
• $J$, $J^*$, both sides of (6.5), and the sample path average cost $J_S$ are computed in EReal, so no limit superior or inferior is a junk value. Part (iii) is the two equalities $J(x,\pi^*)=J^*(x)$ and $J^*(x)=\rho(x)$.
• Part (iv) is not posed: its proof goes through value iteration under Assumptions 2.1–2.3, which Theorem 6.3 does not assume.
• Part (vi) is stated under the hypothesis of (v), $\rho\equiv\rho^*$ constant. As printed it has no hypothesis on $\rho$ and is false: two absorbing states with costs $0$ and $1$ give a canonical triplet whose pathwise average costs differ by state.
• The identity $J_N(x,\pi,h)=J_N(x,\pi)+E^\pi_x[h(X_N)]$ is stated for every $\pi$; the page writes it for $\pi^*$ and applies it to an arbitrary $\pi$ in the proof of (i).
• The sentence "for a canonical policy $\pi^*$, $\Phi(X_t,A_t)=0$, $\mathcal P^\pi_x$-a.s." is stated with $\mathcal P^{\pi^*}_x$, the only reading that makes sense.
• $\Phi\ge0$ is derived on the page from (6.7) via Theorem 6.2, which covers stationary $\pi^*$; here it is stated directly from the canonical triplet for arbitrary $\pi^*\in\Pi$.
• Sample path optimality quantifies over all initial laws (probability measures on $S$), as on p. 288.
• None of the hypotheses is vacuous: the one-state, one-action model with zero cost and $\rho\equiv h\equiv0$ is a canonical triplet (checked in Lean). Strong average optimality is stated as limsup against liminf, not the weaker limsup against limsup.

Contributions welcome: a.s. confinement of trajectories to $K$, integrability lemmas for $J_N$, the Markov property of trajMeasure in the form above, and a strong law for bounded martingale differences.

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 (Theorem 6.3 on p. 318, its proof on pp. 318–319; (6.4), (6.5) on p. 316)
• E. B. Dynkin, A. A. Yushkevich, Controlled Markov Processes, Springer-Verlag, New York, 1979 (reference [51] of the survey; Chap. 7).
• A. A. Yushkevich, On a class of strategies in general Markov decision models, Theory Probab. Appl. 18 (1973) 777–779 (reference [204] of the survey).
• P. Mandl, Estimation and control in Markov chains, Adv. Appl. Probab. 6 (1974) 40–60 (reference [124] of the survey).
• J.-P. Georgin, Contrôle de chaînes de Markov sur des espaces arbitraires, Ann. Inst. H. Poincaré Sect. B 14 (1978) 255–277 (reference [72] of the survey).
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, Cambridge, MA, 1960 (reference [95] of the survey).

Motivation

Many control problems in queueing, inventory and communication systems run indefinitely, and the quantity of interest is the long-run cost per unit time rather than a discounted total. The average cost criterion is harder to analyse than the discounted one: the discounted dynamic programming operator is a contraction, while the average cost problem has no contraction, and on an infinite state space its behaviour depends on the recurrence structure of the controlled chain. The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993)) organises the theory around the average cost optimality equation (ACOE) and the conditions under which it has a solution.

Timeline (as recorded in the survey's §3 and §5). Derman studied the ACOE and characterized optimal stationary policies by its solutions (Derman, On sequential decisions and Markov chains, Management Sci. 1962; Denumerable state Markovian decision processes — average cost criterion, Ann. Math. Statist. 1966). Taylor introduced a vanishing discount argument for a replacement problem (Ann. Math. Statist. 1965). Ross extended it to general countable models, showing that uniformly bounded differential discounted value functions yield a bounded solution of the ACOE (Ann. Math. Statist. 1968, two papers; Introduction to Stochastic Dynamic Programming, 1983). Sennott replaced the uniform bound by one-sided bounds and obtained the average cost optimality inequality (Oper. Res. 1989). The survey presents Ross's result as Theorem 5.2, following the 1983 book; this mission formalizes it.

Setting

A controlled Markov process on the countable state space $S=\{0,1,2,\dots\}$ consists of a metric space $\mathbf A$ of actions; for each state $i$ a nonempty compact set $U(i)\subseteq\mathbf A$ of admissible actions; a cost $c(i,a)\ge0$; and transition probabilities $P(j\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)$.

An admissible policy $\pi$ chooses, at each time $t$, a probability distribution on $U(X_t)$ that may depend on the whole past $(X_0,A_0,\dots,X_t)$. The class of all of them is $\Pi$, and $\Pi_{SD}$ is the class of stationary deterministic policies, maps $f$ with $f(i)\in U(i)$. Each initial state $i$ and policy $\pi$ define a law $P^\pi_i$ of the trajectory, with expectation $E^\pi_i$. For a discount factor $0<\beta<1$,

$$J_\beta(i,\pi)=E^\pi_i\sum_{t=0}^\infty\beta^tc(X_t,A_t),\qquad J(i,\pi)=\limsup_{N\to\infty}\frac1N E^\pi_i\sum_{t=0}^{N-1}c(X_t,A_t),$$

and $J^*_\beta(i)=\inf_{\pi\in\Pi}J_\beta(i,\pi)$, $J^*(i)=\inf_{\pi\in\Pi}J(i,\pi)$. The differential discounted value function is $h_\beta(i)=J^*_\beta(i)-J^*_\beta(0)$. A pair $(\rho,h)$, $\rho\in\mathbb R$, $h:S\to\mathbb R$, solves the ACOE if

$$\rho+h(i)=\min_{a\in U(i)}\Big\{c(i,a)+\sum_{j\in S}P(j\mid i,a)h(j)\Big\},\qquad i\in S.\tag{5.1}$$

In the Lean development these objects are CMP, Policy, StationaryPolicy, pathMeasure, discCost, avgCost, discValue ($J^*_\beta$), optAvg ($J^*$), hRel ($h_\beta$) and ACOE.

Formalization targets

Goal: Theorem 5.2 (p. 301)

Assume $J^*_\beta(i)<\infty$ for all $\beta\in(0,1)$ and $i\in S$, and that there is $K>0$ with $|h_\beta(i)|\le K$ for all such $\beta$ and $i$. Then there are $\rho\in\mathbb R$, a bounded $h:S\to\mathbb R$ and a sequence $\beta_n\in(0,1)$, $\beta_n\to1$, with

$$(\rho,h)\text{ solves (5.1)},\qquad h(i)=\lim_{n\to\infty}h_{\beta_n}(i),\qquad \lim_{\beta\uparrow1}(1-\beta)J^*_\beta(i)=\rho\qquad(i\in S).$$

The goal does not assert that $\rho$ is the optimal average cost; that follows from Theorem 5.1 and Remark 5.1(a), which are milestones.

Milestones

1. Lemma 2.1 (p. 289): the dynamic programming map $T(v)(i)=\inf_{a\in U(i)}\{c(i,a)+\sum_jP(j\mid i,a)v(j)\}$ satisfies $T(v+k)=T(v)+k$ and is monotone.
2. Theorem 2.1 (i), (iii) (p. 289), in the countable model: $J^*_\beta=T_\beta J^*_\beta$ and a $\beta$-discount optimal $f\in\Pi_{SD}$ exists.
3. Equation (5.6) (p. 301): $(1-\beta)J^*_\beta(0)+h_\beta(i)=\min_{a\in U(i)}\{c(i,a)+\beta\sum_jP(j\mid i,a)h_\beta(j)\}$.
4. Theorem 5.1 (p. 299): a solution of (5.1) with $\lim_t\frac1tE^\pi_ih(X_t)=0$ gives $\rho=J(i,f)=J^*(i)$ for a minimizing selector $f$; minimizing selectors are average optimal; conversely, an average optimal $f$ with an irreducible positive recurrent chain is a minimizing selector.
5. Remark 5.1(a) (p. 300): a bounded solution of (5.1) satisfies the growth condition of Theorem 5.1.

Significance

Theorem 5.2 is the template of the vanishing discount method. Under its hypothesis the average cost problem has a bounded solution of the ACOE, so (through Theorem 5.1) the optimal average cost is a constant $\rho$ independent of the initial state, it is attained by a stationary deterministic policy, and it is the Abelian limit of the scaled discounted values. Recurrence conditions on the controlled chain, such as uniformly bounded mean return times to a fixed state (Theorem 5.3 of the survey), are verified by checking the hypothesis of Theorem 5.2; the later results of §5 refine its conclusion under weaker hypotheses.

The theorem itself is classical. What this mission adds is a machine-checked statement and, eventually, proof, on a model with history-dependent randomized policies, compact action sets and unbounded costs, together with the supporting verification theorem (Theorem 5.1) and the discounted optimality equation. To our knowledge none of these results has been formalized in Lean; Mathlib has the Ionescu-Tulcea construction of the path measure but no controlled Markov processes.

Difficulty

The obvious argument fixes a sequence $\beta_n\uparrow1$, extracts a pointwise convergent subsequence of the bounded functions $h_{\beta_n}$ and of the bounded numbers $(1-\beta_n)J^*_{\beta_n}(0)$, and passes to the limit in (5.6). Two steps resist this. First, the limit of a minimum over $U(i)$ is not in general the minimum of the limits: the convergence of $a\mapsto\sum_jP(j\mid i,a)h_{\beta_n}(j)$ must be shown to be uniform on the compact set $U(i)$, which requires more than pointwise continuity of each $P(j\mid i,\cdot)$. Second, the subsequential limit $\rho$ could depend on the subsequence, so part (iii), a limit along all $\beta\uparrow1$, needs an independent identification of $\rho$, here as the optimal average cost through Theorem 5.1, which in turn needs the comparison with arbitrary history-dependent policies. The discounted optimality equation behind (5.6) also has to be established for unbounded costs, where $J^*_\beta$ is not the unique fixed point of $T_\beta$.

Formalization scope

The state space is ℕ; state 0 is the reference state of $h_\beta$. Policies are history-dependent randomized stochastic kernels with the admissibility constraint $\pi_t(U(x_t)\mid h_t)=1$, and $J^*$, $J^*_\beta$ are infima over all of them. Costs are lower Lebesgue integrals with values in $[0,\infty]$, built from Mathlib's Kernel.trajMeasure. The following choices make implicit hypotheses explicit:

• Finiteness of $J^*_\beta$. The paper's bound $|h_\beta|\le K$ presupposes finite values; the goal assumes $J^*_\beta(i)<\infty$, and (5.6) assumes it for its $\beta$.
• Convergent series in the ACOE. A solution of (5.1) requires every series $\sum_jP(j\mid i,a)h(j)$, $a\in U(i)$, to converge, and the minimum to be attained.
• (5.2) over all policies. The paper prints the growth condition of Theorem 5.1 for $\pi\in\Pi_{SD}$, but its conclusion $\rho=J^*(i)$ concerns all policies, and the proof uses the condition for arbitrary $\pi$. It is stated for every $\pi\in\Pi$, with integrability of $h(X_t)$ explicit.
• Theorem 2.1 is cited without proof in the survey for Borel models; in the countable model its Assumptions 2.2–2.3 follow from the continuity assumptions of §5. Only parts (i) and (iii) are stated.
• Lemma 2.1 is stated for functions bounded below (on discrete ℕ these are the lower semicontinuous functions bounded below), with convergent series.
• Irreducible, positive recurrent (converse of Theorem 5.1): every state is reached with positive probability from every state, and every state has finite expected return time.

A formalization in which $J^*$ is an infimum over stationary policies only, in which the ACOE is an inequality or holds for one fixed action, or in which $h_\beta$ is computed from $+\infty$ values through a junk conversion, would trivialize the goal; all three are excluded by the definitions above.

A complete development needs the Ionescu-Tulcea path measure for history-dependent policies, the discounted optimality equation for nonnegative unbounded costs, Scheffé-type uniform convergence on compact action sets, and the martingale identity behind Theorem 5.1. The model file is reusable by the other missions of this series and by any countable-state average cost result; proofs of the milestones are welcome independently of the goal.

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 (reference [38] of the survey).
• C. Derman, Denumerable state Markovian decision processes — average cost criterion, Ann. Math. Statist. 37 (1966) 1545–1553 (reference [39]).
• H. M. Taylor, Markovian sequential replacement processes, Ann. Math. Statist. 36 (1965) 1677–1694 (reference [177]).
• S. M. Ross, Non-discounted denumerable Markovian decision models, Ann. Math. Statist. 39 (1968) 412–423, and Arbitrary state Markovian decision processes, Ann. Math. Statist. 39 (1968) 2118–2122 (references [147], [148]).
• S. M. Ross, Introduction to Stochastic Dynamic Programming, Academic Press, New York, 1983 (reference [150]).
• L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Oper. Res. 37 (1989) 626–633 (reference [156]).