PaperlayerView exact revision on arXiv

Source-linked AI summary

Memory-Dependent Interval Markov Chain Abstractions of Stochastic Dynamics

Menno van Zutphen, Adrien Banse, Domagoj Herceg, Giannis Delimpaltadakis, Duarte Antunes

arXiv:2610.02950v1eess.SYcs.SYmath.DSmath.OC

TL;DR

Continuous stochastic systems can be hard to analyze when their randomness cannot be propagated quantitatively, and state aggregation can make visited-cell processes non-Markovian. This paper develops memory-dependent and no-memory IMC constructions and derives bounds for their tightness. Its examples show tighter expected-cost bounds for memory than partition refinement in the tested settings, without establishing a universal ordering.

  • Problem

    Strong nonlinearities can make stochasticity difficult to propagate quantitatively, while aggregating states can make the visited-cell process non-Markovian.

    Source: §1 · p. 2

  • Method

    The paper constructs memory-dependent IMC abstractions using filtering to restrict conditional state measures, and also formulates a no-memory construction.

    Source: §1 · p. 2, §6 · p. 14

  • Results

    Memory yields substantially tighter expected-cost widths than partition refinement on the linear-Gaussian benchmark at equal transition-storage complexity, while no general ordering is established.

    Source: §6 · p. 15

  • Takeaways & Limitations

    Memory is an alternative to partition refinement, but the relative effectiveness of the two depends on system properties not yet characterized by the bounds.

    Source: §6 · p. 15

    The derived upper bounds do not order exact expected-cost interval widths or provide criteria for choosing memory versus finer partitions at a given complexity budget.

    Source: §6 · p. 15

Abstract

from arXiv · show

Finite-state interval Markov-chain (IMC) abstractions provide sound verification and performance bounds for continuous-state stochastic systems by enclosing cell-to-cell transition probabilities and costs in intervals. Finite-state Markovian abstractions are generally lossy, as state aggregation often destroys the Markov property. Recently, memory-dependent Markov-chain (MC) abstractions of stochastic systems have been developed to mitigate this by recording recently visited cells. In this paper, we develop the memory-dependent extension of IMC abstractions. Building on the insight that memory narrows the family of state distributions that could occur inside the current cell, we prove that memory tightens the local intervals, at the price of a larger abstraction. We also formulate no-memory IMC abstractions, tightening classic IMC abstraction intervals without enlarging the state space. To characterize spatial refinement relative to memory, we derive two cost-guarantee tightness upper bounds. The bounds depend, respectively, on cell size, and on the worst-case remaining distributional ambiguity after filtering over the remembered past. We then specialize our result to linear-Gaussian systems, for which we derive a closed-form upper bound on this ambiguity. Numerical examples show that the memory-dependent and no-memory constructions can produce tighter expected-cost intervals than comparable partition refined models.

1 Introduction

Finite-state IMC abstractions support sound analysis of stochastic systems, but aggregation can erase the Markov property. This paper extends them with memory-dependent and no-memory constructions, analyzes how memory and refinement tighten expected-cost bounds, and compares them experimentally.

1 Introduction

  • Finite-state abstractions replace continuous stochastic processes with discrete ones while retaining quantitative guarantees, addressing cases where stochasticity is difficult to propagate over time.The cited motivation includes strong nonlinearities and formal verification or performance analysis needs.Source: §1 · pp. 1–2
  • Earlier stochastic memory-dependent abstractions used Markov chains with a-posteriori approximation-error guarantees, whereas this paper develops an interval-valued counterpart.The cited prior approach relies on restrictive regularity assumptions and can yield conservative error quantifications [3].Source: §1 · p. 2
  • Filtering restricts admissible conditional state measures, so memory narrows those families and tightens stage-cost and transition intervals; zero memory recovers classic IMCs.The tighter intervals come at the expense of increased computational complexity.Source: §1 · pp. 2–3
  • For fixed horizons, the partition-refinement width bound vanishes with refined-cell diameter, while the linear-Gaussian memory bound decays with memory length when κ < 1.The bounds capture distinct mechanisms: smaller cells reduce geometric variation, while memory reduces worst-case remaining distributional ambiguity.Source: §1 · p. 3
  • Memory-dependent constructions produce substantially tighter expected-cost bounds than partition refinement in the reported examples, but neither approach is universally superior.The comparison uses equal stored transition-interval counts on the linear-Gaussian benchmark; the simple nonlinear example also favors memory.Source: §1 · p. 3

2 Concrete system and abstraction problem

The section sets up finite-horizon continuous-state and finite-state Markov models, then defines interval abstractions and their robust cost bounds. Its abstraction objective is sound containment of the concrete expected cost, with tighter intervals preferred.

2 Concrete system and abstraction problem

  • The paper studies continuous-state Markov chains over a fixed finite horizon, with an initial-state measure, transition kernel, and bounded measurable stage cost.The abstraction approach remembers the ℓ previous abstract cells to tighten the resulting bounds.Source: §2 · p. 3, §2.1 · p. 3

2.1 Preliminaries

  • An IMC specifies admissible intervals for stage costs and transition probabilities, representing a family of time-varying Markov chains whose extrema are computed by robust dynamic programming.The interval model's robust bounds characterize the minimum and maximum expected cumulative costs across the represented chains.Source: §2.1 · p. 4

2.2 The abstraction problem

  • The abstraction problem is to construct a finite-state IMC whose robust expected-cost bounds contain the concrete system's expected cumulative cost.Among sound abstractions, the section prefers narrower expected-cost intervals.Source: §2.2 · p. 5

3 Memory-dependent and no-memory IMC abstractions

The section constructs sound memory-dependent and no-memory IMC abstractions by filtering over information about the concrete process. Remembering past cells tightens local cost and transition intervals, while the no-memory construction uses that information without enlarging the state space.

3.1 Memory-dependent IMC abstractions

  • A memory state retains the current refined cell and ℓ preceding cells, and the resulting cost and transition intervals condition on the remembered path.The memory-conditioned measure uses the remembered tail event and an admissible concrete starting state in the oldest cell.Source: §3 · p. 5, §3.1 · pp. 5–6
  • Memory-dependent abstractions are sound, and conditioning on memory cannot widen local cost or transition intervals relative to the classic interval for the current cell.At ℓ = 0, the construction reduces to the classic IMC abstraction.Source: §3.1 · pp. 7–8

3.2 No-memory abstractions

  • The no-memory abstraction relaxes the remembered-cell constraints while retaining additional transition-kernel information, so its state space remains the refined partition R.It is constructed separately from the memory-dependent abstraction; the mixture argument also establishes its soundness.Source: §3.2 · pp. 8–10

4 Bounding the robust value-function widths

The section bounds robust value-function width under memory and partition refinement, then derives a computable linear-Gaussian memory bound. It also accounts for unbounded linear-Gaussian state spaces by truncating them and correcting the resulting cost bounds for exits.

4.1 Bounding the general robust value-function width

  • For fixed horizon, the partition-refinement upper bound vanishes as refined-cell diameter approaches zero.Source: §4.1 · p. 10
  • Under Lipschitz cost and transition-density sensitivity assumptions, the bounds relate robust value-function width to memory length or partition refinement, without generally ordering the two methods.Partition refinement acts through cell diameter; memory acts through the remaining distributional ambiguity after conditioning on remembered states.Source: §4.1 · pp. 10–11
  • The worst-case remaining distributional ambiguity is nonincreasing with memory length, and the memory bound can vanish as that ambiguity tends to zero at fixed remaining horizon.The paper notes that this ambiguity is not immediately computable, motivating its later linear-Gaussian bound.Source: §4.1 · pp. 10–11

4.2 Linear-Gaussian systems

  • The linear-Gaussian bounds are applied to unbounded processes by compact truncation with an absorbing overflow state, then correcting cost bounds for the probability of exiting the truncated region.The augmented process preserves transitions inside the retained set and assigns exits to the absorbing state; verified exit-probability bounds may be used in the correction.Source: §4.2 · p. 12

4.2.1 Linear-Gaussian width bounds

  • For linear-Gaussian dynamics, the paper derives a computable memory-width bound whose contraction factor κ determines whether the bound decays with memory length.When κ < 1, the bound vanishes along full-memory stages as memory length grows with fixed remaining horizon; an expansive A and coarse grid relative to noise can make κ ≥ 1 and leave only the trivial bound.Source: §4.2.1 · pp. 12–13
  • The memory-width result is an upper bound: a large κ makes the bound uninformative, but does not establish that memory lengthening fails to tighten the abstraction.The relative sizes of the memory and refinement bounds also do not directly order the exact widths.Source: §4.1 · p. 11, §4.2.1 · p. 13

5 Numerical examples

The examples compare classic, no-memory, memory-dependent, and partition-refined IMC abstractions at different transition-interval budgets. In both examples, the memory-dependent construction yields tighter expected-cost bounds than partition refinement in the reported comparisons.

5 Numerical examples

  • The authors compare four IMC abstractions—classic, no-memory, memory-dependent, and partition-refined classic—on a linear-Gaussian variation and Example 3.4, using stored transition-probability intervals as the complexity measure.For Example 3.4 at M = 2, they evaluate at H = 16; memory-dependent gives tightest bounds, followed by no-memory, partition refinement, and baseline.Source: §5 · p. 13, §5.2 · p. 14

5.1 Linear-Gaussian benchmark

  • 10.6731 for partition refinement versus 1.5295 for the memory-dependent abstraction: the latter has the narrower expected-cost interval at matched complexity.The comparison is for the modified linear-Gaussian system at H = 16; both constructions store 531,441 non-absorbing transition probability intervals.Source: §5.1 · p. 13, Figure 5 · p. 14

5.2 Simple example system

  • In Example 3.4, the memory-dependent abstraction is tightest, followed by no-memory, partition refinement, and the baseline.The comparison uses 8 shift-compatible intervals for memory, 16 for partition refinement, and 4 each for the baseline and no-memory constructions; predicting the tighter approach beforehand remains unresolved.Source: Figure 6 · p. 14, §5.2 · p. 14

6 Conclusions and future work

The paper develops memory-dependent and no-memory IMC constructions and bounds how their expected-cost intervals tighten relative to partition refinement. Numerical examples favor memory in the reported comparisons, while a general ordering of exact widths remains unresolved.

6 Conclusions and future work

  • Memory-dependent and no-memory IMC constructions yield sound finite-horizon expected-cost bounds, with memory conditioning tightening local cost and transition intervals.The no-memory construction uses transition-kernel information without enlarging the abstract state space.Source: §6 · p. 14
  • Under Lipschitz assumptions, robust value-function width bounds depend on refined-cell diameter or remaining distributional ambiguity; linear-Gaussian dynamics provide a computable coefficient for geometric decay when κ < 1.The decay claim applies along full-memory stages with fixed remaining horizon.Source: §6 · p. 15
  • On the linear-Gaussian benchmark, memory yields substantially tighter expected-cost widths than partition refinement at equal transition-storage complexity; on the simple system, it yields substantially tighter bounds with fewer stored intervals.The examples support memory as an alternative to partition refinement, not a general ordering of their widths.Source: §6 · p. 15
  • The derived upper bounds do not order exact expected-cost interval widths, leaving criteria for choosing memory versus finer partitions at a fixed complexity budget unresolved.The paper identifies this comparison as a direction for future work.Source: §6 · p. 15
  • The presented canonical form assumes uniform partitioning across all state-space dimensions, and memory length also makes partition choices affect remembered-state information.A systematic binning optimization approach is not yet available in the literature, according to the paper.Source: §6 · p. 15

A Technical results and proofs

The proofs construct a finite-state Markov-chain clone of the observed process and show that its costs and transitions are admissible in the memory-dependent IMC. They then bound abstraction widths and specialize the ambiguity analysis to linear-Gaussian dynamics.

A Technical results and proofs

  • The time-varying finite-state clone matches the observed process's state marginals and expected cost, and its costs and transitions are admissible under the memory-dependent IMC.These properties establish the soundness claim.Source: A Technical results and proofs · pp. 15–16
  • Under the stated Lipschitz bounds, memory-dependent local cost and transition widths scale with ∆ℓ, while partition-refined bounds scale with cell diameter dM/N.The proof propagates these local bounds through the robust Bellman recursion.Source: A Technical results and proofs · pp. 17–18
  • Memory-dependent ambiguity is nonincreasing with memory length, and the linear-Gaussian analysis gives an isotropic-noise contraction factor determined by the dynamics, grid diameter, and noise scale.In the isotropic case, κ is ∥A∥2 when dM ≥ 2σ and ∥A∥2dM^2/(4σ^2) when dM < 2σ.Source: A Technical results and proofs · pp. 18, 21
  • The trajectories and accumulated costs agree before τX; at every later stage, the original-process cost minus cmin lies in [0, Cc], yielding a pathwise comparison whose expectation proves (17).Source: A Technical results and proofs · p. 18
  • Backward-tail conditioning yields kernels for the path conditioned on remembered cells, and the resulting conditioned sequence is Markov when its oldest state is fixed.This provides the filtering structure used in the memory-dependent ambiguity analysis.Source: A Technical results and proofs · pp. 19–20
Loading 2610.02950v1…