Source
Calo, Jonsson, Neu, Schwartz and Segovia-Aguas (2024), LIT-962, read in NOTE-757: §2 (Eqs. 2–5), §3 (Lemma 1, Theorem 1), Appendix A.1 and Appendix B (Theorem 3 and the proof of Lemma 1).
What was actually shown
The setting. Take two finite stationary Markov chains M_X and M_Y, with fixed initial states, a ground cost c on state pairs and γ ∈ (0, 1). The transport distance is W_γ = inf ∫ Σ_t γ^t c(X_t, Y_t) dM_XY over bicausal couplings: joint processes in which, given the joint past, each chain’s next state keeps its own law.
The Bellman form (Theorem 3, after Moulos 2021). The infimum is attained by a stationary transition coupling. W_γ(x, y) is the unique solution of V(xy) = c(xy) + γ inf_{p ∈ Π_xy} Σ p(x’y’) V(x’y’), where Π_xy is the set of couplings of P_X(·|x) and P_Y(·|y). The proof is an application of Bertsekas (1977).
The identification (§2.2). For a chain with no actions, the bisimulation metric of Ferns et al. is the unique solution of U(xy) = (1−γ)|r(x)−r(y)| + γ inf_{p ∈ Π_xy} Σ p(x’y’) U(x’y’). That is the same equation with c(xy) = (1−γ)|r(x)−r(y)|, so U = W_γ. This could have failed: had the bisimulation metric’s step been anything other than an optimal coupling of next-state laws with this cost, the equations would differ. The equality of this fixed point with the logical definition (a supremum over a grammar of functional expressions) is van Breugel and Worrell’s theorem, cited.
The finite LP (Lemma 1, Theorem 1). Let µ(xy, x’y’) be the discounted frequency of the transition from pair xy to pair x’y’. A distribution µ on (X×Y)² arises from a valid transition coupling if and only if it satisfies three linear systems:
- the flow constraint;
- coherence with P_X;
- coherence with P_Y.
Then W_γ = (1/(1−γ)) min ⟨µ, c⟩ over that polytope, a program with |X|²|Y|² variables. The “if” direction is proved by building π_µ = µ/ν_µ and showing that the flow equations have a unique solution, since I − γZ is invertible.
What this does not say
- Not for systems with actions. The chains have no inputs. The identification is for action-free labelled Markov chains. Ferns et al.’s MDP metric, which takes a maximum over actions, is mentioned and not recast as transport. A communicative system updated by a chosen utterance is the action case.
- Not that the fixed point is the logical bisimulation metric. The equality of this fixed point with the Desharnais–van Breugel–Worrell metric, a supremum over a grammar of functional expressions, is van Breugel and Worrell’s theorem, cited in LIT-962 and not proved there (NOTE-757, claim C6, “second-hand”). This THEORY holds the fixed-point form only.
- Not a new proof that the metric characterises bisimilarity. That distance zero means bisimilar is cited from van Breugel and Worrell (2001) and Desharnais et al. (2002). Calo et al. do not reprove it.
- Not a comparison with trace equivalence. The only statement about traces is second-hand: Bian and Abate (2017) show that near-bisimilar implies close finite-trace distributions, and the converse “is not shown to hold”. The paper does not say that dropping bicausality yields a trace distance. The record may want to argue that (see QUESTION-008), but it is not shown here.
- Not efficient computation in the strong sense. The strongly polynomial solvability of the LP is asserted via Ye (2011), not proved. Sinkhorn Value Iteration’s iteration bound, K ≥ 324 ‖c‖²∞ log(|X||Y|)/((1−γ)⁵ε²), holds only with exact inner fixed points. The authors call removing that condition a conjecture.
- Not undiscounted or weak bisimulation. γ < 1 throughout. The weak-bisimulation metric (Desharnais et al. 2002) is not treated.
Connections
- QUESTION-008 (Deferred) asks whether pragmatic fidelity is
approximate bisimulation. This THEORY supplies the formal object for the
action-free case: approximate bisimulation as a transport cost over
couplings that may not anticipate. It does not answer the question,
which needs actions and a judgement that observational equivalence
(TERM-033) gets wrong. No
answers:relation is filed. - CLAIM-034. The metric is symmetric. The one-way simulation that CLAIM-034 calls for would need an asymmetric (simulation) metric, which the paper does not give.
- THEORY-280 builds on this LP and makes the same quantity estimable from samples.
Note of 2026-10-19: the two checks, by an independent route
The identification. For any cost c, define (T V)(xy) = c(xy) + γ min over p in Π_xy of Σ p(x′y′) V(x′y′). A minimum of linear functionals over one fixed set is 1-Lipschitz in sup norm, since each p is a probability vector. So ‖T V − T W‖∞ ≤ γ ‖V − W‖∞, and T has a unique fixed point. With c(xy) = (1−γ)|r(x) − r(y)|, Eq. 3 and Eq. 5 are the same operator, so their unique fixed points coincide.
Lemma 1, as an occupancy-measure LP. Read the pairs xy as the states of a finite MDP whose actions at xy are the couplings in Π_xy. A stationary coupling π gives an occupancy measure µ_π that satisfies the flow constraint and both coherence constraints. Conversely, take a feasible µ with pair marginal ν. Where ν > 0, set π = µ/ν, and take any coupling elsewhere. Coherence makes π a coupling of the two next-state laws. Then ν solves νᵀ = (1−γ)δᵀ + γνᵀZ_π, and I − γZ_π is invertible, so that solution is unique and µ = µ_π. The objective ⟨µ, c⟩ is the discounted cost of π times (1−γ), so the LP’s minimum is (1−γ)W_γ, by Theorem 3. This is the textbook occupancy-measure argument, not the paper’s own text.