Dynamic Programming

Motivation

Reinforcement learning (RL) formalizes sequential decision-making under uncertainty: an agent repeatedly observes a state, takes an action, receives a reward, and transitions to a new state, with the goal of maximizing cumulative reward over an unknown environment. It underlies applications from game-playing agents to robotics and adaptive medical treatment. What separates RL from the bandit and contextual bandit problems of earlier chapters in this series is state: the environment carries information forward across time steps, so a good action now can pay off many steps later, and a poor exploration strategy can take exponentially long to discover it. This mission formalizes the foundational results of finite-horizon episodic RL — the Markov Decision Process (MDP) model, the Bellman-optimality principle that makes dynamic programming possible, and the analytical toolkit (the performance-difference and Bellman-residual-decomposition lemmas) used throughout the field's regret analyses — culminating in a polynomial regret guarantee for UCB-VI, the canonical optimism-based algorithm for tabular RL introduced by Azar, Osband, and Munos (Minimax Regret Bounds for Reinforcement Learning, ICML 2017, arXiv:1703.05449).

Setting

A finite-horizon episodic Markov Decision Process $M = (S, A, \{P^M_h\}_{h=1}^H, \{R^M_h\}_{h=1}^H, d_1)$ consists of a finite state space $S$, a finite action space $A$, a horizon $H$, per-layer transition kernels $P^M_h : S\times A \to \Delta(S)$ and reward distributions $R^M_h : S\times A \to \Delta(\mathbb R)$, and an initial state distribution $d_1 \in \Delta(S)$. An episode unrolls for $h=1,\dots,H$: the learner selects an action $a_h \sim \pi_h(s_h)$ under a randomized non-stationary policy $\pi = (\pi_1,\dots,\pi_H) \in \Pi^{\mathrm{rns}}$ (each $\pi_h : S \to \Delta(A)$), receives reward $r_h \sim R^M_h(s_h,a_h)$, and transitions to $s_{h+1}\sim P^M_h(s_h,a_h)$. The value of $\pi$ is $f^M(\pi) := \mathbb E^{M,\pi}[\sum_h r_h]$, and the state-action and state value functions $Q^{M,\pi}_h(s,a)$, $V^{M,\pi}_h(s)$ are the analogous reward-to-go quantities from layer $h$ onward. In the online RL problem, $M^\star$ is unknown, the learner interacts with it for $T$ episodes, and the goal is to minimize the regret $\mathrm{Reg} = \sum_{t=1}^T \big(f^{M^\star} (\pi^{M^\star}) - f^{M^\star}(\pi^t)\big)$ against the best policy $\pi^{M^\star} \in \arg\max_{\pi\in\Pi^{\mathrm{rns}}} f^{M^\star}(\pi)$.

Formalization targets

Goal — Theorem 1 (UCB-VI regret)

$$\exists\, C>0,\ \forall\, \delta\in(0,1],\quad \Pr\Big[\mathrm{Reg} \le C\cdot H\cdot S\cdot\sqrt{A\,T}\cdot\sqrt{\log(SAHT/\delta)}\Big] \ge 1-\delta,$$

for the UCB-VI algorithm run with the explicit bonus $b^t_{h,\delta}(s,a) = 2\sqrt{\log(2SAHT/\delta)/n^t_h(s,a)}$, under Assumption 6 (deterministic, known, $[0,1]$-bounded rewards). This is the weakest stable form of the guarantee: it fixes only the shape of the bound (polynomial in $S,A,H,T$, logarithmic in $1/\delta$), leaving the exact leading constant — which the book itself does not pin down on this page — outside the formal claim.

Reaching it rests on three structural facts, each formalized as a milestone in attack order:

• Proposition 25 (Bellman optimality): existence of a single deterministic policy simultaneously optimal at every state, computable by backward induction — the reason dynamic programming solves planning at all.
• Lemma 13 (Performance difference) and Lemma 14 (Bellman residual decomposition): two "credit assignment" identities decomposing a value gap (between two policies, or one policy under two models) into a sum of per-layer, on-roll-in terms.
• Lemma 15 (Error decomposition for optimistic policies): the fact that a greedy policy driven by any optimistic value estimate suffers sub-optimality controlled additively — not exponentially — by that estimate's own Bellman residuals, evaluated on-policy.

Significance

The result itself. Theorem 1 is the chapter's headline result: the first guarantee, in this development, that a learning algorithm — one that does not know the environment's transitions in advance — can achieve regret growing only polynomially in the size of the state space, the action space, and the horizon, and only as $\sqrt T$ in the number of episodes. The chapter's own "combination lock" example (Figure 8) shows this is not automatic: naive exploration strategies (such as $\varepsilon$-greedy, which suffices for ordinary bandits) incur regret exponential in the horizon on some MDPs with as few as $H+2$ states. UCB-VI's guarantee is the sample-complexity foundation on which essentially every subsequent result on tabular, linear, and general function-approximation RL in the book is built.

Formalizing it. No part of this chapter's mathematical content already has a faithful counterpart on the platform (see Difficulty, below, and Formalization scope). This mission contributes: (i) a from-scratch Lean formalization of the finite-horizon episodic MDP model and its value functions, faithful to the book's $0$/$1$-indexing and reward-distribution conventions; (ii) faithful statements (drafted with sorry, not yet proved) of Proposition 25 and Lemmas 13–15; and (iii) a faithful statement of Theorem 1 itself, including a from-scratch construction of the finite $T$-episode adaptive interaction process needed to make sense of a high-probability regret guarantee. Proving these — Proposition 25 by backward induction, Lemmas 13–15 by telescoping, and Theorem 1 by combining Lemma 15's optimism bound with a concentration argument bounding the estimation-error and martingale terms of Eqs. (5.30)–(5.33) (omitted here; see Difficulty) — is open work for solvers.

Difficulty

The obvious approach to Theorem 1 — bound the regret episode-by-episode using only the fact that $Q^t$ is close to $Q^{M^\star,\star}$ in some fixed sense — fails because $Q^t$'s error is itself random (it depends on the transitions observed so far) and compounds across $H$ layers of dynamic programming. Lemma 15 defuses the compounding: it shows the sub-optimality gap is additive in the per-layer Bellman residuals rather than multiplicative, provided $Q^t$ is optimistic. Making $Q^t$ optimistic with high probability, in turn, requires a concentration argument for the empirical transition estimates $\widehat P^t_h$ (an application of Freedman's or the Azuma–Hoeffding inequality, not included among this mission's milestones) and a union bound over all $(s,a,h,t)$ — accounting for the $SAHT$ inside the bonus's logarithm. The final regret sum further requires bounding $\sum_t \sum_h 1/\sqrt{n^t_h(s^t_h,a^t_h)}$ by a pigeonhole/potential-function argument over the visitation counts, which is where the $S\sqrt{AT}$ scaling — rather than a naive $SA\sqrt{T}$ — originates. None of this concentration or counting machinery is included in the current milestones; a solver attempting Theorem 1 needs it as prerequisite lemmas.

Formalization scope

MDP and value functions. States and actions are finite types (Fintype); layers are represented $0$-indexed throughout the Lean development (the book's layer $h$ is h - 1), with the terminal convention V _ _ H _ = 0 matching $V_{H+1}\equiv 0$. Since every value/expectation formula in this chapter uses the reward distribution $R_h(s,a)\in\Delta(\mathbb R)$ only through its mean, EpisodicMDP.R records that mean directly — equivalent, by linearity of expectation, to carrying the full distribution, and changing no theorem's content. Transition kernels and policies are represented as plain real-valued functions (S → A → ℝ-style) rather than as Mathlib's PMF, with IsPolicy/the EpisodicMDP structure's own proof fields asserting the probability-distribution properties (nonnegativity, summing to $1$) where the book requires membership in $\Pi^{\mathrm{rns}}$ or a well-formed kernel; this keeps every expectation a finite Finset.sum, needing no measure theory. The optimal value functions Qstar/Vstar are defined as literal suprema over the entire (uncountable, since $|A|\ge2$) policy type — not via a recursive shortcut — which is what rules out the trivializing formalization of Proposition 25: defining Vstar by the very recursion the proposition asserts would make the proposition a tautology, whereas here it is a genuine claim about a supremum over an enormous space of competitor policies.

UCB-VI and Theorem 1. Because $S$, $A$, $H$, and $T$ are all finite, the $T$-episode adaptive interaction (in which round $t$'s policy is a function of the realized history of the first $t-1$ episodes) is modeled as a finite probability space: the outcome type Fin T → Trajectory S A H is a Fintype, "probability" is a finite sum over it, and "with probability $\ge 1-\delta$" is a plain inequality between two real numbers — no MeasureTheory is used anywhere in this mission. The universal constant $C$ in Theorem 1 is existentially quantified (∃ C > 0, …) rather than given as a literal numeral, since its value is not pinned down by the book on this page and this mission does not carry out the (non-milestoned) concentration argument that would derive it; this is the convention adopted throughout for the book's own "$\lesssim$" notation. The empirical-transition estimator inside $Q^t_h$ is defined to be $0$ when $n^t_h(s,a)=0$ (no data yet collected for that pair) — a boundary case Eq. (5.25) does not address, resolved here by convention rather than proof.

Prior art. The platform's existing BanditAlgorithm.UCRL2Algorithm mission formalizes UCRL2 for the average-reward, infinite-horizon MDP setting with a diameter parameter, and its Bellman-optimality statement is the average-cost optimality equation — genuinely different from this chapter's finite-horizon episodic Bellman recursion, even though both go by the name "Bellman optimality." No reference item was reused; every definition and theorem in this mission is drafted from scratch. Both missions bound regret via optimism over a confidence set of models, but for different objectives (average reward vs. finite-horizon cumulative reward) and different MDP classes.

Reusable infrastructure and open contributions. EpisodicMDP, Policy, V/Q/Qstar/Vstar, and stateDist/stateExp are reusable by any future mission on finite-horizon episodic RL in this book's later chapters. Contributions welcome: proofs of the four milestone lemmas (by backward induction and telescoping, respectively); the concentration lemmas underlying Theorem 1's optimism guarantee (Eqs. (5.30)–(5.33) of the source, not milestoned here); and the final regret proof combining them.

Selected references

• Foster, D. J. and Rakhlin, A., Foundations of Reinforcement Learning and Interactive Decision Making, 2023. arXiv:2312.16730v1
• Azar, M. G., Osband, I., and Munos, R., Minimax Regret Bounds for Reinforcement Learning, ICML 2017. arXiv:1703.05449
• Jaksch, T., Ortner, R., and Auer, P., Near-optimal Regret Bounds for Reinforcement Learning, JMLR 11 (2010).

Motivation

The separation theorem — certainty equivalence for linear-quadratic control with imperfect state information — is one of the celebrated structural results of stochastic control: the optimal controller splits into a least-squares estimator and the deterministic LQR actuator, designed independently. It underlies every LQG autopilot and Kalman-filter-based regulator. Section 5.2 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) proves it from the DP algorithm over information vectors, with Lemma 5.2.1 supplying the key fact that the estimation error is beyond the controller's influence. No formal analogue exists in Mathlib.

Setting

Linear dynamics and measurements

$$x_{k+1} = A_k x_k + B_k u_k + w_k, \qquad z_k = C_k x_k + v_k,$$

with quadratic cost $\mathbb{E}\big[x_N^\top Q_N x_N + \sum_{k<N}(x_k^\top Q_k x_k + u_k^\top R_k u_k)\big]$, $Q_k \succeq 0$, $R_k \succ 0$. The initial state and the zero-mean disturbances/noises are independent with finite ranges; independence is structural — the sample space is the product of an initial-state coordinate and per-stage noise coordinates (BertsekasLQGModel, BertsekasLQGSample, BertsekasLQGProb). A policy maps the realized measurement history $(z_0,\dots,z_k)$ to $u_k$; the closed-loop process is BertsekasLQGTraj, the expected cost BertsekasLQGCost. The estimator $\mathbb{E}[x_k \mid I_k]$ is an explicit conditional average (BertsekasCondExpVec, BertsekasLQGEstimate); the gains $L_k$ come from the time-varying Riccati recursion (BertsekasLQGRiccati, BertsekasLQGGain).

Target

$$\pi^*(I_k) = L_k\, \mathbb{E}[x_k \mid I_k] \ \text{ along its own trajectories} \quad\Longrightarrow\quad J(\pi^*) \le J(\pi)\ \ \forall \pi,$$

— BertsekasDP.lqg_certainty_equivalence (goal). Milestone: Lemma 5.2.1 in pointwise form — the error $x_k - \mathbb{E}[x_k \mid I_k]$ is the same under any two policies, outcome by outcome (lqg_estimation_error_policy_independent).

Significance

This is the theorem that justifies designing estimator and controller separately — remove it and the entire LQG methodology loses its warrant. The formalization also yields the first machine-checked instance of the informational decomposition (control-dependent part + policy-independent error) that recurs throughout imperfect-information control. Notably the result needs no Gaussian assumption — only zero mean and independence — and the finite-support model makes that generality exact. The result is classical (Joseph–Tou 1961, Gunckel–Franklin 1963; the book's §5.2); the formal proof is new.

Difficulty

The heart is Lemma 5.2.1: showing the estimation error coincides, sample by sample, with the error of the control-free system — which requires proving that the observation-history σ-events under any policy coincide with those of the control-free system (controls are determined by the history, so they shift observations by a known amount). Then the DP argument over information histories must carry the quadratic decomposition through the backward recursion. Bookkeeping over histories-as-lists is the main formal burden; probability theory stays finite.

Formalization scope

Finite-support randomness (all expectations are finite sums); conditional expectation with the explicit junk value 0 on zero-probability events — the goal's hypothesis is accordingly restricted to outcomes of positive probability. Policies are functions of the measurement list only (equivalent to the book's information vector for deterministic policies, since past controls are recoverable from past measurements). Matrices are time-varying; positive definiteness of $R_k$ makes every matrix inverse in the gains genuine. Measurement noise covariance is not assumed positive definite — the estimator is the abstract conditional expectation, not the Kalman filter (whose recursive form, §5.2.1, would be a natural follow-up mission).

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§5.2, Lemma 5.2.1.) http://www.athenasc.com/dpbook.html
• P. D. Joseph, J. T. Tou, On linear control theory, Trans. AIEE 80 (1961), 193–196. https://doi.org/10.1109/TAI.1961.6371743
• T. L. Gunckel, G. F. Franklin, A general solution for linear sampled-data control, J. Basic Eng. 85 (1963), 197–201. https://doi.org/10.1115/1.3656559

Motivation

Retailers and restaurants increasingly deliver orders from their own stores within an hour or less. Orders arrive throughout the day, a fixed pool of drivers is based at the store, and in each dispatch wave the operator must decide how many drivers to send out now and along which routes. Sending many drivers now gives short delivery times for the current orders but leaves few drivers for orders that arrive while those drivers are still on the road. Liu and Luo (arXiv:2107.13058, Manufacturing & Service Operations Management, 2023) model this trade-off as a finite-horizon stochastic dynamic program and propose a rollout policy built on a tractable approximation of its cost-to-go. Their Theorem 1 justifies the approximation: with suitable parameters it lies below the true expected cost-to-go, with other parameters it lies between that cost and the cost of any feasible simple policy, and in the last period it is exact. This mission formalizes that theorem.

Setting

A store (the depot $0$) serves a finite set $\mathcal I$ of customer locations over $N$ periods with strictly increasing decision epochs $t_1 < \dots < t_N$. A fleet of $\bar K$ drivers carries at most $Q$ items per trip; travel times $\tau(i,j) \ge 0$, an on-site service time $s \ge 0$ and a delivery target $L_{\max}$ are given. At epoch $t_n$ the operator observes the demand of period $n$: the set $\mathcal I^n \subseteq \mathcal I$ of locations with an order and the quantities $q^n_i$, drawn from a finitely supported law $\mathbb Q^n$, independently across periods.

The driver status $\zeta^n = (\zeta^n_1,\dots,\zeta^n_N)$ records how many drivers are still en route in each period $n'$ because of earlier dispatches, so $\bar K - \zeta^n_n$ drivers are available at $t_n$. A decision $Y^n$ is a set of depot-to-depot routes $0 \to i_1 \to \dots \to i_m \to 0$, one per dispatched driver. It is feasible if it uses at most $\bar K - \zeta^n_n$ drivers, serves every current order exactly once, loads at most $Q$ items per route, and delivers every order within $L_{\max}$. The delivery times are $u_{i_1} = \tau(0,i_1)$ and $u_{i_{k+1}} = u_{i_k} + s + \tau(i_k,i_{k+1})$; the cost of $Y^n$ is $\sum_{i \in \mathcal I^n} u_i(Y^n)$. A driver whose route lasts longer than $t_{n'} - t_n$ is counted as en route in period $n'$; this is the transition (9) from $\zeta^n$ to $\zeta^{n+1}$.

The cost-to-go $\mathcal H_n(\mathcal I^n, q^n, \zeta^n)$ is the minimum over feasible $Y^n$ of the period's cost plus $\mathbb E_{\mathbb Q^{n+1}}[\mathcal H_{n+1}]$ at the resulting status, with $\mathcal H_N$ the period cost alone ((7)–(8)). The single-period cost $\mathcal H^s(K, \mathcal I^n, q^n)$ is the minimum cost of serving the demand with at most $K$ drivers.

The approximation $\mathbf{APT}^n(\zeta^n)$ (10) replaces the future by single-period problems coupled only through driver counts:

$$V^n_{APT}(\zeta^n) = \min_{K^{n'} \in \mathbb N} \sum_{n'=n}^{N} \mathbb E_{\mathbb Q^{n'}}\big[\mathcal H^s(K^{n'}, \mathcal I^{n'}, q^{n'})\big] \ \ \text{s.t.}\ \ \sum_{m=n}^{n'} \omega^{n'}_m(K^m) \le \bar K - \zeta^n_{n'},\ \ n' = n,\dots,N,$$

where $\omega^{n'}_{n'}(K) = K$ and the nonnegative parameters $\omega^{n'}_m(K^m)$, $m < n'$, estimate how many of the $K^m$ drivers dispatched in period $m$ are still en route in period $n'$. A static myopic policy dispatches a state-independent number $K^{n',sm}$ of drivers in each period and routes them to minimize the single-period cost; it is feasible from $(n,\zeta^n)$ if it never asks for more drivers than are available and its single-period problems are always feasible.

Formalization targets

Goal: Theorem 1 (p. 13)

For $1 \le n \le N$ and a status with $\zeta^n_{n'} \le \bar K$:

$$\exists\,\omega:\ V^n_{APT}(\zeta^n;\omega) \le \mathbb E_{\mathbb Q^n}[\mathcal H_n], \qquad \forall\,\pi^{sm}\ \text{feasible}\ \exists\,\omega:\ \mathbb E_{\mathbb Q^n}[\mathcal H_n] \le V^n_{APT}(\zeta^n;\omega) \le J_n(\pi^{sm}),$$

and $V^N_{APT}(\zeta;\omega) = \mathbb E_{\mathbb Q^N}[\mathcal H_N(\cdot,\zeta)]$ for every $\omega$.

Milestones (Appendix D, pp. 34–35, and Lemma 1, p. 12)

1. With $\omega^{n'}_m \equiv 0$ for $m < n'$: $V^n_{APT} = \sum_{n'} \mathbb E[\mathcal H^s(\bar K - \zeta^n_{n'})] \le \mathbb E[\mathcal H_n]$.
2. For $n < N$ and a feasible static myopic policy: $\mathbb E[\mathcal H_n] \le J_n(\pi^{sm})$, and some $\omega$ gives $V^n_{APT} = J_n(\pi^{sm})$.
3. At $n = N$: $\mathbb E[\mathcal H_N] = \min_{K^N \le \bar K - \zeta^N_N} \mathbb E[\mathcal H^s(K^N,\cdot)]$.
4. Lemma 1: $\mathcal H_n$ and, for nonnegative $\omega$, $V^n_{APT}$ are nondecreasing in $\zeta^n$.

Significance

The rollout policy AJRP of the paper solves, at each epoch, the current routing problem together with $\mathbf{APT}^{n+1}$ as a stand-in for the future. Theorem 1 is what connects that stand-in to the dynamic program: it shows that the en route parameters move the approximation between a valid lower bound and the cost of an implementable policy, and its exactness part yields the paper's Corollary 1 (AJRP is optimal for $N = 2$). Lemma 1 shows the approximation keeps the monotonicity of the true value in the driver status.

The paper's proofs are in its Online Appendix (Appendix D). They are short but informal, and the formal statement here differs from the printed one in three pinned-down respects: the single-period cost is read with at most $K$ drivers, as the proofs use it; the upper bound is capped by the policy's cost, since otherwise it is vacuous; and the parameter choice printed for the upper bound has to be corrected in the last period. No part of the result has a machine-checked proof. A formal proof makes these readings definitive, and it produces a reusable Lean model of multi-period dispatching with routes, en route drivers and a Bellman recursion over a random demand.

Difficulty

Every part is a backward induction on the remaining periods, but the inductions run over a state that grows: the status $\zeta^{n+1}$ depends on the durations of the routes chosen in period $n$, and the infimum in (7) is over finite lists of routes, not over a finite action set. The lower bound needs that a larger status can only raise the cost; the upper bound needs that a policy which is feasible on its reachable states stays feasible after every realized demand. Exchanging the expectation with the minimum over the driver count in the last period is not a general fact and holds only because the single-period cost is nonincreasing in the number of available drivers. The obvious choice of parameters for the upper bound, the one printed in the proof, does not bound the last period's count and fails.

Formalization scope

Locations are a type with the depot as none; periods are 1-based natural numbers and every statement carries $1 \le n \le N$. Costs and values lie in $[0,\infty]$; every minimum is an infimum, equal to $+\infty$ on an empty feasible set; expectations are sums against the probability mass function of $\mathbb Q^n$. A decision is a list of nonempty routes covering the current orders exactly once. The parameters $\omega$ are nonnegative reals by their type, with the diagonal $\omega^{n'}_{n'}(K) = K$ written into (10). The available drivers in the dynamic program are $\bar K - \zeta^n_n$ in $\mathbb N$; in APT the right-hand side is the real $\bar K - \zeta^n_{n'}$.

Standing assumptions, shared by every statement: $N \ge 1$; strictly increasing epochs; finitely supported, period-independent demand laws; $q^n_i = 0$ off $\mathcal I^n$. Added hypothesis: $\zeta^n_{n'} \le \bar K$ for $n \le n' \le N$ (the en route drivers belong to the fleet). Disclosed readings: travel times do not depend on the period; delivery times follow the recursion of Appendix C with equality, starting from the depot leg; a policy's expected cost is defined recursively along its decisions.

Ruled out: defining $\mathcal H_N$ or $\mathcal H^s$ through the APT objective (exactness would become definitional); decision sets that may leave orders unserved (every cost would vanish); an upper bound without the cap by the policy's cost; negative parameters $\omega$.

The development needs the model and its recursion (provided as one definition file), monotonicity of $\mathcal H^s$ in $K$, and induction principles for the well-founded recursions. Proofs of the milestones in any order are welcome; Lemma 1 is not used by the paper's proof of Theorem 1 but is a natural first step.

Selected references

• S. Liu, Z. Luo, On-Demand Delivery from Stores: Dynamic Dispatching and Routing with Random Demand, Manufacturing & Service Operations Management, 2023; preprint arXiv:2107.13058v3, 2022. https://arxiv.org/abs/2107.13058
• W. B. Powell, Approximate Dynamic Programming: Solving the Curses of Dimensionality, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9781118029176
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 4th ed., Athena Scientific, 2017 (rollout policies, Ch. 6).

Motivation

Multistage stochastic linear programs model decisions taken over time under uncertainty: reservoir releases in hydro-thermal scheduling, production and inventory plans, capacity expansion. Their standard solution method, stochastic dual dynamic programming (SDDP, Pereira and Pinto 1991), approximates each stage's cost-to-go function from below by cutting planes. This gives a lower bound on the optimal value and a candidate policy, but no guaranteed upper bound: in the risk-neutral case the policy's expected cost is estimated by Monte Carlo simulation.

Planners who are averse to risk replace the expectation in each stage by a coherent risk measure (Artzner, Delbaen, Eber and Heath 1999), nested stage by stage so that the resulting dynamic risk measure is time consistent (Ruszczyński and Shapiro 2006). Under such a nested objective, simulation no longer estimates the cost of a policy: the nested risk of a policy is not an average over sampled scenarios. Philpott, de Matos and Finardi (2013) address this by an inner approximation of the cost-to-go functions from above, built from convex combinations of finitely many points with known upper bounds. Their Proposition 5 shows that the optimal value $y$ of the resulting first-stage problem bounds the nested risk-adjusted cost of the policy defined by the inner approximation. This gives a deterministic upper bound that complements the SDDP lower bound, and they apply it to the Brazilian hydro-thermal system.

Setting

There are $T\ge2$ stages. The decision at stage $t$ is $x_t\in\mathbb R^n$; $A_t,E_t$ are $m\times n$ matrices and $c_t\in\mathbb R^n$. Stage 1 is deterministic: $A_1x_1=b_1$. For $t\ge2$ a random outcome $\omega_t$ ranges over a finite set $\Omega_t$, independently of earlier stages, and enters through the right-hand side $b_t(\omega_t)$. The feasible set of stage $t$ given the previous decision $x_{t-1}$ is

$$\mathcal X_t(\omega_t)=\{x_t\ge0:\ A_tx_t=b_t(\omega_t)-E_tx_{t-1}\}.$$

A coherent risk measure $\rho$ maps random costs $Z:\Omega\to\mathbb R$ to $\mathbb R$ and is subadditive, monotone ($Z_1\le Z_2\Rightarrow\rho(Z_1)\le\rho(Z_2)$), positively homogeneous and translation equivariant ($\rho(\lambda+Z)=\lambda+\rho(Z)$). Larger is worse: these are costs. Each stage $t\ge2$ carries a one-step coherent risk measure $\rho_t$ on random costs over $\Omega_t$. It is extended to costs in $\mathbb R\cup\{+\infty\}$ by $\bar\rho_t(Z)=+\infty$ whenever some outcome has infinite cost.

For $s=2,\dots,T$ fix points $x^1_{s-1},\dots,x^{J_{s-1}}_{s-1}$ and numbers $q^1_s,\dots,q^{J_{s-1}}_s$. The inner approximation is the lower boundary of the convex hull of the pairs $(x^j_{s-1},q^j_s)$:

$$\hat{\mathcal Q}_s(x)=\min\Big\{\sum_j\lambda^jq^j_s:\ \sum_j\lambda^jx^j_{s-1}=x,\ \lambda\ge0,\ \sum_j\lambda^j=1\Big\},$$

which is $+\infty$ off the convex hull of the points, with $\hat{\mathcal Q}_{T+1}\equiv0$. The policy's stage problem (13) and the first-stage problem (8) are

$$q_t(x_{t-1},\omega_t)=\min_{x_t\in\mathcal X_t(\omega_t)}c_t^\top x_t+\hat{\mathcal Q}_{t+1}(x_t),\qquad y=\min_{A_1x_1=b_1}c_1^\top x_1+\hat{\mathcal Q}_2(x_1).$$

The numbers $q^j_s$ are upper bounds when $q^j_s\ge\bar\rho_s\big(q_s(x^j_{s-1},\omega_s)\big)$ for all $s$ and $j$. A policy defined by the inner approximation, $\hat\pi$, takes at each state $x_{t-1}$ and outcome $\omega_t$ an action $\hat x_t(x_{t-1},\omega_t)$ solving (13), and a first-stage action $\hat x_1$ solving (8). The actual risk-adjusted cost of $\hat\pi$ over stages $t,\dots,T$ is

$$\hat v_t(x_{t-1},\omega_t)=c_t^\top\hat x_t+\bar\rho_{t+1}\big(\hat v_{t+1}(\hat x_t,\omega_{t+1})\big),$$

with no future term at $t=T$. The nested risk-adjusted cost of the policy is $v(\hat\pi)=c_1^\top\hat x_1+\bar\rho_2(\hat v_2(\hat x_1,\omega_2))$.

Formalization targets

Goal: Proposition 5

$$v(\hat\pi)\ \le\ y.$$

The bound holds for every $T\ge2$, every family of coherent $\rho_t$, every choice of points satisfying the upper-bound property, and every minimizing selection $\hat\pi$.

Milestones

1. The convexity display of §2: subadditivity and positive homogeneity imply $\rho(\alpha Z_1+(1-\alpha)Z_2)\le\alpha\rho(Z_1)+(1-\alpha)\rho(Z_2)$.
2. $\hat{\mathcal Q}_s$ is the lower boundary of the convex hull $\mathcal H$ of the pairs $(x^j_{s-1},q^j_s)$ (its epigraph is $\mathcal H$ plus the vertical half-line), hence convex with $\hat{\mathcal Q}_s(x^j_{s-1})\le q^j_s$, and every convex function bounded by the $q^j_s$ at the points lies below $\hat{\mathcal Q}_s$.
3. $q_t(\cdot,\omega_t)$ is convex in $x_{t-1}$.
4. The interpolation bound $\bar\rho_t\big(q_t(x_{t-1},\omega_t)\big)\le\hat{\mathcal Q}_t(x_{t-1})$.
5. The induction claim $\bar\rho_t\big(\hat v_t(x_{t-1},\omega_t)\big)\le\hat{\mathcal Q}_t(x_{t-1})$ for $t=2,\dots,T$ and every $x_{t-1}$.

Companions

Proposition 3, the risk-neutral case $\rho_t=\mathbb E$. Proposition 4, the subgradient rule $\sum_mp_m\tilde\zeta_mg(\tilde x,\omega_m)\in\partial_x\rho(Z(x,\omega))$ for $\rho$ given by its dual representation. The existence of a policy $\hat\pi$, which shows that the hypotheses of the goal can be met.

Significance

Proposition 5 makes the inner approximation a certificate. Any policy computed by minimizing against $\hat{\mathcal Q}_{t+1}$ has nested risk-adjusted cost at most $y$, a number obtained by solving one linear program. Together with the lower bound $z$ from outer approximation it brackets the risk-adjusted optimal value. The gap $y-z$ then measures the quality of a risk-averse SDDP policy without simulation, which the nested objective does not allow. The bound covers every coherent nesting used in practice, such as mixtures of expectation and CVaR.

The results are proved in the paper. None of them is machine-checked. A formalization adds a precise account of the infinite values the paper does not discuss: infeasible stages, points outside the convex hull, and the extension of $\rho_t$ to $+\infty$. It also pins down the exact form of the upper-bound hypothesis the induction needs.

Difficulty

The obvious reading of the hypothesis on p. 16, "$q^j_{t+1}$ is an upper bound on $\rho_{t+1}(Q_{t+1}(x^j_t,\omega_{t+1}))$" with the true value function $Q_{t+1}$, does not support the induction. The policy $\hat\pi$ does not act optimally, so its cost can exceed the true value, and the inductive step compares $\hat v_t$ with the policy's own stage value $q_t$, not with $Q_t$. The hypothesis that works bounds the risk-adjusted optimal value of the policy's stage problem (13) at the points, which is what the paper's Upper Bound Computation actually computes.

The second difficulty is infinite values, which the paper never discusses. A risk measure is defined on real random costs, yet stage problems can be infeasible, $\hat{\mathcal Q}_s$ is $+\infty$ off a convex hull, and a convex combination may put zero weight on a point whose bound is $+\infty$. Every inequality of the paper has to be re-read in $\mathbb R\cup\{+\infty\}$, and the extended-real arithmetic must not silently produce a value the paper does not intend.

Formalization scope

Vectors are Fin n → ℝ, all stages share $n$ and $m$, and costs that may be infinite are EReal. Minima are EReal infima, $+\infty$ on an empty set. Attainment of a minimum is never built into a definition: the policy is a selection with a minimizing property, required at every state where the stage problem is feasible. Stages are natural numbers. Points and bounds are indexed by the stage $s$ of the function $\hat{\mathcal Q}_s$ they define, so pts s j is $x^j_{s-1}$ and qv s j is $q^j_s$. Stagewise independence is built in: $\omega_t$ ranges over $\Omega_t$ whatever happened before.

Standing assumptions made explicit in the statements:

• $T\ge2$;
• $\rho_t$ coherent for $t=2,\dots,T$ (all four axioms, though the proof uses only monotonicity and convexity);
• the terminal convention $\rho_{T+1}(Q_{T+1})=0$, so $\hat{\mathcal Q}_{T+1}\equiv0$;
• (8) without the constraint $x_1\ge0$, as printed;
• the upper-bound hypothesis in the form above.

The risk measures $\rho_t$ act on real random costs and are extended by $\bar\rho_t(Z)=+\infty$ when some outcome has infinite cost. In Proposition 4, $\rho$ is given by its dual representation (10); the representation theorem itself is not part of the mission. The existence statement adds solvability of $A_1x_1=b_1$ and boundedness below of the last-stage program, without which (8) or the last stage has no solution.

The goal is not to be trivialized. Its hypotheses mention neither $\hat v_t$ nor the induction claim; the policy must minimize at every feasible state, not only along visited states; and the statement is for general $T$ and general coherent $\rho_t$, not the expectation. The bound is trivially true when $y=+\infty$ and is informative when $\hat x_1$ lies in the convex hull of the stage-1 points.

A complete development needs:

• convexity of extended-real linear-programming value functions in their right-hand side;
• convexity of the convex-hull function $\hat{\mathcal Q}$;
• finite Jensen-type inequalities for monotone convex risk measures;
• linear-programming attainment, for the existence companion.

The first two are reusable for any SDDP-type development. Proofs of the milestones in any order are welcome.

Selected references

• A. B. Philpott, V. L. de Matos, E. Finardi, On Solving Multistage Stochastic Programs with Coherent Risk Measures, Operations Research 61(4), 2013. https://doi.org/10.1287/opre.2013.1175
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent Measures of Risk, Mathematical Finance 9(3), 1999. https://doi.org/10.1111/1467-9965.00068
• A. Ruszczyński, A. Shapiro, Conditional Risk Mappings, Mathematics of Operations Research 31(3), 2006. https://doi.org/10.1287/moor.1060.0204
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52, 1991. https://doi.org/10.1007/BF01582895
• A. Shapiro, Analysis of stochastic dual dynamic programming method, European Journal of Operational Research 209(1), 2011. https://doi.org/10.1016/j.ejor.2010.08.007

Why evaluate a policy against an ambiguous transition kernel

A Markov decision process (MDP) evaluates a policy by its expected discounted reward, which requires the transition probabilities. In practice these are estimated from data, and the optimal policy of the estimated model can perform badly under the true kernel. Robust MDPs replace the kernel by an ambiguity set of kernels and judge a policy by its worst-case expected reward over that set (Satia–Lave 1973; Nilim–El Ghaoui 2005; Iyengar 2005).

Robust evaluation is tractable when the ambiguity set is rectangular, meaning that the kernels of different states (or state–action pairs) can be chosen independently. Many natural ambiguity sets are not rectangular, for example confidence regions for jointly estimated parameters. Wiesemann, Kuhn and Rustem (Math. Oper. Res. 2013) show that for general sets robust policy evaluation is NP-hard even to approximate (their Theorem 2.6). They then give a lower bound computable by semidefinite programming, which is the subject of this mission.

Timeline:

• 1973: Satia and Lave pose MDPs with uncertain transition probabilities.
• 2005: Nilim–El Ghaoui and Iyengar solve robust dynamic programming over (s, a)-rectangular sets with deterministic policies.
• 2011: Kuhn, Wiesemann and Georghiou develop affine (linear) decision rules with S-lemma reformulations in stochastic and robust optimization.
• 2013: Wiesemann, Kuhn and Rustem treat s-rectangular and non-rectangular ambiguity sets with randomized policies. For the latter they give the affine approximation of their Theorem 3.8.

The robust MDP with an affinely parametrized ambiguity set

There are finitely many states $\mathcal S$ and actions $\mathcal A$. Choosing action $a$ in state $s$ and moving to $s'$ earns a reward $r(s,a,s')\ge 0$. Rewards are discounted by $\lambda\in(0,1)$, and the initial state has distribution $p_0$ in the probability simplex $\mathcal M(\mathcal S)$. An unknown 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\},$$

where each $O_l$ is symmetric with $O_l\preceq 0$. The set $\Xi$ is bounded and has a Slater point $\bar\xi$, at which every constraint is strict. The transition probabilities depend affinely on $\xi$: $p^\xi(\cdot\mid s,a) = k_{sa}+K_{sa}\xi$, and this is a probability vector for every $\xi\in\Xi$.

A stationary randomized policy $\pi\in\Pi$ fixes a distribution $\pi(\cdot\mid s)$ over actions in each state. It induces the transition matrix $\widehat P_{ss'}(\xi)=\sum_a\pi(a\mid s)p^\xi(s'\mid s,a)$ and the expected rewards $\widehat r_s(\xi)=\sum_a\pi(a\mid s)\sum_{s'}p^\xi(s'\mid s,a)r(s,a,s')$. The reward to-go is $v(\xi)=\sum_{t\ge0}[\lambda\widehat P(\xi)]^t\widehat r(\xi)$. Robust policy evaluation asks for $\inf_{\xi\in\Xi}p_0^\top v(\xi)$.

Fix $\pi$. The affine approximate policy evaluation problem restricts reward to-go functions to affine maps $\vartheta(\xi)=w+W\xi$:

$$\sup_{w,W}\Big\{\inf_{\xi\in\Xi}p_0^\top(w+W\xi) : w+W\xi\le\widehat r(\xi)+\lambda\widehat P(\xi)(w+W\xi)\ \ \forall\xi\in\Xi\Big\}. \tag{19}$$

The semidefinite program (20) maximizes $\tau$ over $(\tau,w,W,\gamma,\Gamma)$ with $\gamma\ge0$ and $\Gamma\ge0$, subject to $(1+q)\times(1+q)$ linear matrix inequalities. Constraint (20b) involves $p_0^\top w-\tau$, $W^\top p_0$ and the matrices $Q_l=\big[\begin{smallmatrix}\omega_l & \frac12 o_l^\top\\ \frac12 o_l & O_l\end{smallmatrix}\big]$. Constraints (20c), one per state, involve $k_{sa}$, $K_{sa}$, $r_{sa}=(r(s,a,s'))_{s'}$, $w$, $W$ and $Q_l$.

Formalization targets

Goal: Theorem 3.8

Let $(\tau^*,w^*,W^*,\gamma^*,\Gamma^*)$ be an optimal solution of (20).

• If $L=1$, then $\tau^*$ equals the supremum of (19), and $\vartheta^*(\xi)=w^*+W^*\xi$ is feasible and optimal in (19).
• If $L>1$, then $\vartheta^*$ is feasible in (19), $\tau^*$ is a lower bound on the supremum of (19), and

$$\inf_{\xi\in\Xi}p_0^\top(w^*+W^*\xi)=\tau^*.$$

The theorem takes an optimal solution of (20) as given; it does not assert that (20) has one.

Milestones

1. Proposition 3.1 (c): every sub-solution $w\le\widehat r(\xi)+\lambda\widehat P(\xi)w$ lies below $v(\xi)$.
2. Every feasible $(w,W)$ of (19) satisfies $w+W\xi\le\bar r e/(1-\lambda)$ on $\Xi$, where $\bar r=\max r$.
3. Problem (19) is solvable.
4. Proposition 3.7 (17), the approximate S-lemma: if some $\gamma\ge 0$ makes $\big[\begin{smallmatrix}\sigma & \frac12 s^\top\\ \frac12 s & S\end{smallmatrix}\big]-\sum_l\gamma_lQ_l\succeq0$, then $\xi^\top S\xi+s^\top\xi+\sigma\ge0$ on $\Xi$.
5. The reverse implication of 4 when $S\succeq 0$.
6. The reverse implication of 4 when $L=1$: the published S-procedure, reused here.
7. The constraint $\tau\le p_0^\top(w+W\xi)$ on $\Xi$ is equivalent to (20b).
8. Constraint (20c) at $s$ implies the semi-infinite feasibility constraint of (19) at $s$, with equivalence when $L=1$.

Significance

When the ambiguity set is not rectangular, the robust value of a policy cannot be approximated efficiently in general. Theorem 3.8 gives a certified lower bound $\tau^*$ on it, computable by a semidefinite program of size polynomial in $|\mathcal S|$, $|\mathcal A|$, $q$ and $L$. Proposition 3.1 (c) makes (19) a restriction of the exact evaluation problem. For $L=1$, for example an ellipsoidal confidence region for $\xi$, the bound is the best affine one. The paper uses the theorem to compare policies under non-rectangular ambiguity, and in Proposition 3.10 to show that the bound is tight for s-rectangular sets.

On the formal side, the theorems are proved in the paper, and none of them, nor Proposition 3.7, has been formalized before. The platform has the exact S-procedure for one constraint, reused here, and other S-lemma variants in other settings. It has no approximate S-lemma for several concave quadratic constraints, no convex-Farkas argument for $S\succeq 0$, and no robust MDP with an affine parametrization. A completed mission would give a machine-checked SDP reformulation of a semi-infinite constraint in a dynamic programming setting.

Difficulty

Each direction rests on a different fact. The step from (20) to (19) is the elementary direction of the S-lemma, applied state by state and then combined with the objective's epigraph constraint. Showing that the bound is attained for $L=1$ needs four further facts:

• Problem (19) has an optimal solution. Its feasible region is unbounded (adding a constant $c\le0$ to $w$ preserves feasibility), so attainment needs the uniform bound of milestone 2 and a Slater ball inside $\Xi$.
• The objective's epigraph constraint $\tau\le p_0^\top(w+W\xi)$ on $\Xi$ and (20b) are exactly equivalent for every $L$, by convex Farkas (milestone 5).
• (20c) is exact for $L=1$, by the lossless S-procedure.
• The lower-right block $\lambda K_{sa}^\top W$ of (20c) is not symmetric.

A tempting shortcut is to treat (20c) as an ordinary positive semidefinite constraint on a symmetric matrix. That is wrong here: the matrix is not symmetric, and only its quadratic form carries meaning.

Formalization scope

Everything is finite-dimensional, and no measure theory is used.

• Types. States and actions are nonempty finite types. A policy is $\pi:\mathcal S\to\mathcal A\to\mathbb R$ with each $\pi(s)$ a probability vector (the published IsPolicy). $\widehat P$ and $\widehat r$ are built from the published InducedTransition and InducedReward.
• Reward to-go. $v$ is defined by the matrix-power series (8). The paper defines it as an expectation (5) and cites that (5) equals (8).
• The set $\Xi$. It is the set defined by the data $(O_l,o_l,\omega_l)$, with $\omega_l$ indexed by $l$; the page prints $\omega$ without the index in (3b). Boundedness, the Slater point and $O_l\preceq0$ (as PosSemidef of $-O_l$) are hypotheses.
• Problem (19). Affine $\vartheta$ is encoded as $(w,W)$, the paper's own (21). The objective is an infimum over the subtype $\Xi$, which is attained because $\Xi$ is nonempty and compact. "The supremum of (19)" is the greatest element, or every upper bound, of the set of feasible objective values.
• Block matrices. They have index type Unit ⊕ Fin q, with the scalar entry first. "$A\succeq0$" means $x^\top Ax\ge0$ for all $x$. This agrees with positive semidefiniteness on symmetric matrices and is the only faithful reading for (20c). Encoding (20c) with Mathlib's PosSemidef would make (20) infeasible and the goal vacuous, which is ruled out here. A verification instance with $|\mathcal S|=2$, $q=L=1$ shows that the standing hypotheses hold and that $(0,0,0,0,0)$ is feasible in (20).
• The S-procedure reference. It puts the scalar entry last and uses the opposite sign convention. Applying it to (17) for $L=1$ takes a permutation congruence and negation.

Welcome contributions include:

• the approximate S-lemma and the convex Farkas theorem of the alternative for several quadratic constraints, both reusable well beyond this mission;
• Proposition 3.1 (c) (the comparison principle for discounted Markov reward processes);
• compactness and attainment arguments for semi-infinite linear programs over $\Xi$.

Selected references

• W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov Decision Processes, Mathematics of Operations Research 38(1), 2013; preprint Optimization Online 2610, revision of February 9, 2012. https://doi.org/10.1287/moor.1120.0566
• A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. https://doi.org/10.1287/moor.1040.0129
• D. Kuhn, W. Wiesemann, A. Georghiou, Primal and dual linear decision rules in stochastic and robust optimization, Mathematical Programming 130(1), 2011. https://doi.org/10.1007/s10107-009-0331-4
• I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49(3), 2007. https://doi.org/10.1137/S003614450444614X
• L. Vandenberghe, S. Boyd, Semidefinite programming, SIAM Review 38(1), 1996. https://doi.org/10.1137/1038003
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

At a busy airport the runway is the bottleneck, and the order in which aircraft land or take off determines how much of its capacity is used. Wake turbulence forces a minimum time between consecutive operations that depends on the weight classes of the leading and trailing aircraft, so reordering a first-come-first-served (FCFS) queue can increase throughput or reduce delay. Controllers cannot reorder freely: constrained position shifting (CPS), introduced by Dear (1976, MIT Flight Transportation Laboratory Report R76-9), allows each aircraft to move at most $k$ positions from its FCFS position, which keeps the sequence fair and predictable.

Balakrishnan and Chandran (Oper. Res. 58(6), 2010) cast CPS scheduling as dynamic programming on a layered network whose paths are the admissible sequences. For makespan and total delay the separations are assumed to satisfy the triangle inequality, which holds for arrivals only or departures only. When arrivals and departures share a runway it fails: in the separation table of the paper, a heavy arrival followed by a departure and then a small arrival needs only $75+60=135$ seconds through the departure, while the direct requirement is $196$ seconds. Section 6.2 of the paper handles this case for arbitrary per-aircraft cost functions, by expanding the network state. This mission formalizes that construction and its correctness.

Setting

Time is discrete: all data are integer multiples of one period. There are $n$ aircraft labelled in FCFS order, a maximum shift $k$, a minimum separation $\delta_{ab}\in\mathbb N$ between a leading aircraft $a$ and a trailing aircraft $b$, a time window $[e_a,l_a]$ for each aircraft, a finite set of precedence pairs $(x,y)$ ($x$ lands before $y$), and a cost $c_a(t)$ of landing aircraft $a$ at period $t$.

A $k$-CPS sequence is a bijection $\sigma$ from positions to aircraft with $|\sigma(p)-p|\le k$. A feasible schedule is a $k$-CPS sequence with integer landing times $t_p$ such that precedence pairs are respected, $e_{\sigma(p)}\le t_p\le l_{\sigma(p)}$, and

$$t_q-t_p\ \ge\ \delta_{\sigma(p)\sigma(q)}\qquad\text{for all positions } p<q .$$

Its cost is $\sum_p c_{\sigma(p)}(t_p)$.

The CPS network has stages $1,\dots,n$. A node of stage $p$ is a list of $\min\{2k+1,p\}$ distinct aircraft that may occupy positions $p-\min\{2k+1,p\}+1,\dots,p$; its last aircraft is the final aircraft $\mathrm{fin}(i)$. An arc joins consecutive stages when the lists overlap. Removing the nodes that violate a precedence pair gives the network $G$. For a node $i$, $\Gamma(i)$ is the set of integer times in the window of $\mathrm{fin}(i)$.

The modified network of §6.2 has nodes $(i,t,d)$: a node $i$ of $G$, a time $t\in\Gamma(i)$, and a lower bound $d$ on the separation between $\mathrm{fin}(i)$ and its predecessor, with $d=0$ at stage $1$ and otherwise $d^{\min}_i\le d\le d^{\max}_i$, where, for the penultimate and final aircraft $a,b$ of $i$,

$$d^{\min}_i=\delta_{ab},\qquad d^{\max}_i=\max\Big\{\max_{j:\,i\in P(j)}\big(\delta_{a,\mathrm{fin}(j)}-\delta_{b,\mathrm{fin}(j)}\big),\ d^{\min}_i\Big\}.$$

An arc $(i,t',d')\to(j,t'',d'')$ requires an arc $(i,j)$ of $G$, $t''-t'\ge d^{\min}_j$, $d''=\min\{t''-t',d^{\max}_j\}$, and $d'+t''-t'$ at least the separation between the penultimate aircraft of $i$ and $\mathrm{fin}(j)$. Arcs entering $(i,t,d)$ cost $c_{\mathrm{fin}(i)}(t)$.

Formalization targets

Goal: minimum-cost paths are optimal schedules

Under $k\ge 1$, positive costs, and the polygon inequalities of three or more hops (below):

1. a feasible schedule exists if and only if the modified network has a source-sink path;

$$\min_{(\sigma,t)\ \text{feasible}}\ \sum_p c_{\sigma(p)}(t_p)\;=\;\min_{\text{paths}}\ \sum_{p=1}^n c_{\mathrm{fin}(i_p)}(t_p),$$

each minimum existing exactly when the other does; 3. every minimum-cost path represents a feasible, optimal schedule.

Milestones

• Theorem 1 (with §3.1): the $k$-CPS sequences respecting precedence are exactly the sequences of source-sink paths of $G$.
• Lemma 5: every source-sink path of the modified network represents a feasible schedule.
• Lemma 6: every feasible schedule (in particular an optimal one) is represented by a source-sink path.
• Remark 1: under the triangle inequality, $d^{\min}_i=d^{\max}_i=\delta_{ab}$.
• Lemma 4: under the triangle inequality, a feasible schedule exists if and only if the simpler discrete-time network of §6.1.2, with nodes $(i,t)$, has a source-sink path.

Significance

The result turns a scheduling problem with arbitrary separable costs, time windows, precedence and non-metric separations into a shortest-path problem whose size is polynomial in $n$ for fixed $k$ and in the number of periods. It covers mixed arrival–departure operations, where the triangle inequality genuinely fails, and it is the basis of the paper's §7.1 algorithm for coupled arrivals and departures.

The paper proves Lemmas 5 and 6 in a few paragraphs and omits the proof of Lemma 4. No machine-checked version of the CPS network or of these lemmas exists. A formal development pins down the boundary cases the prose passes over (the first two stages, the last stage where $d^{\max}$ has no successors), and it makes explicit an assumption the prose leaves unstated: Lemma 5 needs the polygon inequalities, not only the two-step check in its proof.

Difficulty

The obvious argument checks separations only between consecutive aircraft, which is what the network of §6.1.2 does. Without the triangle inequality this misses aircraft two positions apart. The state $d$ repairs that but is capped at $d^{\max}$, so one must show that the cap loses nothing: a capped value still certifies the separation to the next aircraft. That uses the definition of $d^{\max}$ over the successors of a node in $G$, so the proof depends on how the network is pruned. Separations three or more positions apart are not tracked at all and rely on the polygon inequalities. Relating network paths to sequences (Theorem 1) requires reasoning about overlapping windows of the sequence and about the precedence pruning rule.

Formalization scope

Aircraft and positions are $0$-based (Fin n), stages $1$-based, and $n\ge 1$ (NeZero n). Times, windows and separations are natural numbers (periods); $d$, $d^{\min}$, $d^{\max}$ and time differences are integers, since $d^{\max}$ involves differences of separations that can be negative. Separation is required for all pairs of aircraft, not only consecutive ones. Minima are stated with IsLeast on sets of costs, never with a real infimum.

The following readings of the paper are committed:

• Polygon inequalities. Lemma 5 and the goal assume that for every chain $x_0,\dots,x_m$ of $m\ge 3$ hops between distinct aircraft, $\delta_{x_0x_m}\le\sum_i\delta_{x_ix_{i+1}}$. Without this hypothesis Lemma 5 is false: there are small instances violating the quadrilateral inequality whose minimum-cost path is infeasible. §7 of the paper asserts these inequalities for mixed operations; this mission states them as a hypothesis and makes no claim about the paper's Table 1.
• $\Gamma(i)$ is the full time window, not the narrowed set of §6.1.3, whose justification needs nondecreasing costs. With the full window Lemma 6 holds for every feasible schedule and arbitrary costs; it is stated in that stronger form.
• $k\ge 1$, so that every node beyond stage $1$ has a penultimate aircraft. Arc condition 4 is not imposed on arcs leaving stage $1$.
• Arc cost $c(i,t)$ of the paper is read as $c_{\mathrm{fin}(i)}(t)$.
• Precedence pruning uses the printed rule of §3.1; nodes unreachable from the source or the sink are not removed (this does not change the set of source-sink paths).
• Running times (§6.1.4, §6.3) and the bound $\lambda$ of recursion (4) are not formalized.

A trivializing formalization is ruled out: the networks are concrete definitions computed from the instance, not arbitrary graphs pinned by hypotheses, and the goal compares two independently defined minima, so it cannot hold by an empty feasible set or an unconstrained optimum.

A complete development needs basic list combinatorics (windows of a sequence, overlap of consecutive windows), the correspondence between bijections and paths, and finite minimization. The CPS network layer is shared with the other missions of this series and is reusable for any CPS scheduling result. Contributions on Theorem 1 alone are welcome, as it is independent of the time-expanded networks.

Selected references

• H. Balakrishnan, B. G. Chandran, Algorithms for Scheduling Runway Operations Under Constrained Position Shifting, Operations Research 58(6), 1650–1665, 2010. https://doi.org/10.1287/opre.1100.0869
• R. G. Dear, The Dynamic Scheduling of Aircraft in the Near Terminal Area, MIT Flight Transportation Laboratory Report R76-9, Massachusetts Institute of Technology, 1976 (as cited in the paper above).
• H. Lee, Tradeoff Evaluation of Scheduling Algorithms for Terminal-Area Air Traffic Control, Master's thesis, Massachusetts Institute of Technology, 2008 (source of the separation table; as cited in the paper above).

Motivation

A Markov decision process (MDP) is evaluated by solving a linear fixed-point equation built from its transition probabilities. In practice those probabilities are rarely known exactly: they are estimated from data, elicited from experts, or obtained by aggregating the states of a larger model, and each estimate comes with an error band. Givan, Leach and Dean (Bounded-parameter Markov decision processes, Artificial Intelligence, 2000) replace each transition probability by a closed interval and ask what can still be said about the value of a policy. Their answer for a fixed policy is an interval value: at each state, the smallest and the largest expected discounted reward the policy can obtain over all exact MDPs consistent with the intervals.

The same model reappears under other names. Robust MDPs with rectangular uncertainty sets (Nilim and El Ghaoui, Operations Research, 2005; Iyengar, Mathematics of Operations Research, 2005) take the pessimistic end of the interval, and optimistic model-based reinforcement learning (for example UCRL-type algorithms) takes the optimistic end over a confidence set. Interval transition models are also used to bound the error of state aggregation. In all of these, the basic computational question is how to evaluate a fixed policy against a whole family of MDPs at once.

Setting

Fix a finite set $Q$ of states and a finite nonempty set $A$ of actions. An exact MDP $M=\langle Q,A,F,R\rangle$ has transition probabilities $F_{pq}(\alpha)$, each row $q\mapsto F_{pq}(\alpha)$ a probability distribution, a reward $R(q)\in\mathbb R$ per state, and a discount rate $0\le\gamma<1$. A policy is a map $\pi:Q\to A$. Its value function $V_{M,\pi}$ is the expected discounted cumulative reward of the Markov chain with transition matrix $F_{pq}(\pi(p))$:

$$V_{M,\pi}(p)=\sum_{t\ge0}\gamma^t\,(P_\pi^tR)(p),\qquad P_\pi(p,q)=F_{pq}(\pi(p)).$$

On the space $\overline V$ of value functions $v:Q\to\mathbb R$, with the sup norm $\|v\|=\max_q|v(q)|$, the value-iteration operator is $VI_{M,\pi}(v)(p)=R(p)+\gamma\sum_{q}F_{pq}(\pi(p))\,v(q)$, and $VI_{M,\alpha}$ is the same with the action $\alpha$ in place of $\pi(p)$. An operator $T$ on $\overline V$ is a contraction mapping if $\|Tv-Tu\|\le\lambda\|v-u\|$ for all $u,v$ and some $0\le\lambda<1$.

A bounded-parameter MDP (BMDP) $M_\updownarrow$ gives intervals $[F_{\downarrow pq}(\alpha),F_{\uparrow pq}(\alpha)]\subseteq[0,1]$ with $\sum_qF_{\downarrow pq}(\alpha)\le1\le\sum_qF_{\uparrow pq}(\alpha)$, a reward $R$ and a discount rate $\gamma$. An exact MDP belongs to $M_\updownarrow$ if it has the same $R$ and $\gamma$ and every transition probability lies in its interval. The interval value of a policy $\pi$ (Definition 3) is

$$V_{\updownarrow\pi}(q)=\Big[V_{\downarrow\pi}(q),V_{\uparrow\pi}(q)\Big]=\Big[\min_{M\in M_\updownarrow}V_{M,\pi}(q),\ \max_{M\in M_\updownarrow}V_{M,\pi}(q)\Big].$$

Interval policy evaluation acts on an interval value function $V_\updownarrow=[V_\downarrow,V_\uparrow]$ by

$$IVI_{\updownarrow\pi}(V_\updownarrow)(p)=\Big[\min_{M\in M_\updownarrow}VI_{M,\pi}(V_\downarrow)(p),\ \max_{M\in M_\updownarrow}VI_{M,\pi}(V_\uparrow)(p)\Big],$$

with lower and upper bound maps $IVI_{\downarrow\pi},IVI_{\uparrow\pi}:\overline V\to\overline V$.

For the optional part, interval value iteration adds a maximization over actions: $IVI_{\updownarrow opt}$ and $IVI_{\updownarrow pes}$ take, at each state, the largest of the candidate intervals $\big[\min_MVI_{M,\alpha}(V_\downarrow)(p),\max_MVI_{M,\alpha}(V_\uparrow)(p)\big]$ for the lexicographic orders $\le_{opt}$ (upper end first) and $\le_{pes}$ (lower end first). For a value function $V$, $\rho_V(p)$ and $\sigma_V(p)$ are the actions maximizing $\max_MVI_{M,\alpha}(V)(p)$ and $\min_MVI_{M,\alpha}(V)(p)$, and $IVI_{\downarrow opt,V}(V')=IVI_{\downarrow opt}([V',V])$, $IVI_{\uparrow pes,V}(V')=IVI_{\uparrow pes}([V,V'])$.

Formalization targets

Goal: convergence of interval policy evaluation (Section 5.1, p. 22)

For every BMDP, every policy $\pi$, and every interval value function $V_{\updownarrow0}=[V_{\downarrow0},V_{\uparrow0}]$ with $V_{\downarrow0}\le V_{\uparrow0}$,

$$\lim_{n\to\infty}IVI_{\updownarrow\pi}^{\,n}(V_{\updownarrow0})=V_{\updownarrow\pi}.$$

The limit is the interval value of Definition 3, an extremum over infinitely many MDPs; nothing about the starting point is assumed beyond its being an interval value function.

Milestones on the goal's path

• Theorem 10 (p. 21): $IVI_{\downarrow\pi}$ and $IVI_{\uparrow\pi}$ are contraction mappings on $\overline V$.
• Theorem 11 (p. 22): $IVI_{\downarrow\pi}(V_{\downarrow\pi})=V_{\downarrow\pi}$, $IVI_{\uparrow\pi}(V_{\uparrow\pi})=V_{\uparrow\pi}$, and hence $IVI_{\updownarrow\pi}(V_{\updownarrow\pi})=V_{\updownarrow\pi}$.

Further results on interval value iteration (Section 5.2)

• Lemma 4 (p. 25): $IVI_{\downarrow opt,V}(V')(p)=\max_{\alpha\in\rho_V(p)}\min_{M}VI_{M,\alpha}(V')(p)$ and $IVI_{\uparrow pes,V}(V')(p)=\max_{\alpha\in\sigma_V(p)}\max_{M}VI_{M,\alpha}(V')(p)$.
• Theorem 13(a) (p. 25): $IVI_{\uparrow opt}$ and $IVI_{\downarrow pes}$ are contraction mappings.
• Theorem 13(b) (p. 25): for every value function $V$, $IVI_{\downarrow opt,V}$ and $IVI_{\uparrow pes,V}$ are contraction mappings.

Significance

The result. The interval value is defined as a minimum and a maximum over a continuum of MDPs, and there is no a priori reason it should be computable by a dynamic program. The goal says it is: one operator, whose per-state step is a small linear program over a box intersected with a simplex, iterated from any start, converges to both ends of the interval simultaneously. The pessimistic end is the robust value of the policy under rectangular uncertainty, so the goal is also a policy-evaluation theorem for interval-rectangular robust MDPs; the optimistic end is the value used by optimism-based exploration. Theorem 11 is the bridge between the "game" definition (nature picks the MDP) and the fixed-point characterization; Theorem 13 is the corresponding first step for the optimal interval values of the companion mission.

Formalizing it. The results are proved in the paper (2000), with Theorem 11 relying on the existence of a single member MDP that is $\pi$-minimizing at every state simultaneously (the paper's Theorem 7). No machine-checked version of the BMDP model or of these results is known. Nearby statements formalized elsewhere concern other models: robust MDPs with costs and general row sets, and optimistic Bellman equations over compact confidence sets. This mission produces the BMDP model and its interval operators, the contraction and fixed-point theorems, and the convergence theorem, all stated against the member-MDP definition of $V_{\updownarrow\pi}$.

Difficulty

The contraction estimates (Theorems 10 and 13) follow the familiar pattern for Bellman operators, with the extra point that the minimum or maximum over the infinite family $M_\updownarrow$ must be attained. The real difficulty is Theorem 11. The obvious argument compares $V_{\downarrow\pi}(q)$ with $VI_{M,\pi}(V_{\downarrow\pi})(q)$ state by state; but $V_{\downarrow\pi}(q)$ is a minimum taken separately at each state, possibly by a different MDP at each state, and $V_{\downarrow\pi}$ need not a priori be the value function of any single member MDP. Without a member MDP that is minimizing at all states at once, the inequality $IVI_{\downarrow\pi}(V_{\downarrow\pi})\ge V_{\downarrow\pi}$ does not follow. Establishing that simultaneous minimizer is the central step.

Formalization scope

All statements live in the namespace BoundedParamMDP.IntervalEval. The exact MDP, the BMDP, its member MDPs, $V_{M,\pi}$, $VI_{M,\pi}$, $VI_{M,\alpha}$ and Definition 3's $V_{\downarrow\pi}$, $V_{\uparrow\pi}$ are the shared definitions BoundedParamMDP.Optimal.MDP and BoundedParamMDP.Optimal.BMDP used by the companion mission, so its theorems apply to the same objects. Conventions:

• $Q$ and $A$ are finite types, $A$ is nonempty; $Q$ may be empty (every statement then holds for the paper's own reasons). Policies are deterministic and stationary, Q → A.
• An exact MDP is a structure with F p α q $=F_{pq}(\alpha)$, rows nonnegative and summing to $1$, a state reward R, and the discount rate $0\le\gamma<1$ as a field. Rewards are tight (the paper's footnote 3): members share the BMDP's R and γ.
• $V_{M,\pi}$ is the discounted series $\sum_t\gamma^t P_\pi^tR$, not a solution chosen from the Bellman equation.
• Minima and maxima over $M_\updownarrow$ are the real infimum and supremum over the nonempty subtype Member B; all quantities are bounded, so these are the genuine values (and attained, by the paper's Lemma 1).
• An interval value function is a pair (V↓, V↑) of functions Q → ℝ. The operators are defined on all pairs; the goal assumes $V_{\downarrow0}\le V_{\uparrow0}$ as the paper's interval notion, though the conclusion does not need it.
• The norm is Mathlib's norm on Q → ℝ (the sup norm (4)); convergence of pairs is in the product topology. A contraction mapping is "there exists $\lambda\in[0,1)$", as on p. 6; the modulus is not fixed to $\gamma$.
• $\max_{\alpha,\le_{opt}}$ is the supremum over the finite action set in the lexicographic order on (upper end, lower end); $\le_{pes}$ uses (lower end, upper end). $\rho_V(p)$, $\sigma_V(p)$ are sets of actions.
• Theorem 13(a) is stated for $IVI_{\uparrow opt}$ as the upper end of $IVI_{\updownarrow opt}$ with arbitrary lower inputs on both sides: the bound by $\lambda\|U'-U\|$ includes the independence from the lower input that the paper uses (p. 23) to regard $IVI_{\uparrow opt}$ as a map on $\overline V$.
• Lemma 4's second line is printed with $\min_{M}$; the evident reading $\max_M$ (eq. (29), proof of Theorem 13(b), p. 47) is stated.

A trivializing formalization is excluded: the limit in the goal is Definition 3's infimum and supremum over member MDPs, not the fixed point of $IVI_{\updownarrow\pi}$, so the goal is not Banach's theorem alone; and the member type is nonempty for every BMDP, so the infima and suprema are not the junk value $0$.

The proof of Theorem 11 uses the paper's Lemma 1 (attainment in the order-maximizing family), Theorem 3 ($V_{M,\pi}$ is the unique fixed point of $VI_{M,\pi}$), Theorem 6 (comparison principle) and Theorem 7 (existence of $\pi$-minimizing and $\pi$-maximizing MDPs). These are milestones of the companion mission Bounded-parameter Markov Decision Processes 1 and are not restated here. The Banach fixed-point theorem is Mathlib's ContractingWith. Contributions welcome: proofs of the milestones, a reusable lemma on the attained minimum of a linear function over a box intersected with the simplex, and the order-maximizing construction itself.

Selected references

• R. Givan, S. Leach, T. Dean, Bounded-parameter Markov decision processes, Artificial Intelligence 122 (2000). https://doi.org/10.1016/S0004-3702(00)00047-3
• A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. https://doi.org/10.1287/moor.1040.0129
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887