The Swiss Army Formula of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds the calculus that the rest of the book runs on. Its subject is the relation between two ways of looking at the same stationary system: from a clock fixed in time, and from a customer arriving into it. The two are not the same — the interval a random instant falls into is longer than a typical interval, a fact every queueing student meets as the inspection paradox — and the object that makes the difference precise is the Palm probability P⁰_N.

The chapter defines P⁰_N by the Matthes definition in terms of counting,

λ t P⁰_N(A) = E[ Σ_{n ∈ ℤ} 1_A(θ_{T_n}) 1_{(0,t]}(T_n) ],                          (1.2.1)

and everything else is a theorem about it. That ordering is deliberate here too: P⁰_N is carried in the formalization as a predicate satisfying (1.2.1), not as a measure constructed to make Mecke's formula true. If it were the latter, Mecke's formula would be a definition and the inversion formula and the goal theorem would inherit that emptiness.

From (1.2.1) the chapter derives, in order: that P⁰_N is invariant under the point shift (1.2.16); Mecke's formula (1.2.17), which the literature also knows as the generalized Campbell formula; the inversion formula of Ryll-Nardzewski and Slivnyak (1.2.25), which runs back from P⁰_N to P; the mean-value formulas (1.3.2)–(1.3.3); the Neveu exchange formula (1.3.4), which relates two point processes stationary for the same flow; and the Miyazawa rate conservation principle (1.3.10), which balances the drift of a process between its jumps against the rate at which it jumps.

The goal

§1.3.7 then collects all of them into one identity. Its name is the book's own:

Depending on which blade is selected, a Swiss army knife transforms itself into various useful tools. The formula obtained in this subsection is called the Swiss army formula of Palm calculus because it contains the main formulas of this theory, as well as some new ones.

Theorem 1.3.1 (p.29). For arrivals {T_n} with counting measure A and intensity λ_A, departures {τ_n} with counting measure D — not assumed ordered — sojourn times W_n = τ_n − T_n ≥ 0 forming a sequence of marks of A, the number in system {X(t)} with X(b) − X(a) = A((a,b]) − D((a,b]), a non-decreasing corlol integrator {B(t)} and a non-negative process {Z(t)}, all compatible with a measurable flow under which P is invariant:

λ_A E⁰_A [ ∫_(0,W_0] Z(s) dB(s) ] = (1/t) E [ ∫_(0,t] X(s−) Z(s) dB(s) ].              (1.3.28)

Selecting the blade Z ≡ 1, B(t) = t turns it into λ_A E⁰_A[W_0] = E[X(0)] — Little's law, here in its full stationary-ergodic form rather than as a deterministic sample-path identity. Other choices give the inversion formula, the Miyazawa conservation principle and the rate conservation law.

The local meaning of P⁰_N

One milestone stands slightly apart. Theorem 1.5.1 (p.45) is what licenses the whole reading of P⁰_N as "what an arriving customer sees":

lim_{t→0} sup_{A ∈ F} | P⁰_N(A) − P(θ_{T_1} ∈ A | T_1 ≤ t) | = 0.                       (1.5.3)

The supremum is inside the limit. The convergence is uniform over every measurable event, which is what Dobrushin's estimate of §1.5.1 buys and what a pointwise limit would not give.

What this mission provides

Nothing in this chapter exists on the platform or in Mathlib: not stationary marked point processes, not Palm probability, not the Campbell measure. Four of the five missions in this series import the vocabulary built here, and the two definition items — the substrate of §§1.1–1.2 and the setting of §1.3.7 — are as much of the deliverable as the theorems are.

Formalization scope

• The flow {θ_t} is a one-parameter group with (t, ω) ↦ θ_t ω jointly measurable (p.5 (a)); a point process is its strictly increasing points {T_n}_{n ∈ ℤ} with T_0 ≤ 0 < T_1, infinitely many on each side (Hypothesis 1.1.1), with finite non-null intensity λ = E[N((0,1])].
• P⁰_N is characterized by (1.2.1) for every t > 0, which determines it uniquely; nothing is axiomatized. A formalization that introduced P⁰_N as any measure satisfying Mecke's formula would make the milestones and the goal trivial and is ruled out.
• Every "for all non-negative measurable" formula (Mecke, inversion, mean-value, Neveu, Wald, the goal) is stated in [0, ∞] with lower Lebesgue integrals, for all such functions, not only bounded or integrable ones.
• Three hypotheses the book uses without listing them are explicit: the Swiss army formula assumes the integrator {B(t)} is θ_t-compatible (the proof uses it, and without it the identity fails); it is stated for t > 0, the only values at which 1/t and (0, t] give it content; and the Miyazawa principle assumes Y'(0) ∈ L¹(P), which its E[Y'(0)] presupposes.
• Theorem 1.5.1 keeps the supremum over all events inside the limit (one δ for every A).

Motivation

Countable-state Markov chains are the standard model of queues with unbounded buffers, but any numerical computation of their long-run behaviour works on a finite state space. The usual remedy is truncation: restrict the chain to a finite set $S_N$ and redistribute the probability of leaving $S_N$ back into it. Whether the steady state probabilities and average costs of the truncated chains converge to those of the original chain depends on how that probability is redistributed. Gibson and Seneta studied this question for the stationary distributions of chains without costs (Gibson and Seneta, J. Appl. Prob., 1987). Sennott extended it to chains with costs and expected first passage costs (Sennott, Adv. Appl. Prob. 29, 1997; ZOR Math. Meth. Oper. Res. 45, 1997), and used it as the basis of the approximating sequence method for average-cost Markov decision chains (Sennott, 1999, Chapter 8). This mission covers Appendix C, Sections C.4–C.5 of the 1999 book, the Markov-chain results that the book's average-cost approximation theorems use.

Setting

A Markov chain with costs $\Gamma$ on a denumerable state space $S$ has transition probabilities $P_{ij}$ with $\sum_jP_{ij}=1$ and a finite nonnegative cost $C(i)$ at each state. For a set $G\subseteq S$ and a start $i$, $T_{iG}\ge 1$ is the first passage time to $G$. The taboo probability ${}_GP^{(t)}_{ik}$ is the probability of moving from $i$ to $k$ in $t$ steps with no intermediate state in $G$. The expected visits ${}_Gu_{ik}$ count the visits to $k$ at times $0\le t<T_{iG}$. The mean first passage time is $m_{iG}=E[T_{iG}]$, infinite when $G$ is missed with positive probability. The first passage cost is $c_{iG}=E\big[\sum_{t<T_{iG}}C(X_t)\big]$. A state $i$ is positive recurrent when $m_{ii}<\infty$, and the steady state probability is $\pi_i=m_{ii}^{-1}$. On a positive recurrent class $R$ the average cost is $J_R=\sum_{j\in R}\pi_jC(j)$. The chain is $z$ standard when $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$. Such a chain has one positive recurrent class $R\ni z$ with $J_R<\infty$, and every other state is transient.

An approximating sequence (AS) $(\Gamma_N)_{N\ge N_0}$ consists of increasing nonempty finite sets $S_N$ with $\bigcup_NS_N=S$ and, for each $N$, a chain $\Gamma_N$ on $S_N$ with the same costs and transition probabilities $P_{ij}(N)\to P_{ij}$. The quantities of $\Gamma_N$ are written $m_{iG}(N)$, $c_{iG}(N)$, $\pi_i(N)$ and $J(i)(N)$. An AS is conforming (for a $z$ standard $\Gamma$) if, for large $N$, $\Gamma_N$ is unichain with $z$ in its positive recurrent class, and $m_{iz}(N)\to m_{iz}$ and $c_{iz}(N)\to c_{iz}$ for all $i$. It is conforming on $R$ if $\pi_i(N)\to\pi_i$ and $J(i)(N)\to J_R$ on $R$.

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the probability of each excluded target $r\notin S_N$ according to an augmentation distribution $q_\cdot(i,r,N)$ on $S_N$:

$$P_{ij}(N)=P_{ij}+\sum_{r\in S-S_N}P_{ir}\,q_j(i,r,N),\qquad j\in S_N.$$

It sends excess probability to $G$ if every $q_\cdot(i,r,N)$ is concentrated on $G$.

Formalization targets

Goal: Proposition C.5.2

For a $z$ standard chain $\Gamma$ and a finite nonempty $G\subseteq S$,

$$\text{every ATAS that sends excess probability to } G \text{ is conforming},$$

and if $G\subseteq R$ it is also conforming on $R$. No rate of convergence and no constants are involved, and $G$ need not contain $z$.

Milestones

1. Proposition C.4.2: for fixed $t$, $\lim_N{}_GP^{(t)}_{ik}(N)={}_GP^{(t)}_{ik}$; also $\liminf_N{}_Gu_{ik}(N)\ge{}_Gu_{ik}$ and $\liminf_Nm_{iG}(N)\ge m_{iG}$.
2. Proposition C.4.3: $\pi_i(N)\to0$ off the positive recurrent states, and along subsequences $\pi_i(N_s)\to b\pi_i$ on a class, with $0\le b\le1$.
3. Proposition C.4.5: $\liminf_Nc_{iG}(N)\ge c_{iG}$.
4. Proposition C.4.6: on a positive recurrent class, convergence of $\pi$, of $m_{zz}$ and of all $m_{iG}$ are equivalent. Given these, convergence of $J(i)$, of $c_{zz}$ and of all $c_{iG}$ are equivalent.
5. Proposition C.4.9: conformity implies $\pi_i(N)\to\pi_i$ for all $i$, and that the constant average costs $J(N)$ of $\Gamma_N$ converge to $J_R$.

Further results

6. Proposition C.5.3: an ATAS is conforming when, for $N\ge N^*$, the augmentation distributions satisfy $\sum_{j\ne z}q_j(i,r,N)m_{jz}\le m_{rz}$ and $\sum_{j\ne z}q_j(i,r,N)c_{jz}\le c_{rz}$.
7. Corollary C.5.4: for a $0$ standard chain on $\{0,1,2,\dots\}$ with an upper Hessenberg transition matrix, truncated to $S_N=\{0,\dots,N\}$ with the excess sent to $N$, the ATAS is conforming.

Significance

The result. Conformity is the hypothesis under which the book's approximating sequence method works for average-cost queueing control (Chapter 8). The method computes optimal policies for finite truncations and passes to the limit. That argument needs the first passage times and costs to a distinguished state to converge along the chains induced by fixed policies. Propositions C.5.2 and C.5.3 turn this analytic requirement into conditions on the truncation scheme that can be checked in practice: send the overflow to a fixed finite set, or to states from which reaching $z$ is no more expensive. Examples C.4.4 and C.4.7 of the book show that an arbitrary approximating sequence can fail. The limit of the steady state probabilities can be a strict multiple $b\pi$ with $b<1$. First passage costs can converge to the wrong value even when the steady state probabilities converge.

Formalizing it. The results are proved in the book, some in abbreviated form ("the proof for the costs is similar and is omitted"). The Prove2Me library had no statement on truncation or augmentation of countable Markov chains when this mission was drafted (September 2026). A formalization supplies the omitted cost arguments, makes the passage between $\liminf$ bounds and limits in $[0,\infty]$ explicit, and produces a reusable library of first passage quantities for countable chains.

Difficulty

The lower bounds of Propositions C.4.2 and C.4.5 are the routine part. The difficulty is the matching upper bound: in $\Gamma_N$, a first passage that leaves $S_N$ is restarted elsewhere, which can lengthen it without bound. Taking limits termwise in the first passage equation $m_{iz}(N)=1+\sum_{j\ne z}P_{ij}(N)m_{jz}(N)$ fails, because no dominating function is available and mass can escape to infinity. Example C.4.4 exhibits exactly this. Unichain structure is also not automatic: $\Gamma_N$ may have several recurrent classes, or a recurrent class not containing $z$, and ruling this out is part of the conclusion rather than an assumption.

Formalization scope

The Lean development works in SennottDP.ChainASM. A chain is a structure MC S with P : S → S → ℝ≥0∞, ∑' j, P i j = 1 and C : S → ℝ≥0. Theorems assume [Countable S] [Infinite S], matching the book's denumerable state space. Taboo probabilities, expected visits, $m_{iG}$, $c_{iG}$, $\pi_j=(m_{jj})^{-1}$ and $J_R=\sum_{j\in R}\pi_jC(j)$ are defined as sums in $[0,\infty]$. $m_{iG}=\sum_{t\ge0}P(T_{iG}>t)$ is infinite whenever $G$ is missed with positive probability. The average cost $J(i)$ is the $\limsup$ of the Cesàro cost averages.

An AS is a structure carrying $N_0$, the finite sets $S_N$ (as Finset S) and $P_{ij}(N)$. $\Gamma_N$ is built as an MC on the subtype of $S_N$, and a set $G$ is read in $\Gamma_N$ as $G\cap S_N$. Quantities of $\Gamma_N$ are lifted to functions of $N$ and of states of $S$ with the value $0$ where they are undefined ($N<N_0$ or a state outside $S_N$). For fixed states this affects finitely many $N$, and all statements are limits, $\liminf$s or eventual equalities. All convergence is in $[0,\infty]$. The conformity predicate includes the standing assumption that $\Gamma$ is $z$ standard. The positive recurrent class $R$ of a $z$ standard chain is the communicating class of $z$.

A trivializing formalization is excluded: the AS of Example C.4.4, whose positive recurrent class $\{N\}$ excludes $z=0$, is not conforming under these definitions. The ATAS predicate requires the augmentation distributions to be probability distributions and to reproduce $P_{ij}(N)$ exactly by (C.27).

A complete development needs first passage decompositions for countable chains, the renewal-reward identity $J_R=c_{zz}/m_{zz}$, and dominated and Fatou-type limit theorems for sums (the book's Appendix A). The first passage library and the lifted-quantity conventions can be reused by the average-cost approximation chapters. Contributions of intermediate lemmas are welcome, especially the finite-state unichain facts of Section C.3 and the identities of Propositions C.1.4 and C.2.2.

Proposition C.5.5 (lower Hessenberg chains, from Gibson and Seneta) is stated in the book without proof and without naming the distinguished state, and is not included.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, Sections C.4–C.5. https://doi.org/10.1002/9780470317037
• L. I. Sennott, "The computation of average optimal policies in denumerable state Markov decision chains", Advances in Applied Probability 29 (1997) 114–137 (cited in the book as Sennott 1997a).
• L. I. Sennott, "On computing average cost optimal policies with application to routing to parallel queues", ZOR Mathematical Methods of Operations Research 45 (1997) 45–62 (cited in the book as Sennott 1997b).
• D. Gibson and E. Seneta, "Augmented truncations of infinite stochastic matrices", Journal of Applied Probability (1987).

Motivation

The periodic-review inventory problem with a fixed ordering cost is one of the basic models of operations research. A firm reviews its stock once per period, may order at a cost $K$ per order plus a unit cost, and then faces a random demand; unmet demand is backlogged. Scarf (1960) and Iglehart (1963) showed that for this model an $(s, S)$ policy is optimal: order up to $S$ whenever the stock falls below $s$, and otherwise do nothing. That result tells a manager what shape a good policy has, but not which pair $(s, S)$ to use.

Veinott and Wagner, Computing Optimal (s, S) Inventory Policies (Management Science 11 (1965) 525–552), gave the first practical algorithm for computing an optimal pair when demand is discrete. The algorithm rests on a closed form, their Eq. (11), for the discounted cost of an arbitrary stationary $(s, S)$ policy, obtained by a renewal argument in their Section 3. The same closed form, in the undiscounted limit, is the classical expression of the long-run average cost of an $(s, S)$ policy used throughout inventory theory textbooks.

Timeline:

• 1958: Arrow, Karlin and Scarf collect the early dynamic inventory models.
• 1960: Scarf proves optimality of $(s, S)$ policies in the finite-horizon model via $K$-convexity.
• 1963: Iglehart extends optimality to the infinite-horizon model.
• 1965: Veinott and Wagner derive the renewal closed form (10)–(11) and the bounds and search procedure built on it.

Setting

Demands $\xi_1, \xi_2, \dots$ are independent random variables on $\{0, 1, 2, \dots\}$ with common distribution $\varphi$, $\varphi(k) = \Pr(\xi_t = k)$. Write $\varphi^i$ for the $i$-fold convolution of $\varphi$ ($\varphi^0$ is the point mass at $0$) and $\Phi^i(k) = \sum_{t=0}^{k}\varphi^i(t)$ for its distribution function, so $\Phi^0 \equiv 1$.

In period $t$ the stock before ordering is $X_t \in \mathbb Z$ and the stock after ordering is $Y_t \ge X_t$; then $X_{t+1} = Y_t - \xi_t$. With the unit purchase cost eliminated as in the paper's Eq. (2), the cost of period $t$ is $K\delta(Y_t - X_t) + G_\alpha(Y_t)$, where $K \ge 0$ is the set-up cost, $\delta(0) = 0$, $\delta(z) = 1$ for $z > 0$, and $G_\alpha : \mathbb Z \to \mathbb R$ is the one-period cost. Period $t$ is discounted by $\alpha^{t-1}$ with $0 \le \alpha < 1$.

A stationary $(s, S)$ policy, for integers $s \le S$, sets $Y_t = S$ if $X_t < s$ and $Y_t = X_t$ otherwise. Its total expected discounted cost from $X_1 = x$ is

$$f(x \mid s, S) = \sum_{t=1}^{\infty} \alpha^{t-1} E\bigl[K\delta(Y_t - X_t) + G_\alpha(Y_t)\bigr],$$

and its equivalent cost per period is $a_\alpha(x \mid s, S) = (1 - \alpha) f(x \mid s, S)$.

The renewal quantities are

$$m_\alpha(k) = \sum_{i=1}^{\infty}\alpha^i\varphi^i(k), \qquad M_\alpha(k) = \sum_{i=1}^{\infty}\alpha^i\Phi^i(k),$$

the latter being the discount renewal function,

$$L_\alpha(x, d) = G_\alpha(x) + \sum_{i=1}^{\infty}\sum_{k=0}^{d}\alpha^i G_\alpha(x - k)\varphi^i(k), \qquad r_\alpha(d) = \sum_{i=1}^{\infty}\alpha^i\bigl[\Phi^{i-1}(d) - \Phi^i(d)\bigr].$$

If $T(d)$ is the first period in which cumulative demand exceeds $d$, then $L_\alpha(x, d)$ is the expected discounted one-period cost over periods $1, \dots, T(d)$ from stock $x$ without ordering, and $r_\alpha(d) = E[\alpha^{T(d)}]$.

Formalization targets

Goal: Eq. (11)

With $D = S - s$,

$$a_\alpha(x \mid s, S) = \begin{cases} \dfrac{L_\alpha(S, D) + K}{1 + M_\alpha(D)} & x < s, \\[2ex] (1 - \alpha)L_\alpha(x, x - s) + \dfrac{L_\alpha(S, D) + K}{1 + M_\alpha(D)}\, r_\alpha(x - s) & x \ge s. \end{cases}$$

Milestones

1. Appendix §1: $M_\alpha(k) < \infty$ for $0 \le \alpha \le 1$ with $\alpha\varphi(0) < 1$.
2. Eq. (8): $L_\alpha(x, d) = G_\alpha(x) + \sum_{j=0}^{d} G_\alpha(x - j)m_\alpha(j)$.
3. Eq. (9): $r_\alpha(d) = \alpha - (1 - \alpha)M_\alpha(d)$.
4. The renewal equation $f(S) = L_\alpha(S, D) + Kr_\alpha(D) + f(S)r_\alpha(D)$.
5. $f(x) = K + f(S)$ for $x < s$.
6. $f(x) = L_\alpha(x, x - s) + Kr_\alpha(x - s) + f(S)r_\alpha(x - s)$ for $x \ge s$.
7. Eq. (10): the closed form of $f$ with denominator $1 - r_\alpha(D)$.

Significance

Eq. (11) turns the cost of an $(s, S)$ policy, an infinite series over the trajectories of a controlled Markov chain, into a finite expression in $G_\alpha$, $K$ and the renewal sequence $m_\alpha$, which the paper computes by a one-line recursion. Everything in the paper's Section 4 builds on it: the search for an optimal pair minimizes $a_\alpha(\cdot \mid s, S)$ over a finite box, and the undiscounted limit $\alpha \to 1$ gives the long-run average cost $(L_1(S, D) + K)/(1 + M_1(D))$.

The result is classical and proved in the paper. What this mission adds is a machine-checked derivation from the definition of the policy's expected cost, including the renewal step, which the paper states in one sentence ("a renewal of the process takes place"). It also produces a reusable Lean layer: discrete convolution powers, the discount renewal function, and the law of an $(s, S)$-controlled inventory chain. To the best of our knowledge none of these is formalized in Mathlib or on the platform.

Difficulty

The paper's argument conditions on the random time $T(D)$ at which the process renews and uses the strong Markov property at that time. In the formalization, $f$ is defined as a sum over periods of expectations under the law of $X_t$. Relating that sum to one that splits at the random time $T(D)$ requires either a stopping-time decomposition of the chain or an explicit accounting of the law of $X_t$ before and after the first order. Neither is a direct computation. A second difficulty is the interchange of the infinite sum over periods with the sum over states $y \in \mathbb Z$, which has infinitely many states reachable (demand is unbounded below). The renewal equation (milestone 4) alone does not determine $f(S)$ without the fact that $r_\alpha(D) < 1$ for $\alpha < 1$, which comes from (9).

Formalization scope

• Namespace VeinottWagnerSS.RenewalCost. Stock levels are integers, demands natural numbers; $x - s$ and $D = S - s$ enter $L_\alpha$, $M_\alpha$, $r_\alpha$ through Int.toNat, which is exact because the statements assume $s \le x$ or $s \le S$.
• Reduced model. The primitives are $G_\alpha$, $K$, $\alpha$ and $\varphi$, as in the paper's Eq. (2): the unit purchase cost is set to $0$ and the holding–penalty cost is replaced by $G_\alpha$.
• Demand is a real function $\varphi : \mathbb N \to \mathbb R$, non-negative and summing to $1$.
• The cost $f$ is the expected discounted cost of the controlled chain: the law of $X_t$ is built recursively from $X_1 = x$ and the transition $\Pr(X_{t+1} = z \mid X_t = y) = \varphi(Y(y) - z)$. It is not defined by (10) or by the renewal equations, and not as the solution of a fixed-point equation. A formalization in which any of milestones 4–7 or the goal holds by definition is ruled out.
• Series are real tsums. $L_\alpha$ is defined by the series (7) and $r_\alpha$ by the first line of (9), i.e. through the law $\Pr[T(d) = i] = \Phi^{i-1}(d) - \Phi^i(d)$; the paper's derivations of these series from $T(d)$ are not formalized. For $\alpha < 1$ all series converge for every $G_\alpha$, because after period $1$ the stock after ordering lies in the finite set $\{S\} \cup [s, \max(x, S)]$.
• Hypotheses. Milestones 1–3 assume $0 \le \alpha \le 1$ and $\alpha\varphi(0) < 1$, the paper's standing assumption on p. 533. Milestones 4–7 and the goal assume $0 \le \alpha < 1$, $K \ge 0$ and $s \le S$. The paper's standing assumptions that $G_\alpha$ is convex and tends to $+\infty$ as $|y| \to \infty$ are not imposed: the statements hold for every $G_\alpha$ when $\alpha < 1$, and the paper's derivation does not use them. This is a disclosed generalization.
• Printed slips. None found in the formalized statements.
• Not formalized: the recursion (A1) for $m_\alpha$, the limit (12) as $\alpha \to 1$, and the stationary analysis (13)–(20).

Contributions welcome: proofs of the milestones, general lemmas on discrete renewal sequences and convolution powers, and a first-passage decomposition for integer-valued Markov chains, which is reusable beyond this mission.

Selected references

• A. F. Veinott Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5), 525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2), 259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• K. J. Arrow, S. Karlin and H. Scarf, Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.

Motivation

A Markov-renewal program is a sequential decision model in which a system moves among finitely many states, the time between transitions is random and may depend on both the current and the next state, and a reward accrues during each sojourn. It generalizes the Markov decision process, where every transition takes one time unit, and is the standard model for maintenance, inventory and queueing control problems in which decisions are made at irregular epochs. W. S. Jewell introduced the model in two companion papers in Operations Research in 1963 (Part I, Part II).

Part II studies returns over an unbounded planning horizon. When the horizon is measured in number of transitions and rewards are not discounted, the expected return of a stationary policy grows linearly, and the paper's policy-improvement algorithm for this model rests on the precise form of that growth: a rate, the gain, and a state-dependent offset, the bias. Appendix A of Part II derives this asymptotic form from the Kemeny–Snell theory of finite Markov chains. This mission formalizes that derivation.

The result is the transition-counting counterpart of Howard's gain–bias analysis for Markov decision processes (R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960), and the fundamental matrix it uses is that of J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.

Setting

Fix a stationary policy. Only the embedded chain and the mean one-step rewards matter for the infinite-step undiscounted model (the paper, p. 961: these processes "depend only on the means"). The data are:

• a finite nonempty state set $S$ and a transition matrix $P = (p_{ij})_{i,j\in S}$ with $p_{ij}\ge 0$ and $\sum_j p_{ij} = 1$;
• the one-step expected rewards $\rho \in \mathbb R^S$ (the paper's (I 17));
• the terminal rewards $V(0)\in\mathbb R^S$.

The chain is ergodic (assumption 2, p. 951): $P$ is irreducible, meaning every state can be reached from every other state with positive probability. $P$ may be periodic. A stationary probability vector is $\pi\in\mathbb R^S$ with $\pi_i\ge 0$, $\sum_i\pi_i = 1$ and $\pi P = \pi$; $\Pi$ denotes the matrix every row of which is $\pi$.

The $n$-step return of the policy is the recursion (I 16) without the maximization:

$$V_i(n) = \rho_i + \sum_{j} p_{ij}V_j(n-1),\qquad n = 1,2,\ldots$$

The system gain is $G = \sum_i \pi_i\rho_i$ (A 6), the bias after $n$ steps is $W_i(n) = V_i(n) - Gn$, and the fundamental matrix is $Z = (I - P + \Pi)^{-1}$ (A 7).

Formalization targets

Goal: gain and Cesàro bias of the infinite-step return

For every irreducible row-stochastic $P$, stationary $\pi$, rewards $\rho$ and terminal rewards $V(0)$: the matrix $I - P + \Pi$ is invertible, and

$$\lim_{n\to\infty}\frac1n\sum_{m=1}^{n} W(m) = (Z - \Pi)\rho + \Pi V(0).$$

This is (A 4) with (A 5)–(A 7), in the form that is true for every ergodic chain and every terminal-reward vector.

Milestones

In order: the stationary vector exists, is unique and positive, and $\frac1n\sum_{k<n}P^k\to\Pi$ (Appendix A); the increment identity $V(n)-V(n-1) = P^{n-1}\rho$ (A 1) for constant $V(0)$; the Cesàro limit $\Pi\rho = G\mathbf 1$ of the increments (A 2); invertibility of $I-(P-\Pi)$ and the relations $PZ = ZP$, $\pi Z = \pi$, $I - Z = \Pi - PZ$; the Cesàro summability of $I+\sum_{j=1}^{n-1}(P^j-\Pi)$ to $Z$; the finite-$n$ bias formula (A 3) for constant $V(0)$; the relative-value equations $W_i + G = \rho_i + \sum_j p_{ij}W_j$ (4) for the limiting bias; and the paper's two-state machine example, where the four stationary policies have gains $70, 50, 80, 60$, the policy $(B,A)$ is optimal for every $n$ with $V_1(n) = 80n+170+(-1)^{n+1}170$, the limiting biases are $\pm170$, and the relative values of (5) are $340$ and $0$.

Stronger: aperiodic chains

If $P$ is moreover primitive (aperiodic), $W(n)$ itself converges to $(Z-\Pi)\rho + \Pi V(0)$. This is included as a supporting statement.

Significance

The asymptotic $V(n)\approx Gn + W$ is what makes average-reward policy improvement work: substituting it into the recursion yields the linear equations (4), whose solution (the relative values) is the test quantity of the paper's algorithm. The gain identifies which stationary policy earns most per transition in the long run, and the bias separates policies of equal gain. The same gain–bias decomposition underlies average-cost dynamic programming, the analysis of Markov reward processes, and the deviation matrix used in sensitivity analysis of Markov chains.

The result is classical and proved on paper. Formalizing it adds, first, a machine-checked account of the fundamental matrix of an irreducible, possibly periodic, finite chain: invertibility of $I - P + \Pi$, its algebraic relations and its Cesàro characterization. Mathlib has irreducible and primitive nonnegative matrices and row-stochastic matrices, but no stationary-vector uniqueness for irreducible chains, no Cesàro ergodic theorem for finite chains, and no fundamental matrix. Second, it fixes two slips of the printed appendix (below) with an exact statement. No machine-checked proof of this result is known.

Difficulty

The obvious argument writes $W(n) = \sum_{k<n}(P^k - \Pi)\rho + P^nV(0)$ and passes to the limit term by term. This fails for periodic chains: $P^k$ does not converge, $P^k - \Pi$ does not tend to zero, and the series $\sum_k (P^k - \Pi)$ does not converge. The paper's own example ($P$ swaps two states) is of this kind, and there $W(n)$ oscillates forever. What survives is Cesàro convergence, and establishing it needs control of all eigenvalues of $P$ of modulus one (they are simple roots of unity for an irreducible stochastic matrix) or an equivalent combinatorial argument. Invertibility of $I - P + \Pi$ requires that $1$ be a simple eigenvalue of $P$ with left eigenvector $\pi$, which is the Perron–Frobenius uniqueness statement for irreducible matrices; positivity of all entries of $P$, or a one-step Doeblin condition, is not available.

Formalization scope

States are a finite type with decidable equality and at least one element; vectors are S → ℝ, matrices Matrix S S ℝ, column vectors act by P *ᵥ v, the row vector $\pi$ by π ᵥ* P. Ergodicity is P ∈ Matrix.rowStochastic ℝ S ∧ P.IsIrreducible. The stationary vector is a hypothesis-constrained parameter (nonnegative, summing to one, $\pi P = \pi$), which is unique by the first milestone. $\Pi$, $G$ and $Z$ are definitions computed from $P$, $\pi$ and $\rho$, never free variables. Cesàro means are $\frac1n\sum_{m=1}^{n}$, equal to $0$ at $n = 0$. Mathlib's matrix inverse is $0$ on singular matrices, so the goal asserts invertibility of $I - P + \Pi$ explicitly.

Two printed slips are corrected, and the milestone texts are kept verbatim:

1. The paper's (A 4)–(A 5) have $+V(0)$ where iterating (I 16) gives $P^nV(0)$, whose Cesàro limit is $\Pi V(0)$. The goal uses $\Pi V(0)$; this is also the only form consistent with the paper's equation (4). Accordingly (A 1) and (A 3), which hold exactly when $PV(0) = V(0)$, carry the hypothesis that $V(0)$ is constant. The paper's example has $V(0) = 0$, where both readings agree.
2. The paper writes ordinary limits while noting that $P^{n-1}$ "converges or is Cesàro-summable". The goal and (A 2) are Cesàro limits; an ordinary limit is false for periodic chains.

The printed $\pi = \{\pi_1,\ldots,\pi_n\}$ uses $n$ for the number of states $N$.

A trivializing formalization is ruled out: $Z$ is not a junk inverse (invertibility is part of the goal), $\pi$ is a genuine stationary probability vector of $P$ rather than an arbitrary vector, $G$ is computed from $\pi$ and $\rho$, and the hypotheses are met by the paper's periodic two-state example.

Needed infrastructure: stationary vectors of irreducible stochastic matrices (existence, positivity, uniqueness), the Cesàro ergodic theorem $\frac1n\sum_{k<n}P^k\to\Pi$, and the fundamental matrix. These are reusable for any finite-chain average-reward result. Contributions proving any milestone, or the aperiodic variant, are welcome.

Selected references

• W. S. Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Operations Research 11(6), 949–971, 1963. https://doi.org/10.1287/opre.11.6.949
• W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6), 938–948, 1963. https://doi.org/10.1287/opre.11.6.938
• J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• E. Seneta, Non-negative Matrices and Markov Chains, 2nd ed., Springer, 2006. https://doi.org/10.1007/0-387-32792-4

Motivation

Many controlled systems do not move in unit time steps. A machine runs for a random time before it breaks down, a repair takes a random time, a queue sits in a state until the next arrival or departure. A Markov-renewal program (in later terminology a semi-Markov decision process) models such a system: the sequence of visited states is a Markov chain controlled by the decision maker, but each transition takes a random time and earns a reward that may depend on that time. When the horizon is long and rewards are not discounted, the natural criterion is the gain rate, the long-run expected reward per unit of time, not per transition.

Howard's policy-iteration algorithm (Howard 1960) finds a policy of maximal gain per transition for finite Markov decision processes. W. S. Jewell's Markov-Renewal Programming. II (Oper. Res. 11 (1963) 949–971) extends it to the time-average criterion. The paper's Fig. 2 gives the algorithm; pp. 954–955 state its claim: the algorithm "will find an optimal stationary policy for the infinite-time, undiscounted model, in the sense that the policy will have a gain rate, $g$, which is at least as large as that obtained for any other policy". Appendix D compares Jewell's test quantity with an alternative one proposed by P. Schweitzer, and states the identity (D 3) that measures the gain-rate improvement produced by either.

Timeline. Howard (1960) introduced policy iteration for the per-transition gain of finite Markov decision processes, and sketched a semi-Markov version. Jewell (1963, Parts I and II) developed Markov-renewal programming, with the ratio test quantity of Fig. 2 for the undiscounted time-average case. Schweitzer (unpublished MIT report, cited in Appendix D) proposed the test quantity (D 1). The ratio criterion was later treated systematically for semi-Markov decision processes (e.g. Puterman 1994, Ch. 11).

Setting

There are finitely many states $i = 1, \dots, N$ and, in each state, finitely many alternatives $z$. Under alternative $z$ in state $i$ the next state is $j$ with probability $p^z_{ij}$ ($p^z_{ij} \ge 0$, $\sum_j p^z_{ij} = 1$). The transition $i \to j$ takes a random time with finite mean $\nu^z_{ij}$, and the transition out of $i$ earns an expected reward $\rho^z_i$. The mean sojourn time is $\nu^z_i = \sum_j p^z_{ij}\nu^z_{ij}$, and it is positive.

A stationary policy $z$ picks one alternative $z(i)$ in each state. Its chain has transition matrix $P^z_{ij} = p^{z(i)}_{ij}$, and $\rho_i$, $\nu_i$ denote the data of $z(i)$. The paper's standing assumption 2 is that this chain is ergodic (irreducible) for every policy. Let $\pi$ be the stationary probability vector of $P^z$ ($\pi_i \ge 0$, $\sum_i \pi_i = 1$, $\pi P^z = \pi$). The gain rate of $z$ is (B 7):

$$g = \frac{\sum_{i=1}^{N} \pi_i \rho_i}{\sum_{k=1}^{N} \pi_k \nu_k}.$$

The value-determination equations (13) of $z$ are, in the $N+1$ unknowns $g, v_1, \dots, v_N$,

$$v_i + g\,\nu_i = \rho_i + \sum_{j=1}^{N} p_{ij} v_j \quad (i = 1, \dots, N), \qquad v_N = 0.$$

The test quantity of Fig. 2 for alternative $z$ in state $i$ is $\frac{1}{\nu^z_i}\{\rho^z_i + \sum_j p^z_{ij} v_j - v_i\}$. One cycle of the algorithm solves (13) for the current policy and then chooses, in every state, an alternative that maximizes the test quantity, retaining the current alternative when it already attains the maximum. The algorithm stops when the policy does not change.

Formalization targets

Goal: Fig. 2 terminates at a policy of maximal gain rate

For every run $z_0, z_1, \dots$ of the algorithm, from any initial policy and with any choice among tied maximizers, there is $K$ with $z_{K+1} = z_K$; and whenever $z_{K+1} = z_K$, $g_K$ is the gain rate of $z_K$ and, for every stationary policy $z'$,

$$g^{z'} = \frac{\sum_i \pi'_i \rho^{z'(i)}_i}{\sum_k \pi'_k \nu^{z'(k)}_k} \;\le\; g_K .$$

Milestones

1. (12)–(13), p. 955. The equations (13) have exactly one solution, and its $g$ equals (B 7).
2. (D 3), p. 970. For policies $A$, $B$, with $\Gamma_j$ and $\gamma_j$ the changes in the test quantities (D 1) and (D 2) computed with $A$'s $(g, v)$, and $P^B_j = \nu^B_j\pi^B_j / \sum_k \pi^B_k\nu^B_k$ the time-stationary probabilities (C 12),

$$g^B - g^A = \sum_{j} \frac{\Gamma_j}{\nu^B_j} P^B_j = \sum_j \gamma_j P^B_j .$$

3. p. 955. If the test quantity indicates a change from $z_1$ to $z_2$, then $g^{z_2} > g^{z_1}$.
4. (29)–(30), p. 961. For two states with $p_{12}, p_{21} > 0$: $g = (p_{21}\rho_1 + p_{12}\rho_2)/(\nu_1 p_{21} + \nu_2 p_{12})$ and $v_1 = (\nu_2\rho_1 - \nu_1\rho_2)/(\nu_1 p_{21} + \nu_2 p_{12})$, $v_2 = 0$.

Significance

The result makes the time-average criterion computable: a finite sequence of linear solves and pointwise maximizations produces a policy whose reward per unit time is optimal among all stationary policies. The identity (D 3) is the quantitative content: it expresses the gain-rate change as an average of local improvements, weighted by the fraction of time the new policy spends in each state. Both test quantities, Jewell's (D 2) and Schweitzer's (D 1), are covered by it. When every $\nu^z_i = 1$ the model is a Markov decision process and the algorithm is Howard's.

The result is classical and has textbook proofs for semi-Markov decision processes. The paper states the proof as "elementary" and does not write it out. None of it is machine-checked on Prove2Me, and no semi-Markov or ratio-criterion result is on the platform. The mission produces a checked account of value determination for irreducible finite chains, the improvement identity, and termination of policy iteration under ties.

Difficulty

The gain rate is a ratio, so the per-transition argument for Markov decision processes does not transfer by rescaling rewards: the denominator $\sum_k\pi_k\nu_k$ changes with the policy. Comparing two policies requires weighting local improvements by the new policy's time-stationary probabilities, and a strict improvement needs those probabilities to be positive in every state, which uses irreducibility of the new policy, not only of the current one. Termination rests on the retain-on-tie rule: without it the algorithm can cycle among tied maximizers without improving. Finally, (13) has $N+1$ unknowns and $N+1$ equations only because of the normalization $v_N = 0$; its unique solvability is a statement about the kernel and range of $I - P$ for an irreducible stochastic $P$.

Formalization scope

States are Fin N with NeZero N; the paper's state $N$ is index $N-1$ (lastState N). Alternatives form a type α; the goal assumes Fintype α and Nonempty α. The model records only $p^z_{ij}$, $\nu^z_{ij} \ge 0$ and $\rho^z_i$, with $\nu^z_i > 0$ as a field. The transition-time distributions and reward functions of the paper enter the undiscounted infinite-time model only through these means, and every such choice of means is realized by some distributions, so nothing is lost. Ergodicity is Matrix.IsIrreducible of the policy matrix for every policy. Stationary vectors are nonnegative, sum to one and satisfy $\pi P = \pi$; every statement quantifies over all of them.

The gain rate is defined by its closed form (B 7). Its identification with $\lim_{t\to\infty} v_i(t)/t$ ((B 6), argued in Appendix B from renewal theory) is not part of the mission. (13) is stated with the full sum $\sum_{j=1}^N$, equal to the paper's $\sum_{j=1}^{N-1}$ because $v_N = 0$. The paper states (D 3) for a policy $A$ "which led to an improved policy $B$"; the identity holds for any two policies and is stated that way. A run of the algorithm is a relation, not a chosen argmax: the goal quantifies over every run, so the termination claim cannot be met by a particular tie-breaking. A run begins at an arbitrary policy; the "initial set of returns" entry of Fig. 2 is a run started one cycle later.

A formalization in which the improvement step already asserts optimality, or in which termination is assumed, would be trivial; here the step only asks for pointwise maximization of the test quantity, and termination is part of the conclusion.

Needed infrastructure: stationary vectors of irreducible stochastic matrices (existence, uniqueness, strict positivity), the kernel of $I - P$, and finite-policy termination arguments. These are reusable for any finite Markov decision or semi-Markov model. Proofs of any milestone, and of the $\nu \equiv 1$ specialization, are welcome.

Selected references

• W. S. Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Operations Research 11(6), 949–971, 1963. https://doi.org/10.1287/opre.11.6.949
• W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6), 938–948, 1963. https://doi.org/10.1287/opre.11.6.938
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960. https://mitpress.mit.edu/9780262080095/
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887