A decision walk decomposes into a simple path and simple cycles
ProvedMDPComplexity.StationaryHorizon.cycle_decompositioncombinatoricsgraph-theoryp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1walks
Let be an -arc walk in a finite stationary deterministic process. There are a simple path and a finite list of simple cycles such that has the same initial and final states as , every cycle is based at a state visited by , the cycles and path use exactly the multiset of decision arcs in , and
This records the length and cost preservation of the cycle removal described before Theorem 5.
Formalization Note The list records cycles with multiplicity. A loop is a simple cycle of one arc. The decomposition records the attachment state of each removed cycle. Equality of arc multisets distinguishes parallel decisions.
Preamble
import Mathlib import Definitions.Def_MDPComplexity_StationaryHorizon_Model
Formal statement
namespace MDPComplexity.StationaryHorizon
variable {S : Type} [Fintype S]
/-- §3, p. 447: repeatedly removing the first simple cycle leaves a simple path.
The recorded cycles preserve the original walk's arc count and cost. -/
theorem cycle_decomposition (M : DetMDP S) {l : ℕ} (W : M.Walk l) :
∃ (p : ℕ) (P : M.Walk p) (Cs : List (Σ k : ℕ, M.Walk k)),
M.IsCycleDecomposition W P Cs := by sorry
end MDPComplexity.StationaryHorizon
Source
Papadimitriou and Tsitsiklis, The Complexity of Markov Decision Processes, Math. Oper. Res. 12(3) (1987), p. 447, §3 The finite horizon, stationary case, cycle-removal paragraph, https://doi.org/10.1287/moor.12.3.441
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.