A Foundational Theory of Quantitative Abstraction: Adjunctions, Duality, and Logic for Probabilistic Systems

TL;DR

The paper constructs a principled theory of quantitative abstraction for probabilistic systems by unifying category theory, coalgebra, and optimal transport. It defines a canonical, universal $\varepsilon$-quotient of the behavioral pseudo-metric $d_M$ and shows that abstractions factoring through this quotient preserve a guaranteed value-loss bound, via an abstraction-realization adjunction $Q_\varepsilon \dashv R_\varepsilon$. A quantitative modal $\mu$-calculus $\mathcal{L}_\mu$ is developed with expressive completeness for $d_M$, including a countable fragment $\mathcal{L}_\mu^c$ suitable for computation. The framework is instantiated coalgebraically on Polish spaces with the Giry monad and $W_1$, and validated through finite-MDP experiments using exact optimal transport, confirming contraction, stability, and scalability properties and linking to representation learning. Collectively, this yields a rigorous, compositional foundation for quantitative state abstraction and learning in probabilistic domains, with concrete pathways to efficient algorithms and modular system design.

Abstract

The analysis and control of stochastic dynamical systems rely on probabilistic models such as (continuous-space) Markov decision processes, but large or continuous state spaces make exact analysis intractable and call for principled quantitative abstraction. This work develops a unified theory of such abstraction by integrating category theory, coalgebra, quantitative logic, and optimal transport, centred on a canonical $\varepsilon$-quotient of the behavioral pseudo-metric with a universal property: among all abstractions that collapse behavioral differences below $\varepsilon$, it is the most detailed, and every other abstraction achieving the same discounted value-loss guarantee factors uniquely through it. Categorically, a quotient functor $Q_\varepsilon$ from a category of probabilistic systems to a category of metric specifications admits, via the Special Adjoint Functor Theorem, a right adjoint $R_\varepsilon$, yielding an adjunction $Q_\varepsilon \dashv R_\varepsilon$ that formalizes a duality between abstraction and realization; logically, a quantitative modal $μ$-calculus with separate reward and transition modalities is shown, for a broad class of systems, to be expressively complete for the behavioral pseudo-metric, with a countable fully abstract fragment suitable for computation. The theory is developed coalgebraically over Polish spaces and the Giry monad and validated on finite-state models using optimal-transport solvers, with experiments corroborating the predicted contraction properties and structural stability and aligning with the theoretical value-loss bounds, thereby providing a rigorous foundation for quantitative state abstraction and representation learning in probabilistic domains.

Figures (4)

• Figure 1: Iterative contraction of behavioral distances under $\mathcal{K}_c$. Each iteration of the behavioral operator $\mathcal{K}_c$ contracts pairwise distances by the discount factor $\gamma$. The sequence converges geometrically to the unique fixed point $d_M$, which quantifies steady-state behavioral similarity.
• Figure 2: Logic--metric duality. The behavioral pseudo-metric $d_M$ and the quantitative logic $\mathcal{L}_\mu$ determine each other: the distance between states equals the maximal deviation in formula semantics, and the logic is expressively complete for $d_M$.
• Figure 3: Universal property of the canonical $\varepsilon$-quotient. Any $\varepsilon$-collapsing non-expansive map $f:S\to T$ factors uniquely through the quotient $Q_\varepsilon:S\to S/{\!\sim_\varepsilon}$.
• Figure 4: Adjunction $Q_{\varepsilon} \dashv R_{\varepsilon}$. The functor $Q_\varepsilon$ maps concrete systems to canonical $\varepsilon$-abstractions, while $R_\varepsilon$ constructs canonical realizations of metric specifications. The adjunction establishes a duality between verifying specifications via abstractions and implementing specifications via realizations.

Theorems & Definitions (69)

• Example 1: Running Example: A Three-State Chain
• Definition 1.1: Monad
• Definition 1.2: Polish Spaces
• Remark 1.3: Why Polish Spaces Are the Natural Universe
• Definition 1.4: Borel Probability Measures and the Giry Monad
• Proposition 1.5
• proof
• Definition 1.6: 1-Wasserstein Distance
• Theorem 1.7: Kantorovich--Rubinstein Duality
• proof